This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 ⊢ 𝐽 = ( topGen ‘ ran (,) )
lptre2pt.a ⊢ ( 𝜑 → 𝐴 ⊆ ℝ )
lptre2pt.x ⊢ ( 𝜑 → ( ( limPt ‘ 𝐽 ) ‘ 𝐴 ) ≠ ∅ )
lptre2pt.e ⊢ ( 𝜑 → 𝐸 ∈ ℝ+ )
Assertion lptre2pt ( 𝜑 → ∃ 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ 𝐴 ( 𝑥 ≠ 𝑦 ∧ ( abs ‘ ( 𝑥 − 𝑦 ) ) < 𝐸 ) )

Proof

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