Metamath Proof Explorer


Theorem sqeqori

Description: The squares of two complex numbers are equal iff one number equals the other or its negative. Lemma 15-4.7 of Gleason p. 311 and its converse. (Contributed by NM, 15-Jan-2006)

Ref Expression
Hypotheses binom2.1 A
binom2.2 B
Assertion sqeqori A 2 = B 2 A = B A = B

Proof

Step Hyp Ref Expression
1 binom2.1 A
2 binom2.2 B
3 1 2 subsqi A 2 B 2 = A + B A B
4 3 eqeq1i A 2 B 2 = 0 A + B A B = 0
5 1 sqcli A 2
6 2 sqcli B 2
7 5 6 subeq0i A 2 B 2 = 0 A 2 = B 2
8 1 2 addcli A + B
9 1 2 subcli A B
10 8 9 mul0ori A + B A B = 0 A + B = 0 A B = 0
11 4 7 10 3bitr3i A 2 = B 2 A + B = 0 A B = 0
12 orcom A + B = 0 A B = 0 A B = 0 A + B = 0
13 1 2 subeq0i A B = 0 A = B
14 1 2 subnegi A B = A + B
15 14 eqeq1i A B = 0 A + B = 0
16 2 negcli B
17 1 16 subeq0i A B = 0 A = B
18 15 17 bitr3i A + B = 0 A = B
19 13 18 orbi12i A B = 0 A + B = 0 A = B A = B
20 11 12 19 3bitri A 2 = B 2 A = B A = B