This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem atansopn

Description: The domain of continuity of the arctangent is an open set. (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 atansopn 
|- S e. ( TopOpen ` CCfld )

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 eqid 
 |-  ( y e. CC |-> ( 1 + ( y ^ 2 ) ) ) = ( y e. CC |-> ( 1 + ( y ^ 2 ) ) )
4 3 mptpreima 
 |-  ( `' ( y e. CC |-> ( 1 + ( y ^ 2 ) ) ) " D ) = { y e. CC | ( 1 + ( y ^ 2 ) ) e. D }
5 2 4 eqtr4i 
 |-  S = ( `' ( y e. CC |-> ( 1 + ( y ^ 2 ) ) ) " D )
6 eqid 
 |-  ( TopOpen ` CCfld ) = ( TopOpen ` CCfld )
7 6 cnfldtopon 
 |-  ( TopOpen ` CCfld ) e. ( TopOn ` CC )
8 7 a1i 
 |-  ( T. -> ( TopOpen ` CCfld ) e. ( TopOn ` CC ) )
9 1cnd 
 |-  ( T. -> 1 e. CC )
10 8 8 9 cnmptc 
 |-  ( T. -> ( y e. CC |-> 1 ) e. ( ( TopOpen ` CCfld ) Cn ( TopOpen ` CCfld ) ) )
11 2nn0 
 |-  2 e. NN0
12 6 expcn 
 |-  ( 2 e. NN0 -> ( y e. CC |-> ( y ^ 2 ) ) e. ( ( TopOpen ` CCfld ) Cn ( TopOpen ` CCfld ) ) )
13 11 12 mp1i 
 |-  ( T. -> ( y e. CC |-> ( y ^ 2 ) ) e. ( ( TopOpen ` CCfld ) Cn ( TopOpen ` CCfld ) ) )
14 6 addcn 
 |-  + e. ( ( ( TopOpen ` CCfld ) tX ( TopOpen ` CCfld ) ) Cn ( TopOpen ` CCfld ) )
15 14 a1i 
 |-  ( T. -> + e. ( ( ( TopOpen ` CCfld ) tX ( TopOpen ` CCfld ) ) Cn ( TopOpen ` CCfld ) ) )
16 8 10 13 15 cnmpt12f 
 |-  ( T. -> ( y e. CC |-> ( 1 + ( y ^ 2 ) ) ) e. ( ( TopOpen ` CCfld ) Cn ( TopOpen ` CCfld ) ) )
17 16 mptru 
 |-  ( y e. CC |-> ( 1 + ( y ^ 2 ) ) ) e. ( ( TopOpen ` CCfld ) Cn ( TopOpen ` CCfld ) )
18 1 logdmopn 
 |-  D e. ( TopOpen ` CCfld )
19 cnima 
 |-  ( ( ( y e. CC |-> ( 1 + ( y ^ 2 ) ) ) e. ( ( TopOpen ` CCfld ) Cn ( TopOpen ` CCfld ) ) /\ D e. ( TopOpen ` CCfld ) ) -> ( `' ( y e. CC |-> ( 1 + ( y ^ 2 ) ) ) " D ) e. ( TopOpen ` CCfld ) )
20 17 18 19 mp2an 
 |-  ( `' ( y e. CC |-> ( 1 + ( y ^ 2 ) ) ) " D ) e. ( TopOpen ` CCfld )
21 5 20 eqeltri 
 |-  S e. ( TopOpen ` CCfld )