tangtx - Intuitionistic Logic Explorer

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

Theorem tangtx 15588

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 10149	. . . . 5
2	1	recoscld 12305	. . . . 5
3	1, 2	remulcld 8212	. . . 4
4		1re 8180	. . . . . . 7
5		rehalfcl 9373	. . . . . . . . . 10
6	1, 5	syl 14	. . . . . . . . 9
7	6	resqcld 10964	. . . . . . . 8
8		3nn 9308	. . . . . . . 8
9		nndivre 9181	. . . . . . . 8 $/\$
10	7, 8, 9	sylancl 413	. . . . . . 7
11		resubcl 8445	. . . . . . 7 $/\$
12	4, 10, 11	sylancr 414	. . . . . 6
13	1, 12	remulcld 8212	. . . . 5
14		2re 9215	. . . . . . 7
15		remulcl 8162	. . . . . . 7 $/\$
16	14, 10, 15	sylancr 414	. . . . . 6
17		resubcl 8445	. . . . . 6 $/\$
18	4, 16, 17	sylancr 414	. . . . 5
19	13, 18	remulcld 8212	. . . 4
20	1	resincld 12304	. . . 4
21	12	resqcld 10964	. . . . . . . . 9
22		remulcl 8162	. . . . . . . . 9 $/\$
23	14, 21, 22	sylancr 414	. . . . . . . 8
24		resubcl 8445	. . . . . . . 8 $/\$
25	23, 4, 24	sylancl 413	. . . . . . 7
26	12, 18	remulcld 8212	. . . . . . 7
27	1	recnd 8210	. . . . . . . . . . 11
28		2cn 9216	. . . . . . . . . . . 12
29	28	a1i 9	. . . . . . . . . . 11
30		2ap0 9238	. . . . . . . . . . . 12 #
31	30	a1i 9	. . . . . . . . . . 11 #
32	27, 29, 31	divcanap2d 8974	. . . . . . . . . 10
33	32	fveq2d 5643	. . . . . . . . 9
34	6	recnd 8210	. . . . . . . . . 10
35		cos2t 12331	. . . . . . . . . 10
36	34, 35	syl 14	. . . . . . . . 9
37	33, 36	eqtr3d 2265	. . . . . . . 8
38	6	recoscld 12305	. . . . . . . . . . 11
39	38	resqcld 10964	. . . . . . . . . 10
40		remulcl 8162	. . . . . . . . . 10 $/\$
41	14, 39, 40	sylancr 414	. . . . . . . . 9
42	4	a1i 9	. . . . . . . . 9
43	14	a1i 9	. . . . . . . . . . . . . . 15
44		eliooord 10165	. . . . . . . . . . . . . . . 16 $/\$
45	44	simpld 112	. . . . . . . . . . . . . . 15
46		2pos 9236	. . . . . . . . . . . . . . . 16
47	46	a1i 9	. . . . . . . . . . . . . . 15
48	1, 43, 45, 47	divgt0d 9117	. . . . . . . . . . . . . 14
49		pire 15536	. . . . . . . . . . . . . . . . . . 19
50		rehalfcl 9373	. . . . . . . . . . . . . . . . . . 19
51	49, 50	mp1i 10	. . . . . . . . . . . . . . . . . 18
52	44	simprd 114	. . . . . . . . . . . . . . . . . 18
53		pigt2lt4 15534	. . . . . . . . . . . . . . . . . . . . . 22 $/\$
54	53	simpri 113	. . . . . . . . . . . . . . . . . . . . 21
55		2t2e4 9300	. . . . . . . . . . . . . . . . . . . . 21
56	54, 55	breqtrri 4114	. . . . . . . . . . . . . . . . . . . 20
57	14, 46	pm3.2i 272	. . . . . . . . . . . . . . . . . . . . 21 $/\$
58		ltdivmul 9058	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$ $/\$
59	49, 14, 57, 58	mp3an 1373	. . . . . . . . . . . . . . . . . . . 20
60	56, 59	mpbir 146	. . . . . . . . . . . . . . . . . . 19
61	60	a1i 9	. . . . . . . . . . . . . . . . . 18
62	1, 51, 43, 52, 61	lttrd 8307	. . . . . . . . . . . . . . . . 17
63	28	mullidi 8184	. . . . . . . . . . . . . . . . 17
64	62, 63	breqtrrdi 4129	. . . . . . . . . . . . . . . 16
65		ltdivmul2 9060	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$
66	1, 42, 43, 47, 65	syl112anc 1277	. . . . . . . . . . . . . . . 16
67	64, 66	mpbird 167	. . . . . . . . . . . . . . 15
68	6, 42, 67	ltled 8300	. . . . . . . . . . . . . 14
69		0xr 8228	. . . . . . . . . . . . . . 15
70		elioc2 10173	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$
71	69, 4, 70	mp2an 426	. . . . . . . . . . . . . 14 $/\$ $/\$
72	6, 48, 68, 71	syl3anbrc 1207	. . . . . . . . . . . . 13
73		cos01bnd 12339	. . . . . . . . . . . . 13 $/\$
74	72, 73	syl 14	. . . . . . . . . . . 12 $/\$
75	74	simprd 114	. . . . . . . . . . 11
76		cos01gt0 12344	. . . . . . . . . . . . . 14
77	72, 76	syl 14	. . . . . . . . . . . . 13
78		0re 8181	. . . . . . . . . . . . . 14
79		ltle 8269	. . . . . . . . . . . . . 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 8307	. . . . . . . . . . . . 13
84	82, 12, 83	ltled 8300	. . . . . . . . . . . 12
85	38, 12, 81, 84	lt2sqd 10969	. . . . . . . . . . 11
86	75, 85	mpbid 147	. . . . . . . . . 10
87		ltmul2 9038	. . . . . . . . . . 11 $/\$ $/\$ $/\$
88	39, 21, 43, 47, 87	syl112anc 1277	. . . . . . . . . 10
89	86, 88	mpbid 147	. . . . . . . . 9
90	41, 23, 42, 89	ltsub1dd 8739	. . . . . . . 8
91	37, 90	eqbrtrd 4109	. . . . . . 7
92		3re 9219	. . . . . . . . . 10
93		remulcl 8162	. . . . . . . . . 10 $/\$
94	92, 10, 93	sylancr 414	. . . . . . . . 9
95		4re 9222	. . . . . . . . . 10
96		remulcl 8162	. . . . . . . . . 10 $/\$
97	95, 10, 96	sylancr 414	. . . . . . . . 9
98	10	resqcld 10964	. . . . . . . . . . 11
99		remulcl 8162	. . . . . . . . . . 11 $/\$
100	14, 98, 99	sylancr 414	. . . . . . . . . 10
101		readdcl 8160	. . . . . . . . . 10 $/\$
102	4, 100, 101	sylancr 414	. . . . . . . . 9
103		3lt4 9318	. . . . . . . . . 10
104	92	a1i 9	. . . . . . . . . . 11
105	95	a1i 9	. . . . . . . . . . 11
106	6, 48	gt0ap0d 8811	. . . . . . . . . . . . 13 #
107	6, 106	sqgt0apd 10966	. . . . . . . . . . . 12
108		3pos 9239	. . . . . . . . . . . . 13
109	108	a1i 9	. . . . . . . . . . . 12
110	7, 104, 107, 109	divgt0d 9117	. . . . . . . . . . 11
111		ltmul1 8774	. . . . . . . . . . 11 $/\$ $/\$ $/\$
112	104, 105, 10, 110, 111	syl112anc 1277	. . . . . . . . . 10
113	103, 112	mpbii 148	. . . . . . . . 9
114	94, 97, 102, 113	ltsub2dd 8740	. . . . . . . 8
115	42	recnd 8210	. . . . . . . . 9
116		ax-1cn 8127	. . . . . . . . . . 11
117	100	recnd 8210	. . . . . . . . . . 11
118		addcl 8159	. . . . . . . . . . 11 $/\$
119	116, 117, 118	sylancr 414	. . . . . . . . . 10
120	97	recnd 8210	. . . . . . . . . 10
121	119, 120	subcld 8492	. . . . . . . . 9
122		sq1 10898	. . . . . . . . . . . . . . 15
123	122	a1i 9	. . . . . . . . . . . . . 14
124	10	recnd 8210	. . . . . . . . . . . . . . . 16
125	124	mulid2d 8200	. . . . . . . . . . . . . . 15
126	125	oveq2d 6036	. . . . . . . . . . . . . 14
127	123, 126	oveq12d 6038	. . . . . . . . . . . . 13
128	127	oveq1d 6035	. . . . . . . . . . . 12
129		binom2sub 10918	. . . . . . . . . . . . 13 $/\$
130	116, 124, 129	sylancr 414	. . . . . . . . . . . 12
131	98	recnd 8210	. . . . . . . . . . . . 13
132	16	recnd 8210	. . . . . . . . . . . . 13
133	115, 131, 132	addsubd 8513	. . . . . . . . . . . 12
134	128, 130, 133	3eqtr4d 2273	. . . . . . . . . . 11
135	134	oveq2d 6036	. . . . . . . . . 10
136		addcl 8159	. . . . . . . . . . . 12 $/\$
137	116, 131, 136	sylancr 414	. . . . . . . . . . 11
138	29, 137, 132	subdid 8595	. . . . . . . . . 10
139	29, 115, 131	adddid 8206	. . . . . . . . . . . . 13
140	116	2timesi 9275	. . . . . . . . . . . . . . 15
141	140	oveq1i 6030	. . . . . . . . . . . . . 14
142	115, 115, 117	addassd 8204	. . . . . . . . . . . . . 14
143	141, 142	eqtrid 2275	. . . . . . . . . . . . 13
144	139, 143	eqtrd 2263	. . . . . . . . . . . 12
145	29, 29, 124	mulassd 8205	. . . . . . . . . . . . 13
146	55	oveq1i 6030	. . . . . . . . . . . . 13
147	145, 146	eqtr3di 2278	. . . . . . . . . . . 12
148	144, 147	oveq12d 6038	. . . . . . . . . . 11
149	115, 119, 120, 148	assraddsubd 8549	. . . . . . . . . 10
150	135, 138, 149	3eqtrd 2267	. . . . . . . . 9
151	115, 121, 150	mvrladdd 8548	. . . . . . . 8
152		subcl 8380	. . . . . . . . . . 11 $/\$
153	116, 124, 152	sylancr 414	. . . . . . . . . 10
154	153, 115, 132	subdid 8595	. . . . . . . . 9
155	153	mulridd 8198	. . . . . . . . . 10
156	115, 124, 132	subdird 8596	. . . . . . . . . . 11
157	132	mulid2d 8200	. . . . . . . . . . . 12
158	124, 29, 124	mul12d 8333	. . . . . . . . . . . . 13
159	124	sqvald 10935	. . . . . . . . . . . . . 14
160	159	oveq2d 6036	. . . . . . . . . . . . 13
161	158, 160	eqtr4d 2266	. . . . . . . . . . . 12
162	157, 161	oveq12d 6038	. . . . . . . . . . 11
163	156, 162	eqtrd 2263	. . . . . . . . . 10
164	155, 163	oveq12d 6038	. . . . . . . . 9
165	115, 124, 132, 117	subadd4d 8540	. . . . . . . . . 10
166		df-3 9205	. . . . . . . . . . . . . 14
167	28, 116	addcomi 8325	. . . . . . . . . . . . . 14
168	166, 167	eqtri 2251	. . . . . . . . . . . . 13
169	168	oveq1i 6030	. . . . . . . . . . . 12
170	125	oveq1d 6035	. . . . . . . . . . . . 13
171	115, 124, 29, 170	joinlmuladdmuld 8209	. . . . . . . . . . . 12
172	169, 171	eqtrid 2275	. . . . . . . . . . 11
173	172	oveq2d 6036	. . . . . . . . . 10
174	165, 173	eqtr4d 2266	. . . . . . . . 9
175	154, 164, 174	3eqtrd 2267	. . . . . . . 8
176	114, 151, 175	3brtr4d 4119	. . . . . . 7
177	2, 25, 26, 91, 176	lttrd 8307	. . . . . 6
178		ltmul2 9038	. . . . . . 7 $/\$ $/\$ $/\$
179	2, 26, 1, 45, 178	syl112anc 1277	. . . . . 6
180	177, 179	mpbid 147	. . . . 5
181	18	recnd 8210	. . . . . 6
182	27, 153, 181	mulassd 8205	. . . . 5
183	180, 182	breqtrrd 4115	. . . 4
184	13, 38	remulcld 8212	. . . . 5
185	74	simpld 112	. . . . . 6
186	1, 12, 45, 83	mulgt0d 8304	. . . . . . 7
187		ltmul2 9038	. . . . . . 7 $/\$ $/\$ $/\$
188	18, 38, 13, 186, 187	syl112anc 1277	. . . . . 6
189	185, 188	mpbid 147	. . . . 5
190	29, 34, 153	mulassd 8205	. . . . . . . . 9
191	32	oveq1d 6035	. . . . . . . . 9
192	34, 115, 124	subdid 8595	. . . . . . . . . . 11
193	34	mulridd 8198	. . . . . . . . . . . 12
194	166	oveq2i 6031	. . . . . . . . . . . . . . . 16
195		2nn0 9421	. . . . . . . . . . . . . . . . 17
196		expp1 10811	. . . . . . . . . . . . . . . . 17 $/\$
197	34, 195, 196	sylancl 413	. . . . . . . . . . . . . . . 16
198	194, 197	eqtrid 2275	. . . . . . . . . . . . . . 15
199	7	recnd 8210	. . . . . . . . . . . . . . . 16
200	199, 34	mulcomd 8203	. . . . . . . . . . . . . . 15
201	198, 200	eqtrd 2263	. . . . . . . . . . . . . 14
202	201	oveq1d 6035	. . . . . . . . . . . . 13
203		3cn 9220	. . . . . . . . . . . . . . 15
204	203	a1i 9	. . . . . . . . . . . . . 14
205	104, 109	gt0ap0d 8811	. . . . . . . . . . . . . 14 #
206	34, 199, 204, 205	divassapd 9008	. . . . . . . . . . . . 13
207	202, 206	eqtr2d 2264	. . . . . . . . . . . 12
208	193, 207	oveq12d 6038	. . . . . . . . . . 11
209	192, 208	eqtrd 2263	. . . . . . . . . 10
210	209	oveq2d 6036	. . . . . . . . 9
211	190, 191, 210	3eqtr3d 2271	. . . . . . . 8
212		sin01bnd 12338	. . . . . . . . . . 11 $/\$
213	72, 212	syl 14	. . . . . . . . . 10 $/\$
214	213	simpld 112	. . . . . . . . 9
215		3nn0 9422	. . . . . . . . . . . . 13
216		reexpcl 10821	. . . . . . . . . . . . 13 $/\$
217	6, 215, 216	sylancl 413	. . . . . . . . . . . 12
218		nndivre 9181	. . . . . . . . . . . 12 $/\$
219	217, 8, 218	sylancl 413	. . . . . . . . . . 11
220	6, 219	resubcld 8562	. . . . . . . . . 10
221	6	resincld 12304	. . . . . . . . . 10
222		ltmul2 9038	. . . . . . . . . 10 $/\$ $/\$ $/\$
223	220, 221, 43, 47, 222	syl112anc 1277	. . . . . . . . 9
224	214, 223	mpbid 147	. . . . . . . 8
225	211, 224	eqbrtrd 4109	. . . . . . 7
226		remulcl 8162	. . . . . . . . 9 $/\$
227	14, 221, 226	sylancr 414	. . . . . . . 8
228		ltmul1 8774	. . . . . . . 8 $/\$ $/\$ $/\$
229	13, 227, 38, 77, 228	syl112anc 1277	. . . . . . 7
230	225, 229	mpbid 147	. . . . . 6
231	221	recnd 8210	. . . . . . . 8
232	38	recnd 8210	. . . . . . . 8
233	29, 231, 232	mulassd 8205	. . . . . . 7
234		sin2t 12330	. . . . . . . 8
235	34, 234	syl 14	. . . . . . 7
236	32	fveq2d 5643	. . . . . . 7
237	233, 235, 236	3eqtr2rd 2270	. . . . . 6
238	230, 237	breqtrrd 4115	. . . . 5
239	19, 184, 20, 189, 238	lttrd 8307	. . . 4
240	3, 19, 20, 183, 239	lttrd 8307	. . 3
241		sincosq1sgn 15576	. . . . 5 $/\$
242	241	simprd 114	. . . 4
243		ltmuldiv 9056	. . . 4 $/\$ $/\$ $/\$
244	1, 20, 2, 242, 243	syl112anc 1277	. . 3
245	240, 244	mpbid 147	. 2
246	2, 242	gt0ap0d 8811	. . 3 #
247		tanvalap 12289	. . 3 $/\$ #
248	27, 246, 247	syl2anc 411	. 2
249	245, 248	breqtrrd 4115	1

