Metamath Proof Explorer

Theorem tanord1

Description: The tangent function is strictly increasing on the nonnegative part of its principal domain. (Lemma for tanord .) (Contributed by Mario Carneiro, 29-Jul-2014) Revised to replace an OLD theorem. (Revised by Wolf Lammen, 20-Sep-2020)

Ref Expression
Assertion tanord1 
|- ( ( A e. ( 0 [,) ( _pi / 2 ) ) /\ B e. ( 0 [,) ( _pi / 2 ) ) ) -> ( A < B <-> ( tan ` A ) < ( tan ` B ) ) )

Proof

Step Hyp Ref Expression
1 tru 
 |-  T.
2 fveq2 
 |-  ( x = y -> ( tan ` x ) = ( tan ` y ) )
3 fveq2 
 |-  ( x = A -> ( tan ` x ) = ( tan ` A ) )
4 fveq2 
 |-  ( x = B -> ( tan ` x ) = ( tan ` B ) )
5 0re 
 |-  0 e. RR
6 halfpire 
 |-  ( _pi / 2 ) e. RR
7 6 rexri 
 |-  ( _pi / 2 ) e. RR*
8 icossre 
 |-  ( ( 0 e. RR /\ ( _pi / 2 ) e. RR* ) -> ( 0 [,) ( _pi / 2 ) ) C_ RR )
9 5 7 8 mp2an 
 |-  ( 0 [,) ( _pi / 2 ) ) C_ RR
10 9 sseli 
 |-  ( x e. ( 0 [,) ( _pi / 2 ) ) -> x e. RR )
11 neghalfpirx 
 |-  -u ( _pi / 2 ) e. RR*
12 pire 
 |-  _pi e. RR
13 2re 
 |-  2 e. RR
14 pipos 
 |-  0 < _pi
15 2pos 
 |-  0 < 2
16 12 13 14 15 divgt0ii 
 |-  0 < ( _pi / 2 )
17 lt0neg2 
 |-  ( ( _pi / 2 ) e. RR -> ( 0 < ( _pi / 2 ) <-> -u ( _pi / 2 ) < 0 ) )
18 6 17 ax-mp 
 |-  ( 0 < ( _pi / 2 ) <-> -u ( _pi / 2 ) < 0 )
19 16 18 mpbi 
 |-  -u ( _pi / 2 ) < 0
20 df-ioo 
 |-  (,) = ( x e. RR* , y e. RR* |-> { z e. RR* | ( x < z /\ z < y ) } )
21 df-ico 
 |-  [,) = ( x e. RR* , y e. RR* |-> { z e. RR* | ( x <_ z /\ z < y ) } )
22 xrltletr 
 |-  ( ( -u ( _pi / 2 ) e. RR* /\ 0 e. RR* /\ w e. RR* ) -> ( ( -u ( _pi / 2 ) < 0 /\ 0 <_ w ) -> -u ( _pi / 2 ) < w ) )
23 20 21 22 ixxss1 
 |-  ( ( -u ( _pi / 2 ) e. RR* /\ -u ( _pi / 2 ) < 0 ) -> ( 0 [,) ( _pi / 2 ) ) C_ ( -u ( _pi / 2 ) (,) ( _pi / 2 ) ) )
24 11 19 23 mp2an 
 |-  ( 0 [,) ( _pi / 2 ) ) C_ ( -u ( _pi / 2 ) (,) ( _pi / 2 ) )
25 24 sseli 
 |-  ( x e. ( 0 [,) ( _pi / 2 ) ) -> x e. ( -u ( _pi / 2 ) (,) ( _pi / 2 ) ) )
26 cosq14gt0 
 |-  ( x e. ( -u ( _pi / 2 ) (,) ( _pi / 2 ) ) -> 0 < ( cos ` x ) )
27 25 26 syl 
 |-  ( x e. ( 0 [,) ( _pi / 2 ) ) -> 0 < ( cos ` x ) )
