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 ‘ 𝐴 ) ) )