tangtx - Intuitionistic Logic Explorer

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

Theorem tangtx 15649

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 10208	. . . . 5
2	1	recoscld 12365	. . . . 5
3	1, 2	remulcld 8269	. . . 4
4		1re 8238	. . . . . . 7
5		rehalfcl 9430	. . . . . . . . . 10
6	1, 5	syl 14	. . . . . . . . 9
7	6	resqcld 11024	. . . . . . . 8
8		3nn 9365	. . . . . . . 8
9		nndivre 9238	. . . . . . . 8 $/\$
10	7, 8, 9	sylancl 413	. . . . . . 7
11		resubcl 8502	. . . . . . 7 $/\$
12	4, 10, 11	sylancr 414	. . . . . 6
13	1, 12	remulcld 8269	. . . . 5
14		2re 9272	. . . . . . 7
15		remulcl 8220	. . . . . . 7 $/\$
16	14, 10, 15	sylancr 414	. . . . . 6
17		resubcl 8502	. . . . . 6 $/\$
18	4, 16, 17	sylancr 414	. . . . 5
19	13, 18	remulcld 8269	. . . 4
20	1	resincld 12364	. . . 4
21	12	resqcld 11024	. . . . . . . . 9
22		remulcl 8220	. . . . . . . . 9 $/\$
23	14, 21, 22	sylancr 414	. . . . . . . 8
24		resubcl 8502	. . . . . . . 8 $/\$
25	23, 4, 24	sylancl 413	. . . . . . 7
26	12, 18	remulcld 8269	. . . . . . 7
27	1	recnd 8267	. . . . . . . . . . 11
28		2cn 9273	. . . . . . . . . . . 12
29	28	a1i 9	. . . . . . . . . . 11
30		2ap0 9295	. . . . . . . . . . . 12 #
31	30	a1i 9	. . . . . . . . . . 11 #
32	27, 29, 31	divcanap2d 9031	. . . . . . . . . 10
33	32	fveq2d 5652	. . . . . . . . 9
34	6	recnd 8267	. . . . . . . . . 10
35		cos2t 12391	. . . . . . . . . 10
36	34, 35	syl 14	. . . . . . . . 9
37	33, 36	eqtr3d 2266	. . . . . . . 8
38	6	recoscld 12365	. . . . . . . . . . 11
39	38	resqcld 11024	. . . . . . . . . 10
40		remulcl 8220	. . . . . . . . . 10 $/\$
41	14, 39, 40	sylancr 414	. . . . . . . . 9
42	4	a1i 9	. . . . . . . . 9
43	14	a1i 9	. . . . . . . . . . . . . . 15
44		eliooord 10224	. . . . . . . . . . . . . . . 16 $/\$
45	44	simpld 112	. . . . . . . . . . . . . . 15
46		2pos 9293	. . . . . . . . . . . . . . . 16
47	46	a1i 9	. . . . . . . . . . . . . . 15
48	1, 43, 45, 47	divgt0d 9174	. . . . . . . . . . . . . 14
49		pire 15597	. . . . . . . . . . . . . . . . . . 19
50		rehalfcl 9430	. . . . . . . . . . . . . . . . . . 19
51	49, 50	mp1i 10	. . . . . . . . . . . . . . . . . 18
52	44	simprd 114	. . . . . . . . . . . . . . . . . 18
53		pigt2lt4 15595	. . . . . . . . . . . . . . . . . . . . . 22 $/\$
54	53	simpri 113	. . . . . . . . . . . . . . . . . . . . 21
55		2t2e4 9357	. . . . . . . . . . . . . . . . . . . . 21
56	54, 55	breqtrri 4120	. . . . . . . . . . . . . . . . . . . 20
57	14, 46	pm3.2i 272	. . . . . . . . . . . . . . . . . . . . 21 $/\$
58		ltdivmul 9115	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$ $/\$
59	49, 14, 57, 58	mp3an 1374	. . . . . . . . . . . . . . . . . . . 20
60	56, 59	mpbir 146	. . . . . . . . . . . . . . . . . . 19
61	60	a1i 9	. . . . . . . . . . . . . . . . . 18
62	1, 51, 43, 52, 61	lttrd 8364	. . . . . . . . . . . . . . . . 17
63	28	mullidi 8242	. . . . . . . . . . . . . . . . 17
64	62, 63	breqtrrdi 4135	. . . . . . . . . . . . . . . 16
65		ltdivmul2 9117	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$
66	1, 42, 43, 47, 65	syl112anc 1278	. . . . . . . . . . . . . . . 16
67	64, 66	mpbird 167	. . . . . . . . . . . . . . 15
68	6, 42, 67	ltled 8357	. . . . . . . . . . . . . 14
69		0xr 8285	. . . . . . . . . . . . . . 15
70		elioc2 10232	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$
71	69, 4, 70	mp2an 426	. . . . . . . . . . . . . 14 $/\$ $/\$
72	6, 48, 68, 71	syl3anbrc 1208	. . . . . . . . . . . . 13
73		cos01bnd 12399	. . . . . . . . . . . . 13 $/\$
74	72, 73	syl 14	. . . . . . . . . . . 12 $/\$
75	74	simprd 114	. . . . . . . . . . 11
76		cos01gt0 12404	. . . . . . . . . . . . . 14
77	72, 76	syl 14	. . . . . . . . . . . . 13
78		0re 8239	. . . . . . . . . . . . . 14
79		ltle 8326	. . . . . . . . . . . . . 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 8364	. . . . . . . . . . . . 13
84	82, 12, 83	ltled 8357	. . . . . . . . . . . 12
85	38, 12, 81, 84	lt2sqd 11029	. . . . . . . . . . 11
86	75, 85	mpbid 147	. . . . . . . . . 10
87		ltmul2 9095	. . . . . . . . . . 11 $/\$ $/\$ $/\$
88	39, 21, 43, 47, 87	syl112anc 1278	. . . . . . . . . 10
89	86, 88	mpbid 147	. . . . . . . . 9
90	41, 23, 42, 89	ltsub1dd 8796	. . . . . . . 8
91	37, 90	eqbrtrd 4115	. . . . . . 7
92		3re 9276	. . . . . . . . . 10
93		remulcl 8220	. . . . . . . . . 10 $/\$
94	92, 10, 93	sylancr 414	. . . . . . . . 9
95		4re 9279	. . . . . . . . . 10
96		remulcl 8220	. . . . . . . . . 10 $/\$
97	95, 10, 96	sylancr 414	. . . . . . . . 9
98	10	resqcld 11024	. . . . . . . . . . 11
99		remulcl 8220	. . . . . . . . . . 11 $/\$
100	14, 98, 99	sylancr 414	. . . . . . . . . 10
101		readdcl 8218	. . . . . . . . . 10 $/\$
102	4, 100, 101	sylancr 414	. . . . . . . . 9
103		3lt4 9375	. . . . . . . . . 10
104	92	a1i 9	. . . . . . . . . . 11
105	95	a1i 9	. . . . . . . . . . 11
106	6, 48	gt0ap0d 8868	. . . . . . . . . . . . 13 #
107	6, 106	sqgt0apd 11026	. . . . . . . . . . . 12
108		3pos 9296	. . . . . . . . . . . . 13
109	108	a1i 9	. . . . . . . . . . . 12
110	7, 104, 107, 109	divgt0d 9174	. . . . . . . . . . 11
111		ltmul1 8831	. . . . . . . . . . 11 $/\$ $/\$ $/\$
112	104, 105, 10, 110, 111	syl112anc 1278	. . . . . . . . . 10
113	103, 112	mpbii 148	. . . . . . . . 9
114	94, 97, 102, 113	ltsub2dd 8797	. . . . . . . 8
115	42	recnd 8267	. . . . . . . . 9
116		ax-1cn 8185	. . . . . . . . . . 11
117	100	recnd 8267	. . . . . . . . . . 11
118		addcl 8217	. . . . . . . . . . 11 $/\$
119	116, 117, 118	sylancr 414	. . . . . . . . . 10
120	97	recnd 8267	. . . . . . . . . 10
121	119, 120	subcld 8549	. . . . . . . . 9
122		sq1 10958	. . . . . . . . . . . . . . 15
123	122	a1i 9	. . . . . . . . . . . . . 14
124	10	recnd 8267	. . . . . . . . . . . . . . . 16
125	124	mullidd 8257	. . . . . . . . . . . . . . 15
126	125	oveq2d 6044	. . . . . . . . . . . . . 14
127	123, 126	oveq12d 6046	. . . . . . . . . . . . 13
128	127	oveq1d 6043	. . . . . . . . . . . 12
129		binom2sub 10978	. . . . . . . . . . . . 13 $/\$
130	116, 124, 129	sylancr 414	. . . . . . . . . . . 12
131	98	recnd 8267	. . . . . . . . . . . . 13
132	16	recnd 8267	. . . . . . . . . . . . 13
133	115, 131, 132	addsubd 8570	. . . . . . . . . . . 12
134	128, 130, 133	3eqtr4d 2274	. . . . . . . . . . 11
135	134	oveq2d 6044	. . . . . . . . . 10
136		addcl 8217	. . . . . . . . . . . 12 $/\$
137	116, 131, 136	sylancr 414	. . . . . . . . . . 11
138	29, 137, 132	subdid 8652	. . . . . . . . . 10
139	29, 115, 131	adddid 8263	. . . . . . . . . . . . 13
140	116	2timesi 9332	. . . . . . . . . . . . . . 15
141	140	oveq1i 6038	. . . . . . . . . . . . . 14
142	115, 115, 117	addassd 8261	. . . . . . . . . . . . . 14
143	141, 142	eqtrid 2276	. . . . . . . . . . . . 13
144	139, 143	eqtrd 2264	. . . . . . . . . . . 12
145	29, 29, 124	mulassd 8262	. . . . . . . . . . . . 13
146	55	oveq1i 6038	. . . . . . . . . . . . 13
147	145, 146	eqtr3di 2279	. . . . . . . . . . . 12
148	144, 147	oveq12d 6046	. . . . . . . . . . 11
149	115, 119, 120, 148	assraddsubd 8606	. . . . . . . . . 10
150	135, 138, 149	3eqtrd 2268	. . . . . . . . 9
151	115, 121, 150	mvrladdd 8605	. . . . . . . 8
152		subcl 8437	. . . . . . . . . . 11 $/\$
153	116, 124, 152	sylancr 414	. . . . . . . . . 10
154	153, 115, 132	subdid 8652	. . . . . . . . 9
155	153	mulridd 8256	. . . . . . . . . 10
156	115, 124, 132	subdird 8653	. . . . . . . . . . 11
157	132	mullidd 8257	. . . . . . . . . . . 12
158	124, 29, 124	mul12d 8390	. . . . . . . . . . . . 13
159	124	sqvald 10995	. . . . . . . . . . . . . 14
160	159	oveq2d 6044	. . . . . . . . . . . . 13
161	158, 160	eqtr4d 2267	. . . . . . . . . . . 12
162	157, 161	oveq12d 6046	. . . . . . . . . . 11
163	156, 162	eqtrd 2264	. . . . . . . . . 10
164	155, 163	oveq12d 6046	. . . . . . . . 9
165	115, 124, 132, 117	subadd4d 8597	. . . . . . . . . 10
166		df-3 9262	. . . . . . . . . . . . . 14
167	28, 116	addcomi 8382	. . . . . . . . . . . . . 14
168	166, 167	eqtri 2252	. . . . . . . . . . . . 13
169	168	oveq1i 6038	. . . . . . . . . . . 12
170	125	oveq1d 6043	. . . . . . . . . . . . 13
171	115, 124, 29, 170	joinlmuladdmuld 8266	. . . . . . . . . . . 12
172	169, 171	eqtrid 2276	. . . . . . . . . . 11
173	172	oveq2d 6044	. . . . . . . . . 10
174	165, 173	eqtr4d 2267	. . . . . . . . 9
175	154, 164, 174	3eqtrd 2268	. . . . . . . 8
176	114, 151, 175	3brtr4d 4125	. . . . . . 7
177	2, 25, 26, 91, 176	lttrd 8364	. . . . . 6
178		ltmul2 9095	. . . . . . 7 $/\$ $/\$ $/\$
179	2, 26, 1, 45, 178	syl112anc 1278	. . . . . 6
180	177, 179	mpbid 147	. . . . 5
181	18	recnd 8267	. . . . . 6
182	27, 153, 181	mulassd 8262	. . . . 5
183	180, 182	breqtrrd 4121	. . . 4
184	13, 38	remulcld 8269	. . . . 5
185	74	simpld 112	. . . . . 6
186	1, 12, 45, 83	mulgt0d 8361	. . . . . . 7
187		ltmul2 9095	. . . . . . 7 $/\$ $/\$ $/\$
188	18, 38, 13, 186, 187	syl112anc 1278	. . . . . 6
189	185, 188	mpbid 147	. . . . 5
190	29, 34, 153	mulassd 8262	. . . . . . . . 9
191	32	oveq1d 6043	. . . . . . . . 9
192	34, 115, 124	subdid 8652	. . . . . . . . . . 11
193	34	mulridd 8256	. . . . . . . . . . . 12
194	166	oveq2i 6039	. . . . . . . . . . . . . . . 16
195		2nn0 9478	. . . . . . . . . . . . . . . . 17
196		expp1 10871	. . . . . . . . . . . . . . . . 17 $/\$
197	34, 195, 196	sylancl 413	. . . . . . . . . . . . . . . 16
198	194, 197	eqtrid 2276	. . . . . . . . . . . . . . 15
199	7	recnd 8267	. . . . . . . . . . . . . . . 16
200	199, 34	mulcomd 8260	. . . . . . . . . . . . . . 15
201	198, 200	eqtrd 2264	. . . . . . . . . . . . . 14
202	201	oveq1d 6043	. . . . . . . . . . . . 13
203		3cn 9277	. . . . . . . . . . . . . . 15
204	203	a1i 9	. . . . . . . . . . . . . 14
205	104, 109	gt0ap0d 8868	. . . . . . . . . . . . . 14 #
206	34, 199, 204, 205	divassapd 9065	. . . . . . . . . . . . 13
207	202, 206	eqtr2d 2265	. . . . . . . . . . . 12
208	193, 207	oveq12d 6046	. . . . . . . . . . 11
209	192, 208	eqtrd 2264	. . . . . . . . . 10
210	209	oveq2d 6044	. . . . . . . . 9
211	190, 191, 210	3eqtr3d 2272	. . . . . . . 8
212		sin01bnd 12398	. . . . . . . . . . 11 $/\$
213	72, 212	syl 14	. . . . . . . . . 10 $/\$
214	213	simpld 112	. . . . . . . . 9
215		3nn0 9479	. . . . . . . . . . . . 13
216		reexpcl 10881	. . . . . . . . . . . . 13 $/\$
217	6, 215, 216	sylancl 413	. . . . . . . . . . . 12
218		nndivre 9238	. . . . . . . . . . . 12 $/\$
219	217, 8, 218	sylancl 413	. . . . . . . . . . 11
220	6, 219	resubcld 8619	. . . . . . . . . 10
221	6	resincld 12364	. . . . . . . . . 10
222		ltmul2 9095	. . . . . . . . . 10 $/\$ $/\$ $/\$
223	220, 221, 43, 47, 222	syl112anc 1278	. . . . . . . . 9
224	214, 223	mpbid 147	. . . . . . . 8
225	211, 224	eqbrtrd 4115	. . . . . . 7
226		remulcl 8220	. . . . . . . . 9 $/\$
227	14, 221, 226	sylancr 414	. . . . . . . 8
228		ltmul1 8831	. . . . . . . 8 $/\$ $/\$ $/\$
229	13, 227, 38, 77, 228	syl112anc 1278	. . . . . . 7
230	225, 229	mpbid 147	. . . . . 6
231	221	recnd 8267	. . . . . . . 8
232	38	recnd 8267	. . . . . . . 8
233	29, 231, 232	mulassd 8262	. . . . . . 7
234		sin2t 12390	. . . . . . . 8
235	34, 234	syl 14	. . . . . . 7
236	32	fveq2d 5652	. . . . . . 7
237	233, 235, 236	3eqtr2rd 2271	. . . . . 6
238	230, 237	breqtrrd 4121	. . . . 5
239	19, 184, 20, 189, 238	lttrd 8364	. . . 4
240	3, 19, 20, 183, 239	lttrd 8364	. . 3
241		sincosq1sgn 15637	. . . . 5 $/\$
242	241	simprd 114	. . . 4
243		ltmuldiv 9113	. . . 4 $/\$ $/\$ $/\$
244	1, 20, 2, 242, 243	syl112anc 1278	. . 3
245	240, 244	mpbid 147	. 2
246	2, 242	gt0ap0d 8868	. . 3 #
247		tanvalap 12349	. . 3 $/\$ #
248	27, 246, 247	syl2anc 411	. 2
249	245, 248	breqtrrd 4121	1