Colors of variables: wff set class

Syntax hints:

wi 4 $/\$ wa 104

wb 105 $/\$ w3a 1004

wceq 1397

wcel 2201 class class class wbr 4087

cfv 5325 (class class class)co 6020

cc 8032

cr 8033

cc0 8034

c1 8035

caddc 8037

cmul 8039

cxr 8215

clt 8216

cle 8217

cmin 8352 # cap 8763

cdiv 8854

cn 9145

c2 9196

c3 9197

c4 9198

cn0 9404

cioo 10125

cioc 10126

cexp 10803

csin 12225

ccos 12226

ctan 12227

cpi 12228

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 716 ax-5 1495 ax-7 1496 ax-gen 1497 ax-ie1 1541 ax-ie2 1542 ax-8 1552 ax-10 1553 ax-11 1554 ax-i12 1555 ax-bndl 1557 ax-4 1558 ax-17 1574 ax-i9 1578 ax-ial 1582 ax-i5r 1583 ax-13 2203 ax-14 2204 ax-ext 2212 ax-coll 4203 ax-sep 4206 ax-nul 4214 ax-pow 4263 ax-pr 4298 ax-un 4529 ax-setind 4634 ax-iinf 4685 ax-cnex 8125 ax-resscn 8126 ax-1cn 8127 ax-1re 8128 ax-icn 8129 ax-addcl 8130 ax-addrcl 8131 ax-mulcl 8132 ax-mulrcl 8133 ax-addcom 8134 ax-mulcom 8135 ax-addass 8136 ax-mulass 8137 ax-distr 8138 ax-i2m1 8139 ax-0lt1 8140 ax-1rid 8141 ax-0id 8142 ax-rnegex 8143 ax-precex 8144 ax-cnre 8145 ax-pre-ltirr 8146 ax-pre-ltwlin 8147 ax-pre-lttrn 8148 ax-pre-apti 8149 ax-pre-ltadd 8150 ax-pre-mulgt0 8151 ax-pre-mulext 8152 ax-arch 8153 ax-caucvg 8154 ax-pre-suploc 8155 ax-addf 8156 ax-mulf 8157

