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 ∈ A x ≠ 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 ≠ ∅ ↔ ∃ w w ∈ limPt ⁡ J ⁡ A
6 3 5 sylib ⊢ φ → ∃ w w ∈ 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 ∈ a b → a b ∩ A ∖ w ≠ ∅
18 7 17 mpbid ⊢ φ ∧ w ∈ limPt ⁡ J ⁡ A → ∀ a ∈ ℝ * ∀ b ∈ ℝ * w ∈ a b → a b ∩ A ∖ w ≠ ∅
19 4 rpred ⊢ φ → E ∈ ℝ
20 19 adantr ⊢ φ ∧ w ∈ limPt ⁡ J ⁡ A → E ∈ ℝ
21 20 rehalfcld ⊢ φ ∧ w ∈ limPt ⁡ J ⁡ A → E 2 ∈ ℝ
22 16 21 resubcld ⊢ φ ∧ w ∈ limPt ⁡ J ⁡ A → w − E 2 ∈ ℝ
23 22 rexrd ⊢ φ ∧ w ∈ limPt ⁡ J ⁡ A → w − E 2 ∈ ℝ *
24 16 21 readdcld ⊢ φ ∧ w ∈ limPt ⁡ J ⁡ A → w + E 2 ∈ ℝ
25 24 rexrd ⊢ φ ∧ w ∈ limPt ⁡ J ⁡ A → w + E 2 ∈ ℝ *
26 4 rphalfcld ⊢ φ → E 2 ∈ ℝ +
27 26 adantr ⊢ φ ∧ w ∈ limPt ⁡ J ⁡ A → E 2 ∈ ℝ +
28 16 27 ltsubrpd ⊢ φ ∧ w ∈ limPt ⁡ J ⁡ A → w − E 2 < w
29 16 27 ltaddrpd ⊢ φ ∧ w ∈ limPt ⁡ J ⁡ A → w < w + E 2
30 23 25 16 28 29 eliood ⊢ φ ∧ w ∈ limPt ⁡ J ⁡ A → w ∈ w − E 2 w + E 2
31 oveq1 ⊢ a = w − E 2 → a b = w − E 2 b
32 31 eleq2d ⊢ a = w − E 2 → w ∈ a b ↔ w ∈ w − E 2 b
33 31 ineq1d ⊢ a = w − E 2 → a b ∩ A ∖ w = w − E 2 b ∩ A ∖ w
34 33 neeq1d ⊢ a = w − E 2 → a b ∩ A ∖ w ≠ ∅ ↔ w − E 2 b ∩ A ∖ w ≠ ∅
35 32 34 imbi12d ⊢ a = w − E 2 → w ∈ a b → a b ∩ A ∖ w ≠ ∅ ↔ w ∈ w − E 2 b → w − E 2 b ∩ A ∖ w ≠ ∅
36 oveq2 ⊢ b = w + E 2 → w − E 2 b = w − E 2 w + E 2
37 36 eleq2d ⊢ b = w + E 2 → w ∈ w − E 2 b ↔ w ∈ w − E 2 w + E 2
38 36 ineq1d ⊢ b = w + E 2 → w − E 2 b ∩ A ∖ w = w − E 2 w + E 2 ∩ A ∖ w
39 38 neeq1d ⊢ b = w + E 2 → w − E 2 b ∩ A ∖ w ≠ ∅ ↔ w − E 2 w + E 2 ∩ A ∖ w ≠ ∅
40 37 39 imbi12d ⊢ b = w + E 2 → w ∈ w − E 2 b → w − E 2 b ∩ A ∖ w ≠ ∅ ↔ w ∈ w − E 2 w + E 2 → w − E 2 w + E 2 ∩ A ∖ w ≠ ∅
41 35 40 rspc2v ⊢ w − E 2 ∈ ℝ * ∧ w + E 2 ∈ ℝ * → ∀ a ∈ ℝ * ∀ b ∈ ℝ * w ∈ a b → a b ∩ A ∖ w ≠ ∅ → w ∈ w − E 2 w + E 2 → w − E 2 w + E 2 ∩ A ∖ w ≠ ∅
42 23 25 41 syl2anc ⊢ φ ∧ w ∈ limPt ⁡ J ⁡ A → ∀ a ∈ ℝ * ∀ b ∈ ℝ * w ∈ a b → a b ∩ A ∖ w ≠ ∅ → w ∈ w − E 2 w + E 2 → w − E 2 w + E 2 ∩ A ∖ w ≠ ∅
43 18 30 42 mp2d ⊢ φ ∧ w ∈ limPt ⁡ J ⁡ A → w − E 2 w + E 2 ∩ A ∖ w ≠ ∅
44 n0 ⊢ w − E 2 w + E 2 ∩ A ∖ w ≠ ∅ ↔ ∃ x x ∈ w − E 2 w + E 2 ∩ A ∖ w
45 43 44 sylib ⊢ φ ∧ w ∈ limPt ⁡ J ⁡ A → ∃ x x ∈ w − E 2 w + E 2 ∩ A ∖ w
46 elinel2 ⊢ x ∈ w − E 2 w + E 2 ∩ A ∖ w → x ∈ A ∖ w
47 46 eldifad ⊢ x ∈ w − E 2 w + E 2 ∩ A ∖ w → x ∈ A
48 47 adantl ⊢ φ ∧ w ∈ limPt ⁡ J ⁡ A ∧ x ∈ w − E 2 w + E 2 ∩ A ∖ w → x ∈ A
49 elinel1 ⊢ x ∈ w − E 2 w + E 2 ∩ A ∖ w → x ∈ w − E 2 w + E 2
50 49 adantl ⊢ φ ∧ w ∈ limPt ⁡ J ⁡ A ∧ x ∈ w − E 2 w + E 2 ∩ A ∖ w → x ∈ w − E 2 w + E 2
51 46 eldifbd ⊢ x ∈ w − E 2 w + E 2 ∩ A ∖ w → ¬ x ∈ w
52 51 adantl ⊢ φ ∧ w ∈ limPt ⁡ J ⁡ A ∧ x ∈ w − E 2 w + E 2 ∩ A ∖ w → ¬ x ∈ w
53 50 52 eldifd ⊢ φ ∧ w ∈ limPt ⁡ J ⁡ A ∧ x ∈ w − E 2 w + E 2 ∩ A ∖ w → x ∈ w − E 2 w + E 2 ∖ w
54 48 53 jca ⊢ φ ∧ w ∈ limPt ⁡ J ⁡ A ∧ x ∈ w − E 2 w + E 2 ∩ A ∖ w → x ∈ A ∧ x ∈ w − E 2 w + E 2 ∖ w
55 54 ex ⊢ φ ∧ w ∈ limPt ⁡ J ⁡ A → x ∈ w − E 2 w + E 2 ∩ A ∖ w → x ∈ A ∧ x ∈ w − E 2 w + E 2 ∖ w
56 55 eximdv ⊢ φ ∧ w ∈ limPt ⁡ J ⁡ A → ∃ x x ∈ w − E 2 w + E 2 ∩ A ∖ w → ∃ x x ∈ A ∧ x ∈ w − E 2 w + E 2 ∖ w
57 45 56 mpd ⊢ φ ∧ w ∈ limPt ⁡ J ⁡ A → ∃ x x ∈ A ∧ x ∈ w − E 2 w + E 2 ∖ w
58 df-rex ⊢ ∃ x ∈ A x ∈ w − E 2 w + E 2 ∖ w ↔ ∃ x x ∈ A ∧ x ∈ w − E 2 w + E 2 ∖ w
59 57 58 sylibr ⊢ φ ∧ w ∈ limPt ⁡ J ⁡ A → ∃ x ∈ A x ∈ w − E 2 w + E 2 ∖ w
60 18 adantr ⊢ φ ∧ w ∈ limPt ⁡ J ⁡ A ∧ x ∈ w − E 2 w + E 2 ∖ w → ∀ a ∈ ℝ * ∀ b ∈ ℝ * w ∈ a b → a b ∩ A ∖ w ≠ ∅
61 eldifi ⊢ x ∈ w − E 2 w + E 2 ∖ w → x ∈ w − E 2 w + E 2
62 elioore ⊢ x ∈ w − E 2 w + E 2 → x ∈ ℝ
63 61 62 syl ⊢ x ∈ w − E 2 w + E 2 ∖ w → x ∈ ℝ
64 63 adantl ⊢ φ ∧ w ∈ limPt ⁡ J ⁡ A ∧ x ∈ w − E 2 w + E 2 ∖ w → x ∈ ℝ
65 16 adantr ⊢ φ ∧ w ∈ limPt ⁡ J ⁡ A ∧ x ∈ w − E 2 w + E 2 ∖ w → w ∈ ℝ
66 eldifsni ⊢ x ∈ w − E 2 w + E 2 ∖ w → x ≠ w
67 66 adantl ⊢ φ ∧ w ∈ limPt ⁡ J ⁡ A ∧ x ∈ w − E 2 w + E 2 ∖ 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 − w w + x − w
89 64 65 67 88 syl3anc ⊢ φ ∧ w ∈ limPt ⁡ J ⁡ A ∧ x ∈ w − E 2 w + E 2 ∖ w → w ∈ w − x − w w + x − w
90 63 recnd ⊢ x ∈ w − E 2 w + E 2 ∖ w → x ∈ ℂ
91 90 adantl ⊢ φ ∧ w ∈ limPt ⁡ J ⁡ A ∧ x ∈ w − E 2 w + E 2 ∖ w → x ∈ ℂ
92 65 recnd ⊢ φ ∧ w ∈ limPt ⁡ J ⁡ A ∧ x ∈ w − E 2 w + E 2 ∖ w → w ∈ ℂ
93 91 92 subcld ⊢ φ ∧ w ∈ limPt ⁡ J ⁡ A ∧ x ∈ w − E 2 w + E 2 ∖ w → x − w ∈ ℂ
94 93 abscld ⊢ φ ∧ w ∈ limPt ⁡ J ⁡ A ∧ x ∈ w − E 2 w + E 2 ∖ w → x − w ∈ ℝ
95 65 94 resubcld ⊢ φ ∧ w ∈ limPt ⁡ J ⁡ A ∧ x ∈ w − E 2 w + E 2 ∖ w → w − x − w ∈ ℝ
96 95 rexrd ⊢ φ ∧ w ∈ limPt ⁡ J ⁡ A ∧ x ∈ w − E 2 w + E 2 ∖ w → w − x − w ∈ ℝ *
97 65 94 readdcld ⊢ φ ∧ w ∈ limPt ⁡ J ⁡ A ∧ x ∈ w − E 2 w + E 2 ∖ w → w + x − w ∈ ℝ
98 97 rexrd ⊢ φ ∧ w ∈ limPt ⁡ J ⁡ A ∧ x ∈ w − E 2 w + E 2 ∖ w → w + x − w ∈ ℝ *
99 oveq1 ⊢ a = w − x − w → a b = w − x − w b
100 99 eleq2d ⊢ a = w − x − w → w ∈ a b ↔ w ∈ w − x − w b
101 99 ineq1d ⊢ a = w − x − w → a b ∩ A ∖ w = w − x − w b ∩ A ∖ w
102 101 neeq1d ⊢ a = w − x − w → a b ∩ A ∖ w ≠ ∅ ↔ w − x − w b ∩ A ∖ w ≠ ∅
103 100 102 imbi12d ⊢ a = w − x − w → w ∈ a b → a b ∩ A ∖ w ≠ ∅ ↔ w ∈ w − x − w b → w − x − w b ∩ A ∖ w ≠ ∅
104 oveq2 ⊢ b = w + x − w → w − x − w b = w − x − w w + x − w
105 104 eleq2d ⊢ b = w + x − w → w ∈ w − x − w b ↔ w ∈ w − x − w w + x − w
106 104 ineq1d ⊢ b = w + x − w → w − x − w b ∩ A ∖ w = w − x − w w + x − w ∩ A ∖ w
107 106 neeq1d ⊢ b = w + x − w → w − x − w b ∩ A ∖ w ≠ ∅ ↔ w − x − w w + x − w ∩ A ∖ w ≠ ∅
108 105 107 imbi12d ⊢ b = w + x − w → w ∈ w − x − w b → w − x − w b ∩ A ∖ w ≠ ∅ ↔ w ∈ w − x − w w + x − w → w − x − w w + x − w ∩ A ∖ w ≠ ∅
109 103 108 rspc2v ⊢ w − x − w ∈ ℝ * ∧ w + x − w ∈ ℝ * → ∀ a ∈ ℝ * ∀ b ∈ ℝ * w ∈ a b → a b ∩ A ∖ w ≠ ∅ → w ∈ w − x − w w + x − w → w − x − w w + x − w ∩ A ∖ w ≠ ∅
110 96 98 109 syl2anc ⊢ φ ∧ w ∈ limPt ⁡ J ⁡ A ∧ x ∈ w − E 2 w + E 2 ∖ w → ∀ a ∈ ℝ * ∀ b ∈ ℝ * w ∈ a b → a b ∩ A ∖ w ≠ ∅ → w ∈ w − x − w w + x − w → w − x − w w + x − w ∩ A ∖ w ≠ ∅
111 60 89 110 mp2d ⊢ φ ∧ w ∈ limPt ⁡ J ⁡ A ∧ x ∈ w − E 2 w + E 2 ∖ w → w − x − w w + x − w ∩ A ∖ w ≠ ∅
112 n0 ⊢ w − x − w w + x − w ∩ A ∖ w ≠ ∅ ↔ ∃ y y ∈ w − x − w w + x − w ∩ A ∖ w
113 111 112 sylib ⊢ φ ∧ w ∈ limPt ⁡ J ⁡ A ∧ x ∈ w − E 2 w + E 2 ∖ w → ∃ y y ∈ w − x − w w + x − w ∩ A ∖ w
114 elinel2 ⊢ y ∈ w − x − w w + x − w ∩ A ∖ w → y ∈ A ∖ w
115 114 eldifad ⊢ y ∈ w − x − w w + x − w ∩ A ∖ w → y ∈ A
116 115 adantl ⊢ φ ∧ w ∈ limPt ⁡ J ⁡ A ∧ x ∈ w − E 2 w + E 2 ∖ w ∧ y ∈ w − x − w w + x − w ∩ A ∖ w → y ∈ A
117 65 adantr ⊢ φ ∧ w ∈ limPt ⁡ J ⁡ A ∧ x ∈ w − E 2 w + E 2 ∖ w ∧ y ∈ w − x − w w + x − w ∩ A ∖ w → w ∈ ℝ
118 64 adantr ⊢ φ ∧ w ∈ limPt ⁡ J ⁡ A ∧ x ∈ w − E 2 w + E 2 ∖ w ∧ y ∈ w − x − w w + x − w ∩ A ∖ w → x ∈ ℝ
119 elinel1 ⊢ y ∈ w − x − w w + x − w ∩ A ∖ w → y ∈ w − x − w w + x − w
120 119 adantl ⊢ φ ∧ w ∈ limPt ⁡ J ⁡ A ∧ x ∈ w − E 2 w + E 2 ∖ w ∧ y ∈ w − x − w w + x − w ∩ A ∖ w → y ∈ w − x − w w + x − w
121 simpl1 ⊢ w ∈ ℝ ∧ x ∈ ℝ ∧ y ∈ w − x − w w + x − w ∧ 0 ≤ x − w → w ∈ ℝ
122 simpl2 ⊢ w ∈ ℝ ∧ x ∈ ℝ ∧ y ∈ w − x − w w + x − w ∧ 0 ≤ x − w → x ∈ ℝ
123 simpl3 ⊢ w ∈ ℝ ∧ x ∈ ℝ ∧ y ∈ w − x − w w + x − w ∧ 0 ≤ x − w → y ∈ w − x − w w + x − w
124 simpr ⊢ w ∈ ℝ ∧ x ∈ ℝ ∧ y ∈ w − x − w w + x − w ∧ 0 ≤ x − w → 0 ≤ x − w
125 122 121 subge0d ⊢ w ∈ ℝ ∧ x ∈ ℝ ∧ y ∈ w − x − w w + x − w ∧ 0 ≤ x − w → 0 ≤ x − w ↔ w ≤ x
126 124 125 mpbid ⊢ w ∈ ℝ ∧ x ∈ ℝ ∧ y ∈ w − x − w w + x − w ∧ 0 ≤ x − w → w ≤ x
127 121 122 126 abssubge0d ⊢ w ∈ ℝ ∧ x ∈ ℝ ∧ y ∈ w − x − w w + x − w ∧ 0 ≤ x − w → x − w = x − w
128 127 oveq2d ⊢ w ∈ ℝ ∧ x ∈ ℝ ∧ y ∈ w − x − w w + x − w ∧ 0 ≤ x − w → w − x − w = w − x − w
129 127 oveq2d ⊢ w ∈ ℝ ∧ x ∈ ℝ ∧ y ∈ w − x − w w + x − w ∧ 0 ≤ x − w → w + x − w = w + x - w
130 128 129 oveq12d ⊢ w ∈ ℝ ∧ x ∈ ℝ ∧ y ∈ w − x − w w + x − w ∧ 0 ≤ x − w → w − x − w w + x − w = w − x − w w + x - w
131 123 130 eleqtrd ⊢ w ∈ ℝ ∧ x ∈ ℝ ∧ y ∈ w − x − w w + x − w ∧ 0 ≤ x − w → y ∈ w − x − w w + x - w
132 elioore ⊢ y ∈ w − x − w w + x - w → y ∈ ℝ
133 132 3ad2ant3 ⊢ w ∈ ℝ ∧ x ∈ ℝ ∧ y ∈ w − x − w w + 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 − w w + 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 − w w + x - w → w + x - w ∈ ℝ *
142 simp3 ⊢ w ∈ ℝ ∧ x ∈ ℝ ∧ y ∈ w − x − w w + x - w → y ∈ w − x − w w + x - w
143 iooltub ⊢ w − x − w ∈ ℝ * ∧ w + x - w ∈ ℝ * ∧ y ∈ w − x − w w + x - w → y < w + x - w
144 138 141 142 143 syl3anc ⊢ w ∈ ℝ ∧ x ∈ ℝ ∧ y ∈ w − x − w w + 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 − w w + x - w → w + x - w = x
149 144 148 breqtrd ⊢ w ∈ ℝ ∧ x ∈ ℝ ∧ y ∈ w − x − w w + x - w → y < x
150 133 149 gtned ⊢ w ∈ ℝ ∧ x ∈ ℝ ∧ y ∈ w − x − w w + x - w → x ≠ y
151 121 122 131 150 syl3anc ⊢ w ∈ ℝ ∧ x ∈ ℝ ∧ y ∈ w − x − w w + x − w ∧ 0 ≤ x − w → x ≠ y
152 simpl1 ⊢ w ∈ ℝ ∧ x ∈ ℝ ∧ y ∈ w − x − w w + x − w ∧ ¬ 0 ≤ x − w → w ∈ ℝ
153 simpl2 ⊢ w ∈ ℝ ∧ x ∈ ℝ ∧ y ∈ w − x − w w + x − w ∧ ¬ 0 ≤ x − w → x ∈ ℝ
154 simpl3 ⊢ w ∈ ℝ ∧ x ∈ ℝ ∧ y ∈ w − x − w w + x − w ∧ ¬ 0 ≤ x − w → y ∈ w − x − w w + 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 − w w + x − w = w − w − x w + w - x
169 168 3adantl3 ⊢ w ∈ ℝ ∧ x ∈ ℝ ∧ y ∈ w − x − w w + x − w ∧ ¬ 0 ≤ x − w → w − x − w w + x − w = w − w − x w + w - x
170 154 169 eleqtrd ⊢ w ∈ ℝ ∧ x ∈ ℝ ∧ y ∈ w − x − w w + x − w ∧ ¬ 0 ≤ x − w → y ∈ w − w − x w + w - x
171 simp2 ⊢ w ∈ ℝ ∧ x ∈ ℝ ∧ y ∈ w − w − x w + w - x → x ∈ ℝ
172 171 rexrd ⊢ w ∈ ℝ ∧ x ∈ ℝ ∧ y ∈ w − w − x w + 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 − x w + w - x → w + w - x ∈ ℝ *
177 simp3 ⊢ w ∈ ℝ ∧ x ∈ ℝ ∧ y ∈ w − w − x w + w - x → y ∈ w − w − x w + w - x
178 145 146 nncand ⊢ w ∈ ℝ ∧ x ∈ ℝ → w − w − x = x
179 178 oveq1d ⊢ w ∈ ℝ ∧ x ∈ ℝ → w − w − x w + w - x = x w + w - x
180 179 3adant3 ⊢ w ∈ ℝ ∧ x ∈ ℝ ∧ y ∈ w − w − x w + w - x → w − w − x w + w - x = x w + w - x
181 177 180 eleqtrd ⊢ w ∈ ℝ ∧ x ∈ ℝ ∧ y ∈ w − w − x w + w - x → y ∈ x w + w - x
182 ioogtlb ⊢ x ∈ ℝ * ∧ w + w - x ∈ ℝ * ∧ y ∈ x w + w - x → x < y
183 172 176 181 182 syl3anc ⊢ w ∈ ℝ ∧ x ∈ ℝ ∧ y ∈ w − w − x w + w - x → x < y
184 171 183 ltned ⊢ w ∈ ℝ ∧ x ∈ ℝ ∧ y ∈ w − w − x w + w - x → x ≠ y
185 152 153 170 184 syl3anc ⊢ w ∈ ℝ ∧ x ∈ ℝ ∧ y ∈ w − x − w w + x − w ∧ ¬ 0 ≤ x − w → x ≠ y
186 151 185 pm2.61dan ⊢ w ∈ ℝ ∧ x ∈ ℝ ∧ y ∈ w − x − w w + x − w → x ≠ y
187 117 118 120 186 syl3anc ⊢ φ ∧ w ∈ limPt ⁡ J ⁡ A ∧ x ∈ w − E 2 w + E 2 ∖ w ∧ y ∈ w − x − w w + x − w ∩ A ∖ w → x ≠ y
188 63 adantr ⊢ x ∈ w − E 2 w + E 2 ∖ w ∧ y ∈ w − x − w w + x − w ∩ A ∖ w → x ∈ ℝ
189 elioore ⊢ y ∈ w − x − w w + x − w → y ∈ ℝ
190 119 189 syl ⊢ y ∈ w − x − w w + x − w ∩ A ∖ w → y ∈ ℝ
191 190 adantl ⊢ x ∈ w − E 2 w + E 2 ∖ w ∧ y ∈ w − x − w w + x − w ∩ A ∖ w → y ∈ ℝ
192 188 191 resubcld ⊢ x ∈ w − E 2 w + E 2 ∖ w ∧ y ∈ w − x − w w + x − w ∩ A ∖ w → x − y ∈ ℝ
193 192 recnd ⊢ x ∈ w − E 2 w + E 2 ∖ w ∧ y ∈ w − x − w w + x − w ∩ A ∖ w → x − y ∈ ℂ
194 193 adantll ⊢ φ ∧ x ∈ w − E 2 w + E 2 ∖ w ∧ y ∈ w − x − w w + x − w ∩ A ∖ w → x − y ∈ ℂ
195 194 abscld ⊢ φ ∧ x ∈ w − E 2 w + E 2 ∖ w ∧ y ∈ w − x − w w + x − w ∩ A ∖ w → x − y ∈ ℝ
196 195 adantllr ⊢ φ ∧ w ∈ limPt ⁡ J ⁡ A ∧ x ∈ w − E 2 w + E 2 ∖ w ∧ y ∈ w − x − w w + x − w ∩ A ∖ w → x − y ∈ ℝ
197 94 adantr ⊢ φ ∧ w ∈ limPt ⁡ J ⁡ A ∧ x ∈ w − E 2 w + E 2 ∖ w ∧ y ∈ w − x − w w + x − w ∩ A ∖ w → x − w ∈ ℝ
198 16 adantr ⊢ φ ∧ w ∈ limPt ⁡ J ⁡ A ∧ y ∈ w − x − w w + x − w ∩ A ∖ w → w ∈ ℝ
199 190 adantl ⊢ φ ∧ w ∈ limPt ⁡ J ⁡ A ∧ y ∈ w − x − w w + x − w ∩ A ∖ w → y ∈ ℝ
200 198 199 resubcld ⊢ φ ∧ w ∈ limPt ⁡ J ⁡ A ∧ y ∈ w − x − w w + x − w ∩ A ∖ w → w − y ∈ ℝ
201 200 recnd ⊢ φ ∧ w ∈ limPt ⁡ J ⁡ A ∧ y ∈ w − x − w w + x − w ∩ A ∖ w → w − y ∈ ℂ
202 201 abscld ⊢ φ ∧ w ∈ limPt ⁡ J ⁡ A ∧ y ∈ w − x − w w + x − w ∩ A ∖ w → w − y ∈ ℝ
203 202 adantlr ⊢ φ ∧ w ∈ limPt ⁡ J ⁡ A ∧ x ∈ w − E 2 w + E 2 ∖ w ∧ y ∈ w − x − w w + x − w ∩ A ∖ w → w − y ∈ ℝ
204 197 203 readdcld ⊢ φ ∧ w ∈ limPt ⁡ J ⁡ A ∧ x ∈ w − E 2 w + E 2 ∖ w ∧ y ∈ w − x − w w + x − w ∩ A ∖ w → x − w + w − y ∈ ℝ
205 19 ad3antrrr ⊢ φ ∧ w ∈ limPt ⁡ J ⁡ A ∧ x ∈ w − E 2 w + E 2 ∖ w ∧ y ∈ w − x − w w + x − w ∩ A ∖ w → E ∈ ℝ
206 118 recnd ⊢ φ ∧ w ∈ limPt ⁡ J ⁡ A ∧ x ∈ w − E 2 w + E 2 ∖ w ∧ y ∈ w − x − w w + x − w ∩ A ∖ w → x ∈ ℂ
207 190 recnd ⊢ y ∈ w − x − w w + x − w ∩ A ∖ w → y ∈ ℂ
208 207 adantl ⊢ φ ∧ w ∈ limPt ⁡ J ⁡ A ∧ x ∈ w − E 2 w + E 2 ∖ w ∧ y ∈ w − x − w w + x − w ∩ A ∖ w → y ∈ ℂ
209 92 adantr ⊢ φ ∧ w ∈ limPt ⁡ J ⁡ A ∧ x ∈ w − E 2 w + E 2 ∖ w ∧ y ∈ w − x − w w + x − w ∩ A ∖ w → w ∈ ℂ
210 206 208 209 abs3difd ⊢ φ ∧ w ∈ limPt ⁡ J ⁡ A ∧ x ∈ w − E 2 w + E 2 ∖ w ∧ y ∈ w − x − w w + x − w ∩ A ∖ w → x − y ≤ x − w + w − y
211 21 ad2antrr ⊢ φ ∧ w ∈ limPt ⁡ J ⁡ A ∧ x ∈ w − E 2 w + E 2 ∖ w ∧ y ∈ w − x − w w + x − w ∩ A ∖ w → E 2 ∈ ℝ
212 simpll ⊢ φ ∧ w ∈ limPt ⁡ J ⁡ A ∧ x ∈ w − E 2 w + E 2 ∖ w → φ
213 61 adantl ⊢ φ ∧ w ∈ limPt ⁡ J ⁡ A ∧ x ∈ w − E 2 w + E 2 ∖ w → x ∈ w − E 2 w + E 2
214 62 146 sylan2 ⊢ w ∈ ℝ ∧ x ∈ w − E 2 w + E 2 → x ∈ ℂ
215 62 145 sylan2 ⊢ w ∈ ℝ ∧ x ∈ w − E 2 w + E 2 → w ∈ ℂ
216 214 215 abssubd ⊢ w ∈ ℝ ∧ x ∈ w − E 2 w + E 2 → x − w = w − x
217 216 3adant1 ⊢ φ ∧ w ∈ ℝ ∧ x ∈ w − E 2 w + E 2 → x − w = w − x
218 simp2 ⊢ φ ∧ w ∈ ℝ ∧ x ∈ w − E 2 w + E 2 → w ∈ ℝ
219 19 rehalfcld ⊢ φ → E 2 ∈ ℝ
220 219 3ad2ant1 ⊢ φ ∧ w ∈ ℝ ∧ x ∈ w − E 2 w + E 2 → E 2 ∈ ℝ
221 simp3 ⊢ φ ∧ w ∈ ℝ ∧ x ∈ w − E 2 w + E 2 → x ∈ w − E 2 w + E 2
222 218 220 221 iooabslt ⊢ φ ∧ w ∈ ℝ ∧ x ∈ w − E 2 w + E 2 → w − x < E 2
223 217 222 eqbrtrd ⊢ φ ∧ w ∈ ℝ ∧ x ∈ w − E 2 w + E 2 → x − w < E 2
224 212 65 213 223 syl3anc ⊢ φ ∧ w ∈ limPt ⁡ J ⁡ A ∧ x ∈ w − E 2 w + E 2 ∖ w → x − w < E 2
225 224 adantr ⊢ φ ∧ w ∈ limPt ⁡ J ⁡ A ∧ x ∈ w − E 2 w + E 2 ∖ w ∧ y ∈ w − x − w w + x − w ∩ A ∖ w → x − w < E 2
226 212 65 213 3jca ⊢ φ ∧ w ∈ limPt ⁡ J ⁡ A ∧ x ∈ w − E 2 w + E 2 ∖ w → φ ∧ w ∈ ℝ ∧ x ∈ w − E 2 w + E 2
227 simpl ⊢ w ∈ ℝ ∧ y ∈ w − x − w w + x − w → w ∈ ℝ
228 189 adantl ⊢ w ∈ ℝ ∧ y ∈ w − x − w w + x − w → y ∈ ℝ
229 227 228 resubcld ⊢ w ∈ ℝ ∧ y ∈ w − x − w w + x − w → w − y ∈ ℝ
230 229 recnd ⊢ w ∈ ℝ ∧ y ∈ w − x − w w + x − w → w − y ∈ ℂ
231 230 abscld ⊢ w ∈ ℝ ∧ y ∈ w − x − w w + x − w → w − y ∈ ℝ
232 231 3ad2antl2 ⊢ φ ∧ w ∈ ℝ ∧ x ∈ w − E 2 w + E 2 ∧ y ∈ w − x − w w + x − w → w − y ∈ ℝ
233 220 adantr ⊢ φ ∧ w ∈ ℝ ∧ x ∈ w − E 2 w + E 2 ∧ y ∈ w − x − w w + x − w → E 2 ∈ ℝ
234 214 215 subcld ⊢ w ∈ ℝ ∧ x ∈ w − E 2 w + E 2 → x − w ∈ ℂ
235 234 abscld ⊢ w ∈ ℝ ∧ x ∈ w − E 2 w + E 2 → x − w ∈ ℝ
236 235 3adant1 ⊢ φ ∧ w ∈ ℝ ∧ x ∈ w − E 2 w + E 2 → x − w ∈ ℝ
237 236 adantr ⊢ φ ∧ w ∈ ℝ ∧ x ∈ w − E 2 w + E 2 ∧ y ∈ w − x − w w + x − w → x − w ∈ ℝ
238 simpl2 ⊢ φ ∧ w ∈ ℝ ∧ x ∈ w − E 2 w + E 2 ∧ y ∈ w − x − w w + x − w → w ∈ ℝ
239 simpr ⊢ φ ∧ w ∈ ℝ ∧ x ∈ w − E 2 w + E 2 ∧ y ∈ w − x − w w + x − w → y ∈ w − x − w w + x − w
240 238 237 239 iooabslt ⊢ φ ∧ w ∈ ℝ ∧ x ∈ w − E 2 w + E 2 ∧ y ∈ w − x − w w + x − w → w − y < x − w
241 223 adantr ⊢ φ ∧ w ∈ ℝ ∧ x ∈ w − E 2 w + E 2 ∧ y ∈ w − x − w w + x − w → x − w < E 2
242 232 237 233 240 241 lttrd ⊢ φ ∧ w ∈ ℝ ∧ x ∈ w − E 2 w + E 2 ∧ y ∈ w − x − w w + x − w → w − y < E 2
243 232 233 242 ltled ⊢ φ ∧ w ∈ ℝ ∧ x ∈ w − E 2 w + E 2 ∧ y ∈ w − x − w w + x − w → w − y ≤ E 2
244 226 119 243 syl2an ⊢ φ ∧ w ∈ limPt ⁡ J ⁡ A ∧ x ∈ w − E 2 w + E 2 ∖ w ∧ y ∈ w − x − w w + x − w ∩ A ∖ w → w − y ≤ E 2
245 197 203 211 211 225 244 ltleaddd ⊢ φ ∧ w ∈ limPt ⁡ J ⁡ A ∧ x ∈ w − E 2 w + E 2 ∖ w ∧ y ∈ w − x − w w + x − w ∩ A ∖ w → x − w + w − y < E 2 + E 2
246 19 recnd ⊢ φ → E ∈ ℂ
247 246 2halvesd ⊢ φ → E 2 + E 2 = E
248 247 ad3antrrr ⊢ φ ∧ w ∈ limPt ⁡ J ⁡ A ∧ x ∈ w − E 2 w + E 2 ∖ w ∧ y ∈ w − x − w w + x − w ∩ A ∖ w → E 2 + E 2 = E
249 245 248 breqtrd ⊢ φ ∧ w ∈ limPt ⁡ J ⁡ A ∧ x ∈ w − E 2 w + E 2 ∖ w ∧ y ∈ w − x − w w + x − w ∩ A ∖ w → x − w + w − y < E
250 196 204 205 210 249 lelttrd ⊢ φ ∧ w ∈ limPt ⁡ J ⁡ A ∧ x ∈ w − E 2 w + E 2 ∖ w ∧ y ∈ w − x − w w + x − w ∩ A ∖ w → x − y < E
251 116 187 250 jca32 ⊢ φ ∧ w ∈ limPt ⁡ J ⁡ A ∧ x ∈ w − E 2 w + E 2 ∖ w ∧ y ∈ w − x − w w + x − w ∩ A ∖ w → y ∈ A ∧ x ≠ y ∧ x − y < E
252 251 ex ⊢ φ ∧ w ∈ limPt ⁡ J ⁡ A ∧ x ∈ w − E 2 w + E 2 ∖ w → y ∈ w − x − w w + x − w ∩ A ∖ w → y ∈ A ∧ x ≠ y ∧ x − y < E
253 252 eximdv ⊢ φ ∧ w ∈ limPt ⁡ J ⁡ A ∧ x ∈ w − E 2 w + E 2 ∖ w → ∃ y y ∈ w − x − w w + x − w ∩ A ∖ w → ∃ y y ∈ A ∧ x ≠ y ∧ x − y < E
254 113 253 mpd ⊢ φ ∧ w ∈ limPt ⁡ J ⁡ A ∧ x ∈ w − E 2 w + E 2 ∖ w → ∃ y y ∈ A ∧ x ≠ y ∧ x − y < E
255 df-rex ⊢ ∃ y ∈ A x ≠ y ∧ x − y < E ↔ ∃ y y ∈ A ∧ x ≠ y ∧ x − y < E
256 254 255 sylibr ⊢ φ ∧ w ∈ limPt ⁡ J ⁡ A ∧ x ∈ w − E 2 w + E 2 ∖ w → ∃ y ∈ A x ≠ y ∧ x − y < E
257 256 ex ⊢ φ ∧ w ∈ limPt ⁡ J ⁡ A → x ∈ w − E 2 w + E 2 ∖ w → ∃ y ∈ A x ≠ y ∧ x − y < E
258 257 reximdv ⊢ φ ∧ w ∈ limPt ⁡ J ⁡ A → ∃ x ∈ A x ∈ w − E 2 w + E 2 ∖ w → ∃ x ∈ A ∃ y ∈ A x ≠ y ∧ x − y < E
259 59 258 mpd ⊢ φ ∧ w ∈ limPt ⁡ J ⁡ A → ∃ x ∈ A ∃ y ∈ A x ≠ y ∧ x − y < E
260 6 259 exlimddv ⊢ φ → ∃ x ∈ A ∃ y ∈ A x ≠ y ∧ x − y < E