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