tangtx - Intuitionistic Logic Explorer

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

Theorem tangtx 13553

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 9869	. . . . 5
2	1	recoscld 11687	. . . . 5
3	1, 2	remulcld 7950	. . . 4
4		1re 7919	. . . . . . 7
5		rehalfcl 9105	. . . . . . . . . 10
6	1, 5	syl 14	. . . . . . . . 9
7	6	resqcld 10635	. . . . . . . 8
8		3nn 9040	. . . . . . . 8
9		nndivre 8914	. . . . . . . 8 $/\$
10	7, 8, 9	sylancl 411	. . . . . . 7
11		resubcl 8183	. . . . . . 7 $/\$
12	4, 10, 11	sylancr 412	. . . . . 6
13	1, 12	remulcld 7950	. . . . 5
14		2re 8948	. . . . . . 7
15		remulcl 7902	. . . . . . 7 $/\$
16	14, 10, 15	sylancr 412	. . . . . 6
17		resubcl 8183	. . . . . 6 $/\$
18	4, 16, 17	sylancr 412	. . . . 5
19	13, 18	remulcld 7950	. . . 4
20	1	resincld 11686	. . . 4
21	12	resqcld 10635	. . . . . . . . 9
22		remulcl 7902	. . . . . . . . 9 $/\$
23	14, 21, 22	sylancr 412	. . . . . . . 8
24		resubcl 8183	. . . . . . . 8 $/\$
25	23, 4, 24	sylancl 411	. . . . . . 7
26	12, 18	remulcld 7950	. . . . . . 7
27	1	recnd 7948	. . . . . . . . . . 11
28		2cn 8949	. . . . . . . . . . . 12
29	28	a1i 9	. . . . . . . . . . 11
30		2ap0 8971	. . . . . . . . . . . 12 #
31	30	a1i 9	. . . . . . . . . . 11 #
32	27, 29, 31	divcanap2d 8709	. . . . . . . . . 10
33	32	fveq2d 5500	. . . . . . . . 9
34	6	recnd 7948	. . . . . . . . . 10
35		cos2t 11713	. . . . . . . . . 10
36	34, 35	syl 14	. . . . . . . . 9
37	33, 36	eqtr3d 2205	. . . . . . . 8
38	6	recoscld 11687	. . . . . . . . . . 11
39	38	resqcld 10635	. . . . . . . . . 10
40		remulcl 7902	. . . . . . . . . 10 $/\$
41	14, 39, 40	sylancr 412	. . . . . . . . 9
42	4	a1i 9	. . . . . . . . 9
43	14	a1i 9	. . . . . . . . . . . . . . 15
44		eliooord 9885	. . . . . . . . . . . . . . . 16 $/\$
45	44	simpld 111	. . . . . . . . . . . . . . 15
46		2pos 8969	. . . . . . . . . . . . . . . 16
47	46	a1i 9	. . . . . . . . . . . . . . 15
48	1, 43, 45, 47	divgt0d 8851	. . . . . . . . . . . . . 14
49		pire 13501	. . . . . . . . . . . . . . . . . . 19
50		rehalfcl 9105	. . . . . . . . . . . . . . . . . . 19
51	49, 50	mp1i 10	. . . . . . . . . . . . . . . . . 18
52	44	simprd 113	. . . . . . . . . . . . . . . . . 18
53		pigt2lt4 13499	. . . . . . . . . . . . . . . . . . . . . 22 $/\$
54	53	simpri 112	. . . . . . . . . . . . . . . . . . . . 21
55		2t2e4 9032	. . . . . . . . . . . . . . . . . . . . 21
56	54, 55	breqtrri 4016	. . . . . . . . . . . . . . . . . . . 20
57	14, 46	pm3.2i 270	. . . . . . . . . . . . . . . . . . . . 21 $/\$
58		ltdivmul 8792	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$ $/\$
59	49, 14, 57, 58	mp3an 1332	. . . . . . . . . . . . . . . . . . . 20
60	56, 59	mpbir 145	. . . . . . . . . . . . . . . . . . 19
61	60	a1i 9	. . . . . . . . . . . . . . . . . 18
62	1, 51, 43, 52, 61	lttrd 8045	. . . . . . . . . . . . . . . . 17
63	28	mulid2i 7923	. . . . . . . . . . . . . . . . 17
64	62, 63	breqtrrdi 4031	. . . . . . . . . . . . . . . 16
65		ltdivmul2 8794	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$
66	1, 42, 43, 47, 65	syl112anc 1237	. . . . . . . . . . . . . . . 16
67	64, 66	mpbird 166	. . . . . . . . . . . . . . 15
68	6, 42, 67	ltled 8038	. . . . . . . . . . . . . 14
69		0xr 7966	. . . . . . . . . . . . . . 15
70		elioc2 9893	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$
71	69, 4, 70	mp2an 424	. . . . . . . . . . . . . 14 $/\$ $/\$
72	6, 48, 68, 71	syl3anbrc 1176	. . . . . . . . . . . . 13
73		cos01bnd 11721	. . . . . . . . . . . . 13 $/\$
74	72, 73	syl 14	. . . . . . . . . . . 12 $/\$
75	74	simprd 113	. . . . . . . . . . 11
76		cos01gt0 11725	. . . . . . . . . . . . . 14
77	72, 76	syl 14	. . . . . . . . . . . . 13
78		0re 7920	. . . . . . . . . . . . . 14
79		ltle 8007	. . . . . . . . . . . . . 14 $/\$
80	78, 38, 79	sylancr 412	. . . . . . . . . . . . 13
81	77, 80	mpd 13	. . . . . . . . . . . 12
82	78	a1i 9	. . . . . . . . . . . . 13
83	82, 38, 12, 77, 75	lttrd 8045	. . . . . . . . . . . . 13
84	82, 12, 83	ltled 8038	. . . . . . . . . . . 12
85	38, 12, 81, 84	lt2sqd 10640	. . . . . . . . . . 11
86	75, 85	mpbid 146	. . . . . . . . . 10
87		ltmul2 8772	. . . . . . . . . . 11 $/\$ $/\$ $/\$
88	39, 21, 43, 47, 87	syl112anc 1237	. . . . . . . . . 10
89	86, 88	mpbid 146	. . . . . . . . 9
90	41, 23, 42, 89	ltsub1dd 8476	. . . . . . . 8
91	37, 90	eqbrtrd 4011	. . . . . . 7
92		3re 8952	. . . . . . . . . 10
93		remulcl 7902	. . . . . . . . . 10 $/\$
94	92, 10, 93	sylancr 412	. . . . . . . . 9
95		4re 8955	. . . . . . . . . 10
96		remulcl 7902	. . . . . . . . . 10 $/\$
97	95, 10, 96	sylancr 412	. . . . . . . . 9
98	10	resqcld 10635	. . . . . . . . . . 11
99		remulcl 7902	. . . . . . . . . . 11 $/\$
100	14, 98, 99	sylancr 412	. . . . . . . . . 10
101		readdcl 7900	. . . . . . . . . 10 $/\$
102	4, 100, 101	sylancr 412	. . . . . . . . 9
103		3lt4 9050	. . . . . . . . . 10
104	92	a1i 9	. . . . . . . . . . 11
105	95	a1i 9	. . . . . . . . . . 11
106	6, 48	gt0ap0d 8548	. . . . . . . . . . . . 13 #
107	6, 106	sqgt0apd 10637	. . . . . . . . . . . 12
108		3pos 8972	. . . . . . . . . . . . 13
109	108	a1i 9	. . . . . . . . . . . 12
110	7, 104, 107, 109	divgt0d 8851	. . . . . . . . . . 11
111		ltmul1 8511	. . . . . . . . . . 11 $/\$ $/\$ $/\$
112	104, 105, 10, 110, 111	syl112anc 1237	. . . . . . . . . 10
113	103, 112	mpbii 147	. . . . . . . . 9
114	94, 97, 102, 113	ltsub2dd 8477	. . . . . . . 8
115	42	recnd 7948	. . . . . . . . 9
116		ax-1cn 7867	. . . . . . . . . . 11
117	100	recnd 7948	. . . . . . . . . . 11
118		addcl 7899	. . . . . . . . . . 11 $/\$
119	116, 117, 118	sylancr 412	. . . . . . . . . 10
120	97	recnd 7948	. . . . . . . . . 10
121	119, 120	subcld 8230	. . . . . . . . 9
122		sq1 10569	. . . . . . . . . . . . . . 15
123	122	a1i 9	. . . . . . . . . . . . . 14
124	10	recnd 7948	. . . . . . . . . . . . . . . 16
125	124	mulid2d 7938	. . . . . . . . . . . . . . 15
126	125	oveq2d 5869	. . . . . . . . . . . . . 14
127	123, 126	oveq12d 5871	. . . . . . . . . . . . 13
128	127	oveq1d 5868	. . . . . . . . . . . 12
129		binom2sub 10589	. . . . . . . . . . . . 13 $/\$
130	116, 124, 129	sylancr 412	. . . . . . . . . . . 12
131	98	recnd 7948	. . . . . . . . . . . . 13
132	16	recnd 7948	. . . . . . . . . . . . 13
133	115, 131, 132	addsubd 8251	. . . . . . . . . . . 12
134	128, 130, 133	3eqtr4d 2213	. . . . . . . . . . 11
135	134	oveq2d 5869	. . . . . . . . . 10
136		addcl 7899	. . . . . . . . . . . 12 $/\$
137	116, 131, 136	sylancr 412	. . . . . . . . . . 11
138	29, 137, 132	subdid 8333	. . . . . . . . . 10
139	29, 115, 131	adddid 7944	. . . . . . . . . . . . 13
140	116	2timesi 9008	. . . . . . . . . . . . . . 15
141	140	oveq1i 5863	. . . . . . . . . . . . . 14
142	115, 115, 117	addassd 7942	. . . . . . . . . . . . . 14
143	141, 142	eqtrid 2215	. . . . . . . . . . . . 13
144	139, 143	eqtrd 2203	. . . . . . . . . . . 12
145	29, 29, 124	mulassd 7943	. . . . . . . . . . . . 13
146	55	oveq1i 5863	. . . . . . . . . . . . 13
147	145, 146	eqtr3di 2218	. . . . . . . . . . . 12
148	144, 147	oveq12d 5871	. . . . . . . . . . 11
149	115, 119, 120, 148	assraddsubd 8287	. . . . . . . . . 10
150	135, 138, 149	3eqtrd 2207	. . . . . . . . 9
151	115, 121, 150	mvrladdd 8286	. . . . . . . 8
152		subcl 8118	. . . . . . . . . . 11 $/\$
153	116, 124, 152	sylancr 412	. . . . . . . . . 10
154	153, 115, 132	subdid 8333	. . . . . . . . 9
155	153	mulid1d 7937	. . . . . . . . . 10
156	115, 124, 132	subdird 8334	. . . . . . . . . . 11
157	132	mulid2d 7938	. . . . . . . . . . . 12
158	124, 29, 124	mul12d 8071	. . . . . . . . . . . . 13
159	124	sqvald 10606	. . . . . . . . . . . . . 14
160	159	oveq2d 5869	. . . . . . . . . . . . 13
161	158, 160	eqtr4d 2206	. . . . . . . . . . . 12
162	157, 161	oveq12d 5871	. . . . . . . . . . 11
163	156, 162	eqtrd 2203	. . . . . . . . . 10
164	155, 163	oveq12d 5871	. . . . . . . . 9
165	115, 124, 132, 117	subadd4d 8278	. . . . . . . . . 10
166		df-3 8938	. . . . . . . . . . . . . 14
167	28, 116	addcomi 8063	. . . . . . . . . . . . . 14
168	166, 167	eqtri 2191	. . . . . . . . . . . . 13
169	168	oveq1i 5863	. . . . . . . . . . . 12
170	125	oveq1d 5868	. . . . . . . . . . . . 13
171	115, 124, 29, 170	joinlmuladdmuld 7947	. . . . . . . . . . . 12
172	169, 171	eqtrid 2215	. . . . . . . . . . 11
173	172	oveq2d 5869	. . . . . . . . . 10
174	165, 173	eqtr4d 2206	. . . . . . . . 9
175	154, 164, 174	3eqtrd 2207	. . . . . . . 8
176	114, 151, 175	3brtr4d 4021	. . . . . . 7
177	2, 25, 26, 91, 176	lttrd 8045	. . . . . 6
178		ltmul2 8772	. . . . . . 7 $/\$ $/\$ $/\$
179	2, 26, 1, 45, 178	syl112anc 1237	. . . . . 6
180	177, 179	mpbid 146	. . . . 5
181	18	recnd 7948	. . . . . 6
182	27, 153, 181	mulassd 7943	. . . . 5
183	180, 182	breqtrrd 4017	. . . 4
184	13, 38	remulcld 7950	. . . . 5
185	74	simpld 111	. . . . . 6
186	1, 12, 45, 83	mulgt0d 8042	. . . . . . 7
187		ltmul2 8772	. . . . . . 7 $/\$ $/\$ $/\$
188	18, 38, 13, 186, 187	syl112anc 1237	. . . . . 6
189	185, 188	mpbid 146	. . . . 5
190	29, 34, 153	mulassd 7943	. . . . . . . . 9
191	32	oveq1d 5868	. . . . . . . . 9
192	34, 115, 124	subdid 8333	. . . . . . . . . . 11
193	34	mulid1d 7937	. . . . . . . . . . . 12
194	166	oveq2i 5864	. . . . . . . . . . . . . . . 16
195		2nn0 9152	. . . . . . . . . . . . . . . . 17
196		expp1 10483	. . . . . . . . . . . . . . . . 17 $/\$
197	34, 195, 196	sylancl 411	. . . . . . . . . . . . . . . 16
198	194, 197	eqtrid 2215	. . . . . . . . . . . . . . 15
199	7	recnd 7948	. . . . . . . . . . . . . . . 16
200	199, 34	mulcomd 7941	. . . . . . . . . . . . . . 15
201	198, 200	eqtrd 2203	. . . . . . . . . . . . . 14
202	201	oveq1d 5868	. . . . . . . . . . . . 13
203		3cn 8953	. . . . . . . . . . . . . . 15
204	203	a1i 9	. . . . . . . . . . . . . 14
205	104, 109	gt0ap0d 8548	. . . . . . . . . . . . . 14 #
206	34, 199, 204, 205	divassapd 8743	. . . . . . . . . . . . 13
207	202, 206	eqtr2d 2204	. . . . . . . . . . . 12
208	193, 207	oveq12d 5871	. . . . . . . . . . 11
209	192, 208	eqtrd 2203	. . . . . . . . . 10
210	209	oveq2d 5869	. . . . . . . . 9
211	190, 191, 210	3eqtr3d 2211	. . . . . . . 8
212		sin01bnd 11720	. . . . . . . . . . 11 $/\$
213	72, 212	syl 14	. . . . . . . . . 10 $/\$
214	213	simpld 111	. . . . . . . . 9
215		3nn0 9153	. . . . . . . . . . . . 13
216		reexpcl 10493	. . . . . . . . . . . . 13 $/\$
217	6, 215, 216	sylancl 411	. . . . . . . . . . . 12
218		nndivre 8914	. . . . . . . . . . . 12 $/\$
219	217, 8, 218	sylancl 411	. . . . . . . . . . 11
220	6, 219	resubcld 8300	. . . . . . . . . 10
221	6	resincld 11686	. . . . . . . . . 10
222		ltmul2 8772	. . . . . . . . . 10 $/\$ $/\$ $/\$
223	220, 221, 43, 47, 222	syl112anc 1237	. . . . . . . . 9
224	214, 223	mpbid 146	. . . . . . . 8
225	211, 224	eqbrtrd 4011	. . . . . . 7
226		remulcl 7902	. . . . . . . . 9 $/\$
227	14, 221, 226	sylancr 412	. . . . . . . 8
228		ltmul1 8511	. . . . . . . 8 $/\$ $/\$ $/\$
229	13, 227, 38, 77, 228	syl112anc 1237	. . . . . . 7
230	225, 229	mpbid 146	. . . . . 6
231	221	recnd 7948	. . . . . . . 8
232	38	recnd 7948	. . . . . . . 8
233	29, 231, 232	mulassd 7943	. . . . . . 7
234		sin2t 11712	. . . . . . . 8
235	34, 234	syl 14	. . . . . . 7
236	32	fveq2d 5500	. . . . . . 7
237	233, 235, 236	3eqtr2rd 2210	. . . . . 6
238	230, 237	breqtrrd 4017	. . . . 5
239	19, 184, 20, 189, 238	lttrd 8045	. . . 4
240	3, 19, 20, 183, 239	lttrd 8045	. . 3
241		sincosq1sgn 13541	. . . . 5 $/\$
242	241	simprd 113	. . . 4
243		ltmuldiv 8790	. . . 4 $/\$ $/\$ $/\$
244	1, 20, 2, 242, 243	syl112anc 1237	. . 3
245	240, 244	mpbid 146	. 2
246	2, 242	gt0ap0d 8548	. . 3 #
247		tanvalap 11671	. . 3 $/\$ #
248	27, 246, 247	syl2anc 409	. 2
249	245, 248	breqtrrd 4017	1

