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 31892

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 3803	. . 3
3	1, 2	sylib 196	. 2
4		simpr 461	. . . . . . . 8 $/\$
5		lptre2pt.j	. . . . . . . . 9
6		lptre2pt.a	. . . . . . . . . 10
7	6	adantr 465	. . . . . . . . 9 $/\$
8		retop 21485	. . . . . . . . . . . 12
9	5, 8	eqeltri 2541	. . . . . . . . . . 11
10		uniretop 21486	. . . . . . . . . . . . 13
11	5	unieqi 4260	. . . . . . . . . . . . 13
12	10, 11	eqtr4i 2489	. . . . . . . . . . . 12
13	12	lpss 19861	. . . . . . . . . . 11 $/\$
14	9, 7, 13	sylancr 663	. . . . . . . . . 10 $/\$
15	14, 4	sseldd 3500	. . . . . . . . 9 $/\$
16	5, 7, 15	islptre 31871	. . . . . . . 8 $/\$ $\$
17	4, 16	mpbid 210	. . . . . . 7 $/\$ $\$
18		lptre2pt.e	. . . . . . . . . . . . 13
19	18	rpred 11281	. . . . . . . . . . . 12
20	19	adantr 465	. . . . . . . . . . 11 $/\$
21	20	rehalfcld 10806	. . . . . . . . . 10 $/\$
22	15, 21	resubcld 10008	. . . . . . . . 9 $/\$
23	22	rexrd 9660	. . . . . . . 8 $/\$
24	15, 21	readdcld 9640	. . . . . . . . 9 $/\$
25	24	rexrd 9660	. . . . . . . 8 $/\$
26	18	rphalfcld 11293	. . . . . . . . . 10
27	26	adantr 465	. . . . . . . . 9 $/\$
28	15, 27	ltsubrpd 11309	. . . . . . . 8 $/\$
29	15, 27	ltaddrpd 11310	. . . . . . . 8 $/\$
30	23, 25, 15, 28, 29	eliood 31777	. . . . . . 7 $/\$
31		oveq1 6303	. . . . . . . . . . 11
32	31	eleq2d 2527	. . . . . . . . . 10
33	31	ineq1d 3695	. . . . . . . . . . 11 $\$ $\$
34	33	neeq1d 2734	. . . . . . . . . 10 $\$ $\$
35	32, 34	imbi12d 320	. . . . . . . . 9 $\$ $\$
36		oveq2 6304	. . . . . . . . . . 11
37	36	eleq2d 2527	. . . . . . . . . 10
38	36	ineq1d 3695	. . . . . . . . . . 11 $\$ $\$
39	38	neeq1d 2734	. . . . . . . . . 10 $\$ $\$
40	37, 39	imbi12d 320	. . . . . . . . 9 $\$ $\$
41	35, 40	rspc2v 3219	. . . . . . . 8 $/\$ $\$ $\$
42	23, 25, 41	syl2anc 661	. . . . . . 7 $/\$ $\$ $\$
43	17, 30, 42	mp2d 45	. . . . . 6 $/\$ $\$
44		n0 3803	. . . . . 6 $\$ $\$
45	43, 44	sylib 196	. . . . 5 $/\$ $\$
46		elinel2 31669	. . . . . . . . . 10 $\$ $\$
47	46	eldifad 3483	. . . . . . . . 9 $\$
48	47	adantl 466	. . . . . . . 8 $/\$ $/\$ $\$
49		elinel1 31670	. . . . . . . . . 10 $\$
50	49	adantl 466	. . . . . . . . 9 $/\$ $/\$ $\$
51	46	eldifbd 3484	. . . . . . . . . 10 $\$
52	51	adantl 466	. . . . . . . . 9 $/\$ $/\$ $\$
53	50, 52	eldifd 3482	. . . . . . . 8 $/\$ $/\$ $\$ $\$
54	48, 53	jca 532	. . . . . . 7 $/\$ $/\$ $\$ $/\$ $\$
55	54	ex 434	. . . . . 6 $/\$ $\$ $/\$ $\$
56	55	eximdv 1711	. . . . 5 $/\$ $\$ $/\$ $\$
57	45, 56	mpd 15	. . . 4 $/\$ $/\$ $\$
58		df-rex 2813	. . . 4 $\$ $/\$ $\$
59	57, 58	sylibr 212	. . 3 $/\$ $\$
60	17	adantr 465	. . . . . . . . 9 $/\$ $/\$ $\$ $\$
61		eldifi 3622	. . . . . . . . . . . 12 $\$
62		elioore 11584	. . . . . . . . . . . 12
63	61, 62	syl 16	. . . . . . . . . . 11 $\$
64	63	adantl 466	. . . . . . . . . 10 $/\$ $/\$ $\$
65	15	adantr 465	. . . . . . . . . 10 $/\$ $/\$ $\$
66		eldifsni 4158	. . . . . . . . . . 11 $\$
67	66	adantl 466	. . . . . . . . . 10 $/\$ $/\$ $\$
68		simpr 461	. . . . . . . . . . . . . 14 $/\$
69		resubcl 9902	. . . . . . . . . . . . . . . 16 $/\$
70	69	recnd 9639	. . . . . . . . . . . . . . 15 $/\$
71	70	abscld 13370	. . . . . . . . . . . . . 14 $/\$
72	68, 71	resubcld 10008	. . . . . . . . . . . . 13 $/\$
73	72	rexrd 9660	. . . . . . . . . . . 12 $/\$
74	73	3adant3 1016	. . . . . . . . . . 11 $/\$ $/\$
75	68, 71	readdcld 9640	. . . . . . . . . . . . 13 $/\$
76	75	rexrd 9660	. . . . . . . . . . . 12 $/\$
77	76	3adant3 1016	. . . . . . . . . . 11 $/\$ $/\$
78		simp2 997	. . . . . . . . . . 11 $/\$ $/\$
79	70	3adant3 1016	. . . . . . . . . . . . 13 $/\$ $/\$
80		recn 9599	. . . . . . . . . . . . . . 15
81	80	3ad2ant1 1017	. . . . . . . . . . . . . 14 $/\$ $/\$
82	78	recnd 9639	. . . . . . . . . . . . . 14 $/\$ $/\$
83		simp3 998	. . . . . . . . . . . . . 14 $/\$ $/\$
84	81, 82, 83	subne0d 9959	. . . . . . . . . . . . 13 $/\$ $/\$
85	79, 84	absrpcld 13382	. . . . . . . . . . . 12 $/\$ $/\$
86	78, 85	ltsubrpd 11309	. . . . . . . . . . 11 $/\$ $/\$
87	78, 85	ltaddrpd 11310	. . . . . . . . . . 11 $/\$ $/\$
88	74, 77, 78, 86, 87	eliood 31777	. . . . . . . . . 10 $/\$ $/\$
89	64, 65, 67, 88	syl3anc 1228	. . . . . . . . 9 $/\$ $/\$ $\$
90	63	recnd 9639	. . . . . . . . . . . . . . 15 $\$
91	90	adantl 466	. . . . . . . . . . . . . 14 $/\$ $/\$ $\$
92	65	recnd 9639	. . . . . . . . . . . . . 14 $/\$ $/\$ $\$
93	91, 92	subcld 9950	. . . . . . . . . . . . 13 $/\$ $/\$ $\$
94	93	abscld 13370	. . . . . . . . . . . 12 $/\$ $/\$ $\$
95	65, 94	resubcld 10008	. . . . . . . . . . 11 $/\$ $/\$ $\$
96	95	rexrd 9660	. . . . . . . . . 10 $/\$ $/\$ $\$
97	65, 94	readdcld 9640	. . . . . . . . . . 11 $/\$ $/\$ $\$
98	97	rexrd 9660	. . . . . . . . . 10 $/\$ $/\$ $\$
99		oveq1 6303	. . . . . . . . . . . . 13
100	99	eleq2d 2527	. . . . . . . . . . . 12
101	99	ineq1d 3695	. . . . . . . . . . . . 13 $\$ $\$
102	101	neeq1d 2734	. . . . . . . . . . . 12 $\$ $\$
103	100, 102	imbi12d 320	. . . . . . . . . . 11 $\$ $\$
104		oveq2 6304	. . . . . . . . . . . . 13
105	104	eleq2d 2527	. . . . . . . . . . . 12
106	104	ineq1d 3695	. . . . . . . . . . . . 13 $\$ $\$
107	106	neeq1d 2734	. . . . . . . . . . . 12 $\$ $\$
108	105, 107	imbi12d 320	. . . . . . . . . . 11 $\$ $\$
109	103, 108	rspc2v 3219	. . . . . . . . . 10 $/\$ $\$ $\$
110	96, 98, 109	syl2anc 661	. . . . . . . . 9 $/\$ $/\$ $\$ $\$ $\$
111	60, 89, 110	mp2d 45	. . . . . . . 8 $/\$ $/\$ $\$ $\$
112		n0 3803	. . . . . . . 8 $\$ $\$
113	111, 112	sylib 196	. . . . . . 7 $/\$ $/\$ $\$ $\$
114		elinel2 31669	. . . . . . . . . . . 12 $\$ $\$
115	114	eldifad 3483	. . . . . . . . . . 11 $\$
116	115	adantl 466	. . . . . . . . . 10 $/\$ $/\$ $\$ $/\$ $\$
117	65	adantr 465	. . . . . . . . . . 11 $/\$ $/\$ $\$ $/\$ $\$
118	64	adantr 465	. . . . . . . . . . 11 $/\$ $/\$ $\$ $/\$ $\$
119		elinel1 31670	. . . . . . . . . . . 12 $\$
120	119	adantl 466	. . . . . . . . . . 11 $/\$ $/\$ $\$ $/\$ $\$
121		simpl1 999	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$
122		simpl2 1000	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$
123		simpl3 1001	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$
124		simpr 461	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$
125	122, 121	subge0d 10163	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$
126	124, 125	mpbid 210	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$
127	121, 122, 126	abssubge0d 13366	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$
128	127	oveq2d 6312	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$
129	127	oveq2d 6312	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$
130	128, 129	oveq12d 6314	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$
131	123, 130	eleqtrd 2547	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$
132		elioore 11584	. . . . . . . . . . . . . . 15
133	132	3ad2ant3 1019	. . . . . . . . . . . . . 14 $/\$ $/\$
134		simpl 457	. . . . . . . . . . . . . . . . . . 19 $/\$
135	69	ancoms 453	. . . . . . . . . . . . . . . . . . 19 $/\$
136	134, 135	resubcld 10008	. . . . . . . . . . . . . . . . . 18 $/\$
137	136	rexrd 9660	. . . . . . . . . . . . . . . . 17 $/\$
138	137	3adant3 1016	. . . . . . . . . . . . . . . 16 $/\$ $/\$
139	134, 135	readdcld 9640	. . . . . . . . . . . . . . . . . 18 $/\$
140	139	rexrd 9660	. . . . . . . . . . . . . . . . 17 $/\$
141	140	3adant3 1016	. . . . . . . . . . . . . . . 16 $/\$ $/\$
142		simp3 998	. . . . . . . . . . . . . . . 16 $/\$ $/\$
143		iooltub 31794	. . . . . . . . . . . . . . . 16 $/\$ $/\$
144	138, 141, 142, 143	syl3anc 1228	. . . . . . . . . . . . . . 15 $/\$ $/\$
145	134	recnd 9639	. . . . . . . . . . . . . . . . 17 $/\$
146	80	adantl 466	. . . . . . . . . . . . . . . . 17 $/\$
147	145, 146	pncan3d 9953	. . . . . . . . . . . . . . . 16 $/\$
148	147	3adant3 1016	. . . . . . . . . . . . . . 15 $/\$ $/\$
149	144, 148	breqtrd 4480	. . . . . . . . . . . . . 14 $/\$ $/\$
150	133, 149	gtned 9737	. . . . . . . . . . . . 13 $/\$ $/\$
151	121, 122, 131, 150	syl3anc 1228	. . . . . . . . . . . 12 $/\$ $/\$ $/\$
152		simpl1 999	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$
153		simpl2 1000	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$
154		simpl3 1001	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$
155	135	adantr 465	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$
156		0red 9614	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$
157		simpr 461	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$
158	155, 156	ltnled 9749	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$
159	157, 158	mpbird 232	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$
160	155, 156, 159	ltled 9750	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$
161	155, 160	absnidd 13348	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$
162	146	adantr 465	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$
163	145	adantr 465	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$
164	162, 163	negsubdi2d 9966	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$
165	161, 164	eqtrd 2498	. . . . . . . . . . . . . . . . 17 $/\$ $/\$
166	165	oveq2d 6312	. . . . . . . . . . . . . . . 16 $/\$ $/\$
167	165	oveq2d 6312	. . . . . . . . . . . . . . . 16 $/\$ $/\$
168	166, 167	oveq12d 6314	. . . . . . . . . . . . . . 15 $/\$ $/\$
169	168	3adantl3 1154	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$
170	154, 169	eleqtrd 2547	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$
171		simp2 997	. . . . . . . . . . . . . 14 $/\$ $/\$
172	171	rexrd 9660	. . . . . . . . . . . . . . 15 $/\$ $/\$
173		resubcl 9902	. . . . . . . . . . . . . . . . . 18 $/\$
174	134, 173	readdcld 9640	. . . . . . . . . . . . . . . . 17 $/\$
175	174	rexrd 9660	. . . . . . . . . . . . . . . 16 $/\$
176	175	3adant3 1016	. . . . . . . . . . . . . . 15 $/\$ $/\$
177		simp3 998	. . . . . . . . . . . . . . . 16 $/\$ $/\$
178	145, 146	nncand 9955	. . . . . . . . . . . . . . . . . 18 $/\$
179	178	oveq1d 6311	. . . . . . . . . . . . . . . . 17 $/\$
180	179	3adant3 1016	. . . . . . . . . . . . . . . 16 $/\$ $/\$
181	177, 180	eleqtrd 2547	. . . . . . . . . . . . . . 15 $/\$ $/\$
182		ioogtlb 31774	. . . . . . . . . . . . . . 15 $/\$ $/\$
183	172, 176, 181, 182	syl3anc 1228	. . . . . . . . . . . . . 14 $/\$ $/\$
184	171, 183	ltned 9738	. . . . . . . . . . . . 13 $/\$ $/\$
185	152, 153, 170, 184	syl3anc 1228	. . . . . . . . . . . 12 $/\$ $/\$ $/\$
186	151, 185	pm2.61dan 791	. . . . . . . . . . 11 $/\$ $/\$
187	117, 118, 120, 186	syl3anc 1228	. . . . . . . . . 10 $/\$ $/\$ $\$ $/\$ $\$
188	63	adantr 465	. . . . . . . . . . . . . . . 16 $\$ $/\$ $\$
189		elioore 11584	. . . . . . . . . . . . . . . . . 18
190	119, 189	syl 16	. . . . . . . . . . . . . . . . 17 $\$
191	190	adantl 466	. . . . . . . . . . . . . . . 16 $\$ $/\$ $\$
192	188, 191	resubcld 10008	. . . . . . . . . . . . . . 15 $\$ $/\$ $\$
193	192	recnd 9639	. . . . . . . . . . . . . 14 $\$ $/\$ $\$
194	193	adantll 713	. . . . . . . . . . . . 13 $/\$ $\$ $/\$ $\$
195	194	abscld 13370	. . . . . . . . . . . 12 $/\$ $\$ $/\$ $\$
196	195	adantllr 718	. . . . . . . . . . 11 $/\$ $/\$ $\$ $/\$ $\$
197	94	adantr 465	. . . . . . . . . . . 12 $/\$ $/\$ $\$ $/\$ $\$
198	15	adantr 465	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $\$
199	190	adantl 466	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $\$
200	198, 199	resubcld 10008	. . . . . . . . . . . . . . 15 $/\$ $/\$ $\$
201	200	recnd 9639	. . . . . . . . . . . . . 14 $/\$ $/\$ $\$
202	201	abscld 13370	. . . . . . . . . . . . 13 $/\$ $/\$ $\$
203	202	adantlr 714	. . . . . . . . . . . 12 $/\$ $/\$ $\$ $/\$ $\$
204	197, 203	readdcld 9640	. . . . . . . . . . 11 $/\$ $/\$ $\$ $/\$ $\$
205	19	ad3antrrr 729	. . . . . . . . . . 11 $/\$ $/\$ $\$ $/\$ $\$
206	118	recnd 9639	. . . . . . . . . . . 12 $/\$ $/\$ $\$ $/\$ $\$
207	190	recnd 9639	. . . . . . . . . . . . 13 $\$
208	207	adantl 466	. . . . . . . . . . . 12 $/\$ $/\$ $\$ $/\$ $\$
209	92	adantr 465	. . . . . . . . . . . 12 $/\$ $/\$ $\$ $/\$ $\$
210	206, 208, 209	abs3difd 13394	. . . . . . . . . . 11 $/\$ $/\$ $\$ $/\$ $\$
211	21	ad2antrr 725	. . . . . . . . . . . . 13 $/\$ $/\$ $\$ $/\$ $\$
212		simpll 753	. . . . . . . . . . . . . . 15 $/\$ $/\$ $\$
213	61	adantl 466	. . . . . . . . . . . . . . 15 $/\$ $/\$ $\$
214	62, 146	sylan2 474	. . . . . . . . . . . . . . . . . 18 $/\$
215	62, 145	sylan2 474	. . . . . . . . . . . . . . . . . 18 $/\$
216	214, 215	abssubd 13387	. . . . . . . . . . . . . . . . 17 $/\$
217	216	3adant1 1014	. . . . . . . . . . . . . . . 16 $/\$ $/\$
218		simp2 997	. . . . . . . . . . . . . . . . 17 $/\$ $/\$
219	19	rehalfcld 10806	. . . . . . . . . . . . . . . . . 18
220	219	3ad2ant1 1017	. . . . . . . . . . . . . . . . 17 $/\$ $/\$
221		simp3 998	. . . . . . . . . . . . . . . . 17 $/\$ $/\$
222	218, 220, 221	iooabslt 31778	. . . . . . . . . . . . . . . 16 $/\$ $/\$
223	217, 222	eqbrtrd 4476	. . . . . . . . . . . . . . 15 $/\$ $/\$
224	212, 65, 213, 223	syl3anc 1228	. . . . . . . . . . . . . 14 $/\$ $/\$ $\$
225	224	adantr 465	. . . . . . . . . . . . 13 $/\$ $/\$ $\$ $/\$ $\$
226	212, 65, 213	3jca 1176	. . . . . . . . . . . . . 14 $/\$ $/\$ $\$ $/\$ $/\$
227		simpl 457	. . . . . . . . . . . . . . . . . . 19 $/\$
228	189	adantl 466	. . . . . . . . . . . . . . . . . . 19 $/\$
229	227, 228	resubcld 10008	. . . . . . . . . . . . . . . . . 18 $/\$
230	229	recnd 9639	. . . . . . . . . . . . . . . . 17 $/\$
231	230	abscld 13370	. . . . . . . . . . . . . . . 16 $/\$
232	231	3ad2antl2 1159	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$
233	220	adantr 465	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$
234	214, 215	subcld 9950	. . . . . . . . . . . . . . . . . . 19 $/\$
235	234	abscld 13370	. . . . . . . . . . . . . . . . . 18 $/\$
236	235	3adant1 1014	. . . . . . . . . . . . . . . . 17 $/\$ $/\$
237	236	adantr 465	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$
238		simpl2 1000	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$
239		simpr 461	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$
240	238, 237, 239	iooabslt 31778	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$
241	223	adantr 465	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$
242	232, 237, 233, 240, 241	lttrd 9760	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$
243	232, 233, 242	ltled 9750	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$
244	226, 119, 243	syl2an 477	. . . . . . . . . . . . 13 $/\$ $/\$ $\$ $/\$ $\$
245	197, 203, 211, 211, 225, 244	ltleaddd 10193	. . . . . . . . . . . 12 $/\$ $/\$ $\$ $/\$ $\$
246	19	recnd 9639	. . . . . . . . . . . . . 14
247	246	2halvesd 10805	. . . . . . . . . . . . 13
248	247	ad3antrrr 729	. . . . . . . . . . . 12 $/\$ $/\$ $\$ $/\$ $\$
249	245, 248	breqtrd 4480	. . . . . . . . . . 11 $/\$ $/\$ $\$ $/\$ $\$
250	196, 204, 205, 210, 249	lelttrd 9757	. . . . . . . . . 10 $/\$ $/\$ $\$ $/\$ $\$
251	116, 187, 250	jca32 535	. . . . . . . . 9 $/\$ $/\$ $\$ $/\$ $\$ $/\$ $/\$
252	251	ex 434	. . . . . . . 8 $/\$ $/\$ $\$ $\$ $/\$ $/\$
253	252	eximdv 1711	. . . . . . 7 $/\$ $/\$ $\$ $\$ $/\$ $/\$
254	113, 253	mpd 15	. . . . . 6 $/\$ $/\$ $\$ $/\$ $/\$
255		df-rex 2813	. . . . . 6 $/\$ $/\$ $/\$
256	254, 255	sylibr 212	. . . . 5 $/\$ $/\$ $\$ $/\$
257	256	ex 434	. . . 4 $/\$ $\$ $/\$
258	257	reximdv 2931	. . 3 $/\$ $\$ $/\$
259	59, 258	mpd 15	. 2 $/\$ $/\$
260	3, 259	exlimddv 1727	1 $/\$

