This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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