tangtx - Intuitionistic Logic Explorer

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

Theorem tangtx 12919

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 9695	. . . . 5
2	1	recoscld 11431	. . . . 5
3	1, 2	remulcld 7796	. . . 4
4		1re 7765	. . . . . . 7
5		rehalfcl 8947	. . . . . . . . . 10
6	1, 5	syl 14	. . . . . . . . 9
7	6	resqcld 10450	. . . . . . . 8
8		3nn 8882	. . . . . . . 8
9		nndivre 8756	. . . . . . . 8 $/\$
10	7, 8, 9	sylancl 409	. . . . . . 7
11		resubcl 8026	. . . . . . 7 $/\$
12	4, 10, 11	sylancr 410	. . . . . 6
13	1, 12	remulcld 7796	. . . . 5
14		2re 8790	. . . . . . 7
15		remulcl 7748	. . . . . . 7 $/\$
16	14, 10, 15	sylancr 410	. . . . . 6
17		resubcl 8026	. . . . . 6 $/\$
18	4, 16, 17	sylancr 410	. . . . 5
19	13, 18	remulcld 7796	. . . 4
20	1	resincld 11430	. . . 4
21	12	resqcld 10450	. . . . . . . . 9
22		remulcl 7748	. . . . . . . . 9 $/\$
23	14, 21, 22	sylancr 410	. . . . . . . 8
24		resubcl 8026	. . . . . . . 8 $/\$
25	23, 4, 24	sylancl 409	. . . . . . 7
26	12, 18	remulcld 7796	. . . . . . 7
27	1	recnd 7794	. . . . . . . . . . 11
28		2cn 8791	. . . . . . . . . . . 12
29	28	a1i 9	. . . . . . . . . . 11
30		2ap0 8813	. . . . . . . . . . . 12 #
31	30	a1i 9	. . . . . . . . . . 11 #
32	27, 29, 31	divcanap2d 8552	. . . . . . . . . 10
33	32	fveq2d 5425	. . . . . . . . 9
34	6	recnd 7794	. . . . . . . . . 10
35		cos2t 11457	. . . . . . . . . 10
36	34, 35	syl 14	. . . . . . . . 9
37	33, 36	eqtr3d 2174	. . . . . . . 8
38	6	recoscld 11431	. . . . . . . . . . 11
39	38	resqcld 10450	. . . . . . . . . 10
40		remulcl 7748	. . . . . . . . . 10 $/\$
41	14, 39, 40	sylancr 410	. . . . . . . . 9
42	4	a1i 9	. . . . . . . . 9
43	14	a1i 9	. . . . . . . . . . . . . . 15
44		eliooord 9711	. . . . . . . . . . . . . . . 16 $/\$
45	44	simpld 111	. . . . . . . . . . . . . . 15
46		2pos 8811	. . . . . . . . . . . . . . . 16
47	46	a1i 9	. . . . . . . . . . . . . . 15
48	1, 43, 45, 47	divgt0d 8693	. . . . . . . . . . . . . 14
49		pire 12867	. . . . . . . . . . . . . . . . . . 19
50		rehalfcl 8947	. . . . . . . . . . . . . . . . . . 19
51	49, 50	mp1i 10	. . . . . . . . . . . . . . . . . 18
52	44	simprd 113	. . . . . . . . . . . . . . . . . 18
53		pigt2lt4 12865	. . . . . . . . . . . . . . . . . . . . . 22 $/\$
54	53	simpri 112	. . . . . . . . . . . . . . . . . . . . 21
55		2t2e4 8874	. . . . . . . . . . . . . . . . . . . . 21
56	54, 55	breqtrri 3955	. . . . . . . . . . . . . . . . . . . 20
57	14, 46	pm3.2i 270	. . . . . . . . . . . . . . . . . . . . 21 $/\$
58		ltdivmul 8634	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$ $/\$
59	49, 14, 57, 58	mp3an 1315	. . . . . . . . . . . . . . . . . . . 20
60	56, 59	mpbir 145	. . . . . . . . . . . . . . . . . . 19
61	60	a1i 9	. . . . . . . . . . . . . . . . . 18
62	1, 51, 43, 52, 61	lttrd 7888	. . . . . . . . . . . . . . . . 17
63	28	mulid2i 7769	. . . . . . . . . . . . . . . . 17
64	62, 63	breqtrrdi 3970	. . . . . . . . . . . . . . . 16
65		ltdivmul2 8636	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$
66	1, 42, 43, 47, 65	syl112anc 1220	. . . . . . . . . . . . . . . 16
67	64, 66	mpbird 166	. . . . . . . . . . . . . . 15
68	6, 42, 67	ltled 7881	. . . . . . . . . . . . . 14
69		0xr 7812	. . . . . . . . . . . . . . 15
70		elioc2 9719	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$
71	69, 4, 70	mp2an 422	. . . . . . . . . . . . . 14 $/\$ $/\$
72	6, 48, 68, 71	syl3anbrc 1165	. . . . . . . . . . . . 13
73		cos01bnd 11465	. . . . . . . . . . . . 13 $/\$
74	72, 73	syl 14	. . . . . . . . . . . 12 $/\$
75	74	simprd 113	. . . . . . . . . . 11
76		cos01gt0 11469	. . . . . . . . . . . . . 14
77	72, 76	syl 14	. . . . . . . . . . . . 13
78		0re 7766	. . . . . . . . . . . . . 14
79		ltle 7851	. . . . . . . . . . . . . 14 $/\$
80	78, 38, 79	sylancr 410	. . . . . . . . . . . . 13
81	77, 80	mpd 13	. . . . . . . . . . . 12
82	78	a1i 9	. . . . . . . . . . . . 13
83	82, 38, 12, 77, 75	lttrd 7888	. . . . . . . . . . . . 13
84	82, 12, 83	ltled 7881	. . . . . . . . . . . 12
85	38, 12, 81, 84	lt2sqd 10455	. . . . . . . . . . 11
86	75, 85	mpbid 146	. . . . . . . . . 10
87		ltmul2 8614	. . . . . . . . . . 11 $/\$ $/\$ $/\$
88	39, 21, 43, 47, 87	syl112anc 1220	. . . . . . . . . 10
89	86, 88	mpbid 146	. . . . . . . . 9
90	41, 23, 42, 89	ltsub1dd 8319	. . . . . . . 8
91	37, 90	eqbrtrd 3950	. . . . . . 7
92		3re 8794	. . . . . . . . . 10
93		remulcl 7748	. . . . . . . . . 10 $/\$
94	92, 10, 93	sylancr 410	. . . . . . . . 9
95		4re 8797	. . . . . . . . . 10
96		remulcl 7748	. . . . . . . . . 10 $/\$
97	95, 10, 96	sylancr 410	. . . . . . . . 9
98	10	resqcld 10450	. . . . . . . . . . 11
99		remulcl 7748	. . . . . . . . . . 11 $/\$
100	14, 98, 99	sylancr 410	. . . . . . . . . 10
101		readdcl 7746	. . . . . . . . . 10 $/\$
102	4, 100, 101	sylancr 410	. . . . . . . . 9
103		3lt4 8892	. . . . . . . . . 10
104	92	a1i 9	. . . . . . . . . . 11
105	95	a1i 9	. . . . . . . . . . 11
106	6, 48	gt0ap0d 8391	. . . . . . . . . . . . 13 #
107	6, 106	sqgt0apd 10452	. . . . . . . . . . . 12
108		3pos 8814	. . . . . . . . . . . . 13
109	108	a1i 9	. . . . . . . . . . . 12
110	7, 104, 107, 109	divgt0d 8693	. . . . . . . . . . 11
111		ltmul1 8354	. . . . . . . . . . 11 $/\$ $/\$ $/\$
112	104, 105, 10, 110, 111	syl112anc 1220	. . . . . . . . . 10
113	103, 112	mpbii 147	. . . . . . . . 9
114	94, 97, 102, 113	ltsub2dd 8320	. . . . . . . 8
115	42	recnd 7794	. . . . . . . . 9
116		ax-1cn 7713	. . . . . . . . . . 11
117	100	recnd 7794	. . . . . . . . . . 11
118		addcl 7745	. . . . . . . . . . 11 $/\$
119	116, 117, 118	sylancr 410	. . . . . . . . . 10
120	97	recnd 7794	. . . . . . . . . 10
121	119, 120	subcld 8073	. . . . . . . . 9
122		sq1 10386	. . . . . . . . . . . . . . 15
123	122	a1i 9	. . . . . . . . . . . . . 14
124	10	recnd 7794	. . . . . . . . . . . . . . . 16
125	124	mulid2d 7784	. . . . . . . . . . . . . . 15
126	125	oveq2d 5790	. . . . . . . . . . . . . 14
127	123, 126	oveq12d 5792	. . . . . . . . . . . . 13
128	127	oveq1d 5789	. . . . . . . . . . . 12
129		binom2sub 10405	. . . . . . . . . . . . 13 $/\$
130	116, 124, 129	sylancr 410	. . . . . . . . . . . 12
131	98	recnd 7794	. . . . . . . . . . . . 13
132	16	recnd 7794	. . . . . . . . . . . . 13
133	115, 131, 132	addsubd 8094	. . . . . . . . . . . 12
134	128, 130, 133	3eqtr4d 2182	. . . . . . . . . . 11
135	134	oveq2d 5790	. . . . . . . . . 10
136		addcl 7745	. . . . . . . . . . . 12 $/\$
137	116, 131, 136	sylancr 410	. . . . . . . . . . 11
138	29, 137, 132	subdid 8176	. . . . . . . . . 10
139	29, 115, 131	adddid 7790	. . . . . . . . . . . . 13
140	116	2timesi 8850	. . . . . . . . . . . . . . 15
141	140	oveq1i 5784	. . . . . . . . . . . . . 14
142	115, 115, 117	addassd 7788	. . . . . . . . . . . . . 14
143	141, 142	syl5eq 2184	. . . . . . . . . . . . 13
144	139, 143	eqtrd 2172	. . . . . . . . . . . 12
145	55	oveq1i 5784	. . . . . . . . . . . . 13
146	29, 29, 124	mulassd 7789	. . . . . . . . . . . . 13
147	145, 146	syl5reqr 2187	. . . . . . . . . . . 12
148	144, 147	oveq12d 5792	. . . . . . . . . . 11
149	115, 119, 120, 148	assraddsubd 8130	. . . . . . . . . 10
150	135, 138, 149	3eqtrd 2176	. . . . . . . . 9
151	115, 121, 150	mvrladdd 8129	. . . . . . . 8
152		subcl 7961	. . . . . . . . . . 11 $/\$
153	116, 124, 152	sylancr 410	. . . . . . . . . 10
154	153, 115, 132	subdid 8176	. . . . . . . . 9
155	153	mulid1d 7783	. . . . . . . . . 10
156	115, 124, 132	subdird 8177	. . . . . . . . . . 11
157	132	mulid2d 7784	. . . . . . . . . . . 12
158	124, 29, 124	mul12d 7914	. . . . . . . . . . . . 13
159	124	sqvald 10421	. . . . . . . . . . . . . 14
160	159	oveq2d 5790	. . . . . . . . . . . . 13
161	158, 160	eqtr4d 2175	. . . . . . . . . . . 12
162	157, 161	oveq12d 5792	. . . . . . . . . . 11
163	156, 162	eqtrd 2172	. . . . . . . . . 10
164	155, 163	oveq12d 5792	. . . . . . . . 9
165	115, 124, 132, 117	subadd4d 8121	. . . . . . . . . 10
166		df-3 8780	. . . . . . . . . . . . . 14
167	28, 116	addcomi 7906	. . . . . . . . . . . . . 14
168	166, 167	eqtri 2160	. . . . . . . . . . . . 13
169	168	oveq1i 5784	. . . . . . . . . . . 12
170	125	oveq1d 5789	. . . . . . . . . . . . 13
171	115, 124, 29, 170	joinlmuladdmuld 7793	. . . . . . . . . . . 12
172	169, 171	syl5eq 2184	. . . . . . . . . . 11
173	172	oveq2d 5790	. . . . . . . . . 10
174	165, 173	eqtr4d 2175	. . . . . . . . 9
175	154, 164, 174	3eqtrd 2176	. . . . . . . 8
176	114, 151, 175	3brtr4d 3960	. . . . . . 7
177	2, 25, 26, 91, 176	lttrd 7888	. . . . . 6
178		ltmul2 8614	. . . . . . 7 $/\$ $/\$ $/\$
179	2, 26, 1, 45, 178	syl112anc 1220	. . . . . 6
180	177, 179	mpbid 146	. . . . 5
181	18	recnd 7794	. . . . . 6
182	27, 153, 181	mulassd 7789	. . . . 5
183	180, 182	breqtrrd 3956	. . . 4
184	13, 38	remulcld 7796	. . . . 5
185	74	simpld 111	. . . . . 6
186	1, 12, 45, 83	mulgt0d 7885	. . . . . . 7
187		ltmul2 8614	. . . . . . 7 $/\$ $/\$ $/\$
188	18, 38, 13, 186, 187	syl112anc 1220	. . . . . 6
189	185, 188	mpbid 146	. . . . 5
190	29, 34, 153	mulassd 7789	. . . . . . . . 9
191	32	oveq1d 5789	. . . . . . . . 9
192	34, 115, 124	subdid 8176	. . . . . . . . . . 11
193	34	mulid1d 7783	. . . . . . . . . . . 12
194	166	oveq2i 5785	. . . . . . . . . . . . . . . 16
195		2nn0 8994	. . . . . . . . . . . . . . . . 17
196		expp1 10300	. . . . . . . . . . . . . . . . 17 $/\$
197	34, 195, 196	sylancl 409	. . . . . . . . . . . . . . . 16
198	194, 197	syl5eq 2184	. . . . . . . . . . . . . . 15
199	7	recnd 7794	. . . . . . . . . . . . . . . 16
200	199, 34	mulcomd 7787	. . . . . . . . . . . . . . 15
201	198, 200	eqtrd 2172	. . . . . . . . . . . . . 14
202	201	oveq1d 5789	. . . . . . . . . . . . 13
203		3cn 8795	. . . . . . . . . . . . . . 15
204	203	a1i 9	. . . . . . . . . . . . . 14
205	104, 109	gt0ap0d 8391	. . . . . . . . . . . . . 14 #
206	34, 199, 204, 205	divassapd 8586	. . . . . . . . . . . . 13
207	202, 206	eqtr2d 2173	. . . . . . . . . . . 12
208	193, 207	oveq12d 5792	. . . . . . . . . . 11
209	192, 208	eqtrd 2172	. . . . . . . . . 10
210	209	oveq2d 5790	. . . . . . . . 9
211	190, 191, 210	3eqtr3d 2180	. . . . . . . 8
212		sin01bnd 11464	. . . . . . . . . . 11 $/\$
213	72, 212	syl 14	. . . . . . . . . 10 $/\$
214	213	simpld 111	. . . . . . . . 9
215		3nn0 8995	. . . . . . . . . . . . 13
216		reexpcl 10310	. . . . . . . . . . . . 13 $/\$
217	6, 215, 216	sylancl 409	. . . . . . . . . . . 12
218		nndivre 8756	. . . . . . . . . . . 12 $/\$
219	217, 8, 218	sylancl 409	. . . . . . . . . . 11
220	6, 219	resubcld 8143	. . . . . . . . . 10
221	6	resincld 11430	. . . . . . . . . 10
222		ltmul2 8614	. . . . . . . . . 10 $/\$ $/\$ $/\$
223	220, 221, 43, 47, 222	syl112anc 1220	. . . . . . . . 9
224	214, 223	mpbid 146	. . . . . . . 8
225	211, 224	eqbrtrd 3950	. . . . . . 7
226		remulcl 7748	. . . . . . . . 9 $/\$
227	14, 221, 226	sylancr 410	. . . . . . . 8
228		ltmul1 8354	. . . . . . . 8 $/\$ $/\$ $/\$
229	13, 227, 38, 77, 228	syl112anc 1220	. . . . . . 7
230	225, 229	mpbid 146	. . . . . 6
231	221	recnd 7794	. . . . . . . 8
232	38	recnd 7794	. . . . . . . 8
233	29, 231, 232	mulassd 7789	. . . . . . 7
234		sin2t 11456	. . . . . . . 8
235	34, 234	syl 14	. . . . . . 7
236	32	fveq2d 5425	. . . . . . 7
237	233, 235, 236	3eqtr2rd 2179	. . . . . 6
238	230, 237	breqtrrd 3956	. . . . 5
239	19, 184, 20, 189, 238	lttrd 7888	. . . 4
240	3, 19, 20, 183, 239	lttrd 7888	. . 3
241		sincosq1sgn 12907	. . . . 5 $/\$
242	241	simprd 113	. . . 4
243		ltmuldiv 8632	. . . 4 $/\$ $/\$ $/\$
244	1, 20, 2, 242, 243	syl112anc 1220	. . 3
245	240, 244	mpbid 146	. 2
246	2, 242	gt0ap0d 8391	. . 3 #
247		tanvalap 11415	. . 3 $/\$ #
248	27, 246, 247	syl2anc 408	. 2
249	245, 248	breqtrrd 3956	1