Colors of variables: wff setvar class

Syntax hints:

wn 3

wi 4 $/\$ wa 369 $/\$ w3a 973

wceq 1395

wex 1613

wcel 1819

wne 2652

wral 2807

wrex 2808 $\$ cdif 3468

cin 3470

wss 3471

c0 3793

csn 4032

cuni 4251 class class class wbr 4456

crn 5009

cfv 5594 (class class class)co 6296

cc 9507

cr 9508

cc0 9509

caddc 9512

cxr 9644

clt 9645

cle 9646

cmin 9824

cneg 9825

cdiv 10227

c2 10606

crp 11245

cioo 11554

cabs 13170

ctg 14946

ctop 19612

clp 19853

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1619 ax-4 1632 ax-5 1705 ax-6 1748 ax-7 1791 ax-8 1821 ax-9 1823 ax-10 1838 ax-11 1843 ax-12 1855 ax-13 2000 ax-ext 2435 ax-rep 4568 ax-sep 4578 ax-nul 4586 ax-pow 4634 ax-pr 4695 ax-un 6591 ax-cnex 9565 ax-resscn 9566 ax-1cn 9567 ax-icn 9568 ax-addcl 9569 ax-addrcl 9570 ax-mulcl 9571 ax-mulrcl 9572 ax-mulcom 9573 ax-addass 9574 ax-mulass 9575 ax-distr 9576 ax-i2m1 9577 ax-1ne0 9578 ax-1rid 9579 ax-rnegex 9580 ax-rrecex 9581 ax-cnre 9582 ax-pre-lttri 9583 ax-pre-lttrn 9584 ax-pre-ltadd 9585 ax-pre-mulgt0 9586 ax-pre-sup 9587

