Metamath Proof Explorer

Theorem atancn

Description: The arctangent is a continuous function. (Contributed by Mario Carneiro, 7-Apr-2015)

Ref Expression
Hypotheses atansopn.d 
|- D = ( CC \ ( -oo (,] 0 ) )
atansopn.s 
|- S = { y e. CC | ( 1 + ( y ^ 2 ) ) e. D }
Assertion atancn 
|- ( arctan |` S ) e. ( S -cn-> CC )

Proof

Step Hyp Ref Expression
1 atansopn.d 
 |-  D = ( CC \ ( -oo (,] 0 ) )
2 atansopn.s 
 |-  S = { y e. CC | ( 1 + ( y ^ 2 ) ) e. D }
3 ssid 
 |-  CC C_ CC
4 atanf 
 |-  arctan : ( CC \ { -u _i , _i } ) --> CC
5 1 2 atansssdm 
 |-  S C_ dom arctan
6 4 fdmi 
 |-  dom arctan = ( CC \ { -u _i , _i } )
7 5 6 sseqtri 
 |-  S C_ ( CC \ { -u _i , _i } )
8 fssres 
 |-  ( ( arctan : ( CC \ { -u _i , _i } ) --> CC /\ S C_ ( CC \ { -u _i , _i } ) ) -> ( arctan |` S ) : S --> CC )
9 4 7 8 mp2an 
 |-  ( arctan |` S ) : S --> CC
10 2 ssrab3 
 |-  S C_ CC
11 ovex 
 |-  ( 1 / ( 1 + ( x ^ 2 ) ) ) e. _V
12 1 2 dvatan 
 |-  ( CC _D ( arctan |` S ) ) = ( x e. S |-> ( 1 / ( 1 + ( x ^ 2 ) ) ) )
13 11 12 dmmpti 
 |-  dom ( CC _D ( arctan |` S ) ) = S
14 dvcn 
 |-  ( ( ( CC C_ CC /\ ( arctan |` S ) : S --> CC /\ S C_ CC ) /\ dom ( CC _D ( arctan |` S ) ) = S ) -> ( arctan |` S ) e. ( S -cn-> CC ) )
15 13 14 mpan2 
 |-  ( ( CC C_ CC /\ ( arctan |` S ) : S --> CC /\ S C_ CC ) -> ( arctan |` S ) e. ( S -cn-> CC ) )
16 3 9 10 15 mp3an 
 |-  ( arctan |` S ) e. ( S -cn-> CC )