tangtx - Intuitionistic Logic Explorer

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

Theorem tangtx 14344

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 9914	. . . . 5
2	1	recoscld 11734	. . . . 5
3	1, 2	remulcld 7990	. . . 4
4		1re 7958	. . . . . . 7
5		rehalfcl 9148	. . . . . . . . . 10
6	1, 5	syl 14	. . . . . . . . 9
7	6	resqcld 10682	. . . . . . . 8
8		3nn 9083	. . . . . . . 8
9		nndivre 8957	. . . . . . . 8 $/\$
10	7, 8, 9	sylancl 413	. . . . . . 7
11		resubcl 8223	. . . . . . 7 $/\$
12	4, 10, 11	sylancr 414	. . . . . 6
13	1, 12	remulcld 7990	. . . . 5
14		2re 8991	. . . . . . 7
15		remulcl 7941	. . . . . . 7 $/\$
16	14, 10, 15	sylancr 414	. . . . . 6
17		resubcl 8223	. . . . . 6 $/\$
18	4, 16, 17	sylancr 414	. . . . 5
19	13, 18	remulcld 7990	. . . 4
20	1	resincld 11733	. . . 4
21	12	resqcld 10682	. . . . . . . . 9
22		remulcl 7941	. . . . . . . . 9 $/\$
23	14, 21, 22	sylancr 414	. . . . . . . 8
24		resubcl 8223	. . . . . . . 8 $/\$
25	23, 4, 24	sylancl 413	. . . . . . 7
26	12, 18	remulcld 7990	. . . . . . 7
27	1	recnd 7988	. . . . . . . . . . 11
28		2cn 8992	. . . . . . . . . . . 12
29	28	a1i 9	. . . . . . . . . . 11
30		2ap0 9014	. . . . . . . . . . . 12 #
31	30	a1i 9	. . . . . . . . . . 11 #
32	27, 29, 31	divcanap2d 8751	. . . . . . . . . 10
33	32	fveq2d 5521	. . . . . . . . 9
34	6	recnd 7988	. . . . . . . . . 10
35		cos2t 11760	. . . . . . . . . 10
36	34, 35	syl 14	. . . . . . . . 9
37	33, 36	eqtr3d 2212	. . . . . . . 8
38	6	recoscld 11734	. . . . . . . . . . 11
39	38	resqcld 10682	. . . . . . . . . 10
40		remulcl 7941	. . . . . . . . . 10 $/\$
41	14, 39, 40	sylancr 414	. . . . . . . . 9
42	4	a1i 9	. . . . . . . . 9
43	14	a1i 9	. . . . . . . . . . . . . . 15
44		eliooord 9930	. . . . . . . . . . . . . . . 16 $/\$
45	44	simpld 112	. . . . . . . . . . . . . . 15
46		2pos 9012	. . . . . . . . . . . . . . . 16
47	46	a1i 9	. . . . . . . . . . . . . . 15
48	1, 43, 45, 47	divgt0d 8894	. . . . . . . . . . . . . 14
49		pire 14292	. . . . . . . . . . . . . . . . . . 19
50		rehalfcl 9148	. . . . . . . . . . . . . . . . . . 19
51	49, 50	mp1i 10	. . . . . . . . . . . . . . . . . 18
52	44	simprd 114	. . . . . . . . . . . . . . . . . 18
53		pigt2lt4 14290	. . . . . . . . . . . . . . . . . . . . . 22 $/\$
54	53	simpri 113	. . . . . . . . . . . . . . . . . . . . 21
55		2t2e4 9075	. . . . . . . . . . . . . . . . . . . . 21
56	54, 55	breqtrri 4032	. . . . . . . . . . . . . . . . . . . 20
57	14, 46	pm3.2i 272	. . . . . . . . . . . . . . . . . . . . 21 $/\$
58		ltdivmul 8835	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$ $/\$
59	49, 14, 57, 58	mp3an 1337	. . . . . . . . . . . . . . . . . . . 20
60	56, 59	mpbir 146	. . . . . . . . . . . . . . . . . . 19
61	60	a1i 9	. . . . . . . . . . . . . . . . . 18
62	1, 51, 43, 52, 61	lttrd 8085	. . . . . . . . . . . . . . . . 17
63	28	mullidi 7962	. . . . . . . . . . . . . . . . 17
64	62, 63	breqtrrdi 4047	. . . . . . . . . . . . . . . 16
65		ltdivmul2 8837	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$
66	1, 42, 43, 47, 65	syl112anc 1242	. . . . . . . . . . . . . . . 16
67	64, 66	mpbird 167	. . . . . . . . . . . . . . 15
68	6, 42, 67	ltled 8078	. . . . . . . . . . . . . 14
69		0xr 8006	. . . . . . . . . . . . . . 15
70		elioc2 9938	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$
71	69, 4, 70	mp2an 426	. . . . . . . . . . . . . 14 $/\$ $/\$
72	6, 48, 68, 71	syl3anbrc 1181	. . . . . . . . . . . . 13
73		cos01bnd 11768	. . . . . . . . . . . . 13 $/\$
74	72, 73	syl 14	. . . . . . . . . . . 12 $/\$
75	74	simprd 114	. . . . . . . . . . 11
76		cos01gt0 11772	. . . . . . . . . . . . . 14
77	72, 76	syl 14	. . . . . . . . . . . . 13
78		0re 7959	. . . . . . . . . . . . . 14
79		ltle 8047	. . . . . . . . . . . . . 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 8085	. . . . . . . . . . . . 13
84	82, 12, 83	ltled 8078	. . . . . . . . . . . 12
85	38, 12, 81, 84	lt2sqd 10687	. . . . . . . . . . 11
86	75, 85	mpbid 147	. . . . . . . . . 10
87		ltmul2 8815	. . . . . . . . . . 11 $/\$ $/\$ $/\$
88	39, 21, 43, 47, 87	syl112anc 1242	. . . . . . . . . 10
89	86, 88	mpbid 147	. . . . . . . . 9
90	41, 23, 42, 89	ltsub1dd 8516	. . . . . . . 8
91	37, 90	eqbrtrd 4027	. . . . . . 7
92		3re 8995	. . . . . . . . . 10
93		remulcl 7941	. . . . . . . . . 10 $/\$
94	92, 10, 93	sylancr 414	. . . . . . . . 9
95		4re 8998	. . . . . . . . . 10
96		remulcl 7941	. . . . . . . . . 10 $/\$
97	95, 10, 96	sylancr 414	. . . . . . . . 9
98	10	resqcld 10682	. . . . . . . . . . 11
99		remulcl 7941	. . . . . . . . . . 11 $/\$
100	14, 98, 99	sylancr 414	. . . . . . . . . 10
101		readdcl 7939	. . . . . . . . . 10 $/\$
102	4, 100, 101	sylancr 414	. . . . . . . . 9
103		3lt4 9093	. . . . . . . . . 10
104	92	a1i 9	. . . . . . . . . . 11
105	95	a1i 9	. . . . . . . . . . 11
106	6, 48	gt0ap0d 8588	. . . . . . . . . . . . 13 #
107	6, 106	sqgt0apd 10684	. . . . . . . . . . . 12
108		3pos 9015	. . . . . . . . . . . . 13
109	108	a1i 9	. . . . . . . . . . . 12
110	7, 104, 107, 109	divgt0d 8894	. . . . . . . . . . 11
111		ltmul1 8551	. . . . . . . . . . 11 $/\$ $/\$ $/\$
112	104, 105, 10, 110, 111	syl112anc 1242	. . . . . . . . . 10
113	103, 112	mpbii 148	. . . . . . . . 9
114	94, 97, 102, 113	ltsub2dd 8517	. . . . . . . 8
115	42	recnd 7988	. . . . . . . . 9
116		ax-1cn 7906	. . . . . . . . . . 11
117	100	recnd 7988	. . . . . . . . . . 11
118		addcl 7938	. . . . . . . . . . 11 $/\$
119	116, 117, 118	sylancr 414	. . . . . . . . . 10
120	97	recnd 7988	. . . . . . . . . 10
121	119, 120	subcld 8270	. . . . . . . . 9
122		sq1 10616	. . . . . . . . . . . . . . 15
123	122	a1i 9	. . . . . . . . . . . . . 14
124	10	recnd 7988	. . . . . . . . . . . . . . . 16
125	124	mulid2d 7978	. . . . . . . . . . . . . . 15
126	125	oveq2d 5893	. . . . . . . . . . . . . 14
127	123, 126	oveq12d 5895	. . . . . . . . . . . . 13
128	127	oveq1d 5892	. . . . . . . . . . . 12
129		binom2sub 10636	. . . . . . . . . . . . 13 $/\$
130	116, 124, 129	sylancr 414	. . . . . . . . . . . 12
131	98	recnd 7988	. . . . . . . . . . . . 13
132	16	recnd 7988	. . . . . . . . . . . . 13
133	115, 131, 132	addsubd 8291	. . . . . . . . . . . 12
134	128, 130, 133	3eqtr4d 2220	. . . . . . . . . . 11
135	134	oveq2d 5893	. . . . . . . . . 10
136		addcl 7938	. . . . . . . . . . . 12 $/\$
137	116, 131, 136	sylancr 414	. . . . . . . . . . 11
138	29, 137, 132	subdid 8373	. . . . . . . . . 10
139	29, 115, 131	adddid 7984	. . . . . . . . . . . . 13
140	116	2timesi 9051	. . . . . . . . . . . . . . 15
141	140	oveq1i 5887	. . . . . . . . . . . . . 14
142	115, 115, 117	addassd 7982	. . . . . . . . . . . . . 14
143	141, 142	eqtrid 2222	. . . . . . . . . . . . 13
144	139, 143	eqtrd 2210	. . . . . . . . . . . 12
145	29, 29, 124	mulassd 7983	. . . . . . . . . . . . 13
146	55	oveq1i 5887	. . . . . . . . . . . . 13
147	145, 146	eqtr3di 2225	. . . . . . . . . . . 12
148	144, 147	oveq12d 5895	. . . . . . . . . . 11
149	115, 119, 120, 148	assraddsubd 8327	. . . . . . . . . 10
150	135, 138, 149	3eqtrd 2214	. . . . . . . . 9
151	115, 121, 150	mvrladdd 8326	. . . . . . . 8
152		subcl 8158	. . . . . . . . . . 11 $/\$
153	116, 124, 152	sylancr 414	. . . . . . . . . 10
154	153, 115, 132	subdid 8373	. . . . . . . . 9
155	153	mulridd 7976	. . . . . . . . . 10
156	115, 124, 132	subdird 8374	. . . . . . . . . . 11
157	132	mulid2d 7978	. . . . . . . . . . . 12
158	124, 29, 124	mul12d 8111	. . . . . . . . . . . . 13
159	124	sqvald 10653	. . . . . . . . . . . . . 14
160	159	oveq2d 5893	. . . . . . . . . . . . 13
161	158, 160	eqtr4d 2213	. . . . . . . . . . . 12
162	157, 161	oveq12d 5895	. . . . . . . . . . 11
163	156, 162	eqtrd 2210	. . . . . . . . . 10
164	155, 163	oveq12d 5895	. . . . . . . . 9
165	115, 124, 132, 117	subadd4d 8318	. . . . . . . . . 10
166		df-3 8981	. . . . . . . . . . . . . 14
167	28, 116	addcomi 8103	. . . . . . . . . . . . . 14
168	166, 167	eqtri 2198	. . . . . . . . . . . . 13
169	168	oveq1i 5887	. . . . . . . . . . . 12
170	125	oveq1d 5892	. . . . . . . . . . . . 13
171	115, 124, 29, 170	joinlmuladdmuld 7987	. . . . . . . . . . . 12
172	169, 171	eqtrid 2222	. . . . . . . . . . 11
173	172	oveq2d 5893	. . . . . . . . . 10
174	165, 173	eqtr4d 2213	. . . . . . . . 9
175	154, 164, 174	3eqtrd 2214	. . . . . . . 8
176	114, 151, 175	3brtr4d 4037	. . . . . . 7
177	2, 25, 26, 91, 176	lttrd 8085	. . . . . 6
178		ltmul2 8815	. . . . . . 7 $/\$ $/\$ $/\$
179	2, 26, 1, 45, 178	syl112anc 1242	. . . . . 6
180	177, 179	mpbid 147	. . . . 5
181	18	recnd 7988	. . . . . 6
182	27, 153, 181	mulassd 7983	. . . . 5
183	180, 182	breqtrrd 4033	. . . 4
184	13, 38	remulcld 7990	. . . . 5
185	74	simpld 112	. . . . . 6
186	1, 12, 45, 83	mulgt0d 8082	. . . . . . 7
187		ltmul2 8815	. . . . . . 7 $/\$ $/\$ $/\$
188	18, 38, 13, 186, 187	syl112anc 1242	. . . . . 6
189	185, 188	mpbid 147	. . . . 5
190	29, 34, 153	mulassd 7983	. . . . . . . . 9
191	32	oveq1d 5892	. . . . . . . . 9
192	34, 115, 124	subdid 8373	. . . . . . . . . . 11
193	34	mulridd 7976	. . . . . . . . . . . 12
194	166	oveq2i 5888	. . . . . . . . . . . . . . . 16
195		2nn0 9195	. . . . . . . . . . . . . . . . 17
196		expp1 10529	. . . . . . . . . . . . . . . . 17 $/\$
197	34, 195, 196	sylancl 413	. . . . . . . . . . . . . . . 16
198	194, 197	eqtrid 2222	. . . . . . . . . . . . . . 15
199	7	recnd 7988	. . . . . . . . . . . . . . . 16
200	199, 34	mulcomd 7981	. . . . . . . . . . . . . . 15
201	198, 200	eqtrd 2210	. . . . . . . . . . . . . 14
202	201	oveq1d 5892	. . . . . . . . . . . . 13
203		3cn 8996	. . . . . . . . . . . . . . 15
204	203	a1i 9	. . . . . . . . . . . . . 14
205	104, 109	gt0ap0d 8588	. . . . . . . . . . . . . 14 #
206	34, 199, 204, 205	divassapd 8785	. . . . . . . . . . . . 13
207	202, 206	eqtr2d 2211	. . . . . . . . . . . 12
208	193, 207	oveq12d 5895	. . . . . . . . . . 11
209	192, 208	eqtrd 2210	. . . . . . . . . 10
210	209	oveq2d 5893	. . . . . . . . 9
211	190, 191, 210	3eqtr3d 2218	. . . . . . . 8
212		sin01bnd 11767	. . . . . . . . . . 11 $/\$
213	72, 212	syl 14	. . . . . . . . . 10 $/\$
214	213	simpld 112	. . . . . . . . 9
215		3nn0 9196	. . . . . . . . . . . . 13
216		reexpcl 10539	. . . . . . . . . . . . 13 $/\$
217	6, 215, 216	sylancl 413	. . . . . . . . . . . 12
218		nndivre 8957	. . . . . . . . . . . 12 $/\$
219	217, 8, 218	sylancl 413	. . . . . . . . . . 11
220	6, 219	resubcld 8340	. . . . . . . . . 10
221	6	resincld 11733	. . . . . . . . . 10
222		ltmul2 8815	. . . . . . . . . 10 $/\$ $/\$ $/\$
223	220, 221, 43, 47, 222	syl112anc 1242	. . . . . . . . 9
224	214, 223	mpbid 147	. . . . . . . 8
225	211, 224	eqbrtrd 4027	. . . . . . 7
226		remulcl 7941	. . . . . . . . 9 $/\$
227	14, 221, 226	sylancr 414	. . . . . . . 8
228		ltmul1 8551	. . . . . . . 8 $/\$ $/\$ $/\$
229	13, 227, 38, 77, 228	syl112anc 1242	. . . . . . 7
230	225, 229	mpbid 147	. . . . . 6
231	221	recnd 7988	. . . . . . . 8
232	38	recnd 7988	. . . . . . . 8
233	29, 231, 232	mulassd 7983	. . . . . . 7
234		sin2t 11759	. . . . . . . 8
235	34, 234	syl 14	. . . . . . 7
236	32	fveq2d 5521	. . . . . . 7
237	233, 235, 236	3eqtr2rd 2217	. . . . . 6
238	230, 237	breqtrrd 4033	. . . . 5
239	19, 184, 20, 189, 238	lttrd 8085	. . . 4
240	3, 19, 20, 183, 239	lttrd 8085	. . 3
241		sincosq1sgn 14332	. . . . 5 $/\$
242	241	simprd 114	. . . 4
243		ltmuldiv 8833	. . . 4 $/\$ $/\$ $/\$
244	1, 20, 2, 242, 243	syl112anc 1242	. . 3
245	240, 244	mpbid 147	. 2
246	2, 242	gt0ap0d 8588	. . 3 #
247		tanvalap 11718	. . 3 $/\$ #
248	27, 246, 247	syl2anc 411	. 2
249	245, 248	breqtrrd 4033	1

