lptre2pt - Mathbox for Glauco Siliprandi

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

Theorem lptre2pt 37817

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 3732	. . 3
3	1, 2	sylib 201	. 2
4		simpr 468	. . . . . . . 8 $/\$
5		lptre2pt.j	. . . . . . . . 9
6		lptre2pt.a	. . . . . . . . . 10
7	6	adantr 472	. . . . . . . . 9 $/\$
8		retop 21860	. . . . . . . . . . . 12
9	5, 8	eqeltri 2545	. . . . . . . . . . 11
10		uniretop 21861	. . . . . . . . . . . . 13
11	5	unieqi 4199	. . . . . . . . . . . . 13
12	10, 11	eqtr4i 2496	. . . . . . . . . . . 12
13	12	lpss 20235	. . . . . . . . . . 11 $/\$
14	9, 7, 13	sylancr 676	. . . . . . . . . 10 $/\$
15	14, 4	sseldd 3419	. . . . . . . . 9 $/\$
16	5, 7, 15	islptre 37796	. . . . . . . 8 $/\$ $\$
17	4, 16	mpbid 215	. . . . . . 7 $/\$ $\$
18		lptre2pt.e	. . . . . . . . . . . . 13
19	18	rpred 11364	. . . . . . . . . . . 12
20	19	adantr 472	. . . . . . . . . . 11 $/\$
21	20	rehalfcld 10882	. . . . . . . . . 10 $/\$
22	15, 21	resubcld 10068	. . . . . . . . 9 $/\$
23	22	rexrd 9708	. . . . . . . 8 $/\$
24	15, 21	readdcld 9688	. . . . . . . . 9 $/\$
25	24	rexrd 9708	. . . . . . . 8 $/\$
26	18	rphalfcld 11376	. . . . . . . . . 10
27	26	adantr 472	. . . . . . . . 9 $/\$
28	15, 27	ltsubrpd 11393	. . . . . . . 8 $/\$
29	15, 27	ltaddrpd 11394	. . . . . . . 8 $/\$
30	23, 25, 15, 28, 29	eliood 37691	. . . . . . 7 $/\$
31		oveq1 6315	. . . . . . . . . . 11
32	31	eleq2d 2534	. . . . . . . . . 10
33	31	ineq1d 3624	. . . . . . . . . . 11 $\$ $\$
34	33	neeq1d 2702	. . . . . . . . . 10 $\$ $\$
35	32, 34	imbi12d 327	. . . . . . . . 9 $\$ $\$
36		oveq2 6316	. . . . . . . . . . 11
37	36	eleq2d 2534	. . . . . . . . . 10
38	36	ineq1d 3624	. . . . . . . . . . 11 $\$ $\$
39	38	neeq1d 2702	. . . . . . . . . 10 $\$ $\$
40	37, 39	imbi12d 327	. . . . . . . . 9 $\$ $\$
41	35, 40	rspc2v 3147	. . . . . . . 8 $/\$ $\$ $\$
42	23, 25, 41	syl2anc 673	. . . . . . 7 $/\$ $\$ $\$
43	17, 30, 42	mp2d 45	. . . . . 6 $/\$ $\$
44		n0 3732	. . . . . 6 $\$ $\$
45	43, 44	sylib 201	. . . . 5 $/\$ $\$
46		elinel2 3611	. . . . . . . . . 10 $\$ $\$
47	46	eldifad 3402	. . . . . . . . 9 $\$
48	47	adantl 473	. . . . . . . 8 $/\$ $/\$ $\$
49		elinel1 3610	. . . . . . . . . 10 $\$
50	49	adantl 473	. . . . . . . . 9 $/\$ $/\$ $\$
51	46	eldifbd 3403	. . . . . . . . . 10 $\$
52	51	adantl 473	. . . . . . . . 9 $/\$ $/\$ $\$
53	50, 52	eldifd 3401	. . . . . . . 8 $/\$ $/\$ $\$ $\$
54	48, 53	jca 541	. . . . . . 7 $/\$ $/\$ $\$ $/\$ $\$
55	54	ex 441	. . . . . 6 $/\$ $\$ $/\$ $\$
56	55	eximdv 1772	. . . . 5 $/\$ $\$ $/\$ $\$
57	45, 56	mpd 15	. . . 4 $/\$ $/\$ $\$
58		df-rex 2762	. . . 4 $\$ $/\$ $\$
59	57, 58	sylibr 217	. . 3 $/\$ $\$
60	17	adantr 472	. . . . . . . . 9 $/\$ $/\$ $\$ $\$
61		eldifi 3544	. . . . . . . . . . . 12 $\$
62		elioore 11691	. . . . . . . . . . . 12
63	61, 62	syl 17	. . . . . . . . . . 11 $\$
64	63	adantl 473	. . . . . . . . . 10 $/\$ $/\$ $\$
65	15	adantr 472	. . . . . . . . . 10 $/\$ $/\$ $\$
66		eldifsni 4089	. . . . . . . . . . 11 $\$
67	66	adantl 473	. . . . . . . . . 10 $/\$ $/\$ $\$
68		simpr 468	. . . . . . . . . . . . . 14 $/\$
69		resubcl 9958	. . . . . . . . . . . . . . . 16 $/\$
70	69	recnd 9687	. . . . . . . . . . . . . . 15 $/\$
71	70	abscld 13575	. . . . . . . . . . . . . 14 $/\$
72	68, 71	resubcld 10068	. . . . . . . . . . . . 13 $/\$
73	72	rexrd 9708	. . . . . . . . . . . 12 $/\$
74	73	3adant3 1050	. . . . . . . . . . 11 $/\$ $/\$
75	68, 71	readdcld 9688	. . . . . . . . . . . . 13 $/\$
76	75	rexrd 9708	. . . . . . . . . . . 12 $/\$
77	76	3adant3 1050	. . . . . . . . . . 11 $/\$ $/\$
78		simp2 1031	. . . . . . . . . . 11 $/\$ $/\$
79	70	3adant3 1050	. . . . . . . . . . . . 13 $/\$ $/\$
80		recn 9647	. . . . . . . . . . . . . . 15
81	80	3ad2ant1 1051	. . . . . . . . . . . . . 14 $/\$ $/\$
82	78	recnd 9687	. . . . . . . . . . . . . 14 $/\$ $/\$
83		simp3 1032	. . . . . . . . . . . . . 14 $/\$ $/\$
84	81, 82, 83	subne0d 10014	. . . . . . . . . . . . 13 $/\$ $/\$
85	79, 84	absrpcld 13587	. . . . . . . . . . . 12 $/\$ $/\$
86	78, 85	ltsubrpd 11393	. . . . . . . . . . 11 $/\$ $/\$
87	78, 85	ltaddrpd 11394	. . . . . . . . . . 11 $/\$ $/\$
88	74, 77, 78, 86, 87	eliood 37691	. . . . . . . . . 10 $/\$ $/\$
89	64, 65, 67, 88	syl3anc 1292	. . . . . . . . 9 $/\$ $/\$ $\$
90	63	recnd 9687	. . . . . . . . . . . . . . 15 $\$
91	90	adantl 473	. . . . . . . . . . . . . 14 $/\$ $/\$ $\$
92	65	recnd 9687	. . . . . . . . . . . . . 14 $/\$ $/\$ $\$
93	91, 92	subcld 10005	. . . . . . . . . . . . 13 $/\$ $/\$ $\$
94	93	abscld 13575	. . . . . . . . . . . 12 $/\$ $/\$ $\$
95	65, 94	resubcld 10068	. . . . . . . . . . 11 $/\$ $/\$ $\$
96	95	rexrd 9708	. . . . . . . . . 10 $/\$ $/\$ $\$
97	65, 94	readdcld 9688	. . . . . . . . . . 11 $/\$ $/\$ $\$
98	97	rexrd 9708	. . . . . . . . . 10 $/\$ $/\$ $\$
99		oveq1 6315	. . . . . . . . . . . . 13
100	99	eleq2d 2534	. . . . . . . . . . . 12
101	99	ineq1d 3624	. . . . . . . . . . . . 13 $\$ $\$
102	101	neeq1d 2702	. . . . . . . . . . . 12 $\$ $\$
103	100, 102	imbi12d 327	. . . . . . . . . . 11 $\$ $\$
104		oveq2 6316	. . . . . . . . . . . . 13
105	104	eleq2d 2534	. . . . . . . . . . . 12
106	104	ineq1d 3624	. . . . . . . . . . . . 13 $\$ $\$
107	106	neeq1d 2702	. . . . . . . . . . . 12 $\$ $\$
108	105, 107	imbi12d 327	. . . . . . . . . . 11 $\$ $\$
109	103, 108	rspc2v 3147	. . . . . . . . . 10 $/\$ $\$ $\$
110	96, 98, 109	syl2anc 673	. . . . . . . . 9 $/\$ $/\$ $\$ $\$ $\$
111	60, 89, 110	mp2d 45	. . . . . . . 8 $/\$ $/\$ $\$ $\$
112		n0 3732	. . . . . . . 8 $\$ $\$
113	111, 112	sylib 201	. . . . . . 7 $/\$ $/\$ $\$ $\$
114		elinel2 3611	. . . . . . . . . . . 12 $\$ $\$
115	114	eldifad 3402	. . . . . . . . . . 11 $\$
116	115	adantl 473	. . . . . . . . . 10 $/\$ $/\$ $\$ $/\$ $\$
117	65	adantr 472	. . . . . . . . . . 11 $/\$ $/\$ $\$ $/\$ $\$
118	64	adantr 472	. . . . . . . . . . 11 $/\$ $/\$ $\$ $/\$ $\$
119		elinel1 3610	. . . . . . . . . . . 12 $\$
120	119	adantl 473	. . . . . . . . . . 11 $/\$ $/\$ $\$ $/\$ $\$
121		simpl1 1033	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$
122		simpl2 1034	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$
123		simpl3 1035	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$
124		simpr 468	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$
125	122, 121	subge0d 10224	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$
126	124, 125	mpbid 215	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$
127	121, 122, 126	abssubge0d 13570	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$
128	127	oveq2d 6324	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$
129	127	oveq2d 6324	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$
130	128, 129	oveq12d 6326	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$
131	123, 130	eleqtrd 2551	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$
132		elioore 11691	. . . . . . . . . . . . . . 15
133	132	3ad2ant3 1053	. . . . . . . . . . . . . 14 $/\$ $/\$
134		simpl 464	. . . . . . . . . . . . . . . . . . 19 $/\$
135	69	ancoms 460	. . . . . . . . . . . . . . . . . . 19 $/\$
136	134, 135	resubcld 10068	. . . . . . . . . . . . . . . . . 18 $/\$
137	136	rexrd 9708	. . . . . . . . . . . . . . . . 17 $/\$
138	137	3adant3 1050	. . . . . . . . . . . . . . . 16 $/\$ $/\$
139	134, 135	readdcld 9688	. . . . . . . . . . . . . . . . . 18 $/\$
140	139	rexrd 9708	. . . . . . . . . . . . . . . . 17 $/\$
141	140	3adant3 1050	. . . . . . . . . . . . . . . 16 $/\$ $/\$
142		simp3 1032	. . . . . . . . . . . . . . . 16 $/\$ $/\$
143		iooltub 37706	. . . . . . . . . . . . . . . 16 $/\$ $/\$
144	138, 141, 142, 143	syl3anc 1292	. . . . . . . . . . . . . . 15 $/\$ $/\$
145	134	recnd 9687	. . . . . . . . . . . . . . . . 17 $/\$
146	80	adantl 473	. . . . . . . . . . . . . . . . 17 $/\$
147	145, 146	pncan3d 10008	. . . . . . . . . . . . . . . 16 $/\$
148	147	3adant3 1050	. . . . . . . . . . . . . . 15 $/\$ $/\$
149	144, 148	breqtrd 4420	. . . . . . . . . . . . . 14 $/\$ $/\$
150	133, 149	gtned 9787	. . . . . . . . . . . . 13 $/\$ $/\$
151	121, 122, 131, 150	syl3anc 1292	. . . . . . . . . . . 12 $/\$ $/\$ $/\$
152		simpl1 1033	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$
153		simpl2 1034	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$
154		simpl3 1035	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$
155	135	adantr 472	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$
156		0red 9662	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$
157		simpr 468	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$
158	155, 156	ltnled 9799	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$
159	157, 158	mpbird 240	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$
160	155, 156, 159	ltled 9800	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$
161	155, 160	absnidd 13552	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$
162	146	adantr 472	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$
163	145	adantr 472	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$
164	162, 163	negsubdi2d 10021	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$
165	161, 164	eqtrd 2505	. . . . . . . . . . . . . . . . 17 $/\$ $/\$
166	165	oveq2d 6324	. . . . . . . . . . . . . . . 16 $/\$ $/\$
167	165	oveq2d 6324	. . . . . . . . . . . . . . . 16 $/\$ $/\$
168	166, 167	oveq12d 6326	. . . . . . . . . . . . . . 15 $/\$ $/\$
169	168	3adantl3 1188	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$
170	154, 169	eleqtrd 2551	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$
171		simp2 1031	. . . . . . . . . . . . . 14 $/\$ $/\$
172	171	rexrd 9708	. . . . . . . . . . . . . . 15 $/\$ $/\$
173		resubcl 9958	. . . . . . . . . . . . . . . . . 18 $/\$
174	134, 173	readdcld 9688	. . . . . . . . . . . . . . . . 17 $/\$
175	174	rexrd 9708	. . . . . . . . . . . . . . . 16 $/\$
176	175	3adant3 1050	. . . . . . . . . . . . . . 15 $/\$ $/\$
177		simp3 1032	. . . . . . . . . . . . . . . 16 $/\$ $/\$
178	145, 146	nncand 10010	. . . . . . . . . . . . . . . . . 18 $/\$
179	178	oveq1d 6323	. . . . . . . . . . . . . . . . 17 $/\$
180	179	3adant3 1050	. . . . . . . . . . . . . . . 16 $/\$ $/\$
181	177, 180	eleqtrd 2551	. . . . . . . . . . . . . . 15 $/\$ $/\$
182		ioogtlb 37688	. . . . . . . . . . . . . . 15 $/\$ $/\$
183	172, 176, 181, 182	syl3anc 1292	. . . . . . . . . . . . . 14 $/\$ $/\$
184	171, 183	ltned 9788	. . . . . . . . . . . . 13 $/\$ $/\$
185	152, 153, 170, 184	syl3anc 1292	. . . . . . . . . . . 12 $/\$ $/\$ $/\$
186	151, 185	pm2.61dan 808	. . . . . . . . . . 11 $/\$ $/\$
187	117, 118, 120, 186	syl3anc 1292	. . . . . . . . . 10 $/\$ $/\$ $\$ $/\$ $\$
188	63	adantr 472	. . . . . . . . . . . . . . . 16 $\$ $/\$ $\$
189		elioore 11691	. . . . . . . . . . . . . . . . . 18
190	119, 189	syl 17	. . . . . . . . . . . . . . . . 17 $\$
191	190	adantl 473	. . . . . . . . . . . . . . . 16 $\$ $/\$ $\$
192	188, 191	resubcld 10068	. . . . . . . . . . . . . . 15 $\$ $/\$ $\$
193	192	recnd 9687	. . . . . . . . . . . . . 14 $\$ $/\$ $\$
194	193	adantll 728	. . . . . . . . . . . . 13 $/\$ $\$ $/\$ $\$
195	194	abscld 13575	. . . . . . . . . . . 12 $/\$ $\$ $/\$ $\$
196	195	adantllr 733	. . . . . . . . . . 11 $/\$ $/\$ $\$ $/\$ $\$
197	94	adantr 472	. . . . . . . . . . . 12 $/\$ $/\$ $\$ $/\$ $\$
198	15	adantr 472	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $\$
199	190	adantl 473	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $\$
200	198, 199	resubcld 10068	. . . . . . . . . . . . . . 15 $/\$ $/\$ $\$
201	200	recnd 9687	. . . . . . . . . . . . . 14 $/\$ $/\$ $\$
202	201	abscld 13575	. . . . . . . . . . . . 13 $/\$ $/\$ $\$
203	202	adantlr 729	. . . . . . . . . . . 12 $/\$ $/\$ $\$ $/\$ $\$
204	197, 203	readdcld 9688	. . . . . . . . . . 11 $/\$ $/\$ $\$ $/\$ $\$
205	19	ad3antrrr 744	. . . . . . . . . . 11 $/\$ $/\$ $\$ $/\$ $\$
206	118	recnd 9687	. . . . . . . . . . . 12 $/\$ $/\$ $\$ $/\$ $\$
207	190	recnd 9687	. . . . . . . . . . . . 13 $\$
208	207	adantl 473	. . . . . . . . . . . 12 $/\$ $/\$ $\$ $/\$ $\$
209	92	adantr 472	. . . . . . . . . . . 12 $/\$ $/\$ $\$ $/\$ $\$
210	206, 208, 209	abs3difd 13599	. . . . . . . . . . 11 $/\$ $/\$ $\$ $/\$ $\$
211	21	ad2antrr 740	. . . . . . . . . . . . 13 $/\$ $/\$ $\$ $/\$ $\$
212		simpll 768	. . . . . . . . . . . . . . 15 $/\$ $/\$ $\$
213	61	adantl 473	. . . . . . . . . . . . . . 15 $/\$ $/\$ $\$
214	62, 146	sylan2 482	. . . . . . . . . . . . . . . . . 18 $/\$
215	62, 145	sylan2 482	. . . . . . . . . . . . . . . . . 18 $/\$
216	214, 215	abssubd 13592	. . . . . . . . . . . . . . . . 17 $/\$
217	216	3adant1 1048	. . . . . . . . . . . . . . . 16 $/\$ $/\$
218		simp2 1031	. . . . . . . . . . . . . . . . 17 $/\$ $/\$
219	19	rehalfcld 10882	. . . . . . . . . . . . . . . . . 18
220	219	3ad2ant1 1051	. . . . . . . . . . . . . . . . 17 $/\$ $/\$
221		simp3 1032	. . . . . . . . . . . . . . . . 17 $/\$ $/\$
222	218, 220, 221	iooabslt 37692	. . . . . . . . . . . . . . . 16 $/\$ $/\$
223	217, 222	eqbrtrd 4416	. . . . . . . . . . . . . . 15 $/\$ $/\$
224	212, 65, 213, 223	syl3anc 1292	. . . . . . . . . . . . . 14 $/\$ $/\$ $\$
225	224	adantr 472	. . . . . . . . . . . . 13 $/\$ $/\$ $\$ $/\$ $\$
226	212, 65, 213	3jca 1210	. . . . . . . . . . . . . 14 $/\$ $/\$ $\$ $/\$ $/\$
227		simpl 464	. . . . . . . . . . . . . . . . . . 19 $/\$
228	189	adantl 473	. . . . . . . . . . . . . . . . . . 19 $/\$
229	227, 228	resubcld 10068	. . . . . . . . . . . . . . . . . 18 $/\$
230	229	recnd 9687	. . . . . . . . . . . . . . . . 17 $/\$
231	230	abscld 13575	. . . . . . . . . . . . . . . 16 $/\$
232	231	3ad2antl2 1193	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$
233	220	adantr 472	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$
234	214, 215	subcld 10005	. . . . . . . . . . . . . . . . . . 19 $/\$
235	234	abscld 13575	. . . . . . . . . . . . . . . . . 18 $/\$
236	235	3adant1 1048	. . . . . . . . . . . . . . . . 17 $/\$ $/\$
237	236	adantr 472	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$
238		simpl2 1034	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$
239		simpr 468	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$
240	238, 237, 239	iooabslt 37692	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$
241	223	adantr 472	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$
242	232, 237, 233, 240, 241	lttrd 9813	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$
243	232, 233, 242	ltled 9800	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$
244	226, 119, 243	syl2an 485	. . . . . . . . . . . . 13 $/\$ $/\$ $\$ $/\$ $\$
245	197, 203, 211, 211, 225, 244	ltleaddd 10255	. . . . . . . . . . . 12 $/\$ $/\$ $\$ $/\$ $\$
246	19	recnd 9687	. . . . . . . . . . . . . 14
247	246	2halvesd 10881	. . . . . . . . . . . . 13
248	247	ad3antrrr 744	. . . . . . . . . . . 12 $/\$ $/\$ $\$ $/\$ $\$
249	245, 248	breqtrd 4420	. . . . . . . . . . 11 $/\$ $/\$ $\$ $/\$ $\$
250	196, 204, 205, 210, 249	lelttrd 9810	. . . . . . . . . 10 $/\$ $/\$ $\$ $/\$ $\$
251	116, 187, 250	jca32 544	. . . . . . . . 9 $/\$ $/\$ $\$ $/\$ $\$ $/\$ $/\$
252	251	ex 441	. . . . . . . 8 $/\$ $/\$ $\$ $\$ $/\$ $/\$
253	252	eximdv 1772	. . . . . . 7 $/\$ $/\$ $\$ $\$ $/\$ $/\$
254	113, 253	mpd 15	. . . . . 6 $/\$ $/\$ $\$ $/\$ $/\$
255		df-rex 2762	. . . . . 6 $/\$ $/\$ $/\$
256	254, 255	sylibr 217	. . . . 5 $/\$ $/\$ $\$ $/\$
257	256	ex 441	. . . 4 $/\$ $\$ $/\$
258	257	reximdv 2857	. . 3 $/\$ $\$ $/\$
259	59, 258	mpd 15	. 2 $/\$ $/\$
260	3, 259	exlimddv 1789	1 $/\$

