tangtx - Intuitionistic Logic Explorer

	Intuitionistic Logic Explorer		< Previous Next > Nearby theorems
Mirrors > Home > ILE Home > Th. List > tangtx		Unicode version

Theorem tangtx 15862

Description: The tangent function is greater than its argument on positive reals in its principal domain. (Contributed by Mario Carneiro, 29-Jul-2014.)

**Assertion**
Ref	Expression
tangtx

**Proof of Theorem tangtx**
Step	Hyp	Ref	Expression
1		elioore 10293	. . . . 5
2	1	recoscld 12469	. . . . 5
3	1, 2	remulcld 8346	. . . 4
4		1re 8315	. . . . . . 7
5		rehalfcl 9511	. . . . . . . . . 10
6	1, 5	syl 14	. . . . . . . . 9
7	6	resqcld 11115	. . . . . . . 8
8		3nn 9446	. . . . . . . 8
9		nndivre 9319	. . . . . . . 8 $/\$
10	7, 8, 9	sylancl 417	. . . . . . 7
11		resubcl 8580	. . . . . . 7 $/\$
12	4, 10, 11	sylancr 418	. . . . . 6
13	1, 12	remulcld 8346	. . . . 5
14		2re 9353	. . . . . . 7
15		remulcl 8297	. . . . . . 7 $/\$
16	14, 10, 15	sylancr 418	. . . . . 6
17		resubcl 8580	. . . . . 6 $/\$
18	4, 16, 17	sylancr 418	. . . . 5
19	13, 18	remulcld 8346	. . . 4
20	1	resincld 12468	. . . 4
21	12	resqcld 11115	. . . . . . . . 9
22		remulcl 8297	. . . . . . . . 9 $/\$
23	14, 21, 22	sylancr 418	. . . . . . . 8
24		resubcl 8580	. . . . . . . 8 $/\$
25	23, 4, 24	sylancl 417	. . . . . . 7
26	12, 18	remulcld 8346	. . . . . . 7
27	1	recnd 8344	. . . . . . . . . . 11
28		2cn 9354	. . . . . . . . . . . 12
29	28	a1i 9	. . . . . . . . . . 11
30		2ap0 9376	. . . . . . . . . . . 12 #
31	30	a1i 9	. . . . . . . . . . 11 #
32	27, 29, 31	divcanap2d 9112	. . . . . . . . . 10
33	32	fveq2d 5694	. . . . . . . . 9
34	6	recnd 8344	. . . . . . . . . 10
35		cos2t 12495	. . . . . . . . . 10
36	34, 35	syl 14	. . . . . . . . 9
37	33, 36	eqtr3d 2273	. . . . . . . 8
38	6	recoscld 12469	. . . . . . . . . . 11
39	38	resqcld 11115	. . . . . . . . . 10
40		remulcl 8297	. . . . . . . . . 10 $/\$
41	14, 39, 40	sylancr 418	. . . . . . . . 9
42	4	a1i 9	. . . . . . . . 9
43	14	a1i 9	. . . . . . . . . . . . . . 15
44		eliooord 10309	. . . . . . . . . . . . . . . 16 $/\$
45	44	simpld 112	. . . . . . . . . . . . . . 15
46		2pos 9374	. . . . . . . . . . . . . . . 16
47	46	a1i 9	. . . . . . . . . . . . . . 15
48	1, 43, 45, 47	divgt0d 9255	. . . . . . . . . . . . . 14
49		pire 15810	. . . . . . . . . . . . . . . . . . 19
50		rehalfcl 9511	. . . . . . . . . . . . . . . . . . 19
51	49, 50	mp1i 10	. . . . . . . . . . . . . . . . . 18
52	44	simprd 114	. . . . . . . . . . . . . . . . . 18
53		pigt2lt4 15808	. . . . . . . . . . . . . . . . . . . . . 22 $/\$
54	53	simpri 113	. . . . . . . . . . . . . . . . . . . . 21
55		2t2e4 9438	. . . . . . . . . . . . . . . . . . . . 21
56	54, 55	breqtrri 4152	. . . . . . . . . . . . . . . . . . . 20
57	14, 46	pm3.2i 272	. . . . . . . . . . . . . . . . . . . . 21 $/\$
58		ltdivmul 9196	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$ $/\$
59	49, 14, 57, 58	mp3an 1378	. . . . . . . . . . . . . . . . . . . 20
60	56, 59	mpbir 146	. . . . . . . . . . . . . . . . . . 19
61	60	a1i 9	. . . . . . . . . . . . . . . . . 18
62	1, 51, 43, 52, 61	lttrd 8442	. . . . . . . . . . . . . . . . 17
63	28	mullidi 8319	. . . . . . . . . . . . . . . . 17
64	62, 63	breqtrrdi 4167	. . . . . . . . . . . . . . . 16
65		ltdivmul2 9198	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$
66	1, 42, 43, 47, 65	syl112anc 1282	. . . . . . . . . . . . . . . 16
67	64, 66	mpbird 167	. . . . . . . . . . . . . . 15
68	6, 42, 67	ltled 8435	. . . . . . . . . . . . . 14
69		0xr 8362	. . . . . . . . . . . . . . 15
70		elioc2 10317	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$
71	69, 4, 70	mp2an 430	. . . . . . . . . . . . . 14 $/\$ $/\$
72	6, 48, 68, 71	syl3anbrc 1212	. . . . . . . . . . . . 13
73		cos01bnd 12503	. . . . . . . . . . . . 13 $/\$
74	72, 73	syl 14	. . . . . . . . . . . 12 $/\$
75	74	simprd 114	. . . . . . . . . . 11
76		cos01gt0 12508	. . . . . . . . . . . . . 14
77	72, 76	syl 14	. . . . . . . . . . . . 13
78		0re 8316	. . . . . . . . . . . . . 14
79		ltle 8403	. . . . . . . . . . . . . 14 $/\$
80	78, 38, 79	sylancr 418	. . . . . . . . . . . . 13
81	77, 80	mpd 13	. . . . . . . . . . . 12
82	78	a1i 9	. . . . . . . . . . . . 13
83	82, 38, 12, 77, 75	lttrd 8442	. . . . . . . . . . . . 13
84	82, 12, 83	ltled 8435	. . . . . . . . . . . 12
85	38, 12, 81, 84	lt2sqd 11120	. . . . . . . . . . 11
86	75, 85	mpbid 147	. . . . . . . . . 10
87		ltmul2 9176	. . . . . . . . . . 11 $/\$ $/\$ $/\$
88	39, 21, 43, 47, 87	syl112anc 1282	. . . . . . . . . 10
89	86, 88	mpbid 147	. . . . . . . . 9
90	41, 23, 42, 89	ltsub1dd 8875	. . . . . . . 8
91	37, 90	eqbrtrd 4147	. . . . . . 7
92		3re 9357	. . . . . . . . . 10
93		remulcl 8297	. . . . . . . . . 10 $/\$
94	92, 10, 93	sylancr 418	. . . . . . . . 9
95		4re 9360	. . . . . . . . . 10
96		remulcl 8297	. . . . . . . . . 10 $/\$
97	95, 10, 96	sylancr 418	. . . . . . . . 9
98	10	resqcld 11115	. . . . . . . . . . 11
99		remulcl 8297	. . . . . . . . . . 11 $/\$
100	14, 98, 99	sylancr 418	. . . . . . . . . 10
101		readdcl 8295	. . . . . . . . . 10 $/\$
102	4, 100, 101	sylancr 418	. . . . . . . . 9
103		3lt4 9456	. . . . . . . . . 10
104	92	a1i 9	. . . . . . . . . . 11
105	95	a1i 9	. . . . . . . . . . 11
106	6, 48	gt0ap0d 8947	. . . . . . . . . . . . 13 #
107	6, 106	sqgt0apd 11117	. . . . . . . . . . . 12
108		3pos 9377	. . . . . . . . . . . . 13
109	108	a1i 9	. . . . . . . . . . . 12
110	7, 104, 107, 109	divgt0d 9255	. . . . . . . . . . 11
111		ltmul1 8910	. . . . . . . . . . 11 $/\$ $/\$ $/\$
112	104, 105, 10, 110, 111	syl112anc 1282	. . . . . . . . . 10
113	103, 112	mpbii 148	. . . . . . . . 9
114	94, 97, 102, 113	ltsub2dd 8876	. . . . . . . 8
115	42	recnd 8344	. . . . . . . . 9
116		ax-1cn 8262	. . . . . . . . . . 11
117	100	recnd 8344	. . . . . . . . . . 11
118		addcl 8294	. . . . . . . . . . 11 $/\$
119	116, 117, 118	sylancr 418	. . . . . . . . . 10
120	97	recnd 8344	. . . . . . . . . 10
121	119, 120	subcld 8627	. . . . . . . . 9
122		sq1 11048	. . . . . . . . . . . . . . 15
123	122	a1i 9	. . . . . . . . . . . . . 14
124	10	recnd 8344	. . . . . . . . . . . . . . . 16
125	124	mullidd 8334	. . . . . . . . . . . . . . 15
126	125	oveq2d 6091	. . . . . . . . . . . . . 14
127	123, 126	oveq12d 6093	. . . . . . . . . . . . 13
128	127	oveq1d 6090	. . . . . . . . . . . 12
129		binom2sub 11068	. . . . . . . . . . . . 13 $/\$
130	116, 124, 129	sylancr 418	. . . . . . . . . . . 12
131	98	recnd 8344	. . . . . . . . . . . . 13
132	16	recnd 8344	. . . . . . . . . . . . 13
133	115, 131, 132	addsubd 8648	. . . . . . . . . . . 12
134	128, 130, 133	3eqtr4d 2281	. . . . . . . . . . 11
135	134	oveq2d 6091	. . . . . . . . . 10
136		addcl 8294	. . . . . . . . . . . 12 $/\$
137	116, 131, 136	sylancr 418	. . . . . . . . . . 11
138	29, 137, 132	subdid 8731	. . . . . . . . . 10
139	29, 115, 131	adddid 8340	. . . . . . . . . . . . 13
140	116	2timesi 9413	. . . . . . . . . . . . . . 15
141	140	oveq1i 6085	. . . . . . . . . . . . . 14
142	115, 115, 117	addassd 8338	. . . . . . . . . . . . . 14
143	141, 142	eqtrid 2283	. . . . . . . . . . . . 13
144	139, 143	eqtrd 2271	. . . . . . . . . . . 12
145	29, 29, 124	mulassd 8339	. . . . . . . . . . . . 13
146	55	oveq1i 6085	. . . . . . . . . . . . 13
147	145, 146	eqtr3di 2286	. . . . . . . . . . . 12
148	144, 147	oveq12d 6093	. . . . . . . . . . 11
149	115, 119, 120, 148	assraddsubd 8684	. . . . . . . . . 10
150	135, 138, 149	3eqtrd 2275	. . . . . . . . 9
151	115, 121, 150	mvrladdd 8683	. . . . . . . 8
152		subcl 8515	. . . . . . . . . . 11 $/\$
153	116, 124, 152	sylancr 418	. . . . . . . . . 10
154	153, 115, 132	subdid 8731	. . . . . . . . 9
155	153	mulridd 8333	. . . . . . . . . 10
156	115, 124, 132	subdird 8732	. . . . . . . . . . 11
157	132	mullidd 8334	. . . . . . . . . . . 12
158	124, 29, 124	mul12d 8468	. . . . . . . . . . . . 13
159	124	sqvald 11086	. . . . . . . . . . . . . 14
160	159	oveq2d 6091	. . . . . . . . . . . . 13
161	158, 160	eqtr4d 2274	. . . . . . . . . . . 12
162	157, 161	oveq12d 6093	. . . . . . . . . . 11
163	156, 162	eqtrd 2271	. . . . . . . . . 10
164	155, 163	oveq12d 6093	. . . . . . . . 9
165	115, 124, 132, 117	subadd4d 8675	. . . . . . . . . 10
166		df-3 9343	. . . . . . . . . . . . . 14
167	28, 116	addcomi 8460	. . . . . . . . . . . . . 14
168	166, 167	eqtri 2259	. . . . . . . . . . . . 13
169	168	oveq1i 6085	. . . . . . . . . . . 12
170	125	oveq1d 6090	. . . . . . . . . . . . 13
171	115, 124, 29, 170	joinlmuladdmuld 8343	. . . . . . . . . . . 12
172	169, 171	eqtrid 2283	. . . . . . . . . . 11
173	172	oveq2d 6091	. . . . . . . . . 10
174	165, 173	eqtr4d 2274	. . . . . . . . 9
175	154, 164, 174	3eqtrd 2275	. . . . . . . 8
176	114, 151, 175	3brtr4d 4157	. . . . . . 7
177	2, 25, 26, 91, 176	lttrd 8442	. . . . . 6
178		ltmul2 9176	. . . . . . 7 $/\$ $/\$ $/\$
179	2, 26, 1, 45, 178	syl112anc 1282	. . . . . 6
180	177, 179	mpbid 147	. . . . 5
181	18	recnd 8344	. . . . . 6
182	27, 153, 181	mulassd 8339	. . . . 5
183	180, 182	breqtrrd 4153	. . . 4
184	13, 38	remulcld 8346	. . . . 5
185	74	simpld 112	. . . . . 6
186	1, 12, 45, 83	mulgt0d 8439	. . . . . . 7
187		ltmul2 9176	. . . . . . 7 $/\$ $/\$ $/\$
188	18, 38, 13, 186, 187	syl112anc 1282	. . . . . 6
189	185, 188	mpbid 147	. . . . 5
190	29, 34, 153	mulassd 8339	. . . . . . . . 9
191	32	oveq1d 6090	. . . . . . . . 9
192	34, 115, 124	subdid 8731	. . . . . . . . . . 11
193	34	mulridd 8333	. . . . . . . . . . . 12
194	166	oveq2i 6086	. . . . . . . . . . . . . . . 16
195		2nn0 9559	. . . . . . . . . . . . . . . . 17
196		expp1 10961	. . . . . . . . . . . . . . . . 17 $/\$
197	34, 195, 196	sylancl 417	. . . . . . . . . . . . . . . 16
198	194, 197	eqtrid 2283	. . . . . . . . . . . . . . 15
199	7	recnd 8344	. . . . . . . . . . . . . . . 16
200	199, 34	mulcomd 8337	. . . . . . . . . . . . . . 15
201	198, 200	eqtrd 2271	. . . . . . . . . . . . . 14
202	201	oveq1d 6090	. . . . . . . . . . . . 13
203		3cn 9358	. . . . . . . . . . . . . . 15
204	203	a1i 9	. . . . . . . . . . . . . 14
205	104, 109	gt0ap0d 8947	. . . . . . . . . . . . . 14 #
206	34, 199, 204, 205	divassapd 9146	. . . . . . . . . . . . 13
207	202, 206	eqtr2d 2272	. . . . . . . . . . . 12
208	193, 207	oveq12d 6093	. . . . . . . . . . 11
209	192, 208	eqtrd 2271	. . . . . . . . . 10
210	209	oveq2d 6091	. . . . . . . . 9
211	190, 191, 210	3eqtr3d 2279	. . . . . . . 8
212		sin01bnd 12502	. . . . . . . . . . 11 $/\$
213	72, 212	syl 14	. . . . . . . . . 10 $/\$
214	213	simpld 112	. . . . . . . . 9
215		3nn0 9560	. . . . . . . . . . . . 13
216		reexpcl 10971	. . . . . . . . . . . . 13 $/\$
217	6, 215, 216	sylancl 417	. . . . . . . . . . . 12
218		nndivre 9319	. . . . . . . . . . . 12 $/\$
219	217, 8, 218	sylancl 417	. . . . . . . . . . 11
220	6, 219	resubcld 8698	. . . . . . . . . 10
221	6	resincld 12468	. . . . . . . . . 10
222		ltmul2 9176	. . . . . . . . . 10 $/\$ $/\$ $/\$
223	220, 221, 43, 47, 222	syl112anc 1282	. . . . . . . . 9
224	214, 223	mpbid 147	. . . . . . . 8
225	211, 224	eqbrtrd 4147	. . . . . . 7
226		remulcl 8297	. . . . . . . . 9 $/\$
227	14, 221, 226	sylancr 418	. . . . . . . 8
228		ltmul1 8910	. . . . . . . 8 $/\$ $/\$ $/\$
229	13, 227, 38, 77, 228	syl112anc 1282	. . . . . . 7
230	225, 229	mpbid 147	. . . . . 6
231	221	recnd 8344	. . . . . . . 8
232	38	recnd 8344	. . . . . . . 8
233	29, 231, 232	mulassd 8339	. . . . . . 7
234		sin2t 12494	. . . . . . . 8
235	34, 234	syl 14	. . . . . . 7
236	32	fveq2d 5694	. . . . . . 7
237	233, 235, 236	3eqtr2rd 2278	. . . . . 6
238	230, 237	breqtrrd 4153	. . . . 5
239	19, 184, 20, 189, 238	lttrd 8442	. . . 4
240	3, 19, 20, 183, 239	lttrd 8442	. . 3
241		sincosq1sgn 15850	. . . . 5 $/\$
242	241	simprd 114	. . . 4
243		ltmuldiv 9194	. . . 4 $/\$ $/\$ $/\$
244	1, 20, 2, 242, 243	syl112anc 1282	. . 3
245	240, 244	mpbid 147	. 2
246	2, 242	gt0ap0d 8947	. . 3 #
247		tanvalap 12453	. . 3 $/\$ #
248	27, 246, 247	syl2anc 415	. 2
249	245, 248	breqtrrd 4153	1