Colors of variables: wff set class

Syntax hints:

wi 4 $/\$ wa 104

wb 105 $/\$ w3a 1005

wceq 1398

wcel 2202 class class class wbr 4093

cfv 5333 (class class class)co 6028

cc 8090

cr 8091

cc0 8092

c1 8093

caddc 8095

cmul 8097

cxr 8272

clt 8273

cle 8274

cmin 8409 # cap 8820

cdiv 8911

cn 9202

c2 9253

c3 9254

c4 9255

cn0 9461

cioo 10184

cioc 10185

cexp 10863

csin 12285

ccos 12286

ctan 12287

cpi 12288

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 619 ax-in2 620 ax-io 717 ax-5 1496 ax-7 1497 ax-gen 1498 ax-ie1 1542 ax-ie2 1543 ax-8 1553 ax-10 1554 ax-11 1555 ax-i12 1556 ax-bndl 1558 ax-4 1559 ax-17 1575 ax-i9 1579 ax-ial 1583 ax-i5r 1584 ax-13 2204 ax-14 2205 ax-ext 2213 ax-coll 4209 ax-sep 4212 ax-nul 4220 ax-pow 4270 ax-pr 4305 ax-un 4536 ax-setind 4641 ax-iinf 4692 ax-cnex 8183 ax-resscn 8184 ax-1cn 8185 ax-1re 8186 ax-icn 8187 ax-addcl 8188 ax-addrcl 8189 ax-mulcl 8190 ax-mulrcl 8191 ax-addcom 8192 ax-mulcom 8193 ax-addass 8194 ax-mulass 8195 ax-distr 8196 ax-i2m1 8197 ax-0lt1 8198 ax-1rid 8199 ax-0id 8200 ax-rnegex 8201 ax-precex 8202 ax-cnre 8203 ax-pre-ltirr 8204 ax-pre-ltwlin 8205 ax-pre-lttrn 8206 ax-pre-apti 8207 ax-pre-ltadd 8208 ax-pre-mulgt0 8209 ax-pre-mulext 8210 ax-arch 8211 ax-caucvg 8212 ax-pre-suploc 8213 ax-addf 8214 ax-mulf 8215

