tangtx - Intuitionistic Logic Explorer

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

Theorem tangtx 15561

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 10146	. . . . 5
2	1	recoscld 12284	. . . . 5
3	1, 2	remulcld 8209	. . . 4
4		1re 8177	. . . . . . 7
5		rehalfcl 9370	. . . . . . . . . 10
6	1, 5	syl 14	. . . . . . . . 9
7	6	resqcld 10960	. . . . . . . 8
8		3nn 9305	. . . . . . . 8
9		nndivre 9178	. . . . . . . 8 $/\$
10	7, 8, 9	sylancl 413	. . . . . . 7
11		resubcl 8442	. . . . . . 7 $/\$
12	4, 10, 11	sylancr 414	. . . . . 6
13	1, 12	remulcld 8209	. . . . 5
14		2re 9212	. . . . . . 7
15		remulcl 8159	. . . . . . 7 $/\$
16	14, 10, 15	sylancr 414	. . . . . 6
17		resubcl 8442	. . . . . 6 $/\$
18	4, 16, 17	sylancr 414	. . . . 5
19	13, 18	remulcld 8209	. . . 4
20	1	resincld 12283	. . . 4
21	12	resqcld 10960	. . . . . . . . 9
22		remulcl 8159	. . . . . . . . 9 $/\$
23	14, 21, 22	sylancr 414	. . . . . . . 8
24		resubcl 8442	. . . . . . . 8 $/\$
25	23, 4, 24	sylancl 413	. . . . . . 7
26	12, 18	remulcld 8209	. . . . . . 7
27	1	recnd 8207	. . . . . . . . . . 11
28		2cn 9213	. . . . . . . . . . . 12
29	28	a1i 9	. . . . . . . . . . 11
30		2ap0 9235	. . . . . . . . . . . 12 #
31	30	a1i 9	. . . . . . . . . . 11 #
32	27, 29, 31	divcanap2d 8971	. . . . . . . . . 10
33	32	fveq2d 5643	. . . . . . . . 9
34	6	recnd 8207	. . . . . . . . . 10
35		cos2t 12310	. . . . . . . . . 10
36	34, 35	syl 14	. . . . . . . . 9
37	33, 36	eqtr3d 2266	. . . . . . . 8
38	6	recoscld 12284	. . . . . . . . . . 11
39	38	resqcld 10960	. . . . . . . . . 10
40		remulcl 8159	. . . . . . . . . 10 $/\$
41	14, 39, 40	sylancr 414	. . . . . . . . 9
42	4	a1i 9	. . . . . . . . 9
43	14	a1i 9	. . . . . . . . . . . . . . 15
44		eliooord 10162	. . . . . . . . . . . . . . . 16 $/\$
45	44	simpld 112	. . . . . . . . . . . . . . 15
46		2pos 9233	. . . . . . . . . . . . . . . 16
47	46	a1i 9	. . . . . . . . . . . . . . 15
48	1, 43, 45, 47	divgt0d 9114	. . . . . . . . . . . . . 14
49		pire 15509	. . . . . . . . . . . . . . . . . . 19
50		rehalfcl 9370	. . . . . . . . . . . . . . . . . . 19
51	49, 50	mp1i 10	. . . . . . . . . . . . . . . . . 18
52	44	simprd 114	. . . . . . . . . . . . . . . . . 18
53		pigt2lt4 15507	. . . . . . . . . . . . . . . . . . . . . 22 $/\$
54	53	simpri 113	. . . . . . . . . . . . . . . . . . . . 21
55		2t2e4 9297	. . . . . . . . . . . . . . . . . . . . 21
56	54, 55	breqtrri 4115	. . . . . . . . . . . . . . . . . . . 20
57	14, 46	pm3.2i 272	. . . . . . . . . . . . . . . . . . . . 21 $/\$
58		ltdivmul 9055	. . . . . . . . . . . . . . . . . . . . 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 8304	. . . . . . . . . . . . . . . . 17
63	28	mullidi 8181	. . . . . . . . . . . . . . . . 17
64	62, 63	breqtrrdi 4130	. . . . . . . . . . . . . . . 16
65		ltdivmul2 9057	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$
66	1, 42, 43, 47, 65	syl112anc 1277	. . . . . . . . . . . . . . . 16
67	64, 66	mpbird 167	. . . . . . . . . . . . . . 15
68	6, 42, 67	ltled 8297	. . . . . . . . . . . . . 14
69		0xr 8225	. . . . . . . . . . . . . . 15
70		elioc2 10170	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$
71	69, 4, 70	mp2an 426	. . . . . . . . . . . . . 14 $/\$ $/\$
72	6, 48, 68, 71	syl3anbrc 1207	. . . . . . . . . . . . 13
73		cos01bnd 12318	. . . . . . . . . . . . 13 $/\$
74	72, 73	syl 14	. . . . . . . . . . . 12 $/\$
75	74	simprd 114	. . . . . . . . . . 11
76		cos01gt0 12323	. . . . . . . . . . . . . 14
77	72, 76	syl 14	. . . . . . . . . . . . 13
78		0re 8178	. . . . . . . . . . . . . 14
79		ltle 8266	. . . . . . . . . . . . . 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 8304	. . . . . . . . . . . . 13
84	82, 12, 83	ltled 8297	. . . . . . . . . . . 12
85	38, 12, 81, 84	lt2sqd 10965	. . . . . . . . . . 11
86	75, 85	mpbid 147	. . . . . . . . . 10
87		ltmul2 9035	. . . . . . . . . . 11 $/\$ $/\$ $/\$
88	39, 21, 43, 47, 87	syl112anc 1277	. . . . . . . . . 10
89	86, 88	mpbid 147	. . . . . . . . 9
90	41, 23, 42, 89	ltsub1dd 8736	. . . . . . . 8
91	37, 90	eqbrtrd 4110	. . . . . . 7
92		3re 9216	. . . . . . . . . 10
93		remulcl 8159	. . . . . . . . . 10 $/\$
94	92, 10, 93	sylancr 414	. . . . . . . . 9
95		4re 9219	. . . . . . . . . 10
96		remulcl 8159	. . . . . . . . . 10 $/\$
97	95, 10, 96	sylancr 414	. . . . . . . . 9
98	10	resqcld 10960	. . . . . . . . . . 11
99		remulcl 8159	. . . . . . . . . . 11 $/\$
100	14, 98, 99	sylancr 414	. . . . . . . . . 10
101		readdcl 8157	. . . . . . . . . 10 $/\$
102	4, 100, 101	sylancr 414	. . . . . . . . 9
103		3lt4 9315	. . . . . . . . . 10
104	92	a1i 9	. . . . . . . . . . 11
105	95	a1i 9	. . . . . . . . . . 11
106	6, 48	gt0ap0d 8808	. . . . . . . . . . . . 13 #
107	6, 106	sqgt0apd 10962	. . . . . . . . . . . 12
108		3pos 9236	. . . . . . . . . . . . 13
109	108	a1i 9	. . . . . . . . . . . 12
110	7, 104, 107, 109	divgt0d 9114	. . . . . . . . . . 11
111		ltmul1 8771	. . . . . . . . . . 11 $/\$ $/\$ $/\$
112	104, 105, 10, 110, 111	syl112anc 1277	. . . . . . . . . 10
113	103, 112	mpbii 148	. . . . . . . . 9
114	94, 97, 102, 113	ltsub2dd 8737	. . . . . . . 8
115	42	recnd 8207	. . . . . . . . 9
116		ax-1cn 8124	. . . . . . . . . . 11
117	100	recnd 8207	. . . . . . . . . . 11
118		addcl 8156	. . . . . . . . . . 11 $/\$
119	116, 117, 118	sylancr 414	. . . . . . . . . 10
120	97	recnd 8207	. . . . . . . . . 10
121	119, 120	subcld 8489	. . . . . . . . 9
122		sq1 10894	. . . . . . . . . . . . . . 15
123	122	a1i 9	. . . . . . . . . . . . . 14
124	10	recnd 8207	. . . . . . . . . . . . . . . 16
125	124	mulid2d 8197	. . . . . . . . . . . . . . 15
126	125	oveq2d 6033	. . . . . . . . . . . . . 14
127	123, 126	oveq12d 6035	. . . . . . . . . . . . 13
128	127	oveq1d 6032	. . . . . . . . . . . 12
129		binom2sub 10914	. . . . . . . . . . . . 13 $/\$
130	116, 124, 129	sylancr 414	. . . . . . . . . . . 12
131	98	recnd 8207	. . . . . . . . . . . . 13
132	16	recnd 8207	. . . . . . . . . . . . 13
133	115, 131, 132	addsubd 8510	. . . . . . . . . . . 12
134	128, 130, 133	3eqtr4d 2274	. . . . . . . . . . 11
135	134	oveq2d 6033	. . . . . . . . . 10
136		addcl 8156	. . . . . . . . . . . 12 $/\$
137	116, 131, 136	sylancr 414	. . . . . . . . . . 11
138	29, 137, 132	subdid 8592	. . . . . . . . . 10
139	29, 115, 131	adddid 8203	. . . . . . . . . . . . 13
140	116	2timesi 9272	. . . . . . . . . . . . . . 15
141	140	oveq1i 6027	. . . . . . . . . . . . . 14
142	115, 115, 117	addassd 8201	. . . . . . . . . . . . . 14
143	141, 142	eqtrid 2276	. . . . . . . . . . . . 13
144	139, 143	eqtrd 2264	. . . . . . . . . . . 12
145	29, 29, 124	mulassd 8202	. . . . . . . . . . . . 13
146	55	oveq1i 6027	. . . . . . . . . . . . 13
147	145, 146	eqtr3di 2279	. . . . . . . . . . . 12
148	144, 147	oveq12d 6035	. . . . . . . . . . 11
149	115, 119, 120, 148	assraddsubd 8546	. . . . . . . . . 10
150	135, 138, 149	3eqtrd 2268	. . . . . . . . 9
151	115, 121, 150	mvrladdd 8545	. . . . . . . 8
152		subcl 8377	. . . . . . . . . . 11 $/\$
153	116, 124, 152	sylancr 414	. . . . . . . . . 10
154	153, 115, 132	subdid 8592	. . . . . . . . 9
155	153	mulridd 8195	. . . . . . . . . 10
156	115, 124, 132	subdird 8593	. . . . . . . . . . 11
157	132	mulid2d 8197	. . . . . . . . . . . 12
158	124, 29, 124	mul12d 8330	. . . . . . . . . . . . 13
159	124	sqvald 10931	. . . . . . . . . . . . . 14
160	159	oveq2d 6033	. . . . . . . . . . . . 13
161	158, 160	eqtr4d 2267	. . . . . . . . . . . 12
162	157, 161	oveq12d 6035	. . . . . . . . . . 11
163	156, 162	eqtrd 2264	. . . . . . . . . 10
164	155, 163	oveq12d 6035	. . . . . . . . 9
165	115, 124, 132, 117	subadd4d 8537	. . . . . . . . . 10
166		df-3 9202	. . . . . . . . . . . . . 14
167	28, 116	addcomi 8322	. . . . . . . . . . . . . 14
168	166, 167	eqtri 2252	. . . . . . . . . . . . 13
169	168	oveq1i 6027	. . . . . . . . . . . 12
170	125	oveq1d 6032	. . . . . . . . . . . . 13
171	115, 124, 29, 170	joinlmuladdmuld 8206	. . . . . . . . . . . 12
172	169, 171	eqtrid 2276	. . . . . . . . . . 11
173	172	oveq2d 6033	. . . . . . . . . 10
174	165, 173	eqtr4d 2267	. . . . . . . . 9
175	154, 164, 174	3eqtrd 2268	. . . . . . . 8
176	114, 151, 175	3brtr4d 4120	. . . . . . 7
177	2, 25, 26, 91, 176	lttrd 8304	. . . . . 6
178		ltmul2 9035	. . . . . . 7 $/\$ $/\$ $/\$
179	2, 26, 1, 45, 178	syl112anc 1277	. . . . . 6
180	177, 179	mpbid 147	. . . . 5
181	18	recnd 8207	. . . . . 6
182	27, 153, 181	mulassd 8202	. . . . 5
183	180, 182	breqtrrd 4116	. . . 4
184	13, 38	remulcld 8209	. . . . 5
185	74	simpld 112	. . . . . 6
186	1, 12, 45, 83	mulgt0d 8301	. . . . . . 7
187		ltmul2 9035	. . . . . . 7 $/\$ $/\$ $/\$
188	18, 38, 13, 186, 187	syl112anc 1277	. . . . . 6
189	185, 188	mpbid 147	. . . . 5
190	29, 34, 153	mulassd 8202	. . . . . . . . 9
191	32	oveq1d 6032	. . . . . . . . 9
192	34, 115, 124	subdid 8592	. . . . . . . . . . 11
193	34	mulridd 8195	. . . . . . . . . . . 12
194	166	oveq2i 6028	. . . . . . . . . . . . . . . 16
195		2nn0 9418	. . . . . . . . . . . . . . . . 17
196		expp1 10807	. . . . . . . . . . . . . . . . 17 $/\$
197	34, 195, 196	sylancl 413	. . . . . . . . . . . . . . . 16
198	194, 197	eqtrid 2276	. . . . . . . . . . . . . . 15
199	7	recnd 8207	. . . . . . . . . . . . . . . 16
200	199, 34	mulcomd 8200	. . . . . . . . . . . . . . 15
201	198, 200	eqtrd 2264	. . . . . . . . . . . . . 14
202	201	oveq1d 6032	. . . . . . . . . . . . 13
203		3cn 9217	. . . . . . . . . . . . . . 15
204	203	a1i 9	. . . . . . . . . . . . . 14
205	104, 109	gt0ap0d 8808	. . . . . . . . . . . . . 14 #
206	34, 199, 204, 205	divassapd 9005	. . . . . . . . . . . . 13
207	202, 206	eqtr2d 2265	. . . . . . . . . . . 12
208	193, 207	oveq12d 6035	. . . . . . . . . . 11
209	192, 208	eqtrd 2264	. . . . . . . . . 10
210	209	oveq2d 6033	. . . . . . . . 9
211	190, 191, 210	3eqtr3d 2272	. . . . . . . 8
212		sin01bnd 12317	. . . . . . . . . . 11 $/\$
213	72, 212	syl 14	. . . . . . . . . 10 $/\$
214	213	simpld 112	. . . . . . . . 9
215		3nn0 9419	. . . . . . . . . . . . 13
216		reexpcl 10817	. . . . . . . . . . . . 13 $/\$
217	6, 215, 216	sylancl 413	. . . . . . . . . . . 12
218		nndivre 9178	. . . . . . . . . . . 12 $/\$
219	217, 8, 218	sylancl 413	. . . . . . . . . . 11
220	6, 219	resubcld 8559	. . . . . . . . . 10
221	6	resincld 12283	. . . . . . . . . 10
222		ltmul2 9035	. . . . . . . . . 10 $/\$ $/\$ $/\$
223	220, 221, 43, 47, 222	syl112anc 1277	. . . . . . . . 9
224	214, 223	mpbid 147	. . . . . . . 8
225	211, 224	eqbrtrd 4110	. . . . . . 7
226		remulcl 8159	. . . . . . . . 9 $/\$
227	14, 221, 226	sylancr 414	. . . . . . . 8
228		ltmul1 8771	. . . . . . . 8 $/\$ $/\$ $/\$
229	13, 227, 38, 77, 228	syl112anc 1277	. . . . . . 7
230	225, 229	mpbid 147	. . . . . 6
231	221	recnd 8207	. . . . . . . 8
232	38	recnd 8207	. . . . . . . 8
233	29, 231, 232	mulassd 8202	. . . . . . 7
234		sin2t 12309	. . . . . . . 8
235	34, 234	syl 14	. . . . . . 7
236	32	fveq2d 5643	. . . . . . 7
237	233, 235, 236	3eqtr2rd 2271	. . . . . 6
238	230, 237	breqtrrd 4116	. . . . 5
239	19, 184, 20, 189, 238	lttrd 8304	. . . 4
240	3, 19, 20, 183, 239	lttrd 8304	. . 3
241		sincosq1sgn 15549	. . . . 5 $/\$
242	241	simprd 114	. . . 4
243		ltmuldiv 9053	. . . 4 $/\$ $/\$ $/\$
244	1, 20, 2, 242, 243	syl112anc 1277	. . 3
245	240, 244	mpbid 147	. 2
246	2, 242	gt0ap0d 8808	. . 3 #
247		tanvalap 12268	. . 3 $/\$ #
248	27, 246, 247	syl2anc 411	. 2
249	245, 248	breqtrrd 4116	1