Colors of variables: wff set class

Syntax hints:

wi 4 $/\$ wa 104

wb 105 $/\$ w3a 1009

wceq 1402

wcel 2209 class class class wbr 4125

cfv 5372 (class class class)co 6075

cc 8167

cr 8168

cc0 8169

c1 8170

caddc 8172

cmul 8174

cxr 8349

clt 8350

cle 8351

cmin 8487 # cap 8899

cdiv 8992

cn 9283

c2 9334

c3 9335

c4 9336

cn0 9542

cioo 10269

cioc 10270

cexp 10953

csin 12389

ccos 12390

ctan 12391

cpi 12392

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-ia1 106 ax-ia2 107 ax-ia3 108 ax-in1 623 ax-in2 624 ax-io 721 ax-5 1500 ax-7 1501 ax-gen 1502 ax-ie1 1546 ax-ie2 1547 ax-8 1557 ax-10 1558 ax-11 1559 ax-i12 1560 ax-bndl 1562 ax-4 1563 ax-17 1579 ax-i9 1583 ax-ial 1587 ax-i5r 1588 ax-14 2212 ax-ext 2220 ax-coll 4241 ax-sep 4244 ax-nul 4254 ax-pow 4306 ax-pr 4341 ax-un 4573 ax-setind 4679 ax-iinf 4730 ax-cnex 8260 ax-resscn 8261 ax-1cn 8262 ax-1re 8263 ax-icn 8264 ax-addcl 8265 ax-addrcl 8266 ax-mulcl 8267 ax-mulrcl 8268 ax-addcom 8269 ax-mulcom 8270 ax-addass 8271 ax-mulass 8272 ax-distr 8273 ax-i2m1 8274 ax-0lt1 8275 ax-1rid 8276 ax-0id 8277 ax-rnegex 8278 ax-precex 8279 ax-cnre 8280 ax-pre-ltirr 8281 ax-pre-ltwlin 8282 ax-pre-lttrn 8283 ax-pre-apti 8284 ax-pre-ltadd 8285 ax-pre-mulgt0 8286 ax-pre-mulext 8287 ax-arch 8288 ax-caucvg 8289 ax-pre-suploc 8290 ax-addf 8291 ax-mulf 8292