This theorem depends on definitions: df-bi 185 df-or 370 df-an 371 df-3or 974 df-3an 975 df-tru 1398 df-ex 1614 df-nf 1618 df-sb 1741 df-eu 2287 df-mo 2288 df-clab 2443 df-cleq 2449 df-clel 2452 df-nfc 2607 df-ne 2654 df-nel 2655 df-ral 2812 df-rex 2813 df-reu 2814 df-rmo 2815 df-rab 2816 df-v 3111 df-sbc 3328 df-csb 3431 df-dif 3474 df-un 3476 df-in 3478 df-ss 3485 df-pss 3487 df-nul 3794 df-if 3945 df-pw 4017 df-sn 4033 df-pr 4035 df-tp 4037 df-op 4039 df-uni 4252 df-int 4289 df-iun 4334 df-iin 4335 df-br 4457 df-opab 4516 df-mpt 4517 df-tr 4551 df-eprel 4800 df-id 4804 df-po 4809 df-so 4810 df-fr 4847 df-we 4849 df-ord 4890 df-on 4891 df-lim 4892 df-suc 4893 df-xp 5014 df-rel 5015 df-cnv 5016 df-co 5017 df-dm 5018 df-rn 5019 df-res 5020 df-ima 5021 df-iota 5557 df-fun 5596 df-fn 5597 df-f 5598 df-f1 5599 df-fo 5600 df-f1o 5601 df-fv 5602 df-riota 6258 df-ov 6299 df-oprab 6300 df-mpt2 6301 df-om 6700 df-1st 6799 df-2nd 6800 df-recs 7060 df-rdg 7094 df-er 7329 df-map 7440 df-en 7536 df-dom 7537 df-sdom 7538 df-sup 7919 df-pnf 9647 df-mnf 9648 df-xr 9649 df-ltxr 9650 df-le 9651 df-sub 9826 df-neg 9827 df-div 10228 df-nn 10557 df-2 10615 df-3 10616 df-n0 10817 df-z 10886 df-uz 11107 df-q 11208 df-rp 11246 df-xadd 11344 df-ioo 11558 df-seq 12111 df-exp 12170 df-cj 13035 df-re 13036 df-im 13037 df-sqrt 13171 df-abs 13172 df-topgen 14952 df-psmet 18629 df-xmet 18630 df-met 18631 df-bl 18632 df-top 19617 df-bases 19619 df-topon 19620 df-cld 19738 df-ntr 19739 df-cls 19740 df-nei 19817 df-lp 19855

This theorem is referenced by: fourierdlem42 32177

W3C validator