tangtx - Intuitionistic Logic Explorer

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

Theorem tangtx 15310

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 10034	. . . . 5
2	1	recoscld 12035	. . . . 5
3	1, 2	remulcld 8103	. . . 4
4		1re 8071	. . . . . . 7
5		rehalfcl 9264	. . . . . . . . . 10
6	1, 5	syl 14	. . . . . . . . 9
7	6	resqcld 10844	. . . . . . . 8
8		3nn 9199	. . . . . . . 8
9		nndivre 9072	. . . . . . . 8 $/\$
10	7, 8, 9	sylancl 413	. . . . . . 7
11		resubcl 8336	. . . . . . 7 $/\$
12	4, 10, 11	sylancr 414	. . . . . 6
13	1, 12	remulcld 8103	. . . . 5
14		2re 9106	. . . . . . 7
15		remulcl 8053	. . . . . . 7 $/\$
16	14, 10, 15	sylancr 414	. . . . . 6
17		resubcl 8336	. . . . . 6 $/\$
18	4, 16, 17	sylancr 414	. . . . 5
19	13, 18	remulcld 8103	. . . 4
20	1	resincld 12034	. . . 4
21	12	resqcld 10844	. . . . . . . . 9
22		remulcl 8053	. . . . . . . . 9 $/\$
23	14, 21, 22	sylancr 414	. . . . . . . 8
24		resubcl 8336	. . . . . . . 8 $/\$
25	23, 4, 24	sylancl 413	. . . . . . 7
26	12, 18	remulcld 8103	. . . . . . 7
27	1	recnd 8101	. . . . . . . . . . 11
28		2cn 9107	. . . . . . . . . . . 12
29	28	a1i 9	. . . . . . . . . . 11
30		2ap0 9129	. . . . . . . . . . . 12 #
31	30	a1i 9	. . . . . . . . . . 11 #
32	27, 29, 31	divcanap2d 8865	. . . . . . . . . 10
33	32	fveq2d 5580	. . . . . . . . 9
34	6	recnd 8101	. . . . . . . . . 10
35		cos2t 12061	. . . . . . . . . 10
36	34, 35	syl 14	. . . . . . . . 9
37	33, 36	eqtr3d 2240	. . . . . . . 8
38	6	recoscld 12035	. . . . . . . . . . 11
39	38	resqcld 10844	. . . . . . . . . 10
40		remulcl 8053	. . . . . . . . . 10 $/\$
41	14, 39, 40	sylancr 414	. . . . . . . . 9
42	4	a1i 9	. . . . . . . . 9
43	14	a1i 9	. . . . . . . . . . . . . . 15
44		eliooord 10050	. . . . . . . . . . . . . . . 16 $/\$
45	44	simpld 112	. . . . . . . . . . . . . . 15
46		2pos 9127	. . . . . . . . . . . . . . . 16
47	46	a1i 9	. . . . . . . . . . . . . . 15
48	1, 43, 45, 47	divgt0d 9008	. . . . . . . . . . . . . 14
49		pire 15258	. . . . . . . . . . . . . . . . . . 19
50		rehalfcl 9264	. . . . . . . . . . . . . . . . . . 19
51	49, 50	mp1i 10	. . . . . . . . . . . . . . . . . 18
52	44	simprd 114	. . . . . . . . . . . . . . . . . 18
53		pigt2lt4 15256	. . . . . . . . . . . . . . . . . . . . . 22 $/\$
54	53	simpri 113	. . . . . . . . . . . . . . . . . . . . 21
55		2t2e4 9191	. . . . . . . . . . . . . . . . . . . . 21
56	54, 55	breqtrri 4071	. . . . . . . . . . . . . . . . . . . 20
57	14, 46	pm3.2i 272	. . . . . . . . . . . . . . . . . . . . 21 $/\$
58		ltdivmul 8949	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$ $/\$
59	49, 14, 57, 58	mp3an 1350	. . . . . . . . . . . . . . . . . . . 20
60	56, 59	mpbir 146	. . . . . . . . . . . . . . . . . . 19
61	60	a1i 9	. . . . . . . . . . . . . . . . . 18
62	1, 51, 43, 52, 61	lttrd 8198	. . . . . . . . . . . . . . . . 17
63	28	mullidi 8075	. . . . . . . . . . . . . . . . 17
64	62, 63	breqtrrdi 4086	. . . . . . . . . . . . . . . 16
65		ltdivmul2 8951	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$
66	1, 42, 43, 47, 65	syl112anc 1254	. . . . . . . . . . . . . . . 16
67	64, 66	mpbird 167	. . . . . . . . . . . . . . 15
68	6, 42, 67	ltled 8191	. . . . . . . . . . . . . 14
69		0xr 8119	. . . . . . . . . . . . . . 15
70		elioc2 10058	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$
71	69, 4, 70	mp2an 426	. . . . . . . . . . . . . 14 $/\$ $/\$
72	6, 48, 68, 71	syl3anbrc 1184	. . . . . . . . . . . . 13
73		cos01bnd 12069	. . . . . . . . . . . . 13 $/\$
74	72, 73	syl 14	. . . . . . . . . . . 12 $/\$
75	74	simprd 114	. . . . . . . . . . 11
76		cos01gt0 12074	. . . . . . . . . . . . . 14
77	72, 76	syl 14	. . . . . . . . . . . . 13
78		0re 8072	. . . . . . . . . . . . . 14
79		ltle 8160	. . . . . . . . . . . . . 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 8198	. . . . . . . . . . . . 13
84	82, 12, 83	ltled 8191	. . . . . . . . . . . 12
85	38, 12, 81, 84	lt2sqd 10849	. . . . . . . . . . 11
86	75, 85	mpbid 147	. . . . . . . . . 10
87		ltmul2 8929	. . . . . . . . . . 11 $/\$ $/\$ $/\$
88	39, 21, 43, 47, 87	syl112anc 1254	. . . . . . . . . 10
89	86, 88	mpbid 147	. . . . . . . . 9
90	41, 23, 42, 89	ltsub1dd 8630	. . . . . . . 8
91	37, 90	eqbrtrd 4066	. . . . . . 7
92		3re 9110	. . . . . . . . . 10
93		remulcl 8053	. . . . . . . . . 10 $/\$
94	92, 10, 93	sylancr 414	. . . . . . . . 9
95		4re 9113	. . . . . . . . . 10
96		remulcl 8053	. . . . . . . . . 10 $/\$
97	95, 10, 96	sylancr 414	. . . . . . . . 9
98	10	resqcld 10844	. . . . . . . . . . 11
99		remulcl 8053	. . . . . . . . . . 11 $/\$
100	14, 98, 99	sylancr 414	. . . . . . . . . 10
101		readdcl 8051	. . . . . . . . . 10 $/\$
102	4, 100, 101	sylancr 414	. . . . . . . . 9
103		3lt4 9209	. . . . . . . . . 10
104	92	a1i 9	. . . . . . . . . . 11
105	95	a1i 9	. . . . . . . . . . 11
106	6, 48	gt0ap0d 8702	. . . . . . . . . . . . 13 #
107	6, 106	sqgt0apd 10846	. . . . . . . . . . . 12
108		3pos 9130	. . . . . . . . . . . . 13
109	108	a1i 9	. . . . . . . . . . . 12
110	7, 104, 107, 109	divgt0d 9008	. . . . . . . . . . 11
111		ltmul1 8665	. . . . . . . . . . 11 $/\$ $/\$ $/\$
112	104, 105, 10, 110, 111	syl112anc 1254	. . . . . . . . . 10
113	103, 112	mpbii 148	. . . . . . . . 9
114	94, 97, 102, 113	ltsub2dd 8631	. . . . . . . 8
115	42	recnd 8101	. . . . . . . . 9
116		ax-1cn 8018	. . . . . . . . . . 11
117	100	recnd 8101	. . . . . . . . . . 11
118		addcl 8050	. . . . . . . . . . 11 $/\$
119	116, 117, 118	sylancr 414	. . . . . . . . . 10
120	97	recnd 8101	. . . . . . . . . 10
121	119, 120	subcld 8383	. . . . . . . . 9
122		sq1 10778	. . . . . . . . . . . . . . 15
123	122	a1i 9	. . . . . . . . . . . . . 14
124	10	recnd 8101	. . . . . . . . . . . . . . . 16
125	124	mulid2d 8091	. . . . . . . . . . . . . . 15
126	125	oveq2d 5960	. . . . . . . . . . . . . 14
127	123, 126	oveq12d 5962	. . . . . . . . . . . . 13
128	127	oveq1d 5959	. . . . . . . . . . . 12
129		binom2sub 10798	. . . . . . . . . . . . 13 $/\$
130	116, 124, 129	sylancr 414	. . . . . . . . . . . 12
131	98	recnd 8101	. . . . . . . . . . . . 13
132	16	recnd 8101	. . . . . . . . . . . . 13
133	115, 131, 132	addsubd 8404	. . . . . . . . . . . 12
134	128, 130, 133	3eqtr4d 2248	. . . . . . . . . . 11
135	134	oveq2d 5960	. . . . . . . . . 10
136		addcl 8050	. . . . . . . . . . . 12 $/\$
137	116, 131, 136	sylancr 414	. . . . . . . . . . 11
138	29, 137, 132	subdid 8486	. . . . . . . . . 10
139	29, 115, 131	adddid 8097	. . . . . . . . . . . . 13
140	116	2timesi 9166	. . . . . . . . . . . . . . 15
141	140	oveq1i 5954	. . . . . . . . . . . . . 14
142	115, 115, 117	addassd 8095	. . . . . . . . . . . . . 14
143	141, 142	eqtrid 2250	. . . . . . . . . . . . 13
144	139, 143	eqtrd 2238	. . . . . . . . . . . 12
145	29, 29, 124	mulassd 8096	. . . . . . . . . . . . 13
146	55	oveq1i 5954	. . . . . . . . . . . . 13
147	145, 146	eqtr3di 2253	. . . . . . . . . . . 12
148	144, 147	oveq12d 5962	. . . . . . . . . . 11
149	115, 119, 120, 148	assraddsubd 8440	. . . . . . . . . 10
150	135, 138, 149	3eqtrd 2242	. . . . . . . . 9
151	115, 121, 150	mvrladdd 8439	. . . . . . . 8
152		subcl 8271	. . . . . . . . . . 11 $/\$
153	116, 124, 152	sylancr 414	. . . . . . . . . 10
154	153, 115, 132	subdid 8486	. . . . . . . . 9
155	153	mulridd 8089	. . . . . . . . . 10
156	115, 124, 132	subdird 8487	. . . . . . . . . . 11
157	132	mulid2d 8091	. . . . . . . . . . . 12
158	124, 29, 124	mul12d 8224	. . . . . . . . . . . . 13
159	124	sqvald 10815	. . . . . . . . . . . . . 14
160	159	oveq2d 5960	. . . . . . . . . . . . 13
161	158, 160	eqtr4d 2241	. . . . . . . . . . . 12
162	157, 161	oveq12d 5962	. . . . . . . . . . 11
163	156, 162	eqtrd 2238	. . . . . . . . . 10
164	155, 163	oveq12d 5962	. . . . . . . . 9
165	115, 124, 132, 117	subadd4d 8431	. . . . . . . . . 10
166		df-3 9096	. . . . . . . . . . . . . 14
167	28, 116	addcomi 8216	. . . . . . . . . . . . . 14
168	166, 167	eqtri 2226	. . . . . . . . . . . . 13
169	168	oveq1i 5954	. . . . . . . . . . . 12
170	125	oveq1d 5959	. . . . . . . . . . . . 13
171	115, 124, 29, 170	joinlmuladdmuld 8100	. . . . . . . . . . . 12
172	169, 171	eqtrid 2250	. . . . . . . . . . 11
173	172	oveq2d 5960	. . . . . . . . . 10
174	165, 173	eqtr4d 2241	. . . . . . . . 9
175	154, 164, 174	3eqtrd 2242	. . . . . . . 8
176	114, 151, 175	3brtr4d 4076	. . . . . . 7
177	2, 25, 26, 91, 176	lttrd 8198	. . . . . 6
178		ltmul2 8929	. . . . . . 7 $/\$ $/\$ $/\$
179	2, 26, 1, 45, 178	syl112anc 1254	. . . . . 6
180	177, 179	mpbid 147	. . . . 5
181	18	recnd 8101	. . . . . 6
182	27, 153, 181	mulassd 8096	. . . . 5
183	180, 182	breqtrrd 4072	. . . 4
184	13, 38	remulcld 8103	. . . . 5
185	74	simpld 112	. . . . . 6
186	1, 12, 45, 83	mulgt0d 8195	. . . . . . 7
187		ltmul2 8929	. . . . . . 7 $/\$ $/\$ $/\$
188	18, 38, 13, 186, 187	syl112anc 1254	. . . . . 6
189	185, 188	mpbid 147	. . . . 5
190	29, 34, 153	mulassd 8096	. . . . . . . . 9
191	32	oveq1d 5959	. . . . . . . . 9
192	34, 115, 124	subdid 8486	. . . . . . . . . . 11
193	34	mulridd 8089	. . . . . . . . . . . 12
194	166	oveq2i 5955	. . . . . . . . . . . . . . . 16
195		2nn0 9312	. . . . . . . . . . . . . . . . 17
196		expp1 10691	. . . . . . . . . . . . . . . . 17 $/\$
197	34, 195, 196	sylancl 413	. . . . . . . . . . . . . . . 16
198	194, 197	eqtrid 2250	. . . . . . . . . . . . . . 15
199	7	recnd 8101	. . . . . . . . . . . . . . . 16
200	199, 34	mulcomd 8094	. . . . . . . . . . . . . . 15
201	198, 200	eqtrd 2238	. . . . . . . . . . . . . 14
202	201	oveq1d 5959	. . . . . . . . . . . . 13
203		3cn 9111	. . . . . . . . . . . . . . 15
204	203	a1i 9	. . . . . . . . . . . . . 14
205	104, 109	gt0ap0d 8702	. . . . . . . . . . . . . 14 #
206	34, 199, 204, 205	divassapd 8899	. . . . . . . . . . . . 13
207	202, 206	eqtr2d 2239	. . . . . . . . . . . 12
208	193, 207	oveq12d 5962	. . . . . . . . . . 11
209	192, 208	eqtrd 2238	. . . . . . . . . 10
210	209	oveq2d 5960	. . . . . . . . 9
211	190, 191, 210	3eqtr3d 2246	. . . . . . . 8
212		sin01bnd 12068	. . . . . . . . . . 11 $/\$
213	72, 212	syl 14	. . . . . . . . . 10 $/\$
214	213	simpld 112	. . . . . . . . 9
215		3nn0 9313	. . . . . . . . . . . . 13
216		reexpcl 10701	. . . . . . . . . . . . 13 $/\$
217	6, 215, 216	sylancl 413	. . . . . . . . . . . 12
218		nndivre 9072	. . . . . . . . . . . 12 $/\$
219	217, 8, 218	sylancl 413	. . . . . . . . . . 11
220	6, 219	resubcld 8453	. . . . . . . . . 10
221	6	resincld 12034	. . . . . . . . . 10
222		ltmul2 8929	. . . . . . . . . 10 $/\$ $/\$ $/\$
223	220, 221, 43, 47, 222	syl112anc 1254	. . . . . . . . 9
224	214, 223	mpbid 147	. . . . . . . 8
225	211, 224	eqbrtrd 4066	. . . . . . 7
226		remulcl 8053	. . . . . . . . 9 $/\$
227	14, 221, 226	sylancr 414	. . . . . . . 8
228		ltmul1 8665	. . . . . . . 8 $/\$ $/\$ $/\$
229	13, 227, 38, 77, 228	syl112anc 1254	. . . . . . 7
230	225, 229	mpbid 147	. . . . . 6
231	221	recnd 8101	. . . . . . . 8
232	38	recnd 8101	. . . . . . . 8
233	29, 231, 232	mulassd 8096	. . . . . . 7
234		sin2t 12060	. . . . . . . 8
235	34, 234	syl 14	. . . . . . 7
236	32	fveq2d 5580	. . . . . . 7
237	233, 235, 236	3eqtr2rd 2245	. . . . . 6
238	230, 237	breqtrrd 4072	. . . . 5
239	19, 184, 20, 189, 238	lttrd 8198	. . . 4
240	3, 19, 20, 183, 239	lttrd 8198	. . 3
241		sincosq1sgn 15298	. . . . 5 $/\$
242	241	simprd 114	. . . 4
243		ltmuldiv 8947	. . . 4 $/\$ $/\$ $/\$
244	1, 20, 2, 242, 243	syl112anc 1254	. . 3
245	240, 244	mpbid 147	. 2
246	2, 242	gt0ap0d 8702	. . 3 #
247		tanvalap 12019	. . 3 $/\$ #
248	27, 246, 247	syl2anc 411	. 2
249	245, 248	breqtrrd 4072	1