28 27 gt0ne0d 
 |-  ( x e. ( 0 [,) ( _pi / 2 ) ) -> ( cos ` x ) =/= 0 )
29 10 28 retancld 
 |-  ( x e. ( 0 [,) ( _pi / 2 ) ) -> ( tan ` x ) e. RR )
30 29 adantl 
 |-  ( ( T. /\ x e. ( 0 [,) ( _pi / 2 ) ) ) -> ( tan ` x ) e. RR )
31 10 resincld 
 |-  ( x e. ( 0 [,) ( _pi / 2 ) ) -> ( sin ` x ) e. RR )
32 10 recoscld 
 |-  ( x e. ( 0 [,) ( _pi / 2 ) ) -> ( cos ` x ) e. RR )
33 31 32 28 redivcld 
 |-  ( x e. ( 0 [,) ( _pi / 2 ) ) -> ( ( sin ` x ) / ( cos ` x ) ) e. RR )
34 33 3ad2ant1 
 |-  ( ( x e. ( 0 [,) ( _pi / 2 ) ) /\ y e. ( 0 [,) ( _pi / 2 ) ) /\ x < y ) -> ( ( sin ` x ) / ( cos ` x ) ) e. RR )
35 9 sseli 
 |-  ( y e. ( 0 [,) ( _pi / 2 ) ) -> y e. RR )
36 35 3ad2ant2 
 |-  ( ( x e. ( 0 [,) ( _pi / 2 ) ) /\ y e. ( 0 [,) ( _pi / 2 ) ) /\ x < y ) -> y e. RR )
37 36 resincld 
 |-  ( ( x e. ( 0 [,) ( _pi / 2 ) ) /\ y e. ( 0 [,) ( _pi / 2 ) ) /\ x < y ) -> ( sin ` y ) e. RR )
38 32 3ad2ant1 
 |-  ( ( x e. ( 0 [,) ( _pi / 2 ) ) /\ y e. ( 0 [,) ( _pi / 2 ) ) /\ x < y ) -> ( cos ` x ) e. RR )
39 28 3ad2ant1 
 |-  ( ( x e. ( 0 [,) ( _pi / 2 ) ) /\ y e. ( 0 [,) ( _pi / 2 ) ) /\ x < y ) -> ( cos ` x ) =/= 0 )
40 37 38 39 redivcld 
 |-  ( ( x e. ( 0 [,) ( _pi / 2 ) ) /\ y e. ( 0 [,) ( _pi / 2 ) ) /\ x < y ) -> ( ( sin ` y ) / ( cos ` x ) ) e. RR )
41 36 recoscld 
 |-  ( ( x e. ( 0 [,) ( _pi / 2 ) ) /\ y e. ( 0 [,) ( _pi / 2 ) ) /\ x < y ) -> ( cos ` y ) e. RR )
42 24 sseli 
 |-  ( y e. ( 0 [,) ( _pi / 2 ) ) -> y e. ( -u ( _pi / 2 ) (,) ( _pi / 2 ) ) )
43 cosq14gt0 
 |-  ( y e. ( -u ( _pi / 2 ) (,) ( _pi / 2 ) ) -> 0 < ( cos ` y ) )
44 42 43 syl 
 |-  ( y e. ( 0 [,) ( _pi / 2 ) ) -> 0 < ( cos ` y ) )
45 44 gt0ne0d 
 |-  ( y e. ( 0 [,) ( _pi / 2 ) ) -> ( cos ` y ) =/= 0 )
