lptre2pt - Mathbox for Glauco Siliprandi

	Mathbox for Glauco Siliprandi	< Previous Next > Nearby theorems
Mirrors > Home > MPE Home > Th. List > Mathboxes > lptre2pt		Structured version Unicode version

Theorem lptre2pt 37546

Description: If a set in the real line has a limit point than it contains two distinct points that are closer than a given distance. (Contributed by Glauco Siliprandi, 11-Dec-2019.)

**Hypotheses**
Ref	Expression
lptre2pt.j
lptre2pt.a
lptre2pt.x
lptre2pt.e

**Assertion**
Ref	Expression
lptre2pt	$/\$

Distinct variable groups:

Proof of Theorem lptre2pt Dummy variables

are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		lptre2pt.x	. . 3
2		n0 3772	. . 3
3	1, 2	sylib 200	. 2
4		simpr 463	. . . . . . . 8 $/\$
5		lptre2pt.j	. . . . . . . . 9
6		lptre2pt.a	. . . . . . . . . 10
7	6	adantr 467	. . . . . . . . 9 $/\$
8		retop 21774	. . . . . . . . . . . 12
9	5, 8	eqeltri 2507	. . . . . . . . . . 11
10		uniretop 21775	. . . . . . . . . . . . 13
11	5	unieqi 4226	. . . . . . . . . . . . 13
12	10, 11	eqtr4i 2455	. . . . . . . . . . . 12
13	12	lpss 20150	. . . . . . . . . . 11 $/\$
14	9, 7, 13	sylancr 668	. . . . . . . . . 10 $/\$
15	14, 4	sseldd 3466	. . . . . . . . 9 $/\$
16	5, 7, 15	islptre 37525	. . . . . . . 8 $/\$ $\$
17	4, 16	mpbid 214	. . . . . . 7 $/\$ $\$
18		lptre2pt.e	. . . . . . . . . . . . 13
19	18	rpred 11343	. . . . . . . . . . . 12
20	19	adantr 467	. . . . . . . . . . 11 $/\$
21	20	rehalfcld 10861	. . . . . . . . . 10 $/\$
22	15, 21	resubcld 10049	. . . . . . . . 9 $/\$
23	22	rexrd 9692	. . . . . . . 8 $/\$
24	15, 21	readdcld 9672	. . . . . . . . 9 $/\$
25	24	rexrd 9692	. . . . . . . 8 $/\$
26	18	rphalfcld 11355	. . . . . . . . . 10
27	26	adantr 467	. . . . . . . . 9 $/\$
28	15, 27	ltsubrpd 11372	. . . . . . . 8 $/\$
29	15, 27	ltaddrpd 11373	. . . . . . . 8 $/\$
30	23, 25, 15, 28, 29	eliood 37432	. . . . . . 7 $/\$
31		oveq1 6310	. . . . . . . . . . 11
32	31	eleq2d 2493	. . . . . . . . . 10
33	31	ineq1d 3664	. . . . . . . . . . 11 $\$ $\$
34	33	neeq1d 2702	. . . . . . . . . 10 $\$ $\$
35	32, 34	imbi12d 322	. . . . . . . . 9 $\$ $\$
36		oveq2 6311	. . . . . . . . . . 11
37	36	eleq2d 2493	. . . . . . . . . 10
38	36	ineq1d 3664	. . . . . . . . . . 11 $\$ $\$
39	38	neeq1d 2702	. . . . . . . . . 10 $\$ $\$
40	37, 39	imbi12d 322	. . . . . . . . 9 $\$ $\$
41	35, 40	rspc2v 3192	. . . . . . . 8 $/\$ $\$ $\$
42	23, 25, 41	syl2anc 666	. . . . . . 7 $/\$ $\$ $\$
43	17, 30, 42	mp2d 47	. . . . . 6 $/\$ $\$
44		n0 3772	. . . . . 6 $\$ $\$
45	43, 44	sylib 200	. . . . 5 $/\$ $\$
46		elinel2 3653	. . . . . . . . . 10 $\$ $\$
47	46	eldifad 3449	. . . . . . . . 9 $\$
48	47	adantl 468	. . . . . . . 8 $/\$ $/\$ $\$
49		elinel1 3652	. . . . . . . . . 10 $\$
50	49	adantl 468	. . . . . . . . 9 $/\$ $/\$ $\$
51	46	eldifbd 3450	. . . . . . . . . 10 $\$
52	51	adantl 468	. . . . . . . . 9 $/\$ $/\$ $\$
53	50, 52	eldifd 3448	. . . . . . . 8 $/\$ $/\$ $\$ $\$
54	48, 53	jca 535	. . . . . . 7 $/\$ $/\$ $\$ $/\$ $\$
55	54	ex 436	. . . . . 6 $/\$ $\$ $/\$ $\$
56	55	eximdv 1755	. . . . 5 $/\$ $\$ $/\$ $\$
57	45, 56	mpd 15	. . . 4 $/\$ $/\$ $\$
58		df-rex 2782	. . . 4 $\$ $/\$ $\$
59	57, 58	sylibr 216	. . 3 $/\$ $\$
60	17	adantr 467	. . . . . . . . 9 $/\$ $/\$ $\$ $\$
61		eldifi 3588	. . . . . . . . . . . 12 $\$
62		elioore 11668	. . . . . . . . . . . 12
63	61, 62	syl 17	. . . . . . . . . . 11 $\$
64	63	adantl 468	. . . . . . . . . 10 $/\$ $/\$ $\$
65	15	adantr 467	. . . . . . . . . 10 $/\$ $/\$ $\$
66		eldifsni 4124	. . . . . . . . . . 11 $\$
67	66	adantl 468	. . . . . . . . . 10 $/\$ $/\$ $\$
68		simpr 463	. . . . . . . . . . . . . 14 $/\$
69		resubcl 9940	. . . . . . . . . . . . . . . 16 $/\$
70	69	recnd 9671	. . . . . . . . . . . . . . 15 $/\$
71	70	abscld 13491	. . . . . . . . . . . . . 14 $/\$
72	68, 71	resubcld 10049	. . . . . . . . . . . . 13 $/\$
73	72	rexrd 9692	. . . . . . . . . . . 12 $/\$
74	73	3adant3 1026	. . . . . . . . . . 11 $/\$ $/\$
75	68, 71	readdcld 9672	. . . . . . . . . . . . 13 $/\$
76	75	rexrd 9692	. . . . . . . . . . . 12 $/\$
77	76	3adant3 1026	. . . . . . . . . . 11 $/\$ $/\$
78		simp2 1007	. . . . . . . . . . 11 $/\$ $/\$
79	70	3adant3 1026	. . . . . . . . . . . . 13 $/\$ $/\$
80		recn 9631	. . . . . . . . . . . . . . 15
81	80	3ad2ant1 1027	. . . . . . . . . . . . . 14 $/\$ $/\$
82	78	recnd 9671	. . . . . . . . . . . . . 14 $/\$ $/\$
83		simp3 1008	. . . . . . . . . . . . . 14 $/\$ $/\$
84	81, 82, 83	subne0d 9997	. . . . . . . . . . . . 13 $/\$ $/\$
85	79, 84	absrpcld 13503	. . . . . . . . . . . 12 $/\$ $/\$
86	78, 85	ltsubrpd 11372	. . . . . . . . . . 11 $/\$ $/\$
87	78, 85	ltaddrpd 11373	. . . . . . . . . . 11 $/\$ $/\$
88	74, 77, 78, 86, 87	eliood 37432	. . . . . . . . . 10 $/\$ $/\$
89	64, 65, 67, 88	syl3anc 1265	. . . . . . . . 9 $/\$ $/\$ $\$
90	63	recnd 9671	. . . . . . . . . . . . . . 15 $\$
91	90	adantl 468	. . . . . . . . . . . . . 14 $/\$ $/\$ $\$
92	65	recnd 9671	. . . . . . . . . . . . . 14 $/\$ $/\$ $\$
93	91, 92	subcld 9988	. . . . . . . . . . . . 13 $/\$ $/\$ $\$
94	93	abscld 13491	. . . . . . . . . . . 12 $/\$ $/\$ $\$
95	65, 94	resubcld 10049	. . . . . . . . . . 11 $/\$ $/\$ $\$
96	95	rexrd 9692	. . . . . . . . . 10 $/\$ $/\$ $\$
97	65, 94	readdcld 9672	. . . . . . . . . . 11 $/\$ $/\$ $\$
98	97	rexrd 9692	. . . . . . . . . 10 $/\$ $/\$ $\$
99		oveq1 6310	. . . . . . . . . . . . 13
100	99	eleq2d 2493	. . . . . . . . . . . 12
101	99	ineq1d 3664	. . . . . . . . . . . . 13 $\$ $\$
102	101	neeq1d 2702	. . . . . . . . . . . 12 $\$ $\$
103	100, 102	imbi12d 322	. . . . . . . . . . 11 $\$ $\$
104		oveq2 6311	. . . . . . . . . . . . 13
105	104	eleq2d 2493	. . . . . . . . . . . 12
106	104	ineq1d 3664	. . . . . . . . . . . . 13 $\$ $\$
107	106	neeq1d 2702	. . . . . . . . . . . 12 $\$ $\$
108	105, 107	imbi12d 322	. . . . . . . . . . 11 $\$ $\$
109	103, 108	rspc2v 3192	. . . . . . . . . 10 $/\$ $\$ $\$
110	96, 98, 109	syl2anc 666	. . . . . . . . 9 $/\$ $/\$ $\$ $\$ $\$
111	60, 89, 110	mp2d 47	. . . . . . . 8 $/\$ $/\$ $\$ $\$
112		n0 3772	. . . . . . . 8 $\$ $\$
113	111, 112	sylib 200	. . . . . . 7 $/\$ $/\$ $\$ $\$
114		elinel2 3653	. . . . . . . . . . . 12 $\$ $\$
115	114	eldifad 3449	. . . . . . . . . . 11 $\$
116	115	adantl 468	. . . . . . . . . 10 $/\$ $/\$ $\$ $/\$ $\$
117	65	adantr 467	. . . . . . . . . . 11 $/\$ $/\$ $\$ $/\$ $\$
118	64	adantr 467	. . . . . . . . . . 11 $/\$ $/\$ $\$ $/\$ $\$
119		elinel1 3652	. . . . . . . . . . . 12 $\$
120	119	adantl 468	. . . . . . . . . . 11 $/\$ $/\$ $\$ $/\$ $\$
121		simpl1 1009	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$
122		simpl2 1010	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$
123		simpl3 1011	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$
124		simpr 463	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$
125	122, 121	subge0d 10205	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$
126	124, 125	mpbid 214	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$
127	121, 122, 126	abssubge0d 13487	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$
128	127	oveq2d 6319	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$
129	127	oveq2d 6319	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$
130	128, 129	oveq12d 6321	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$
131	123, 130	eleqtrd 2513	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$
132		elioore 11668	. . . . . . . . . . . . . . 15
133	132	3ad2ant3 1029	. . . . . . . . . . . . . 14 $/\$ $/\$
134		simpl 459	. . . . . . . . . . . . . . . . . . 19 $/\$
135	69	ancoms 455	. . . . . . . . . . . . . . . . . . 19 $/\$
136	134, 135	resubcld 10049	. . . . . . . . . . . . . . . . . 18 $/\$
137	136	rexrd 9692	. . . . . . . . . . . . . . . . 17 $/\$
138	137	3adant3 1026	. . . . . . . . . . . . . . . 16 $/\$ $/\$
139	134, 135	readdcld 9672	. . . . . . . . . . . . . . . . . 18 $/\$
140	139	rexrd 9692	. . . . . . . . . . . . . . . . 17 $/\$
141	140	3adant3 1026	. . . . . . . . . . . . . . . 16 $/\$ $/\$
142		simp3 1008	. . . . . . . . . . . . . . . 16 $/\$ $/\$
143		iooltub 37447	. . . . . . . . . . . . . . . 16 $/\$ $/\$
144	138, 141, 142, 143	syl3anc 1265	. . . . . . . . . . . . . . 15 $/\$ $/\$
145	134	recnd 9671	. . . . . . . . . . . . . . . . 17 $/\$
146	80	adantl 468	. . . . . . . . . . . . . . . . 17 $/\$
147	145, 146	pncan3d 9991	. . . . . . . . . . . . . . . 16 $/\$
148	147	3adant3 1026	. . . . . . . . . . . . . . 15 $/\$ $/\$
149	144, 148	breqtrd 4446	. . . . . . . . . . . . . 14 $/\$ $/\$
150	133, 149	gtned 9772	. . . . . . . . . . . . 13 $/\$ $/\$
151	121, 122, 131, 150	syl3anc 1265	. . . . . . . . . . . 12 $/\$ $/\$ $/\$
152		simpl1 1009	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$
153		simpl2 1010	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$
154		simpl3 1011	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$
155	135	adantr 467	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$
156		0red 9646	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$
157		simpr 463	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$
158	155, 156	ltnled 9784	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$
159	157, 158	mpbird 236	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$
160	155, 156, 159	ltled 9785	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$
161	155, 160	absnidd 13469	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$
162	146	adantr 467	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$
163	145	adantr 467	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$
164	162, 163	negsubdi2d 10004	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$
165	161, 164	eqtrd 2464	. . . . . . . . . . . . . . . . 17 $/\$ $/\$
166	165	oveq2d 6319	. . . . . . . . . . . . . . . 16 $/\$ $/\$
167	165	oveq2d 6319	. . . . . . . . . . . . . . . 16 $/\$ $/\$
168	166, 167	oveq12d 6321	. . . . . . . . . . . . . . 15 $/\$ $/\$
169	168	3adantl3 1164	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$
170	154, 169	eleqtrd 2513	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$
171		simp2 1007	. . . . . . . . . . . . . 14 $/\$ $/\$
172	171	rexrd 9692	. . . . . . . . . . . . . . 15 $/\$ $/\$
173		resubcl 9940	. . . . . . . . . . . . . . . . . 18 $/\$
174	134, 173	readdcld 9672	. . . . . . . . . . . . . . . . 17 $/\$
175	174	rexrd 9692	. . . . . . . . . . . . . . . 16 $/\$
176	175	3adant3 1026	. . . . . . . . . . . . . . 15 $/\$ $/\$
177		simp3 1008	. . . . . . . . . . . . . . . 16 $/\$ $/\$
178	145, 146	nncand 9993	. . . . . . . . . . . . . . . . . 18 $/\$
179	178	oveq1d 6318	. . . . . . . . . . . . . . . . 17 $/\$
180	179	3adant3 1026	. . . . . . . . . . . . . . . 16 $/\$ $/\$
181	177, 180	eleqtrd 2513	. . . . . . . . . . . . . . 15 $/\$ $/\$
182		ioogtlb 37429	. . . . . . . . . . . . . . 15 $/\$ $/\$
183	172, 176, 181, 182	syl3anc 1265	. . . . . . . . . . . . . 14 $/\$ $/\$
184	171, 183	ltned 9773	. . . . . . . . . . . . 13 $/\$ $/\$
185	152, 153, 170, 184	syl3anc 1265	. . . . . . . . . . . 12 $/\$ $/\$ $/\$
186	151, 185	pm2.61dan 799	. . . . . . . . . . 11 $/\$ $/\$
187	117, 118, 120, 186	syl3anc 1265	. . . . . . . . . 10 $/\$ $/\$ $\$ $/\$ $\$
188	63	adantr 467	. . . . . . . . . . . . . . . 16 $\$ $/\$ $\$
189		elioore 11668	. . . . . . . . . . . . . . . . . 18
190	119, 189	syl 17	. . . . . . . . . . . . . . . . 17 $\$
191	190	adantl 468	. . . . . . . . . . . . . . . 16 $\$ $/\$ $\$
192	188, 191	resubcld 10049	. . . . . . . . . . . . . . 15 $\$ $/\$ $\$
193	192	recnd 9671	. . . . . . . . . . . . . 14 $\$ $/\$ $\$
194	193	adantll 719	. . . . . . . . . . . . 13 $/\$ $\$ $/\$ $\$
195	194	abscld 13491	. . . . . . . . . . . 12 $/\$ $\$ $/\$ $\$
196	195	adantllr 724	. . . . . . . . . . 11 $/\$ $/\$ $\$ $/\$ $\$
197	94	adantr 467	. . . . . . . . . . . 12 $/\$ $/\$ $\$ $/\$ $\$
198	15	adantr 467	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $\$
199	190	adantl 468	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $\$
200	198, 199	resubcld 10049	. . . . . . . . . . . . . . 15 $/\$ $/\$ $\$
201	200	recnd 9671	. . . . . . . . . . . . . 14 $/\$ $/\$ $\$
202	201	abscld 13491	. . . . . . . . . . . . 13 $/\$ $/\$ $\$
203	202	adantlr 720	. . . . . . . . . . . 12 $/\$ $/\$ $\$ $/\$ $\$
204	197, 203	readdcld 9672	. . . . . . . . . . 11 $/\$ $/\$ $\$ $/\$ $\$
205	19	ad3antrrr 735	. . . . . . . . . . 11 $/\$ $/\$ $\$ $/\$ $\$
206	118	recnd 9671	. . . . . . . . . . . 12 $/\$ $/\$ $\$ $/\$ $\$
207	190	recnd 9671	. . . . . . . . . . . . 13 $\$
208	207	adantl 468	. . . . . . . . . . . 12 $/\$ $/\$ $\$ $/\$ $\$
209	92	adantr 467	. . . . . . . . . . . 12 $/\$ $/\$ $\$ $/\$ $\$
210	206, 208, 209	abs3difd 13515	. . . . . . . . . . 11 $/\$ $/\$ $\$ $/\$ $\$
211	21	ad2antrr 731	. . . . . . . . . . . . 13 $/\$ $/\$ $\$ $/\$ $\$
212		simpll 759	. . . . . . . . . . . . . . 15 $/\$ $/\$ $\$
213	61	adantl 468	. . . . . . . . . . . . . . 15 $/\$ $/\$ $\$
214	62, 146	sylan2 477	. . . . . . . . . . . . . . . . . 18 $/\$
215	62, 145	sylan2 477	. . . . . . . . . . . . . . . . . 18 $/\$
216	214, 215	abssubd 13508	. . . . . . . . . . . . . . . . 17 $/\$
217	216	3adant1 1024	. . . . . . . . . . . . . . . 16 $/\$ $/\$
218		simp2 1007	. . . . . . . . . . . . . . . . 17 $/\$ $/\$
219	19	rehalfcld 10861	. . . . . . . . . . . . . . . . . 18
220	219	3ad2ant1 1027	. . . . . . . . . . . . . . . . 17 $/\$ $/\$
221		simp3 1008	. . . . . . . . . . . . . . . . 17 $/\$ $/\$
222	218, 220, 221	iooabslt 37433	. . . . . . . . . . . . . . . 16 $/\$ $/\$
223	217, 222	eqbrtrd 4442	. . . . . . . . . . . . . . 15 $/\$ $/\$
224	212, 65, 213, 223	syl3anc 1265	. . . . . . . . . . . . . 14 $/\$ $/\$ $\$
225	224	adantr 467	. . . . . . . . . . . . 13 $/\$ $/\$ $\$ $/\$ $\$
226	212, 65, 213	3jca 1186	. . . . . . . . . . . . . 14 $/\$ $/\$ $\$ $/\$ $/\$
227		simpl 459	. . . . . . . . . . . . . . . . . . 19 $/\$
228	189	adantl 468	. . . . . . . . . . . . . . . . . . 19 $/\$
229	227, 228	resubcld 10049	. . . . . . . . . . . . . . . . . 18 $/\$
230	229	recnd 9671	. . . . . . . . . . . . . . . . 17 $/\$
231	230	abscld 13491	. . . . . . . . . . . . . . . 16 $/\$
232	231	3ad2antl2 1169	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$
233	220	adantr 467	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$
234	214, 215	subcld 9988	. . . . . . . . . . . . . . . . . . 19 $/\$
235	234	abscld 13491	. . . . . . . . . . . . . . . . . 18 $/\$
236	235	3adant1 1024	. . . . . . . . . . . . . . . . 17 $/\$ $/\$
237	236	adantr 467	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$
238		simpl2 1010	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$
239		simpr 463	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$
240	238, 237, 239	iooabslt 37433	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$
241	223	adantr 467	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$
242	232, 237, 233, 240, 241	lttrd 9798	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$
243	232, 233, 242	ltled 9785	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$
244	226, 119, 243	syl2an 480	. . . . . . . . . . . . 13 $/\$ $/\$ $\$ $/\$ $\$
245	197, 203, 211, 211, 225, 244	ltleaddd 10236	. . . . . . . . . . . 12 $/\$ $/\$ $\$ $/\$ $\$
246	19	recnd 9671	. . . . . . . . . . . . . 14
247	246	2halvesd 10860	. . . . . . . . . . . . 13
248	247	ad3antrrr 735	. . . . . . . . . . . 12 $/\$ $/\$ $\$ $/\$ $\$
249	245, 248	breqtrd 4446	. . . . . . . . . . 11 $/\$ $/\$ $\$ $/\$ $\$
250	196, 204, 205, 210, 249	lelttrd 9795	. . . . . . . . . 10 $/\$ $/\$ $\$ $/\$ $\$
251	116, 187, 250	jca32 538	. . . . . . . . 9 $/\$ $/\$ $\$ $/\$ $\$ $/\$ $/\$
252	251	ex 436	. . . . . . . 8 $/\$ $/\$ $\$ $\$ $/\$ $/\$
253	252	eximdv 1755	. . . . . . 7 $/\$ $/\$ $\$ $\$ $/\$ $/\$
254	113, 253	mpd 15	. . . . . 6 $/\$ $/\$ $\$ $/\$ $/\$
255		df-rex 2782	. . . . . 6 $/\$ $/\$ $/\$
256	254, 255	sylibr 216	. . . . 5 $/\$ $/\$ $\$ $/\$
257	256	ex 436	. . . 4 $/\$ $\$ $/\$
258	257	reximdv 2900	. . 3 $/\$ $\$ $/\$
259	59, 258	mpd 15	. 2 $/\$ $/\$
260	3, 259	exlimddv 1771	1 $/\$

