Metamath Proof Explorer

Theorem resqrtcl

Description: Closure of the square root function. (Contributed by Mario Carneiro, 9-Jul-2013)

Ref Expression
Assertion resqrtcl 
|- ( ( A e. RR /\ 0 <_ A ) -> ( sqrt ` A ) e. RR )

Proof

Step Hyp Ref Expression
1 resqrex 
 |-  ( ( A e. RR /\ 0 <_ A ) -> E. y e. RR ( 0 <_ y /\ ( y ^ 2 ) = A ) )
2 simp1l 
 |-  ( ( ( A e. RR /\ 0 <_ A ) /\ y e. RR /\ ( 0 <_ y /\ ( y ^ 2 ) = A ) ) -> A e. RR )
3 recn 
 |-  ( A e. RR -> A e. CC )
4 sqrtval 
 |-  ( A e. CC -> ( sqrt ` A ) = ( iota_ x e. CC ( ( x ^ 2 ) = A /\ 0 <_ ( Re ` x ) /\ ( _i x. x ) e/ RR+ ) ) )
5 2 3 4 3syl 
 |-  ( ( ( A e. RR /\ 0 <_ A ) /\ y e. RR /\ ( 0 <_ y /\ ( y ^ 2 ) = A ) ) -> ( sqrt ` A ) = ( iota_ x e. CC ( ( x ^ 2 ) = A /\ 0 <_ ( Re ` x ) /\ ( _i x. x ) e/ RR+ ) ) )
6 simp3r 
 |-  ( ( ( A e. RR /\ 0 <_ A ) /\ y e. RR /\ ( 0 <_ y /\ ( y ^ 2 ) = A ) ) -> ( y ^ 2 ) = A )
7 simp3l 
 |-  ( ( ( A e. RR /\ 0 <_ A ) /\ y e. RR /\ ( 0 <_ y /\ ( y ^ 2 ) = A ) ) -> 0 <_ y )
8 rere 
 |-  ( y e. RR -> ( Re ` y ) = y )
9 8 3ad2ant2 
 |-  ( ( ( A e. RR /\ 0 <_ A ) /\ y e. RR /\ ( 0 <_ y /\ ( y ^ 2 ) = A ) ) -> ( Re ` y ) = y )
10 7 9 breqtrrd 
 |-  ( ( ( A e. RR /\ 0 <_ A ) /\ y e. RR /\ ( 0 <_ y /\ ( y ^ 2 ) = A ) ) -> 0 <_ ( Re ` y ) )
11 rennim 
 |-  ( y e. RR -> ( _i x. y ) e/ RR+ )
12 11 3ad2ant2 
 |-  ( ( ( A e. RR /\ 0 <_ A ) /\ y e. RR /\ ( 0 <_ y /\ ( y ^ 2 ) = A ) ) -> ( _i x. y ) e/ RR+ )
13 6 10 12 3jca 
 |-  ( ( ( A e. RR /\ 0 <_ A ) /\ y e. RR /\ ( 0 <_ y /\ ( y ^ 2 ) = A ) ) -> ( ( y ^ 2 ) = A /\ 0 <_ ( Re ` y ) /\ ( _i x. y ) e/ RR+ ) )
14 recn 
 |-  ( y e. RR -> y e. CC )
15 14 3ad2ant2 
 |-  ( ( ( A e. RR /\ 0 <_ A ) /\ y e. RR /\ ( 0 <_ y /\ ( y ^ 2 ) = A ) ) -> y e. CC )
16 resqreu 
 |-  ( ( A e. RR /\ 0 <_ A ) -> E! x e. CC ( ( x ^ 2 ) = A /\ 0 <_ ( Re ` x ) /\ ( _i x. x ) e/ RR+ ) )
17 16 3ad2ant1 
 |-  ( ( ( A e. RR /\ 0 <_ A ) /\ y e. RR /\ ( 0 <_ y /\ ( y ^ 2 ) = A ) ) -> E! x e. CC ( ( x ^ 2 ) = A /\ 0 <_ ( Re ` x ) /\ ( _i x. x ) e/ RR+ ) )
18 oveq1 
 |-  ( x = y -> ( x ^ 2 ) = ( y ^ 2 ) )
19 18 eqeq1d 
 |-  ( x = y -> ( ( x ^ 2 ) = A <-> ( y ^ 2 ) = A ) )
20 fveq2 
 |-  ( x = y -> ( Re ` x ) = ( Re ` y ) )
21 20 breq2d 
 |-  ( x = y -> ( 0 <_ ( Re ` x ) <-> 0 <_ ( Re ` y ) ) )
22 oveq2 
 |-  ( x = y -> ( _i x. x ) = ( _i x. y ) )
23 neleq1 
 |-  ( ( _i x. x ) = ( _i x. y ) -> ( ( _i x. x ) e/ RR+ <-> ( _i x. y ) e/ RR+ ) )
24 22 23 syl 
 |-  ( x = y -> ( ( _i x. x ) e/ RR+ <-> ( _i x. y ) e/ RR+ ) )
25 19 21 24 3anbi123d 
 |-  ( x = y -> ( ( ( x ^ 2 ) = A /\ 0 <_ ( Re ` x ) /\ ( _i x. x ) e/ RR+ ) <-> ( ( y ^ 2 ) = A /\ 0 <_ ( Re ` y ) /\ ( _i x. y ) e/ RR+ ) ) )
26 25 riota2 
 |-  ( ( y e. CC /\ E! x e. CC ( ( x ^ 2 ) = A /\ 0 <_ ( Re ` x ) /\ ( _i x. x ) e/ RR+ ) ) -> ( ( ( y ^ 2 ) = A /\ 0 <_ ( Re ` y ) /\ ( _i x. y ) e/ RR+ ) <-> ( iota_ x e. CC ( ( x ^ 2 ) = A /\ 0 <_ ( Re ` x ) /\ ( _i x. x ) e/ RR+ ) ) = y ) )
27 15 17 26 syl2anc 
 |-  ( ( ( A e. RR /\ 0 <_ A ) /\ y e. RR /\ ( 0 <_ y /\ ( y ^ 2 ) = A ) ) -> ( ( ( y ^ 2 ) = A /\ 0 <_ ( Re ` y ) /\ ( _i x. y ) e/ RR+ ) <-> ( iota_ x e. CC ( ( x ^ 2 ) = A /\ 0 <_ ( Re ` x ) /\ ( _i x. x ) e/ RR+ ) ) = y ) )
28 13 27 mpbid 
 |-  ( ( ( A e. RR /\ 0 <_ A ) /\ y e. RR /\ ( 0 <_ y /\ ( y ^ 2 ) = A ) ) -> ( iota_ x e. CC ( ( x ^ 2 ) = A /\ 0 <_ ( Re ` x ) /\ ( _i x. x ) e/ RR+ ) ) = y )
29 5 28 eqtrd 
 |-  ( ( ( A e. RR /\ 0 <_ A ) /\ y e. RR /\ ( 0 <_ y /\ ( y ^ 2 ) = A ) ) -> ( sqrt ` A ) = y )
30 simp2 
 |-  ( ( ( A e. RR /\ 0 <_ A ) /\ y e. RR /\ ( 0 <_ y /\ ( y ^ 2 ) = A ) ) -> y e. RR )
31 29 30 eqeltrd 
 |-  ( ( ( A e. RR /\ 0 <_ A ) /\ y e. RR /\ ( 0 <_ y /\ ( y ^ 2 ) = A ) ) -> ( sqrt ` A ) e. RR )
32 31 rexlimdv3a 
 |-  ( ( A e. RR /\ 0 <_ A ) -> ( E. y e. RR ( 0 <_ y /\ ( y ^ 2 ) = A ) -> ( sqrt ` A ) e. RR ) )
33 1 32 mpd 
 |-  ( ( A e. RR /\ 0 <_ A ) -> ( sqrt ` A ) e. RR )