46 45 3ad2ant2 
 |-  ( ( x e. ( 0 [,) ( _pi / 2 ) ) /\ y e. ( 0 [,) ( _pi / 2 ) ) /\ x < y ) -> ( cos ` y ) =/= 0 )
47 37 41 46 redivcld 
 |-  ( ( x e. ( 0 [,) ( _pi / 2 ) ) /\ y e. ( 0 [,) ( _pi / 2 ) ) /\ x < y ) -> ( ( sin ` y ) / ( cos ` y ) ) e. RR )
48 ioossicc 
 |-  ( -u ( _pi / 2 ) (,) ( _pi / 2 ) ) C_ ( -u ( _pi / 2 ) [,] ( _pi / 2 ) )
49 24 48 sstri 
 |-  ( 0 [,) ( _pi / 2 ) ) C_ ( -u ( _pi / 2 ) [,] ( _pi / 2 ) )
50 49 sseli 
 |-  ( x e. ( 0 [,) ( _pi / 2 ) ) -> x e. ( -u ( _pi / 2 ) [,] ( _pi / 2 ) ) )
51 49 sseli 
 |-  ( y e. ( 0 [,) ( _pi / 2 ) ) -> y e. ( -u ( _pi / 2 ) [,] ( _pi / 2 ) ) )
52 sinord 
 |-  ( ( x e. ( -u ( _pi / 2 ) [,] ( _pi / 2 ) ) /\ y e. ( -u ( _pi / 2 ) [,] ( _pi / 2 ) ) ) -> ( x < y <-> ( sin ` x ) < ( sin ` y ) ) )
53 50 51 52 syl2an 
 |-  ( ( x e. ( 0 [,) ( _pi / 2 ) ) /\ y e. ( 0 [,) ( _pi / 2 ) ) ) -> ( x < y <-> ( sin ` x ) < ( sin ` y ) ) )
54 53 biimp3a 
 |-  ( ( x e. ( 0 [,) ( _pi / 2 ) ) /\ y e. ( 0 [,) ( _pi / 2 ) ) /\ x < y ) -> ( sin ` x ) < ( sin ` y ) )
55 10 3ad2ant1 
 |-  ( ( x e. ( 0 [,) ( _pi / 2 ) ) /\ y e. ( 0 [,) ( _pi / 2 ) ) /\ x < y ) -> x e. RR )
56 55 resincld 
 |-  ( ( x e. ( 0 [,) ( _pi / 2 ) ) /\ y e. ( 0 [,) ( _pi / 2 ) ) /\ x < y ) -> ( sin ` x ) e. RR )
