Identity: Let $R$ be a ring and $x \in R$. Then $x^2=(-x)^2.$
It's exam marking time here, and one of the students used the above identity in a proof. The identity is true, but I can't think of a straightforward proof of this.
Question: Is there a short proof of this identity? (Note: $R$ might not have a multiplicative identity.)
Here's a proof generated by Prover9, which makes me think there might not be a shorter proof. However, this might not necessarily be true, since Prover9 can only work with the ring theory axioms I input (and would have to prove any auxiliary lemmata we would take for granted).
============================== PROOF ================================= % Proof 1 at 0.01 (+ 0.00) seconds. % Length of proof is 26. % Level of proof is 10. % Maximum clause weight is 16. % Given clauses 30. 1 x * x = -x * -x # label(non_clause) # label(goal). [goal]. 2 x + (y + z) = (x + y) + z. [assumption]. 3 (x + y) + z = x + (y + z). [copy(2),flip(a)]. 4 x + 0 = x. [assumption]. 5 0 + x = x. [assumption]. 6 x + -x = 0. [assumption]. 8 x + y = y + x. [assumption]. 10 x * (y + z) = (x * y) + (x * z). [assumption]. 11 (x + y) * z = (x * z) + (y * z). [assumption]. 12 -c1 * -c1 != c1 * c1. [deny(1)]. 13 x + (-x + y) = y. [para(6(a,1),3(a,1,1)),rewrite([5(2)]),flip(a)]. 18 (x * 0) + (x * y) = x * y. [para(5(a,1),10(a,1,2)),flip(a)]. 19 (x * y) + (x * -y) = x * 0. [para(6(a,1),10(a,1,2)),flip(a)]. 24 --x = x. [para(6(a,1),13(a,1,2)),rewrite([4(2)]),flip(a)]. 25 x + (y + -x) = y. [para(8(a,1),13(a,1,2))]. 27 (x * y) + ((-x * y) + (z * y)) = z * y. [para(13(a,1),11(a,1,1)),rewrite([11(5)]),flip(a)]. 33 -x + (y + x) = y. [para(24(a,1),25(a,1,2,2))]. 40 x + -(x + y) = -y. [para(33(a,1),33(a,1,2)),rewrite([8(3)])]. 57 -(x + y) = -y + -x. [para(33(a,1),40(a,1,2,1)),flip(a)]. 69 x * 0 = 0. [para(18(a,1),33(a,1,2)),rewrite([8(4),6(4)]),flip(a)]. 70 (x * y) + (x * -y) = 0. [back_rewrite(19),rewrite([69(6)])]. 78 -(x * -y) = x * y. [para(70(a,1),33(a,1,2)),rewrite([8(5),5(5)])]. 87 x * -y = -(x * y). [para(78(a,1),24(a,1,1)),flip(a)]. 88 -(-c1 * c1) != c1 * c1. [back_rewrite(12),rewrite([87(5)])]. 101 -(-x * y) = x * y. [para(27(a,1),33(a,1,2)),rewrite([57(5),8(8),13(8)])]. 102 $F. [resolve(101,a,88,a)]. ============================== end of proof ==========================