tangtx - Intuitionistic Logic Explorer

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

Theorem tangtx 15506

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 10104	. . . . 5
2	1	recoscld 12230	. . . . 5
3	1, 2	remulcld 8173	. . . 4
4		1re 8141	. . . . . . 7
5		rehalfcl 9334	. . . . . . . . . 10
6	1, 5	syl 14	. . . . . . . . 9
7	6	resqcld 10916	. . . . . . . 8
8		3nn 9269	. . . . . . . 8
9		nndivre 9142	. . . . . . . 8 $/\$
10	7, 8, 9	sylancl 413	. . . . . . 7
11		resubcl 8406	. . . . . . 7 $/\$
12	4, 10, 11	sylancr 414	. . . . . 6
13	1, 12	remulcld 8173	. . . . 5
14		2re 9176	. . . . . . 7
15		remulcl 8123	. . . . . . 7 $/\$
16	14, 10, 15	sylancr 414	. . . . . 6
17		resubcl 8406	. . . . . 6 $/\$
18	4, 16, 17	sylancr 414	. . . . 5
19	13, 18	remulcld 8173	. . . 4
20	1	resincld 12229	. . . 4
21	12	resqcld 10916	. . . . . . . . 9
22		remulcl 8123	. . . . . . . . 9 $/\$
23	14, 21, 22	sylancr 414	. . . . . . . 8
24		resubcl 8406	. . . . . . . 8 $/\$
25	23, 4, 24	sylancl 413	. . . . . . 7
26	12, 18	remulcld 8173	. . . . . . 7
27	1	recnd 8171	. . . . . . . . . . 11
28		2cn 9177	. . . . . . . . . . . 12
29	28	a1i 9	. . . . . . . . . . 11
30		2ap0 9199	. . . . . . . . . . . 12 #
31	30	a1i 9	. . . . . . . . . . 11 #
32	27, 29, 31	divcanap2d 8935	. . . . . . . . . 10
33	32	fveq2d 5630	. . . . . . . . 9
34	6	recnd 8171	. . . . . . . . . 10
35		cos2t 12256	. . . . . . . . . 10
36	34, 35	syl 14	. . . . . . . . 9
37	33, 36	eqtr3d 2264	. . . . . . . 8
38	6	recoscld 12230	. . . . . . . . . . 11
39	38	resqcld 10916	. . . . . . . . . 10
40		remulcl 8123	. . . . . . . . . 10 $/\$
41	14, 39, 40	sylancr 414	. . . . . . . . 9
42	4	a1i 9	. . . . . . . . 9
43	14	a1i 9	. . . . . . . . . . . . . . 15
44		eliooord 10120	. . . . . . . . . . . . . . . 16 $/\$
45	44	simpld 112	. . . . . . . . . . . . . . 15
46		2pos 9197	. . . . . . . . . . . . . . . 16
47	46	a1i 9	. . . . . . . . . . . . . . 15
48	1, 43, 45, 47	divgt0d 9078	. . . . . . . . . . . . . 14
49		pire 15454	. . . . . . . . . . . . . . . . . . 19
50		rehalfcl 9334	. . . . . . . . . . . . . . . . . . 19
51	49, 50	mp1i 10	. . . . . . . . . . . . . . . . . 18
52	44	simprd 114	. . . . . . . . . . . . . . . . . 18
53		pigt2lt4 15452	. . . . . . . . . . . . . . . . . . . . . 22 $/\$
54	53	simpri 113	. . . . . . . . . . . . . . . . . . . . 21
55		2t2e4 9261	. . . . . . . . . . . . . . . . . . . . 21
56	54, 55	breqtrri 4109	. . . . . . . . . . . . . . . . . . . 20
57	14, 46	pm3.2i 272	. . . . . . . . . . . . . . . . . . . . 21 $/\$
58		ltdivmul 9019	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$ $/\$
59	49, 14, 57, 58	mp3an 1371	. . . . . . . . . . . . . . . . . . . 20
60	56, 59	mpbir 146	. . . . . . . . . . . . . . . . . . 19
61	60	a1i 9	. . . . . . . . . . . . . . . . . 18
62	1, 51, 43, 52, 61	lttrd 8268	. . . . . . . . . . . . . . . . 17
63	28	mullidi 8145	. . . . . . . . . . . . . . . . 17
64	62, 63	breqtrrdi 4124	. . . . . . . . . . . . . . . 16
65		ltdivmul2 9021	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$
66	1, 42, 43, 47, 65	syl112anc 1275	. . . . . . . . . . . . . . . 16
67	64, 66	mpbird 167	. . . . . . . . . . . . . . 15
68	6, 42, 67	ltled 8261	. . . . . . . . . . . . . 14
69		0xr 8189	. . . . . . . . . . . . . . 15
70		elioc2 10128	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$
71	69, 4, 70	mp2an 426	. . . . . . . . . . . . . 14 $/\$ $/\$
72	6, 48, 68, 71	syl3anbrc 1205	. . . . . . . . . . . . 13
73		cos01bnd 12264	. . . . . . . . . . . . 13 $/\$
74	72, 73	syl 14	. . . . . . . . . . . 12 $/\$
75	74	simprd 114	. . . . . . . . . . 11
76		cos01gt0 12269	. . . . . . . . . . . . . 14
77	72, 76	syl 14	. . . . . . . . . . . . 13
78		0re 8142	. . . . . . . . . . . . . 14
79		ltle 8230	. . . . . . . . . . . . . 14 $/\$
80	78, 38, 79	sylancr 414	. . . . . . . . . . . . 13
81	77, 80	mpd 13	. . . . . . . . . . . 12
82	78	a1i 9	. . . . . . . . . . . . 13
83	82, 38, 12, 77, 75	lttrd 8268	. . . . . . . . . . . . 13
84	82, 12, 83	ltled 8261	. . . . . . . . . . . 12
85	38, 12, 81, 84	lt2sqd 10921	. . . . . . . . . . 11
86	75, 85	mpbid 147	. . . . . . . . . 10
87		ltmul2 8999	. . . . . . . . . . 11 $/\$ $/\$ $/\$
88	39, 21, 43, 47, 87	syl112anc 1275	. . . . . . . . . 10
89	86, 88	mpbid 147	. . . . . . . . 9
90	41, 23, 42, 89	ltsub1dd 8700	. . . . . . . 8
91	37, 90	eqbrtrd 4104	. . . . . . 7
92		3re 9180	. . . . . . . . . 10
93		remulcl 8123	. . . . . . . . . 10 $/\$
94	92, 10, 93	sylancr 414	. . . . . . . . 9
95		4re 9183	. . . . . . . . . 10
96		remulcl 8123	. . . . . . . . . 10 $/\$
97	95, 10, 96	sylancr 414	. . . . . . . . 9
98	10	resqcld 10916	. . . . . . . . . . 11
99		remulcl 8123	. . . . . . . . . . 11 $/\$
100	14, 98, 99	sylancr 414	. . . . . . . . . 10
101		readdcl 8121	. . . . . . . . . 10 $/\$
102	4, 100, 101	sylancr 414	. . . . . . . . 9
103		3lt4 9279	. . . . . . . . . 10
104	92	a1i 9	. . . . . . . . . . 11
105	95	a1i 9	. . . . . . . . . . 11
106	6, 48	gt0ap0d 8772	. . . . . . . . . . . . 13 #
107	6, 106	sqgt0apd 10918	. . . . . . . . . . . 12
108		3pos 9200	. . . . . . . . . . . . 13
109	108	a1i 9	. . . . . . . . . . . 12
110	7, 104, 107, 109	divgt0d 9078	. . . . . . . . . . 11
111		ltmul1 8735	. . . . . . . . . . 11 $/\$ $/\$ $/\$
112	104, 105, 10, 110, 111	syl112anc 1275	. . . . . . . . . 10
113	103, 112	mpbii 148	. . . . . . . . 9
114	94, 97, 102, 113	ltsub2dd 8701	. . . . . . . 8
115	42	recnd 8171	. . . . . . . . 9
116		ax-1cn 8088	. . . . . . . . . . 11
117	100	recnd 8171	. . . . . . . . . . 11
118		addcl 8120	. . . . . . . . . . 11 $/\$
119	116, 117, 118	sylancr 414	. . . . . . . . . 10
120	97	recnd 8171	. . . . . . . . . 10
121	119, 120	subcld 8453	. . . . . . . . 9
122		sq1 10850	. . . . . . . . . . . . . . 15
123	122	a1i 9	. . . . . . . . . . . . . 14
124	10	recnd 8171	. . . . . . . . . . . . . . . 16
125	124	mulid2d 8161	. . . . . . . . . . . . . . 15
126	125	oveq2d 6016	. . . . . . . . . . . . . 14
127	123, 126	oveq12d 6018	. . . . . . . . . . . . 13
128	127	oveq1d 6015	. . . . . . . . . . . 12
129		binom2sub 10870	. . . . . . . . . . . . 13 $/\$
130	116, 124, 129	sylancr 414	. . . . . . . . . . . 12
131	98	recnd 8171	. . . . . . . . . . . . 13
132	16	recnd 8171	. . . . . . . . . . . . 13
133	115, 131, 132	addsubd 8474	. . . . . . . . . . . 12
134	128, 130, 133	3eqtr4d 2272	. . . . . . . . . . 11
135	134	oveq2d 6016	. . . . . . . . . 10
136		addcl 8120	. . . . . . . . . . . 12 $/\$
137	116, 131, 136	sylancr 414	. . . . . . . . . . 11
138	29, 137, 132	subdid 8556	. . . . . . . . . 10
139	29, 115, 131	adddid 8167	. . . . . . . . . . . . 13
140	116	2timesi 9236	. . . . . . . . . . . . . . 15
141	140	oveq1i 6010	. . . . . . . . . . . . . 14
142	115, 115, 117	addassd 8165	. . . . . . . . . . . . . 14
143	141, 142	eqtrid 2274	. . . . . . . . . . . . 13
144	139, 143	eqtrd 2262	. . . . . . . . . . . 12
145	29, 29, 124	mulassd 8166	. . . . . . . . . . . . 13
146	55	oveq1i 6010	. . . . . . . . . . . . 13
147	145, 146	eqtr3di 2277	. . . . . . . . . . . 12
148	144, 147	oveq12d 6018	. . . . . . . . . . 11
149	115, 119, 120, 148	assraddsubd 8510	. . . . . . . . . 10
150	135, 138, 149	3eqtrd 2266	. . . . . . . . 9
151	115, 121, 150	mvrladdd 8509	. . . . . . . 8
152		subcl 8341	. . . . . . . . . . 11 $/\$
153	116, 124, 152	sylancr 414	. . . . . . . . . 10
154	153, 115, 132	subdid 8556	. . . . . . . . 9
155	153	mulridd 8159	. . . . . . . . . 10
156	115, 124, 132	subdird 8557	. . . . . . . . . . 11
157	132	mulid2d 8161	. . . . . . . . . . . 12
158	124, 29, 124	mul12d 8294	. . . . . . . . . . . . 13
159	124	sqvald 10887	. . . . . . . . . . . . . 14
160	159	oveq2d 6016	. . . . . . . . . . . . 13
161	158, 160	eqtr4d 2265	. . . . . . . . . . . 12
162	157, 161	oveq12d 6018	. . . . . . . . . . 11
163	156, 162	eqtrd 2262	. . . . . . . . . 10
164	155, 163	oveq12d 6018	. . . . . . . . 9
165	115, 124, 132, 117	subadd4d 8501	. . . . . . . . . 10
166		df-3 9166	. . . . . . . . . . . . . 14
167	28, 116	addcomi 8286	. . . . . . . . . . . . . 14
168	166, 167	eqtri 2250	. . . . . . . . . . . . 13
169	168	oveq1i 6010	. . . . . . . . . . . 12
170	125	oveq1d 6015	. . . . . . . . . . . . 13
171	115, 124, 29, 170	joinlmuladdmuld 8170	. . . . . . . . . . . 12
172	169, 171	eqtrid 2274	. . . . . . . . . . 11
173	172	oveq2d 6016	. . . . . . . . . 10
174	165, 173	eqtr4d 2265	. . . . . . . . 9
175	154, 164, 174	3eqtrd 2266	. . . . . . . 8
176	114, 151, 175	3brtr4d 4114	. . . . . . 7
177	2, 25, 26, 91, 176	lttrd 8268	. . . . . 6
178		ltmul2 8999	. . . . . . 7 $/\$ $/\$ $/\$
179	2, 26, 1, 45, 178	syl112anc 1275	. . . . . 6
180	177, 179	mpbid 147	. . . . 5
181	18	recnd 8171	. . . . . 6
182	27, 153, 181	mulassd 8166	. . . . 5
183	180, 182	breqtrrd 4110	. . . 4
184	13, 38	remulcld 8173	. . . . 5
185	74	simpld 112	. . . . . 6
186	1, 12, 45, 83	mulgt0d 8265	. . . . . . 7
187		ltmul2 8999	. . . . . . 7 $/\$ $/\$ $/\$
188	18, 38, 13, 186, 187	syl112anc 1275	. . . . . 6
189	185, 188	mpbid 147	. . . . 5
190	29, 34, 153	mulassd 8166	. . . . . . . . 9
191	32	oveq1d 6015	. . . . . . . . 9
192	34, 115, 124	subdid 8556	. . . . . . . . . . 11
193	34	mulridd 8159	. . . . . . . . . . . 12
194	166	oveq2i 6011	. . . . . . . . . . . . . . . 16
195		2nn0 9382	. . . . . . . . . . . . . . . . 17
196		expp1 10763	. . . . . . . . . . . . . . . . 17 $/\$
197	34, 195, 196	sylancl 413	. . . . . . . . . . . . . . . 16
198	194, 197	eqtrid 2274	. . . . . . . . . . . . . . 15
199	7	recnd 8171	. . . . . . . . . . . . . . . 16
200	199, 34	mulcomd 8164	. . . . . . . . . . . . . . 15
201	198, 200	eqtrd 2262	. . . . . . . . . . . . . 14
202	201	oveq1d 6015	. . . . . . . . . . . . 13
203		3cn 9181	. . . . . . . . . . . . . . 15
204	203	a1i 9	. . . . . . . . . . . . . 14
205	104, 109	gt0ap0d 8772	. . . . . . . . . . . . . 14 #
206	34, 199, 204, 205	divassapd 8969	. . . . . . . . . . . . 13
207	202, 206	eqtr2d 2263	. . . . . . . . . . . 12
208	193, 207	oveq12d 6018	. . . . . . . . . . 11
209	192, 208	eqtrd 2262	. . . . . . . . . 10
210	209	oveq2d 6016	. . . . . . . . 9
211	190, 191, 210	3eqtr3d 2270	. . . . . . . 8
212		sin01bnd 12263	. . . . . . . . . . 11 $/\$
213	72, 212	syl 14	. . . . . . . . . 10 $/\$
214	213	simpld 112	. . . . . . . . 9
215		3nn0 9383	. . . . . . . . . . . . 13
216		reexpcl 10773	. . . . . . . . . . . . 13 $/\$
217	6, 215, 216	sylancl 413	. . . . . . . . . . . 12
218		nndivre 9142	. . . . . . . . . . . 12 $/\$
219	217, 8, 218	sylancl 413	. . . . . . . . . . 11
220	6, 219	resubcld 8523	. . . . . . . . . 10
221	6	resincld 12229	. . . . . . . . . 10
222		ltmul2 8999	. . . . . . . . . 10 $/\$ $/\$ $/\$
223	220, 221, 43, 47, 222	syl112anc 1275	. . . . . . . . 9
224	214, 223	mpbid 147	. . . . . . . 8
225	211, 224	eqbrtrd 4104	. . . . . . 7
226		remulcl 8123	. . . . . . . . 9 $/\$
227	14, 221, 226	sylancr 414	. . . . . . . 8
228		ltmul1 8735	. . . . . . . 8 $/\$ $/\$ $/\$
229	13, 227, 38, 77, 228	syl112anc 1275	. . . . . . 7
230	225, 229	mpbid 147	. . . . . 6
231	221	recnd 8171	. . . . . . . 8
232	38	recnd 8171	. . . . . . . 8
233	29, 231, 232	mulassd 8166	. . . . . . 7
234		sin2t 12255	. . . . . . . 8
235	34, 234	syl 14	. . . . . . 7
236	32	fveq2d 5630	. . . . . . 7
237	233, 235, 236	3eqtr2rd 2269	. . . . . 6
238	230, 237	breqtrrd 4110	. . . . 5
239	19, 184, 20, 189, 238	lttrd 8268	. . . 4
240	3, 19, 20, 183, 239	lttrd 8268	. . 3
241		sincosq1sgn 15494	. . . . 5 $/\$
242	241	simprd 114	. . . 4
243		ltmuldiv 9017	. . . 4 $/\$ $/\$ $/\$
244	1, 20, 2, 242, 243	syl112anc 1275	. . 3
245	240, 244	mpbid 147	. 2
246	2, 242	gt0ap0d 8772	. . 3 #
247		tanvalap 12214	. . 3 $/\$ #
248	27, 246, 247	syl2anc 411	. 2
249	245, 248	breqtrrd 4110	1

