Metamath Proof Explorer

Theorem ressatans

Description: The real number line is a subset of the domain of continuity of the arctangent. (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 ressatans 
|- RR C_ S

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 ax-resscn 
 |-  RR C_ CC
4 1re 
 |-  1 e. RR
5 resqcl 
 |-  ( y e. RR -> ( y ^ 2 ) e. RR )
6 readdcl 
 |-  ( ( 1 e. RR /\ ( y ^ 2 ) e. RR ) -> ( 1 + ( y ^ 2 ) ) e. RR )
7 4 5 6 sylancr 
 |-  ( y e. RR -> ( 1 + ( y ^ 2 ) ) e. RR )
8 7 recnd 
 |-  ( y e. RR -> ( 1 + ( y ^ 2 ) ) e. CC )
9 4 a1i 
 |-  ( y e. RR -> 1 e. RR )
10 0lt1 
 |-  0 < 1
11 10 a1i 
 |-  ( y e. RR -> 0 < 1 )
12 sqge0 
 |-  ( y e. RR -> 0 <_ ( y ^ 2 ) )
13 9 5 11 12 addgtge0d 
 |-  ( y e. RR -> 0 < ( 1 + ( y ^ 2 ) ) )
14 0re 
 |-  0 e. RR
15 ltnle 
 |-  ( ( 0 e. RR /\ ( 1 + ( y ^ 2 ) ) e. RR ) -> ( 0 < ( 1 + ( y ^ 2 ) ) <-> -. ( 1 + ( y ^ 2 ) ) <_ 0 ) )
16 14 7 15 sylancr 
 |-  ( y e. RR -> ( 0 < ( 1 + ( y ^ 2 ) ) <-> -. ( 1 + ( y ^ 2 ) ) <_ 0 ) )
17 13 16 mpbid 
 |-  ( y e. RR -> -. ( 1 + ( y ^ 2 ) ) <_ 0 )
18 mnfxr 
 |-  -oo e. RR*
19 elioc2 
 |-  ( ( -oo e. RR* /\ 0 e. RR ) -> ( ( 1 + ( y ^ 2 ) ) e. ( -oo (,] 0 ) <-> ( ( 1 + ( y ^ 2 ) ) e. RR /\ -oo < ( 1 + ( y ^ 2 ) ) /\ ( 1 + ( y ^ 2 ) ) <_ 0 ) ) )
20 18 14 19 mp2an 
 |-  ( ( 1 + ( y ^ 2 ) ) e. ( -oo (,] 0 ) <-> ( ( 1 + ( y ^ 2 ) ) e. RR /\ -oo < ( 1 + ( y ^ 2 ) ) /\ ( 1 + ( y ^ 2 ) ) <_ 0 ) )
21 20 simp3bi 
 |-  ( ( 1 + ( y ^ 2 ) ) e. ( -oo (,] 0 ) -> ( 1 + ( y ^ 2 ) ) <_ 0 )
22 17 21 nsyl 
 |-  ( y e. RR -> -. ( 1 + ( y ^ 2 ) ) e. ( -oo (,] 0 ) )
23 8 22 eldifd 
 |-  ( y e. RR -> ( 1 + ( y ^ 2 ) ) e. ( CC \ ( -oo (,] 0 ) ) )
24 23 1 eleqtrrdi 
 |-  ( y e. RR -> ( 1 + ( y ^ 2 ) ) e. D )
25 24 rgen 
 |-  A. y e. RR ( 1 + ( y ^ 2 ) ) e. D
26 ssrab 
 |-  ( RR C_ { y e. CC | ( 1 + ( y ^ 2 ) ) e. D } <-> ( RR C_ CC /\ A. y e. RR ( 1 + ( y ^ 2 ) ) e. D ) )
27 3 25 26 mpbir2an 
 |-  RR C_ { y e. CC | ( 1 + ( y ^ 2 ) ) e. D }
28 27 2 sseqtrri 
 |-  RR C_ S