tangtx - Intuitionistic Logic Explorer

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

Theorem tangtx 15527

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 10120	. . . . 5
2	1	recoscld 12250	. . . . 5
3	1, 2	remulcld 8188	. . . 4
4		1re 8156	. . . . . . 7
5		rehalfcl 9349	. . . . . . . . . 10
6	1, 5	syl 14	. . . . . . . . 9
7	6	resqcld 10933	. . . . . . . 8
8		3nn 9284	. . . . . . . 8
9		nndivre 9157	. . . . . . . 8 $/\$
10	7, 8, 9	sylancl 413	. . . . . . 7
11		resubcl 8421	. . . . . . 7 $/\$
12	4, 10, 11	sylancr 414	. . . . . 6
13	1, 12	remulcld 8188	. . . . 5
14		2re 9191	. . . . . . 7
15		remulcl 8138	. . . . . . 7 $/\$
16	14, 10, 15	sylancr 414	. . . . . 6
17		resubcl 8421	. . . . . 6 $/\$
18	4, 16, 17	sylancr 414	. . . . 5
19	13, 18	remulcld 8188	. . . 4
20	1	resincld 12249	. . . 4
21	12	resqcld 10933	. . . . . . . . 9
22		remulcl 8138	. . . . . . . . 9 $/\$
23	14, 21, 22	sylancr 414	. . . . . . . 8
24		resubcl 8421	. . . . . . . 8 $/\$
25	23, 4, 24	sylancl 413	. . . . . . 7
26	12, 18	remulcld 8188	. . . . . . 7
27	1	recnd 8186	. . . . . . . . . . 11
28		2cn 9192	. . . . . . . . . . . 12
29	28	a1i 9	. . . . . . . . . . 11
30		2ap0 9214	. . . . . . . . . . . 12 #
31	30	a1i 9	. . . . . . . . . . 11 #
32	27, 29, 31	divcanap2d 8950	. . . . . . . . . 10
33	32	fveq2d 5633	. . . . . . . . 9
34	6	recnd 8186	. . . . . . . . . 10
35		cos2t 12276	. . . . . . . . . 10
36	34, 35	syl 14	. . . . . . . . 9
37	33, 36	eqtr3d 2264	. . . . . . . 8
38	6	recoscld 12250	. . . . . . . . . . 11
39	38	resqcld 10933	. . . . . . . . . 10
40		remulcl 8138	. . . . . . . . . 10 $/\$
41	14, 39, 40	sylancr 414	. . . . . . . . 9
42	4	a1i 9	. . . . . . . . 9
43	14	a1i 9	. . . . . . . . . . . . . . 15
44		eliooord 10136	. . . . . . . . . . . . . . . 16 $/\$
45	44	simpld 112	. . . . . . . . . . . . . . 15
46		2pos 9212	. . . . . . . . . . . . . . . 16
47	46	a1i 9	. . . . . . . . . . . . . . 15
48	1, 43, 45, 47	divgt0d 9093	. . . . . . . . . . . . . 14
49		pire 15475	. . . . . . . . . . . . . . . . . . 19
50		rehalfcl 9349	. . . . . . . . . . . . . . . . . . 19
51	49, 50	mp1i 10	. . . . . . . . . . . . . . . . . 18
52	44	simprd 114	. . . . . . . . . . . . . . . . . 18
53		pigt2lt4 15473	. . . . . . . . . . . . . . . . . . . . . 22 $/\$
54	53	simpri 113	. . . . . . . . . . . . . . . . . . . . 21
55		2t2e4 9276	. . . . . . . . . . . . . . . . . . . . 21
56	54, 55	breqtrri 4110	. . . . . . . . . . . . . . . . . . . 20
57	14, 46	pm3.2i 272	. . . . . . . . . . . . . . . . . . . . 21 $/\$
58		ltdivmul 9034	. . . . . . . . . . . . . . . . . . . . 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 8283	. . . . . . . . . . . . . . . . 17
63	28	mullidi 8160	. . . . . . . . . . . . . . . . 17
64	62, 63	breqtrrdi 4125	. . . . . . . . . . . . . . . 16
65		ltdivmul2 9036	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$
66	1, 42, 43, 47, 65	syl112anc 1275	. . . . . . . . . . . . . . . 16
67	64, 66	mpbird 167	. . . . . . . . . . . . . . 15
68	6, 42, 67	ltled 8276	. . . . . . . . . . . . . 14
69		0xr 8204	. . . . . . . . . . . . . . 15
70		elioc2 10144	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$
71	69, 4, 70	mp2an 426	. . . . . . . . . . . . . 14 $/\$ $/\$
72	6, 48, 68, 71	syl3anbrc 1205	. . . . . . . . . . . . 13
73		cos01bnd 12284	. . . . . . . . . . . . 13 $/\$
74	72, 73	syl 14	. . . . . . . . . . . 12 $/\$
75	74	simprd 114	. . . . . . . . . . 11
76		cos01gt0 12289	. . . . . . . . . . . . . 14
77	72, 76	syl 14	. . . . . . . . . . . . 13
78		0re 8157	. . . . . . . . . . . . . 14
79		ltle 8245	. . . . . . . . . . . . . 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 8283	. . . . . . . . . . . . 13
84	82, 12, 83	ltled 8276	. . . . . . . . . . . 12
85	38, 12, 81, 84	lt2sqd 10938	. . . . . . . . . . 11
86	75, 85	mpbid 147	. . . . . . . . . 10
87		ltmul2 9014	. . . . . . . . . . 11 $/\$ $/\$ $/\$
88	39, 21, 43, 47, 87	syl112anc 1275	. . . . . . . . . 10
89	86, 88	mpbid 147	. . . . . . . . 9
90	41, 23, 42, 89	ltsub1dd 8715	. . . . . . . 8
91	37, 90	eqbrtrd 4105	. . . . . . 7
92		3re 9195	. . . . . . . . . 10
93		remulcl 8138	. . . . . . . . . 10 $/\$
94	92, 10, 93	sylancr 414	. . . . . . . . 9
95		4re 9198	. . . . . . . . . 10
96		remulcl 8138	. . . . . . . . . 10 $/\$
97	95, 10, 96	sylancr 414	. . . . . . . . 9
98	10	resqcld 10933	. . . . . . . . . . 11
99		remulcl 8138	. . . . . . . . . . 11 $/\$
100	14, 98, 99	sylancr 414	. . . . . . . . . 10
101		readdcl 8136	. . . . . . . . . 10 $/\$
102	4, 100, 101	sylancr 414	. . . . . . . . 9
103		3lt4 9294	. . . . . . . . . 10
104	92	a1i 9	. . . . . . . . . . 11
105	95	a1i 9	. . . . . . . . . . 11
106	6, 48	gt0ap0d 8787	. . . . . . . . . . . . 13 #
107	6, 106	sqgt0apd 10935	. . . . . . . . . . . 12
108		3pos 9215	. . . . . . . . . . . . 13
109	108	a1i 9	. . . . . . . . . . . 12
110	7, 104, 107, 109	divgt0d 9093	. . . . . . . . . . 11
111		ltmul1 8750	. . . . . . . . . . 11 $/\$ $/\$ $/\$
112	104, 105, 10, 110, 111	syl112anc 1275	. . . . . . . . . 10
113	103, 112	mpbii 148	. . . . . . . . 9
114	94, 97, 102, 113	ltsub2dd 8716	. . . . . . . 8
115	42	recnd 8186	. . . . . . . . 9
116		ax-1cn 8103	. . . . . . . . . . 11
117	100	recnd 8186	. . . . . . . . . . 11
118		addcl 8135	. . . . . . . . . . 11 $/\$
119	116, 117, 118	sylancr 414	. . . . . . . . . 10
120	97	recnd 8186	. . . . . . . . . 10
121	119, 120	subcld 8468	. . . . . . . . 9
122		sq1 10867	. . . . . . . . . . . . . . 15
123	122	a1i 9	. . . . . . . . . . . . . 14
124	10	recnd 8186	. . . . . . . . . . . . . . . 16
125	124	mulid2d 8176	. . . . . . . . . . . . . . 15
126	125	oveq2d 6023	. . . . . . . . . . . . . 14
127	123, 126	oveq12d 6025	. . . . . . . . . . . . 13
128	127	oveq1d 6022	. . . . . . . . . . . 12
129		binom2sub 10887	. . . . . . . . . . . . 13 $/\$
130	116, 124, 129	sylancr 414	. . . . . . . . . . . 12
131	98	recnd 8186	. . . . . . . . . . . . 13
132	16	recnd 8186	. . . . . . . . . . . . 13
133	115, 131, 132	addsubd 8489	. . . . . . . . . . . 12
134	128, 130, 133	3eqtr4d 2272	. . . . . . . . . . 11
135	134	oveq2d 6023	. . . . . . . . . 10
136		addcl 8135	. . . . . . . . . . . 12 $/\$
137	116, 131, 136	sylancr 414	. . . . . . . . . . 11
138	29, 137, 132	subdid 8571	. . . . . . . . . 10
139	29, 115, 131	adddid 8182	. . . . . . . . . . . . 13
140	116	2timesi 9251	. . . . . . . . . . . . . . 15
141	140	oveq1i 6017	. . . . . . . . . . . . . 14
142	115, 115, 117	addassd 8180	. . . . . . . . . . . . . 14
143	141, 142	eqtrid 2274	. . . . . . . . . . . . 13
144	139, 143	eqtrd 2262	. . . . . . . . . . . 12
145	29, 29, 124	mulassd 8181	. . . . . . . . . . . . 13
146	55	oveq1i 6017	. . . . . . . . . . . . 13
147	145, 146	eqtr3di 2277	. . . . . . . . . . . 12
148	144, 147	oveq12d 6025	. . . . . . . . . . 11
149	115, 119, 120, 148	assraddsubd 8525	. . . . . . . . . 10
150	135, 138, 149	3eqtrd 2266	. . . . . . . . 9
151	115, 121, 150	mvrladdd 8524	. . . . . . . 8
152		subcl 8356	. . . . . . . . . . 11 $/\$
153	116, 124, 152	sylancr 414	. . . . . . . . . 10
154	153, 115, 132	subdid 8571	. . . . . . . . 9
155	153	mulridd 8174	. . . . . . . . . 10
156	115, 124, 132	subdird 8572	. . . . . . . . . . 11
157	132	mulid2d 8176	. . . . . . . . . . . 12
158	124, 29, 124	mul12d 8309	. . . . . . . . . . . . 13
159	124	sqvald 10904	. . . . . . . . . . . . . 14
160	159	oveq2d 6023	. . . . . . . . . . . . 13
161	158, 160	eqtr4d 2265	. . . . . . . . . . . 12
162	157, 161	oveq12d 6025	. . . . . . . . . . 11
163	156, 162	eqtrd 2262	. . . . . . . . . 10
164	155, 163	oveq12d 6025	. . . . . . . . 9
165	115, 124, 132, 117	subadd4d 8516	. . . . . . . . . 10
166		df-3 9181	. . . . . . . . . . . . . 14
167	28, 116	addcomi 8301	. . . . . . . . . . . . . 14
168	166, 167	eqtri 2250	. . . . . . . . . . . . 13
169	168	oveq1i 6017	. . . . . . . . . . . 12
170	125	oveq1d 6022	. . . . . . . . . . . . 13
171	115, 124, 29, 170	joinlmuladdmuld 8185	. . . . . . . . . . . 12
172	169, 171	eqtrid 2274	. . . . . . . . . . 11
173	172	oveq2d 6023	. . . . . . . . . 10
174	165, 173	eqtr4d 2265	. . . . . . . . 9
175	154, 164, 174	3eqtrd 2266	. . . . . . . 8
176	114, 151, 175	3brtr4d 4115	. . . . . . 7
177	2, 25, 26, 91, 176	lttrd 8283	. . . . . 6
178		ltmul2 9014	. . . . . . 7 $/\$ $/\$ $/\$
179	2, 26, 1, 45, 178	syl112anc 1275	. . . . . 6
180	177, 179	mpbid 147	. . . . 5
181	18	recnd 8186	. . . . . 6
182	27, 153, 181	mulassd 8181	. . . . 5
183	180, 182	breqtrrd 4111	. . . 4
184	13, 38	remulcld 8188	. . . . 5
185	74	simpld 112	. . . . . 6
186	1, 12, 45, 83	mulgt0d 8280	. . . . . . 7
187		ltmul2 9014	. . . . . . 7 $/\$ $/\$ $/\$
188	18, 38, 13, 186, 187	syl112anc 1275	. . . . . 6
189	185, 188	mpbid 147	. . . . 5
190	29, 34, 153	mulassd 8181	. . . . . . . . 9
191	32	oveq1d 6022	. . . . . . . . 9
192	34, 115, 124	subdid 8571	. . . . . . . . . . 11
193	34	mulridd 8174	. . . . . . . . . . . 12
194	166	oveq2i 6018	. . . . . . . . . . . . . . . 16
195		2nn0 9397	. . . . . . . . . . . . . . . . 17
196		expp1 10780	. . . . . . . . . . . . . . . . 17 $/\$
197	34, 195, 196	sylancl 413	. . . . . . . . . . . . . . . 16
198	194, 197	eqtrid 2274	. . . . . . . . . . . . . . 15
199	7	recnd 8186	. . . . . . . . . . . . . . . 16
200	199, 34	mulcomd 8179	. . . . . . . . . . . . . . 15
201	198, 200	eqtrd 2262	. . . . . . . . . . . . . 14
202	201	oveq1d 6022	. . . . . . . . . . . . 13
203		3cn 9196	. . . . . . . . . . . . . . 15
204	203	a1i 9	. . . . . . . . . . . . . 14
205	104, 109	gt0ap0d 8787	. . . . . . . . . . . . . 14 #
206	34, 199, 204, 205	divassapd 8984	. . . . . . . . . . . . 13
207	202, 206	eqtr2d 2263	. . . . . . . . . . . 12
208	193, 207	oveq12d 6025	. . . . . . . . . . 11
209	192, 208	eqtrd 2262	. . . . . . . . . 10
210	209	oveq2d 6023	. . . . . . . . 9
211	190, 191, 210	3eqtr3d 2270	. . . . . . . 8
212		sin01bnd 12283	. . . . . . . . . . 11 $/\$
213	72, 212	syl 14	. . . . . . . . . 10 $/\$
214	213	simpld 112	. . . . . . . . 9
215		3nn0 9398	. . . . . . . . . . . . 13
216		reexpcl 10790	. . . . . . . . . . . . 13 $/\$
217	6, 215, 216	sylancl 413	. . . . . . . . . . . 12
218		nndivre 9157	. . . . . . . . . . . 12 $/\$
219	217, 8, 218	sylancl 413	. . . . . . . . . . 11
220	6, 219	resubcld 8538	. . . . . . . . . 10
221	6	resincld 12249	. . . . . . . . . 10
222		ltmul2 9014	. . . . . . . . . 10 $/\$ $/\$ $/\$
223	220, 221, 43, 47, 222	syl112anc 1275	. . . . . . . . 9
224	214, 223	mpbid 147	. . . . . . . 8
225	211, 224	eqbrtrd 4105	. . . . . . 7
226		remulcl 8138	. . . . . . . . 9 $/\$
227	14, 221, 226	sylancr 414	. . . . . . . 8
228		ltmul1 8750	. . . . . . . 8 $/\$ $/\$ $/\$
229	13, 227, 38, 77, 228	syl112anc 1275	. . . . . . 7
230	225, 229	mpbid 147	. . . . . 6
231	221	recnd 8186	. . . . . . . 8
232	38	recnd 8186	. . . . . . . 8
233	29, 231, 232	mulassd 8181	. . . . . . 7
234		sin2t 12275	. . . . . . . 8
235	34, 234	syl 14	. . . . . . 7
236	32	fveq2d 5633	. . . . . . 7
237	233, 235, 236	3eqtr2rd 2269	. . . . . 6
238	230, 237	breqtrrd 4111	. . . . 5
239	19, 184, 20, 189, 238	lttrd 8283	. . . 4
240	3, 19, 20, 183, 239	lttrd 8283	. . 3
241		sincosq1sgn 15515	. . . . 5 $/\$
242	241	simprd 114	. . . 4
243		ltmuldiv 9032	. . . 4 $/\$ $/\$ $/\$
244	1, 20, 2, 242, 243	syl112anc 1275	. . 3
245	240, 244	mpbid 147	. 2
246	2, 242	gt0ap0d 8787	. . 3 #
247		tanvalap 12234	. . 3 $/\$ #
248	27, 246, 247	syl2anc 411	. 2
249	245, 248	breqtrrd 4111	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 4083

