Metamath Proof Explorer

Theorem sqreu

Description: Existence and uniqueness for the square root function in general. (Contributed by Mario Carneiro, 9-Jul-2013)

Ref Expression
Assertion sqreu 
|- ( A e. CC -> E! x e. CC ( ( x ^ 2 ) = A /\ 0 <_ ( Re ` x ) /\ ( _i x. x ) e/ RR+ ) )

Proof

Step Hyp Ref Expression
1 abscl 
 |-  ( A e. CC -> ( abs ` A ) e. RR )
2 1 recnd 
 |-  ( A e. CC -> ( abs ` A ) e. CC )
3 subneg 
 |-  ( ( ( abs ` A ) e. CC /\ A e. CC ) -> ( ( abs ` A ) - -u A ) = ( ( abs ` A ) + A ) )
4 2 3 mpancom 
 |-  ( A e. CC -> ( ( abs ` A ) - -u A ) = ( ( abs ` A ) + A ) )
5 4 eqeq1d 
 |-  ( A e. CC -> ( ( ( abs ` A ) - -u A ) = 0 <-> ( ( abs ` A ) + A ) = 0 ) )
6 negcl 
 |-  ( A e. CC -> -u A e. CC )
7 2 6 subeq0ad 
 |-  ( A e. CC -> ( ( ( abs ` A ) - -u A ) = 0 <-> ( abs ` A ) = -u A ) )
8 5 7 bitr3d 
 |-  ( A e. CC -> ( ( ( abs ` A ) + A ) = 0 <-> ( abs ` A ) = -u A ) )
9 ax-icn 
 |-  _i e. CC
10 absge0 
 |-  ( A e. CC -> 0 <_ ( abs ` A ) )
11 1 10 jca 
 |-  ( A e. CC -> ( ( abs ` A ) e. RR /\ 0 <_ ( abs ` A ) ) )
12 eleq1 
 |-  ( ( abs ` A ) = -u A -> ( ( abs ` A ) e. RR <-> -u A e. RR ) )
13 breq2 
 |-  ( ( abs ` A ) = -u A -> ( 0 <_ ( abs ` A ) <-> 0 <_ -u A ) )
14 12 13 anbi12d 
 |-  ( ( abs ` A ) = -u A -> ( ( ( abs ` A ) e. RR /\ 0 <_ ( abs ` A ) ) <-> ( -u A e. RR /\ 0 <_ -u A ) ) )
15 11 14 syl5ib 
 |-  ( ( abs ` A ) = -u A -> ( A e. CC -> ( -u A e. RR /\ 0 <_ -u A ) ) )
16 15 impcom 
 |-  ( ( A e. CC /\ ( abs ` A ) = -u A ) -> ( -u A e. RR /\ 0 <_ -u A ) )
17 resqrtcl 
 |-  ( ( -u A e. RR /\ 0 <_ -u A ) -> ( sqrt ` -u A ) e. RR )
18 16 17 syl 
 |-  ( ( A e. CC /\ ( abs ` A ) = -u A ) -> ( sqrt ` -u A ) e. RR )
19 18 recnd 
 |-  ( ( A e. CC /\ ( abs ` A ) = -u A ) -> ( sqrt ` -u A ) e. CC )
20 mulcl 
 |-  ( ( _i e. CC /\ ( sqrt ` -u A ) e. CC ) -> ( _i x. ( sqrt ` -u A ) ) e. CC )
21 9 19 20 sylancr 
 |-  ( ( A e. CC /\ ( abs ` A ) = -u A ) -> ( _i x. ( sqrt ` -u A ) ) e. CC )
22 sqrtneglem 
 |-  ( ( -u A e. RR /\ 0 <_ -u A ) -> ( ( ( _i x. ( sqrt ` -u A ) ) ^ 2 ) = -u -u A /\ 0 <_ ( Re ` ( _i x. ( sqrt ` -u A ) ) ) /\ ( _i x. ( _i x. ( sqrt ` -u A ) ) ) e/ RR+ ) )
23 16 22 syl 
 |-  ( ( A e. CC /\ ( abs ` A ) = -u A ) -> ( ( ( _i x. ( sqrt ` -u A ) ) ^ 2 ) = -u -u A /\ 0 <_ ( Re ` ( _i x. ( sqrt ` -u A ) ) ) /\ ( _i x. ( _i x. ( sqrt ` -u A ) ) ) e/ RR+ ) )
24 negneg 
 |-  ( A e. CC -> -u -u A = A )
25 24 adantr 
 |-  ( ( A e. CC /\ ( abs ` A ) = -u A ) -> -u -u A = A )
26 25 eqeq2d 
 |-  ( ( A e. CC /\ ( abs ` A ) = -u A ) -> ( ( ( _i x. ( sqrt ` -u A ) ) ^ 2 ) = -u -u A <-> ( ( _i x. ( sqrt ` -u A ) ) ^ 2 ) = A ) )
27 26 3anbi1d 
 |-  ( ( A e. CC /\ ( abs ` A ) = -u A ) -> ( ( ( ( _i x. ( sqrt ` -u A ) ) ^ 2 ) = -u -u A /\ 0 <_ ( Re ` ( _i x. ( sqrt ` -u A ) ) ) /\ ( _i x. ( _i x. ( sqrt ` -u A ) ) ) e/ RR+ ) <-> ( ( ( _i x. ( sqrt ` -u A ) ) ^ 2 ) = A /\ 0 <_ ( Re ` ( _i x. ( sqrt ` -u A ) ) ) /\ ( _i x. ( _i x. ( sqrt ` -u A ) ) ) e/ RR+ ) ) )
28 23 27 mpbid 
 |-  ( ( A e. CC /\ ( abs ` A ) = -u A ) -> ( ( ( _i x. ( sqrt ` -u A ) ) ^ 2 ) = A /\ 0 <_ ( Re ` ( _i x. ( sqrt ` -u A ) ) ) /\ ( _i x. ( _i x. ( sqrt ` -u A ) ) ) e/ RR+ ) )
29 oveq1 
 |-  ( x = ( _i x. ( sqrt ` -u A ) ) -> ( x ^ 2 ) = ( ( _i x. ( sqrt ` -u A ) ) ^ 2 ) )
30 29 eqeq1d 
 |-  ( x = ( _i x. ( sqrt ` -u A ) ) -> ( ( x ^ 2 ) = A <-> ( ( _i x. ( sqrt ` -u A ) ) ^ 2 ) = A ) )
