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 e. ( -u ( _pi / 2 ) (,) ( _pi / 2 ) ) -> ( abs ` A ) <_ ( abs ` ( tan ` A ) ) )

Proof

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