This theorem depends on definitions: df-bi 117 df-stab 839 df-dc 843 df-3or 1006 df-3an 1007 df-tru 1401 df-fal 1404 df-nf 1510 df-sb 1811 df-eu 2082 df-mo 2083 df-clab 2218 df-cleq 2224 df-clel 2227 df-nfc 2364 df-ne 2404 df-nel 2499 df-ral 2516 df-rex 2517 df-reu 2518 df-rmo 2519 df-rab 2520 df-v 2805 df-sbc 3033 df-csb 3129 df-dif 3203 df-un 3205 df-in 3207 df-ss 3214 df-nul 3497 df-if 3608 df-pw 3658 df-sn 3679 df-pr 3680 df-op 3682 df-uni 3899 df-int 3934 df-iun 3977 df-disj 4070 df-br 4094 df-opab 4156 df-mpt 4157 df-tr 4193 df-id 4396 df-po 4399 df-iso 4400 df-iord 4469 df-on 4471 df-ilim 4472 df-suc 4474 df-iom 4695 df-xp 4737 df-rel 4738 df-cnv 4739 df-co 4740 df-dm 4741 df-rn 4742 df-res 4743 df-ima 4744 df-iota 5293 df-fun 5335 df-fn 5336 df-f 5337 df-f1 5338 df-fo 5339 df-f1o 5340 df-fv 5341 df-isom 5342 df-riota 5981 df-ov 6031 df-oprab 6032 df-mpo 6033 df-of 6244 df-1st 6312 df-2nd 6313 df-recs 6514 df-irdg 6579 df-frec 6600 df-1o 6625 df-oadd 6629 df-er 6745 df-map 6862 df-pm 6863 df-en 6953 df-dom 6954 df-fin 6955 df-sup 7243 df-inf 7244 df-pnf 8275 df-mnf 8276 df-xr 8277 df-ltxr 8278 df-le 8279 df-sub 8411 df-neg 8412 df-reap 8814 df-ap 8821 df-div 8912 df-inn 9203 df-2 9261 df-3 9262 df-4 9263 df-5 9264 df-6 9265 df-7 9266 df-8 9267 df-9 9268 df-n0 9462 df-z 9541 df-uz 9817 df-q 9915 df-rp 9950 df-xneg 10068 df-xadd 10069 df-ioo 10188 df-ioc 10189 df-ico 10190 df-icc 10191 df-fz 10306 df-fzo 10440 df-seqfrec 10773 df-exp 10864 df-fac 11051 df-bc 11073 df-ihash 11101 df-shft 11455 df-cj 11482 df-re 11483 df-im 11484 df-rsqrt 11638 df-abs 11639 df-clim 11919 df-sumdc 11994 df-ef 12289 df-sin 12291 df-cos 12292 df-tan 12293 df-pi 12294 df-rest 13404 df-topgen 13423 df-psmet 14639 df-xmet 14640 df-met 14641 df-bl 14642 df-mopn 14643 df-top 14809 df-topon 14822 df-bases 14854 df-ntr 14907 df-cn 14999 df-cnp 15000 df-tx 15064 df-cncf 15382 df-limced 15467 df-dvap 15468

This theorem is referenced by: (None)

W3C validator