Metamath Proof Explorer

Theorem sqeqd

Description: A deduction for showing two numbers whose squares are equal are themselves equal. (Contributed by Mario Carneiro, 3-Apr-2015)

Ref Expression
Hypotheses sqeqd.1 
|- ( ph -> A e. CC )
sqeqd.2 
|- ( ph -> B e. CC )
sqeqd.3 
|- ( ph -> ( A ^ 2 ) = ( B ^ 2 ) )
sqeqd.4 
|- ( ph -> 0 <_ ( Re ` A ) )
sqeqd.5 
|- ( ph -> 0 <_ ( Re ` B ) )
sqeqd.6 
|- ( ( ph /\ ( Re ` A ) = 0 /\ ( Re ` B ) = 0 ) -> A = B )
Assertion sqeqd 
|- ( ph -> A = B )

Proof

Step Hyp Ref Expression
1 sqeqd.1 
 |-  ( ph -> A e. CC )
2 sqeqd.2 
 |-  ( ph -> B e. CC )
3 sqeqd.3 
 |-  ( ph -> ( A ^ 2 ) = ( B ^ 2 ) )
4 sqeqd.4 
 |-  ( ph -> 0 <_ ( Re ` A ) )
5 sqeqd.5 
 |-  ( ph -> 0 <_ ( Re ` B ) )
6 sqeqd.6 
 |-  ( ( ph /\ ( Re ` A ) = 0 /\ ( Re ` B ) = 0 ) -> A = B )
7 sqeqor 
 |-  ( ( A e. CC /\ B e. CC ) -> ( ( A ^ 2 ) = ( B ^ 2 ) <-> ( A = B \/ A = -u B ) ) )
8 1 2 7 syl2anc 
 |-  ( ph -> ( ( A ^ 2 ) = ( B ^ 2 ) <-> ( A = B \/ A = -u B ) ) )
9 3 8 mpbid 
 |-  ( ph -> ( A = B \/ A = -u B ) )
10 9 ord 
 |-  ( ph -> ( -. A = B -> A = -u B ) )
11 simpl 
 |-  ( ( ph /\ A = -u B ) -> ph )
12 fveq2 
 |-  ( A = -u B -> ( Re ` A ) = ( Re ` -u B ) )
13 reneg 
 |-  ( B e. CC -> ( Re ` -u B ) = -u ( Re ` B ) )
14 2 13 syl 
 |-  ( ph -> ( Re ` -u B ) = -u ( Re ` B ) )
15 12 14 sylan9eqr 
 |-  ( ( ph /\ A = -u B ) -> ( Re ` A ) = -u ( Re ` B ) )
16 4 adantr 
 |-  ( ( ph /\ A = -u B ) -> 0 <_ ( Re ` A ) )
17 16 15 breqtrd 
 |-  ( ( ph /\ A = -u B ) -> 0 <_ -u ( Re ` B ) )
18 2 adantr 
 |-  ( ( ph /\ A = -u B ) -> B e. CC )
19 recl 
 |-  ( B e. CC -> ( Re ` B ) e. RR )
20 18 19 syl 
 |-  ( ( ph /\ A = -u B ) -> ( Re ` B ) e. RR )
21 20 le0neg1d 
 |-  ( ( ph /\ A = -u B ) -> ( ( Re ` B ) <_ 0 <-> 0 <_ -u ( Re ` B ) ) )
22 17 21 mpbird 
 |-  ( ( ph /\ A = -u B ) -> ( Re ` B ) <_ 0 )
23 5 adantr 
 |-  ( ( ph /\ A = -u B ) -> 0 <_ ( Re ` B ) )
24 0re 
 |-  0 e. RR
25 letri3 
 |-  ( ( ( Re ` B ) e. RR /\ 0 e. RR ) -> ( ( Re ` B ) = 0 <-> ( ( Re ` B ) <_ 0 /\ 0 <_ ( Re ` B ) ) ) )
26 20 24 25 sylancl 
 |-  ( ( ph /\ A = -u B ) -> ( ( Re ` B ) = 0 <-> ( ( Re ` B ) <_ 0 /\ 0 <_ ( Re ` B ) ) ) )
27 22 23 26 mpbir2and 
 |-  ( ( ph /\ A = -u B ) -> ( Re ` B ) = 0 )
28 27 negeqd 
 |-  ( ( ph /\ A = -u B ) -> -u ( Re ` B ) = -u 0 )
29 neg0 
 |-  -u 0 = 0
30 28 29 eqtrdi 
 |-  ( ( ph /\ A = -u B ) -> -u ( Re ` B ) = 0 )
31 15 30 eqtrd 
 |-  ( ( ph /\ A = -u B ) -> ( Re ` A ) = 0 )
32 11 31 27 6 syl3anc 
 |-  ( ( ph /\ A = -u B ) -> A = B )
33 32 ex 
 |-  ( ph -> ( A = -u B -> A = B ) )
34 10 33 syld 
 |-  ( ph -> ( -. A = B -> A = B ) )
35 34 pm2.18d 
 |-  ( ph -> A = B )