Colors of variables: wff set class

Syntax hints:

wi 4 $/\$ wa 104

wb 105 $/\$ w3a 1002

wceq 1395

wcel 2200 class class class wbr 4082

cfv 5317 (class class class)co 6000

cc 7993

cr 7994

cc0 7995

c1 7996

caddc 7998

cmul 8000

cxr 8176

clt 8177

cle 8178

cmin 8313 # cap 8724

cdiv 8815

cn 9106

c2 9157

c3 9158

c4 9159

cn0 9365

cioo 10080

cioc 10081

cexp 10755

csin 12150

ccos 12151

ctan 12152

cpi 12153

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 617 ax-in2 618 ax-io 714 ax-5 1493 ax-7 1494 ax-gen 1495 ax-ie1 1539 ax-ie2 1540 ax-8 1550 ax-10 1551 ax-11 1552 ax-i12 1553 ax-bndl 1555 ax-4 1556 ax-17 1572 ax-i9 1576 ax-ial 1580 ax-i5r 1581 ax-13 2202 ax-14 2203 ax-ext 2211 ax-coll 4198 ax-sep 4201 ax-nul 4209 ax-pow 4257 ax-pr 4292 ax-un 4523 ax-setind 4628 ax-iinf 4679 ax-cnex 8086 ax-resscn 8087 ax-1cn 8088 ax-1re 8089 ax-icn 8090 ax-addcl 8091 ax-addrcl 8092 ax-mulcl 8093 ax-mulrcl 8094 ax-addcom 8095 ax-mulcom 8096 ax-addass 8097 ax-mulass 8098 ax-distr 8099 ax-i2m1 8100 ax-0lt1 8101 ax-1rid 8102 ax-0id 8103 ax-rnegex 8104 ax-precex 8105 ax-cnre 8106 ax-pre-ltirr 8107 ax-pre-ltwlin 8108 ax-pre-lttrn 8109 ax-pre-apti 8110 ax-pre-ltadd 8111 ax-pre-mulgt0 8112 ax-pre-mulext 8113 ax-arch 8114 ax-caucvg 8115 ax-pre-suploc 8116 ax-addf 8117 ax-mulf 8118