Colors of variables: wff setvar class

Syntax hints:

wn 3

wi 4 $/\$ wa 371 $/\$ w3a 983

wceq 1438

wex 1660

wcel 1869

wne 2619

wral 2776

wrex 2777 $\$ cdif 3434

cin 3436

wss 3437

c0 3762

csn 3997

cuni 4217 class class class wbr 4421

crn 4852

cfv 5599 (class class class)co 6303

cc 9539

cr 9540

cc0 9541

caddc 9544

cxr 9676

clt 9677

cle 9678

cmin 9862

cneg 9863

cdiv 10271

c2 10661

crp 11304

cioo 11637

cabs 13291

ctg 15329

ctop 19909

clp 20142

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1666 ax-4 1679 ax-5 1749 ax-6 1795 ax-7 1840 ax-8 1871 ax-9 1873 ax-10 1888 ax-11 1893 ax-12 1906 ax-13 2054 ax-ext 2401 ax-rep 4534 ax-sep 4544 ax-nul 4553 ax-pow 4600 ax-pr 4658 ax-un 6595 ax-cnex 9597 ax-resscn 9598 ax-1cn 9599 ax-icn 9600 ax-addcl 9601 ax-addrcl 9602 ax-mulcl 9603 ax-mulrcl 9604 ax-mulcom 9605 ax-addass 9606 ax-mulass 9607 ax-distr 9608 ax-i2m1 9609 ax-1ne0 9610 ax-1rid 9611 ax-rnegex 9612 ax-rrecex 9613 ax-cnre 9614 ax-pre-lttri 9615 ax-pre-lttrn 9616 ax-pre-ltadd 9617 ax-pre-mulgt0 9618 ax-pre-sup 9619