57 27 3ad2ant1 
 |-  ( ( x e. ( 0 [,) ( _pi / 2 ) ) /\ y e. ( 0 [,) ( _pi / 2 ) ) /\ x < y ) -> 0 < ( cos ` x ) )
58 ltdiv1 
 |-  ( ( ( sin ` x ) e. RR /\ ( sin ` y ) e. RR /\ ( ( cos ` x ) e. RR /\ 0 < ( cos ` x ) ) ) -> ( ( sin ` x ) < ( sin ` y ) <-> ( ( sin ` x ) / ( cos ` x ) ) < ( ( sin ` y ) / ( cos ` x ) ) ) )
59 56 37 38 57 58 syl112anc 
 |-  ( ( x e. ( 0 [,) ( _pi / 2 ) ) /\ y e. ( 0 [,) ( _pi / 2 ) ) /\ x < y ) -> ( ( sin ` x ) < ( sin ` y ) <-> ( ( sin ` x ) / ( cos ` x ) ) < ( ( sin ` y ) / ( cos ` x ) ) ) )
60 54 59 mpbid 
 |-  ( ( x e. ( 0 [,) ( _pi / 2 ) ) /\ y e. ( 0 [,) ( _pi / 2 ) ) /\ x < y ) -> ( ( sin ` x ) / ( cos ` x ) ) < ( ( sin ` y ) / ( cos ` x ) ) )
61 12 rexri 
 |-  _pi e. RR*
62 pirp 
 |-  _pi e. RR+
63 rphalflt 
 |-  ( _pi e. RR+ -> ( _pi / 2 ) < _pi )
64 62 63 ax-mp 
 |-  ( _pi / 2 ) < _pi
65 df-icc 
 |-  [,] = ( x e. RR* , y e. RR* |-> { z e. RR* | ( x <_ z /\ z <_ y ) } )
66 xrlttr 
 |-  ( ( w e. RR* /\ ( _pi / 2 ) e. RR* /\ _pi e. RR* ) -> ( ( w < ( _pi / 2 ) /\ ( _pi / 2 ) < _pi ) -> w < _pi ) )
67 xrltle 
 |-  ( ( w e. RR* /\ _pi e. RR* ) -> ( w < _pi -> w <_ _pi ) )
68 67 3adant2 
 |-  ( ( w e. RR* /\ ( _pi / 2 ) e. RR* /\ _pi e. RR* ) -> ( w < _pi -> w <_ _pi ) )
69 66 68 syld 
 |-  ( ( w e. RR* /\ ( _pi / 2 ) e. RR* /\ _pi e. RR* ) -> ( ( w < ( _pi / 2 ) /\ ( _pi / 2 ) < _pi ) -> w <_ _pi ) )
70 65 21 69 ixxss2 
 |-  ( ( _pi e. RR* /\ ( _pi / 2 ) < _pi ) -> ( 0 [,) ( _pi / 2 ) ) C_ ( 0 [,] _pi ) )
71 61 64 70 mp2an 
 |-  ( 0 [,) ( _pi / 2 ) ) C_ ( 0 [,] _pi )
72 71 sseli 
 |-  ( x e. ( 0 [,) ( _pi / 2 ) ) -> x e. ( 0 [,] _pi ) )
73 71 sseli 
 |-  ( y e. ( 0 [,) ( _pi / 2 ) ) -> y e. ( 0 [,] _pi ) )
74 cosord 
 |-  ( ( x e. ( 0 [,] _pi ) /\ y e. ( 0 [,] _pi ) ) -> ( x < y <-> ( cos ` y ) < ( cos ` x ) ) )
75 72 73 74 syl2an 
 |-  ( ( x e. ( 0 [,) ( _pi / 2 ) ) /\ y e. ( 0 [,) ( _pi / 2 ) ) ) -> ( x < y <-> ( cos ` y ) < ( cos ` x ) ) )
76 75 biimp3a 
 |-  ( ( x e. ( 0 [,) ( _pi / 2 ) ) /\ y e. ( 0 [,) ( _pi / 2 ) ) /\ x < y ) -> ( cos ` y ) < ( cos ` x ) )
77 0red 
 |-  ( ( x e. ( 0 [,) ( _pi / 2 ) ) /\ y e. ( 0 [,) ( _pi / 2 ) ) /\ x < y ) -> 0 e. RR )
78 simp1 
 |-  ( ( x e. ( 0 [,) ( _pi / 2 ) ) /\ y e. ( 0 [,) ( _pi / 2 ) ) /\ x < y ) -> x e. ( 0 [,) ( _pi / 2 ) ) )
79 elico2 
 |-  ( ( 0 e. RR /\ ( _pi / 2 ) e. RR* ) -> ( x e. ( 0 [,) ( _pi / 2 ) ) <-> ( x e. RR /\ 0 <_ x /\ x < ( _pi / 2 ) ) ) )
80 5 7 79 mp2an 
 |-  ( x e. ( 0 [,) ( _pi / 2 ) ) <-> ( x e. RR /\ 0 <_ x /\ x < ( _pi / 2 ) ) )
81 78 80 sylib 
 |-  ( ( x e. ( 0 [,) ( _pi / 2 ) ) /\ y e. ( 0 [,) ( _pi / 2 ) ) /\ x < y ) -> ( x e. RR /\ 0 <_ x /\ x < ( _pi / 2 ) ) )
82 81 simp2d 
 |-  ( ( x e. ( 0 [,) ( _pi / 2 ) ) /\ y e. ( 0 [,) ( _pi / 2 ) ) /\ x < y ) -> 0 <_ x )
83 simp3 
 |-  ( ( x e. ( 0 [,) ( _pi / 2 ) ) /\ y e. ( 0 [,) ( _pi / 2 ) ) /\ x < y ) -> x < y )
84 77 55 36 82 83 lelttrd 
 |-  ( ( x e. ( 0 [,) ( _pi / 2 ) ) /\ y e. ( 0 [,) ( _pi / 2 ) ) /\ x < y ) -> 0 < y )
85 simp2 
 |-  ( ( x e. ( 0 [,) ( _pi / 2 ) ) /\ y e. ( 0 [,) ( _pi / 2 ) ) /\ x < y ) -> y e. ( 0 [,) ( _pi / 2 ) ) )
86 elico2 
 |-  ( ( 0 e. RR /\ ( _pi / 2 ) e. RR* ) -> ( y e. ( 0 [,) ( _pi / 2 ) ) <-> ( y e. RR /\ 0 <_ y /\ y < ( _pi / 2 ) ) ) )
87 5 7 86 mp2an 
 |-  ( y e. ( 0 [,) ( _pi / 2 ) ) <-> ( y e. RR /\ 0 <_ y /\ y < ( _pi / 2 ) ) )
88 85 87 sylib 
 |-  ( ( x e. ( 0 [,) ( _pi / 2 ) ) /\ y e. ( 0 [,) ( _pi / 2 ) ) /\ x < y ) -> ( y e. RR /\ 0 <_ y /\ y < ( _pi / 2 ) ) )
89 88 simp3d 
 |-  ( ( x e. ( 0 [,) ( _pi / 2 ) ) /\ y e. ( 0 [,) ( _pi / 2 ) ) /\ x < y ) -> y < ( _pi / 2 ) )
90 0xr 
 |-  0 e. RR*
91 elioo2 
 |-  ( ( 0 e. RR* /\ ( _pi / 2 ) e. RR* ) -> ( y e. ( 0 (,) ( _pi / 2 ) ) <-> ( y e. RR /\ 0 < y /\ y < ( _pi / 2 ) ) ) )
92 90 7 91 mp2an 
 |-  ( y e. ( 0 (,) ( _pi / 2 ) ) <-> ( y e. RR /\ 0 < y /\ y < ( _pi / 2 ) ) )
93 36 84 89 92 syl3anbrc 
 |-  ( ( x e. ( 0 [,) ( _pi / 2 ) ) /\ y e. ( 0 [,) ( _pi / 2 ) ) /\ x < y ) -> y e. ( 0 (,) ( _pi / 2 ) ) )
94 sincosq1sgn 
 |-  ( y e. ( 0 (,) ( _pi / 2 ) ) -> ( 0 < ( sin ` y ) /\ 0 < ( cos ` y ) ) )
95 93 94 syl 
 |-  ( ( x e. ( 0 [,) ( _pi / 2 ) ) /\ y e. ( 0 [,) ( _pi / 2 ) ) /\ x < y ) -> ( 0 < ( sin ` y ) /\ 0 < ( cos ` y ) ) )
96 95 simprd 
 |-  ( ( x e. ( 0 [,) ( _pi / 2 ) ) /\ y e. ( 0 [,) ( _pi / 2 ) ) /\ x < y ) -> 0 < ( cos ` y ) )
