Metamath Proof Explorer

Theorem sqrtcn

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

Ref Expression
Hypothesis sqrcn.d 
|- D = ( CC \ ( -oo (,] 0 ) )
Assertion sqrtcn 
|- ( sqrt |` D ) e. ( D -cn-> CC )

Proof

Step Hyp Ref Expression
1 sqrcn.d 
 |-  D = ( CC \ ( -oo (,] 0 ) )
2 sqrtf 
 |-  sqrt : CC --> CC
3 2 a1i 
 |-  ( T. -> sqrt : CC --> CC )
4 3 feqmptd 
 |-  ( T. -> sqrt = ( x e. CC |-> ( sqrt ` x ) ) )
5 4 reseq1d 
 |-  ( T. -> ( sqrt |` D ) = ( ( x e. CC |-> ( sqrt ` x ) ) |` D ) )
6 difss 
 |-  ( CC \ ( -oo (,] 0 ) ) C_ CC
7 1 6 eqsstri 
 |-  D C_ CC
8 resmpt 
 |-  ( D C_ CC -> ( ( x e. CC |-> ( sqrt ` x ) ) |` D ) = ( x e. D |-> ( sqrt ` x ) ) )
9 7 8 mp1i 
 |-  ( T. -> ( ( x e. CC |-> ( sqrt ` x ) ) |` D ) = ( x e. D |-> ( sqrt ` x ) ) )
10 7 sseli 
 |-  ( x e. D -> x e. CC )
11 10 adantl 
 |-  ( ( T. /\ x e. D ) -> x e. CC )
12 cxpsqrt 
 |-  ( x e. CC -> ( x ^c ( 1 / 2 ) ) = ( sqrt ` x ) )
13 11 12 syl 
 |-  ( ( T. /\ x e. D ) -> ( x ^c ( 1 / 2 ) ) = ( sqrt ` x ) )
14 13 eqcomd 
 |-  ( ( T. /\ x e. D ) -> ( sqrt ` x ) = ( x ^c ( 1 / 2 ) ) )
15 14 mpteq2dva 
 |-  ( T. -> ( x e. D |-> ( sqrt ` x ) ) = ( x e. D |-> ( x ^c ( 1 / 2 ) ) ) )
16 5 9 15 3eqtrd 
 |-  ( T. -> ( sqrt |` D ) = ( x e. D |-> ( x ^c ( 1 / 2 ) ) ) )
17 eqid 
 |-  ( TopOpen ` CCfld ) = ( TopOpen ` CCfld )
18 17 cnfldtopon 
 |-  ( TopOpen ` CCfld ) e. ( TopOn ` CC )
19 18 a1i 
 |-  ( T. -> ( TopOpen ` CCfld ) e. ( TopOn ` CC ) )
20 resttopon 
 |-  ( ( ( TopOpen ` CCfld ) e. ( TopOn ` CC ) /\ D C_ CC ) -> ( ( TopOpen ` CCfld ) |`t D ) e. ( TopOn ` D ) )
21 19 7 20 sylancl 
 |-  ( T. -> ( ( TopOpen ` CCfld ) |`t D ) e. ( TopOn ` D ) )
22 21 cnmptid 
 |-  ( T. -> ( x e. D |-> x ) e. ( ( ( TopOpen ` CCfld ) |`t D ) Cn ( ( TopOpen ` CCfld ) |`t D ) ) )
23 ax-1cn 
 |-  1 e. CC
24 halfcl 
 |-  ( 1 e. CC -> ( 1 / 2 ) e. CC )
25 23 24 mp1i 
 |-  ( T. -> ( 1 / 2 ) e. CC )
26 21 19 25 cnmptc 
 |-  ( T. -> ( x e. D |-> ( 1 / 2 ) ) e. ( ( ( TopOpen ` CCfld ) |`t D ) Cn ( TopOpen ` CCfld ) ) )
27 eqid 
 |-  ( ( TopOpen ` CCfld ) |`t D ) = ( ( TopOpen ` CCfld ) |`t D )
28 1 17 27 cxpcn 
 |-  ( y e. D , z e. CC |-> ( y ^c z ) ) e. ( ( ( ( TopOpen ` CCfld ) |`t D ) tX ( TopOpen ` CCfld ) ) Cn ( TopOpen ` CCfld ) )
29 28 a1i 
 |-  ( T. -> ( y e. D , z e. CC |-> ( y ^c z ) ) e. ( ( ( ( TopOpen ` CCfld ) |`t D ) tX ( TopOpen ` CCfld ) ) Cn ( TopOpen ` CCfld ) ) )
30 oveq12 
 |-  ( ( y = x /\ z = ( 1 / 2 ) ) -> ( y ^c z ) = ( x ^c ( 1 / 2 ) ) )
31 21 22 26 21 19 29 30 cnmpt12 
 |-  ( T. -> ( x e. D |-> ( x ^c ( 1 / 2 ) ) ) e. ( ( ( TopOpen ` CCfld ) |`t D ) Cn ( TopOpen ` CCfld ) ) )
32 ssid 
 |-  CC C_ CC
33 18 toponrestid 
 |-  ( TopOpen ` CCfld ) = ( ( TopOpen ` CCfld ) |`t CC )
34 17 27 33 cncfcn 
 |-  ( ( D C_ CC /\ CC C_ CC ) -> ( D -cn-> CC ) = ( ( ( TopOpen ` CCfld ) |`t D ) Cn ( TopOpen ` CCfld ) ) )
35 7 32 34 mp2an 
 |-  ( D -cn-> CC ) = ( ( ( TopOpen ` CCfld ) |`t D ) Cn ( TopOpen ` CCfld ) )
36 31 35 eleqtrrdi 
 |-  ( T. -> ( x e. D |-> ( x ^c ( 1 / 2 ) ) ) e. ( D -cn-> CC ) )
37 16 36 eqeltrd 
 |-  ( T. -> ( sqrt |` D ) e. ( D -cn-> CC ) )
38 37 mptru 
 |-  ( sqrt |` D ) e. ( D -cn-> CC )