Metamath Proof Explorer

Theorem sqeqor

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 Paul Chapman, 15-Mar-2008)

Ref Expression
Assertion sqeqor 
|- ( ( A e. CC /\ B e. CC ) -> ( ( A ^ 2 ) = ( B ^ 2 ) <-> ( A = B \/ A = -u B ) ) )

Proof

Step Hyp Ref Expression
1 oveq1 
 |-  ( A = if ( A e. CC , A , 0 ) -> ( A ^ 2 ) = ( if ( A e. CC , A , 0 ) ^ 2 ) )
2 1 eqeq1d 
 |-  ( A = if ( A e. CC , A , 0 ) -> ( ( A ^ 2 ) = ( B ^ 2 ) <-> ( if ( A e. CC , A , 0 ) ^ 2 ) = ( B ^ 2 ) ) )
3 eqeq1 
 |-  ( A = if ( A e. CC , A , 0 ) -> ( A = B <-> if ( A e. CC , A , 0 ) = B ) )
4 eqeq1 
 |-  ( A = if ( A e. CC , A , 0 ) -> ( A = -u B <-> if ( A e. CC , A , 0 ) = -u B ) )
5 3 4 orbi12d 
 |-  ( A = if ( A e. CC , A , 0 ) -> ( ( A = B \/ A = -u B ) <-> ( if ( A e. CC , A , 0 ) = B \/ if ( A e. CC , A , 0 ) = -u B ) ) )
6 2 5 bibi12d 
 |-  ( A = if ( A e. CC , A , 0 ) -> ( ( ( A ^ 2 ) = ( B ^ 2 ) <-> ( A = B \/ A = -u B ) ) <-> ( ( if ( A e. CC , A , 0 ) ^ 2 ) = ( B ^ 2 ) <-> ( if ( A e. CC , A , 0 ) = B \/ if ( A e. CC , A , 0 ) = -u B ) ) ) )
7 oveq1 
 |-  ( B = if ( B e. CC , B , 0 ) -> ( B ^ 2 ) = ( if ( B e. CC , B , 0 ) ^ 2 ) )
8 7 eqeq2d 
 |-  ( B = if ( B e. CC , B , 0 ) -> ( ( if ( A e. CC , A , 0 ) ^ 2 ) = ( B ^ 2 ) <-> ( if ( A e. CC , A , 0 ) ^ 2 ) = ( if ( B e. CC , B , 0 ) ^ 2 ) ) )
9 eqeq2 
 |-  ( B = if ( B e. CC , B , 0 ) -> ( if ( A e. CC , A , 0 ) = B <-> if ( A e. CC , A , 0 ) = if ( B e. CC , B , 0 ) ) )
10 negeq 
 |-  ( B = if ( B e. CC , B , 0 ) -> -u B = -u if ( B e. CC , B , 0 ) )
11 10 eqeq2d 
 |-  ( B = if ( B e. CC , B , 0 ) -> ( if ( A e. CC , A , 0 ) = -u B <-> if ( A e. CC , A , 0 ) = -u if ( B e. CC , B , 0 ) ) )
12 9 11 orbi12d 
 |-  ( B = if ( B e. CC , B , 0 ) -> ( ( if ( A e. CC , A , 0 ) = B \/ if ( A e. CC , A , 0 ) = -u B ) <-> ( if ( A e. CC , A , 0 ) = if ( B e. CC , B , 0 ) \/ if ( A e. CC , A , 0 ) = -u if ( B e. CC , B , 0 ) ) ) )
13 8 12 bibi12d 
 |-  ( B = if ( B e. CC , B , 0 ) -> ( ( ( if ( A e. CC , A , 0 ) ^ 2 ) = ( B ^ 2 ) <-> ( if ( A e. CC , A , 0 ) = B \/ if ( A e. CC , A , 0 ) = -u B ) ) <-> ( ( if ( A e. CC , A , 0 ) ^ 2 ) = ( if ( B e. CC , B , 0 ) ^ 2 ) <-> ( if ( A e. CC , A , 0 ) = if ( B e. CC , B , 0 ) \/ if ( A e. CC , A , 0 ) = -u if ( B e. CC , B , 0 ) ) ) ) )
14 0cn 
 |-  0 e. CC
15 14 elimel 
 |-  if ( A e. CC , A , 0 ) e. CC
16 14 elimel 
 |-  if ( B e. CC , B , 0 ) e. CC
17 15 16 sqeqori 
 |-  ( ( if ( A e. CC , A , 0 ) ^ 2 ) = ( if ( B e. CC , B , 0 ) ^ 2 ) <-> ( if ( A e. CC , A , 0 ) = if ( B e. CC , B , 0 ) \/ if ( A e. CC , A , 0 ) = -u if ( B e. CC , B , 0 ) ) )
18 6 13 17 dedth2h 
 |-  ( ( A e. CC /\ B e. CC ) -> ( ( A ^ 2 ) = ( B ^ 2 ) <-> ( A = B \/ A = -u B ) ) )