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 ‘ ( 𝑥 − 𝑦 ) ) < 𝐸 ) )