31 fveq2 
 |-  ( x = ( _i x. ( sqrt ` -u A ) ) -> ( Re ` x ) = ( Re ` ( _i x. ( sqrt ` -u A ) ) ) )
32 31 breq2d 
 |-  ( x = ( _i x. ( sqrt ` -u A ) ) -> ( 0 <_ ( Re ` x ) <-> 0 <_ ( Re ` ( _i x. ( sqrt ` -u A ) ) ) ) )
33 oveq2 
 |-  ( x = ( _i x. ( sqrt ` -u A ) ) -> ( _i x. x ) = ( _i x. ( _i x. ( sqrt ` -u A ) ) ) )
34 neleq1 
 |-  ( ( _i x. x ) = ( _i x. ( _i x. ( sqrt ` -u A ) ) ) -> ( ( _i x. x ) e/ RR+ <-> ( _i x. ( _i x. ( sqrt ` -u A ) ) ) e/ RR+ ) )
35 33 34 syl 
 |-  ( x = ( _i x. ( sqrt ` -u A ) ) -> ( ( _i x. x ) e/ RR+ <-> ( _i x. ( _i x. ( sqrt ` -u A ) ) ) e/ RR+ ) )
36 30 32 35 3anbi123d 
 |-  ( x = ( _i x. ( sqrt ` -u A ) ) -> ( ( ( x ^ 2 ) = A /\ 0 <_ ( Re ` x ) /\ ( _i x. x ) e/ RR+ ) <-> ( ( ( _i x. ( sqrt ` -u A ) ) ^ 2 ) = A /\ 0 <_ ( Re ` ( _i x. ( sqrt ` -u A ) ) ) /\ ( _i x. ( _i x. ( sqrt ` -u A ) ) ) e/ RR+ ) ) )
37 36 rspcev 
 |-  ( ( ( _i x. ( sqrt ` -u A ) ) e. CC /\ ( ( ( _i x. ( sqrt ` -u A ) ) ^ 2 ) = A /\ 0 <_ ( Re ` ( _i x. ( sqrt ` -u A ) ) ) /\ ( _i x. ( _i x. ( sqrt ` -u A ) ) ) e/ RR+ ) ) -> E. x e. CC ( ( x ^ 2 ) = A /\ 0 <_ ( Re ` x ) /\ ( _i x. x ) e/ RR+ ) )
