Metamath Proof Explorer

Theorem lptre2pt

Description: If a set in the real line has a limit point than it contains two distinct points that are closer than a given distance. (Contributed by Glauco Siliprandi, 11-Dec-2019)

Ref Expression
Hypotheses lptre2pt.j 
|- J = ( topGen ` ran (,) )
lptre2pt.a 
|- ( ph -> A C_ RR )
lptre2pt.x 
|- ( ph -> ( ( limPt ` J ) ` A ) =/= (/) )
lptre2pt.e 
|- ( ph -> E e. RR+ )
Assertion lptre2pt 
|- ( ph -> E. x e. A E. y e. A ( x =/= y /\ ( abs ` ( x - y ) ) < E ) )

Proof

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