This theorem depends on definitions: df-bi 117 df-stab 843 df-dc 847 df-3or 1010 df-3an 1011 df-tru 1405 df-fal 1408 df-nf 1514 df-sb 1816 df-eu 2089 df-mo 2090 df-clab 2225 df-cleq 2231 df-clel 2234 df-nfc 2381 df-ne 2421 df-nel 2516 df-ral 2533 df-rex 2534 df-reu 2535 df-rmo 2536 df-rab 2537 df-v 2823 df-sbc 3052 df-csb 3148 df-dif 3222 df-un 3224 df-in 3226 df-ss 3233 df-nul 3521 df-if 3636 df-pw 3687 df-sn 3711 df-pr 3712 df-op 3714 df-uni 3931 df-int 3966 df-iun 4009 df-disj 4102 df-br 4126 df-opab 4188 df-mpt 4189 df-tr 4225 df-id 4433 df-po 4436 df-iso 4437 df-iord 4506 df-on 4508 df-ilim 4509 df-suc 4511 df-iom 4733 df-xp 4775 df-rel 4776 df-cnv 4777 df-co 4778 df-dm 4779 df-rn 4780 df-res 4781 df-ima 4782 df-iota 5332 df-fun 5374 df-fn 5375 df-f 5376 df-f1 5377 df-fo 5378 df-f1o 5379 df-fv 5380 df-isom 5381 df-riota 6028 df-ov 6078 df-oprab 6079 df-mpo 6080 df-of 6292 df-1st 6364 df-2nd 6365 df-recs 6566 df-irdg 6631 df-frec 6652 df-1o 6677 df-oadd 6681 df-er 6797 df-map 6914 df-pm 6915 df-en 7013 df-dom 7014 df-fin 7015 df-sup 7314 df-inf 7315 df-pnf 8352 df-mnf 8353 df-xr 8354 df-ltxr 8355 df-le 8356 df-sub 8489 df-neg 8490 df-reap 8893 df-ap 8900 df-div 8993 df-inn 9284 df-2 9342 df-3 9343 df-4 9344 df-5 9345 df-6 9346 df-7 9347 df-8 9348 df-9 9349 df-n0 9543 df-z 9624 df-uz 9901 df-q 9999 df-rp 10034 df-xneg 10153 df-xadd 10154 df-ioo 10273 df-ioc 10274 df-ico 10275 df-icc 10276 df-fz 10391 df-fzo 10528 df-seqfrec 10863 df-exp 10954 df-fac 11142 df-bc 11164 df-ihash 11193 df-shft 11558 df-cj 11585 df-re 11586 df-im 11587 df-rsqrt 11742 df-abs 11743 df-clim 12023 df-sumdc 12098 df-ef 12393 df-sin 12395 df-cos 12396 df-tan 12397 df-pi 12398 df-rest 13572 df-topgen 13591 df-psmet 14852 df-xmet 14853 df-met 14854 df-bl 14855 df-mopn 14856 df-top 15022 df-topon 15035 df-bases 15067 df-ntr 15120 df-cn 15212 df-cnp 15213 df-tx 15277 df-cncf 15595 df-limced 15680 df-dvap 15681

This theorem is referenced by: (None)

W3C validator