Metamath Proof Explorer

Theorem resqrtcn

Description: Continuity of the real square root function. (Contributed by Mario Carneiro, 2-May-2016)

Ref Expression
Assertion resqrtcn 
|- ( sqrt |` ( 0 [,) +oo ) ) e. ( ( 0 [,) +oo ) -cn-> RR )

Proof

Step Hyp Ref Expression
1 sqrtf 
 |-  sqrt : CC --> CC
2 1 a1i 
 |-  ( T. -> sqrt : CC --> CC )
3 2 feqmptd 
 |-  ( T. -> sqrt = ( x e. CC |-> ( sqrt ` x ) ) )
4 3 reseq1d 
 |-  ( T. -> ( sqrt |` ( 0 [,) +oo ) ) = ( ( x e. CC |-> ( sqrt ` x ) ) |` ( 0 [,) +oo ) ) )
5 elrege0 
 |-  ( x e. ( 0 [,) +oo ) <-> ( x e. RR /\ 0 <_ x ) )
6 5 simplbi 
 |-  ( x e. ( 0 [,) +oo ) -> x e. RR )
7 6 recnd 
 |-  ( x e. ( 0 [,) +oo ) -> x e. CC )
8 7 ssriv 
 |-  ( 0 [,) +oo ) C_ CC
9 resmpt 
 |-  ( ( 0 [,) +oo ) C_ CC -> ( ( x e. CC |-> ( sqrt ` x ) ) |` ( 0 [,) +oo ) ) = ( x e. ( 0 [,) +oo ) |-> ( sqrt ` x ) ) )