This theorem depends on definitions: df-bi 117 df-stab 836 df-dc 840 df-3or 1003 df-3an 1004 df-tru 1398 df-fal 1401 df-nf 1507 df-sb 1809 df-eu 2080 df-mo 2081 df-clab 2216 df-cleq 2222 df-clel 2225 df-nfc 2361 df-ne 2401 df-nel 2496 df-ral 2513 df-rex 2514 df-reu 2515 df-rmo 2516 df-rab 2517 df-v 2801 df-sbc 3029 df-csb 3125 df-dif 3199 df-un 3201 df-in 3203 df-ss 3210 df-nul 3492 df-if 3603 df-pw 3651 df-sn 3672 df-pr 3673 df-op 3675 df-uni 3888 df-int 3923 df-iun 3966 df-disj 4059 df-br 4083 df-opab 4145 df-mpt 4146 df-tr 4182 df-id 4383 df-po 4386 df-iso 4387 df-iord 4456 df-on 4458 df-ilim 4459 df-suc 4461 df-iom 4682 df-xp 4724 df-rel 4725 df-cnv 4726 df-co 4727 df-dm 4728 df-rn 4729 df-res 4730 df-ima 4731 df-iota 5277 df-fun 5319 df-fn 5320 df-f 5321 df-f1 5322 df-fo 5323 df-f1o 5324 df-fv 5325 df-isom 5326 df-riota 5953 df-ov 6003 df-oprab 6004 df-mpo 6005 df-of 6216 df-1st 6284 df-2nd 6285 df-recs 6449 df-irdg 6514 df-frec 6535 df-1o 6560 df-oadd 6564 df-er 6678 df-map 6795 df-pm 6796 df-en 6886 df-dom 6887 df-fin 6888 df-sup 7147 df-inf 7148 df-pnf 8179 df-mnf 8180 df-xr 8181 df-ltxr 8182 df-le 8183 df-sub 8315 df-neg 8316 df-reap 8718 df-ap 8725 df-div 8816 df-inn 9107 df-2 9165 df-3 9166 df-4 9167 df-5 9168 df-6 9169 df-7 9170 df-8 9171 df-9 9172 df-n0 9366 df-z 9443 df-uz 9719 df-q 9811 df-rp 9846 df-xneg 9964 df-xadd 9965 df-ioo 10084 df-ioc 10085 df-ico 10086 df-icc 10087 df-fz 10201 df-fzo 10335 df-seqfrec 10665 df-exp 10756 df-fac 10943 df-bc 10965 df-ihash 10993 df-shft 11321 df-cj 11348 df-re 11349 df-im 11350 df-rsqrt 11504 df-abs 11505 df-clim 11785 df-sumdc 11860 df-ef 12154 df-sin 12156 df-cos 12157 df-tan 12158 df-pi 12159 df-rest 13269 df-topgen 13288 df-psmet 14501 df-xmet 14502 df-met 14503 df-bl 14504 df-mopn 14505 df-top 14666 df-topon 14679 df-bases 14711 df-ntr 14764 df-cn 14856 df-cnp 14857 df-tx 14921 df-cncf 15239 df-limced 15324 df-dvap 15325

This theorem is referenced by: (None)

W3C validator