cfv 5318 (class class class)co 6007

cc 8008

cr 8009

cc0 8010

c1 8011

caddc 8013

cmul 8015

cxr 8191

clt 8192

cle 8193

cmin 8328 # cap 8739

cdiv 8830

cn 9121

c2 9172

c3 9173

c4 9174

cn0 9380

cioo 10096

cioc 10097

cexp 10772

csin 12170

ccos 12171

ctan 12172

cpi 12173

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 4199 ax-sep 4202 ax-nul 4210 ax-pow 4258 ax-pr 4293 ax-un 4524 ax-setind 4629 ax-iinf 4680 ax-cnex 8101 ax-resscn 8102 ax-1cn 8103 ax-1re 8104 ax-icn 8105 ax-addcl 8106 ax-addrcl 8107 ax-mulcl 8108 ax-mulrcl 8109 ax-addcom 8110 ax-mulcom 8111 ax-addass 8112 ax-mulass 8113 ax-distr 8114 ax-i2m1 8115 ax-0lt1 8116 ax-1rid 8117 ax-0id 8118 ax-rnegex 8119 ax-precex 8120 ax-cnre 8121 ax-pre-ltirr 8122 ax-pre-ltwlin 8123 ax-pre-lttrn 8124 ax-pre-apti 8125 ax-pre-ltadd 8126 ax-pre-mulgt0 8127 ax-pre-mulext 8128 ax-arch 8129 ax-caucvg 8130 ax-pre-suploc 8131 ax-addf 8132 ax-mulf 8133

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 3889 df-int 3924 df-iun 3967 df-disj 4060 df-br 4084 df-opab 4146 df-mpt 4147 df-tr 4183 df-id 4384 df-po 4387 df-iso 4388 df-iord 4457 df-on 4459 df-ilim 4460 df-suc 4462 df-iom 4683 df-xp 4725 df-rel 4726 df-cnv 4727 df-co 4728 df-dm 4729 df-rn 4730 df-res 4731 df-ima 4732 df-iota 5278 df-fun 5320 df-fn 5321 df-f 5322 df-f1 5323 df-fo 5324 df-f1o 5325 df-fv 5326 df-isom 5327 df-riota 5960 df-ov 6010 df-oprab 6011 df-mpo 6012 df-of 6224 df-1st 6292 df-2nd 6293 df-recs 6457 df-irdg 6522 df-frec 6543 df-1o 6568 df-oadd 6572 df-er 6688 df-map 6805 df-pm 6806 df-en 6896 df-dom 6897 df-fin 6898 df-sup 7162 df-inf 7163 df-pnf 8194 df-mnf 8195 df-xr 8196 df-ltxr 8197 df-le 8198 df-sub 8330 df-neg 8331 df-reap 8733 df-ap 8740 df-div 8831 df-inn 9122 df-2 9180 df-3 9181 df-4 9182 df-5 9183 df-6 9184 df-7 9185 df-8 9186 df-9 9187 df-n0 9381 df-z 9458 df-uz 9734 df-q 9827 df-rp 9862 df-xneg 9980 df-xadd 9981 df-ioo 10100 df-ioc 10101 df-ico 10102 df-icc 10103 df-fz 10217 df-fzo 10351 df-seqfrec 10682 df-exp 10773 df-fac 10960 df-bc 10982 df-ihash 11010 df-shft 11341 df-cj 11368 df-re 11369 df-im 11370 df-rsqrt 11524 df-abs 11525 df-clim 11805 df-sumdc 11880 df-ef 12174 df-sin 12176 df-cos 12177 df-tan 12178 df-pi 12179 df-rest 13289 df-topgen 13308 df-psmet 14522 df-xmet 14523 df-met 14524 df-bl 14525 df-mopn 14526 df-top 14687 df-topon 14700 df-bases 14732 df-ntr 14785 df-cn 14877 df-cnp 14878 df-tx 14942 df-cncf 15260 df-limced 15345 df-dvap 15346

This theorem is referenced by: (None)

W3C validator