10 8 9 mp1i 
 |-  ( T. -> ( ( x e. CC |-> ( sqrt ` x ) ) |` ( 0 [,) +oo ) ) = ( x e. ( 0 [,) +oo ) |-> ( sqrt ` x ) ) )
11 4 10 eqtrd 
 |-  ( T. -> ( sqrt |` ( 0 [,) +oo ) ) = ( x e. ( 0 [,) +oo ) |-> ( sqrt ` x ) ) )
12 11 mptru 
 |-  ( sqrt |` ( 0 [,) +oo ) ) = ( x e. ( 0 [,) +oo ) |-> ( sqrt ` x ) )
13 eqid 
 |-  ( x e. ( 0 [,) +oo ) |-> ( sqrt ` x ) ) = ( x e. ( 0 [,) +oo ) |-> ( sqrt ` x ) )
14 resqrtcl 
 |-  ( ( x e. RR /\ 0 <_ x ) -> ( sqrt ` x ) e. RR )
15 5 14 sylbi 
 |-  ( x e. ( 0 [,) +oo ) -> ( sqrt ` x ) e. RR )
16 13 15 fmpti 
 |-  ( x e. ( 0 [,) +oo ) |-> ( sqrt ` x ) ) : ( 0 [,) +oo ) --> RR
17 ax-resscn 
 |-  RR C_ CC
18 cxpsqrt 
 |-  ( x e. CC -> ( x ^c ( 1 / 2 ) ) = ( sqrt ` x ) )
19 7 18 syl 
 |-  ( x e. ( 0 [,) +oo ) -> ( x ^c ( 1 / 2 ) ) = ( sqrt ` x ) )
20 19 mpteq2ia 
 |-  ( x e. ( 0 [,) +oo ) |-> ( x ^c ( 1 / 2 ) ) ) = ( x e. ( 0 [,) +oo ) |-> ( sqrt ` x ) )
21 eqid 
 |-  ( TopOpen ` CCfld ) = ( TopOpen ` CCfld )
22 21 cnfldtopon 
 |-  ( TopOpen ` CCfld ) e. ( TopOn ` CC )
23 22 a1i 
 |-  ( T. -> ( TopOpen ` CCfld ) e. ( TopOn ` CC ) )
24 resttopon 
 |-  ( ( ( TopOpen ` CCfld ) e. ( TopOn ` CC ) /\ ( 0 [,) +oo ) C_ CC ) -> ( ( TopOpen ` CCfld ) |`t ( 0 [,) +oo ) ) e. ( TopOn ` ( 0 [,) +oo ) ) )
25 23 8 24 sylancl 
 |-  ( T. -> ( ( TopOpen ` CCfld ) |`t ( 0 [,) +oo ) ) e. ( TopOn ` ( 0 [,) +oo ) ) )
26 25 cnmptid 
 |-  ( T. -> ( x e. ( 0 [,) +oo ) |-> x ) e. ( ( ( TopOpen ` CCfld ) |`t ( 0 [,) +oo ) ) Cn ( ( TopOpen ` CCfld ) |`t ( 0 [,) +oo ) ) ) )
27 cnvimass 
 |-  ( `' Re " RR+ ) C_ dom Re
28 ref 
 |-  Re : CC --> RR
29 28 fdmi 
 |-  dom Re = CC
30 27 29 sseqtri 
 |-  ( `' Re " RR+ ) C_ CC
31 resttopon 
 |-  ( ( ( TopOpen ` CCfld ) e. ( TopOn ` CC ) /\ ( `' Re " RR+ ) C_ CC ) -> ( ( TopOpen ` CCfld ) |`t ( `' Re " RR+ ) ) e. ( TopOn ` ( `' Re " RR+ ) ) )
32 23 30 31 sylancl 
 |-  ( T. -> ( ( TopOpen ` CCfld ) |`t ( `' Re " RR+ ) ) e. ( TopOn ` ( `' Re " RR+ ) ) )
33 halfcn 
 |-  ( 1 / 2 ) e. CC
34 1rp 
 |-  1 e. RR+
35 rphalfcl 
 |-  ( 1 e. RR+ -> ( 1 / 2 ) e. RR+ )
36 34 35 ax-mp 
 |-  ( 1 / 2 ) e. RR+
37 rpre 
 |-  ( ( 1 / 2 ) e. RR+ -> ( 1 / 2 ) e. RR )
38 rere 
 |-  ( ( 1 / 2 ) e. RR -> ( Re ` ( 1 / 2 ) ) = ( 1 / 2 ) )
39 36 37 38 mp2b 
 |-  ( Re ` ( 1 / 2 ) ) = ( 1 / 2 )
40 39 36 eqeltri 
 |-  ( Re ` ( 1 / 2 ) ) e. RR+
41 ffn 
 |-  ( Re : CC --> RR -> Re Fn CC )
42 elpreima 
 |-  ( Re Fn CC -> ( ( 1 / 2 ) e. ( `' Re " RR+ ) <-> ( ( 1 / 2 ) e. CC /\ ( Re ` ( 1 / 2 ) ) e. RR+ ) ) )
43 28 41 42 mp2b 
 |-  ( ( 1 / 2 ) e. ( `' Re " RR+ ) <-> ( ( 1 / 2 ) e. CC /\ ( Re ` ( 1 / 2 ) ) e. RR+ ) )
44 33 40 43 mpbir2an 
 |-  ( 1 / 2 ) e. ( `' Re " RR+ )
45 44 a1i 
 |-  ( T. -> ( 1 / 2 ) e. ( `' Re " RR+ ) )
46 25 32 45 cnmptc 
 |-  ( T. -> ( x e. ( 0 [,) +oo ) |-> ( 1 / 2 ) ) e. ( ( ( TopOpen ` CCfld ) |`t ( 0 [,) +oo ) ) Cn ( ( TopOpen ` CCfld ) |`t ( `' Re " RR+ ) ) ) )
47 eqid 
 |-  ( `' Re " RR+ ) = ( `' Re " RR+ )
48 eqid 
 |-  ( ( TopOpen ` CCfld ) |`t ( 0 [,) +oo ) ) = ( ( TopOpen ` CCfld ) |`t ( 0 [,) +oo ) )
49 eqid 
 |-  ( ( TopOpen ` CCfld ) |`t ( `' Re " RR+ ) ) = ( ( TopOpen ` CCfld ) |`t ( `' Re " RR+ ) )
50 47 21 48 49 cxpcn3 
 |-  ( y e. ( 0 [,) +oo ) , z e. ( `' Re " RR+ ) |-> ( y ^c z ) ) e. ( ( ( ( TopOpen ` CCfld ) |`t ( 0 [,) +oo ) ) tX ( ( TopOpen ` CCfld ) |`t ( `' Re " RR+ ) ) ) Cn ( TopOpen ` CCfld ) )
51 50 a1i 
 |-  ( T. -> ( y e. ( 0 [,) +oo ) , z e. ( `' Re " RR+ ) |-> ( y ^c z ) ) e. ( ( ( ( TopOpen ` CCfld ) |`t ( 0 [,) +oo ) ) tX ( ( TopOpen ` CCfld ) |`t ( `' Re " RR+ ) ) ) Cn ( TopOpen ` CCfld ) ) )
52 oveq12 
 |-  ( ( y = x /\ z = ( 1 / 2 ) ) -> ( y ^c z ) = ( x ^c ( 1 / 2 ) ) )
53 25 26 46 25 32 51 52 cnmpt12 
 |-  ( T. -> ( x e. ( 0 [,) +oo ) |-> ( x ^c ( 1 / 2 ) ) ) e. ( ( ( TopOpen ` CCfld ) |`t ( 0 [,) +oo ) ) Cn ( TopOpen ` CCfld ) ) )
54 ssid 
 |-  CC C_ CC
55 22 toponrestid 
 |-  ( TopOpen ` CCfld ) = ( ( TopOpen ` CCfld ) |`t CC )
56 21 48 55 cncfcn 
 |-  ( ( ( 0 [,) +oo ) C_ CC /\ CC C_ CC ) -> ( ( 0 [,) +oo ) -cn-> CC ) = ( ( ( TopOpen ` CCfld ) |`t ( 0 [,) +oo ) ) Cn ( TopOpen ` CCfld ) ) )
57 8 54 56 mp2an 
 |-  ( ( 0 [,) +oo ) -cn-> CC ) = ( ( ( TopOpen ` CCfld ) |`t ( 0 [,) +oo ) ) Cn ( TopOpen ` CCfld ) )
58 53 57 eleqtrrdi 
 |-  ( T. -> ( x e. ( 0 [,) +oo ) |-> ( x ^c ( 1 / 2 ) ) ) e. ( ( 0 [,) +oo ) -cn-> CC ) )
59 20 58 eqeltrrid 
 |-  ( T. -> ( x e. ( 0 [,) +oo ) |-> ( sqrt ` x ) ) e. ( ( 0 [,) +oo ) -cn-> CC ) )
60 59 mptru 
 |-  ( x e. ( 0 [,) +oo ) |-> ( sqrt ` x ) ) e. ( ( 0 [,) +oo ) -cn-> CC )
61 cncffvrn 
 |-  ( ( RR C_ CC /\ ( x e. ( 0 [,) +oo ) |-> ( sqrt ` x ) ) e. ( ( 0 [,) +oo ) -cn-> CC ) ) -> ( ( x e. ( 0 [,) +oo ) |-> ( sqrt ` x ) ) e. ( ( 0 [,) +oo ) -cn-> RR ) <-> ( x e. ( 0 [,) +oo ) |-> ( sqrt ` x ) ) : ( 0 [,) +oo ) --> RR ) )
62 17 60 61 mp2an 
 |-  ( ( x e. ( 0 [,) +oo ) |-> ( sqrt ` x ) ) e. ( ( 0 [,) +oo ) -cn-> RR ) <-> ( x e. ( 0 [,) +oo ) |-> ( sqrt ` x ) ) : ( 0 [,) +oo ) --> RR )
63 16 62 mpbir 
 |-  ( x e. ( 0 [,) +oo ) |-> ( sqrt ` x ) ) e. ( ( 0 [,) +oo ) -cn-> RR )
64 12 63 eqeltri 
 |-  ( sqrt |` ( 0 [,) +oo ) ) e. ( ( 0 [,) +oo ) -cn-> RR )