Metamath Proof Explorer

Theorem lptre2pt

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)

Ref Expression
Hypotheses lptre2pt.j ⊢J=topGen⁡ran⁡.
lptre2pt.a ⊢φ→A⊆ℝ
lptre2pt.x ⊢φ→limPt⁡J⁡A≠∅
lptre2pt.e ⊢φ→E∈ℝ+
Assertion lptre2pt ⊢φ→∃x∈A∃y∈Ax≠y∧x−y<E

Proof

Step Hyp Ref Expression
1 lptre2pt.j ⊢J=topGen⁡ran⁡.
2 lptre2pt.a ⊢φ→A⊆ℝ
3 lptre2pt.x ⊢φ→limPt⁡J⁡A≠∅
4 lptre2pt.e ⊢φ→E∈ℝ+
5 n0 ⊢limPt⁡J⁡A≠∅↔∃ww∈limPt⁡J⁡A
6 3 5 sylib ⊢φ→∃ww∈limPt⁡J⁡A
7 simpr ⊢φ∧w∈limPt⁡J⁡A→w∈limPt⁡J⁡A
8 2 adantr ⊢φ∧w∈limPt⁡J⁡A→A⊆ℝ
9 retop ⊢topGen⁡ran⁡.∈Top
10 1 9 eqeltri ⊢J∈Top
11 uniretop ⊢ℝ=⋃topGen⁡ran⁡.
12 1 unieqi ⊢⋃J=⋃topGen⁡ran⁡.
13 11 12 eqtr4i ⊢ℝ=⋃J
14 13 lpss ⊢J∈Top∧A⊆ℝ→limPt⁡J⁡A⊆ℝ
15 10 8 14 sylancr ⊢φ∧w∈limPt⁡J⁡A→limPt⁡J⁡A⊆ℝ
16 15 7 sseldd ⊢φ∧w∈limPt⁡J⁡A→w∈ℝ
17 1 8 16 islptre ⊢φ∧w∈limPt⁡J⁡A→w∈limPt⁡J⁡A↔∀a∈ℝ*∀b∈ℝ*w∈ab→ab∩A∖w≠∅
18 7 17 mpbid ⊢φ∧w∈limPt⁡J⁡A→∀a∈ℝ*∀b∈ℝ*w∈ab→ab∩A∖w≠∅
19 4 rpred ⊢φ→E∈ℝ
20 19 adantr ⊢φ∧w∈limPt⁡J⁡A→E∈ℝ
21 20 rehalfcld ⊢φ∧w∈limPt⁡J⁡A→E2∈ℝ
22 16 21 resubcld ⊢φ∧w∈limPt⁡J⁡A→w−E2∈ℝ
23 22 rexrd ⊢φ∧w∈limPt⁡J⁡A→w−E2∈ℝ*
24 16 21 readdcld ⊢φ∧w∈limPt⁡J⁡A→w+E2∈ℝ
25 24 rexrd ⊢φ∧w∈limPt⁡J⁡A→w+E2∈ℝ*
26 4 rphalfcld ⊢φ→E2∈ℝ+
27 26 adantr ⊢φ∧w∈limPt⁡J⁡A→E2∈ℝ+
28 16 27 ltsubrpd ⊢φ∧w∈limPt⁡J⁡A→w−E2<w
29 16 27 ltaddrpd ⊢φ∧w∈limPt⁡J⁡A→w<w+E2
30 23 25 16 28 29 eliood ⊢φ∧w∈limPt⁡J⁡A→w∈w−E2w+E2
31 oveq1 ⊢a=w−E2→ab=w−E2b
32 31 eleq2d ⊢a=w−E2→w∈ab↔w∈w−E2b
33 31 ineq1d ⊢a=w−E2→ab∩A∖w=w−E2b∩A∖w
34 33 neeq1d ⊢a=w−E2→ab∩A∖w≠∅↔w−E2b∩A∖w≠∅
35 32 34 imbi12d ⊢a=w−E2→w∈ab→ab∩A∖w≠∅↔w∈w−E2b→w−E2b∩A∖w≠∅
36 oveq2 ⊢b=w+E2→w−E2b=w−E2w+E2
37 36 eleq2d ⊢b=w+E2→w∈w−E2b↔w∈w−E2w+E2
38 36 ineq1d ⊢b=w+E2→w−E2b∩A∖w=w−E2w+E2∩A∖w
39 38 neeq1d ⊢b=w+E2→w−E2b∩A∖w≠∅↔w−E2w+E2∩A∖w≠∅
40 37 39 imbi12d ⊢b=w+E2→w∈w−E2b→w−E2b∩A∖w≠∅↔w∈w−E2w+E2→w−E2w+E2∩A∖w≠∅
41 35 40 rspc2v ⊢w−E2∈ℝ*∧w+E2∈ℝ*→∀a∈ℝ*∀b∈ℝ*w∈ab→ab∩A∖w≠∅→w∈w−E2w+E2→w−E2w+E2∩A∖w≠∅
42 23 25 41 syl2anc ⊢φ∧w∈limPt⁡J⁡A→∀a∈ℝ*∀b∈ℝ*w∈ab→ab∩A∖w≠∅→w∈w−E2w+E2→w−E2w+E2∩A∖w≠∅
43 18 30 42 mp2d ⊢φ∧w∈limPt⁡J⁡A→w−E2w+E2∩A∖w≠∅
44 n0 ⊢w−E2w+E2∩A∖w≠∅↔∃xx∈w−E2w+E2∩A∖w
45 43 44 sylib ⊢φ∧w∈limPt⁡J⁡A→∃xx∈w−E2w+E2∩A∖w
46 elinel2 ⊢x∈w−E2w+E2∩A∖w→x∈A∖w
47 46 eldifad ⊢x∈w−E2w+E2∩A∖w→x∈A
48 47 adantl ⊢φ∧w∈limPt⁡J⁡A∧x∈w−E2w+E2∩A∖w→x∈A
49 elinel1 ⊢x∈w−E2w+E2∩A∖w→x∈w−E2w+E2
50 49 adantl ⊢φ∧w∈limPt⁡J⁡A∧x∈w−E2w+E2∩A∖w→x∈w−E2w+E2
51 46 eldifbd ⊢x∈w−E2w+E2∩A∖w→¬x∈w
52 51 adantl ⊢φ∧w∈limPt⁡J⁡A∧x∈w−E2w+E2∩A∖w→¬x∈w
53 50 52 eldifd ⊢φ∧w∈limPt⁡J⁡A∧x∈w−E2w+E2∩A∖w→x∈w−E2w+E2∖w
54 48 53 jca ⊢φ∧w∈limPt⁡J⁡A∧x∈w−E2w+E2∩A∖w→x∈A∧x∈w−E2w+E2∖w
55 54 ex ⊢φ∧w∈limPt⁡J⁡A→x∈w−E2w+E2∩A∖w→x∈A∧x∈w−E2w+E2∖w
56 55 eximdv ⊢φ∧w∈limPt⁡J⁡A→∃xx∈w−E2w+E2∩A∖w→∃xx∈A∧x∈w−E2w+E2∖w
57 45 56 mpd ⊢φ∧w∈limPt⁡J⁡A→∃xx∈A∧x∈w−E2w+E2∖w
58 df-rex ⊢∃x∈Ax∈w−E2w+E2∖w↔∃xx∈A∧x∈w−E2w+E2∖w
59 57 58 sylibr ⊢φ∧w∈limPt⁡J⁡A→∃x∈Ax∈w−E2w+E2∖w
60 18 adantr ⊢φ∧w∈limPt⁡J⁡A∧x∈w−E2w+E2∖w→∀a∈ℝ*∀b∈ℝ*w∈ab→ab∩A∖w≠∅
61 eldifi ⊢x∈w−E2w+E2∖w→x∈w−E2w+E2
62 elioore ⊢x∈w−E2w+E2→x∈ℝ
63 61 62 syl ⊢x∈w−E2w+E2∖w→x∈ℝ
64 63 adantl ⊢φ∧w∈limPt⁡J⁡A∧x∈w−E2w+E2∖w→x∈ℝ
65 16 adantr ⊢φ∧w∈limPt⁡J⁡A∧x∈w−E2w+E2∖w→w∈ℝ
66 eldifsni ⊢x∈w−E2w+E2∖w→x≠w
67 66 adantl ⊢φ∧w∈limPt⁡J⁡A∧x∈w−E2w+E2∖w→x≠w
68 simpr ⊢x∈ℝ∧w∈ℝ→w∈ℝ
69 resubcl ⊢x∈ℝ∧w∈ℝ→x−w∈ℝ
70 69 recnd ⊢x∈ℝ∧w∈ℝ→x−w∈ℂ
71 70 abscld ⊢x∈ℝ∧w∈ℝ→x−w∈ℝ
72 68 71 resubcld ⊢x∈ℝ∧w∈ℝ→w−x−w∈ℝ
73 72 rexrd ⊢x∈ℝ∧w∈ℝ→w−x−w∈ℝ*
74 73 3adant3 ⊢x∈ℝ∧w∈ℝ∧x≠w→w−x−w∈ℝ*
75 68 71 readdcld ⊢x∈ℝ∧w∈ℝ→w+x−w∈ℝ
76 75 rexrd ⊢x∈ℝ∧w∈ℝ→w+x−w∈ℝ*
77 76 3adant3 ⊢x∈ℝ∧w∈ℝ∧x≠w→w+x−w∈ℝ*
78 simp2 ⊢x∈ℝ∧w∈ℝ∧x≠w→w∈ℝ
79 70 3adant3 ⊢x∈ℝ∧w∈ℝ∧x≠w→x−w∈ℂ
80 recn ⊢x∈ℝ→x∈ℂ
81 80 3ad2ant1 ⊢x∈ℝ∧w∈ℝ∧x≠w→x∈ℂ
82 78 recnd ⊢x∈ℝ∧w∈ℝ∧x≠w→w∈ℂ
83 simp3 ⊢x∈ℝ∧w∈ℝ∧x≠w→x≠w
84 81 82 83 subne0d ⊢x∈ℝ∧w∈ℝ∧x≠w→x−w≠0
85 79 84 absrpcld ⊢x∈ℝ∧w∈ℝ∧x≠w→x−w∈ℝ+
86 78 85 ltsubrpd ⊢x∈ℝ∧w∈ℝ∧x≠w→w−x−w<w
87 78 85 ltaddrpd ⊢x∈ℝ∧w∈ℝ∧x≠w→w<w+x−w
88 74 77 78 86 87 eliood ⊢x∈ℝ∧w∈ℝ∧x≠w→w∈w−x−ww+x−w
89 64 65 67 88 syl3anc ⊢φ∧w∈limPt⁡J⁡A∧x∈w−E2w+E2∖w→w∈w−x−ww+x−w
90 63 recnd ⊢x∈w−E2w+E2∖w→x∈ℂ
91 90 adantl ⊢φ∧w∈limPt⁡J⁡A∧x∈w−E2w+E2∖w→x∈ℂ
92 65 recnd ⊢φ∧w∈limPt⁡J⁡A∧x∈w−E2w+E2∖w→w∈ℂ
93 91 92 subcld ⊢φ∧w∈limPt⁡J⁡A∧x∈w−E2w+E2∖w→x−w∈ℂ
94 93 abscld ⊢φ∧w∈limPt⁡J⁡A∧x∈w−E2w+E2∖w→x−w∈ℝ
95 65 94 resubcld ⊢φ∧w∈limPt⁡J⁡A∧x∈w−E2w+E2∖w→w−x−w∈ℝ
96 95 rexrd ⊢φ∧w∈limPt⁡J⁡A∧x∈w−E2w+E2∖w→w−x−w∈ℝ*
97 65 94 readdcld ⊢φ∧w∈limPt⁡J⁡A∧x∈w−E2w+E2∖w→w+x−w∈ℝ
98 97 rexrd ⊢φ∧w∈limPt⁡J⁡A∧x∈w−E2w+E2∖w→w+x−w∈ℝ*
99 oveq1 ⊢a=w−x−w→ab=w−x−wb
100 99 eleq2d ⊢a=w−x−w→w∈ab↔w∈w−x−wb
101 99 ineq1d ⊢a=w−x−w→ab∩A∖w=w−x−wb∩A∖w
102 101 neeq1d ⊢a=w−x−w→ab∩A∖w≠∅↔w−x−wb∩A∖w≠∅
103 100 102 imbi12d ⊢a=w−x−w→w∈ab→ab∩A∖w≠∅↔w∈w−x−wb→w−x−wb∩A∖w≠∅
104 oveq2 ⊢b=w+x−w→w−x−wb=w−x−ww+x−w
105 104 eleq2d ⊢b=w+x−w→w∈w−x−wb↔w∈w−x−ww+x−w
106 104 ineq1d ⊢b=w+x−w→w−x−wb∩A∖w=w−x−ww+x−w∩A∖w
107 106 neeq1d ⊢b=w+x−w→w−x−wb∩A∖w≠∅↔w−x−ww+x−w∩A∖w≠∅
108 105 107 imbi12d ⊢b=w+x−w→w∈w−x−wb→w−x−wb∩A∖w≠∅↔w∈w−x−ww+x−w→w−x−ww+x−w∩A∖w≠∅
109 103 108 rspc2v ⊢w−x−w∈ℝ*∧w+x−w∈ℝ*→∀a∈ℝ*∀b∈ℝ*w∈ab→ab∩A∖w≠∅→w∈w−x−ww+x−w→w−x−ww+x−w∩A∖w≠∅
110 96 98 109 syl2anc ⊢φ∧w∈limPt⁡J⁡A∧x∈w−E2w+E2∖w→∀a∈ℝ*∀b∈ℝ*w∈ab→ab∩A∖w≠∅→w∈w−x−ww+x−w→w−x−ww+x−w∩A∖w≠∅
111 60 89 110 mp2d ⊢φ∧w∈limPt⁡J⁡A∧x∈w−E2w+E2∖w→w−x−ww+x−w∩A∖w≠∅
112 n0 ⊢w−x−ww+x−w∩A∖w≠∅↔∃yy∈w−x−ww+x−w∩A∖w
113 111 112 sylib ⊢φ∧w∈limPt⁡J⁡A∧x∈w−E2w+E2∖w→∃yy∈w−x−ww+x−w∩A∖w
114 elinel2 ⊢y∈w−x−ww+x−w∩A∖w→y∈A∖w
115 114 eldifad ⊢y∈w−x−ww+x−w∩A∖w→y∈A
116 115 adantl ⊢φ∧w∈limPt⁡J⁡A∧x∈w−E2w+E2∖w∧y∈w−x−ww+x−w∩A∖w→y∈A
117 65 adantr ⊢φ∧w∈limPt⁡J⁡A∧x∈w−E2w+E2∖w∧y∈w−x−ww+x−w∩A∖w→w∈ℝ
118 64 adantr ⊢φ∧w∈limPt⁡J⁡A∧x∈w−E2w+E2∖w∧y∈w−x−ww+x−w∩A∖w→x∈ℝ
119 elinel1 ⊢y∈w−x−ww+x−w∩A∖w→y∈w−x−ww+x−w
120 119 adantl ⊢φ∧w∈limPt⁡J⁡A∧x∈w−E2w+E2∖w∧y∈w−x−ww+x−w∩A∖w→y∈w−x−ww+x−w
121 simpl1 ⊢w∈ℝ∧x∈ℝ∧y∈w−x−ww+x−w∧0≤x−w→w∈ℝ
122 simpl2 ⊢w∈ℝ∧x∈ℝ∧y∈w−x−ww+x−w∧0≤x−w→x∈ℝ
123 simpl3 ⊢w∈ℝ∧x∈ℝ∧y∈w−x−ww+x−w∧0≤x−w→y∈w−x−ww+x−w
124 simpr ⊢w∈ℝ∧x∈ℝ∧y∈w−x−ww+x−w∧0≤x−w→0≤x−w
125 122 121 subge0d ⊢w∈ℝ∧x∈ℝ∧y∈w−x−ww+x−w∧0≤x−w→0≤x−w↔w≤x
126 124 125 mpbid ⊢w∈ℝ∧x∈ℝ∧y∈w−x−ww+x−w∧0≤x−w→w≤x
127 121 122 126 abssubge0d ⊢w∈ℝ∧x∈ℝ∧y∈w−x−ww+x−w∧0≤x−w→x−w=x−w
128 127 oveq2d ⊢w∈ℝ∧x∈ℝ∧y∈w−x−ww+x−w∧0≤x−w→w−x−w=w−x−w
129 127 oveq2d ⊢w∈ℝ∧x∈ℝ∧y∈w−x−ww+x−w∧0≤x−w→w+x−w=w+x-w
130 128 129 oveq12d ⊢w∈ℝ∧x∈ℝ∧y∈w−x−ww+x−w∧0≤x−w→w−x−ww+x−w=w−x−ww+x-w
131 123 130 eleqtrd ⊢w∈ℝ∧x∈ℝ∧y∈w−x−ww+x−w∧0≤x−w→y∈w−x−ww+x-w
132 elioore ⊢y∈w−x−ww+x-w→y∈ℝ
133 132 3ad2ant3 ⊢w∈ℝ∧x∈ℝ∧y∈w−x−ww+x-w→y∈ℝ
134 simpl ⊢w∈ℝ∧x∈ℝ→w∈ℝ
135 69 ancoms ⊢w∈ℝ∧x∈ℝ→x−w∈ℝ
136 134 135 resubcld ⊢w∈ℝ∧x∈ℝ→w−x−w∈ℝ
137 136 rexrd ⊢w∈ℝ∧x∈ℝ→w−x−w∈ℝ*
138 137 3adant3 ⊢w∈ℝ∧x∈ℝ∧y∈w−x−ww+x-w→w−x−w∈ℝ*
139 134 135 readdcld ⊢w∈ℝ∧x∈ℝ→w+x-w∈ℝ
140 139 rexrd ⊢w∈ℝ∧x∈ℝ→w+x-w∈ℝ*
141 140 3adant3 ⊢w∈ℝ∧x∈ℝ∧y∈w−x−ww+x-w→w+x-w∈ℝ*
142 simp3 ⊢w∈ℝ∧x∈ℝ∧y∈w−x−ww+x-w→y∈w−x−ww+x-w
143 iooltub ⊢w−x−w∈ℝ*∧w+x-w∈ℝ*∧y∈w−x−ww+x-w→y<w+x-w
144 138 141 142 143 syl3anc ⊢w∈ℝ∧x∈ℝ∧y∈w−x−ww+x-w→y<w+x-w
145 134 recnd ⊢w∈ℝ∧x∈ℝ→w∈ℂ
146 80 adantl ⊢w∈ℝ∧x∈ℝ→x∈ℂ
147 145 146 pncan3d ⊢w∈ℝ∧x∈ℝ→w+x-w=x
148 147 3adant3 ⊢w∈ℝ∧x∈ℝ∧y∈w−x−ww+x-w→w+x-w=x
149 144 148 breqtrd ⊢w∈ℝ∧x∈ℝ∧y∈w−x−ww+x-w→y<x
150 133 149 gtned ⊢w∈ℝ∧x∈ℝ∧y∈w−x−ww+x-w→x≠y
151 121 122 131 150 syl3anc ⊢w∈ℝ∧x∈ℝ∧y∈w−x−ww+x−w∧0≤x−w→x≠y
152 simpl1 ⊢w∈ℝ∧x∈ℝ∧y∈w−x−ww+x−w∧¬0≤x−w→w∈ℝ
153 simpl2 ⊢w∈ℝ∧x∈ℝ∧y∈w−x−ww+x−w∧¬0≤x−w→x∈ℝ
154 simpl3 ⊢w∈ℝ∧x∈ℝ∧y∈w−x−ww+x−w∧¬0≤x−w→y∈w−x−ww+x−w
155 135 adantr ⊢w∈ℝ∧x∈ℝ∧¬0≤x−w→x−w∈ℝ
156 0red ⊢w∈ℝ∧x∈ℝ∧¬0≤x−w→0∈ℝ
157 simpr ⊢w∈ℝ∧x∈ℝ∧¬0≤x−w→¬0≤x−w
158 155 156 ltnled ⊢w∈ℝ∧x∈ℝ∧¬0≤x−w→x−w<0↔¬0≤x−w
159 157 158 mpbird ⊢w∈ℝ∧x∈ℝ∧¬0≤x−w→x−w<0
160 155 156 159 ltled ⊢w∈ℝ∧x∈ℝ∧¬0≤x−w→x−w≤0
161 155 160 absnidd ⊢w∈ℝ∧x∈ℝ∧¬0≤x−w→x−w=−x−w
162 146 adantr ⊢w∈ℝ∧x∈ℝ∧¬0≤x−w→x∈ℂ
163 145 adantr ⊢w∈ℝ∧x∈ℝ∧¬0≤x−w→w∈ℂ
164 162 163 negsubdi2d ⊢w∈ℝ∧x∈ℝ∧¬0≤x−w→−x−w=w−x
165 161 164 eqtrd ⊢w∈ℝ∧x∈ℝ∧¬0≤x−w→x−w=w−x
166 165 oveq2d ⊢w∈ℝ∧x∈ℝ∧¬0≤x−w→w−x−w=w−w−x
167 165 oveq2d ⊢w∈ℝ∧x∈ℝ∧¬0≤x−w→w+x−w=w+w-x
168 166 167 oveq12d ⊢w∈ℝ∧x∈ℝ∧¬0≤x−w→w−x−ww+x−w=w−w−xw+w-x
169 168 3adantl3 ⊢w∈ℝ∧x∈ℝ∧y∈w−x−ww+x−w∧¬0≤x−w→w−x−ww+x−w=w−w−xw+w-x
170 154 169 eleqtrd ⊢w∈ℝ∧x∈ℝ∧y∈w−x−ww+x−w∧¬0≤x−w→y∈w−w−xw+w-x
171 simp2 ⊢w∈ℝ∧x∈ℝ∧y∈w−w−xw+w-x→x∈ℝ
172 171 rexrd ⊢w∈ℝ∧x∈ℝ∧y∈w−w−xw+w-x→x∈ℝ*
173 resubcl ⊢w∈ℝ∧x∈ℝ→w−x∈ℝ
174 134 173 readdcld ⊢w∈ℝ∧x∈ℝ→w+w-x∈ℝ
175 174 rexrd ⊢w∈ℝ∧x∈ℝ→w+w-x∈ℝ*
176 175 3adant3 ⊢w∈ℝ∧x∈ℝ∧y∈w−w−xw+w-x→w+w-x∈ℝ*
177 simp3 ⊢w∈ℝ∧x∈ℝ∧y∈w−w−xw+w-x→y∈w−w−xw+w-x
178 145 146 nncand ⊢w∈ℝ∧x∈ℝ→w−w−x=x
179 178 oveq1d ⊢w∈ℝ∧x∈ℝ→w−w−xw+w-x=xw+w-x
180 179 3adant3 ⊢w∈ℝ∧x∈ℝ∧y∈w−w−xw+w-x→w−w−xw+w-x=xw+w-x
181 177 180 eleqtrd ⊢w∈ℝ∧x∈ℝ∧y∈w−w−xw+w-x→y∈xw+w-x
182 ioogtlb ⊢x∈ℝ*∧w+w-x∈ℝ*∧y∈xw+w-x→x<y
183 172 176 181 182 syl3anc ⊢w∈ℝ∧x∈ℝ∧y∈w−w−xw+w-x→x<y
184 171 183 ltned ⊢w∈ℝ∧x∈ℝ∧y∈w−w−xw+w-x→x≠y
185 152 153 170 184 syl3anc ⊢w∈ℝ∧x∈ℝ∧y∈w−x−ww+x−w∧¬0≤x−w→x≠y
186 151 185 pm2.61dan ⊢w∈ℝ∧x∈ℝ∧y∈w−x−ww+x−w→x≠y
187 117 118 120 186 syl3anc ⊢φ∧w∈limPt⁡J⁡A∧x∈w−E2w+E2∖w∧y∈w−x−ww+x−w∩A∖w→x≠y
188 63 adantr ⊢x∈w−E2w+E2∖w∧y∈w−x−ww+x−w∩A∖w→x∈ℝ
189 elioore ⊢y∈w−x−ww+x−w→y∈ℝ
190 119 189 syl ⊢y∈w−x−ww+x−w∩A∖w→y∈ℝ
191 190 adantl ⊢x∈w−E2w+E2∖w∧y∈w−x−ww+x−w∩A∖w→y∈ℝ
192 188 191 resubcld ⊢x∈w−E2w+E2∖w∧y∈w−x−ww+x−w∩A∖w→x−y∈ℝ
193 192 recnd ⊢x∈w−E2w+E2∖w∧y∈w−x−ww+x−w∩A∖w→x−y∈ℂ
194 193 adantll ⊢φ∧x∈w−E2w+E2∖w∧y∈w−x−ww+x−w∩A∖w→x−y∈ℂ
195 194 abscld ⊢φ∧x∈w−E2w+E2∖w∧y∈w−x−ww+x−w∩A∖w→x−y∈ℝ
196 195 adantllr ⊢φ∧w∈limPt⁡J⁡A∧x∈w−E2w+E2∖w∧y∈w−x−ww+x−w∩A∖w→x−y∈ℝ
197 94 adantr ⊢φ∧w∈limPt⁡J⁡A∧x∈w−E2w+E2∖w∧y∈w−x−ww+x−w∩A∖w→x−w∈ℝ
198 16 adantr ⊢φ∧w∈limPt⁡J⁡A∧y∈w−x−ww+x−w∩A∖w→w∈ℝ
199 190 adantl ⊢φ∧w∈limPt⁡J⁡A∧y∈w−x−ww+x−w∩A∖w→y∈ℝ
200 198 199 resubcld ⊢φ∧w∈limPt⁡J⁡A∧y∈w−x−ww+x−w∩A∖w→w−y∈ℝ
201 200 recnd ⊢φ∧w∈limPt⁡J⁡A∧y∈w−x−ww+x−w∩A∖w→w−y∈ℂ
202 201 abscld ⊢φ∧w∈limPt⁡J⁡A∧y∈w−x−ww+x−w∩A∖w→w−y∈ℝ
203 202 adantlr ⊢φ∧w∈limPt⁡J⁡A∧x∈w−E2w+E2∖w∧y∈w−x−ww+x−w∩A∖w→w−y∈ℝ
204 197 203 readdcld ⊢φ∧w∈limPt⁡J⁡A∧x∈w−E2w+E2∖w∧y∈w−x−ww+x−w∩A∖w→x−w+w−y∈ℝ
205 19 ad3antrrr ⊢φ∧w∈limPt⁡J⁡A∧x∈w−E2w+E2∖w∧y∈w−x−ww+x−w∩A∖w→E∈ℝ
206 118 recnd ⊢φ∧w∈limPt⁡J⁡A∧x∈w−E2w+E2∖w∧y∈w−x−ww+x−w∩A∖w→x∈ℂ
207 190 recnd ⊢y∈w−x−ww+x−w∩A∖w→y∈ℂ
208 207 adantl ⊢φ∧w∈limPt⁡J⁡A∧x∈w−E2w+E2∖w∧y∈w−x−ww+x−w∩A∖w→y∈ℂ
209 92 adantr ⊢φ∧w∈limPt⁡J⁡A∧x∈w−E2w+E2∖w∧y∈w−x−ww+x−w∩A∖w→w∈ℂ
210 206 208 209 abs3difd ⊢φ∧w∈limPt⁡J⁡A∧x∈w−E2w+E2∖w∧y∈w−x−ww+x−w∩A∖w→x−y≤x−w+w−y
211 21 ad2antrr ⊢φ∧w∈limPt⁡J⁡A∧x∈w−E2w+E2∖w∧y∈w−x−ww+x−w∩A∖w→E2∈ℝ
212 simpll ⊢φ∧w∈limPt⁡J⁡A∧x∈w−E2w+E2∖w→φ
213 61 adantl ⊢φ∧w∈limPt⁡J⁡A∧x∈w−E2w+E2∖w→x∈w−E2w+E2
214 62 146 sylan2 ⊢w∈ℝ∧x∈w−E2w+E2→x∈ℂ
215 62 145 sylan2 ⊢w∈ℝ∧x∈w−E2w+E2→w∈ℂ
216 214 215 abssubd ⊢w∈ℝ∧x∈w−E2w+E2→x−w=w−x
217 216 3adant1 ⊢φ∧w∈ℝ∧x∈w−E2w+E2→x−w=w−x
218 simp2 ⊢φ∧w∈ℝ∧x∈w−E2w+E2→w∈ℝ
219 19 rehalfcld ⊢φ→E2∈ℝ
220 219 3ad2ant1 ⊢φ∧w∈ℝ∧x∈w−E2w+E2→E2∈ℝ
221 simp3 ⊢φ∧w∈ℝ∧x∈w−E2w+E2→x∈w−E2w+E2
222 218 220 221 iooabslt ⊢φ∧w∈ℝ∧x∈w−E2w+E2→w−x<E2
223 217 222 eqbrtrd ⊢φ∧w∈ℝ∧x∈w−E2w+E2→x−w<E2
224 212 65 213 223 syl3anc ⊢φ∧w∈limPt⁡J⁡A∧x∈w−E2w+E2∖w→x−w<E2
225 224 adantr ⊢φ∧w∈limPt⁡J⁡A∧x∈w−E2w+E2∖w∧y∈w−x−ww+x−w∩A∖w→x−w<E2
226 212 65 213 3jca ⊢φ∧w∈limPt⁡J⁡A∧x∈w−E2w+E2∖w→φ∧w∈ℝ∧x∈w−E2w+E2
227 simpl ⊢w∈ℝ∧y∈w−x−ww+x−w→w∈ℝ
228 189 adantl ⊢w∈ℝ∧y∈w−x−ww+x−w→y∈ℝ
229 227 228 resubcld ⊢w∈ℝ∧y∈w−x−ww+x−w→w−y∈ℝ
230 229 recnd ⊢w∈ℝ∧y∈w−x−ww+x−w→w−y∈ℂ
231 230 abscld ⊢w∈ℝ∧y∈w−x−ww+x−w→w−y∈ℝ
232 231 3ad2antl2 ⊢φ∧w∈ℝ∧x∈w−E2w+E2∧y∈w−x−ww+x−w→w−y∈ℝ
233 220 adantr ⊢φ∧w∈ℝ∧x∈w−E2w+E2∧y∈w−x−ww+x−w→E2∈ℝ
234 214 215 subcld ⊢w∈ℝ∧x∈w−E2w+E2→x−w∈ℂ
235 234 abscld ⊢w∈ℝ∧x∈w−E2w+E2→x−w∈ℝ
236 235 3adant1 ⊢φ∧w∈ℝ∧x∈w−E2w+E2→x−w∈ℝ
237 236 adantr ⊢φ∧w∈ℝ∧x∈w−E2w+E2∧y∈w−x−ww+x−w→x−w∈ℝ
238 simpl2 ⊢φ∧w∈ℝ∧x∈w−E2w+E2∧y∈w−x−ww+x−w→w∈ℝ
239 simpr ⊢φ∧w∈ℝ∧x∈w−E2w+E2∧y∈w−x−ww+x−w→y∈w−x−ww+x−w
240 238 237 239 iooabslt ⊢φ∧w∈ℝ∧x∈w−E2w+E2∧y∈w−x−ww+x−w→w−y<x−w
241 223 adantr ⊢φ∧w∈ℝ∧x∈w−E2w+E2∧y∈w−x−ww+x−w→x−w<E2
242 232 237 233 240 241 lttrd ⊢φ∧w∈ℝ∧x∈w−E2w+E2∧y∈w−x−ww+x−w→w−y<E2
243 232 233 242 ltled ⊢φ∧w∈ℝ∧x∈w−E2w+E2∧y∈w−x−ww+x−w→w−y≤E2
244 226 119 243 syl2an ⊢φ∧w∈limPt⁡J⁡A∧x∈w−E2w+E2∖w∧y∈w−x−ww+x−w∩A∖w→w−y≤E2
245 197 203 211 211 225 244 ltleaddd ⊢φ∧w∈limPt⁡J⁡A∧x∈w−E2w+E2∖w∧y∈w−x−ww+x−w∩A∖w→x−w+w−y<E2+E2
246 19 recnd ⊢φ→E∈ℂ
247 246 2halvesd ⊢φ→E2+E2=E
248 247 ad3antrrr ⊢φ∧w∈limPt⁡J⁡A∧x∈w−E2w+E2∖w∧y∈w−x−ww+x−w∩A∖w→E2+E2=E
249 245 248 breqtrd ⊢φ∧w∈limPt⁡J⁡A∧x∈w−E2w+E2∖w∧y∈w−x−ww+x−w∩A∖w→x−w+w−y<E
250 196 204 205 210 249 lelttrd ⊢φ∧w∈limPt⁡J⁡A∧x∈w−E2w+E2∖w∧y∈w−x−ww+x−w∩A∖w→x−y<E
251 116 187 250 jca32 ⊢φ∧w∈limPt⁡J⁡A∧x∈w−E2w+E2∖w∧y∈w−x−ww+x−w∩A∖w→y∈A∧x≠y∧x−y<E
252 251 ex ⊢φ∧w∈limPt⁡J⁡A∧x∈w−E2w+E2∖w→y∈w−x−ww+x−w∩A∖w→y∈A∧x≠y∧x−y<E
253 252 eximdv ⊢φ∧w∈limPt⁡J⁡A∧x∈w−E2w+E2∖w→∃yy∈w−x−ww+x−w∩A∖w→∃yy∈A∧x≠y∧x−y<E
254 113 253 mpd ⊢φ∧w∈limPt⁡J⁡A∧x∈w−E2w+E2∖w→∃yy∈A∧x≠y∧x−y<E
255 df-rex ⊢∃y∈Ax≠y∧x−y<E↔∃yy∈A∧x≠y∧x−y<E
256 254 255 sylibr ⊢φ∧w∈limPt⁡J⁡A∧x∈w−E2w+E2∖w→∃y∈Ax≠y∧x−y<E
257 256 ex ⊢φ∧w∈limPt⁡J⁡A→x∈w−E2w+E2∖w→∃y∈Ax≠y∧x−y<E
258 257 reximdv ⊢φ∧w∈limPt⁡J⁡A→∃x∈Ax∈w−E2w+E2∖w→∃x∈A∃y∈Ax≠y∧x−y<E
259 59 258 mpd ⊢φ∧w∈limPt⁡J⁡A→∃x∈A∃y∈Ax≠y∧x−y<E
260 6 259 exlimddv ⊢φ→∃x∈A∃y∈Ax≠y∧x−y<E