Colors of variables: wff set class

Syntax hints:

wi 4 $/\$ wa 104

wb 105 $/\$ w3a 981

wceq 1373

wcel 2176 class class class wbr 4044

cfv 5271 (class class class)co 5944

cc 7923

cr 7924

cc0 7925

c1 7926

caddc 7928

cmul 7930

cxr 8106

clt 8107

cle 8108

cmin 8243 # cap 8654

cdiv 8745

cn 9036

c2 9087

c3 9088

c4 9089

cn0 9295

cioo 10010

cioc 10011

cexp 10683

csin 11955

ccos 11956

ctan 11957

cpi 11958

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 615 ax-in2 616 ax-io 711 ax-5 1470 ax-7 1471 ax-gen 1472 ax-ie1 1516 ax-ie2 1517 ax-8 1527 ax-10 1528 ax-11 1529 ax-i12 1530 ax-bndl 1532 ax-4 1533 ax-17 1549 ax-i9 1553 ax-ial 1557 ax-i5r 1558 ax-13 2178 ax-14 2179 ax-ext 2187 ax-coll 4159 ax-sep 4162 ax-nul 4170 ax-pow 4218 ax-pr 4253 ax-un 4480 ax-setind 4585 ax-iinf 4636 ax-cnex 8016 ax-resscn 8017 ax-1cn 8018 ax-1re 8019 ax-icn 8020 ax-addcl 8021 ax-addrcl 8022 ax-mulcl 8023 ax-mulrcl 8024 ax-addcom 8025 ax-mulcom 8026 ax-addass 8027 ax-mulass 8028 ax-distr 8029 ax-i2m1 8030 ax-0lt1 8031 ax-1rid 8032 ax-0id 8033 ax-rnegex 8034 ax-precex 8035 ax-cnre 8036 ax-pre-ltirr 8037 ax-pre-ltwlin 8038 ax-pre-lttrn 8039 ax-pre-apti 8040 ax-pre-ltadd 8041 ax-pre-mulgt0 8042 ax-pre-mulext 8043 ax-arch 8044 ax-caucvg 8045 ax-pre-suploc 8046 ax-addf 8047 ax-mulf 8048