Colors of variables: wff set class

Syntax hints:

wi 4 $/\$ wa 103

wb 104 $/\$ w3a 973

wceq 1348

wcel 2141 class class class wbr 3989

cfv 5198 (class class class)co 5853

cc 7772

cr 7773

cc0 7774

c1 7775

caddc 7777

cmul 7779

cxr 7953

clt 7954

cle 7955

cmin 8090 # cap 8500

cdiv 8589

cn 8878

c2 8929

c3 8930

c4 8931

cn0 9135

cioo 9845

cioc 9846

cexp 10475

csin 11607

ccos 11608

ctan 11609

cpi 11610

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 609 ax-in2 610 ax-io 704 ax-5 1440 ax-7 1441 ax-gen 1442 ax-ie1 1486 ax-ie2 1487 ax-8 1497 ax-10 1498 ax-11 1499 ax-i12 1500 ax-bndl 1502 ax-4 1503 ax-17 1519 ax-i9 1523 ax-ial 1527 ax-i5r 1528 ax-13 2143 ax-14 2144 ax-ext 2152 ax-coll 4104 ax-sep 4107 ax-nul 4115 ax-pow 4160 ax-pr 4194 ax-un 4418 ax-setind 4521 ax-iinf 4572 ax-cnex 7865 ax-resscn 7866 ax-1cn 7867 ax-1re 7868 ax-icn 7869 ax-addcl 7870 ax-addrcl 7871 ax-mulcl 7872 ax-mulrcl 7873 ax-addcom 7874 ax-mulcom 7875 ax-addass 7876 ax-mulass 7877 ax-distr 7878 ax-i2m1 7879 ax-0lt1 7880 ax-1rid 7881 ax-0id 7882 ax-rnegex 7883 ax-precex 7884 ax-cnre 7885 ax-pre-ltirr 7886 ax-pre-ltwlin 7887 ax-pre-lttrn 7888 ax-pre-apti 7889 ax-pre-ltadd 7890 ax-pre-mulgt0 7891 ax-pre-mulext 7892 ax-arch 7893 ax-caucvg 7894 ax-pre-suploc 7895 ax-addf 7896 ax-mulf 7897

