Metamath Proof Explorer


Theorem tanord

Description: The tangent function is strictly increasing on its principal domain. (Contributed by Mario Carneiro, 4-Apr-2015)

Ref Expression
Assertion tanord A π 2 π 2 B π 2 π 2 A < B tan A < tan B

Proof

Step Hyp Ref Expression
1 tru
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 ioossre π 2 π 2
6 elioore x π 2 π 2 x
7 6 recnd x π 2 π 2 x
8 6 rered x π 2 π 2 x = x
9 id x π 2 π 2 x π 2 π 2
10 8 9 eqeltrd x π 2 π 2 x π 2 π 2
11 cosne0 x x π 2 π 2 cos x 0
12 7 10 11 syl2anc x π 2 π 2 cos x 0
13 6 12 retancld x π 2 π 2 tan x
14 13 adantl x π 2 π 2 tan x
15 6 3ad2ant1 x π 2 π 2 y π 2 π 2 x < y x
16 15 adantr x π 2 π 2 y π 2 π 2 x < y x < 0 x
17 16 recnd x π 2 π 2 y π 2 π 2 x < y x < 0 x
18 17 negnegd x π 2 π 2 y π 2 π 2 x < y x < 0 x = x
19 18 fveq2d x π 2 π 2 y π 2 π 2 x < y x < 0 tan x = tan x
20 17 negcld x π 2 π 2 y π 2 π 2 x < y x < 0 x
21 cosneg x cos x = cos x
22 17 21 syl x π 2 π 2 y π 2 π 2 x < y x < 0 cos x = cos x
23 simpl1 x π 2 π 2 y π 2 π 2 x < y x < 0 x π 2 π 2
24 23 12 syl x π 2 π 2 y π 2 π 2 x < y x < 0 cos x 0
25 22 24 eqnetrd x π 2 π 2 y π 2 π 2 x < y x < 0 cos x 0
26 tanneg x cos x 0 tan x = tan x
27 20 25 26 syl2anc x π 2 π 2 y π 2 π 2 x < y x < 0 tan x = tan x
28 19 27 eqtr3d x π 2 π 2 y π 2 π 2 x < y x < 0 tan x = tan x
29 15 adantr x π 2 π 2 y π 2 π 2 x < y x < 0 0 < y x
30 29 renegcld x π 2 π 2 y π 2 π 2 x < y x < 0 0 < y x
31 25 adantrr x π 2 π 2 y π 2 π 2 x < y x < 0 0 < y cos x 0
32 30 31 retancld x π 2 π 2 y π 2 π 2 x < y x < 0 0 < y tan x
33 32 renegcld x π 2 π 2 y π 2 π 2 x < y x < 0 0 < y tan x
34 0red x π 2 π 2 y π 2 π 2 x < y x < 0 0 < y 0
35 simp2 x π 2 π 2 y π 2 π 2 x < y y π 2 π 2
36 5 35 sselid x π 2 π 2 y π 2 π 2 x < y y
37 36 adantr x π 2 π 2 y π 2 π 2 x < y x < 0 0 < y y
38 simpl2 x π 2 π 2 y π 2 π 2 x < y x < 0 0 < y y π 2 π 2
39 elioore y π 2 π 2 y
40 39 recnd y π 2 π 2 y
41 39 rered y π 2 π 2 y = y
42 id y π 2 π 2 y π 2 π 2
43 41 42 eqeltrd y π 2 π 2 y π 2 π 2
44 cosne0 y y π 2 π 2 cos y 0
45 40 43 44 syl2anc y π 2 π 2 cos y 0
46 38 45 syl x π 2 π 2 y π 2 π 2 x < y x < 0 0 < y cos y 0
47 37 46 retancld x π 2 π 2 y π 2 π 2 x < y x < 0 0 < y tan y
48 simprl x π 2 π 2 y π 2 π 2 x < y x < 0 0 < y x < 0
49 29 lt0neg1d x π 2 π 2 y π 2 π 2 x < y x < 0 0 < y x < 0 0 < x
50 48 49 mpbid x π 2 π 2 y π 2 π 2 x < y x < 0 0 < y 0 < x
51 simpl1 x π 2 π 2 y π 2 π 2 x < y x < 0 0 < y x π 2 π 2
52 eliooord x π 2 π 2 π 2 < x x < π 2
53 51 52 syl x π 2 π 2 y π 2 π 2 x < y x < 0 0 < y π 2 < x x < π 2
54 53 simpld x π 2 π 2 y π 2 π 2 x < y x < 0 0 < y π 2 < x
55 halfpire π 2
56 ltnegcon1 π 2 x π 2 < x x < π 2
57 55 29 56 sylancr x π 2 π 2 y π 2 π 2 x < y x < 0 0 < y π 2 < x x < π 2
58 54 57 mpbid x π 2 π 2 y π 2 π 2 x < y x < 0 0 < y x < π 2
59 0xr 0 *
60 55 rexri π 2 *
61 elioo2 0 * π 2 * x 0 π 2 x 0 < x x < π 2
62 59 60 61 mp2an x 0 π 2 x 0 < x x < π 2
63 30 50 58 62 syl3anbrc x π 2 π 2 y π 2 π 2 x < y x < 0 0 < y x 0 π 2
64 tanrpcl x 0 π 2 tan x +
65 63 64 syl x π 2 π 2 y π 2 π 2 x < y x < 0 0 < y tan x +
66 65 rpgt0d x π 2 π 2 y π 2 π 2 x < y x < 0 0 < y 0 < tan x
67 32 lt0neg2d x π 2 π 2 y π 2 π 2 x < y x < 0 0 < y 0 < tan x tan x < 0
68 66 67 mpbid x π 2 π 2 y π 2 π 2 x < y x < 0 0 < y tan x < 0
69 simprr x π 2 π 2 y π 2 π 2 x < y x < 0 0 < y 0 < y
70 eliooord y π 2 π 2 π 2 < y y < π 2
71 38 70 syl x π 2 π 2 y π 2 π 2 x < y x < 0 0 < y π 2 < y y < π 2
72 71 simprd x π 2 π 2 y π 2 π 2 x < y x < 0 0 < y y < π 2
73 elioo2 0 * π 2 * y 0 π 2 y 0 < y y < π 2
74 59 60 73 mp2an y 0 π 2 y 0 < y y < π 2
75 37 69 72 74 syl3anbrc x π 2 π 2 y π 2 π 2 x < y x < 0 0 < y y 0 π 2
76 tanrpcl y 0 π 2 tan y +
77 75 76 syl x π 2 π 2 y π 2 π 2 x < y x < 0 0 < y tan y +
78 77 rpgt0d x π 2 π 2 y π 2 π 2 x < y x < 0 0 < y 0 < tan y
79 33 34 47 68 78 lttrd x π 2 π 2 y π 2 π 2 x < y x < 0 0 < y tan x < tan y
80 79 anassrs x π 2 π 2 y π 2 π 2 x < y x < 0 0 < y tan x < tan y
81 simpl3 x π 2 π 2 y π 2 π 2 x < y y 0 x < y
82 15 adantr x π 2 π 2 y π 2 π 2 x < y y 0 x
83 36 adantr x π 2 π 2 y π 2 π 2 x < y y 0 y
84 82 83 ltnegd x π 2 π 2 y π 2 π 2 x < y y 0 x < y y < x
85 81 84 mpbid x π 2 π 2 y π 2 π 2 x < y y 0 y < x
86 83 renegcld x π 2 π 2 y π 2 π 2 x < y y 0 y
87 simpr x π 2 π 2 y π 2 π 2 x < y y 0 y 0
88 83 le0neg1d x π 2 π 2 y π 2 π 2 x < y y 0 y 0 0 y
89 87 88 mpbid x π 2 π 2 y π 2 π 2 x < y y 0 0 y
90 simpl2 x π 2 π 2 y π 2 π 2 x < y y 0 y π 2 π 2
91 90 70 syl x π 2 π 2 y π 2 π 2 x < y y 0 π 2 < y y < π 2
92 91 simpld x π 2 π 2 y π 2 π 2 x < y y 0 π 2 < y
93 ltnegcon1 π 2 y π 2 < y y < π 2
94 55 83 93 sylancr x π 2 π 2 y π 2 π 2 x < y y 0 π 2 < y y < π 2
95 92 94 mpbid x π 2 π 2 y π 2 π 2 x < y y 0 y < π 2
96 0re 0
97 elico2 0 π 2 * y 0 π 2 y 0 y y < π 2
98 96 60 97 mp2an y 0 π 2 y 0 y y < π 2
99 86 89 95 98 syl3anbrc x π 2 π 2 y π 2 π 2 x < y y 0 y 0 π 2
100 82 renegcld x π 2 π 2 y π 2 π 2 x < y y 0 x
101 simp3 x π 2 π 2 y π 2 π 2 x < y x < y
102 0red x π 2 π 2 y π 2 π 2 x < y 0
103 ltletr x y 0 x < y y 0 x < 0
104 15 36 102 103 syl3anc x π 2 π 2 y π 2 π 2 x < y x < y y 0 x < 0
105 101 104 mpand x π 2 π 2 y π 2 π 2 x < y y 0 x < 0
106 105 imp x π 2 π 2 y π 2 π 2 x < y y 0 x < 0
107 ltle x 0 x < 0 x 0
108 82 96 107 sylancl x π 2 π 2 y π 2 π 2 x < y y 0 x < 0 x 0
109 106 108 mpd x π 2 π 2 y π 2 π 2 x < y y 0 x 0
110 82 le0neg1d x π 2 π 2 y π 2 π 2 x < y y 0 x 0 0 x
111 109 110 mpbid x π 2 π 2 y π 2 π 2 x < y y 0 0 x
112 simpl1 x π 2 π 2 y π 2 π 2 x < y y 0 x π 2 π 2
113 112 52 syl x π 2 π 2 y π 2 π 2 x < y y 0 π 2 < x x < π 2
114 113 simpld x π 2 π 2 y π 2 π 2 x < y y 0 π 2 < x
115 55 82 56 sylancr x π 2 π 2 y π 2 π 2 x < y y 0 π 2 < x x < π 2
116 114 115 mpbid x π 2 π 2 y π 2 π 2 x < y y 0 x < π 2
117 elico2 0 π 2 * x 0 π 2 x 0 x x < π 2
118 96 60 117 mp2an x 0 π 2 x 0 x x < π 2
119 100 111 116 118 syl3anbrc x π 2 π 2 y π 2 π 2 x < y y 0 x 0 π 2
120 tanord1 y 0 π 2 x 0 π 2 y < x tan y < tan x
121 99 119 120 syl2anc x π 2 π 2 y π 2 π 2 x < y y 0 y < x tan y < tan x
122 85 121 mpbid x π 2 π 2 y π 2 π 2 x < y y 0 tan y < tan x
123 83 recnd x π 2 π 2 y π 2 π 2 x < y y 0 y
124 cosneg y cos y = cos y
125 123 124 syl x π 2 π 2 y π 2 π 2 x < y y 0 cos y = cos y
126 90 45 syl x π 2 π 2 y π 2 π 2 x < y y 0 cos y 0
127 125 126 eqnetrd x π 2 π 2 y π 2 π 2 x < y y 0 cos y 0
128 86 127 retancld x π 2 π 2 y π 2 π 2 x < y y 0 tan y
129 106 25 syldan x π 2 π 2 y π 2 π 2 x < y y 0 cos x 0
130 100 129 retancld x π 2 π 2 y π 2 π 2 x < y y 0 tan x
131 128 130 ltnegd x π 2 π 2 y π 2 π 2 x < y y 0 tan y < tan x tan x < tan y
132 122 131 mpbid x π 2 π 2 y π 2 π 2 x < y y 0 tan x < tan y
133 123 negnegd x π 2 π 2 y π 2 π 2 x < y y 0 y = y
134 133 fveq2d x π 2 π 2 y π 2 π 2 x < y y 0 tan y = tan y
135 123 negcld x π 2 π 2 y π 2 π 2 x < y y 0 y
136 tanneg y cos y 0 tan y = tan y
137 135 127 136 syl2anc x π 2 π 2 y π 2 π 2 x < y y 0 tan y = tan y
138 134 137 eqtr3d x π 2 π 2 y π 2 π 2 x < y y 0 tan y = tan y
139 132 138 breqtrrd x π 2 π 2 y π 2 π 2 x < y y 0 tan x < tan y
140 139 adantlr x π 2 π 2 y π 2 π 2 x < y x < 0 y 0 tan x < tan y
141 0red x π 2 π 2 y π 2 π 2 x < y x < 0 0
142 simpl2 x π 2 π 2 y π 2 π 2 x < y x < 0 y π 2 π 2
143 5 142 sselid x π 2 π 2 y π 2 π 2 x < y x < 0 y
144 80 140 141 143 ltlecasei x π 2 π 2 y π 2 π 2 x < y x < 0 tan x < tan y
145 28 144 eqbrtrd x π 2 π 2 y π 2 π 2 x < y x < 0 tan x < tan y
146 simpl3 x π 2 π 2 y π 2 π 2 x < y 0 x x < y
147 15 adantr x π 2 π 2 y π 2 π 2 x < y 0 x x
148 simpr x π 2 π 2 y π 2 π 2 x < y 0 x 0 x
149 simpl1 x π 2 π 2 y π 2 π 2 x < y 0 x x π 2 π 2
150 149 52 syl x π 2 π 2 y π 2 π 2 x < y 0 x π 2 < x x < π 2
151 150 simprd x π 2 π 2 y π 2 π 2 x < y 0 x x < π 2
152 elico2 0 π 2 * x 0 π 2 x 0 x x < π 2
153 96 60 152 mp2an x 0 π 2 x 0 x x < π 2
154 147 148 151 153 syl3anbrc x π 2 π 2 y π 2 π 2 x < y 0 x x 0 π 2
155 simpl2 x π 2 π 2 y π 2 π 2 x < y 0 x y π 2 π 2
156 5 155 sselid x π 2 π 2 y π 2 π 2 x < y 0 x y
157 0red x π 2 π 2 y π 2 π 2 x < y 0 x 0
158 147 156 146 ltled x π 2 π 2 y π 2 π 2 x < y 0 x x y
159 157 147 156 148 158 letrd x π 2 π 2 y π 2 π 2 x < y 0 x 0 y
160 155 70 syl x π 2 π 2 y π 2 π 2 x < y 0 x π 2 < y y < π 2
161 160 simprd x π 2 π 2 y π 2 π 2 x < y 0 x y < π 2
162 elico2 0 π 2 * y 0 π 2 y 0 y y < π 2
163 96 60 162 mp2an y 0 π 2 y 0 y y < π 2
164 156 159 161 163 syl3anbrc x π 2 π 2 y π 2 π 2 x < y 0 x y 0 π 2
165 tanord1 x 0 π 2 y 0 π 2 x < y tan x < tan y
166 154 164 165 syl2anc x π 2 π 2 y π 2 π 2 x < y 0 x x < y tan x < tan y
167 146 166 mpbid x π 2 π 2 y π 2 π 2 x < y 0 x tan x < tan y
168 145 167 15 102 ltlecasei x π 2 π 2 y π 2 π 2 x < y tan x < tan y
169 168 3expia x π 2 π 2 y π 2 π 2 x < y tan x < tan y
170 169 adantl x π 2 π 2 y π 2 π 2 x < y tan x < tan y
171 2 3 4 5 14 170 ltord1 A π 2 π 2 B π 2 π 2 A < B tan A < tan B
172 1 171 mpan A π 2 π 2 B π 2 π 2 A < B tan A < tan B