Colors of variables: wff set class

Syntax hints:

wi 4 $/\$ wa 104

wb 105 $/\$ w3a 978

wceq 1353

wcel 2148 class class class wbr 4005

cfv 5218 (class class class)co 5877

cc 7811

cr 7812

cc0 7813

c1 7814

caddc 7816

cmul 7818

cxr 7993

clt 7994

cle 7995

cmin 8130 # cap 8540

cdiv 8631

cn 8921

c2 8972

c3 8973

c4 8974

cn0 9178

cioo 9890

cioc 9891

cexp 10521

csin 11654

ccos 11655

ctan 11656

cpi 11657

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 614 ax-in2 615 ax-io 709 ax-5 1447 ax-7 1448 ax-gen 1449 ax-ie1 1493 ax-ie2 1494 ax-8 1504 ax-10 1505 ax-11 1506 ax-i12 1507 ax-bndl 1509 ax-4 1510 ax-17 1526 ax-i9 1530 ax-ial 1534 ax-i5r 1535 ax-13 2150 ax-14 2151 ax-ext 2159 ax-coll 4120 ax-sep 4123 ax-nul 4131 ax-pow 4176 ax-pr 4211 ax-un 4435 ax-setind 4538 ax-iinf 4589 ax-cnex 7904 ax-resscn 7905 ax-1cn 7906 ax-1re 7907 ax-icn 7908 ax-addcl 7909 ax-addrcl 7910 ax-mulcl 7911 ax-mulrcl 7912 ax-addcom 7913 ax-mulcom 7914 ax-addass 7915 ax-mulass 7916 ax-distr 7917 ax-i2m1 7918 ax-0lt1 7919 ax-1rid 7920 ax-0id 7921 ax-rnegex 7922 ax-precex 7923 ax-cnre 7924 ax-pre-ltirr 7925 ax-pre-ltwlin 7926 ax-pre-lttrn 7927 ax-pre-apti 7928 ax-pre-ltadd 7929 ax-pre-mulgt0 7930 ax-pre-mulext 7931 ax-arch 7932 ax-caucvg 7933 ax-pre-suploc 7934 ax-addf 7935 ax-mulf 7936

