This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 ) )