97 95 simpld 
 |-  ( ( x e. ( 0 [,) ( _pi / 2 ) ) /\ y e. ( 0 [,) ( _pi / 2 ) ) /\ x < y ) -> 0 < ( sin ` y ) )
98 ltdiv2 
 |-  ( ( ( ( cos ` y ) e. RR /\ 0 < ( cos ` y ) ) /\ ( ( cos ` x ) e. RR /\ 0 < ( cos ` x ) ) /\ ( ( sin ` y ) e. RR /\ 0 < ( sin ` y ) ) ) -> ( ( cos ` y ) < ( cos ` x ) <-> ( ( sin ` y ) / ( cos ` x ) ) < ( ( sin ` y ) / ( cos ` y ) ) ) )
99 41 96 38 57 37 97 98 syl222anc 
 |-  ( ( x e. ( 0 [,) ( _pi / 2 ) ) /\ y e. ( 0 [,) ( _pi / 2 ) ) /\ x < y ) -> ( ( cos ` y ) < ( cos ` x ) <-> ( ( sin ` y ) / ( cos ` x ) ) < ( ( sin ` y ) / ( cos ` y ) ) ) )
100 76 99 mpbid 
 |-  ( ( x e. ( 0 [,) ( _pi / 2 ) ) /\ y e. ( 0 [,) ( _pi / 2 ) ) /\ x < y ) -> ( ( sin ` y ) / ( cos ` x ) ) < ( ( sin ` y ) / ( cos ` y ) ) )
101 34 40 47 60 100 lttrd 
 |-  ( ( x e. ( 0 [,) ( _pi / 2 ) ) /\ y e. ( 0 [,) ( _pi / 2 ) ) /\ x < y ) -> ( ( sin ` x ) / ( cos ` x ) ) < ( ( sin ` y ) / ( cos ` y ) ) )
102 10 recnd 
 |-  ( x e. ( 0 [,) ( _pi / 2 ) ) -> x e. CC )
103 tanval 
 |-  ( ( x e. CC /\ ( cos ` x ) =/= 0 ) -> ( tan ` x ) = ( ( sin ` x ) / ( cos ` x ) ) )
104 102 28 103 syl2anc 
 |-  ( x e. ( 0 [,) ( _pi / 2 ) ) -> ( tan ` x ) = ( ( sin ` x ) / ( cos ` x ) ) )
