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 ⊢A∈−π2π2→A≤tan⁡A

Proof

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