Colors of variables: wff set class

Syntax hints:

wi 4 $/\$ wa 104

wb 105 $/\$ w3a 1004

wceq 1397

wcel 2202 class class class wbr 4088

cfv 5326 (class class class)co 6017

cc 8029

cr 8030

cc0 8031

c1 8032

caddc 8034

cmul 8036

cxr 8212

clt 8213

cle 8214

cmin 8349 # cap 8760

cdiv 8851

cn 9142

c2 9193

c3 9194

c4 9195

cn0 9401

cioo 10122

cioc 10123

cexp 10799

csin 12204

ccos 12205

ctan 12206

cpi 12207

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 2204 ax-14 2205 ax-ext 2213 ax-coll 4204 ax-sep 4207 ax-nul 4215 ax-pow 4264 ax-pr 4299 ax-un 4530 ax-setind 4635 ax-iinf 4686 ax-cnex 8122 ax-resscn 8123 ax-1cn 8124 ax-1re 8125 ax-icn 8126 ax-addcl 8127 ax-addrcl 8128 ax-mulcl 8129 ax-mulrcl 8130 ax-addcom 8131 ax-mulcom 8132 ax-addass 8133 ax-mulass 8134 ax-distr 8135 ax-i2m1 8136 ax-0lt1 8137 ax-1rid 8138 ax-0id 8139 ax-rnegex 8140 ax-precex 8141 ax-cnre 8142 ax-pre-ltirr 8143 ax-pre-ltwlin 8144 ax-pre-lttrn 8145 ax-pre-apti 8146 ax-pre-ltadd 8147 ax-pre-mulgt0 8148 ax-pre-mulext 8149 ax-arch 8150 ax-caucvg 8151 ax-pre-suploc 8152 ax-addf 8153 ax-mulf 8154

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 1811 df-eu 2082 df-mo 2083 df-clab 2218 df-cleq 2224 df-clel 2227 df-nfc 2363 df-ne 2403 df-nel 2498 df-ral 2515 df-rex 2516 df-reu 2517 df-rmo 2518 df-rab 2519 df-v 2804 df-sbc 3032 df-csb 3128 df-dif 3202 df-un 3204 df-in 3206 df-ss 3213 df-nul 3495 df-if 3606 df-pw 3654 df-sn 3675 df-pr 3676 df-op 3678 df-uni 3894 df-int 3929 df-iun 3972 df-disj 4065 df-br 4089 df-opab 4151 df-mpt 4152 df-tr 4188 df-id 4390 df-po 4393 df-iso 4394 df-iord 4463 df-on 4465 df-ilim 4466 df-suc 4468 df-iom 4689 df-xp 4731 df-rel 4732 df-cnv 4733 df-co 4734 df-dm 4735 df-rn 4736 df-res 4737 df-ima 4738 df-iota 5286 df-fun 5328 df-fn 5329 df-f 5330 df-f1 5331 df-fo 5332 df-f1o 5333 df-fv 5334 df-isom 5335 df-riota 5970 df-ov 6020 df-oprab 6021 df-mpo 6022 df-of 6234 df-1st 6302 df-2nd 6303 df-recs 6470 df-irdg 6535 df-frec 6556 df-1o 6581 df-oadd 6585 df-er 6701 df-map 6818 df-pm 6819 df-en 6909 df-dom 6910 df-fin 6911 df-sup 7182 df-inf 7183 df-pnf 8215 df-mnf 8216 df-xr 8217 df-ltxr 8218 df-le 8219 df-sub 8351 df-neg 8352 df-reap 8754 df-ap 8761 df-div 8852 df-inn 9143 df-2 9201 df-3 9202 df-4 9203 df-5 9204 df-6 9205 df-7 9206 df-8 9207 df-9 9208 df-n0 9402 df-z 9479 df-uz 9755 df-q 9853 df-rp 9888 df-xneg 10006 df-xadd 10007 df-ioo 10126 df-ioc 10127 df-ico 10128 df-icc 10129 df-fz 10243 df-fzo 10377 df-seqfrec 10709 df-exp 10800 df-fac 10987 df-bc 11009 df-ihash 11037 df-shft 11375 df-cj 11402 df-re 11403 df-im 11404 df-rsqrt 11558 df-abs 11559 df-clim 11839 df-sumdc 11914 df-ef 12208 df-sin 12210 df-cos 12211 df-tan 12212 df-pi 12213 df-rest 13323 df-topgen 13342 df-psmet 14556 df-xmet 14557 df-met 14558 df-bl 14559 df-mopn 14560 df-top 14721 df-topon 14734 df-bases 14766 df-ntr 14819 df-cn 14911 df-cnp 14912 df-tx 14976 df-cncf 15294 df-limced 15379 df-dvap 15380

This theorem is referenced by: (None)

W3C validator