38 21 28 37 syl2anc 
 |-  ( ( A e. CC /\ ( abs ` A ) = -u A ) -> E. x e. CC ( ( x ^ 2 ) = A /\ 0 <_ ( Re ` x ) /\ ( _i x. x ) e/ RR+ ) )
39 38 ex 
 |-  ( A e. CC -> ( ( abs ` A ) = -u A -> E. x e. CC ( ( x ^ 2 ) = A /\ 0 <_ ( Re ` x ) /\ ( _i x. x ) e/ RR+ ) ) )
40 8 39 sylbid 
 |-  ( A e. CC -> ( ( ( abs ` A ) + A ) = 0 -> E. x e. CC ( ( x ^ 2 ) = A /\ 0 <_ ( Re ` x ) /\ ( _i x. x ) e/ RR+ ) ) )
41 resqrtcl 
 |-  ( ( ( abs ` A ) e. RR /\ 0 <_ ( abs ` A ) ) -> ( sqrt ` ( abs ` A ) ) e. RR )
42 1 10 41 syl2anc 
 |-  ( A e. CC -> ( sqrt ` ( abs ` A ) ) e. RR )
43 42 recnd 
 |-  ( A e. CC -> ( sqrt ` ( abs ` A ) ) e. CC )
44 43 adantr 
 |-  ( ( A e. CC /\ ( ( abs ` A ) + A ) =/= 0 ) -> ( sqrt ` ( abs ` A ) ) e. CC )
45 addcl 
 |-  ( ( ( abs ` A ) e. CC /\ A e. CC ) -> ( ( abs ` A ) + A ) e. CC )
46 2 45 mpancom 
 |-  ( A e. CC -> ( ( abs ` A ) + A ) e. CC )
47 46 adantr 
 |-  ( ( A e. CC /\ ( ( abs ` A ) + A ) =/= 0 ) -> ( ( abs ` A ) + A ) e. CC )
48 abscl 
 |-  ( ( ( abs ` A ) + A ) e. CC -> ( abs ` ( ( abs ` A ) + A ) ) e. RR )
49 46 48 syl 
 |-  ( A e. CC -> ( abs ` ( ( abs ` A ) + A ) ) e. RR )
50 49 recnd 
 |-  ( A e. CC -> ( abs ` ( ( abs ` A ) + A ) ) e. CC )
51 50 adantr 
 |-  ( ( A e. CC /\ ( ( abs ` A ) + A ) =/= 0 ) -> ( abs ` ( ( abs ` A ) + A ) ) e. CC )
52 46 abs00ad 
 |-  ( A e. CC -> ( ( abs ` ( ( abs ` A ) + A ) ) = 0 <-> ( ( abs ` A ) + A ) = 0 ) )
53 52 necon3bid 
 |-  ( A e. CC -> ( ( abs ` ( ( abs ` A ) + A ) ) =/= 0 <-> ( ( abs ` A ) + A ) =/= 0 ) )
54 53 biimpar 
 |-  ( ( A e. CC /\ ( ( abs ` A ) + A ) =/= 0 ) -> ( abs ` ( ( abs ` A ) + A ) ) =/= 0 )
55 47 51 54 divcld 
 |-  ( ( A e. CC /\ ( ( abs ` A ) + A ) =/= 0 ) -> ( ( ( abs ` A ) + A ) / ( abs ` ( ( abs ` A ) + A ) ) ) e. CC )
56 44 55 mulcld 
 |-  ( ( A e. CC /\ ( ( abs ` A ) + A ) =/= 0 ) -> ( ( sqrt ` ( abs ` A ) ) x. ( ( ( abs ` A ) + A ) / ( abs ` ( ( abs ` A ) + A ) ) ) ) e. CC )
57 eqid 
 |-  ( ( sqrt ` ( abs ` A ) ) x. ( ( ( abs ` A ) + A ) / ( abs ` ( ( abs ` A ) + A ) ) ) ) = ( ( sqrt ` ( abs ` A ) ) x. ( ( ( abs ` A ) + A ) / ( abs ` ( ( abs ` A ) + A ) ) ) )
58 57 sqreulem 
 |-  ( ( A e. CC /\ ( ( abs ` A ) + A ) =/= 0 ) -> ( ( ( ( sqrt ` ( abs ` A ) ) x. ( ( ( abs ` A ) + A ) / ( abs ` ( ( abs ` A ) + A ) ) ) ) ^ 2 ) = A /\ 0 <_ ( Re ` ( ( sqrt ` ( abs ` A ) ) x. ( ( ( abs ` A ) + A ) / ( abs ` ( ( abs ` A ) + A ) ) ) ) ) /\ ( _i x. ( ( sqrt ` ( abs ` A ) ) x. ( ( ( abs ` A ) + A ) / ( abs ` ( ( abs ` A ) + A ) ) ) ) ) e/ RR+ ) )
59 oveq1 
 |-  ( x = ( ( sqrt ` ( abs ` A ) ) x. ( ( ( abs ` A ) + A ) / ( abs ` ( ( abs ` A ) + A ) ) ) ) -> ( x ^ 2 ) = ( ( ( sqrt ` ( abs ` A ) ) x. ( ( ( abs ` A ) + A ) / ( abs ` ( ( abs ` A ) + A ) ) ) ) ^ 2 ) )
60 59 eqeq1d 
 |-  ( x = ( ( sqrt ` ( abs ` A ) ) x. ( ( ( abs ` A ) + A ) / ( abs ` ( ( abs ` A ) + A ) ) ) ) -> ( ( x ^ 2 ) = A <-> ( ( ( sqrt ` ( abs ` A ) ) x. ( ( ( abs ` A ) + A ) / ( abs ` ( ( abs ` A ) + A ) ) ) ) ^ 2 ) = A ) )
61 fveq2 
 |-  ( x = ( ( sqrt ` ( abs ` A ) ) x. ( ( ( abs ` A ) + A ) / ( abs ` ( ( abs ` A ) + A ) ) ) ) -> ( Re ` x ) = ( Re ` ( ( sqrt ` ( abs ` A ) ) x. ( ( ( abs ` A ) + A ) / ( abs ` ( ( abs ` A ) + A ) ) ) ) ) )
62 61 breq2d 
 |-  ( x = ( ( sqrt ` ( abs ` A ) ) x. ( ( ( abs ` A ) + A ) / ( abs ` ( ( abs ` A ) + A ) ) ) ) -> ( 0 <_ ( Re ` x ) <-> 0 <_ ( Re ` ( ( sqrt ` ( abs ` A ) ) x. ( ( ( abs ` A ) + A ) / ( abs ` ( ( abs ` A ) + A ) ) ) ) ) ) )
63 oveq2 
 |-  ( x = ( ( sqrt ` ( abs ` A ) ) x. ( ( ( abs ` A ) + A ) / ( abs ` ( ( abs ` A ) + A ) ) ) ) -> ( _i x. x ) = ( _i x. ( ( sqrt ` ( abs ` A ) ) x. ( ( ( abs ` A ) + A ) / ( abs ` ( ( abs ` A ) + A ) ) ) ) ) )
64 neleq1 
 |-  ( ( _i x. x ) = ( _i x. ( ( sqrt ` ( abs ` A ) ) x. ( ( ( abs ` A ) + A ) / ( abs ` ( ( abs ` A ) + A ) ) ) ) ) -> ( ( _i x. x ) e/ RR+ <-> ( _i x. ( ( sqrt ` ( abs ` A ) ) x. ( ( ( abs ` A ) + A ) / ( abs ` ( ( abs ` A ) + A ) ) ) ) ) e/ RR+ ) )
65 63 64 syl 
 |-  ( x = ( ( sqrt ` ( abs ` A ) ) x. ( ( ( abs ` A ) + A ) / ( abs ` ( ( abs ` A ) + A ) ) ) ) -> ( ( _i x. x ) e/ RR+ <-> ( _i x. ( ( sqrt ` ( abs ` A ) ) x. ( ( ( abs ` A ) + A ) / ( abs ` ( ( abs ` A ) + A ) ) ) ) ) e/ RR+ ) )
66 60 62 65 3anbi123d 
 |-  ( x = ( ( sqrt ` ( abs ` A ) ) x. ( ( ( abs ` A ) + A ) / ( abs ` ( ( abs ` A ) + A ) ) ) ) -> ( ( ( x ^ 2 ) = A /\ 0 <_ ( Re ` x ) /\ ( _i x. x ) e/ RR+ ) <-> ( ( ( ( sqrt ` ( abs ` A ) ) x. ( ( ( abs ` A ) + A ) / ( abs ` ( ( abs ` A ) + A ) ) ) ) ^ 2 ) = A /\ 0 <_ ( Re ` ( ( sqrt ` ( abs ` A ) ) x. ( ( ( abs ` A ) + A ) / ( abs ` ( ( abs ` A ) + A ) ) ) ) ) /\ ( _i x. ( ( sqrt ` ( abs ` A ) ) x. ( ( ( abs ` A ) + A ) / ( abs ` ( ( abs ` A ) + A ) ) ) ) ) e/ RR+ ) ) )
67 66 rspcev 
 |-  ( ( ( ( sqrt ` ( abs ` A ) ) x. ( ( ( abs ` A ) + A ) / ( abs ` ( ( abs ` A ) + A ) ) ) ) e. CC /\ ( ( ( ( sqrt ` ( abs ` A ) ) x. ( ( ( abs ` A ) + A ) / ( abs ` ( ( abs ` A ) + A ) ) ) ) ^ 2 ) = A /\ 0 <_ ( Re ` ( ( sqrt ` ( abs ` A ) ) x. ( ( ( abs ` A ) + A ) / ( abs ` ( ( abs ` A ) + A ) ) ) ) ) /\ ( _i x. ( ( sqrt ` ( abs ` A ) ) x. ( ( ( abs ` A ) + A ) / ( abs ` ( ( abs ` A ) + A ) ) ) ) ) e/ RR+ ) ) -> E. x e. CC ( ( x ^ 2 ) = A /\ 0 <_ ( Re ` x ) /\ ( _i x. x ) e/ RR+ ) )
68 56 58 67 syl2anc 
 |-  ( ( A e. CC /\ ( ( abs ` A ) + A ) =/= 0 ) -> E. x e. CC ( ( x ^ 2 ) = A /\ 0 <_ ( Re ` x ) /\ ( _i x. x ) e/ RR+ ) )
69 68 ex 
 |-  ( A e. CC -> ( ( ( abs ` A ) + A ) =/= 0 -> E. x e. CC ( ( x ^ 2 ) = A /\ 0 <_ ( Re ` x ) /\ ( _i x. x ) e/ RR+ ) ) )
70 40 69 pm2.61dne 
 |-  ( A e. CC -> E. x e. CC ( ( x ^ 2 ) = A /\ 0 <_ ( Re ` x ) /\ ( _i x. x ) e/ RR+ ) )
71 sqrmo 
 |-  ( A e. CC -> E* x e. CC ( ( x ^ 2 ) = A /\ 0 <_ ( Re ` x ) /\ ( _i x. x ) e/ RR+ ) )
72 reu5 
 |-  ( E! x e. CC ( ( x ^ 2 ) = A /\ 0 <_ ( Re ` x ) /\ ( _i x. x ) e/ RR+ ) <-> ( E. x e. CC ( ( x ^ 2 ) = A /\ 0 <_ ( Re ` x ) /\ ( _i x. x ) e/ RR+ ) /\ E* x e. CC ( ( x ^ 2 ) = A /\ 0 <_ ( Re ` x ) /\ ( _i x. x ) e/ RR+ ) ) )
73 70 71 72 sylanbrc 
 |-  ( A e. CC -> E! x e. CC ( ( x ^ 2 ) = A /\ 0 <_ ( Re ` x ) /\ ( _i x. x ) e/ RR+ ) )