105 104 3ad2ant1 
 |-  ( ( x e. ( 0 [,) ( _pi / 2 ) ) /\ y e. ( 0 [,) ( _pi / 2 ) ) /\ x < y ) -> ( tan ` x ) = ( ( sin ` x ) / ( cos ` x ) ) )
106 35 recnd 
 |-  ( y e. ( 0 [,) ( _pi / 2 ) ) -> y e. CC )
107 106 3ad2ant2 
 |-  ( ( x e. ( 0 [,) ( _pi / 2 ) ) /\ y e. ( 0 [,) ( _pi / 2 ) ) /\ x < y ) -> y e. CC )
108 tanval 
 |-  ( ( y e. CC /\ ( cos ` y ) =/= 0 ) -> ( tan ` y ) = ( ( sin ` y ) / ( cos ` y ) ) )
109 107 46 108 syl2anc 
 |-  ( ( x e. ( 0 [,) ( _pi / 2 ) ) /\ y e. ( 0 [,) ( _pi / 2 ) ) /\ x < y ) -> ( tan ` y ) = ( ( sin ` y ) / ( cos ` y ) ) )
110 101 105 109 3brtr4d 
 |-  ( ( x e. ( 0 [,) ( _pi / 2 ) ) /\ y e. ( 0 [,) ( _pi / 2 ) ) /\ x < y ) -> ( tan ` x ) < ( tan ` y ) )
111 110 3expia 
 |-  ( ( x e. ( 0 [,) ( _pi / 2 ) ) /\ y e. ( 0 [,) ( _pi / 2 ) ) ) -> ( x < y -> ( tan ` x ) < ( tan ` y ) ) )
112 111 adantl 
 |-  ( ( T. /\ ( x e. ( 0 [,) ( _pi / 2 ) ) /\ y e. ( 0 [,) ( _pi / 2 ) ) ) ) -> ( x < y -> ( tan ` x ) < ( tan ` y ) ) )
113 2 3 4 9 30 112 ltord1 
 |-  ( ( T. /\ ( A e. ( 0 [,) ( _pi / 2 ) ) /\ B e. ( 0 [,) ( _pi / 2 ) ) ) ) -> ( A < B <-> ( tan ` A ) < ( tan ` B ) ) )
114 1 113 mpan 
 |-  ( ( A e. ( 0 [,) ( _pi / 2 ) ) /\ B e. ( 0 [,) ( _pi / 2 ) ) ) -> ( A < B <-> ( tan ` A ) < ( tan ` B ) ) )