Metamath Proof Explorer


Theorem tanabsge

Description: The tangent function is greater than or equal to its argument in absolute value. (Contributed by Mario Carneiro, 25-Feb-2015)

Ref Expression
Assertion tanabsge ( 𝐴 ∈ ( - ( π / 2 ) (,) ( π / 2 ) ) → ( abs ‘ 𝐴 ) ≤ ( abs ‘ ( tan ‘ 𝐴 ) ) )

Proof

Step Hyp Ref Expression
1 elioore ( 𝐴 ∈ ( - ( π / 2 ) (,) ( π / 2 ) ) → 𝐴 ∈ ℝ )
2 1 adantr ( ( 𝐴 ∈ ( - ( π / 2 ) (,) ( π / 2 ) ) ∧ 𝐴 < 0 ) → 𝐴 ∈ ℝ )
3 2 renegcld ( ( 𝐴 ∈ ( - ( π / 2 ) (,) ( π / 2 ) ) ∧ 𝐴 < 0 ) → - 𝐴 ∈ ℝ )
4 1 lt0neg1d ( 𝐴 ∈ ( - ( π / 2 ) (,) ( π / 2 ) ) → ( 𝐴 < 0 ↔ 0 < - 𝐴 ) )
5 4 biimpa ( ( 𝐴 ∈ ( - ( π / 2 ) (,) ( π / 2 ) ) ∧ 𝐴 < 0 ) → 0 < - 𝐴 )
6 eliooord ( 𝐴 ∈ ( - ( π / 2 ) (,) ( π / 2 ) ) → ( - ( π / 2 ) < 𝐴𝐴 < ( π / 2 ) ) )
7 6 simpld ( 𝐴 ∈ ( - ( π / 2 ) (,) ( π / 2 ) ) → - ( π / 2 ) < 𝐴 )
8 7 adantr ( ( 𝐴 ∈ ( - ( π / 2 ) (,) ( π / 2 ) ) ∧ 𝐴 < 0 ) → - ( π / 2 ) < 𝐴 )
9 halfpire ( π / 2 ) ∈ ℝ
10 ltnegcon1 ( ( ( π / 2 ) ∈ ℝ ∧ 𝐴 ∈ ℝ ) → ( - ( π / 2 ) < 𝐴 ↔ - 𝐴 < ( π / 2 ) ) )
11 9 2 10 sylancr ( ( 𝐴 ∈ ( - ( π / 2 ) (,) ( π / 2 ) ) ∧ 𝐴 < 0 ) → ( - ( π / 2 ) < 𝐴 ↔ - 𝐴 < ( π / 2 ) ) )
12 8 11 mpbid ( ( 𝐴 ∈ ( - ( π / 2 ) (,) ( π / 2 ) ) ∧ 𝐴 < 0 ) → - 𝐴 < ( π / 2 ) )
13 0xr 0 ∈ ℝ*
14 9 rexri ( π / 2 ) ∈ ℝ*
15 elioo2 ( ( 0 ∈ ℝ* ∧ ( π / 2 ) ∈ ℝ* ) → ( - 𝐴 ∈ ( 0 (,) ( π / 2 ) ) ↔ ( - 𝐴 ∈ ℝ ∧ 0 < - 𝐴 ∧ - 𝐴 < ( π / 2 ) ) ) )
16 13 14 15 mp2an ( - 𝐴 ∈ ( 0 (,) ( π / 2 ) ) ↔ ( - 𝐴 ∈ ℝ ∧ 0 < - 𝐴 ∧ - 𝐴 < ( π / 2 ) ) )
17 3 5 12 16 syl3anbrc ( ( 𝐴 ∈ ( - ( π / 2 ) (,) ( π / 2 ) ) ∧ 𝐴 < 0 ) → - 𝐴 ∈ ( 0 (,) ( π / 2 ) ) )
18 sincosq1sgn ( - 𝐴 ∈ ( 0 (,) ( π / 2 ) ) → ( 0 < ( sin ‘ - 𝐴 ) ∧ 0 < ( cos ‘ - 𝐴 ) ) )
19 17 18 syl ( ( 𝐴 ∈ ( - ( π / 2 ) (,) ( π / 2 ) ) ∧ 𝐴 < 0 ) → ( 0 < ( sin ‘ - 𝐴 ) ∧ 0 < ( cos ‘ - 𝐴 ) ) )
20 19 simprd ( ( 𝐴 ∈ ( - ( π / 2 ) (,) ( π / 2 ) ) ∧ 𝐴 < 0 ) → 0 < ( cos ‘ - 𝐴 ) )
21 20 gt0ne0d ( ( 𝐴 ∈ ( - ( π / 2 ) (,) ( π / 2 ) ) ∧ 𝐴 < 0 ) → ( cos ‘ - 𝐴 ) ≠ 0 )
22 3 21 retancld ( ( 𝐴 ∈ ( - ( π / 2 ) (,) ( π / 2 ) ) ∧ 𝐴 < 0 ) → ( tan ‘ - 𝐴 ) ∈ ℝ )
23 tangtx ( - 𝐴 ∈ ( 0 (,) ( π / 2 ) ) → - 𝐴 < ( tan ‘ - 𝐴 ) )
24 17 23 syl ( ( 𝐴 ∈ ( - ( π / 2 ) (,) ( π / 2 ) ) ∧ 𝐴 < 0 ) → - 𝐴 < ( tan ‘ - 𝐴 ) )
25 3 22 24 ltled ( ( 𝐴 ∈ ( - ( π / 2 ) (,) ( π / 2 ) ) ∧ 𝐴 < 0 ) → - 𝐴 ≤ ( tan ‘ - 𝐴 ) )
26 0re 0 ∈ ℝ
27 ltle ( ( 𝐴 ∈ ℝ ∧ 0 ∈ ℝ ) → ( 𝐴 < 0 → 𝐴 ≤ 0 ) )
28 1 26 27 sylancl ( 𝐴 ∈ ( - ( π / 2 ) (,) ( π / 2 ) ) → ( 𝐴 < 0 → 𝐴 ≤ 0 ) )
29 28 imp ( ( 𝐴 ∈ ( - ( π / 2 ) (,) ( π / 2 ) ) ∧ 𝐴 < 0 ) → 𝐴 ≤ 0 )
30 2 29 absnidd ( ( 𝐴 ∈ ( - ( π / 2 ) (,) ( π / 2 ) ) ∧ 𝐴 < 0 ) → ( abs ‘ 𝐴 ) = - 𝐴 )
31 1 recnd ( 𝐴 ∈ ( - ( π / 2 ) (,) ( π / 2 ) ) → 𝐴 ∈ ℂ )
32 31 adantr ( ( 𝐴 ∈ ( - ( π / 2 ) (,) ( π / 2 ) ) ∧ 𝐴 < 0 ) → 𝐴 ∈ ℂ )
33 32 negnegd ( ( 𝐴 ∈ ( - ( π / 2 ) (,) ( π / 2 ) ) ∧ 𝐴 < 0 ) → - - 𝐴 = 𝐴 )
34 33 fveq2d ( ( 𝐴 ∈ ( - ( π / 2 ) (,) ( π / 2 ) ) ∧ 𝐴 < 0 ) → ( tan ‘ - - 𝐴 ) = ( tan ‘ 𝐴 ) )
35 32 negcld ( ( 𝐴 ∈ ( - ( π / 2 ) (,) ( π / 2 ) ) ∧ 𝐴 < 0 ) → - 𝐴 ∈ ℂ )
36 tanneg ( ( - 𝐴 ∈ ℂ ∧ ( cos ‘ - 𝐴 ) ≠ 0 ) → ( tan ‘ - - 𝐴 ) = - ( tan ‘ - 𝐴 ) )
37 35 21 36 syl2anc ( ( 𝐴 ∈ ( - ( π / 2 ) (,) ( π / 2 ) ) ∧ 𝐴 < 0 ) → ( tan ‘ - - 𝐴 ) = - ( tan ‘ - 𝐴 ) )
38 34 37 eqtr3d ( ( 𝐴 ∈ ( - ( π / 2 ) (,) ( π / 2 ) ) ∧ 𝐴 < 0 ) → ( tan ‘ 𝐴 ) = - ( tan ‘ - 𝐴 ) )
39 38 fveq2d ( ( 𝐴 ∈ ( - ( π / 2 ) (,) ( π / 2 ) ) ∧ 𝐴 < 0 ) → ( abs ‘ ( tan ‘ 𝐴 ) ) = ( abs ‘ - ( tan ‘ - 𝐴 ) ) )
40 22 recnd ( ( 𝐴 ∈ ( - ( π / 2 ) (,) ( π / 2 ) ) ∧ 𝐴 < 0 ) → ( tan ‘ - 𝐴 ) ∈ ℂ )
41 40 absnegd ( ( 𝐴 ∈ ( - ( π / 2 ) (,) ( π / 2 ) ) ∧ 𝐴 < 0 ) → ( abs ‘ - ( tan ‘ - 𝐴 ) ) = ( abs ‘ ( tan ‘ - 𝐴 ) ) )
42 0red ( ( 𝐴 ∈ ( - ( π / 2 ) (,) ( π / 2 ) ) ∧ 𝐴 < 0 ) → 0 ∈ ℝ )
43 ltle ( ( 0 ∈ ℝ ∧ - 𝐴 ∈ ℝ ) → ( 0 < - 𝐴 → 0 ≤ - 𝐴 ) )
44 26 3 43 sylancr ( ( 𝐴 ∈ ( - ( π / 2 ) (,) ( π / 2 ) ) ∧ 𝐴 < 0 ) → ( 0 < - 𝐴 → 0 ≤ - 𝐴 ) )
45 5 44 mpd ( ( 𝐴 ∈ ( - ( π / 2 ) (,) ( π / 2 ) ) ∧ 𝐴 < 0 ) → 0 ≤ - 𝐴 )
46 42 3 22 45 25 letrd ( ( 𝐴 ∈ ( - ( π / 2 ) (,) ( π / 2 ) ) ∧ 𝐴 < 0 ) → 0 ≤ ( tan ‘ - 𝐴 ) )
47 22 46 absidd ( ( 𝐴 ∈ ( - ( π / 2 ) (,) ( π / 2 ) ) ∧ 𝐴 < 0 ) → ( abs ‘ ( tan ‘ - 𝐴 ) ) = ( tan ‘ - 𝐴 ) )
48 39 41 47 3eqtrd ( ( 𝐴 ∈ ( - ( π / 2 ) (,) ( π / 2 ) ) ∧ 𝐴 < 0 ) → ( abs ‘ ( tan ‘ 𝐴 ) ) = ( tan ‘ - 𝐴 ) )
49 25 30 48 3brtr4d ( ( 𝐴 ∈ ( - ( π / 2 ) (,) ( π / 2 ) ) ∧ 𝐴 < 0 ) → ( abs ‘ 𝐴 ) ≤ ( abs ‘ ( tan ‘ 𝐴 ) ) )
50 abs0 ( abs ‘ 0 ) = 0
51 50 26 eqeltri ( abs ‘ 0 ) ∈ ℝ
52 51 leidi ( abs ‘ 0 ) ≤ ( abs ‘ 0 )
53 52 a1i ( ( 𝐴 ∈ ( - ( π / 2 ) (,) ( π / 2 ) ) ∧ 𝐴 = 0 ) → ( abs ‘ 0 ) ≤ ( abs ‘ 0 ) )
54 simpr ( ( 𝐴 ∈ ( - ( π / 2 ) (,) ( π / 2 ) ) ∧ 𝐴 = 0 ) → 𝐴 = 0 )
55 54 fveq2d ( ( 𝐴 ∈ ( - ( π / 2 ) (,) ( π / 2 ) ) ∧ 𝐴 = 0 ) → ( abs ‘ 𝐴 ) = ( abs ‘ 0 ) )
56 54 fveq2d ( ( 𝐴 ∈ ( - ( π / 2 ) (,) ( π / 2 ) ) ∧ 𝐴 = 0 ) → ( tan ‘ 𝐴 ) = ( tan ‘ 0 ) )
57 tan0 ( tan ‘ 0 ) = 0
58 56 57 eqtrdi ( ( 𝐴 ∈ ( - ( π / 2 ) (,) ( π / 2 ) ) ∧ 𝐴 = 0 ) → ( tan ‘ 𝐴 ) = 0 )
59 58 fveq2d ( ( 𝐴 ∈ ( - ( π / 2 ) (,) ( π / 2 ) ) ∧ 𝐴 = 0 ) → ( abs ‘ ( tan ‘ 𝐴 ) ) = ( abs ‘ 0 ) )
60 53 55 59 3brtr4d ( ( 𝐴 ∈ ( - ( π / 2 ) (,) ( π / 2 ) ) ∧ 𝐴 = 0 ) → ( abs ‘ 𝐴 ) ≤ ( abs ‘ ( tan ‘ 𝐴 ) ) )
61 1 adantr ( ( 𝐴 ∈ ( - ( π / 2 ) (,) ( π / 2 ) ) ∧ 0 < 𝐴 ) → 𝐴 ∈ ℝ )
62 simpr ( ( 𝐴 ∈ ( - ( π / 2 ) (,) ( π / 2 ) ) ∧ 0 < 𝐴 ) → 0 < 𝐴 )
63 6 simprd ( 𝐴 ∈ ( - ( π / 2 ) (,) ( π / 2 ) ) → 𝐴 < ( π / 2 ) )
64 63 adantr ( ( 𝐴 ∈ ( - ( π / 2 ) (,) ( π / 2 ) ) ∧ 0 < 𝐴 ) → 𝐴 < ( π / 2 ) )
65 elioo2 ( ( 0 ∈ ℝ* ∧ ( π / 2 ) ∈ ℝ* ) → ( 𝐴 ∈ ( 0 (,) ( π / 2 ) ) ↔ ( 𝐴 ∈ ℝ ∧ 0 < 𝐴𝐴 < ( π / 2 ) ) ) )
66 13 14 65 mp2an ( 𝐴 ∈ ( 0 (,) ( π / 2 ) ) ↔ ( 𝐴 ∈ ℝ ∧ 0 < 𝐴𝐴 < ( π / 2 ) ) )
67 61 62 64 66 syl3anbrc ( ( 𝐴 ∈ ( - ( π / 2 ) (,) ( π / 2 ) ) ∧ 0 < 𝐴 ) → 𝐴 ∈ ( 0 (,) ( π / 2 ) ) )
68 sincosq1sgn ( 𝐴 ∈ ( 0 (,) ( π / 2 ) ) → ( 0 < ( sin ‘ 𝐴 ) ∧ 0 < ( cos ‘ 𝐴 ) ) )
69 67 68 syl ( ( 𝐴 ∈ ( - ( π / 2 ) (,) ( π / 2 ) ) ∧ 0 < 𝐴 ) → ( 0 < ( sin ‘ 𝐴 ) ∧ 0 < ( cos ‘ 𝐴 ) ) )
70 69 simprd ( ( 𝐴 ∈ ( - ( π / 2 ) (,) ( π / 2 ) ) ∧ 0 < 𝐴 ) → 0 < ( cos ‘ 𝐴 ) )
71 70 gt0ne0d ( ( 𝐴 ∈ ( - ( π / 2 ) (,) ( π / 2 ) ) ∧ 0 < 𝐴 ) → ( cos ‘ 𝐴 ) ≠ 0 )
72 61 71 retancld ( ( 𝐴 ∈ ( - ( π / 2 ) (,) ( π / 2 ) ) ∧ 0 < 𝐴 ) → ( tan ‘ 𝐴 ) ∈ ℝ )
73 tangtx ( 𝐴 ∈ ( 0 (,) ( π / 2 ) ) → 𝐴 < ( tan ‘ 𝐴 ) )
74 67 73 syl ( ( 𝐴 ∈ ( - ( π / 2 ) (,) ( π / 2 ) ) ∧ 0 < 𝐴 ) → 𝐴 < ( tan ‘ 𝐴 ) )
75 61 72 74 ltled ( ( 𝐴 ∈ ( - ( π / 2 ) (,) ( π / 2 ) ) ∧ 0 < 𝐴 ) → 𝐴 ≤ ( tan ‘ 𝐴 ) )
76 ltle ( ( 0 ∈ ℝ ∧ 𝐴 ∈ ℝ ) → ( 0 < 𝐴 → 0 ≤ 𝐴 ) )
77 26 1 76 sylancr ( 𝐴 ∈ ( - ( π / 2 ) (,) ( π / 2 ) ) → ( 0 < 𝐴 → 0 ≤ 𝐴 ) )
78 77 imp ( ( 𝐴 ∈ ( - ( π / 2 ) (,) ( π / 2 ) ) ∧ 0 < 𝐴 ) → 0 ≤ 𝐴 )
79 61 78 absidd ( ( 𝐴 ∈ ( - ( π / 2 ) (,) ( π / 2 ) ) ∧ 0 < 𝐴 ) → ( abs ‘ 𝐴 ) = 𝐴 )
80 0red ( ( 𝐴 ∈ ( - ( π / 2 ) (,) ( π / 2 ) ) ∧ 0 < 𝐴 ) → 0 ∈ ℝ )
81 80 61 72 78 75 letrd ( ( 𝐴 ∈ ( - ( π / 2 ) (,) ( π / 2 ) ) ∧ 0 < 𝐴 ) → 0 ≤ ( tan ‘ 𝐴 ) )
82 72 81 absidd ( ( 𝐴 ∈ ( - ( π / 2 ) (,) ( π / 2 ) ) ∧ 0 < 𝐴 ) → ( abs ‘ ( tan ‘ 𝐴 ) ) = ( tan ‘ 𝐴 ) )
83 75 79 82 3brtr4d ( ( 𝐴 ∈ ( - ( π / 2 ) (,) ( π / 2 ) ) ∧ 0 < 𝐴 ) → ( abs ‘ 𝐴 ) ≤ ( abs ‘ ( tan ‘ 𝐴 ) ) )
84 lttri4 ( ( 𝐴 ∈ ℝ ∧ 0 ∈ ℝ ) → ( 𝐴 < 0 ∨ 𝐴 = 0 ∨ 0 < 𝐴 ) )
85 1 26 84 sylancl ( 𝐴 ∈ ( - ( π / 2 ) (,) ( π / 2 ) ) → ( 𝐴 < 0 ∨ 𝐴 = 0 ∨ 0 < 𝐴 ) )
86 49 60 83 85 mpjao3dan ( 𝐴 ∈ ( - ( π / 2 ) (,) ( π / 2 ) ) → ( abs ‘ 𝐴 ) ≤ ( abs ‘ ( tan ‘ 𝐴 ) ) )