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