This theorem depends on definitions: df-bi 117 df-stab 833 df-dc 837 df-3or 982 df-3an 983 df-tru 1376 df-fal 1379 df-nf 1484 df-sb 1786 df-eu 2057 df-mo 2058 df-clab 2192 df-cleq 2198 df-clel 2201 df-nfc 2337 df-ne 2377 df-nel 2472 df-ral 2489 df-rex 2490 df-reu 2491 df-rmo 2492 df-rab 2493 df-v 2774 df-sbc 2999 df-csb 3094 df-dif 3168 df-un 3170 df-in 3172 df-ss 3179 df-nul 3461 df-if 3572 df-pw 3618 df-sn 3639 df-pr 3640 df-op 3642 df-uni 3851 df-int 3886 df-iun 3929 df-disj 4022 df-br 4045 df-opab 4106 df-mpt 4107 df-tr 4143 df-id 4340 df-po 4343 df-iso 4344 df-iord 4413 df-on 4415 df-ilim 4416 df-suc 4418 df-iom 4639 df-xp 4681 df-rel 4682 df-cnv 4683 df-co 4684 df-dm 4685 df-rn 4686 df-res 4687 df-ima 4688 df-iota 5232 df-fun 5273 df-fn 5274 df-f 5275 df-f1 5276 df-fo 5277 df-f1o 5278 df-fv 5279 df-isom 5280 df-riota 5899 df-ov 5947 df-oprab 5948 df-mpo 5949 df-of 6158 df-1st 6226 df-2nd 6227 df-recs 6391 df-irdg 6456 df-frec 6477 df-1o 6502 df-oadd 6506 df-er 6620 df-map 6737 df-pm 6738 df-en 6828 df-dom 6829 df-fin 6830 df-sup 7086 df-inf 7087 df-pnf 8109 df-mnf 8110 df-xr 8111 df-ltxr 8112 df-le 8113 df-sub 8245 df-neg 8246 df-reap 8648 df-ap 8655 df-div 8746 df-inn 9037 df-2 9095 df-3 9096 df-4 9097 df-5 9098 df-6 9099 df-7 9100 df-8 9101 df-9 9102 df-n0 9296 df-z 9373 df-uz 9649 df-q 9741 df-rp 9776 df-xneg 9894 df-xadd 9895 df-ioo 10014 df-ioc 10015 df-ico 10016 df-icc 10017 df-fz 10131 df-fzo 10265 df-seqfrec 10593 df-exp 10684 df-fac 10871 df-bc 10893 df-ihash 10921 df-shft 11126 df-cj 11153 df-re 11154 df-im 11155 df-rsqrt 11309 df-abs 11310 df-clim 11590 df-sumdc 11665 df-ef 11959 df-sin 11961 df-cos 11962 df-tan 11963 df-pi 11964 df-rest 13073 df-topgen 13092 df-psmet 14305 df-xmet 14306 df-met 14307 df-bl 14308 df-mopn 14309 df-top 14470 df-topon 14483 df-bases 14515 df-ntr 14568 df-cn 14660 df-cnp 14661 df-tx 14725 df-cncf 15043 df-limced 15128 df-dvap 15129

This theorem is referenced by: (None)

W3C validator