Metamath Proof Explorer

Theorem atanbnd

Description: The arctangent function is bounded by _pi / 2 on the reals. (Contributed by Mario Carneiro, 5-Apr-2015)

Ref Expression
Assertion atanbnd 
|- ( A e. RR -> ( arctan ` A ) e. ( -u ( _pi / 2 ) (,) ( _pi / 2 ) ) )

Proof

Step Hyp Ref Expression
1 atanre 
 |-  ( A e. RR -> A e. dom arctan )
2 1 adantr 
 |-  ( ( A e. RR /\ A < 0 ) -> A e. dom arctan )
3 atanneg 
 |-  ( A e. dom arctan -> ( arctan ` -u A ) = -u ( arctan ` A ) )
4 2 3 syl 
 |-  ( ( A e. RR /\ A < 0 ) -> ( arctan ` -u A ) = -u ( arctan ` A ) )
5 renegcl 
 |-  ( A e. RR -> -u A e. RR )
6 5 adantr 
 |-  ( ( A e. RR /\ A < 0 ) -> -u A e. RR )
7 lt0neg1 
 |-  ( A e. RR -> ( A < 0 <-> 0 < -u A ) )
8 7 biimpa 
 |-  ( ( A e. RR /\ A < 0 ) -> 0 < -u A )
9 6 8 elrpd 
 |-  ( ( A e. RR /\ A < 0 ) -> -u A e. RR+ )
10 atanbndlem 
 |-  ( -u A e. RR+ -> ( arctan ` -u A ) e. ( -u ( _pi / 2 ) (,) ( _pi / 2 ) ) )
11 9 10 syl 
 |-  ( ( A e. RR /\ A < 0 ) -> ( arctan ` -u A ) e. ( -u ( _pi / 2 ) (,) ( _pi / 2 ) ) )
12 4 11 eqeltrrd 
 |-  ( ( A e. RR /\ A < 0 ) -> -u ( arctan ` A ) e. ( -u ( _pi / 2 ) (,) ( _pi / 2 ) ) )
13 halfpire 
 |-  ( _pi / 2 ) e. RR
14 13 recni 
 |-  ( _pi / 2 ) e. CC
15 14 negnegi 
 |-  -u -u ( _pi / 2 ) = ( _pi / 2 )
16 15 oveq2i 
 |-  ( -u ( _pi / 2 ) (,) -u -u ( _pi / 2 ) ) = ( -u ( _pi / 2 ) (,) ( _pi / 2 ) )
17 12 16 eleqtrrdi 
 |-  ( ( A e. RR /\ A < 0 ) -> -u ( arctan ` A ) e. ( -u ( _pi / 2 ) (,) -u -u ( _pi / 2 ) ) )
18 neghalfpire 
 |-  -u ( _pi / 2 ) e. RR
19 atanrecl 
 |-  ( A e. RR -> ( arctan ` A ) e. RR )
20 19 adantr 
 |-  ( ( A e. RR /\ A < 0 ) -> ( arctan ` A ) e. RR )
21 iooneg 
 |-  ( ( -u ( _pi / 2 ) e. RR /\ ( _pi / 2 ) e. RR /\ ( arctan ` A ) e. RR ) -> ( ( arctan ` A ) e. ( -u ( _pi / 2 ) (,) ( _pi / 2 ) ) <-> -u ( arctan ` A ) e. ( -u ( _pi / 2 ) (,) -u -u ( _pi / 2 ) ) ) )
22 18 13 20 21 mp3an12i 
 |-  ( ( A e. RR /\ A < 0 ) -> ( ( arctan ` A ) e. ( -u ( _pi / 2 ) (,) ( _pi / 2 ) ) <-> -u ( arctan ` A ) e. ( -u ( _pi / 2 ) (,) -u -u ( _pi / 2 ) ) ) )
23 17 22 mpbird 
 |-  ( ( A e. RR /\ A < 0 ) -> ( arctan ` A ) e. ( -u ( _pi / 2 ) (,) ( _pi / 2 ) ) )
24 simpr 
 |-  ( ( A e. RR /\ A = 0 ) -> A = 0 )
25 24 fveq2d 
 |-  ( ( A e. RR /\ A = 0 ) -> ( arctan ` A ) = ( arctan ` 0 ) )
26 atan0 
 |-  ( arctan ` 0 ) = 0
27 25 26 eqtrdi 
 |-  ( ( A e. RR /\ A = 0 ) -> ( arctan ` A ) = 0 )
28 0re 
 |-  0 e. RR
29 pirp 
 |-  _pi e. RR+
30 rphalfcl 
 |-  ( _pi e. RR+ -> ( _pi / 2 ) e. RR+ )
31 rpgt0 
 |-  ( ( _pi / 2 ) e. RR+ -> 0 < ( _pi / 2 ) )
32 29 30 31 mp2b 
 |-  0 < ( _pi / 2 )
33 lt0neg2 
 |-  ( ( _pi / 2 ) e. RR -> ( 0 < ( _pi / 2 ) <-> -u ( _pi / 2 ) < 0 ) )
34 13 33 ax-mp 
 |-  ( 0 < ( _pi / 2 ) <-> -u ( _pi / 2 ) < 0 )
35 32 34 mpbi 
 |-  -u ( _pi / 2 ) < 0
36 18 rexri 
 |-  -u ( _pi / 2 ) e. RR*
37 13 rexri 
 |-  ( _pi / 2 ) e. RR*
38 elioo2 
 |-  ( ( -u ( _pi / 2 ) e. RR* /\ ( _pi / 2 ) e. RR* ) -> ( 0 e. ( -u ( _pi / 2 ) (,) ( _pi / 2 ) ) <-> ( 0 e. RR /\ -u ( _pi / 2 ) < 0 /\ 0 < ( _pi / 2 ) ) ) )
39 36 37 38 mp2an 
 |-  ( 0 e. ( -u ( _pi / 2 ) (,) ( _pi / 2 ) ) <-> ( 0 e. RR /\ -u ( _pi / 2 ) < 0 /\ 0 < ( _pi / 2 ) ) )
40 28 35 32 39 mpbir3an 
 |-  0 e. ( -u ( _pi / 2 ) (,) ( _pi / 2 ) )
41 27 40 eqeltrdi 
 |-  ( ( A e. RR /\ A = 0 ) -> ( arctan ` A ) e. ( -u ( _pi / 2 ) (,) ( _pi / 2 ) ) )
42 elrp 
 |-  ( A e. RR+ <-> ( A e. RR /\ 0 < A ) )
43 atanbndlem 
 |-  ( A e. RR+ -> ( arctan ` A ) e. ( -u ( _pi / 2 ) (,) ( _pi / 2 ) ) )
44 42 43 sylbir 
 |-  ( ( A e. RR /\ 0 < A ) -> ( arctan ` A ) e. ( -u ( _pi / 2 ) (,) ( _pi / 2 ) ) )
45 lttri4 
 |-  ( ( A e. RR /\ 0 e. RR ) -> ( A < 0 \/ A = 0 \/ 0 < A ) )
46 28 45 mpan2 
 |-  ( A e. RR -> ( A < 0 \/ A = 0 \/ 0 < A ) )
47 23 41 44 46 mpjao3dan 
 |-  ( A e. RR -> ( arctan ` A ) e. ( -u ( _pi / 2 ) (,) ( _pi / 2 ) ) )