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 ( 𝐴 ∈ ℝ → ( arctan ‘ 𝐴 ) ∈ ( - ( π / 2 ) (,) ( π / 2 ) ) )

Proof

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