Colors of variables: wff set class

Syntax hints:

wi 4 $/\$ wa 103

wb 104 $/\$ w3a 962

wceq 1331

wcel 1480 class class class wbr 3929

cfv 5123 (class class class)co 5774

cc 7618

cr 7619

cc0 7620

c1 7621

caddc 7623

cmul 7625

cxr 7799

clt 7800

cle 7801

cmin 7933 # cap 8343

cdiv 8432

cn 8720

c2 8771

c3 8772

c4 8773

cn0 8977

cioo 9671

cioc 9672

cexp 10292

csin 11350

ccos 11351

ctan 11352

cpi 11353

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-ia1 105 ax-ia2 106 ax-ia3 107 ax-in1 603 ax-in2 604 ax-io 698 ax-5 1423 ax-7 1424 ax-gen 1425 ax-ie1 1469 ax-ie2 1470 ax-8 1482 ax-10 1483 ax-11 1484 ax-i12 1485 ax-bndl 1486 ax-4 1487 ax-13 1491 ax-14 1492 ax-17 1506 ax-i9 1510 ax-ial 1514 ax-i5r 1515 ax-ext 2121 ax-coll 4043 ax-sep 4046 ax-nul 4054 ax-pow 4098 ax-pr 4131 ax-un 4355 ax-setind 4452 ax-iinf 4502 ax-cnex 7711 ax-resscn 7712 ax-1cn 7713 ax-1re 7714 ax-icn 7715 ax-addcl 7716 ax-addrcl 7717 ax-mulcl 7718 ax-mulrcl 7719 ax-addcom 7720 ax-mulcom 7721 ax-addass 7722 ax-mulass 7723 ax-distr 7724 ax-i2m1 7725 ax-0lt1 7726 ax-1rid 7727 ax-0id 7728 ax-rnegex 7729 ax-precex 7730 ax-cnre 7731 ax-pre-ltirr 7732 ax-pre-ltwlin 7733 ax-pre-lttrn 7734 ax-pre-apti 7735 ax-pre-ltadd 7736 ax-pre-mulgt0 7737 ax-pre-mulext 7738 ax-arch 7739 ax-caucvg 7740 ax-pre-suploc 7741 ax-addf 7742 ax-mulf 7743

