Metamath Proof Explorer

Theorem resqreu

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

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

Proof

Step Hyp Ref Expression
1 resqrex 
 |-  ( ( A e. RR /\ 0 <_ A ) -> E. x e. RR ( 0 <_ x /\ ( x ^ 2 ) = A ) )
2 recn 
 |-  ( x e. RR -> x e. CC )
3 2 adantr 
 |-  ( ( x e. RR /\ ( 0 <_ x /\ ( x ^ 2 ) = A ) ) -> x e. CC )
4 simprr 
 |-  ( ( x e. RR /\ ( 0 <_ x /\ ( x ^ 2 ) = A ) ) -> ( x ^ 2 ) = A )
5 rere 
 |-  ( x e. RR -> ( Re ` x ) = x )
6 5 breq2d 
 |-  ( x e. RR -> ( 0 <_ ( Re ` x ) <-> 0 <_ x ) )
7 6 biimpar 
 |-  ( ( x e. RR /\ 0 <_ x ) -> 0 <_ ( Re ` x ) )
8 7 adantrr 
 |-  ( ( x e. RR /\ ( 0 <_ x /\ ( x ^ 2 ) = A ) ) -> 0 <_ ( Re ` x ) )
9 rennim 
 |-  ( x e. RR -> ( _i x. x ) e/ RR+ )
10 9 adantr 
 |-  ( ( x e. RR /\ ( 0 <_ x /\ ( x ^ 2 ) = A ) ) -> ( _i x. x ) e/ RR+ )
11 4 8 10 3jca 
 |-  ( ( x e. RR /\ ( 0 <_ x /\ ( x ^ 2 ) = A ) ) -> ( ( x ^ 2 ) = A /\ 0 <_ ( Re ` x ) /\ ( _i x. x ) e/ RR+ ) )
12 3 11 jca 
 |-  ( ( x e. RR /\ ( 0 <_ x /\ ( x ^ 2 ) = A ) ) -> ( x e. CC /\ ( ( x ^ 2 ) = A /\ 0 <_ ( Re ` x ) /\ ( _i x. x ) e/ RR+ ) ) )
13 12 reximi2 
 |-  ( E. x e. RR ( 0 <_ x /\ ( x ^ 2 ) = A ) -> E. x e. CC ( ( x ^ 2 ) = A /\ 0 <_ ( Re ` x ) /\ ( _i x. x ) e/ RR+ ) )
14 1 13 syl 
 |-  ( ( A e. RR /\ 0 <_ A ) -> E. x e. CC ( ( x ^ 2 ) = A /\ 0 <_ ( Re ` x ) /\ ( _i x. x ) e/ RR+ ) )
15 recn 
 |-  ( A e. RR -> A e. CC )
16 15 adantr 
 |-  ( ( A e. RR /\ 0 <_ A ) -> A e. CC )
17 sqrmo 
 |-  ( A e. CC -> E* x e. CC ( ( x ^ 2 ) = A /\ 0 <_ ( Re ` x ) /\ ( _i x. x ) e/ RR+ ) )
18 16 17 syl 
 |-  ( ( A e. RR /\ 0 <_ A ) -> E* x e. CC ( ( x ^ 2 ) = A /\ 0 <_ ( Re ` x ) /\ ( _i x. x ) e/ RR+ ) )
19 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+ ) ) )
20 14 18 19 sylanbrc 
 |-  ( ( A e. RR /\ 0 <_ A ) -> E! x e. CC ( ( x ^ 2 ) = A /\ 0 <_ ( Re ` x ) /\ ( _i x. x ) e/ RR+ ) )