Metamath Proof Explorer

Theorem eqsqrtd

Description: A deduction for showing that a number equals the square root of another. (Contributed by Mario Carneiro, 3-Apr-2015)

Ref Expression
Hypotheses eqsqrtd.1 
|- ( ph -> A e. CC )
eqsqrtd.2 
|- ( ph -> B e. CC )
eqsqrtd.3 
|- ( ph -> ( A ^ 2 ) = B )
eqsqrtd.4 
|- ( ph -> 0 <_ ( Re ` A ) )
eqsqrtd.5 
|- ( ph -> -. ( _i x. A ) e. RR+ )
Assertion eqsqrtd 
|- ( ph -> A = ( sqrt ` B ) )

Proof

Step Hyp Ref Expression
1 eqsqrtd.1 
 |-  ( ph -> A e. CC )
2 eqsqrtd.2 
 |-  ( ph -> B e. CC )
3 eqsqrtd.3 
 |-  ( ph -> ( A ^ 2 ) = B )
4 eqsqrtd.4 
 |-  ( ph -> 0 <_ ( Re ` A ) )
5 eqsqrtd.5 
 |-  ( ph -> -. ( _i x. A ) e. RR+ )
6 sqreu 
 |-  ( B e. CC -> E! x e. CC ( ( x ^ 2 ) = B /\ 0 <_ ( Re ` x ) /\ ( _i x. x ) e/ RR+ ) )
7 reurmo 
 |-  ( E! x e. CC ( ( x ^ 2 ) = B /\ 0 <_ ( Re ` x ) /\ ( _i x. x ) e/ RR+ ) -> E* x e. CC ( ( x ^ 2 ) = B /\ 0 <_ ( Re ` x ) /\ ( _i x. x ) e/ RR+ ) )
8 2 6 7 3syl 
 |-  ( ph -> E* x e. CC ( ( x ^ 2 ) = B /\ 0 <_ ( Re ` x ) /\ ( _i x. x ) e/ RR+ ) )
9 df-nel 
 |-  ( ( _i x. A ) e/ RR+ <-> -. ( _i x. A ) e. RR+ )
10 5 9 sylibr 
 |-  ( ph -> ( _i x. A ) e/ RR+ )
11 3 4 10 3jca 
 |-  ( ph -> ( ( A ^ 2 ) = B /\ 0 <_ ( Re ` A ) /\ ( _i x. A ) e/ RR+ ) )
12 sqrtcl 
 |-  ( B e. CC -> ( sqrt ` B ) e. CC )
13 2 12 syl 
 |-  ( ph -> ( sqrt ` B ) e. CC )
14 sqrtthlem 
 |-  ( B e. CC -> ( ( ( sqrt ` B ) ^ 2 ) = B /\ 0 <_ ( Re ` ( sqrt ` B ) ) /\ ( _i x. ( sqrt ` B ) ) e/ RR+ ) )
15 2 14 syl 
 |-  ( ph -> ( ( ( sqrt ` B ) ^ 2 ) = B /\ 0 <_ ( Re ` ( sqrt ` B ) ) /\ ( _i x. ( sqrt ` B ) ) e/ RR+ ) )
16 oveq1 
 |-  ( x = A -> ( x ^ 2 ) = ( A ^ 2 ) )
17 16 eqeq1d 
 |-  ( x = A -> ( ( x ^ 2 ) = B <-> ( A ^ 2 ) = B ) )
18 fveq2 
 |-  ( x = A -> ( Re ` x ) = ( Re ` A ) )
19 18 breq2d 
 |-  ( x = A -> ( 0 <_ ( Re ` x ) <-> 0 <_ ( Re ` A ) ) )
20 oveq2 
 |-  ( x = A -> ( _i x. x ) = ( _i x. A ) )
21 neleq1 
 |-  ( ( _i x. x ) = ( _i x. A ) -> ( ( _i x. x ) e/ RR+ <-> ( _i x. A ) e/ RR+ ) )
22 20 21 syl 
 |-  ( x = A -> ( ( _i x. x ) e/ RR+ <-> ( _i x. A ) e/ RR+ ) )
23 17 19 22 3anbi123d 
 |-  ( x = A -> ( ( ( x ^ 2 ) = B /\ 0 <_ ( Re ` x ) /\ ( _i x. x ) e/ RR+ ) <-> ( ( A ^ 2 ) = B /\ 0 <_ ( Re ` A ) /\ ( _i x. A ) e/ RR+ ) ) )
24 oveq1 
 |-  ( x = ( sqrt ` B ) -> ( x ^ 2 ) = ( ( sqrt ` B ) ^ 2 ) )
25 24 eqeq1d 
 |-  ( x = ( sqrt ` B ) -> ( ( x ^ 2 ) = B <-> ( ( sqrt ` B ) ^ 2 ) = B ) )
26 fveq2 
 |-  ( x = ( sqrt ` B ) -> ( Re ` x ) = ( Re ` ( sqrt ` B ) ) )
27 26 breq2d 
 |-  ( x = ( sqrt ` B ) -> ( 0 <_ ( Re ` x ) <-> 0 <_ ( Re ` ( sqrt ` B ) ) ) )
28 oveq2 
 |-  ( x = ( sqrt ` B ) -> ( _i x. x ) = ( _i x. ( sqrt ` B ) ) )
29 neleq1 
 |-  ( ( _i x. x ) = ( _i x. ( sqrt ` B ) ) -> ( ( _i x. x ) e/ RR+ <-> ( _i x. ( sqrt ` B ) ) e/ RR+ ) )
30 28 29 syl 
 |-  ( x = ( sqrt ` B ) -> ( ( _i x. x ) e/ RR+ <-> ( _i x. ( sqrt ` B ) ) e/ RR+ ) )
31 25 27 30 3anbi123d 
 |-  ( x = ( sqrt ` B ) -> ( ( ( x ^ 2 ) = B /\ 0 <_ ( Re ` x ) /\ ( _i x. x ) e/ RR+ ) <-> ( ( ( sqrt ` B ) ^ 2 ) = B /\ 0 <_ ( Re ` ( sqrt ` B ) ) /\ ( _i x. ( sqrt ` B ) ) e/ RR+ ) ) )
32 23 31 rmoi 
 |-  ( ( E* x e. CC ( ( x ^ 2 ) = B /\ 0 <_ ( Re ` x ) /\ ( _i x. x ) e/ RR+ ) /\ ( A e. CC /\ ( ( A ^ 2 ) = B /\ 0 <_ ( Re ` A ) /\ ( _i x. A ) e/ RR+ ) ) /\ ( ( sqrt ` B ) e. CC /\ ( ( ( sqrt ` B ) ^ 2 ) = B /\ 0 <_ ( Re ` ( sqrt ` B ) ) /\ ( _i x. ( sqrt ` B ) ) e/ RR+ ) ) ) -> A = ( sqrt ` B ) )
33 8 1 11 13 15 32 syl122anc 
 |-  ( ph -> A = ( sqrt ` B ) )