Colors of variables: wff setvar class

Syntax hints:

wn 3

wi 4 $/\$ wa 376 $/\$ w3a 1007

wceq 1452

wex 1671

wcel 1904

wne 2641

wral 2756

wrex 2757 $\$ cdif 3387

cin 3389

wss 3390

c0 3722

csn 3959

cuni 4190 class class class wbr 4395

crn 4840

cfv 5589 (class class class)co 6308

cc 9555

cr 9556

cc0 9557

caddc 9560

cxr 9692

clt 9693

cle 9694

cmin 9880

cneg 9881

cdiv 10291

c2 10681

crp 11325

cioo 11660

cabs 13374

ctg 15414

ctop 19994

clp 20227

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1677 ax-4 1690 ax-5 1766 ax-6 1813 ax-7 1859 ax-8 1906 ax-9 1913 ax-10 1932 ax-11 1937 ax-12 1950 ax-13 2104 ax-ext 2451 ax-rep 4508 ax-sep 4518 ax-nul 4527 ax-pow 4579 ax-pr 4639 ax-un 6602 ax-cnex 9613 ax-resscn 9614 ax-1cn 9615 ax-icn 9616 ax-addcl 9617 ax-addrcl 9618 ax-mulcl 9619 ax-mulrcl 9620 ax-mulcom 9621 ax-addass 9622 ax-mulass 9623 ax-distr 9624 ax-i2m1 9625 ax-1ne0 9626 ax-1rid 9627 ax-rnegex 9628 ax-rrecex 9629 ax-cnre 9630 ax-pre-lttri 9631 ax-pre-lttrn 9632 ax-pre-ltadd 9633 ax-pre-mulgt0 9634 ax-pre-sup 9635