This theorem depends on definitions: df-bi 189 df-or 372 df-an 373 df-3or 984 df-3an 985 df-tru 1441 df-ex 1661 df-nf 1665 df-sb 1788 df-eu 2270 df-mo 2271 df-clab 2409 df-cleq 2415 df-clel 2418 df-nfc 2573 df-ne 2621 df-nel 2622 df-ral 2781 df-rex 2782 df-reu 2783 df-rmo 2784 df-rab 2785 df-v 3084 df-sbc 3301 df-csb 3397 df-dif 3440 df-un 3442 df-in 3444 df-ss 3451 df-pss 3453 df-nul 3763 df-if 3911 df-pw 3982 df-sn 3998 df-pr 4000 df-tp 4002 df-op 4004 df-uni 4218 df-int 4254 df-iun 4299 df-iin 4300 df-br 4422 df-opab 4481 df-mpt 4482 df-tr 4517 df-eprel 4762 df-id 4766 df-po 4772 df-so 4773 df-fr 4810 df-we 4812 df-xp 4857 df-rel 4858 df-cnv 4859 df-co 4860 df-dm 4861 df-rn 4862 df-res 4863 df-ima 4864 df-pred 5397 df-ord 5443 df-on 5444 df-lim 5445 df-suc 5446 df-iota 5563 df-fun 5601 df-fn 5602 df-f 5603 df-f1 5604 df-fo 5605 df-f1o 5606 df-fv 5607 df-riota 6265 df-ov 6306 df-oprab 6307 df-mpt2 6308 df-om 6705 df-1st 6805 df-2nd 6806 df-wrecs 7034 df-recs 7096 df-rdg 7134 df-er 7369 df-map 7480 df-en 7576 df-dom 7577 df-sdom 7578 df-sup 7960 df-inf 7961 df-pnf 9679 df-mnf 9680 df-xr 9681 df-ltxr 9682 df-le 9683 df-sub 9864 df-neg 9865 df-div 10272 df-nn 10612 df-2 10670 df-3 10671 df-n0 10872 df-z 10940 df-uz 11162 df-q 11267 df-rp 11305 df-xadd 11412 df-ioo 11641 df-seq 12215 df-exp 12274 df-cj 13156 df-re 13157 df-im 13158 df-sqrt 13292 df-abs 13293 df-topgen 15335 df-psmet 18955 df-xmet 18956 df-met 18957 df-bl 18958 df-top 19913 df-bases 19914 df-topon 19915 df-cld 20026 df-ntr 20027 df-cls 20028 df-nei 20106 df-lp 20144

This theorem is referenced by: fourierdlem42 37838 fourierdlem42OLD 37839

W3C validator