This theorem depends on definitions: df-bi 117 df-stab 838 df-dc 842 df-3or 1005 df-3an 1006 df-tru 1400 df-fal 1403 df-nf 1509 df-sb 1810 df-eu 2081 df-mo 2082 df-clab 2217 df-cleq 2223 df-clel 2226 df-nfc 2362 df-ne 2402 df-nel 2497 df-ral 2514 df-rex 2515 df-reu 2516 df-rmo 2517 df-rab 2518 df-v 2803 df-sbc 3031 df-csb 3127 df-dif 3201 df-un 3203 df-in 3205 df-ss 3212 df-nul 3494 df-if 3605 df-pw 3653 df-sn 3674 df-pr 3675 df-op 3677 df-uni 3893 df-int 3928 df-iun 3971 df-disj 4064 df-br 4088 df-opab 4150 df-mpt 4151 df-tr 4187 df-id 4389 df-po 4392 df-iso 4393 df-iord 4462 df-on 4464 df-ilim 4465 df-suc 4467 df-iom 4688 df-xp 4730 df-rel 4731 df-cnv 4732 df-co 4733 df-dm 4734 df-rn 4735 df-res 4736 df-ima 4737 df-iota 5285 df-fun 5327 df-fn 5328 df-f 5329 df-f1 5330 df-fo 5331 df-f1o 5332 df-fv 5333 df-isom 5334 df-riota 5973 df-ov 6023 df-oprab 6024 df-mpo 6025 df-of 6237 df-1st 6305 df-2nd 6306 df-recs 6473 df-irdg 6538 df-frec 6559 df-1o 6584 df-oadd 6588 df-er 6704 df-map 6821 df-pm 6822 df-en 6912 df-dom 6913 df-fin 6914 df-sup 7185 df-inf 7186 df-pnf 8218 df-mnf 8219 df-xr 8220 df-ltxr 8221 df-le 8222 df-sub 8354 df-neg 8355 df-reap 8757 df-ap 8764 df-div 8855 df-inn 9146 df-2 9204 df-3 9205 df-4 9206 df-5 9207 df-6 9208 df-7 9209 df-8 9210 df-9 9211 df-n0 9405 df-z 9482 df-uz 9758 df-q 9856 df-rp 9891 df-xneg 10009 df-xadd 10010 df-ioo 10129 df-ioc 10130 df-ico 10131 df-icc 10132 df-fz 10246 df-fzo 10380 df-seqfrec 10713 df-exp 10804 df-fac 10991 df-bc 11013 df-ihash 11041 df-shft 11395 df-cj 11422 df-re 11423 df-im 11424 df-rsqrt 11578 df-abs 11579 df-clim 11859 df-sumdc 11934 df-ef 12229 df-sin 12231 df-cos 12232 df-tan 12233 df-pi 12234 df-rest 13344 df-topgen 13363 df-psmet 14578 df-xmet 14579 df-met 14580 df-bl 14581 df-mopn 14582 df-top 14748 df-topon 14761 df-bases 14793 df-ntr 14846 df-cn 14938 df-cnp 14939 df-tx 15003 df-cncf 15321 df-limced 15406 df-dvap 15407

This theorem is referenced by: (None)

W3C validator