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 e. CC
binom2.2
|- B e. CC
Assertion sqeqori
|- ( ( A ^ 2 ) = ( B ^ 2 ) <-> ( A = B \/ A = -u B ) )

Proof

Step Hyp Ref Expression
1 binom2.1
 |-  A e. CC
2 binom2.2
 |-  B e. CC
3 1 2 subsqi
 |-  ( ( A ^ 2 ) - ( B ^ 2 ) ) = ( ( A + B ) x. ( A - B ) )
4 3 eqeq1i
 |-  ( ( ( A ^ 2 ) - ( B ^ 2 ) ) = 0 <-> ( ( A + B ) x. ( A - B ) ) = 0 )
5 1 sqcli
 |-  ( A ^ 2 ) e. CC
6 2 sqcli
 |-  ( B ^ 2 ) e. CC
7 5 6 subeq0i
 |-  ( ( ( A ^ 2 ) - ( B ^ 2 ) ) = 0 <-> ( A ^ 2 ) = ( B ^ 2 ) )
8 1 2 addcli
 |-  ( A + B ) e. CC
9 1 2 subcli
 |-  ( A - B ) e. CC
10 8 9 mul0ori
 |-  ( ( ( A + B ) x. ( 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 - -u B ) = ( A + B )
15 14 eqeq1i
 |-  ( ( A - -u B ) = 0 <-> ( A + B ) = 0 )
16 2 negcli
 |-  -u B e. CC
17 1 16 subeq0i
 |-  ( ( A - -u B ) = 0 <-> A = -u B )
18 15 17 bitr3i
 |-  ( ( A + B ) = 0 <-> A = -u B )
19 13 18 orbi12i
 |-  ( ( ( A - B ) = 0 \/ ( A + B ) = 0 ) <-> ( A = B \/ A = -u B ) )
20 11 12 19 3bitri
 |-  ( ( A ^ 2 ) = ( B ^ 2 ) <-> ( A = B \/ A = -u B ) )