This theorem depends on definitions: df-bi 190 df-or 377 df-an 378 df-3or 1008 df-3an 1009 df-tru 1455 df-ex 1672 df-nf 1676 df-sb 1806 df-eu 2323 df-mo 2324 df-clab 2458 df-cleq 2464 df-clel 2467 df-nfc 2601 df-ne 2643 df-nel 2644 df-ral 2761 df-rex 2762 df-reu 2763 df-rmo 2764 df-rab 2765 df-v 3033 df-sbc 3256 df-csb 3350 df-dif 3393 df-un 3395 df-in 3397 df-ss 3404 df-pss 3406 df-nul 3723 df-if 3873 df-pw 3944 df-sn 3960 df-pr 3962 df-tp 3964 df-op 3966 df-uni 4191 df-int 4227 df-iun 4271 df-iin 4272 df-br 4396 df-opab 4455 df-mpt 4456 df-tr 4491 df-eprel 4750 df-id 4754 df-po 4760 df-so 4761 df-fr 4798 df-we 4800 df-xp 4845 df-rel 4846 df-cnv 4847 df-co 4848 df-dm 4849 df-rn 4850 df-res 4851 df-ima 4852 df-pred 5387 df-ord 5433 df-on 5434 df-lim 5435 df-suc 5436 df-iota 5553 df-fun 5591 df-fn 5592 df-f 5593 df-f1 5594 df-fo 5595 df-f1o 5596 df-fv 5597 df-riota 6270 df-ov 6311 df-oprab 6312 df-mpt2 6313 df-om 6712 df-1st 6812 df-2nd 6813 df-wrecs 7046 df-recs 7108 df-rdg 7146 df-er 7381 df-map 7492 df-en 7588 df-dom 7589 df-sdom 7590 df-sup 7974 df-inf 7975 df-pnf 9695 df-mnf 9696 df-xr 9697 df-ltxr 9698 df-le 9699 df-sub 9882 df-neg 9883 df-div 10292 df-nn 10632 df-2 10690 df-3 10691 df-n0 10894 df-z 10962 df-uz 11183 df-q 11288 df-rp 11326 df-xadd 11433 df-ioo 11664 df-seq 12252 df-exp 12311 df-cj 13239 df-re 13240 df-im 13241 df-sqrt 13375 df-abs 13376 df-topgen 15420 df-psmet 19039 df-xmet 19040 df-met 19041 df-bl 19042 df-top 19998 df-bases 19999 df-topon 20000 df-cld 20111 df-ntr 20112 df-cls 20113 df-nei 20191 df-lp 20229

This theorem is referenced by: fourierdlem42 38124 fourierdlem42OLD 38125

W3C validator