This theorem depends on definitions: df-bi 116 df-stab 826 df-dc 830 df-3or 974 df-3an 975 df-tru 1351 df-fal 1354 df-nf 1454 df-sb 1756 df-eu 2022 df-mo 2023 df-clab 2157 df-cleq 2163 df-clel 2166 df-nfc 2301 df-ne 2341 df-nel 2436 df-ral 2453 df-rex 2454 df-reu 2455 df-rmo 2456 df-rab 2457 df-v 2732 df-sbc 2956 df-csb 3050 df-dif 3123 df-un 3125 df-in 3127 df-ss 3134 df-nul 3415 df-if 3527 df-pw 3568 df-sn 3589 df-pr 3590 df-op 3592 df-uni 3797 df-int 3832 df-iun 3875 df-disj 3967 df-br 3990 df-opab 4051 df-mpt 4052 df-tr 4088 df-id 4278 df-po 4281 df-iso 4282 df-iord 4351 df-on 4353 df-ilim 4354 df-suc 4356 df-iom 4575 df-xp 4617 df-rel 4618 df-cnv 4619 df-co 4620 df-dm 4621 df-rn 4622 df-res 4623 df-ima 4624 df-iota 5160 df-fun 5200 df-fn 5201 df-f 5202 df-f1 5203 df-fo 5204 df-f1o 5205 df-fv 5206 df-isom 5207 df-riota 5809 df-ov 5856 df-oprab 5857 df-mpo 5858 df-of 6061 df-1st 6119 df-2nd 6120 df-recs 6284 df-irdg 6349 df-frec 6370 df-1o 6395 df-oadd 6399 df-er 6513 df-map 6628 df-pm 6629 df-en 6719 df-dom 6720 df-fin 6721 df-sup 6961 df-inf 6962 df-pnf 7956 df-mnf 7957 df-xr 7958 df-ltxr 7959 df-le 7960 df-sub 8092 df-neg 8093 df-reap 8494 df-ap 8501 df-div 8590 df-inn 8879 df-2 8937 df-3 8938 df-4 8939 df-5 8940 df-6 8941 df-7 8942 df-8 8943 df-9 8944 df-n0 9136 df-z 9213 df-uz 9488 df-q 9579 df-rp 9611 df-xneg 9729 df-xadd 9730 df-ioo 9849 df-ioc 9850 df-ico 9851 df-icc 9852 df-fz 9966 df-fzo 10099 df-seqfrec 10402 df-exp 10476 df-fac 10660 df-bc 10682 df-ihash 10710 df-shft 10779 df-cj 10806 df-re 10807 df-im 10808 df-rsqrt 10962 df-abs 10963 df-clim 11242 df-sumdc 11317 df-ef 11611 df-sin 11613 df-cos 11614 df-tan 11615 df-pi 11616 df-rest 12581 df-topgen 12600 df-psmet 12781 df-xmet 12782 df-met 12783 df-bl 12784 df-mopn 12785 df-top 12790 df-topon 12803 df-bases 12835 df-ntr 12890 df-cn 12982 df-cnp 12983 df-tx 13047 df-cncf 13352 df-limced 13419 df-dvap 13420

This theorem is referenced by: (None)

W3C validator