This theorem depends on definitions: df-bi 117 df-stab 831 df-dc 835 df-3or 979 df-3an 980 df-tru 1356 df-fal 1359 df-nf 1461 df-sb 1763 df-eu 2029 df-mo 2030 df-clab 2164 df-cleq 2170 df-clel 2173 df-nfc 2308 df-ne 2348 df-nel 2443 df-ral 2460 df-rex 2461 df-reu 2462 df-rmo 2463 df-rab 2464 df-v 2741 df-sbc 2965 df-csb 3060 df-dif 3133 df-un 3135 df-in 3137 df-ss 3144 df-nul 3425 df-if 3537 df-pw 3579 df-sn 3600 df-pr 3601 df-op 3603 df-uni 3812 df-int 3847 df-iun 3890 df-disj 3983 df-br 4006 df-opab 4067 df-mpt 4068 df-tr 4104 df-id 4295 df-po 4298 df-iso 4299 df-iord 4368 df-on 4370 df-ilim 4371 df-suc 4373 df-iom 4592 df-xp 4634 df-rel 4635 df-cnv 4636 df-co 4637 df-dm 4638 df-rn 4639 df-res 4640 df-ima 4641 df-iota 5180 df-fun 5220 df-fn 5221 df-f 5222 df-f1 5223 df-fo 5224 df-f1o 5225 df-fv 5226 df-isom 5227 df-riota 5833 df-ov 5880 df-oprab 5881 df-mpo 5882 df-of 6085 df-1st 6143 df-2nd 6144 df-recs 6308 df-irdg 6373 df-frec 6394 df-1o 6419 df-oadd 6423 df-er 6537 df-map 6652 df-pm 6653 df-en 6743 df-dom 6744 df-fin 6745 df-sup 6985 df-inf 6986 df-pnf 7996 df-mnf 7997 df-xr 7998 df-ltxr 7999 df-le 8000 df-sub 8132 df-neg 8133 df-reap 8534 df-ap 8541 df-div 8632 df-inn 8922 df-2 8980 df-3 8981 df-4 8982 df-5 8983 df-6 8984 df-7 8985 df-8 8986 df-9 8987 df-n0 9179 df-z 9256 df-uz 9531 df-q 9622 df-rp 9656 df-xneg 9774 df-xadd 9775 df-ioo 9894 df-ioc 9895 df-ico 9896 df-icc 9897 df-fz 10011 df-fzo 10145 df-seqfrec 10448 df-exp 10522 df-fac 10708 df-bc 10730 df-ihash 10758 df-shft 10826 df-cj 10853 df-re 10854 df-im 10855 df-rsqrt 11009 df-abs 11010 df-clim 11289 df-sumdc 11364 df-ef 11658 df-sin 11660 df-cos 11661 df-tan 11662 df-pi 11663 df-rest 12695 df-topgen 12714 df-psmet 13532 df-xmet 13533 df-met 13534 df-bl 13535 df-mopn 13536 df-top 13583 df-topon 13596 df-bases 13628 df-ntr 13681 df-cn 13773 df-cnp 13774 df-tx 13838 df-cncf 14143 df-limced 14210 df-dvap 14211

This theorem is referenced by: (None)

W3C validator