This theorem depends on definitions: df-bi 116 df-stab 816 df-dc 820 df-3or 963 df-3an 964 df-tru 1334 df-fal 1337 df-nf 1437 df-sb 1736 df-eu 2002 df-mo 2003 df-clab 2126 df-cleq 2132 df-clel 2135 df-nfc 2270 df-ne 2309 df-nel 2404 df-ral 2421 df-rex 2422 df-reu 2423 df-rmo 2424 df-rab 2425 df-v 2688 df-sbc 2910 df-csb 3004 df-dif 3073 df-un 3075 df-in 3077 df-ss 3084 df-nul 3364 df-if 3475 df-pw 3512 df-sn 3533 df-pr 3534 df-op 3536 df-uni 3737 df-int 3772 df-iun 3815 df-disj 3907 df-br 3930 df-opab 3990 df-mpt 3991 df-tr 4027 df-id 4215 df-po 4218 df-iso 4219 df-iord 4288 df-on 4290 df-ilim 4291 df-suc 4293 df-iom 4505 df-xp 4545 df-rel 4546 df-cnv 4547 df-co 4548 df-dm 4549 df-rn 4550 df-res 4551 df-ima 4552 df-iota 5088 df-fun 5125 df-fn 5126 df-f 5127 df-f1 5128 df-fo 5129 df-f1o 5130 df-fv 5131 df-isom 5132 df-riota 5730 df-ov 5777 df-oprab 5778 df-mpo 5779 df-of 5982 df-1st 6038 df-2nd 6039 df-recs 6202 df-irdg 6267 df-frec 6288 df-1o 6313 df-oadd 6317 df-er 6429 df-map 6544 df-pm 6545 df-en 6635 df-dom 6636 df-fin 6637 df-sup 6871 df-inf 6872 df-pnf 7802 df-mnf 7803 df-xr 7804 df-ltxr 7805 df-le 7806 df-sub 7935 df-neg 7936 df-reap 8337 df-ap 8344 df-div 8433 df-inn 8721 df-2 8779 df-3 8780 df-4 8781 df-5 8782 df-6 8783 df-7 8784 df-8 8785 df-9 8786 df-n0 8978 df-z 9055 df-uz 9327 df-q 9412 df-rp 9442 df-xneg 9559 df-xadd 9560 df-ioo 9675 df-ioc 9676 df-ico 9677 df-icc 9678 df-fz 9791 df-fzo 9920 df-seqfrec 10219 df-exp 10293 df-fac 10472 df-bc 10494 df-ihash 10522 df-shft 10587 df-cj 10614 df-re 10615 df-im 10616 df-rsqrt 10770 df-abs 10771 df-clim 11048 df-sumdc 11123 df-ef 11354 df-sin 11356 df-cos 11357 df-tan 11358 df-pi 11359 df-rest 12122 df-topgen 12141 df-psmet 12156 df-xmet 12157 df-met 12158 df-bl 12159 df-mopn 12160 df-top 12165 df-topon 12178 df-bases 12210 df-ntr 12265 df-cn 12357 df-cnp 12358 df-tx 12422 df-cncf 12727 df-limced 12794 df-dvap 12795

This theorem is referenced by: (None)

W3C validator