Metamath Proof Explorer

Theorem limclner

Description: For a limit point, both from the left and from the right, of the domain, the limit of the function exits only if the left and the right limits are equal. (Contributed by Glauco Siliprandi, 11-Dec-2019)

Ref Expression
Hypotheses limclner.k ⊢ 𝐾 = ( TopOpen ‘ ℂfld )
limclner.a ⊢ ( 𝜑 → 𝐴 ⊆ ℝ )
limclner.j ⊢ 𝐽 = ( topGen ‘ ran (,) )
limclner.f ⊢ ( 𝜑 → 𝐹 : 𝐴 ⟶ ℂ )
limclner.blp1 ⊢ ( 𝜑 → 𝐵 ∈ ( ( limPt ‘ 𝐽 ) ‘ ( 𝐴 ∩ ( -∞ (,) 𝐵 ) ) ) )
limclner.blp2 ⊢ ( 𝜑 → 𝐵 ∈ ( ( limPt ‘ 𝐽 ) ‘ ( 𝐴 ∩ ( 𝐵 (,) +∞ ) ) ) )
limclner.l ⊢ ( 𝜑 → 𝐿 ∈ ( ( 𝐹 ↾ ( -∞ (,) 𝐵 ) ) limℂ 𝐵 ) )
limclner.r ⊢ ( 𝜑 → 𝑅 ∈ ( ( 𝐹 ↾ ( 𝐵 (,) +∞ ) ) limℂ 𝐵 ) )
limclner.lner ⊢ ( 𝜑 → 𝐿 ≠ 𝑅 )
Assertion limclner ( 𝜑 → ( 𝐹 limℂ 𝐵 ) = ∅ )

Proof

Step Hyp Ref Expression
1 limclner.k ⊢ 𝐾 = ( TopOpen ‘ ℂfld )
2 limclner.a ⊢ ( 𝜑 → 𝐴 ⊆ ℝ )
3 limclner.j ⊢ 𝐽 = ( topGen ‘ ran (,) )
4 limclner.f ⊢ ( 𝜑 → 𝐹 : 𝐴 ⟶ ℂ )
5 limclner.blp1 ⊢ ( 𝜑 → 𝐵 ∈ ( ( limPt ‘ 𝐽 ) ‘ ( 𝐴 ∩ ( -∞ (,) 𝐵 ) ) ) )
6 limclner.blp2 ⊢ ( 𝜑 → 𝐵 ∈ ( ( limPt ‘ 𝐽 ) ‘ ( 𝐴 ∩ ( 𝐵 (,) +∞ ) ) ) )
7 limclner.l ⊢ ( 𝜑 → 𝐿 ∈ ( ( 𝐹 ↾ ( -∞ (,) 𝐵 ) ) limℂ 𝐵 ) )
8 limclner.r ⊢ ( 𝜑 → 𝑅 ∈ ( ( 𝐹 ↾ ( 𝐵 (,) +∞ ) ) limℂ 𝐵 ) )
9 limclner.lner ⊢ ( 𝜑 → 𝐿 ≠ 𝑅 )
10 limccl ⊢ ( ( 𝐹 ↾ ( 𝐵 (,) +∞ ) ) limℂ 𝐵 ) ⊆ ℂ
11 10 8 sselid ⊢ ( 𝜑 → 𝑅 ∈ ℂ )
12 11 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℂ ) ∧ ∀ 𝑦 ∈ ℝ+ ∃ 𝑧 ∈ ℝ+ ∀ 𝑤 ∈ 𝐴 ( ( 𝑤 ≠ 𝐵 ∧ ( abs ‘ ( 𝑤 − 𝐵 ) ) < 𝑧 ) → ( abs ‘ ( ( 𝐹 ‘ 𝑤 ) − 𝑥 ) ) < 𝑦 ) ) → 𝑅 ∈ ℂ )
13 limccl ⊢ ( ( 𝐹 ↾ ( -∞ (,) 𝐵 ) ) limℂ 𝐵 ) ⊆ ℂ
14 13 7 sselid ⊢ ( 𝜑 → 𝐿 ∈ ℂ )
15 14 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℂ ) ∧ ∀ 𝑦 ∈ ℝ+ ∃ 𝑧 ∈ ℝ+ ∀ 𝑤 ∈ 𝐴 ( ( 𝑤 ≠ 𝐵 ∧ ( abs ‘ ( 𝑤 − 𝐵 ) ) < 𝑧 ) → ( abs ‘ ( ( 𝐹 ‘ 𝑤 ) − 𝑥 ) ) < 𝑦 ) ) → 𝐿 ∈ ℂ )
16 12 15 subcld ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℂ ) ∧ ∀ 𝑦 ∈ ℝ+ ∃ 𝑧 ∈ ℝ+ ∀ 𝑤 ∈ 𝐴 ( ( 𝑤 ≠ 𝐵 ∧ ( abs ‘ ( 𝑤 − 𝐵 ) ) < 𝑧 ) → ( abs ‘ ( ( 𝐹 ‘ 𝑤 ) − 𝑥 ) ) < 𝑦 ) ) → ( 𝑅 − 𝐿 ) ∈ ℂ )
17 9 necomd ⊢ ( 𝜑 → 𝑅 ≠ 𝐿 )
18 17 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℂ ) ∧ ∀ 𝑦 ∈ ℝ+ ∃ 𝑧 ∈ ℝ+ ∀ 𝑤 ∈ 𝐴 ( ( 𝑤 ≠ 𝐵 ∧ ( abs ‘ ( 𝑤 − 𝐵 ) ) < 𝑧 ) → ( abs ‘ ( ( 𝐹 ‘ 𝑤 ) − 𝑥 ) ) < 𝑦 ) ) → 𝑅 ≠ 𝐿 )
19 12 15 18 subne0d ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℂ ) ∧ ∀ 𝑦 ∈ ℝ+ ∃ 𝑧 ∈ ℝ+ ∀ 𝑤 ∈ 𝐴 ( ( 𝑤 ≠ 𝐵 ∧ ( abs ‘ ( 𝑤 − 𝐵 ) ) < 𝑧 ) → ( abs ‘ ( ( 𝐹 ‘ 𝑤 ) − 𝑥 ) ) < 𝑦 ) ) → ( 𝑅 − 𝐿 ) ≠ 0 )
20 16 19 absrpcld ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℂ ) ∧ ∀ 𝑦 ∈ ℝ+ ∃ 𝑧 ∈ ℝ+ ∀ 𝑤 ∈ 𝐴 ( ( 𝑤 ≠ 𝐵 ∧ ( abs ‘ ( 𝑤 − 𝐵 ) ) < 𝑧 ) → ( abs ‘ ( ( 𝐹 ‘ 𝑤 ) − 𝑥 ) ) < 𝑦 ) ) → ( abs ‘ ( 𝑅 − 𝐿 ) ) ∈ ℝ+ )
21 4re ⊢ 4 ∈ ℝ
22 4pos ⊢ 0 < 4
23 21 22 elrpii ⊢ 4 ∈ ℝ+
24 23 a1i ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℂ ) ∧ ∀ 𝑦 ∈ ℝ+ ∃ 𝑧 ∈ ℝ+ ∀ 𝑤 ∈ 𝐴 ( ( 𝑤 ≠ 𝐵 ∧ ( abs ‘ ( 𝑤 − 𝐵 ) ) < 𝑧 ) → ( abs ‘ ( ( 𝐹 ‘ 𝑤 ) − 𝑥 ) ) < 𝑦 ) ) → 4 ∈ ℝ+ )
25 20 24 rpdivcld ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℂ ) ∧ ∀ 𝑦 ∈ ℝ+ ∃ 𝑧 ∈ ℝ+ ∀ 𝑤 ∈ 𝐴 ( ( 𝑤 ≠ 𝐵 ∧ ( abs ‘ ( 𝑤 − 𝐵 ) ) < 𝑧 ) → ( abs ‘ ( ( 𝐹 ‘ 𝑤 ) − 𝑥 ) ) < 𝑦 ) ) → ( ( abs ‘ ( 𝑅 − 𝐿 ) ) / 4 ) ∈ ℝ+ )
26 nfv ⊢ Ⅎ 𝑦 ( 𝜑 ∧ 𝑥 ∈ ℂ )
27 nfra1 ⊢ Ⅎ 𝑦 ∀ 𝑦 ∈ ℝ+ ∃ 𝑧 ∈ ℝ+ ∀ 𝑤 ∈ 𝐴 ( ( 𝑤 ≠ 𝐵 ∧ ( abs ‘ ( 𝑤 − 𝐵 ) ) < 𝑧 ) → ( abs ‘ ( ( 𝐹 ‘ 𝑤 ) − 𝑥 ) ) < 𝑦 )
28 26 27 nfan ⊢ Ⅎ 𝑦 ( ( 𝜑 ∧ 𝑥 ∈ ℂ ) ∧ ∀ 𝑦 ∈ ℝ+ ∃ 𝑧 ∈ ℝ+ ∀ 𝑤 ∈ 𝐴 ( ( 𝑤 ≠ 𝐵 ∧ ( abs ‘ ( 𝑤 − 𝐵 ) ) < 𝑧 ) → ( abs ‘ ( ( 𝐹 ‘ 𝑤 ) − 𝑥 ) ) < 𝑦 ) )
29 nfv ⊢ Ⅎ 𝑦 ( ( ( abs ‘ ( 𝑅 − 𝐿 ) ) / 4 ) ∈ ℝ+ → ∃ 𝑎 ∈ 𝐴 ∃ 𝑏 ∈ 𝐴 ( abs ‘ ( 𝑅 − 𝐿 ) ) < ( 4 · ( ( abs ‘ ( 𝑅 − 𝐿 ) ) / 4 ) ) )
30 28 29 nfim ⊢ Ⅎ 𝑦 ( ( ( 𝜑 ∧ 𝑥 ∈ ℂ ) ∧ ∀ 𝑦 ∈ ℝ+ ∃ 𝑧 ∈ ℝ+ ∀ 𝑤 ∈ 𝐴 ( ( 𝑤 ≠ 𝐵 ∧ ( abs ‘ ( 𝑤 − 𝐵 ) ) < 𝑧 ) → ( abs ‘ ( ( 𝐹 ‘ 𝑤 ) − 𝑥 ) ) < 𝑦 ) ) → ( ( ( abs ‘ ( 𝑅 − 𝐿 ) ) / 4 ) ∈ ℝ+ → ∃ 𝑎 ∈ 𝐴 ∃ 𝑏 ∈ 𝐴 ( abs ‘ ( 𝑅 − 𝐿 ) ) < ( 4 · ( ( abs ‘ ( 𝑅 − 𝐿 ) ) / 4 ) ) ) )
31 ovex ⊢ ( ( abs ‘ ( 𝑅 − 𝐿 ) ) / 4 ) ∈ V
32 eleq1 ⊢ ( 𝑦 = ( ( abs ‘ ( 𝑅 − 𝐿 ) ) / 4 ) → ( 𝑦 ∈ ℝ+ ↔ ( ( abs ‘ ( 𝑅 − 𝐿 ) ) / 4 ) ∈ ℝ+ ) )
33 oveq2 ⊢ ( 𝑦 = ( ( abs ‘ ( 𝑅 − 𝐿 ) ) / 4 ) → ( 4 · 𝑦 ) = ( 4 · ( ( abs ‘ ( 𝑅 − 𝐿 ) ) / 4 ) ) )
34 33 breq2d ⊢ ( 𝑦 = ( ( abs ‘ ( 𝑅 − 𝐿 ) ) / 4 ) → ( ( abs ‘ ( 𝑅 − 𝐿 ) ) < ( 4 · 𝑦 ) ↔ ( abs ‘ ( 𝑅 − 𝐿 ) ) < ( 4 · ( ( abs ‘ ( 𝑅 − 𝐿 ) ) / 4 ) ) ) )
35 34 2rexbidv ⊢ ( 𝑦 = ( ( abs ‘ ( 𝑅 − 𝐿 ) ) / 4 ) → ( ∃ 𝑎 ∈ 𝐴 ∃ 𝑏 ∈ 𝐴 ( abs ‘ ( 𝑅 − 𝐿 ) ) < ( 4 · 𝑦 ) ↔ ∃ 𝑎 ∈ 𝐴 ∃ 𝑏 ∈ 𝐴 ( abs ‘ ( 𝑅 − 𝐿 ) ) < ( 4 · ( ( abs ‘ ( 𝑅 − 𝐿 ) ) / 4 ) ) ) )
36 32 35 imbi12d ⊢ ( 𝑦 = ( ( abs ‘ ( 𝑅 − 𝐿 ) ) / 4 ) → ( ( 𝑦 ∈ ℝ+ → ∃ 𝑎 ∈ 𝐴 ∃ 𝑏 ∈ 𝐴 ( abs ‘ ( 𝑅 − 𝐿 ) ) < ( 4 · 𝑦 ) ) ↔ ( ( ( abs ‘ ( 𝑅 − 𝐿 ) ) / 4 ) ∈ ℝ+ → ∃ 𝑎 ∈ 𝐴 ∃ 𝑏 ∈ 𝐴 ( abs ‘ ( 𝑅 − 𝐿 ) ) < ( 4 · ( ( abs ‘ ( 𝑅 − 𝐿 ) ) / 4 ) ) ) ) )
37 36 imbi2d ⊢ ( 𝑦 = ( ( abs ‘ ( 𝑅 − 𝐿 ) ) / 4 ) → ( ( ( ( 𝜑 ∧ 𝑥 ∈ ℂ ) ∧ ∀ 𝑦 ∈ ℝ+ ∃ 𝑧 ∈ ℝ+ ∀ 𝑤 ∈ 𝐴 ( ( 𝑤 ≠ 𝐵 ∧ ( abs ‘ ( 𝑤 − 𝐵 ) ) < 𝑧 ) → ( abs ‘ ( ( 𝐹 ‘ 𝑤 ) − 𝑥 ) ) < 𝑦 ) ) → ( 𝑦 ∈ ℝ+ → ∃ 𝑎 ∈ 𝐴 ∃ 𝑏 ∈ 𝐴 ( abs ‘ ( 𝑅 − 𝐿 ) ) < ( 4 · 𝑦 ) ) ) ↔ ( ( ( 𝜑 ∧ 𝑥 ∈ ℂ ) ∧ ∀ 𝑦 ∈ ℝ+ ∃ 𝑧 ∈ ℝ+ ∀ 𝑤 ∈ 𝐴 ( ( 𝑤 ≠ 𝐵 ∧ ( abs ‘ ( 𝑤 − 𝐵 ) ) < 𝑧 ) → ( abs ‘ ( ( 𝐹 ‘ 𝑤 ) − 𝑥 ) ) < 𝑦 ) ) → ( ( ( abs ‘ ( 𝑅 − 𝐿 ) ) / 4 ) ∈ ℝ+ → ∃ 𝑎 ∈ 𝐴 ∃ 𝑏 ∈ 𝐴 ( abs ‘ ( 𝑅 − 𝐿 ) ) < ( 4 · ( ( abs ‘ ( 𝑅 − 𝐿 ) ) / 4 ) ) ) ) ) )
38 simpll ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ ℂ ) ∧ ∀ 𝑦 ∈ ℝ+ ∃ 𝑧 ∈ ℝ+ ∀ 𝑤 ∈ 𝐴 ( ( 𝑤 ≠ 𝐵 ∧ ( abs ‘ ( 𝑤 − 𝐵 ) ) < 𝑧 ) → ( abs ‘ ( ( 𝐹 ‘ 𝑤 ) − 𝑥 ) ) < 𝑦 ) ) ∧ 𝑦 ∈ ℝ+ ) → ( 𝜑 ∧ 𝑥 ∈ ℂ ) )
39 simpr ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ ℂ ) ∧ ∀ 𝑦 ∈ ℝ+ ∃ 𝑧 ∈ ℝ+ ∀ 𝑤 ∈ 𝐴 ( ( 𝑤 ≠ 𝐵 ∧ ( abs ‘ ( 𝑤 − 𝐵 ) ) < 𝑧 ) → ( abs ‘ ( ( 𝐹 ‘ 𝑤 ) − 𝑥 ) ) < 𝑦 ) ) ∧ 𝑦 ∈ ℝ+ ) → 𝑦 ∈ ℝ+ )
40 rspa ⊢ ( ( ∀ 𝑦 ∈ ℝ+ ∃ 𝑧 ∈ ℝ+ ∀ 𝑤 ∈ 𝐴 ( ( 𝑤 ≠ 𝐵 ∧ ( abs ‘ ( 𝑤 − 𝐵 ) ) < 𝑧 ) → ( abs ‘ ( ( 𝐹 ‘ 𝑤 ) − 𝑥 ) ) < 𝑦 ) ∧ 𝑦 ∈ ℝ+ ) → ∃ 𝑧 ∈ ℝ+ ∀ 𝑤 ∈ 𝐴 ( ( 𝑤 ≠ 𝐵 ∧ ( abs ‘ ( 𝑤 − 𝐵 ) ) < 𝑧 ) → ( abs ‘ ( ( 𝐹 ‘ 𝑤 ) − 𝑥 ) ) < 𝑦 ) )
41 40 adantll ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ ℂ ) ∧ ∀ 𝑦 ∈ ℝ+ ∃ 𝑧 ∈ ℝ+ ∀ 𝑤 ∈ 𝐴 ( ( 𝑤 ≠ 𝐵 ∧ ( abs ‘ ( 𝑤 − 𝐵 ) ) < 𝑧 ) → ( abs ‘ ( ( 𝐹 ‘ 𝑤 ) − 𝑥 ) ) < 𝑦 ) ) ∧ 𝑦 ∈ ℝ+ ) → ∃ 𝑧 ∈ ℝ+ ∀ 𝑤 ∈ 𝐴 ( ( 𝑤 ≠ 𝐵 ∧ ( abs ‘ ( 𝑤 − 𝐵 ) ) < 𝑧 ) → ( abs ‘ ( ( 𝐹 ‘ 𝑤 ) − 𝑥 ) ) < 𝑦 ) )
42 fresin ⊢ ( 𝐹 : 𝐴 ⟶ ℂ → ( 𝐹 ↾ ( 𝐵 (,) +∞ ) ) : ( 𝐴 ∩ ( 𝐵 (,) +∞ ) ) ⟶ ℂ )
43 4 42 syl ⊢ ( 𝜑 → ( 𝐹 ↾ ( 𝐵 (,) +∞ ) ) : ( 𝐴 ∩ ( 𝐵 (,) +∞ ) ) ⟶ ℂ )
44 inss2 ⊢ ( 𝐴 ∩ ( 𝐵 (,) +∞ ) ) ⊆ ( 𝐵 (,) +∞ )
45 ioosscn ⊢ ( 𝐵 (,) +∞ ) ⊆ ℂ
46 44 45 sstri ⊢ ( 𝐴 ∩ ( 𝐵 (,) +∞ ) ) ⊆ ℂ
47 46 a1i ⊢ ( 𝜑 → ( 𝐴 ∩ ( 𝐵 (,) +∞ ) ) ⊆ ℂ )
48 retop ⊢ ( topGen ‘ ran (,) ) ∈ Top
49 3 48 eqeltri ⊢ 𝐽 ∈ Top
50 inss2 ⊢ ( 𝐴 ∩ ( -∞ (,) 𝐵 ) ) ⊆ ( -∞ (,) 𝐵 )
51 ioossre ⊢ ( -∞ (,) 𝐵 ) ⊆ ℝ
52 50 51 sstri ⊢ ( 𝐴 ∩ ( -∞ (,) 𝐵 ) ) ⊆ ℝ
53 uniretop ⊢ ℝ = ∪ ( topGen ‘ ran (,) )
54 3 unieqi ⊢ ∪ 𝐽 = ∪ ( topGen ‘ ran (,) )
55 53 54 eqtr4i ⊢ ℝ = ∪ 𝐽
56 55 lpss ⊢ ( ( 𝐽 ∈ Top ∧ ( 𝐴 ∩ ( -∞ (,) 𝐵 ) ) ⊆ ℝ ) → ( ( limPt ‘ 𝐽 ) ‘ ( 𝐴 ∩ ( -∞ (,) 𝐵 ) ) ) ⊆ ℝ )
57 49 52 56 mp2an ⊢ ( ( limPt ‘ 𝐽 ) ‘ ( 𝐴 ∩ ( -∞ (,) 𝐵 ) ) ) ⊆ ℝ
58 57 5 sselid ⊢ ( 𝜑 → 𝐵 ∈ ℝ )
59 58 recnd ⊢ ( 𝜑 → 𝐵 ∈ ℂ )
60 43 47 59 ellimc3 ⊢ ( 𝜑 → ( 𝑅 ∈ ( ( 𝐹 ↾ ( 𝐵 (,) +∞ ) ) limℂ 𝐵 ) ↔ ( 𝑅 ∈ ℂ ∧ ∀ 𝑦 ∈ ℝ+ ∃ 𝑣 ∈ ℝ+ ∀ 𝑤 ∈ ( 𝐴 ∩ ( 𝐵 (,) +∞ ) ) ( ( 𝑤 ≠ 𝐵 ∧ ( abs ‘ ( 𝑤 − 𝐵 ) ) < 𝑣 ) → ( abs ‘ ( ( ( 𝐹 ↾ ( 𝐵 (,) +∞ ) ) ‘ 𝑤 ) − 𝑅 ) ) < 𝑦 ) ) ) )
61 8 60 mpbid ⊢ ( 𝜑 → ( 𝑅 ∈ ℂ ∧ ∀ 𝑦 ∈ ℝ+ ∃ 𝑣 ∈ ℝ+ ∀ 𝑤 ∈ ( 𝐴 ∩ ( 𝐵 (,) +∞ ) ) ( ( 𝑤 ≠ 𝐵 ∧ ( abs ‘ ( 𝑤 − 𝐵 ) ) < 𝑣 ) → ( abs ‘ ( ( ( 𝐹 ↾ ( 𝐵 (,) +∞ ) ) ‘ 𝑤 ) − 𝑅 ) ) < 𝑦 ) ) )
62 61 simprd ⊢ ( 𝜑 → ∀ 𝑦 ∈ ℝ+ ∃ 𝑣 ∈ ℝ+ ∀ 𝑤 ∈ ( 𝐴 ∩ ( 𝐵 (,) +∞ ) ) ( ( 𝑤 ≠ 𝐵 ∧ ( abs ‘ ( 𝑤 − 𝐵 ) ) < 𝑣 ) → ( abs ‘ ( ( ( 𝐹 ↾ ( 𝐵 (,) +∞ ) ) ‘ 𝑤 ) − 𝑅 ) ) < 𝑦 ) )
63 62 r19.21bi ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ℝ+ ) → ∃ 𝑣 ∈ ℝ+ ∀ 𝑤 ∈ ( 𝐴 ∩ ( 𝐵 (,) +∞ ) ) ( ( 𝑤 ≠ 𝐵 ∧ ( abs ‘ ( 𝑤 − 𝐵 ) ) < 𝑣 ) → ( abs ‘ ( ( ( 𝐹 ↾ ( 𝐵 (,) +∞ ) ) ‘ 𝑤 ) − 𝑅 ) ) < 𝑦 ) )
64 63 3ad2ant1 ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ+ ) ∧ 𝑧 ∈ ℝ+ ∧ ∀ 𝑤 ∈ 𝐴 ( ( 𝑤 ≠ 𝐵 ∧ ( abs ‘ ( 𝑤 − 𝐵 ) ) < 𝑧 ) → ( abs ‘ ( ( 𝐹 ‘ 𝑤 ) − 𝑥 ) ) < 𝑦 ) ) → ∃ 𝑣 ∈ ℝ+ ∀ 𝑤 ∈ ( 𝐴 ∩ ( 𝐵 (,) +∞ ) ) ( ( 𝑤 ≠ 𝐵 ∧ ( abs ‘ ( 𝑤 − 𝐵 ) ) < 𝑣 ) → ( abs ‘ ( ( ( 𝐹 ↾ ( 𝐵 (,) +∞ ) ) ‘ 𝑤 ) − 𝑅 ) ) < 𝑦 ) )
65 simp11l ⊢ ( ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ+ ) ∧ 𝑧 ∈ ℝ+ ∧ ∀ 𝑤 ∈ 𝐴 ( ( 𝑤 ≠ 𝐵 ∧ ( abs ‘ ( 𝑤 − 𝐵 ) ) < 𝑧 ) → ( abs ‘ ( ( 𝐹 ‘ 𝑤 ) − 𝑥 ) ) < 𝑦 ) ) ∧ 𝑣 ∈ ℝ+ ∧ ∀ 𝑤 ∈ ( 𝐴 ∩ ( 𝐵 (,) +∞ ) ) ( ( 𝑤 ≠ 𝐵 ∧ ( abs ‘ ( 𝑤 − 𝐵 ) ) < 𝑣 ) → ( abs ‘ ( ( ( 𝐹 ↾ ( 𝐵 (,) +∞ ) ) ‘ 𝑤 ) − 𝑅 ) ) < 𝑦 ) ) → 𝜑 )
66 simp12 ⊢ ( ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ+ ) ∧ 𝑧 ∈ ℝ+ ∧ ∀ 𝑤 ∈ 𝐴 ( ( 𝑤 ≠ 𝐵 ∧ ( abs ‘ ( 𝑤 − 𝐵 ) ) < 𝑧 ) → ( abs ‘ ( ( 𝐹 ‘ 𝑤 ) − 𝑥 ) ) < 𝑦 ) ) ∧ 𝑣 ∈ ℝ+ ∧ ∀ 𝑤 ∈ ( 𝐴 ∩ ( 𝐵 (,) +∞ ) ) ( ( 𝑤 ≠ 𝐵 ∧ ( abs ‘ ( 𝑤 − 𝐵 ) ) < 𝑣 ) → ( abs ‘ ( ( ( 𝐹 ↾ ( 𝐵 (,) +∞ ) ) ‘ 𝑤 ) − 𝑅 ) ) < 𝑦 ) ) → 𝑧 ∈ ℝ+ )
67 simp2 ⊢ ( ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ+ ) ∧ 𝑧 ∈ ℝ+ ∧ ∀ 𝑤 ∈ 𝐴 ( ( 𝑤 ≠ 𝐵 ∧ ( abs ‘ ( 𝑤 − 𝐵 ) ) < 𝑧 ) → ( abs ‘ ( ( 𝐹 ‘ 𝑤 ) − 𝑥 ) ) < 𝑦 ) ) ∧ 𝑣 ∈ ℝ+ ∧ ∀ 𝑤 ∈ ( 𝐴 ∩ ( 𝐵 (,) +∞ ) ) ( ( 𝑤 ≠ 𝐵 ∧ ( abs ‘ ( 𝑤 − 𝐵 ) ) < 𝑣 ) → ( abs ‘ ( ( ( 𝐹 ↾ ( 𝐵 (,) +∞ ) ) ‘ 𝑤 ) − 𝑅 ) ) < 𝑦 ) ) → 𝑣 ∈ ℝ+ )
68 breq2 ⊢ ( 𝑢 = if ( 𝑧 ≤ 𝑣 , 𝑧 , 𝑣 ) → ( ( abs ‘ ( 𝑏 − 𝐵 ) ) < 𝑢 ↔ ( abs ‘ ( 𝑏 − 𝐵 ) ) < if ( 𝑧 ≤ 𝑣 , 𝑧 , 𝑣 ) ) )
69 68 rexbidv ⊢ ( 𝑢 = if ( 𝑧 ≤ 𝑣 , 𝑧 , 𝑣 ) → ( ∃ 𝑏 ∈ ( ( 𝐴 ∩ ( 𝐵 (,) +∞ ) ) ∖ { 𝐵 } ) ( abs ‘ ( 𝑏 − 𝐵 ) ) < 𝑢 ↔ ∃ 𝑏 ∈ ( ( 𝐴 ∩ ( 𝐵 (,) +∞ ) ) ∖ { 𝐵 } ) ( abs ‘ ( 𝑏 − 𝐵 ) ) < if ( 𝑧 ≤ 𝑣 , 𝑧 , 𝑣 ) ) )
70 inss1 ⊢ ( ( ( limPt ‘ 𝐾 ) ‘ ( 𝐴 ∩ ( 𝐵 (,) +∞ ) ) ) ∩ ℝ ) ⊆ ( ( limPt ‘ 𝐾 ) ‘ ( 𝐴 ∩ ( 𝐵 (,) +∞ ) ) )
71 70 a1i ⊢ ( 𝜑 → ( ( ( limPt ‘ 𝐾 ) ‘ ( 𝐴 ∩ ( 𝐵 (,) +∞ ) ) ) ∩ ℝ ) ⊆ ( ( limPt ‘ 𝐾 ) ‘ ( 𝐴 ∩ ( 𝐵 (,) +∞ ) ) ) )
72 1 cnfldtop ⊢ 𝐾 ∈ Top
73 72 a1i ⊢ ( 𝜑 → 𝐾 ∈ Top )
74 ax-resscn ⊢ ℝ ⊆ ℂ
75 74 a1i ⊢ ( 𝜑 → ℝ ⊆ ℂ )
76 ioossre ⊢ ( 𝐵 (,) +∞ ) ⊆ ℝ
77 44 76 sstri ⊢ ( 𝐴 ∩ ( 𝐵 (,) +∞ ) ) ⊆ ℝ
78 77 a1i ⊢ ( 𝜑 → ( 𝐴 ∩ ( 𝐵 (,) +∞ ) ) ⊆ ℝ )
79 unicntop ⊢ ℂ = ∪ ( TopOpen ‘ ℂfld )
80 1 unieqi ⊢ ∪ 𝐾 = ∪ ( TopOpen ‘ ℂfld )
81 79 80 eqtr4i ⊢ ℂ = ∪ 𝐾
82 1 tgioo2 ⊢ ( topGen ‘ ran (,) ) = ( 𝐾 ↾t ℝ )
83 3 82 eqtri ⊢ 𝐽 = ( 𝐾 ↾t ℝ )
84 81 83 restlp ⊢ ( ( 𝐾 ∈ Top ∧ ℝ ⊆ ℂ ∧ ( 𝐴 ∩ ( 𝐵 (,) +∞ ) ) ⊆ ℝ ) → ( ( limPt ‘ 𝐽 ) ‘ ( 𝐴 ∩ ( 𝐵 (,) +∞ ) ) ) = ( ( ( limPt ‘ 𝐾 ) ‘ ( 𝐴 ∩ ( 𝐵 (,) +∞ ) ) ) ∩ ℝ ) )
85 73 75 78 84 syl3anc ⊢ ( 𝜑 → ( ( limPt ‘ 𝐽 ) ‘ ( 𝐴 ∩ ( 𝐵 (,) +∞ ) ) ) = ( ( ( limPt ‘ 𝐾 ) ‘ ( 𝐴 ∩ ( 𝐵 (,) +∞ ) ) ) ∩ ℝ ) )
86 1 eqcomi ⊢ ( TopOpen ‘ ℂfld ) = 𝐾
87 86 fveq2i ⊢ ( limPt ‘ ( TopOpen ‘ ℂfld ) ) = ( limPt ‘ 𝐾 )
88 87 fveq1i ⊢ ( ( limPt ‘ ( TopOpen ‘ ℂfld ) ) ‘ ( 𝐴 ∩ ( 𝐵 (,) +∞ ) ) ) = ( ( limPt ‘ 𝐾 ) ‘ ( 𝐴 ∩ ( 𝐵 (,) +∞ ) ) )
89 88 a1i ⊢ ( 𝜑 → ( ( limPt ‘ ( TopOpen ‘ ℂfld ) ) ‘ ( 𝐴 ∩ ( 𝐵 (,) +∞ ) ) ) = ( ( limPt ‘ 𝐾 ) ‘ ( 𝐴 ∩ ( 𝐵 (,) +∞ ) ) ) )
90 71 85 89 3sstr4d ⊢ ( 𝜑 → ( ( limPt ‘ 𝐽 ) ‘ ( 𝐴 ∩ ( 𝐵 (,) +∞ ) ) ) ⊆ ( ( limPt ‘ ( TopOpen ‘ ℂfld ) ) ‘ ( 𝐴 ∩ ( 𝐵 (,) +∞ ) ) ) )
91 90 6 sseldd ⊢ ( 𝜑 → 𝐵 ∈ ( ( limPt ‘ ( TopOpen ‘ ℂfld ) ) ‘ ( 𝐴 ∩ ( 𝐵 (,) +∞ ) ) ) )
92 47 59 islpcn ⊢ ( 𝜑 → ( 𝐵 ∈ ( ( limPt ‘ ( TopOpen ‘ ℂfld ) ) ‘ ( 𝐴 ∩ ( 𝐵 (,) +∞ ) ) ) ↔ ∀ 𝑢 ∈ ℝ+ ∃ 𝑏 ∈ ( ( 𝐴 ∩ ( 𝐵 (,) +∞ ) ) ∖ { 𝐵 } ) ( abs ‘ ( 𝑏 − 𝐵 ) ) < 𝑢 ) )
93 91 92 mpbid ⊢ ( 𝜑 → ∀ 𝑢 ∈ ℝ+ ∃ 𝑏 ∈ ( ( 𝐴 ∩ ( 𝐵 (,) +∞ ) ) ∖ { 𝐵 } ) ( abs ‘ ( 𝑏 − 𝐵 ) ) < 𝑢 )
94 93 3ad2ant1 ⊢ ( ( 𝜑 ∧ 𝑧 ∈ ℝ+ ∧ 𝑣 ∈ ℝ+ ) → ∀ 𝑢 ∈ ℝ+ ∃ 𝑏 ∈ ( ( 𝐴 ∩ ( 𝐵 (,) +∞ ) ) ∖ { 𝐵 } ) ( abs ‘ ( 𝑏 − 𝐵 ) ) < 𝑢 )
95 ifcl ⊢ ( ( 𝑧 ∈ ℝ+ ∧ 𝑣 ∈ ℝ+ ) → if ( 𝑧 ≤ 𝑣 , 𝑧 , 𝑣 ) ∈ ℝ+ )
96 95 3adant1 ⊢ ( ( 𝜑 ∧ 𝑧 ∈ ℝ+ ∧ 𝑣 ∈ ℝ+ ) → if ( 𝑧 ≤ 𝑣 , 𝑧 , 𝑣 ) ∈ ℝ+ )
97 69 94 96 rspcdva ⊢ ( ( 𝜑 ∧ 𝑧 ∈ ℝ+ ∧ 𝑣 ∈ ℝ+ ) → ∃ 𝑏 ∈ ( ( 𝐴 ∩ ( 𝐵 (,) +∞ ) ) ∖ { 𝐵 } ) ( abs ‘ ( 𝑏 − 𝐵 ) ) < if ( 𝑧 ≤ 𝑣 , 𝑧 , 𝑣 ) )
98 eldifi ⊢ ( 𝑏 ∈ ( ( 𝐴 ∩ ( 𝐵 (,) +∞ ) ) ∖ { 𝐵 } ) → 𝑏 ∈ ( 𝐴 ∩ ( 𝐵 (,) +∞ ) ) )
99 77 98 sselid ⊢ ( 𝑏 ∈ ( ( 𝐴 ∩ ( 𝐵 (,) +∞ ) ) ∖ { 𝐵 } ) → 𝑏 ∈ ℝ )
100 75 sselda ⊢ ( ( 𝜑 ∧ 𝑏 ∈ ℝ ) → 𝑏 ∈ ℂ )
101 59 adantr ⊢ ( ( 𝜑 ∧ 𝑏 ∈ ℝ ) → 𝐵 ∈ ℂ )
102 100 101 subcld ⊢ ( ( 𝜑 ∧ 𝑏 ∈ ℝ ) → ( 𝑏 − 𝐵 ) ∈ ℂ )
103 102 abscld ⊢ ( ( 𝜑 ∧ 𝑏 ∈ ℝ ) → ( abs ‘ ( 𝑏 − 𝐵 ) ) ∈ ℝ )
104 103 3ad2antl1 ⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ ℝ+ ∧ 𝑣 ∈ ℝ+ ) ∧ 𝑏 ∈ ℝ ) → ( abs ‘ ( 𝑏 − 𝐵 ) ) ∈ ℝ )
105 104 adantr ⊢ ( ( ( ( 𝜑 ∧ 𝑧 ∈ ℝ+ ∧ 𝑣 ∈ ℝ+ ) ∧ 𝑏 ∈ ℝ ) ∧ ( abs ‘ ( 𝑏 − 𝐵 ) ) < if ( 𝑧 ≤ 𝑣 , 𝑧 , 𝑣 ) ) → ( abs ‘ ( 𝑏 − 𝐵 ) ) ∈ ℝ )
106 96 rpred ⊢ ( ( 𝜑 ∧ 𝑧 ∈ ℝ+ ∧ 𝑣 ∈ ℝ+ ) → if ( 𝑧 ≤ 𝑣 , 𝑧 , 𝑣 ) ∈ ℝ )
107 106 ad2antrr ⊢ ( ( ( ( 𝜑 ∧ 𝑧 ∈ ℝ+ ∧ 𝑣 ∈ ℝ+ ) ∧ 𝑏 ∈ ℝ ) ∧ ( abs ‘ ( 𝑏 − 𝐵 ) ) < if ( 𝑧 ≤ 𝑣 , 𝑧 , 𝑣 ) ) → if ( 𝑧 ≤ 𝑣 , 𝑧 , 𝑣 ) ∈ ℝ )
108 rpre ⊢ ( 𝑧 ∈ ℝ+ → 𝑧 ∈ ℝ )
109 108 3ad2ant2 ⊢ ( ( 𝜑 ∧ 𝑧 ∈ ℝ+ ∧ 𝑣 ∈ ℝ+ ) → 𝑧 ∈ ℝ )
110 109 ad2antrr ⊢ ( ( ( ( 𝜑 ∧ 𝑧 ∈ ℝ+ ∧ 𝑣 ∈ ℝ+ ) ∧ 𝑏 ∈ ℝ ) ∧ ( abs ‘ ( 𝑏 − 𝐵 ) ) < if ( 𝑧 ≤ 𝑣 , 𝑧 , 𝑣 ) ) → 𝑧 ∈ ℝ )
111 simpr ⊢ ( ( ( ( 𝜑 ∧ 𝑧 ∈ ℝ+ ∧ 𝑣 ∈ ℝ+ ) ∧ 𝑏 ∈ ℝ ) ∧ ( abs ‘ ( 𝑏 − 𝐵 ) ) < if ( 𝑧 ≤ 𝑣 , 𝑧 , 𝑣 ) ) → ( abs ‘ ( 𝑏 − 𝐵 ) ) < if ( 𝑧 ≤ 𝑣 , 𝑧 , 𝑣 ) )
112 rpre ⊢ ( 𝑣 ∈ ℝ+ → 𝑣 ∈ ℝ )
113 min1 ⊢ ( ( 𝑧 ∈ ℝ ∧ 𝑣 ∈ ℝ ) → if ( 𝑧 ≤ 𝑣 , 𝑧 , 𝑣 ) ≤ 𝑧 )
114 108 112 113 syl2an ⊢ ( ( 𝑧 ∈ ℝ+ ∧ 𝑣 ∈ ℝ+ ) → if ( 𝑧 ≤ 𝑣 , 𝑧 , 𝑣 ) ≤ 𝑧 )
115 114 3adant1 ⊢ ( ( 𝜑 ∧ 𝑧 ∈ ℝ+ ∧ 𝑣 ∈ ℝ+ ) → if ( 𝑧 ≤ 𝑣 , 𝑧 , 𝑣 ) ≤ 𝑧 )
116 115 ad2antrr ⊢ ( ( ( ( 𝜑 ∧ 𝑧 ∈ ℝ+ ∧ 𝑣 ∈ ℝ+ ) ∧ 𝑏 ∈ ℝ ) ∧ ( abs ‘ ( 𝑏 − 𝐵 ) ) < if ( 𝑧 ≤ 𝑣 , 𝑧 , 𝑣 ) ) → if ( 𝑧 ≤ 𝑣 , 𝑧 , 𝑣 ) ≤ 𝑧 )
117 105 107 110 111 116 ltletrd ⊢ ( ( ( ( 𝜑 ∧ 𝑧 ∈ ℝ+ ∧ 𝑣 ∈ ℝ+ ) ∧ 𝑏 ∈ ℝ ) ∧ ( abs ‘ ( 𝑏 − 𝐵 ) ) < if ( 𝑧 ≤ 𝑣 , 𝑧 , 𝑣 ) ) → ( abs ‘ ( 𝑏 − 𝐵 ) ) < 𝑧 )
118 112 3ad2ant3 ⊢ ( ( 𝜑 ∧ 𝑧 ∈ ℝ+ ∧ 𝑣 ∈ ℝ+ ) → 𝑣 ∈ ℝ )
119 118 ad2antrr ⊢ ( ( ( ( 𝜑 ∧ 𝑧 ∈ ℝ+ ∧ 𝑣 ∈ ℝ+ ) ∧ 𝑏 ∈ ℝ ) ∧ ( abs ‘ ( 𝑏 − 𝐵 ) ) < if ( 𝑧 ≤ 𝑣 , 𝑧 , 𝑣 ) ) → 𝑣 ∈ ℝ )
120 110 119 min2d ⊢ ( ( ( ( 𝜑 ∧ 𝑧 ∈ ℝ+ ∧ 𝑣 ∈ ℝ+ ) ∧ 𝑏 ∈ ℝ ) ∧ ( abs ‘ ( 𝑏 − 𝐵 ) ) < if ( 𝑧 ≤ 𝑣 , 𝑧 , 𝑣 ) ) → if ( 𝑧 ≤ 𝑣 , 𝑧 , 𝑣 ) ≤ 𝑣 )
121 105 107 119 111 120 ltletrd ⊢ ( ( ( ( 𝜑 ∧ 𝑧 ∈ ℝ+ ∧ 𝑣 ∈ ℝ+ ) ∧ 𝑏 ∈ ℝ ) ∧ ( abs ‘ ( 𝑏 − 𝐵 ) ) < if ( 𝑧 ≤ 𝑣 , 𝑧 , 𝑣 ) ) → ( abs ‘ ( 𝑏 − 𝐵 ) ) < 𝑣 )
122 117 121 jca ⊢ ( ( ( ( 𝜑 ∧ 𝑧 ∈ ℝ+ ∧ 𝑣 ∈ ℝ+ ) ∧ 𝑏 ∈ ℝ ) ∧ ( abs ‘ ( 𝑏 − 𝐵 ) ) < if ( 𝑧 ≤ 𝑣 , 𝑧 , 𝑣 ) ) → ( ( abs ‘ ( 𝑏 − 𝐵 ) ) < 𝑧 ∧ ( abs ‘ ( 𝑏 − 𝐵 ) ) < 𝑣 ) )
123 122 ex ⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ ℝ+ ∧ 𝑣 ∈ ℝ+ ) ∧ 𝑏 ∈ ℝ ) → ( ( abs ‘ ( 𝑏 − 𝐵 ) ) < if ( 𝑧 ≤ 𝑣 , 𝑧 , 𝑣 ) → ( ( abs ‘ ( 𝑏 − 𝐵 ) ) < 𝑧 ∧ ( abs ‘ ( 𝑏 − 𝐵 ) ) < 𝑣 ) ) )
124 99 123 sylan2 ⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ ℝ+ ∧ 𝑣 ∈ ℝ+ ) ∧ 𝑏 ∈ ( ( 𝐴 ∩ ( 𝐵 (,) +∞ ) ) ∖ { 𝐵 } ) ) → ( ( abs ‘ ( 𝑏 − 𝐵 ) ) < if ( 𝑧 ≤ 𝑣 , 𝑧 , 𝑣 ) → ( ( abs ‘ ( 𝑏 − 𝐵 ) ) < 𝑧 ∧ ( abs ‘ ( 𝑏 − 𝐵 ) ) < 𝑣 ) ) )
125 124 reximdva ⊢ ( ( 𝜑 ∧ 𝑧 ∈ ℝ+ ∧ 𝑣 ∈ ℝ+ ) → ( ∃ 𝑏 ∈ ( ( 𝐴 ∩ ( 𝐵 (,) +∞ ) ) ∖ { 𝐵 } ) ( abs ‘ ( 𝑏 − 𝐵 ) ) < if ( 𝑧 ≤ 𝑣 , 𝑧 , 𝑣 ) → ∃ 𝑏 ∈ ( ( 𝐴 ∩ ( 𝐵 (,) +∞ ) ) ∖ { 𝐵 } ) ( ( abs ‘ ( 𝑏 − 𝐵 ) ) < 𝑧 ∧ ( abs ‘ ( 𝑏 − 𝐵 ) ) < 𝑣 ) ) )
126 97 125 mpd ⊢ ( ( 𝜑 ∧ 𝑧 ∈ ℝ+ ∧ 𝑣 ∈ ℝ+ ) → ∃ 𝑏 ∈ ( ( 𝐴 ∩ ( 𝐵 (,) +∞ ) ) ∖ { 𝐵 } ) ( ( abs ‘ ( 𝑏 − 𝐵 ) ) < 𝑧 ∧ ( abs ‘ ( 𝑏 − 𝐵 ) ) < 𝑣 ) )
127 65 66 67 126 syl3anc ⊢ ( ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ+ ) ∧ 𝑧 ∈ ℝ+ ∧ ∀ 𝑤 ∈ 𝐴 ( ( 𝑤 ≠ 𝐵 ∧ ( abs ‘ ( 𝑤 − 𝐵 ) ) < 𝑧 ) → ( abs ‘ ( ( 𝐹 ‘ 𝑤 ) − 𝑥 ) ) < 𝑦 ) ) ∧ 𝑣 ∈ ℝ+ ∧ ∀ 𝑤 ∈ ( 𝐴 ∩ ( 𝐵 (,) +∞ ) ) ( ( 𝑤 ≠ 𝐵 ∧ ( abs ‘ ( 𝑤 − 𝐵 ) ) < 𝑣 ) → ( abs ‘ ( ( ( 𝐹 ↾ ( 𝐵 (,) +∞ ) ) ‘ 𝑤 ) − 𝑅 ) ) < 𝑦 ) ) → ∃ 𝑏 ∈ ( ( 𝐴 ∩ ( 𝐵 (,) +∞ ) ) ∖ { 𝐵 } ) ( ( abs ‘ ( 𝑏 − 𝐵 ) ) < 𝑧 ∧ ( abs ‘ ( 𝑏 − 𝐵 ) ) < 𝑣 ) )
128 nfv ⊢ Ⅎ 𝑏 ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ+ ) ∧ 𝑧 ∈ ℝ+ ∧ ∀ 𝑤 ∈ 𝐴 ( ( 𝑤 ≠ 𝐵 ∧ ( abs ‘ ( 𝑤 − 𝐵 ) ) < 𝑧 ) → ( abs ‘ ( ( 𝐹 ‘ 𝑤 ) − 𝑥 ) ) < 𝑦 ) ) ∧ 𝑣 ∈ ℝ+ ∧ ∀ 𝑤 ∈ ( 𝐴 ∩ ( 𝐵 (,) +∞ ) ) ( ( 𝑤 ≠ 𝐵 ∧ ( abs ‘ ( 𝑤 − 𝐵 ) ) < 𝑣 ) → ( abs ‘ ( ( ( 𝐹 ↾ ( 𝐵 (,) +∞ ) ) ‘ 𝑤 ) − 𝑅 ) ) < 𝑦 ) )
129 nfre1 ⊢ Ⅎ 𝑏 ∃ 𝑏 ∈ 𝐴 ( ( abs ‘ ( ( 𝐹 ‘ 𝑏 ) − 𝑥 ) ) < 𝑦 ∧ ( abs ‘ ( ( 𝐹 ‘ 𝑏 ) − 𝑅 ) ) < 𝑦 )
130 98 elin1d ⊢ ( 𝑏 ∈ ( ( 𝐴 ∩ ( 𝐵 (,) +∞ ) ) ∖ { 𝐵 } ) → 𝑏 ∈ 𝐴 )
131 130 3ad2ant2 ⊢ ( ( ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ+ ) ∧ 𝑧 ∈ ℝ+ ∧ ∀ 𝑤 ∈ 𝐴 ( ( 𝑤 ≠ 𝐵 ∧ ( abs ‘ ( 𝑤 − 𝐵 ) ) < 𝑧 ) → ( abs ‘ ( ( 𝐹 ‘ 𝑤 ) − 𝑥 ) ) < 𝑦 ) ) ∧ 𝑣 ∈ ℝ+ ∧ ∀ 𝑤 ∈ ( 𝐴 ∩ ( 𝐵 (,) +∞ ) ) ( ( 𝑤 ≠ 𝐵 ∧ ( abs ‘ ( 𝑤 − 𝐵 ) ) < 𝑣 ) → ( abs ‘ ( ( ( 𝐹 ↾ ( 𝐵 (,) +∞ ) ) ‘ 𝑤 ) − 𝑅 ) ) < 𝑦 ) ) ∧ 𝑏 ∈ ( ( 𝐴 ∩ ( 𝐵 (,) +∞ ) ) ∖ { 𝐵 } ) ∧ ( ( abs ‘ ( 𝑏 − 𝐵 ) ) < 𝑧 ∧ ( abs ‘ ( 𝑏 − 𝐵 ) ) < 𝑣 ) ) → 𝑏 ∈ 𝐴 )
132 simp113 ⊢ ( ( ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ+ ) ∧ 𝑧 ∈ ℝ+ ∧ ∀ 𝑤 ∈ 𝐴 ( ( 𝑤 ≠ 𝐵 ∧ ( abs ‘ ( 𝑤 − 𝐵 ) ) < 𝑧 ) → ( abs ‘ ( ( 𝐹 ‘ 𝑤 ) − 𝑥 ) ) < 𝑦 ) ) ∧ 𝑣 ∈ ℝ+ ∧ ∀ 𝑤 ∈ ( 𝐴 ∩ ( 𝐵 (,) +∞ ) ) ( ( 𝑤 ≠ 𝐵 ∧ ( abs ‘ ( 𝑤 − 𝐵 ) ) < 𝑣 ) → ( abs ‘ ( ( ( 𝐹 ↾ ( 𝐵 (,) +∞ ) ) ‘ 𝑤 ) − 𝑅 ) ) < 𝑦 ) ) ∧ 𝑏 ∈ ( ( 𝐴 ∩ ( 𝐵 (,) +∞ ) ) ∖ { 𝐵 } ) ∧ ( ( abs ‘ ( 𝑏 − 𝐵 ) ) < 𝑧 ∧ ( abs ‘ ( 𝑏 − 𝐵 ) ) < 𝑣 ) ) → ∀ 𝑤 ∈ 𝐴 ( ( 𝑤 ≠ 𝐵 ∧ ( abs ‘ ( 𝑤 − 𝐵 ) ) < 𝑧 ) → ( abs ‘ ( ( 𝐹 ‘ 𝑤 ) − 𝑥 ) ) < 𝑦 ) )
133 eldifsni ⊢ ( 𝑏 ∈ ( ( 𝐴 ∩ ( 𝐵 (,) +∞ ) ) ∖ { 𝐵 } ) → 𝑏 ≠ 𝐵 )
134 133 adantr ⊢ ( ( 𝑏 ∈ ( ( 𝐴 ∩ ( 𝐵 (,) +∞ ) ) ∖ { 𝐵 } ) ∧ ( ( abs ‘ ( 𝑏 − 𝐵 ) ) < 𝑧 ∧ ( abs ‘ ( 𝑏 − 𝐵 ) ) < 𝑣 ) ) → 𝑏 ≠ 𝐵 )
135 simprl ⊢ ( ( 𝑏 ∈ ( ( 𝐴 ∩ ( 𝐵 (,) +∞ ) ) ∖ { 𝐵 } ) ∧ ( ( abs ‘ ( 𝑏 − 𝐵 ) ) < 𝑧 ∧ ( abs ‘ ( 𝑏 − 𝐵 ) ) < 𝑣 ) ) → ( abs ‘ ( 𝑏 − 𝐵 ) ) < 𝑧 )
136 134 135 jca ⊢ ( ( 𝑏 ∈ ( ( 𝐴 ∩ ( 𝐵 (,) +∞ ) ) ∖ { 𝐵 } ) ∧ ( ( abs ‘ ( 𝑏 − 𝐵 ) ) < 𝑧 ∧ ( abs ‘ ( 𝑏 − 𝐵 ) ) < 𝑣 ) ) → ( 𝑏 ≠ 𝐵 ∧ ( abs ‘ ( 𝑏 − 𝐵 ) ) < 𝑧 ) )
137 136 3adant1 ⊢ ( ( ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ+ ) ∧ 𝑧 ∈ ℝ+ ∧ ∀ 𝑤 ∈ 𝐴 ( ( 𝑤 ≠ 𝐵 ∧ ( abs ‘ ( 𝑤 − 𝐵 ) ) < 𝑧 ) → ( abs ‘ ( ( 𝐹 ‘ 𝑤 ) − 𝑥 ) ) < 𝑦 ) ) ∧ 𝑣 ∈ ℝ+ ∧ ∀ 𝑤 ∈ ( 𝐴 ∩ ( 𝐵 (,) +∞ ) ) ( ( 𝑤 ≠ 𝐵 ∧ ( abs ‘ ( 𝑤 − 𝐵 ) ) < 𝑣 ) → ( abs ‘ ( ( ( 𝐹 ↾ ( 𝐵 (,) +∞ ) ) ‘ 𝑤 ) − 𝑅 ) ) < 𝑦 ) ) ∧ 𝑏 ∈ ( ( 𝐴 ∩ ( 𝐵 (,) +∞ ) ) ∖ { 𝐵 } ) ∧ ( ( abs ‘ ( 𝑏 − 𝐵 ) ) < 𝑧 ∧ ( abs ‘ ( 𝑏 − 𝐵 ) ) < 𝑣 ) ) → ( 𝑏 ≠ 𝐵 ∧ ( abs ‘ ( 𝑏 − 𝐵 ) ) < 𝑧 ) )
138 neeq1 ⊢ ( 𝑤 = 𝑏 → ( 𝑤 ≠ 𝐵 ↔ 𝑏 ≠ 𝐵 ) )
139 fvoveq1 ⊢ ( 𝑤 = 𝑏 → ( abs ‘ ( 𝑤 − 𝐵 ) ) = ( abs ‘ ( 𝑏 − 𝐵 ) ) )
140 139 breq1d ⊢ ( 𝑤 = 𝑏 → ( ( abs ‘ ( 𝑤 − 𝐵 ) ) < 𝑧 ↔ ( abs ‘ ( 𝑏 − 𝐵 ) ) < 𝑧 ) )
141 138 140 anbi12d ⊢ ( 𝑤 = 𝑏 → ( ( 𝑤 ≠ 𝐵 ∧ ( abs ‘ ( 𝑤 − 𝐵 ) ) < 𝑧 ) ↔ ( 𝑏 ≠ 𝐵 ∧ ( abs ‘ ( 𝑏 − 𝐵 ) ) < 𝑧 ) ) )
142 141 imbrov2fvoveq ⊢ ( 𝑤 = 𝑏 → ( ( ( 𝑤 ≠ 𝐵 ∧ ( abs ‘ ( 𝑤 − 𝐵 ) ) < 𝑧 ) → ( abs ‘ ( ( 𝐹 ‘ 𝑤 ) − 𝑥 ) ) < 𝑦 ) ↔ ( ( 𝑏 ≠ 𝐵 ∧ ( abs ‘ ( 𝑏 − 𝐵 ) ) < 𝑧 ) → ( abs ‘ ( ( 𝐹 ‘ 𝑏 ) − 𝑥 ) ) < 𝑦 ) ) )
143 142 rspcva ⊢ ( ( 𝑏 ∈ 𝐴 ∧ ∀ 𝑤 ∈ 𝐴 ( ( 𝑤 ≠ 𝐵 ∧ ( abs ‘ ( 𝑤 − 𝐵 ) ) < 𝑧 ) → ( abs ‘ ( ( 𝐹 ‘ 𝑤 ) − 𝑥 ) ) < 𝑦 ) ) → ( ( 𝑏 ≠ 𝐵 ∧ ( abs ‘ ( 𝑏 − 𝐵 ) ) < 𝑧 ) → ( abs ‘ ( ( 𝐹 ‘ 𝑏 ) − 𝑥 ) ) < 𝑦 ) )
144 143 imp ⊢ ( ( ( 𝑏 ∈ 𝐴 ∧ ∀ 𝑤 ∈ 𝐴 ( ( 𝑤 ≠ 𝐵 ∧ ( abs ‘ ( 𝑤 − 𝐵 ) ) < 𝑧 ) → ( abs ‘ ( ( 𝐹 ‘ 𝑤 ) − 𝑥 ) ) < 𝑦 ) ) ∧ ( 𝑏 ≠ 𝐵 ∧ ( abs ‘ ( 𝑏 − 𝐵 ) ) < 𝑧 ) ) → ( abs ‘ ( ( 𝐹 ‘ 𝑏 ) − 𝑥 ) ) < 𝑦 )
145 131 132 137 144 syl21anc ⊢ ( ( ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ+ ) ∧ 𝑧 ∈ ℝ+ ∧ ∀ 𝑤 ∈ 𝐴 ( ( 𝑤 ≠ 𝐵 ∧ ( abs ‘ ( 𝑤 − 𝐵 ) ) < 𝑧 ) → ( abs ‘ ( ( 𝐹 ‘ 𝑤 ) − 𝑥 ) ) < 𝑦 ) ) ∧ 𝑣 ∈ ℝ+ ∧ ∀ 𝑤 ∈ ( 𝐴 ∩ ( 𝐵 (,) +∞ ) ) ( ( 𝑤 ≠ 𝐵 ∧ ( abs ‘ ( 𝑤 − 𝐵 ) ) < 𝑣 ) → ( abs ‘ ( ( ( 𝐹 ↾ ( 𝐵 (,) +∞ ) ) ‘ 𝑤 ) − 𝑅 ) ) < 𝑦 ) ) ∧ 𝑏 ∈ ( ( 𝐴 ∩ ( 𝐵 (,) +∞ ) ) ∖ { 𝐵 } ) ∧ ( ( abs ‘ ( 𝑏 − 𝐵 ) ) < 𝑧 ∧ ( abs ‘ ( 𝑏 − 𝐵 ) ) < 𝑣 ) ) → ( abs ‘ ( ( 𝐹 ‘ 𝑏 ) − 𝑥 ) ) < 𝑦 )
146 98 3ad2ant2 ⊢ ( ( ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ+ ) ∧ 𝑧 ∈ ℝ+ ∧ ∀ 𝑤 ∈ 𝐴 ( ( 𝑤 ≠ 𝐵 ∧ ( abs ‘ ( 𝑤 − 𝐵 ) ) < 𝑧 ) → ( abs ‘ ( ( 𝐹 ‘ 𝑤 ) − 𝑥 ) ) < 𝑦 ) ) ∧ 𝑣 ∈ ℝ+ ∧ ∀ 𝑤 ∈ ( 𝐴 ∩ ( 𝐵 (,) +∞ ) ) ( ( 𝑤 ≠ 𝐵 ∧ ( abs ‘ ( 𝑤 − 𝐵 ) ) < 𝑣 ) → ( abs ‘ ( ( ( 𝐹 ↾ ( 𝐵 (,) +∞ ) ) ‘ 𝑤 ) − 𝑅 ) ) < 𝑦 ) ) ∧ 𝑏 ∈ ( ( 𝐴 ∩ ( 𝐵 (,) +∞ ) ) ∖ { 𝐵 } ) ∧ ( ( abs ‘ ( 𝑏 − 𝐵 ) ) < 𝑧 ∧ ( abs ‘ ( 𝑏 − 𝐵 ) ) < 𝑣 ) ) → 𝑏 ∈ ( 𝐴 ∩ ( 𝐵 (,) +∞ ) ) )
147 65 3ad2ant1 ⊢ ( ( ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ+ ) ∧ 𝑧 ∈ ℝ+ ∧ ∀ 𝑤 ∈ 𝐴 ( ( 𝑤 ≠ 𝐵 ∧ ( abs ‘ ( 𝑤 − 𝐵 ) ) < 𝑧 ) → ( abs ‘ ( ( 𝐹 ‘ 𝑤 ) − 𝑥 ) ) < 𝑦 ) ) ∧ 𝑣 ∈ ℝ+ ∧ ∀ 𝑤 ∈ ( 𝐴 ∩ ( 𝐵 (,) +∞ ) ) ( ( 𝑤 ≠ 𝐵 ∧ ( abs ‘ ( 𝑤 − 𝐵 ) ) < 𝑣 ) → ( abs ‘ ( ( ( 𝐹 ↾ ( 𝐵 (,) +∞ ) ) ‘ 𝑤 ) − 𝑅 ) ) < 𝑦 ) ) ∧ 𝑏 ∈ ( ( 𝐴 ∩ ( 𝐵 (,) +∞ ) ) ∖ { 𝐵 } ) ∧ ( ( abs ‘ ( 𝑏 − 𝐵 ) ) < 𝑧 ∧ ( abs ‘ ( 𝑏 − 𝐵 ) ) < 𝑣 ) ) → 𝜑 )
148 simp13 ⊢ ( ( ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ+ ) ∧ 𝑧 ∈ ℝ+ ∧ ∀ 𝑤 ∈ 𝐴 ( ( 𝑤 ≠ 𝐵 ∧ ( abs ‘ ( 𝑤 − 𝐵 ) ) < 𝑧 ) → ( abs ‘ ( ( 𝐹 ‘ 𝑤 ) − 𝑥 ) ) < 𝑦 ) ) ∧ 𝑣 ∈ ℝ+ ∧ ∀ 𝑤 ∈ ( 𝐴 ∩ ( 𝐵 (,) +∞ ) ) ( ( 𝑤 ≠ 𝐵 ∧ ( abs ‘ ( 𝑤 − 𝐵 ) ) < 𝑣 ) → ( abs ‘ ( ( ( 𝐹 ↾ ( 𝐵 (,) +∞ ) ) ‘ 𝑤 ) − 𝑅 ) ) < 𝑦 ) ) ∧ 𝑏 ∈ ( ( 𝐴 ∩ ( 𝐵 (,) +∞ ) ) ∖ { 𝐵 } ) ∧ ( ( abs ‘ ( 𝑏 − 𝐵 ) ) < 𝑧 ∧ ( abs ‘ ( 𝑏 − 𝐵 ) ) < 𝑣 ) ) → ∀ 𝑤 ∈ ( 𝐴 ∩ ( 𝐵 (,) +∞ ) ) ( ( 𝑤 ≠ 𝐵 ∧ ( abs ‘ ( 𝑤 − 𝐵 ) ) < 𝑣 ) → ( abs ‘ ( ( ( 𝐹 ↾ ( 𝐵 (,) +∞ ) ) ‘ 𝑤 ) − 𝑅 ) ) < 𝑦 ) )
149 nfv ⊢ Ⅎ 𝑤 𝜑
150 nfra1 ⊢ Ⅎ 𝑤 ∀ 𝑤 ∈ ( 𝐴 ∩ ( 𝐵 (,) +∞ ) ) ( ( 𝑤 ≠ 𝐵 ∧ ( abs ‘ ( 𝑤 − 𝐵 ) ) < 𝑣 ) → ( abs ‘ ( ( ( 𝐹 ↾ ( 𝐵 (,) +∞ ) ) ‘ 𝑤 ) − 𝑅 ) ) < 𝑦 )
151 149 150 nfan ⊢ Ⅎ 𝑤 ( 𝜑 ∧ ∀ 𝑤 ∈ ( 𝐴 ∩ ( 𝐵 (,) +∞ ) ) ( ( 𝑤 ≠ 𝐵 ∧ ( abs ‘ ( 𝑤 − 𝐵 ) ) < 𝑣 ) → ( abs ‘ ( ( ( 𝐹 ↾ ( 𝐵 (,) +∞ ) ) ‘ 𝑤 ) − 𝑅 ) ) < 𝑦 ) )
152 elinel2 ⊢ ( 𝑤 ∈ ( 𝐴 ∩ ( 𝐵 (,) +∞ ) ) → 𝑤 ∈ ( 𝐵 (,) +∞ ) )
153 152 fvresd ⊢ ( 𝑤 ∈ ( 𝐴 ∩ ( 𝐵 (,) +∞ ) ) → ( ( 𝐹 ↾ ( 𝐵 (,) +∞ ) ) ‘ 𝑤 ) = ( 𝐹 ‘ 𝑤 ) )
154 153 eqcomd ⊢ ( 𝑤 ∈ ( 𝐴 ∩ ( 𝐵 (,) +∞ ) ) → ( 𝐹 ‘ 𝑤 ) = ( ( 𝐹 ↾ ( 𝐵 (,) +∞ ) ) ‘ 𝑤 ) )
155 154 fvoveq1d ⊢ ( 𝑤 ∈ ( 𝐴 ∩ ( 𝐵 (,) +∞ ) ) → ( abs ‘ ( ( 𝐹 ‘ 𝑤 ) − 𝑅 ) ) = ( abs ‘ ( ( ( 𝐹 ↾ ( 𝐵 (,) +∞ ) ) ‘ 𝑤 ) − 𝑅 ) ) )
156 155 3ad2ant2 ⊢ ( ( ( 𝜑 ∧ ∀ 𝑤 ∈ ( 𝐴 ∩ ( 𝐵 (,) +∞ ) ) ( ( 𝑤 ≠ 𝐵 ∧ ( abs ‘ ( 𝑤 − 𝐵 ) ) < 𝑣 ) → ( abs ‘ ( ( ( 𝐹 ↾ ( 𝐵 (,) +∞ ) ) ‘ 𝑤 ) − 𝑅 ) ) < 𝑦 ) ) ∧ 𝑤 ∈ ( 𝐴 ∩ ( 𝐵 (,) +∞ ) ) ∧ ( 𝑤 ≠ 𝐵 ∧ ( abs ‘ ( 𝑤 − 𝐵 ) ) < 𝑣 ) ) → ( abs ‘ ( ( 𝐹 ‘ 𝑤 ) − 𝑅 ) ) = ( abs ‘ ( ( ( 𝐹 ↾ ( 𝐵 (,) +∞ ) ) ‘ 𝑤 ) − 𝑅 ) ) )
157 rspa ⊢ ( ( ∀ 𝑤 ∈ ( 𝐴 ∩ ( 𝐵 (,) +∞ ) ) ( ( 𝑤 ≠ 𝐵 ∧ ( abs ‘ ( 𝑤 − 𝐵 ) ) < 𝑣 ) → ( abs ‘ ( ( ( 𝐹 ↾ ( 𝐵 (,) +∞ ) ) ‘ 𝑤 ) − 𝑅 ) ) < 𝑦 ) ∧ 𝑤 ∈ ( 𝐴 ∩ ( 𝐵 (,) +∞ ) ) ) → ( ( 𝑤 ≠ 𝐵 ∧ ( abs ‘ ( 𝑤 − 𝐵 ) ) < 𝑣 ) → ( abs ‘ ( ( ( 𝐹 ↾ ( 𝐵 (,) +∞ ) ) ‘ 𝑤 ) − 𝑅 ) ) < 𝑦 ) )
158 157 3impia ⊢ ( ( ∀ 𝑤 ∈ ( 𝐴 ∩ ( 𝐵 (,) +∞ ) ) ( ( 𝑤 ≠ 𝐵 ∧ ( abs ‘ ( 𝑤 − 𝐵 ) ) < 𝑣 ) → ( abs ‘ ( ( ( 𝐹 ↾ ( 𝐵 (,) +∞ ) ) ‘ 𝑤 ) − 𝑅 ) ) < 𝑦 ) ∧ 𝑤 ∈ ( 𝐴 ∩ ( 𝐵 (,) +∞ ) ) ∧ ( 𝑤 ≠ 𝐵 ∧ ( abs ‘ ( 𝑤 − 𝐵 ) ) < 𝑣 ) ) → ( abs ‘ ( ( ( 𝐹 ↾ ( 𝐵 (,) +∞ ) ) ‘ 𝑤 ) − 𝑅 ) ) < 𝑦 )
159 158 3adant1l ⊢ ( ( ( 𝜑 ∧ ∀ 𝑤 ∈ ( 𝐴 ∩ ( 𝐵 (,) +∞ ) ) ( ( 𝑤 ≠ 𝐵 ∧ ( abs ‘ ( 𝑤 − 𝐵 ) ) < 𝑣 ) → ( abs ‘ ( ( ( 𝐹 ↾ ( 𝐵 (,) +∞ ) ) ‘ 𝑤 ) − 𝑅 ) ) < 𝑦 ) ) ∧ 𝑤 ∈ ( 𝐴 ∩ ( 𝐵 (,) +∞ ) ) ∧ ( 𝑤 ≠ 𝐵 ∧ ( abs ‘ ( 𝑤 − 𝐵 ) ) < 𝑣 ) ) → ( abs ‘ ( ( ( 𝐹 ↾ ( 𝐵 (,) +∞ ) ) ‘ 𝑤 ) − 𝑅 ) ) < 𝑦 )
160 156 159 eqbrtrd ⊢ ( ( ( 𝜑 ∧ ∀ 𝑤 ∈ ( 𝐴 ∩ ( 𝐵 (,) +∞ ) ) ( ( 𝑤 ≠ 𝐵 ∧ ( abs ‘ ( 𝑤 − 𝐵 ) ) < 𝑣 ) → ( abs ‘ ( ( ( 𝐹 ↾ ( 𝐵 (,) +∞ ) ) ‘ 𝑤 ) − 𝑅 ) ) < 𝑦 ) ) ∧ 𝑤 ∈ ( 𝐴 ∩ ( 𝐵 (,) +∞ ) ) ∧ ( 𝑤 ≠ 𝐵 ∧ ( abs ‘ ( 𝑤 − 𝐵 ) ) < 𝑣 ) ) → ( abs ‘ ( ( 𝐹 ‘ 𝑤 ) − 𝑅 ) ) < 𝑦 )
161 160 3exp ⊢ ( ( 𝜑 ∧ ∀ 𝑤 ∈ ( 𝐴 ∩ ( 𝐵 (,) +∞ ) ) ( ( 𝑤 ≠ 𝐵 ∧ ( abs ‘ ( 𝑤 − 𝐵 ) ) < 𝑣 ) → ( abs ‘ ( ( ( 𝐹 ↾ ( 𝐵 (,) +∞ ) ) ‘ 𝑤 ) − 𝑅 ) ) < 𝑦 ) ) → ( 𝑤 ∈ ( 𝐴 ∩ ( 𝐵 (,) +∞ ) ) → ( ( 𝑤 ≠ 𝐵 ∧ ( abs ‘ ( 𝑤 − 𝐵 ) ) < 𝑣 ) → ( abs ‘ ( ( 𝐹 ‘ 𝑤 ) − 𝑅 ) ) < 𝑦 ) ) )
162 151 161 ralrimi ⊢ ( ( 𝜑 ∧ ∀ 𝑤 ∈ ( 𝐴 ∩ ( 𝐵 (,) +∞ ) ) ( ( 𝑤 ≠ 𝐵 ∧ ( abs ‘ ( 𝑤 − 𝐵 ) ) < 𝑣 ) → ( abs ‘ ( ( ( 𝐹 ↾ ( 𝐵 (,) +∞ ) ) ‘ 𝑤 ) − 𝑅 ) ) < 𝑦 ) ) → ∀ 𝑤 ∈ ( 𝐴 ∩ ( 𝐵 (,) +∞ ) ) ( ( 𝑤 ≠ 𝐵 ∧ ( abs ‘ ( 𝑤 − 𝐵 ) ) < 𝑣 ) → ( abs ‘ ( ( 𝐹 ‘ 𝑤 ) − 𝑅 ) ) < 𝑦 ) )
163 147 148 162 syl2anc ⊢ ( ( ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ+ ) ∧ 𝑧 ∈ ℝ+ ∧ ∀ 𝑤 ∈ 𝐴 ( ( 𝑤 ≠ 𝐵 ∧ ( abs ‘ ( 𝑤 − 𝐵 ) ) < 𝑧 ) → ( abs ‘ ( ( 𝐹 ‘ 𝑤 ) − 𝑥 ) ) < 𝑦 ) ) ∧ 𝑣 ∈ ℝ+ ∧ ∀ 𝑤 ∈ ( 𝐴 ∩ ( 𝐵 (,) +∞ ) ) ( ( 𝑤 ≠ 𝐵 ∧ ( abs ‘ ( 𝑤 − 𝐵 ) ) < 𝑣 ) → ( abs ‘ ( ( ( 𝐹 ↾ ( 𝐵 (,) +∞ ) ) ‘ 𝑤 ) − 𝑅 ) ) < 𝑦 ) ) ∧ 𝑏 ∈ ( ( 𝐴 ∩ ( 𝐵 (,) +∞ ) ) ∖ { 𝐵 } ) ∧ ( ( abs ‘ ( 𝑏 − 𝐵 ) ) < 𝑧 ∧ ( abs ‘ ( 𝑏 − 𝐵 ) ) < 𝑣 ) ) → ∀ 𝑤 ∈ ( 𝐴 ∩ ( 𝐵 (,) +∞ ) ) ( ( 𝑤 ≠ 𝐵 ∧ ( abs ‘ ( 𝑤 − 𝐵 ) ) < 𝑣 ) → ( abs ‘ ( ( 𝐹 ‘ 𝑤 ) − 𝑅 ) ) < 𝑦 ) )
164 133 anim1i ⊢ ( ( 𝑏 ∈ ( ( 𝐴 ∩ ( 𝐵 (,) +∞ ) ) ∖ { 𝐵 } ) ∧ ( abs ‘ ( 𝑏 − 𝐵 ) ) < 𝑣 ) → ( 𝑏 ≠ 𝐵 ∧ ( abs ‘ ( 𝑏 − 𝐵 ) ) < 𝑣 ) )
165 164 adantrl ⊢ ( ( 𝑏 ∈ ( ( 𝐴 ∩ ( 𝐵 (,) +∞ ) ) ∖ { 𝐵 } ) ∧ ( ( abs ‘ ( 𝑏 − 𝐵 ) ) < 𝑧 ∧ ( abs ‘ ( 𝑏 − 𝐵 ) ) < 𝑣 ) ) → ( 𝑏 ≠ 𝐵 ∧ ( abs ‘ ( 𝑏 − 𝐵 ) ) < 𝑣 ) )
166 165 3adant1 ⊢ ( ( ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ+ ) ∧ 𝑧 ∈ ℝ+ ∧ ∀ 𝑤 ∈ 𝐴 ( ( 𝑤 ≠ 𝐵 ∧ ( abs ‘ ( 𝑤 − 𝐵 ) ) < 𝑧 ) → ( abs ‘ ( ( 𝐹 ‘ 𝑤 ) − 𝑥 ) ) < 𝑦 ) ) ∧ 𝑣 ∈ ℝ+ ∧ ∀ 𝑤 ∈ ( 𝐴 ∩ ( 𝐵 (,) +∞ ) ) ( ( 𝑤 ≠ 𝐵 ∧ ( abs ‘ ( 𝑤 − 𝐵 ) ) < 𝑣 ) → ( abs ‘ ( ( ( 𝐹 ↾ ( 𝐵 (,) +∞ ) ) ‘ 𝑤 ) − 𝑅 ) ) < 𝑦 ) ) ∧ 𝑏 ∈ ( ( 𝐴 ∩ ( 𝐵 (,) +∞ ) ) ∖ { 𝐵 } ) ∧ ( ( abs ‘ ( 𝑏 − 𝐵 ) ) < 𝑧 ∧ ( abs ‘ ( 𝑏 − 𝐵 ) ) < 𝑣 ) ) → ( 𝑏 ≠ 𝐵 ∧ ( abs ‘ ( 𝑏 − 𝐵 ) ) < 𝑣 ) )
167 139 breq1d ⊢ ( 𝑤 = 𝑏 → ( ( abs ‘ ( 𝑤 − 𝐵 ) ) < 𝑣 ↔ ( abs ‘ ( 𝑏 − 𝐵 ) ) < 𝑣 ) )
168 138 167 anbi12d ⊢ ( 𝑤 = 𝑏 → ( ( 𝑤 ≠ 𝐵 ∧ ( abs ‘ ( 𝑤 − 𝐵 ) ) < 𝑣 ) ↔ ( 𝑏 ≠ 𝐵 ∧ ( abs ‘ ( 𝑏 − 𝐵 ) ) < 𝑣 ) ) )
169 168 imbrov2fvoveq ⊢ ( 𝑤 = 𝑏 → ( ( ( 𝑤 ≠ 𝐵 ∧ ( abs ‘ ( 𝑤 − 𝐵 ) ) < 𝑣 ) → ( abs ‘ ( ( 𝐹 ‘ 𝑤 ) − 𝑅 ) ) < 𝑦 ) ↔ ( ( 𝑏 ≠ 𝐵 ∧ ( abs ‘ ( 𝑏 − 𝐵 ) ) < 𝑣 ) → ( abs ‘ ( ( 𝐹 ‘ 𝑏 ) − 𝑅 ) ) < 𝑦 ) ) )
170 169 rspcva ⊢ ( ( 𝑏 ∈ ( 𝐴 ∩ ( 𝐵 (,) +∞ ) ) ∧ ∀ 𝑤 ∈ ( 𝐴 ∩ ( 𝐵 (,) +∞ ) ) ( ( 𝑤 ≠ 𝐵 ∧ ( abs ‘ ( 𝑤 − 𝐵 ) ) < 𝑣 ) → ( abs ‘ ( ( 𝐹 ‘ 𝑤 ) − 𝑅 ) ) < 𝑦 ) ) → ( ( 𝑏 ≠ 𝐵 ∧ ( abs ‘ ( 𝑏 − 𝐵 ) ) < 𝑣 ) → ( abs ‘ ( ( 𝐹 ‘ 𝑏 ) − 𝑅 ) ) < 𝑦 ) )
171 170 imp ⊢ ( ( ( 𝑏 ∈ ( 𝐴 ∩ ( 𝐵 (,) +∞ ) ) ∧ ∀ 𝑤 ∈ ( 𝐴 ∩ ( 𝐵 (,) +∞ ) ) ( ( 𝑤 ≠ 𝐵 ∧ ( abs ‘ ( 𝑤 − 𝐵 ) ) < 𝑣 ) → ( abs ‘ ( ( 𝐹 ‘ 𝑤 ) − 𝑅 ) ) < 𝑦 ) ) ∧ ( 𝑏 ≠ 𝐵 ∧ ( abs ‘ ( 𝑏 − 𝐵 ) ) < 𝑣 ) ) → ( abs ‘ ( ( 𝐹 ‘ 𝑏 ) − 𝑅 ) ) < 𝑦 )
172 146 163 166 171 syl21anc ⊢ ( ( ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ+ ) ∧ 𝑧 ∈ ℝ+ ∧ ∀ 𝑤 ∈ 𝐴 ( ( 𝑤 ≠ 𝐵 ∧ ( abs ‘ ( 𝑤 − 𝐵 ) ) < 𝑧 ) → ( abs ‘ ( ( 𝐹 ‘ 𝑤 ) − 𝑥 ) ) < 𝑦 ) ) ∧ 𝑣 ∈ ℝ+ ∧ ∀ 𝑤 ∈ ( 𝐴 ∩ ( 𝐵 (,) +∞ ) ) ( ( 𝑤 ≠ 𝐵 ∧ ( abs ‘ ( 𝑤 − 𝐵 ) ) < 𝑣 ) → ( abs ‘ ( ( ( 𝐹 ↾ ( 𝐵 (,) +∞ ) ) ‘ 𝑤 ) − 𝑅 ) ) < 𝑦 ) ) ∧ 𝑏 ∈ ( ( 𝐴 ∩ ( 𝐵 (,) +∞ ) ) ∖ { 𝐵 } ) ∧ ( ( abs ‘ ( 𝑏 − 𝐵 ) ) < 𝑧 ∧ ( abs ‘ ( 𝑏 − 𝐵 ) ) < 𝑣 ) ) → ( abs ‘ ( ( 𝐹 ‘ 𝑏 ) − 𝑅 ) ) < 𝑦 )
173 rspe ⊢ ( ( 𝑏 ∈ 𝐴 ∧ ( ( abs ‘ ( ( 𝐹 ‘ 𝑏 ) − 𝑥 ) ) < 𝑦 ∧ ( abs ‘ ( ( 𝐹 ‘ 𝑏 ) − 𝑅 ) ) < 𝑦 ) ) → ∃ 𝑏 ∈ 𝐴 ( ( abs ‘ ( ( 𝐹 ‘ 𝑏 ) − 𝑥 ) ) < 𝑦 ∧ ( abs ‘ ( ( 𝐹 ‘ 𝑏 ) − 𝑅 ) ) < 𝑦 ) )
174 131 145 172 173 syl12anc ⊢ ( ( ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ+ ) ∧ 𝑧 ∈ ℝ+ ∧ ∀ 𝑤 ∈ 𝐴 ( ( 𝑤 ≠ 𝐵 ∧ ( abs ‘ ( 𝑤 − 𝐵 ) ) < 𝑧 ) → ( abs ‘ ( ( 𝐹 ‘ 𝑤 ) − 𝑥 ) ) < 𝑦 ) ) ∧ 𝑣 ∈ ℝ+ ∧ ∀ 𝑤 ∈ ( 𝐴 ∩ ( 𝐵 (,) +∞ ) ) ( ( 𝑤 ≠ 𝐵 ∧ ( abs ‘ ( 𝑤 − 𝐵 ) ) < 𝑣 ) → ( abs ‘ ( ( ( 𝐹 ↾ ( 𝐵 (,) +∞ ) ) ‘ 𝑤 ) − 𝑅 ) ) < 𝑦 ) ) ∧ 𝑏 ∈ ( ( 𝐴 ∩ ( 𝐵 (,) +∞ ) ) ∖ { 𝐵 } ) ∧ ( ( abs ‘ ( 𝑏 − 𝐵 ) ) < 𝑧 ∧ ( abs ‘ ( 𝑏 − 𝐵 ) ) < 𝑣 ) ) → ∃ 𝑏 ∈ 𝐴 ( ( abs ‘ ( ( 𝐹 ‘ 𝑏 ) − 𝑥 ) ) < 𝑦 ∧ ( abs ‘ ( ( 𝐹 ‘ 𝑏 ) − 𝑅 ) ) < 𝑦 ) )
175 174 3exp ⊢ ( ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ+ ) ∧ 𝑧 ∈ ℝ+ ∧ ∀ 𝑤 ∈ 𝐴 ( ( 𝑤 ≠ 𝐵 ∧ ( abs ‘ ( 𝑤 − 𝐵 ) ) < 𝑧 ) → ( abs ‘ ( ( 𝐹 ‘ 𝑤 ) − 𝑥 ) ) < 𝑦 ) ) ∧ 𝑣 ∈ ℝ+ ∧ ∀ 𝑤 ∈ ( 𝐴 ∩ ( 𝐵 (,) +∞ ) ) ( ( 𝑤 ≠ 𝐵 ∧ ( abs ‘ ( 𝑤 − 𝐵 ) ) < 𝑣 ) → ( abs ‘ ( ( ( 𝐹 ↾ ( 𝐵 (,) +∞ ) ) ‘ 𝑤 ) − 𝑅 ) ) < 𝑦 ) ) → ( 𝑏 ∈ ( ( 𝐴 ∩ ( 𝐵 (,) +∞ ) ) ∖ { 𝐵 } ) → ( ( ( abs ‘ ( 𝑏 − 𝐵 ) ) < 𝑧 ∧ ( abs ‘ ( 𝑏 − 𝐵 ) ) < 𝑣 ) → ∃ 𝑏 ∈ 𝐴 ( ( abs ‘ ( ( 𝐹 ‘ 𝑏 ) − 𝑥 ) ) < 𝑦 ∧ ( abs ‘ ( ( 𝐹 ‘ 𝑏 ) − 𝑅 ) ) < 𝑦 ) ) ) )
176 128 129 175 rexlimd ⊢ ( ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ+ ) ∧ 𝑧 ∈ ℝ+ ∧ ∀ 𝑤 ∈ 𝐴 ( ( 𝑤 ≠ 𝐵 ∧ ( abs ‘ ( 𝑤 − 𝐵 ) ) < 𝑧 ) → ( abs ‘ ( ( 𝐹 ‘ 𝑤 ) − 𝑥 ) ) < 𝑦 ) ) ∧ 𝑣 ∈ ℝ+ ∧ ∀ 𝑤 ∈ ( 𝐴 ∩ ( 𝐵 (,) +∞ ) ) ( ( 𝑤 ≠ 𝐵 ∧ ( abs ‘ ( 𝑤 − 𝐵 ) ) < 𝑣 ) → ( abs ‘ ( ( ( 𝐹 ↾ ( 𝐵 (,) +∞ ) ) ‘ 𝑤 ) − 𝑅 ) ) < 𝑦 ) ) → ( ∃ 𝑏 ∈ ( ( 𝐴 ∩ ( 𝐵 (,) +∞ ) ) ∖ { 𝐵 } ) ( ( abs ‘ ( 𝑏 − 𝐵 ) ) < 𝑧 ∧ ( abs ‘ ( 𝑏 − 𝐵 ) ) < 𝑣 ) → ∃ 𝑏 ∈ 𝐴 ( ( abs ‘ ( ( 𝐹 ‘ 𝑏 ) − 𝑥 ) ) < 𝑦 ∧ ( abs ‘ ( ( 𝐹 ‘ 𝑏 ) − 𝑅 ) ) < 𝑦 ) ) )
177 127 176 mpd ⊢ ( ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ+ ) ∧ 𝑧 ∈ ℝ+ ∧ ∀ 𝑤 ∈ 𝐴 ( ( 𝑤 ≠ 𝐵 ∧ ( abs ‘ ( 𝑤 − 𝐵 ) ) < 𝑧 ) → ( abs ‘ ( ( 𝐹 ‘ 𝑤 ) − 𝑥 ) ) < 𝑦 ) ) ∧ 𝑣 ∈ ℝ+ ∧ ∀ 𝑤 ∈ ( 𝐴 ∩ ( 𝐵 (,) +∞ ) ) ( ( 𝑤 ≠ 𝐵 ∧ ( abs ‘ ( 𝑤 − 𝐵 ) ) < 𝑣 ) → ( abs ‘ ( ( ( 𝐹 ↾ ( 𝐵 (,) +∞ ) ) ‘ 𝑤 ) − 𝑅 ) ) < 𝑦 ) ) → ∃ 𝑏 ∈ 𝐴 ( ( abs ‘ ( ( 𝐹 ‘ 𝑏 ) − 𝑥 ) ) < 𝑦 ∧ ( abs ‘ ( ( 𝐹 ‘ 𝑏 ) − 𝑅 ) ) < 𝑦 ) )
178 177 3exp ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ+ ) ∧ 𝑧 ∈ ℝ+ ∧ ∀ 𝑤 ∈ 𝐴 ( ( 𝑤 ≠ 𝐵 ∧ ( abs ‘ ( 𝑤 − 𝐵 ) ) < 𝑧 ) → ( abs ‘ ( ( 𝐹 ‘ 𝑤 ) − 𝑥 ) ) < 𝑦 ) ) → ( 𝑣 ∈ ℝ+ → ( ∀ 𝑤 ∈ ( 𝐴 ∩ ( 𝐵 (,) +∞ ) ) ( ( 𝑤 ≠ 𝐵 ∧ ( abs ‘ ( 𝑤 − 𝐵 ) ) < 𝑣 ) → ( abs ‘ ( ( ( 𝐹 ↾ ( 𝐵 (,) +∞ ) ) ‘ 𝑤 ) − 𝑅 ) ) < 𝑦 ) → ∃ 𝑏 ∈ 𝐴 ( ( abs ‘ ( ( 𝐹 ‘ 𝑏 ) − 𝑥 ) ) < 𝑦 ∧ ( abs ‘ ( ( 𝐹 ‘ 𝑏 ) − 𝑅 ) ) < 𝑦 ) ) ) )
179 178 rexlimdv ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ+ ) ∧ 𝑧 ∈ ℝ+ ∧ ∀ 𝑤 ∈ 𝐴 ( ( 𝑤 ≠ 𝐵 ∧ ( abs ‘ ( 𝑤 − 𝐵 ) ) < 𝑧 ) → ( abs ‘ ( ( 𝐹 ‘ 𝑤 ) − 𝑥 ) ) < 𝑦 ) ) → ( ∃ 𝑣 ∈ ℝ+ ∀ 𝑤 ∈ ( 𝐴 ∩ ( 𝐵 (,) +∞ ) ) ( ( 𝑤 ≠ 𝐵 ∧ ( abs ‘ ( 𝑤 − 𝐵 ) ) < 𝑣 ) → ( abs ‘ ( ( ( 𝐹 ↾ ( 𝐵 (,) +∞ ) ) ‘ 𝑤 ) − 𝑅 ) ) < 𝑦 ) → ∃ 𝑏 ∈ 𝐴 ( ( abs ‘ ( ( 𝐹 ‘ 𝑏 ) − 𝑥 ) ) < 𝑦 ∧ ( abs ‘ ( ( 𝐹 ‘ 𝑏 ) − 𝑅 ) ) < 𝑦 ) ) )
180 64 179 mpd ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ+ ) ∧ 𝑧 ∈ ℝ+ ∧ ∀ 𝑤 ∈ 𝐴 ( ( 𝑤 ≠ 𝐵 ∧ ( abs ‘ ( 𝑤 − 𝐵 ) ) < 𝑧 ) → ( abs ‘ ( ( 𝐹 ‘ 𝑤 ) − 𝑥 ) ) < 𝑦 ) ) → ∃ 𝑏 ∈ 𝐴 ( ( abs ‘ ( ( 𝐹 ‘ 𝑏 ) − 𝑥 ) ) < 𝑦 ∧ ( abs ‘ ( ( 𝐹 ‘ 𝑏 ) − 𝑅 ) ) < 𝑦 ) )
181 180 3exp ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ℝ+ ) → ( 𝑧 ∈ ℝ+ → ( ∀ 𝑤 ∈ 𝐴 ( ( 𝑤 ≠ 𝐵 ∧ ( abs ‘ ( 𝑤 − 𝐵 ) ) < 𝑧 ) → ( abs ‘ ( ( 𝐹 ‘ 𝑤 ) − 𝑥 ) ) < 𝑦 ) → ∃ 𝑏 ∈ 𝐴 ( ( abs ‘ ( ( 𝐹 ‘ 𝑏 ) − 𝑥 ) ) < 𝑦 ∧ ( abs ‘ ( ( 𝐹 ‘ 𝑏 ) − 𝑅 ) ) < 𝑦 ) ) ) )
182 181 rexlimdv ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ℝ+ ) → ( ∃ 𝑧 ∈ ℝ+ ∀ 𝑤 ∈ 𝐴 ( ( 𝑤 ≠ 𝐵 ∧ ( abs ‘ ( 𝑤 − 𝐵 ) ) < 𝑧 ) → ( abs ‘ ( ( 𝐹 ‘ 𝑤 ) − 𝑥 ) ) < 𝑦 ) → ∃ 𝑏 ∈ 𝐴 ( ( abs ‘ ( ( 𝐹 ‘ 𝑏 ) − 𝑥 ) ) < 𝑦 ∧ ( abs ‘ ( ( 𝐹 ‘ 𝑏 ) − 𝑅 ) ) < 𝑦 ) ) )
183 182 imp ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ+ ) ∧ ∃ 𝑧 ∈ ℝ+ ∀ 𝑤 ∈ 𝐴 ( ( 𝑤 ≠ 𝐵 ∧ ( abs ‘ ( 𝑤 − 𝐵 ) ) < 𝑧 ) → ( abs ‘ ( ( 𝐹 ‘ 𝑤 ) − 𝑥 ) ) < 𝑦 ) ) → ∃ 𝑏 ∈ 𝐴 ( ( abs ‘ ( ( 𝐹 ‘ 𝑏 ) − 𝑥 ) ) < 𝑦 ∧ ( abs ‘ ( ( 𝐹 ‘ 𝑏 ) − 𝑅 ) ) < 𝑦 ) )
184 183 adantllr ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ ℂ ) ∧ 𝑦 ∈ ℝ+ ) ∧ ∃ 𝑧 ∈ ℝ+ ∀ 𝑤 ∈ 𝐴 ( ( 𝑤 ≠ 𝐵 ∧ ( abs ‘ ( 𝑤 − 𝐵 ) ) < 𝑧 ) → ( abs ‘ ( ( 𝐹 ‘ 𝑤 ) − 𝑥 ) ) < 𝑦 ) ) → ∃ 𝑏 ∈ 𝐴 ( ( abs ‘ ( ( 𝐹 ‘ 𝑏 ) − 𝑥 ) ) < 𝑦 ∧ ( abs ‘ ( ( 𝐹 ‘ 𝑏 ) − 𝑅 ) ) < 𝑦 ) )
185 184 ad2antrr ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ ℂ ) ∧ 𝑦 ∈ ℝ+ ) ∧ ∃ 𝑧 ∈ ℝ+ ∀ 𝑤 ∈ 𝐴 ( ( 𝑤 ≠ 𝐵 ∧ ( abs ‘ ( 𝑤 − 𝐵 ) ) < 𝑧 ) → ( abs ‘ ( ( 𝐹 ‘ 𝑤 ) − 𝑥 ) ) < 𝑦 ) ) ∧ 𝑎 ∈ 𝐴 ) ∧ ( ( abs ‘ ( ( 𝐹 ‘ 𝑎 ) − 𝑥 ) ) < 𝑦 ∧ ( abs ‘ ( ( 𝐹 ‘ 𝑎 ) − 𝐿 ) ) < 𝑦 ) ) → ∃ 𝑏 ∈ 𝐴 ( ( abs ‘ ( ( 𝐹 ‘ 𝑏 ) − 𝑥 ) ) < 𝑦 ∧ ( abs ‘ ( ( 𝐹 ‘ 𝑏 ) − 𝑅 ) ) < 𝑦 ) )
186 11 ad6antr ⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ ℂ ) ∧ 𝑦 ∈ ℝ+ ) ∧ 𝑎 ∈ 𝐴 ) ∧ ( ( abs ‘ ( ( 𝐹 ‘ 𝑎 ) − 𝑥 ) ) < 𝑦 ∧ ( abs ‘ ( ( 𝐹 ‘ 𝑎 ) − 𝐿 ) ) < 𝑦 ) ) ∧ 𝑏 ∈ 𝐴 ) ∧ ( ( abs ‘ ( ( 𝐹 ‘ 𝑏 ) − 𝑥 ) ) < 𝑦 ∧ ( abs ‘ ( ( 𝐹 ‘ 𝑏 ) − 𝑅 ) ) < 𝑦 ) ) → 𝑅 ∈ ℂ )
187 14 ad6antr ⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ ℂ ) ∧ 𝑦 ∈ ℝ+ ) ∧ 𝑎 ∈ 𝐴 ) ∧ ( ( abs ‘ ( ( 𝐹 ‘ 𝑎 ) − 𝑥 ) ) < 𝑦 ∧ ( abs ‘ ( ( 𝐹 ‘ 𝑎 ) − 𝐿 ) ) < 𝑦 ) ) ∧ 𝑏 ∈ 𝐴 ) ∧ ( ( abs ‘ ( ( 𝐹 ‘ 𝑏 ) − 𝑥 ) ) < 𝑦 ∧ ( abs ‘ ( ( 𝐹 ‘ 𝑏 ) − 𝑅 ) ) < 𝑦 ) ) → 𝐿 ∈ ℂ )
188 186 187 subcld ⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ ℂ ) ∧ 𝑦 ∈ ℝ+ ) ∧ 𝑎 ∈ 𝐴 ) ∧ ( ( abs ‘ ( ( 𝐹 ‘ 𝑎 ) − 𝑥 ) ) < 𝑦 ∧ ( abs ‘ ( ( 𝐹 ‘ 𝑎 ) − 𝐿 ) ) < 𝑦 ) ) ∧ 𝑏 ∈ 𝐴 ) ∧ ( ( abs ‘ ( ( 𝐹 ‘ 𝑏 ) − 𝑥 ) ) < 𝑦 ∧ ( abs ‘ ( ( 𝐹 ‘ 𝑏 ) − 𝑅 ) ) < 𝑦 ) ) → ( 𝑅 − 𝐿 ) ∈ ℂ )
189 188 abscld ⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ ℂ ) ∧ 𝑦 ∈ ℝ+ ) ∧ 𝑎 ∈ 𝐴 ) ∧ ( ( abs ‘ ( ( 𝐹 ‘ 𝑎 ) − 𝑥 ) ) < 𝑦 ∧ ( abs ‘ ( ( 𝐹 ‘ 𝑎 ) − 𝐿 ) ) < 𝑦 ) ) ∧ 𝑏 ∈ 𝐴 ) ∧ ( ( abs ‘ ( ( 𝐹 ‘ 𝑏 ) − 𝑥 ) ) < 𝑦 ∧ ( abs ‘ ( ( 𝐹 ‘ 𝑏 ) − 𝑅 ) ) < 𝑦 ) ) → ( abs ‘ ( 𝑅 − 𝐿 ) ) ∈ ℝ )
190 simp-6l ⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ ℂ ) ∧ 𝑦 ∈ ℝ+ ) ∧ 𝑎 ∈ 𝐴 ) ∧ ( ( abs ‘ ( ( 𝐹 ‘ 𝑎 ) − 𝑥 ) ) < 𝑦 ∧ ( abs ‘ ( ( 𝐹 ‘ 𝑎 ) − 𝐿 ) ) < 𝑦 ) ) ∧ 𝑏 ∈ 𝐴 ) ∧ ( ( abs ‘ ( ( 𝐹 ‘ 𝑏 ) − 𝑥 ) ) < 𝑦 ∧ ( abs ‘ ( ( 𝐹 ‘ 𝑏 ) − 𝑅 ) ) < 𝑦 ) ) → 𝜑 )
191 simplr ⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ ℂ ) ∧ 𝑦 ∈ ℝ+ ) ∧ 𝑎 ∈ 𝐴 ) ∧ ( ( abs ‘ ( ( 𝐹 ‘ 𝑎 ) − 𝑥 ) ) < 𝑦 ∧ ( abs ‘ ( ( 𝐹 ‘ 𝑎 ) − 𝐿 ) ) < 𝑦 ) ) ∧ 𝑏 ∈ 𝐴 ) ∧ ( ( abs ‘ ( ( 𝐹 ‘ 𝑏 ) − 𝑥 ) ) < 𝑦 ∧ ( abs ‘ ( ( 𝐹 ‘ 𝑏 ) − 𝑅 ) ) < 𝑦 ) ) → 𝑏 ∈ 𝐴 )
192 4 ffvelcdmda ⊢ ( ( 𝜑 ∧ 𝑏 ∈ 𝐴 ) → ( 𝐹 ‘ 𝑏 ) ∈ ℂ )
193 190 191 192 syl2anc ⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ ℂ ) ∧ 𝑦 ∈ ℝ+ ) ∧ 𝑎 ∈ 𝐴 ) ∧ ( ( abs ‘ ( ( 𝐹 ‘ 𝑎 ) − 𝑥 ) ) < 𝑦 ∧ ( abs ‘ ( ( 𝐹 ‘ 𝑎 ) − 𝐿 ) ) < 𝑦 ) ) ∧ 𝑏 ∈ 𝐴 ) ∧ ( ( abs ‘ ( ( 𝐹 ‘ 𝑏 ) − 𝑥 ) ) < 𝑦 ∧ ( abs ‘ ( ( 𝐹 ‘ 𝑏 ) − 𝑅 ) ) < 𝑦 ) ) → ( 𝐹 ‘ 𝑏 ) ∈ ℂ )
194 186 193 subcld ⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ ℂ ) ∧ 𝑦 ∈ ℝ+ ) ∧ 𝑎 ∈ 𝐴 ) ∧ ( ( abs ‘ ( ( 𝐹 ‘ 𝑎 ) − 𝑥 ) ) < 𝑦 ∧ ( abs ‘ ( ( 𝐹 ‘ 𝑎 ) − 𝐿 ) ) < 𝑦 ) ) ∧ 𝑏 ∈ 𝐴 ) ∧ ( ( abs ‘ ( ( 𝐹 ‘ 𝑏 ) − 𝑥 ) ) < 𝑦 ∧ ( abs ‘ ( ( 𝐹 ‘ 𝑏 ) − 𝑅 ) ) < 𝑦 ) ) → ( 𝑅 − ( 𝐹 ‘ 𝑏 ) ) ∈ ℂ )
195 194 abscld ⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ ℂ ) ∧ 𝑦 ∈ ℝ+ ) ∧ 𝑎 ∈ 𝐴 ) ∧ ( ( abs ‘ ( ( 𝐹 ‘ 𝑎 ) − 𝑥 ) ) < 𝑦 ∧ ( abs ‘ ( ( 𝐹 ‘ 𝑎 ) − 𝐿 ) ) < 𝑦 ) ) ∧ 𝑏 ∈ 𝐴 ) ∧ ( ( abs ‘ ( ( 𝐹 ‘ 𝑏 ) − 𝑥 ) ) < 𝑦 ∧ ( abs ‘ ( ( 𝐹 ‘ 𝑏 ) − 𝑅 ) ) < 𝑦 ) ) → ( abs ‘ ( 𝑅 − ( 𝐹 ‘ 𝑏 ) ) ) ∈ ℝ )
196 simp-6r ⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ ℂ ) ∧ 𝑦 ∈ ℝ+ ) ∧ 𝑎 ∈ 𝐴 ) ∧ ( ( abs ‘ ( ( 𝐹 ‘ 𝑎 ) − 𝑥 ) ) < 𝑦 ∧ ( abs ‘ ( ( 𝐹 ‘ 𝑎 ) − 𝐿 ) ) < 𝑦 ) ) ∧ 𝑏 ∈ 𝐴 ) ∧ ( ( abs ‘ ( ( 𝐹 ‘ 𝑏 ) − 𝑥 ) ) < 𝑦 ∧ ( abs ‘ ( ( 𝐹 ‘ 𝑏 ) − 𝑅 ) ) < 𝑦 ) ) → 𝑥 ∈ ℂ )
197 193 196 subcld ⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ ℂ ) ∧ 𝑦 ∈ ℝ+ ) ∧ 𝑎 ∈ 𝐴 ) ∧ ( ( abs ‘ ( ( 𝐹 ‘ 𝑎 ) − 𝑥 ) ) < 𝑦 ∧ ( abs ‘ ( ( 𝐹 ‘ 𝑎 ) − 𝐿 ) ) < 𝑦 ) ) ∧ 𝑏 ∈ 𝐴 ) ∧ ( ( abs ‘ ( ( 𝐹 ‘ 𝑏 ) − 𝑥 ) ) < 𝑦 ∧ ( abs ‘ ( ( 𝐹 ‘ 𝑏 ) − 𝑅 ) ) < 𝑦 ) ) → ( ( 𝐹 ‘ 𝑏 ) − 𝑥 ) ∈ ℂ )
198 197 abscld ⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ ℂ ) ∧ 𝑦 ∈ ℝ+ ) ∧ 𝑎 ∈ 𝐴 ) ∧ ( ( abs ‘ ( ( 𝐹 ‘ 𝑎 ) − 𝑥 ) ) < 𝑦 ∧ ( abs ‘ ( ( 𝐹 ‘ 𝑎 ) − 𝐿 ) ) < 𝑦 ) ) ∧ 𝑏 ∈ 𝐴 ) ∧ ( ( abs ‘ ( ( 𝐹 ‘ 𝑏 ) − 𝑥 ) ) < 𝑦 ∧ ( abs ‘ ( ( 𝐹 ‘ 𝑏 ) − 𝑅 ) ) < 𝑦 ) ) → ( abs ‘ ( ( 𝐹 ‘ 𝑏 ) − 𝑥 ) ) ∈ ℝ )
199 195 198 readdcld ⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ ℂ ) ∧ 𝑦 ∈ ℝ+ ) ∧ 𝑎 ∈ 𝐴 ) ∧ ( ( abs ‘ ( ( 𝐹 ‘ 𝑎 ) − 𝑥 ) ) < 𝑦 ∧ ( abs ‘ ( ( 𝐹 ‘ 𝑎 ) − 𝐿 ) ) < 𝑦 ) ) ∧ 𝑏 ∈ 𝐴 ) ∧ ( ( abs ‘ ( ( 𝐹 ‘ 𝑏 ) − 𝑥 ) ) < 𝑦 ∧ ( abs ‘ ( ( 𝐹 ‘ 𝑏 ) − 𝑅 ) ) < 𝑦 ) ) → ( ( abs ‘ ( 𝑅 − ( 𝐹 ‘ 𝑏 ) ) ) + ( abs ‘ ( ( 𝐹 ‘ 𝑏 ) − 𝑥 ) ) ) ∈ ℝ )
200 simp-4r ⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ ℂ ) ∧ 𝑦 ∈ ℝ+ ) ∧ 𝑎 ∈ 𝐴 ) ∧ ( ( abs ‘ ( ( 𝐹 ‘ 𝑎 ) − 𝑥 ) ) < 𝑦 ∧ ( abs ‘ ( ( 𝐹 ‘ 𝑎 ) − 𝐿 ) ) < 𝑦 ) ) ∧ 𝑏 ∈ 𝐴 ) ∧ ( ( abs ‘ ( ( 𝐹 ‘ 𝑏 ) − 𝑥 ) ) < 𝑦 ∧ ( abs ‘ ( ( 𝐹 ‘ 𝑏 ) − 𝑅 ) ) < 𝑦 ) ) → 𝑎 ∈ 𝐴 )
201 4 ffvelcdmda ⊢ ( ( 𝜑 ∧ 𝑎 ∈ 𝐴 ) → ( 𝐹 ‘ 𝑎 ) ∈ ℂ )
202 190 200 201 syl2anc ⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ ℂ ) ∧ 𝑦 ∈ ℝ+ ) ∧ 𝑎 ∈ 𝐴 ) ∧ ( ( abs ‘ ( ( 𝐹 ‘ 𝑎 ) − 𝑥 ) ) < 𝑦 ∧ ( abs ‘ ( ( 𝐹 ‘ 𝑎 ) − 𝐿 ) ) < 𝑦 ) ) ∧ 𝑏 ∈ 𝐴 ) ∧ ( ( abs ‘ ( ( 𝐹 ‘ 𝑏 ) − 𝑥 ) ) < 𝑦 ∧ ( abs ‘ ( ( 𝐹 ‘ 𝑏 ) − 𝑅 ) ) < 𝑦 ) ) → ( 𝐹 ‘ 𝑎 ) ∈ ℂ )
203 196 202 subcld ⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ ℂ ) ∧ 𝑦 ∈ ℝ+ ) ∧ 𝑎 ∈ 𝐴 ) ∧ ( ( abs ‘ ( ( 𝐹 ‘ 𝑎 ) − 𝑥 ) ) < 𝑦 ∧ ( abs ‘ ( ( 𝐹 ‘ 𝑎 ) − 𝐿 ) ) < 𝑦 ) ) ∧ 𝑏 ∈ 𝐴 ) ∧ ( ( abs ‘ ( ( 𝐹 ‘ 𝑏 ) − 𝑥 ) ) < 𝑦 ∧ ( abs ‘ ( ( 𝐹 ‘ 𝑏 ) − 𝑅 ) ) < 𝑦 ) ) → ( 𝑥 − ( 𝐹 ‘ 𝑎 ) ) ∈ ℂ )
204 203 abscld ⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ ℂ ) ∧ 𝑦 ∈ ℝ+ ) ∧ 𝑎 ∈ 𝐴 ) ∧ ( ( abs ‘ ( ( 𝐹 ‘ 𝑎 ) − 𝑥 ) ) < 𝑦 ∧ ( abs ‘ ( ( 𝐹 ‘ 𝑎 ) − 𝐿 ) ) < 𝑦 ) ) ∧ 𝑏 ∈ 𝐴 ) ∧ ( ( abs ‘ ( ( 𝐹 ‘ 𝑏 ) − 𝑥 ) ) < 𝑦 ∧ ( abs ‘ ( ( 𝐹 ‘ 𝑏 ) − 𝑅 ) ) < 𝑦 ) ) → ( abs ‘ ( 𝑥 − ( 𝐹 ‘ 𝑎 ) ) ) ∈ ℝ )
205 199 204 readdcld ⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ ℂ ) ∧ 𝑦 ∈ ℝ+ ) ∧ 𝑎 ∈ 𝐴 ) ∧ ( ( abs ‘ ( ( 𝐹 ‘ 𝑎 ) − 𝑥 ) ) < 𝑦 ∧ ( abs ‘ ( ( 𝐹 ‘ 𝑎 ) − 𝐿 ) ) < 𝑦 ) ) ∧ 𝑏 ∈ 𝐴 ) ∧ ( ( abs ‘ ( ( 𝐹 ‘ 𝑏 ) − 𝑥 ) ) < 𝑦 ∧ ( abs ‘ ( ( 𝐹 ‘ 𝑏 ) − 𝑅 ) ) < 𝑦 ) ) → ( ( ( abs ‘ ( 𝑅 − ( 𝐹 ‘ 𝑏 ) ) ) + ( abs ‘ ( ( 𝐹 ‘ 𝑏 ) − 𝑥 ) ) ) + ( abs ‘ ( 𝑥 − ( 𝐹 ‘ 𝑎 ) ) ) ) ∈ ℝ )
206 202 187 subcld ⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ ℂ ) ∧ 𝑦 ∈ ℝ+ ) ∧ 𝑎 ∈ 𝐴 ) ∧ ( ( abs ‘ ( ( 𝐹 ‘ 𝑎 ) − 𝑥 ) ) < 𝑦 ∧ ( abs ‘ ( ( 𝐹 ‘ 𝑎 ) − 𝐿 ) ) < 𝑦 ) ) ∧ 𝑏 ∈ 𝐴 ) ∧ ( ( abs ‘ ( ( 𝐹 ‘ 𝑏 ) − 𝑥 ) ) < 𝑦 ∧ ( abs ‘ ( ( 𝐹 ‘ 𝑏 ) − 𝑅 ) ) < 𝑦 ) ) → ( ( 𝐹 ‘ 𝑎 ) − 𝐿 ) ∈ ℂ )
207 206 abscld ⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ ℂ ) ∧ 𝑦 ∈ ℝ+ ) ∧ 𝑎 ∈ 𝐴 ) ∧ ( ( abs ‘ ( ( 𝐹 ‘ 𝑎 ) − 𝑥 ) ) < 𝑦 ∧ ( abs ‘ ( ( 𝐹 ‘ 𝑎 ) − 𝐿 ) ) < 𝑦 ) ) ∧ 𝑏 ∈ 𝐴 ) ∧ ( ( abs ‘ ( ( 𝐹 ‘ 𝑏 ) − 𝑥 ) ) < 𝑦 ∧ ( abs ‘ ( ( 𝐹 ‘ 𝑏 ) − 𝑅 ) ) < 𝑦 ) ) → ( abs ‘ ( ( 𝐹 ‘ 𝑎 ) − 𝐿 ) ) ∈ ℝ )
208 205 207 readdcld ⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ ℂ ) ∧ 𝑦 ∈ ℝ+ ) ∧ 𝑎 ∈ 𝐴 ) ∧ ( ( abs ‘ ( ( 𝐹 ‘ 𝑎 ) − 𝑥 ) ) < 𝑦 ∧ ( abs ‘ ( ( 𝐹 ‘ 𝑎 ) − 𝐿 ) ) < 𝑦 ) ) ∧ 𝑏 ∈ 𝐴 ) ∧ ( ( abs ‘ ( ( 𝐹 ‘ 𝑏 ) − 𝑥 ) ) < 𝑦 ∧ ( abs ‘ ( ( 𝐹 ‘ 𝑏 ) − 𝑅 ) ) < 𝑦 ) ) → ( ( ( ( abs ‘ ( 𝑅 − ( 𝐹 ‘ 𝑏 ) ) ) + ( abs ‘ ( ( 𝐹 ‘ 𝑏 ) − 𝑥 ) ) ) + ( abs ‘ ( 𝑥 − ( 𝐹 ‘ 𝑎 ) ) ) ) + ( abs ‘ ( ( 𝐹 ‘ 𝑎 ) − 𝐿 ) ) ) ∈ ℝ )
209 21 a1i ⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ ℂ ) ∧ 𝑦 ∈ ℝ+ ) ∧ 𝑎 ∈ 𝐴 ) ∧ ( ( abs ‘ ( ( 𝐹 ‘ 𝑎 ) − 𝑥 ) ) < 𝑦 ∧ ( abs ‘ ( ( 𝐹 ‘ 𝑎 ) − 𝐿 ) ) < 𝑦 ) ) ∧ 𝑏 ∈ 𝐴 ) ∧ ( ( abs ‘ ( ( 𝐹 ‘ 𝑏 ) − 𝑥 ) ) < 𝑦 ∧ ( abs ‘ ( ( 𝐹 ‘ 𝑏 ) − 𝑅 ) ) < 𝑦 ) ) → 4 ∈ ℝ )
210 rpre ⊢ ( 𝑦 ∈ ℝ+ → 𝑦 ∈ ℝ )
211 210 ad5antlr ⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ ℂ ) ∧ 𝑦 ∈ ℝ+ ) ∧ 𝑎 ∈ 𝐴 ) ∧ ( ( abs ‘ ( ( 𝐹 ‘ 𝑎 ) − 𝑥 ) ) < 𝑦 ∧ ( abs ‘ ( ( 𝐹 ‘ 𝑎 ) − 𝐿 ) ) < 𝑦 ) ) ∧ 𝑏 ∈ 𝐴 ) ∧ ( ( abs ‘ ( ( 𝐹 ‘ 𝑏 ) − 𝑥 ) ) < 𝑦 ∧ ( abs ‘ ( ( 𝐹 ‘ 𝑏 ) − 𝑅 ) ) < 𝑦 ) ) → 𝑦 ∈ ℝ )
212 209 211 remulcld ⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ ℂ ) ∧ 𝑦 ∈ ℝ+ ) ∧ 𝑎 ∈ 𝐴 ) ∧ ( ( abs ‘ ( ( 𝐹 ‘ 𝑎 ) − 𝑥 ) ) < 𝑦 ∧ ( abs ‘ ( ( 𝐹 ‘ 𝑎 ) − 𝐿 ) ) < 𝑦 ) ) ∧ 𝑏 ∈ 𝐴 ) ∧ ( ( abs ‘ ( ( 𝐹 ‘ 𝑏 ) − 𝑥 ) ) < 𝑦 ∧ ( abs ‘ ( ( 𝐹 ‘ 𝑏 ) − 𝑅 ) ) < 𝑦 ) ) → ( 4 · 𝑦 ) ∈ ℝ )
213 186 193 196 202 187 absnpncan3d ⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ ℂ ) ∧ 𝑦 ∈ ℝ+ ) ∧ 𝑎 ∈ 𝐴 ) ∧ ( ( abs ‘ ( ( 𝐹 ‘ 𝑎 ) − 𝑥 ) ) < 𝑦 ∧ ( abs ‘ ( ( 𝐹 ‘ 𝑎 ) − 𝐿 ) ) < 𝑦 ) ) ∧ 𝑏 ∈ 𝐴 ) ∧ ( ( abs ‘ ( ( 𝐹 ‘ 𝑏 ) − 𝑥 ) ) < 𝑦 ∧ ( abs ‘ ( ( 𝐹 ‘ 𝑏 ) − 𝑅 ) ) < 𝑦 ) ) → ( abs ‘ ( 𝑅 − 𝐿 ) ) ≤ ( ( ( ( abs ‘ ( 𝑅 − ( 𝐹 ‘ 𝑏 ) ) ) + ( abs ‘ ( ( 𝐹 ‘ 𝑏 ) − 𝑥 ) ) ) + ( abs ‘ ( 𝑥 − ( 𝐹 ‘ 𝑎 ) ) ) ) + ( abs ‘ ( ( 𝐹 ‘ 𝑎 ) − 𝐿 ) ) ) )
214 186 193 abssubd ⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ ℂ ) ∧ 𝑦 ∈ ℝ+ ) ∧ 𝑎 ∈ 𝐴 ) ∧ ( ( abs ‘ ( ( 𝐹 ‘ 𝑎 ) − 𝑥 ) ) < 𝑦 ∧ ( abs ‘ ( ( 𝐹 ‘ 𝑎 ) − 𝐿 ) ) < 𝑦 ) ) ∧ 𝑏 ∈ 𝐴 ) ∧ ( ( abs ‘ ( ( 𝐹 ‘ 𝑏 ) − 𝑥 ) ) < 𝑦 ∧ ( abs ‘ ( ( 𝐹 ‘ 𝑏 ) − 𝑅 ) ) < 𝑦 ) ) → ( abs ‘ ( 𝑅 − ( 𝐹 ‘ 𝑏 ) ) ) = ( abs ‘ ( ( 𝐹 ‘ 𝑏 ) − 𝑅 ) ) )
215 simprr ⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ ℂ ) ∧ 𝑦 ∈ ℝ+ ) ∧ 𝑎 ∈ 𝐴 ) ∧ ( ( abs ‘ ( ( 𝐹 ‘ 𝑎 ) − 𝑥 ) ) < 𝑦 ∧ ( abs ‘ ( ( 𝐹 ‘ 𝑎 ) − 𝐿 ) ) < 𝑦 ) ) ∧ 𝑏 ∈ 𝐴 ) ∧ ( ( abs ‘ ( ( 𝐹 ‘ 𝑏 ) − 𝑥 ) ) < 𝑦 ∧ ( abs ‘ ( ( 𝐹 ‘ 𝑏 ) − 𝑅 ) ) < 𝑦 ) ) → ( abs ‘ ( ( 𝐹 ‘ 𝑏 ) − 𝑅 ) ) < 𝑦 )
216 214 215 eqbrtrd ⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ ℂ ) ∧ 𝑦 ∈ ℝ+ ) ∧ 𝑎 ∈ 𝐴 ) ∧ ( ( abs ‘ ( ( 𝐹 ‘ 𝑎 ) − 𝑥 ) ) < 𝑦 ∧ ( abs ‘ ( ( 𝐹 ‘ 𝑎 ) − 𝐿 ) ) < 𝑦 ) ) ∧ 𝑏 ∈ 𝐴 ) ∧ ( ( abs ‘ ( ( 𝐹 ‘ 𝑏 ) − 𝑥 ) ) < 𝑦 ∧ ( abs ‘ ( ( 𝐹 ‘ 𝑏 ) − 𝑅 ) ) < 𝑦 ) ) → ( abs ‘ ( 𝑅 − ( 𝐹 ‘ 𝑏 ) ) ) < 𝑦 )
217 simprl ⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ ℂ ) ∧ 𝑦 ∈ ℝ+ ) ∧ 𝑎 ∈ 𝐴 ) ∧ ( ( abs ‘ ( ( 𝐹 ‘ 𝑎 ) − 𝑥 ) ) < 𝑦 ∧ ( abs ‘ ( ( 𝐹 ‘ 𝑎 ) − 𝐿 ) ) < 𝑦 ) ) ∧ 𝑏 ∈ 𝐴 ) ∧ ( ( abs ‘ ( ( 𝐹 ‘ 𝑏 ) − 𝑥 ) ) < 𝑦 ∧ ( abs ‘ ( ( 𝐹 ‘ 𝑏 ) − 𝑅 ) ) < 𝑦 ) ) → ( abs ‘ ( ( 𝐹 ‘ 𝑏 ) − 𝑥 ) ) < 𝑦 )
218 simp-5r ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ ℂ ) ∧ 𝑦 ∈ ℝ+ ) ∧ 𝑎 ∈ 𝐴 ) ∧ ( ( abs ‘ ( ( 𝐹 ‘ 𝑎 ) − 𝑥 ) ) < 𝑦 ∧ ( abs ‘ ( ( 𝐹 ‘ 𝑎 ) − 𝐿 ) ) < 𝑦 ) ) ∧ 𝑏 ∈ 𝐴 ) → 𝑥 ∈ ℂ )
219 201 ad5ant14 ⊢ ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ ℂ ) ∧ 𝑦 ∈ ℝ+ ) ∧ 𝑎 ∈ 𝐴 ) ∧ ( ( abs ‘ ( ( 𝐹 ‘ 𝑎 ) − 𝑥 ) ) < 𝑦 ∧ ( abs ‘ ( ( 𝐹 ‘ 𝑎 ) − 𝐿 ) ) < 𝑦 ) ) → ( 𝐹 ‘ 𝑎 ) ∈ ℂ )
220 219 adantr ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ ℂ ) ∧ 𝑦 ∈ ℝ+ ) ∧ 𝑎 ∈ 𝐴 ) ∧ ( ( abs ‘ ( ( 𝐹 ‘ 𝑎 ) − 𝑥 ) ) < 𝑦 ∧ ( abs ‘ ( ( 𝐹 ‘ 𝑎 ) − 𝐿 ) ) < 𝑦 ) ) ∧ 𝑏 ∈ 𝐴 ) → ( 𝐹 ‘ 𝑎 ) ∈ ℂ )
221 218 220 abssubd ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ ℂ ) ∧ 𝑦 ∈ ℝ+ ) ∧ 𝑎 ∈ 𝐴 ) ∧ ( ( abs ‘ ( ( 𝐹 ‘ 𝑎 ) − 𝑥 ) ) < 𝑦 ∧ ( abs ‘ ( ( 𝐹 ‘ 𝑎 ) − 𝐿 ) ) < 𝑦 ) ) ∧ 𝑏 ∈ 𝐴 ) → ( abs ‘ ( 𝑥 − ( 𝐹 ‘ 𝑎 ) ) ) = ( abs ‘ ( ( 𝐹 ‘ 𝑎 ) − 𝑥 ) ) )
222 simplrl ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ ℂ ) ∧ 𝑦 ∈ ℝ+ ) ∧ 𝑎 ∈ 𝐴 ) ∧ ( ( abs ‘ ( ( 𝐹 ‘ 𝑎 ) − 𝑥 ) ) < 𝑦 ∧ ( abs ‘ ( ( 𝐹 ‘ 𝑎 ) − 𝐿 ) ) < 𝑦 ) ) ∧ 𝑏 ∈ 𝐴 ) → ( abs ‘ ( ( 𝐹 ‘ 𝑎 ) − 𝑥 ) ) < 𝑦 )
223 221 222 eqbrtrd ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ ℂ ) ∧ 𝑦 ∈ ℝ+ ) ∧ 𝑎 ∈ 𝐴 ) ∧ ( ( abs ‘ ( ( 𝐹 ‘ 𝑎 ) − 𝑥 ) ) < 𝑦 ∧ ( abs ‘ ( ( 𝐹 ‘ 𝑎 ) − 𝐿 ) ) < 𝑦 ) ) ∧ 𝑏 ∈ 𝐴 ) → ( abs ‘ ( 𝑥 − ( 𝐹 ‘ 𝑎 ) ) ) < 𝑦 )
224 223 adantr ⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ ℂ ) ∧ 𝑦 ∈ ℝ+ ) ∧ 𝑎 ∈ 𝐴 ) ∧ ( ( abs ‘ ( ( 𝐹 ‘ 𝑎 ) − 𝑥 ) ) < 𝑦 ∧ ( abs ‘ ( ( 𝐹 ‘ 𝑎 ) − 𝐿 ) ) < 𝑦 ) ) ∧ 𝑏 ∈ 𝐴 ) ∧ ( ( abs ‘ ( ( 𝐹 ‘ 𝑏 ) − 𝑥 ) ) < 𝑦 ∧ ( abs ‘ ( ( 𝐹 ‘ 𝑏 ) − 𝑅 ) ) < 𝑦 ) ) → ( abs ‘ ( 𝑥 − ( 𝐹 ‘ 𝑎 ) ) ) < 𝑦 )
225 simplrr ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ ℂ ) ∧ 𝑦 ∈ ℝ+ ) ∧ 𝑎 ∈ 𝐴 ) ∧ ( ( abs ‘ ( ( 𝐹 ‘ 𝑎 ) − 𝑥 ) ) < 𝑦 ∧ ( abs ‘ ( ( 𝐹 ‘ 𝑎 ) − 𝐿 ) ) < 𝑦 ) ) ∧ 𝑏 ∈ 𝐴 ) → ( abs ‘ ( ( 𝐹 ‘ 𝑎 ) − 𝐿 ) ) < 𝑦 )
226 225 adantr ⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ ℂ ) ∧ 𝑦 ∈ ℝ+ ) ∧ 𝑎 ∈ 𝐴 ) ∧ ( ( abs ‘ ( ( 𝐹 ‘ 𝑎 ) − 𝑥 ) ) < 𝑦 ∧ ( abs ‘ ( ( 𝐹 ‘ 𝑎 ) − 𝐿 ) ) < 𝑦 ) ) ∧ 𝑏 ∈ 𝐴 ) ∧ ( ( abs ‘ ( ( 𝐹 ‘ 𝑏 ) − 𝑥 ) ) < 𝑦 ∧ ( abs ‘ ( ( 𝐹 ‘ 𝑏 ) − 𝑅 ) ) < 𝑦 ) ) → ( abs ‘ ( ( 𝐹 ‘ 𝑎 ) − 𝐿 ) ) < 𝑦 )
227 195 198 204 207 211 216 217 224 226 lt4addmuld ⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ ℂ ) ∧ 𝑦 ∈ ℝ+ ) ∧ 𝑎 ∈ 𝐴 ) ∧ ( ( abs ‘ ( ( 𝐹 ‘ 𝑎 ) − 𝑥 ) ) < 𝑦 ∧ ( abs ‘ ( ( 𝐹 ‘ 𝑎 ) − 𝐿 ) ) < 𝑦 ) ) ∧ 𝑏 ∈ 𝐴 ) ∧ ( ( abs ‘ ( ( 𝐹 ‘ 𝑏 ) − 𝑥 ) ) < 𝑦 ∧ ( abs ‘ ( ( 𝐹 ‘ 𝑏 ) − 𝑅 ) ) < 𝑦 ) ) → ( ( ( ( abs ‘ ( 𝑅 − ( 𝐹 ‘ 𝑏 ) ) ) + ( abs ‘ ( ( 𝐹 ‘ 𝑏 ) − 𝑥 ) ) ) + ( abs ‘ ( 𝑥 − ( 𝐹 ‘ 𝑎 ) ) ) ) + ( abs ‘ ( ( 𝐹 ‘ 𝑎 ) − 𝐿 ) ) ) < ( 4 · 𝑦 ) )
228 189 208 212 213 227 lelttrd ⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ ℂ ) ∧ 𝑦 ∈ ℝ+ ) ∧ 𝑎 ∈ 𝐴 ) ∧ ( ( abs ‘ ( ( 𝐹 ‘ 𝑎 ) − 𝑥 ) ) < 𝑦 ∧ ( abs ‘ ( ( 𝐹 ‘ 𝑎 ) − 𝐿 ) ) < 𝑦 ) ) ∧ 𝑏 ∈ 𝐴 ) ∧ ( ( abs ‘ ( ( 𝐹 ‘ 𝑏 ) − 𝑥 ) ) < 𝑦 ∧ ( abs ‘ ( ( 𝐹 ‘ 𝑏 ) − 𝑅 ) ) < 𝑦 ) ) → ( abs ‘ ( 𝑅 − 𝐿 ) ) < ( 4 · 𝑦 ) )
229 228 ex ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ ℂ ) ∧ 𝑦 ∈ ℝ+ ) ∧ 𝑎 ∈ 𝐴 ) ∧ ( ( abs ‘ ( ( 𝐹 ‘ 𝑎 ) − 𝑥 ) ) < 𝑦 ∧ ( abs ‘ ( ( 𝐹 ‘ 𝑎 ) − 𝐿 ) ) < 𝑦 ) ) ∧ 𝑏 ∈ 𝐴 ) → ( ( ( abs ‘ ( ( 𝐹 ‘ 𝑏 ) − 𝑥 ) ) < 𝑦 ∧ ( abs ‘ ( ( 𝐹 ‘ 𝑏 ) − 𝑅 ) ) < 𝑦 ) → ( abs ‘ ( 𝑅 − 𝐿 ) ) < ( 4 · 𝑦 ) ) )
230 229 adantl3r ⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ ℂ ) ∧ 𝑦 ∈ ℝ+ ) ∧ ∃ 𝑧 ∈ ℝ+ ∀ 𝑤 ∈ 𝐴 ( ( 𝑤 ≠ 𝐵 ∧ ( abs ‘ ( 𝑤 − 𝐵 ) ) < 𝑧 ) → ( abs ‘ ( ( 𝐹 ‘ 𝑤 ) − 𝑥 ) ) < 𝑦 ) ) ∧ 𝑎 ∈ 𝐴 ) ∧ ( ( abs ‘ ( ( 𝐹 ‘ 𝑎 ) − 𝑥 ) ) < 𝑦 ∧ ( abs ‘ ( ( 𝐹 ‘ 𝑎 ) − 𝐿 ) ) < 𝑦 ) ) ∧ 𝑏 ∈ 𝐴 ) → ( ( ( abs ‘ ( ( 𝐹 ‘ 𝑏 ) − 𝑥 ) ) < 𝑦 ∧ ( abs ‘ ( ( 𝐹 ‘ 𝑏 ) − 𝑅 ) ) < 𝑦 ) → ( abs ‘ ( 𝑅 − 𝐿 ) ) < ( 4 · 𝑦 ) ) )
231 230 reximdva ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ ℂ ) ∧ 𝑦 ∈ ℝ+ ) ∧ ∃ 𝑧 ∈ ℝ+ ∀ 𝑤 ∈ 𝐴 ( ( 𝑤 ≠ 𝐵 ∧ ( abs ‘ ( 𝑤 − 𝐵 ) ) < 𝑧 ) → ( abs ‘ ( ( 𝐹 ‘ 𝑤 ) − 𝑥 ) ) < 𝑦 ) ) ∧ 𝑎 ∈ 𝐴 ) ∧ ( ( abs ‘ ( ( 𝐹 ‘ 𝑎 ) − 𝑥 ) ) < 𝑦 ∧ ( abs ‘ ( ( 𝐹 ‘ 𝑎 ) − 𝐿 ) ) < 𝑦 ) ) → ( ∃ 𝑏 ∈ 𝐴 ( ( abs ‘ ( ( 𝐹 ‘ 𝑏 ) − 𝑥 ) ) < 𝑦 ∧ ( abs ‘ ( ( 𝐹 ‘ 𝑏 ) − 𝑅 ) ) < 𝑦 ) → ∃ 𝑏 ∈ 𝐴 ( abs ‘ ( 𝑅 − 𝐿 ) ) < ( 4 · 𝑦 ) ) )
232 185 231 mpd ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ ℂ ) ∧ 𝑦 ∈ ℝ+ ) ∧ ∃ 𝑧 ∈ ℝ+ ∀ 𝑤 ∈ 𝐴 ( ( 𝑤 ≠ 𝐵 ∧ ( abs ‘ ( 𝑤 − 𝐵 ) ) < 𝑧 ) → ( abs ‘ ( ( 𝐹 ‘ 𝑤 ) − 𝑥 ) ) < 𝑦 ) ) ∧ 𝑎 ∈ 𝐴 ) ∧ ( ( abs ‘ ( ( 𝐹 ‘ 𝑎 ) − 𝑥 ) ) < 𝑦 ∧ ( abs ‘ ( ( 𝐹 ‘ 𝑎 ) − 𝐿 ) ) < 𝑦 ) ) → ∃ 𝑏 ∈ 𝐴 ( abs ‘ ( 𝑅 − 𝐿 ) ) < ( 4 · 𝑦 ) )
233 fresin ⊢ ( 𝐹 : 𝐴 ⟶ ℂ → ( 𝐹 ↾ ( -∞ (,) 𝐵 ) ) : ( 𝐴 ∩ ( -∞ (,) 𝐵 ) ) ⟶ ℂ )
234 4 233 syl ⊢ ( 𝜑 → ( 𝐹 ↾ ( -∞ (,) 𝐵 ) ) : ( 𝐴 ∩ ( -∞ (,) 𝐵 ) ) ⟶ ℂ )
235 ioosscn ⊢ ( -∞ (,) 𝐵 ) ⊆ ℂ
236 50 235 sstri ⊢ ( 𝐴 ∩ ( -∞ (,) 𝐵 ) ) ⊆ ℂ
237 236 a1i ⊢ ( 𝜑 → ( 𝐴 ∩ ( -∞ (,) 𝐵 ) ) ⊆ ℂ )
238 234 237 59 ellimc3 ⊢ ( 𝜑 → ( 𝐿 ∈ ( ( 𝐹 ↾ ( -∞ (,) 𝐵 ) ) limℂ 𝐵 ) ↔ ( 𝐿 ∈ ℂ ∧ ∀ 𝑦 ∈ ℝ+ ∃ 𝑣 ∈ ℝ+ ∀ 𝑤 ∈ ( 𝐴 ∩ ( -∞ (,) 𝐵 ) ) ( ( 𝑤 ≠ 𝐵 ∧ ( abs ‘ ( 𝑤 − 𝐵 ) ) < 𝑣 ) → ( abs ‘ ( ( ( 𝐹 ↾ ( -∞ (,) 𝐵 ) ) ‘ 𝑤 ) − 𝐿 ) ) < 𝑦 ) ) ) )
239 7 238 mpbid ⊢ ( 𝜑 → ( 𝐿 ∈ ℂ ∧ ∀ 𝑦 ∈ ℝ+ ∃ 𝑣 ∈ ℝ+ ∀ 𝑤 ∈ ( 𝐴 ∩ ( -∞ (,) 𝐵 ) ) ( ( 𝑤 ≠ 𝐵 ∧ ( abs ‘ ( 𝑤 − 𝐵 ) ) < 𝑣 ) → ( abs ‘ ( ( ( 𝐹 ↾ ( -∞ (,) 𝐵 ) ) ‘ 𝑤 ) − 𝐿 ) ) < 𝑦 ) ) )
240 239 simprd ⊢ ( 𝜑 → ∀ 𝑦 ∈ ℝ+ ∃ 𝑣 ∈ ℝ+ ∀ 𝑤 ∈ ( 𝐴 ∩ ( -∞ (,) 𝐵 ) ) ( ( 𝑤 ≠ 𝐵 ∧ ( abs ‘ ( 𝑤 − 𝐵 ) ) < 𝑣 ) → ( abs ‘ ( ( ( 𝐹 ↾ ( -∞ (,) 𝐵 ) ) ‘ 𝑤 ) − 𝐿 ) ) < 𝑦 ) )
241 240 r19.21bi ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ℝ+ ) → ∃ 𝑣 ∈ ℝ+ ∀ 𝑤 ∈ ( 𝐴 ∩ ( -∞ (,) 𝐵 ) ) ( ( 𝑤 ≠ 𝐵 ∧ ( abs ‘ ( 𝑤 − 𝐵 ) ) < 𝑣 ) → ( abs ‘ ( ( ( 𝐹 ↾ ( -∞ (,) 𝐵 ) ) ‘ 𝑤 ) − 𝐿 ) ) < 𝑦 ) )
242 241 3ad2ant1 ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ+ ) ∧ 𝑧 ∈ ℝ+ ∧ ∀ 𝑤 ∈ 𝐴 ( ( 𝑤 ≠ 𝐵 ∧ ( abs ‘ ( 𝑤 − 𝐵 ) ) < 𝑧 ) → ( abs ‘ ( ( 𝐹 ‘ 𝑤 ) − 𝑥 ) ) < 𝑦 ) ) → ∃ 𝑣 ∈ ℝ+ ∀ 𝑤 ∈ ( 𝐴 ∩ ( -∞ (,) 𝐵 ) ) ( ( 𝑤 ≠ 𝐵 ∧ ( abs ‘ ( 𝑤 − 𝐵 ) ) < 𝑣 ) → ( abs ‘ ( ( ( 𝐹 ↾ ( -∞ (,) 𝐵 ) ) ‘ 𝑤 ) − 𝐿 ) ) < 𝑦 ) )
243 simp11l ⊢ ( ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ+ ) ∧ 𝑧 ∈ ℝ+ ∧ ∀ 𝑤 ∈ 𝐴 ( ( 𝑤 ≠ 𝐵 ∧ ( abs ‘ ( 𝑤 − 𝐵 ) ) < 𝑧 ) → ( abs ‘ ( ( 𝐹 ‘ 𝑤 ) − 𝑥 ) ) < 𝑦 ) ) ∧ 𝑣 ∈ ℝ+ ∧ ∀ 𝑤 ∈ ( 𝐴 ∩ ( -∞ (,) 𝐵 ) ) ( ( 𝑤 ≠ 𝐵 ∧ ( abs ‘ ( 𝑤 − 𝐵 ) ) < 𝑣 ) → ( abs ‘ ( ( ( 𝐹 ↾ ( -∞ (,) 𝐵 ) ) ‘ 𝑤 ) − 𝐿 ) ) < 𝑦 ) ) → 𝜑 )
244 simp12 ⊢ ( ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ+ ) ∧ 𝑧 ∈ ℝ+ ∧ ∀ 𝑤 ∈ 𝐴 ( ( 𝑤 ≠ 𝐵 ∧ ( abs ‘ ( 𝑤 − 𝐵 ) ) < 𝑧 ) → ( abs ‘ ( ( 𝐹 ‘ 𝑤 ) − 𝑥 ) ) < 𝑦 ) ) ∧ 𝑣 ∈ ℝ+ ∧ ∀ 𝑤 ∈ ( 𝐴 ∩ ( -∞ (,) 𝐵 ) ) ( ( 𝑤 ≠ 𝐵 ∧ ( abs ‘ ( 𝑤 − 𝐵 ) ) < 𝑣 ) → ( abs ‘ ( ( ( 𝐹 ↾ ( -∞ (,) 𝐵 ) ) ‘ 𝑤 ) − 𝐿 ) ) < 𝑦 ) ) → 𝑧 ∈ ℝ+ )
245 simp2 ⊢ ( ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ+ ) ∧ 𝑧 ∈ ℝ+ ∧ ∀ 𝑤 ∈ 𝐴 ( ( 𝑤 ≠ 𝐵 ∧ ( abs ‘ ( 𝑤 − 𝐵 ) ) < 𝑧 ) → ( abs ‘ ( ( 𝐹 ‘ 𝑤 ) − 𝑥 ) ) < 𝑦 ) ) ∧ 𝑣 ∈ ℝ+ ∧ ∀ 𝑤 ∈ ( 𝐴 ∩ ( -∞ (,) 𝐵 ) ) ( ( 𝑤 ≠ 𝐵 ∧ ( abs ‘ ( 𝑤 − 𝐵 ) ) < 𝑣 ) → ( abs ‘ ( ( ( 𝐹 ↾ ( -∞ (,) 𝐵 ) ) ‘ 𝑤 ) − 𝐿 ) ) < 𝑦 ) ) → 𝑣 ∈ ℝ+ )
246 breq2 ⊢ ( 𝑢 = if ( 𝑧 ≤ 𝑣 , 𝑧 , 𝑣 ) → ( ( abs ‘ ( 𝑎 − 𝐵 ) ) < 𝑢 ↔ ( abs ‘ ( 𝑎 − 𝐵 ) ) < if ( 𝑧 ≤ 𝑣 , 𝑧 , 𝑣 ) ) )
247 246 rexbidv ⊢ ( 𝑢 = if ( 𝑧 ≤ 𝑣 , 𝑧 , 𝑣 ) → ( ∃ 𝑎 ∈ ( ( 𝐴 ∩ ( -∞ (,) 𝐵 ) ) ∖ { 𝐵 } ) ( abs ‘ ( 𝑎 − 𝐵 ) ) < 𝑢 ↔ ∃ 𝑎 ∈ ( ( 𝐴 ∩ ( -∞ (,) 𝐵 ) ) ∖ { 𝐵 } ) ( abs ‘ ( 𝑎 − 𝐵 ) ) < if ( 𝑧 ≤ 𝑣 , 𝑧 , 𝑣 ) ) )
248 inss1 ⊢ ( ( ( limPt ‘ 𝐾 ) ‘ ( 𝐴 ∩ ( -∞ (,) 𝐵 ) ) ) ∩ ℝ ) ⊆ ( ( limPt ‘ 𝐾 ) ‘ ( 𝐴 ∩ ( -∞ (,) 𝐵 ) ) )
249 248 a1i ⊢ ( 𝜑 → ( ( ( limPt ‘ 𝐾 ) ‘ ( 𝐴 ∩ ( -∞ (,) 𝐵 ) ) ) ∩ ℝ ) ⊆ ( ( limPt ‘ 𝐾 ) ‘ ( 𝐴 ∩ ( -∞ (,) 𝐵 ) ) ) )
250 52 a1i ⊢ ( 𝜑 → ( 𝐴 ∩ ( -∞ (,) 𝐵 ) ) ⊆ ℝ )
251 81 83 restlp ⊢ ( ( 𝐾 ∈ Top ∧ ℝ ⊆ ℂ ∧ ( 𝐴 ∩ ( -∞ (,) 𝐵 ) ) ⊆ ℝ ) → ( ( limPt ‘ 𝐽 ) ‘ ( 𝐴 ∩ ( -∞ (,) 𝐵 ) ) ) = ( ( ( limPt ‘ 𝐾 ) ‘ ( 𝐴 ∩ ( -∞ (,) 𝐵 ) ) ) ∩ ℝ ) )
252 73 75 250 251 syl3anc ⊢ ( 𝜑 → ( ( limPt ‘ 𝐽 ) ‘ ( 𝐴 ∩ ( -∞ (,) 𝐵 ) ) ) = ( ( ( limPt ‘ 𝐾 ) ‘ ( 𝐴 ∩ ( -∞ (,) 𝐵 ) ) ) ∩ ℝ ) )
253 87 fveq1i ⊢ ( ( limPt ‘ ( TopOpen ‘ ℂfld ) ) ‘ ( 𝐴 ∩ ( -∞ (,) 𝐵 ) ) ) = ( ( limPt ‘ 𝐾 ) ‘ ( 𝐴 ∩ ( -∞ (,) 𝐵 ) ) )
254 253 a1i ⊢ ( 𝜑 → ( ( limPt ‘ ( TopOpen ‘ ℂfld ) ) ‘ ( 𝐴 ∩ ( -∞ (,) 𝐵 ) ) ) = ( ( limPt ‘ 𝐾 ) ‘ ( 𝐴 ∩ ( -∞ (,) 𝐵 ) ) ) )
255 249 252 254 3sstr4d ⊢ ( 𝜑 → ( ( limPt ‘ 𝐽 ) ‘ ( 𝐴 ∩ ( -∞ (,) 𝐵 ) ) ) ⊆ ( ( limPt ‘ ( TopOpen ‘ ℂfld ) ) ‘ ( 𝐴 ∩ ( -∞ (,) 𝐵 ) ) ) )
256 255 5 sseldd ⊢ ( 𝜑 → 𝐵 ∈ ( ( limPt ‘ ( TopOpen ‘ ℂfld ) ) ‘ ( 𝐴 ∩ ( -∞ (,) 𝐵 ) ) ) )
257 237 59 islpcn ⊢ ( 𝜑 → ( 𝐵 ∈ ( ( limPt ‘ ( TopOpen ‘ ℂfld ) ) ‘ ( 𝐴 ∩ ( -∞ (,) 𝐵 ) ) ) ↔ ∀ 𝑢 ∈ ℝ+ ∃ 𝑎 ∈ ( ( 𝐴 ∩ ( -∞ (,) 𝐵 ) ) ∖ { 𝐵 } ) ( abs ‘ ( 𝑎 − 𝐵 ) ) < 𝑢 ) )
258 256 257 mpbid ⊢ ( 𝜑 → ∀ 𝑢 ∈ ℝ+ ∃ 𝑎 ∈ ( ( 𝐴 ∩ ( -∞ (,) 𝐵 ) ) ∖ { 𝐵 } ) ( abs ‘ ( 𝑎 − 𝐵 ) ) < 𝑢 )
259 258 3ad2ant1 ⊢ ( ( 𝜑 ∧ 𝑧 ∈ ℝ+ ∧ 𝑣 ∈ ℝ+ ) → ∀ 𝑢 ∈ ℝ+ ∃ 𝑎 ∈ ( ( 𝐴 ∩ ( -∞ (,) 𝐵 ) ) ∖ { 𝐵 } ) ( abs ‘ ( 𝑎 − 𝐵 ) ) < 𝑢 )
260 247 259 96 rspcdva ⊢ ( ( 𝜑 ∧ 𝑧 ∈ ℝ+ ∧ 𝑣 ∈ ℝ+ ) → ∃ 𝑎 ∈ ( ( 𝐴 ∩ ( -∞ (,) 𝐵 ) ) ∖ { 𝐵 } ) ( abs ‘ ( 𝑎 − 𝐵 ) ) < if ( 𝑧 ≤ 𝑣 , 𝑧 , 𝑣 ) )
261 eldifi ⊢ ( 𝑎 ∈ ( ( 𝐴 ∩ ( -∞ (,) 𝐵 ) ) ∖ { 𝐵 } ) → 𝑎 ∈ ( 𝐴 ∩ ( -∞ (,) 𝐵 ) ) )
262 52 261 sselid ⊢ ( 𝑎 ∈ ( ( 𝐴 ∩ ( -∞ (,) 𝐵 ) ) ∖ { 𝐵 } ) → 𝑎 ∈ ℝ )
263 75 sselda ⊢ ( ( 𝜑 ∧ 𝑎 ∈ ℝ ) → 𝑎 ∈ ℂ )
264 59 adantr ⊢ ( ( 𝜑 ∧ 𝑎 ∈ ℝ ) → 𝐵 ∈ ℂ )
265 263 264 subcld ⊢ ( ( 𝜑 ∧ 𝑎 ∈ ℝ ) → ( 𝑎 − 𝐵 ) ∈ ℂ )
266 265 abscld ⊢ ( ( 𝜑 ∧ 𝑎 ∈ ℝ ) → ( abs ‘ ( 𝑎 − 𝐵 ) ) ∈ ℝ )
267 266 3ad2antl1 ⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ ℝ+ ∧ 𝑣 ∈ ℝ+ ) ∧ 𝑎 ∈ ℝ ) → ( abs ‘ ( 𝑎 − 𝐵 ) ) ∈ ℝ )
268 267 adantr ⊢ ( ( ( ( 𝜑 ∧ 𝑧 ∈ ℝ+ ∧ 𝑣 ∈ ℝ+ ) ∧ 𝑎 ∈ ℝ ) ∧ ( abs ‘ ( 𝑎 − 𝐵 ) ) < if ( 𝑧 ≤ 𝑣 , 𝑧 , 𝑣 ) ) → ( abs ‘ ( 𝑎 − 𝐵 ) ) ∈ ℝ )
269 106 ad2antrr ⊢ ( ( ( ( 𝜑 ∧ 𝑧 ∈ ℝ+ ∧ 𝑣 ∈ ℝ+ ) ∧ 𝑎 ∈ ℝ ) ∧ ( abs ‘ ( 𝑎 − 𝐵 ) ) < if ( 𝑧 ≤ 𝑣 , 𝑧 , 𝑣 ) ) → if ( 𝑧 ≤ 𝑣 , 𝑧 , 𝑣 ) ∈ ℝ )
270 109 ad2antrr ⊢ ( ( ( ( 𝜑 ∧ 𝑧 ∈ ℝ+ ∧ 𝑣 ∈ ℝ+ ) ∧ 𝑎 ∈ ℝ ) ∧ ( abs ‘ ( 𝑎 − 𝐵 ) ) < if ( 𝑧 ≤ 𝑣 , 𝑧 , 𝑣 ) ) → 𝑧 ∈ ℝ )
271 simpr ⊢ ( ( ( ( 𝜑 ∧ 𝑧 ∈ ℝ+ ∧ 𝑣 ∈ ℝ+ ) ∧ 𝑎 ∈ ℝ ) ∧ ( abs ‘ ( 𝑎 − 𝐵 ) ) < if ( 𝑧 ≤ 𝑣 , 𝑧 , 𝑣 ) ) → ( abs ‘ ( 𝑎 − 𝐵 ) ) < if ( 𝑧 ≤ 𝑣 , 𝑧 , 𝑣 ) )
272 115 ad2antrr ⊢ ( ( ( ( 𝜑 ∧ 𝑧 ∈ ℝ+ ∧ 𝑣 ∈ ℝ+ ) ∧ 𝑎 ∈ ℝ ) ∧ ( abs ‘ ( 𝑎 − 𝐵 ) ) < if ( 𝑧 ≤ 𝑣 , 𝑧 , 𝑣 ) ) → if ( 𝑧 ≤ 𝑣 , 𝑧 , 𝑣 ) ≤ 𝑧 )
273 268 269 270 271 272 ltletrd ⊢ ( ( ( ( 𝜑 ∧ 𝑧 ∈ ℝ+ ∧ 𝑣 ∈ ℝ+ ) ∧ 𝑎 ∈ ℝ ) ∧ ( abs ‘ ( 𝑎 − 𝐵 ) ) < if ( 𝑧 ≤ 𝑣 , 𝑧 , 𝑣 ) ) → ( abs ‘ ( 𝑎 − 𝐵 ) ) < 𝑧 )
274 118 ad2antrr ⊢ ( ( ( ( 𝜑 ∧ 𝑧 ∈ ℝ+ ∧ 𝑣 ∈ ℝ+ ) ∧ 𝑎 ∈ ℝ ) ∧ ( abs ‘ ( 𝑎 − 𝐵 ) ) < if ( 𝑧 ≤ 𝑣 , 𝑧 , 𝑣 ) ) → 𝑣 ∈ ℝ )
275 min2 ⊢ ( ( 𝑧 ∈ ℝ ∧ 𝑣 ∈ ℝ ) → if ( 𝑧 ≤ 𝑣 , 𝑧 , 𝑣 ) ≤ 𝑣 )
276 108 112 275 syl2an ⊢ ( ( 𝑧 ∈ ℝ+ ∧ 𝑣 ∈ ℝ+ ) → if ( 𝑧 ≤ 𝑣 , 𝑧 , 𝑣 ) ≤ 𝑣 )
277 276 3adant1 ⊢ ( ( 𝜑 ∧ 𝑧 ∈ ℝ+ ∧ 𝑣 ∈ ℝ+ ) → if ( 𝑧 ≤ 𝑣 , 𝑧 , 𝑣 ) ≤ 𝑣 )
278 277 ad2antrr ⊢ ( ( ( ( 𝜑 ∧ 𝑧 ∈ ℝ+ ∧ 𝑣 ∈ ℝ+ ) ∧ 𝑎 ∈ ℝ ) ∧ ( abs ‘ ( 𝑎 − 𝐵 ) ) < if ( 𝑧 ≤ 𝑣 , 𝑧 , 𝑣 ) ) → if ( 𝑧 ≤ 𝑣 , 𝑧 , 𝑣 ) ≤ 𝑣 )
279 268 269 274 271 278 ltletrd ⊢ ( ( ( ( 𝜑 ∧ 𝑧 ∈ ℝ+ ∧ 𝑣 ∈ ℝ+ ) ∧ 𝑎 ∈ ℝ ) ∧ ( abs ‘ ( 𝑎 − 𝐵 ) ) < if ( 𝑧 ≤ 𝑣 , 𝑧 , 𝑣 ) ) → ( abs ‘ ( 𝑎 − 𝐵 ) ) < 𝑣 )
280 273 279 jca ⊢ ( ( ( ( 𝜑 ∧ 𝑧 ∈ ℝ+ ∧ 𝑣 ∈ ℝ+ ) ∧ 𝑎 ∈ ℝ ) ∧ ( abs ‘ ( 𝑎 − 𝐵 ) ) < if ( 𝑧 ≤ 𝑣 , 𝑧 , 𝑣 ) ) → ( ( abs ‘ ( 𝑎 − 𝐵 ) ) < 𝑧 ∧ ( abs ‘ ( 𝑎 − 𝐵 ) ) < 𝑣 ) )
281 280 ex ⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ ℝ+ ∧ 𝑣 ∈ ℝ+ ) ∧ 𝑎 ∈ ℝ ) → ( ( abs ‘ ( 𝑎 − 𝐵 ) ) < if ( 𝑧 ≤ 𝑣 , 𝑧 , 𝑣 ) → ( ( abs ‘ ( 𝑎 − 𝐵 ) ) < 𝑧 ∧ ( abs ‘ ( 𝑎 − 𝐵 ) ) < 𝑣 ) ) )
282 262 281 sylan2 ⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ ℝ+ ∧ 𝑣 ∈ ℝ+ ) ∧ 𝑎 ∈ ( ( 𝐴 ∩ ( -∞ (,) 𝐵 ) ) ∖ { 𝐵 } ) ) → ( ( abs ‘ ( 𝑎 − 𝐵 ) ) < if ( 𝑧 ≤ 𝑣 , 𝑧 , 𝑣 ) → ( ( abs ‘ ( 𝑎 − 𝐵 ) ) < 𝑧 ∧ ( abs ‘ ( 𝑎 − 𝐵 ) ) < 𝑣 ) ) )
283 282 reximdva ⊢ ( ( 𝜑 ∧ 𝑧 ∈ ℝ+ ∧ 𝑣 ∈ ℝ+ ) → ( ∃ 𝑎 ∈ ( ( 𝐴 ∩ ( -∞ (,) 𝐵 ) ) ∖ { 𝐵 } ) ( abs ‘ ( 𝑎 − 𝐵 ) ) < if ( 𝑧 ≤ 𝑣 , 𝑧 , 𝑣 ) → ∃ 𝑎 ∈ ( ( 𝐴 ∩ ( -∞ (,) 𝐵 ) ) ∖ { 𝐵 } ) ( ( abs ‘ ( 𝑎 − 𝐵 ) ) < 𝑧 ∧ ( abs ‘ ( 𝑎 − 𝐵 ) ) < 𝑣 ) ) )
284 260 283 mpd ⊢ ( ( 𝜑 ∧ 𝑧 ∈ ℝ+ ∧ 𝑣 ∈ ℝ+ ) → ∃ 𝑎 ∈ ( ( 𝐴 ∩ ( -∞ (,) 𝐵 ) ) ∖ { 𝐵 } ) ( ( abs ‘ ( 𝑎 − 𝐵 ) ) < 𝑧 ∧ ( abs ‘ ( 𝑎 − 𝐵 ) ) < 𝑣 ) )
285 243 244 245 284 syl3anc ⊢ ( ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ+ ) ∧ 𝑧 ∈ ℝ+ ∧ ∀ 𝑤 ∈ 𝐴 ( ( 𝑤 ≠ 𝐵 ∧ ( abs ‘ ( 𝑤 − 𝐵 ) ) < 𝑧 ) → ( abs ‘ ( ( 𝐹 ‘ 𝑤 ) − 𝑥 ) ) < 𝑦 ) ) ∧ 𝑣 ∈ ℝ+ ∧ ∀ 𝑤 ∈ ( 𝐴 ∩ ( -∞ (,) 𝐵 ) ) ( ( 𝑤 ≠ 𝐵 ∧ ( abs ‘ ( 𝑤 − 𝐵 ) ) < 𝑣 ) → ( abs ‘ ( ( ( 𝐹 ↾ ( -∞ (,) 𝐵 ) ) ‘ 𝑤 ) − 𝐿 ) ) < 𝑦 ) ) → ∃ 𝑎 ∈ ( ( 𝐴 ∩ ( -∞ (,) 𝐵 ) ) ∖ { 𝐵 } ) ( ( abs ‘ ( 𝑎 − 𝐵 ) ) < 𝑧 ∧ ( abs ‘ ( 𝑎 − 𝐵 ) ) < 𝑣 ) )
286 nfv ⊢ Ⅎ 𝑎 ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ+ ) ∧ 𝑧 ∈ ℝ+ ∧ ∀ 𝑤 ∈ 𝐴 ( ( 𝑤 ≠ 𝐵 ∧ ( abs ‘ ( 𝑤 − 𝐵 ) ) < 𝑧 ) → ( abs ‘ ( ( 𝐹 ‘ 𝑤 ) − 𝑥 ) ) < 𝑦 ) ) ∧ 𝑣 ∈ ℝ+ ∧ ∀ 𝑤 ∈ ( 𝐴 ∩ ( -∞ (,) 𝐵 ) ) ( ( 𝑤 ≠ 𝐵 ∧ ( abs ‘ ( 𝑤 − 𝐵 ) ) < 𝑣 ) → ( abs ‘ ( ( ( 𝐹 ↾ ( -∞ (,) 𝐵 ) ) ‘ 𝑤 ) − 𝐿 ) ) < 𝑦 ) )
287 nfre1 ⊢ Ⅎ 𝑎 ∃ 𝑎 ∈ 𝐴 ( ( abs ‘ ( ( 𝐹 ‘ 𝑎 ) − 𝑥 ) ) < 𝑦 ∧ ( abs ‘ ( ( 𝐹 ‘ 𝑎 ) − 𝐿 ) ) < 𝑦 )
288 261 elin1d ⊢ ( 𝑎 ∈ ( ( 𝐴 ∩ ( -∞ (,) 𝐵 ) ) ∖ { 𝐵 } ) → 𝑎 ∈ 𝐴 )
289 288 3ad2ant2 ⊢ ( ( ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ+ ) ∧ 𝑧 ∈ ℝ+ ∧ ∀ 𝑤 ∈ 𝐴 ( ( 𝑤 ≠ 𝐵 ∧ ( abs ‘ ( 𝑤 − 𝐵 ) ) < 𝑧 ) → ( abs ‘ ( ( 𝐹 ‘ 𝑤 ) − 𝑥 ) ) < 𝑦 ) ) ∧ 𝑣 ∈ ℝ+ ∧ ∀ 𝑤 ∈ ( 𝐴 ∩ ( -∞ (,) 𝐵 ) ) ( ( 𝑤 ≠ 𝐵 ∧ ( abs ‘ ( 𝑤 − 𝐵 ) ) < 𝑣 ) → ( abs ‘ ( ( ( 𝐹 ↾ ( -∞ (,) 𝐵 ) ) ‘ 𝑤 ) − 𝐿 ) ) < 𝑦 ) ) ∧ 𝑎 ∈ ( ( 𝐴 ∩ ( -∞ (,) 𝐵 ) ) ∖ { 𝐵 } ) ∧ ( ( abs ‘ ( 𝑎 − 𝐵 ) ) < 𝑧 ∧ ( abs ‘ ( 𝑎 − 𝐵 ) ) < 𝑣 ) ) → 𝑎 ∈ 𝐴 )
290 simp113 ⊢ ( ( ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ+ ) ∧ 𝑧 ∈ ℝ+ ∧ ∀ 𝑤 ∈ 𝐴 ( ( 𝑤 ≠ 𝐵 ∧ ( abs ‘ ( 𝑤 − 𝐵 ) ) < 𝑧 ) → ( abs ‘ ( ( 𝐹 ‘ 𝑤 ) − 𝑥 ) ) < 𝑦 ) ) ∧ 𝑣 ∈ ℝ+ ∧ ∀ 𝑤 ∈ ( 𝐴 ∩ ( -∞ (,) 𝐵 ) ) ( ( 𝑤 ≠ 𝐵 ∧ ( abs ‘ ( 𝑤 − 𝐵 ) ) < 𝑣 ) → ( abs ‘ ( ( ( 𝐹 ↾ ( -∞ (,) 𝐵 ) ) ‘ 𝑤 ) − 𝐿 ) ) < 𝑦 ) ) ∧ 𝑎 ∈ ( ( 𝐴 ∩ ( -∞ (,) 𝐵 ) ) ∖ { 𝐵 } ) ∧ ( ( abs ‘ ( 𝑎 − 𝐵 ) ) < 𝑧 ∧ ( abs ‘ ( 𝑎 − 𝐵 ) ) < 𝑣 ) ) → ∀ 𝑤 ∈ 𝐴 ( ( 𝑤 ≠ 𝐵 ∧ ( abs ‘ ( 𝑤 − 𝐵 ) ) < 𝑧 ) → ( abs ‘ ( ( 𝐹 ‘ 𝑤 ) − 𝑥 ) ) < 𝑦 ) )
291 eldifsni ⊢ ( 𝑎 ∈ ( ( 𝐴 ∩ ( -∞ (,) 𝐵 ) ) ∖ { 𝐵 } ) → 𝑎 ≠ 𝐵 )
292 291 adantr ⊢ ( ( 𝑎 ∈ ( ( 𝐴 ∩ ( -∞ (,) 𝐵 ) ) ∖ { 𝐵 } ) ∧ ( ( abs ‘ ( 𝑎 − 𝐵 ) ) < 𝑧 ∧ ( abs ‘ ( 𝑎 − 𝐵 ) ) < 𝑣 ) ) → 𝑎 ≠ 𝐵 )
293 simprl ⊢ ( ( 𝑎 ∈ ( ( 𝐴 ∩ ( -∞ (,) 𝐵 ) ) ∖ { 𝐵 } ) ∧ ( ( abs ‘ ( 𝑎 − 𝐵 ) ) < 𝑧 ∧ ( abs ‘ ( 𝑎 − 𝐵 ) ) < 𝑣 ) ) → ( abs ‘ ( 𝑎 − 𝐵 ) ) < 𝑧 )
294 292 293 jca ⊢ ( ( 𝑎 ∈ ( ( 𝐴 ∩ ( -∞ (,) 𝐵 ) ) ∖ { 𝐵 } ) ∧ ( ( abs ‘ ( 𝑎 − 𝐵 ) ) < 𝑧 ∧ ( abs ‘ ( 𝑎 − 𝐵 ) ) < 𝑣 ) ) → ( 𝑎 ≠ 𝐵 ∧ ( abs ‘ ( 𝑎 − 𝐵 ) ) < 𝑧 ) )
295 294 3adant1 ⊢ ( ( ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ+ ) ∧ 𝑧 ∈ ℝ+ ∧ ∀ 𝑤 ∈ 𝐴 ( ( 𝑤 ≠ 𝐵 ∧ ( abs ‘ ( 𝑤 − 𝐵 ) ) < 𝑧 ) → ( abs ‘ ( ( 𝐹 ‘ 𝑤 ) − 𝑥 ) ) < 𝑦 ) ) ∧ 𝑣 ∈ ℝ+ ∧ ∀ 𝑤 ∈ ( 𝐴 ∩ ( -∞ (,) 𝐵 ) ) ( ( 𝑤 ≠ 𝐵 ∧ ( abs ‘ ( 𝑤 − 𝐵 ) ) < 𝑣 ) → ( abs ‘ ( ( ( 𝐹 ↾ ( -∞ (,) 𝐵 ) ) ‘ 𝑤 ) − 𝐿 ) ) < 𝑦 ) ) ∧ 𝑎 ∈ ( ( 𝐴 ∩ ( -∞ (,) 𝐵 ) ) ∖ { 𝐵 } ) ∧ ( ( abs ‘ ( 𝑎 − 𝐵 ) ) < 𝑧 ∧ ( abs ‘ ( 𝑎 − 𝐵 ) ) < 𝑣 ) ) → ( 𝑎 ≠ 𝐵 ∧ ( abs ‘ ( 𝑎 − 𝐵 ) ) < 𝑧 ) )
296 neeq1 ⊢ ( 𝑤 = 𝑎 → ( 𝑤 ≠ 𝐵 ↔ 𝑎 ≠ 𝐵 ) )
297 fvoveq1 ⊢ ( 𝑤 = 𝑎 → ( abs ‘ ( 𝑤 − 𝐵 ) ) = ( abs ‘ ( 𝑎 − 𝐵 ) ) )
298 297 breq1d ⊢ ( 𝑤 = 𝑎 → ( ( abs ‘ ( 𝑤 − 𝐵 ) ) < 𝑧 ↔ ( abs ‘ ( 𝑎 − 𝐵 ) ) < 𝑧 ) )
299 296 298 anbi12d ⊢ ( 𝑤 = 𝑎 → ( ( 𝑤 ≠ 𝐵 ∧ ( abs ‘ ( 𝑤 − 𝐵 ) ) < 𝑧 ) ↔ ( 𝑎 ≠ 𝐵 ∧ ( abs ‘ ( 𝑎 − 𝐵 ) ) < 𝑧 ) ) )
300 299 imbrov2fvoveq ⊢ ( 𝑤 = 𝑎 → ( ( ( 𝑤 ≠ 𝐵 ∧ ( abs ‘ ( 𝑤 − 𝐵 ) ) < 𝑧 ) → ( abs ‘ ( ( 𝐹 ‘ 𝑤 ) − 𝑥 ) ) < 𝑦 ) ↔ ( ( 𝑎 ≠ 𝐵 ∧ ( abs ‘ ( 𝑎 − 𝐵 ) ) < 𝑧 ) → ( abs ‘ ( ( 𝐹 ‘ 𝑎 ) − 𝑥 ) ) < 𝑦 ) ) )
301 300 rspcva ⊢ ( ( 𝑎 ∈ 𝐴 ∧ ∀ 𝑤 ∈ 𝐴 ( ( 𝑤 ≠ 𝐵 ∧ ( abs ‘ ( 𝑤 − 𝐵 ) ) < 𝑧 ) → ( abs ‘ ( ( 𝐹 ‘ 𝑤 ) − 𝑥 ) ) < 𝑦 ) ) → ( ( 𝑎 ≠ 𝐵 ∧ ( abs ‘ ( 𝑎 − 𝐵 ) ) < 𝑧 ) → ( abs ‘ ( ( 𝐹 ‘ 𝑎 ) − 𝑥 ) ) < 𝑦 ) )
302 301 imp ⊢ ( ( ( 𝑎 ∈ 𝐴 ∧ ∀ 𝑤 ∈ 𝐴 ( ( 𝑤 ≠ 𝐵 ∧ ( abs ‘ ( 𝑤 − 𝐵 ) ) < 𝑧 ) → ( abs ‘ ( ( 𝐹 ‘ 𝑤 ) − 𝑥 ) ) < 𝑦 ) ) ∧ ( 𝑎 ≠ 𝐵 ∧ ( abs ‘ ( 𝑎 − 𝐵 ) ) < 𝑧 ) ) → ( abs ‘ ( ( 𝐹 ‘ 𝑎 ) − 𝑥 ) ) < 𝑦 )
303 289 290 295 302 syl21anc ⊢ ( ( ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ+ ) ∧ 𝑧 ∈ ℝ+ ∧ ∀ 𝑤 ∈ 𝐴 ( ( 𝑤 ≠ 𝐵 ∧ ( abs ‘ ( 𝑤 − 𝐵 ) ) < 𝑧 ) → ( abs ‘ ( ( 𝐹 ‘ 𝑤 ) − 𝑥 ) ) < 𝑦 ) ) ∧ 𝑣 ∈ ℝ+ ∧ ∀ 𝑤 ∈ ( 𝐴 ∩ ( -∞ (,) 𝐵 ) ) ( ( 𝑤 ≠ 𝐵 ∧ ( abs ‘ ( 𝑤 − 𝐵 ) ) < 𝑣 ) → ( abs ‘ ( ( ( 𝐹 ↾ ( -∞ (,) 𝐵 ) ) ‘ 𝑤 ) − 𝐿 ) ) < 𝑦 ) ) ∧ 𝑎 ∈ ( ( 𝐴 ∩ ( -∞ (,) 𝐵 ) ) ∖ { 𝐵 } ) ∧ ( ( abs ‘ ( 𝑎 − 𝐵 ) ) < 𝑧 ∧ ( abs ‘ ( 𝑎 − 𝐵 ) ) < 𝑣 ) ) → ( abs ‘ ( ( 𝐹 ‘ 𝑎 ) − 𝑥 ) ) < 𝑦 )
304 261 3ad2ant2 ⊢ ( ( ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ+ ) ∧ 𝑧 ∈ ℝ+ ∧ ∀ 𝑤 ∈ 𝐴 ( ( 𝑤 ≠ 𝐵 ∧ ( abs ‘ ( 𝑤 − 𝐵 ) ) < 𝑧 ) → ( abs ‘ ( ( 𝐹 ‘ 𝑤 ) − 𝑥 ) ) < 𝑦 ) ) ∧ 𝑣 ∈ ℝ+ ∧ ∀ 𝑤 ∈ ( 𝐴 ∩ ( -∞ (,) 𝐵 ) ) ( ( 𝑤 ≠ 𝐵 ∧ ( abs ‘ ( 𝑤 − 𝐵 ) ) < 𝑣 ) → ( abs ‘ ( ( ( 𝐹 ↾ ( -∞ (,) 𝐵 ) ) ‘ 𝑤 ) − 𝐿 ) ) < 𝑦 ) ) ∧ 𝑎 ∈ ( ( 𝐴 ∩ ( -∞ (,) 𝐵 ) ) ∖ { 𝐵 } ) ∧ ( ( abs ‘ ( 𝑎 − 𝐵 ) ) < 𝑧 ∧ ( abs ‘ ( 𝑎 − 𝐵 ) ) < 𝑣 ) ) → 𝑎 ∈ ( 𝐴 ∩ ( -∞ (,) 𝐵 ) ) )
305 243 3ad2ant1 ⊢ ( ( ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ+ ) ∧ 𝑧 ∈ ℝ+ ∧ ∀ 𝑤 ∈ 𝐴 ( ( 𝑤 ≠ 𝐵 ∧ ( abs ‘ ( 𝑤 − 𝐵 ) ) < 𝑧 ) → ( abs ‘ ( ( 𝐹 ‘ 𝑤 ) − 𝑥 ) ) < 𝑦 ) ) ∧ 𝑣 ∈ ℝ+ ∧ ∀ 𝑤 ∈ ( 𝐴 ∩ ( -∞ (,) 𝐵 ) ) ( ( 𝑤 ≠ 𝐵 ∧ ( abs ‘ ( 𝑤 − 𝐵 ) ) < 𝑣 ) → ( abs ‘ ( ( ( 𝐹 ↾ ( -∞ (,) 𝐵 ) ) ‘ 𝑤 ) − 𝐿 ) ) < 𝑦 ) ) ∧ 𝑎 ∈ ( ( 𝐴 ∩ ( -∞ (,) 𝐵 ) ) ∖ { 𝐵 } ) ∧ ( ( abs ‘ ( 𝑎 − 𝐵 ) ) < 𝑧 ∧ ( abs ‘ ( 𝑎 − 𝐵 ) ) < 𝑣 ) ) → 𝜑 )
306 simp13 ⊢ ( ( ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ+ ) ∧ 𝑧 ∈ ℝ+ ∧ ∀ 𝑤 ∈ 𝐴 ( ( 𝑤 ≠ 𝐵 ∧ ( abs ‘ ( 𝑤 − 𝐵 ) ) < 𝑧 ) → ( abs ‘ ( ( 𝐹 ‘ 𝑤 ) − 𝑥 ) ) < 𝑦 ) ) ∧ 𝑣 ∈ ℝ+ ∧ ∀ 𝑤 ∈ ( 𝐴 ∩ ( -∞ (,) 𝐵 ) ) ( ( 𝑤 ≠ 𝐵 ∧ ( abs ‘ ( 𝑤 − 𝐵 ) ) < 𝑣 ) → ( abs ‘ ( ( ( 𝐹 ↾ ( -∞ (,) 𝐵 ) ) ‘ 𝑤 ) − 𝐿 ) ) < 𝑦 ) ) ∧ 𝑎 ∈ ( ( 𝐴 ∩ ( -∞ (,) 𝐵 ) ) ∖ { 𝐵 } ) ∧ ( ( abs ‘ ( 𝑎 − 𝐵 ) ) < 𝑧 ∧ ( abs ‘ ( 𝑎 − 𝐵 ) ) < 𝑣 ) ) → ∀ 𝑤 ∈ ( 𝐴 ∩ ( -∞ (,) 𝐵 ) ) ( ( 𝑤 ≠ 𝐵 ∧ ( abs ‘ ( 𝑤 − 𝐵 ) ) < 𝑣 ) → ( abs ‘ ( ( ( 𝐹 ↾ ( -∞ (,) 𝐵 ) ) ‘ 𝑤 ) − 𝐿 ) ) < 𝑦 ) )
307 nfra1 ⊢ Ⅎ 𝑤 ∀ 𝑤 ∈ ( 𝐴 ∩ ( -∞ (,) 𝐵 ) ) ( ( 𝑤 ≠ 𝐵 ∧ ( abs ‘ ( 𝑤 − 𝐵 ) ) < 𝑣 ) → ( abs ‘ ( ( ( 𝐹 ↾ ( -∞ (,) 𝐵 ) ) ‘ 𝑤 ) − 𝐿 ) ) < 𝑦 )
308 149 307 nfan ⊢ Ⅎ 𝑤 ( 𝜑 ∧ ∀ 𝑤 ∈ ( 𝐴 ∩ ( -∞ (,) 𝐵 ) ) ( ( 𝑤 ≠ 𝐵 ∧ ( abs ‘ ( 𝑤 − 𝐵 ) ) < 𝑣 ) → ( abs ‘ ( ( ( 𝐹 ↾ ( -∞ (,) 𝐵 ) ) ‘ 𝑤 ) − 𝐿 ) ) < 𝑦 ) )
309 elinel2 ⊢ ( 𝑤 ∈ ( 𝐴 ∩ ( -∞ (,) 𝐵 ) ) → 𝑤 ∈ ( -∞ (,) 𝐵 ) )
310 309 fvresd ⊢ ( 𝑤 ∈ ( 𝐴 ∩ ( -∞ (,) 𝐵 ) ) → ( ( 𝐹 ↾ ( -∞ (,) 𝐵 ) ) ‘ 𝑤 ) = ( 𝐹 ‘ 𝑤 ) )
311 310 eqcomd ⊢ ( 𝑤 ∈ ( 𝐴 ∩ ( -∞ (,) 𝐵 ) ) → ( 𝐹 ‘ 𝑤 ) = ( ( 𝐹 ↾ ( -∞ (,) 𝐵 ) ) ‘ 𝑤 ) )
312 311 fvoveq1d ⊢ ( 𝑤 ∈ ( 𝐴 ∩ ( -∞ (,) 𝐵 ) ) → ( abs ‘ ( ( 𝐹 ‘ 𝑤 ) − 𝐿 ) ) = ( abs ‘ ( ( ( 𝐹 ↾ ( -∞ (,) 𝐵 ) ) ‘ 𝑤 ) − 𝐿 ) ) )
313 312 3ad2ant2 ⊢ ( ( ( 𝜑 ∧ ∀ 𝑤 ∈ ( 𝐴 ∩ ( -∞ (,) 𝐵 ) ) ( ( 𝑤 ≠ 𝐵 ∧ ( abs ‘ ( 𝑤 − 𝐵 ) ) < 𝑣 ) → ( abs ‘ ( ( ( 𝐹 ↾ ( -∞ (,) 𝐵 ) ) ‘ 𝑤 ) − 𝐿 ) ) < 𝑦 ) ) ∧ 𝑤 ∈ ( 𝐴 ∩ ( -∞ (,) 𝐵 ) ) ∧ ( 𝑤 ≠ 𝐵 ∧ ( abs ‘ ( 𝑤 − 𝐵 ) ) < 𝑣 ) ) → ( abs ‘ ( ( 𝐹 ‘ 𝑤 ) − 𝐿 ) ) = ( abs ‘ ( ( ( 𝐹 ↾ ( -∞ (,) 𝐵 ) ) ‘ 𝑤 ) − 𝐿 ) ) )
314 rspa ⊢ ( ( ∀ 𝑤 ∈ ( 𝐴 ∩ ( -∞ (,) 𝐵 ) ) ( ( 𝑤 ≠ 𝐵 ∧ ( abs ‘ ( 𝑤 − 𝐵 ) ) < 𝑣 ) → ( abs ‘ ( ( ( 𝐹 ↾ ( -∞ (,) 𝐵 ) ) ‘ 𝑤 ) − 𝐿 ) ) < 𝑦 ) ∧ 𝑤 ∈ ( 𝐴 ∩ ( -∞ (,) 𝐵 ) ) ) → ( ( 𝑤 ≠ 𝐵 ∧ ( abs ‘ ( 𝑤 − 𝐵 ) ) < 𝑣 ) → ( abs ‘ ( ( ( 𝐹 ↾ ( -∞ (,) 𝐵 ) ) ‘ 𝑤 ) − 𝐿 ) ) < 𝑦 ) )
315 314 3impia ⊢ ( ( ∀ 𝑤 ∈ ( 𝐴 ∩ ( -∞ (,) 𝐵 ) ) ( ( 𝑤 ≠ 𝐵 ∧ ( abs ‘ ( 𝑤 − 𝐵 ) ) < 𝑣 ) → ( abs ‘ ( ( ( 𝐹 ↾ ( -∞ (,) 𝐵 ) ) ‘ 𝑤 ) − 𝐿 ) ) < 𝑦 ) ∧ 𝑤 ∈ ( 𝐴 ∩ ( -∞ (,) 𝐵 ) ) ∧ ( 𝑤 ≠ 𝐵 ∧ ( abs ‘ ( 𝑤 − 𝐵 ) ) < 𝑣 ) ) → ( abs ‘ ( ( ( 𝐹 ↾ ( -∞ (,) 𝐵 ) ) ‘ 𝑤 ) − 𝐿 ) ) < 𝑦 )
316 315 3adant1l ⊢ ( ( ( 𝜑 ∧ ∀ 𝑤 ∈ ( 𝐴 ∩ ( -∞ (,) 𝐵 ) ) ( ( 𝑤 ≠ 𝐵 ∧ ( abs ‘ ( 𝑤 − 𝐵 ) ) < 𝑣 ) → ( abs ‘ ( ( ( 𝐹 ↾ ( -∞ (,) 𝐵 ) ) ‘ 𝑤 ) − 𝐿 ) ) < 𝑦 ) ) ∧ 𝑤 ∈ ( 𝐴 ∩ ( -∞ (,) 𝐵 ) ) ∧ ( 𝑤 ≠ 𝐵 ∧ ( abs ‘ ( 𝑤 − 𝐵 ) ) < 𝑣 ) ) → ( abs ‘ ( ( ( 𝐹 ↾ ( -∞ (,) 𝐵 ) ) ‘ 𝑤 ) − 𝐿 ) ) < 𝑦 )
317 313 316 eqbrtrd ⊢ ( ( ( 𝜑 ∧ ∀ 𝑤 ∈ ( 𝐴 ∩ ( -∞ (,) 𝐵 ) ) ( ( 𝑤 ≠ 𝐵 ∧ ( abs ‘ ( 𝑤 − 𝐵 ) ) < 𝑣 ) → ( abs ‘ ( ( ( 𝐹 ↾ ( -∞ (,) 𝐵 ) ) ‘ 𝑤 ) − 𝐿 ) ) < 𝑦 ) ) ∧ 𝑤 ∈ ( 𝐴 ∩ ( -∞ (,) 𝐵 ) ) ∧ ( 𝑤 ≠ 𝐵 ∧ ( abs ‘ ( 𝑤 − 𝐵 ) ) < 𝑣 ) ) → ( abs ‘ ( ( 𝐹 ‘ 𝑤 ) − 𝐿 ) ) < 𝑦 )
318 317 3exp ⊢ ( ( 𝜑 ∧ ∀ 𝑤 ∈ ( 𝐴 ∩ ( -∞ (,) 𝐵 ) ) ( ( 𝑤 ≠ 𝐵 ∧ ( abs ‘ ( 𝑤 − 𝐵 ) ) < 𝑣 ) → ( abs ‘ ( ( ( 𝐹 ↾ ( -∞ (,) 𝐵 ) ) ‘ 𝑤 ) − 𝐿 ) ) < 𝑦 ) ) → ( 𝑤 ∈ ( 𝐴 ∩ ( -∞ (,) 𝐵 ) ) → ( ( 𝑤 ≠ 𝐵 ∧ ( abs ‘ ( 𝑤 − 𝐵 ) ) < 𝑣 ) → ( abs ‘ ( ( 𝐹 ‘ 𝑤 ) − 𝐿 ) ) < 𝑦 ) ) )
319 308 318 ralrimi ⊢ ( ( 𝜑 ∧ ∀ 𝑤 ∈ ( 𝐴 ∩ ( -∞ (,) 𝐵 ) ) ( ( 𝑤 ≠ 𝐵 ∧ ( abs ‘ ( 𝑤 − 𝐵 ) ) < 𝑣 ) → ( abs ‘ ( ( ( 𝐹 ↾ ( -∞ (,) 𝐵 ) ) ‘ 𝑤 ) − 𝐿 ) ) < 𝑦 ) ) → ∀ 𝑤 ∈ ( 𝐴 ∩ ( -∞ (,) 𝐵 ) ) ( ( 𝑤 ≠ 𝐵 ∧ ( abs ‘ ( 𝑤 − 𝐵 ) ) < 𝑣 ) → ( abs ‘ ( ( 𝐹 ‘ 𝑤 ) − 𝐿 ) ) < 𝑦 ) )
320 305 306 319 syl2anc ⊢ ( ( ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ+ ) ∧ 𝑧 ∈ ℝ+ ∧ ∀ 𝑤 ∈ 𝐴 ( ( 𝑤 ≠ 𝐵 ∧ ( abs ‘ ( 𝑤 − 𝐵 ) ) < 𝑧 ) → ( abs ‘ ( ( 𝐹 ‘ 𝑤 ) − 𝑥 ) ) < 𝑦 ) ) ∧ 𝑣 ∈ ℝ+ ∧ ∀ 𝑤 ∈ ( 𝐴 ∩ ( -∞ (,) 𝐵 ) ) ( ( 𝑤 ≠ 𝐵 ∧ ( abs ‘ ( 𝑤 − 𝐵 ) ) < 𝑣 ) → ( abs ‘ ( ( ( 𝐹 ↾ ( -∞ (,) 𝐵 ) ) ‘ 𝑤 ) − 𝐿 ) ) < 𝑦 ) ) ∧ 𝑎 ∈ ( ( 𝐴 ∩ ( -∞ (,) 𝐵 ) ) ∖ { 𝐵 } ) ∧ ( ( abs ‘ ( 𝑎 − 𝐵 ) ) < 𝑧 ∧ ( abs ‘ ( 𝑎 − 𝐵 ) ) < 𝑣 ) ) → ∀ 𝑤 ∈ ( 𝐴 ∩ ( -∞ (,) 𝐵 ) ) ( ( 𝑤 ≠ 𝐵 ∧ ( abs ‘ ( 𝑤 − 𝐵 ) ) < 𝑣 ) → ( abs ‘ ( ( 𝐹 ‘ 𝑤 ) − 𝐿 ) ) < 𝑦 ) )
321 291 anim1i ⊢ ( ( 𝑎 ∈ ( ( 𝐴 ∩ ( -∞ (,) 𝐵 ) ) ∖ { 𝐵 } ) ∧ ( abs ‘ ( 𝑎 − 𝐵 ) ) < 𝑣 ) → ( 𝑎 ≠ 𝐵 ∧ ( abs ‘ ( 𝑎 − 𝐵 ) ) < 𝑣 ) )
322 321 adantrl ⊢ ( ( 𝑎 ∈ ( ( 𝐴 ∩ ( -∞ (,) 𝐵 ) ) ∖ { 𝐵 } ) ∧ ( ( abs ‘ ( 𝑎 − 𝐵 ) ) < 𝑧 ∧ ( abs ‘ ( 𝑎 − 𝐵 ) ) < 𝑣 ) ) → ( 𝑎 ≠ 𝐵 ∧ ( abs ‘ ( 𝑎 − 𝐵 ) ) < 𝑣 ) )
323 322 3adant1 ⊢ ( ( ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ+ ) ∧ 𝑧 ∈ ℝ+ ∧ ∀ 𝑤 ∈ 𝐴 ( ( 𝑤 ≠ 𝐵 ∧ ( abs ‘ ( 𝑤 − 𝐵 ) ) < 𝑧 ) → ( abs ‘ ( ( 𝐹 ‘ 𝑤 ) − 𝑥 ) ) < 𝑦 ) ) ∧ 𝑣 ∈ ℝ+ ∧ ∀ 𝑤 ∈ ( 𝐴 ∩ ( -∞ (,) 𝐵 ) ) ( ( 𝑤 ≠ 𝐵 ∧ ( abs ‘ ( 𝑤 − 𝐵 ) ) < 𝑣 ) → ( abs ‘ ( ( ( 𝐹 ↾ ( -∞ (,) 𝐵 ) ) ‘ 𝑤 ) − 𝐿 ) ) < 𝑦 ) ) ∧ 𝑎 ∈ ( ( 𝐴 ∩ ( -∞ (,) 𝐵 ) ) ∖ { 𝐵 } ) ∧ ( ( abs ‘ ( 𝑎 − 𝐵 ) ) < 𝑧 ∧ ( abs ‘ ( 𝑎 − 𝐵 ) ) < 𝑣 ) ) → ( 𝑎 ≠ 𝐵 ∧ ( abs ‘ ( 𝑎 − 𝐵 ) ) < 𝑣 ) )
324 297 breq1d ⊢ ( 𝑤 = 𝑎 → ( ( abs ‘ ( 𝑤 − 𝐵 ) ) < 𝑣 ↔ ( abs ‘ ( 𝑎 − 𝐵 ) ) < 𝑣 ) )
325 296 324 anbi12d ⊢ ( 𝑤 = 𝑎 → ( ( 𝑤 ≠ 𝐵 ∧ ( abs ‘ ( 𝑤 − 𝐵 ) ) < 𝑣 ) ↔ ( 𝑎 ≠ 𝐵 ∧ ( abs ‘ ( 𝑎 − 𝐵 ) ) < 𝑣 ) ) )
326 325 imbrov2fvoveq ⊢ ( 𝑤 = 𝑎 → ( ( ( 𝑤 ≠ 𝐵 ∧ ( abs ‘ ( 𝑤 − 𝐵 ) ) < 𝑣 ) → ( abs ‘ ( ( 𝐹 ‘ 𝑤 ) − 𝐿 ) ) < 𝑦 ) ↔ ( ( 𝑎 ≠ 𝐵 ∧ ( abs ‘ ( 𝑎 − 𝐵 ) ) < 𝑣 ) → ( abs ‘ ( ( 𝐹 ‘ 𝑎 ) − 𝐿 ) ) < 𝑦 ) ) )
327 326 rspcva ⊢ ( ( 𝑎 ∈ ( 𝐴 ∩ ( -∞ (,) 𝐵 ) ) ∧ ∀ 𝑤 ∈ ( 𝐴 ∩ ( -∞ (,) 𝐵 ) ) ( ( 𝑤 ≠ 𝐵 ∧ ( abs ‘ ( 𝑤 − 𝐵 ) ) < 𝑣 ) → ( abs ‘ ( ( 𝐹 ‘ 𝑤 ) − 𝐿 ) ) < 𝑦 ) ) → ( ( 𝑎 ≠ 𝐵 ∧ ( abs ‘ ( 𝑎 − 𝐵 ) ) < 𝑣 ) → ( abs ‘ ( ( 𝐹 ‘ 𝑎 ) − 𝐿 ) ) < 𝑦 ) )
328 327 imp ⊢ ( ( ( 𝑎 ∈ ( 𝐴 ∩ ( -∞ (,) 𝐵 ) ) ∧ ∀ 𝑤 ∈ ( 𝐴 ∩ ( -∞ (,) 𝐵 ) ) ( ( 𝑤 ≠ 𝐵 ∧ ( abs ‘ ( 𝑤 − 𝐵 ) ) < 𝑣 ) → ( abs ‘ ( ( 𝐹 ‘ 𝑤 ) − 𝐿 ) ) < 𝑦 ) ) ∧ ( 𝑎 ≠ 𝐵 ∧ ( abs ‘ ( 𝑎 − 𝐵 ) ) < 𝑣 ) ) → ( abs ‘ ( ( 𝐹 ‘ 𝑎 ) − 𝐿 ) ) < 𝑦 )
329 304 320 323 328 syl21anc ⊢ ( ( ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ+ ) ∧ 𝑧 ∈ ℝ+ ∧ ∀ 𝑤 ∈ 𝐴 ( ( 𝑤 ≠ 𝐵 ∧ ( abs ‘ ( 𝑤 − 𝐵 ) ) < 𝑧 ) → ( abs ‘ ( ( 𝐹 ‘ 𝑤 ) − 𝑥 ) ) < 𝑦 ) ) ∧ 𝑣 ∈ ℝ+ ∧ ∀ 𝑤 ∈ ( 𝐴 ∩ ( -∞ (,) 𝐵 ) ) ( ( 𝑤 ≠ 𝐵 ∧ ( abs ‘ ( 𝑤 − 𝐵 ) ) < 𝑣 ) → ( abs ‘ ( ( ( 𝐹 ↾ ( -∞ (,) 𝐵 ) ) ‘ 𝑤 ) − 𝐿 ) ) < 𝑦 ) ) ∧ 𝑎 ∈ ( ( 𝐴 ∩ ( -∞ (,) 𝐵 ) ) ∖ { 𝐵 } ) ∧ ( ( abs ‘ ( 𝑎 − 𝐵 ) ) < 𝑧 ∧ ( abs ‘ ( 𝑎 − 𝐵 ) ) < 𝑣 ) ) → ( abs ‘ ( ( 𝐹 ‘ 𝑎 ) − 𝐿 ) ) < 𝑦 )
330 rspe ⊢ ( ( 𝑎 ∈ 𝐴 ∧ ( ( abs ‘ ( ( 𝐹 ‘ 𝑎 ) − 𝑥 ) ) < 𝑦 ∧ ( abs ‘ ( ( 𝐹 ‘ 𝑎 ) − 𝐿 ) ) < 𝑦 ) ) → ∃ 𝑎 ∈ 𝐴 ( ( abs ‘ ( ( 𝐹 ‘ 𝑎 ) − 𝑥 ) ) < 𝑦 ∧ ( abs ‘ ( ( 𝐹 ‘ 𝑎 ) − 𝐿 ) ) < 𝑦 ) )
331 289 303 329 330 syl12anc ⊢ ( ( ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ+ ) ∧ 𝑧 ∈ ℝ+ ∧ ∀ 𝑤 ∈ 𝐴 ( ( 𝑤 ≠ 𝐵 ∧ ( abs ‘ ( 𝑤 − 𝐵 ) ) < 𝑧 ) → ( abs ‘ ( ( 𝐹 ‘ 𝑤 ) − 𝑥 ) ) < 𝑦 ) ) ∧ 𝑣 ∈ ℝ+ ∧ ∀ 𝑤 ∈ ( 𝐴 ∩ ( -∞ (,) 𝐵 ) ) ( ( 𝑤 ≠ 𝐵 ∧ ( abs ‘ ( 𝑤 − 𝐵 ) ) < 𝑣 ) → ( abs ‘ ( ( ( 𝐹 ↾ ( -∞ (,) 𝐵 ) ) ‘ 𝑤 ) − 𝐿 ) ) < 𝑦 ) ) ∧ 𝑎 ∈ ( ( 𝐴 ∩ ( -∞ (,) 𝐵 ) ) ∖ { 𝐵 } ) ∧ ( ( abs ‘ ( 𝑎 − 𝐵 ) ) < 𝑧 ∧ ( abs ‘ ( 𝑎 − 𝐵 ) ) < 𝑣 ) ) → ∃ 𝑎 ∈ 𝐴 ( ( abs ‘ ( ( 𝐹 ‘ 𝑎 ) − 𝑥 ) ) < 𝑦 ∧ ( abs ‘ ( ( 𝐹 ‘ 𝑎 ) − 𝐿 ) ) < 𝑦 ) )
332 331 3exp ⊢ ( ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ+ ) ∧ 𝑧 ∈ ℝ+ ∧ ∀ 𝑤 ∈ 𝐴 ( ( 𝑤 ≠ 𝐵 ∧ ( abs ‘ ( 𝑤 − 𝐵 ) ) < 𝑧 ) → ( abs ‘ ( ( 𝐹 ‘ 𝑤 ) − 𝑥 ) ) < 𝑦 ) ) ∧ 𝑣 ∈ ℝ+ ∧ ∀ 𝑤 ∈ ( 𝐴 ∩ ( -∞ (,) 𝐵 ) ) ( ( 𝑤 ≠ 𝐵 ∧ ( abs ‘ ( 𝑤 − 𝐵 ) ) < 𝑣 ) → ( abs ‘ ( ( ( 𝐹 ↾ ( -∞ (,) 𝐵 ) ) ‘ 𝑤 ) − 𝐿 ) ) < 𝑦 ) ) → ( 𝑎 ∈ ( ( 𝐴 ∩ ( -∞ (,) 𝐵 ) ) ∖ { 𝐵 } ) → ( ( ( abs ‘ ( 𝑎 − 𝐵 ) ) < 𝑧 ∧ ( abs ‘ ( 𝑎 − 𝐵 ) ) < 𝑣 ) → ∃ 𝑎 ∈ 𝐴 ( ( abs ‘ ( ( 𝐹 ‘ 𝑎 ) − 𝑥 ) ) < 𝑦 ∧ ( abs ‘ ( ( 𝐹 ‘ 𝑎 ) − 𝐿 ) ) < 𝑦 ) ) ) )
333 286 287 332 rexlimd ⊢ ( ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ+ ) ∧ 𝑧 ∈ ℝ+ ∧ ∀ 𝑤 ∈ 𝐴 ( ( 𝑤 ≠ 𝐵 ∧ ( abs ‘ ( 𝑤 − 𝐵 ) ) < 𝑧 ) → ( abs ‘ ( ( 𝐹 ‘ 𝑤 ) − 𝑥 ) ) < 𝑦 ) ) ∧ 𝑣 ∈ ℝ+ ∧ ∀ 𝑤 ∈ ( 𝐴 ∩ ( -∞ (,) 𝐵 ) ) ( ( 𝑤 ≠ 𝐵 ∧ ( abs ‘ ( 𝑤 − 𝐵 ) ) < 𝑣 ) → ( abs ‘ ( ( ( 𝐹 ↾ ( -∞ (,) 𝐵 ) ) ‘ 𝑤 ) − 𝐿 ) ) < 𝑦 ) ) → ( ∃ 𝑎 ∈ ( ( 𝐴 ∩ ( -∞ (,) 𝐵 ) ) ∖ { 𝐵 } ) ( ( abs ‘ ( 𝑎 − 𝐵 ) ) < 𝑧 ∧ ( abs ‘ ( 𝑎 − 𝐵 ) ) < 𝑣 ) → ∃ 𝑎 ∈ 𝐴 ( ( abs ‘ ( ( 𝐹 ‘ 𝑎 ) − 𝑥 ) ) < 𝑦 ∧ ( abs ‘ ( ( 𝐹 ‘ 𝑎 ) − 𝐿 ) ) < 𝑦 ) ) )
334 285 333 mpd ⊢ ( ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ+ ) ∧ 𝑧 ∈ ℝ+ ∧ ∀ 𝑤 ∈ 𝐴 ( ( 𝑤 ≠ 𝐵 ∧ ( abs ‘ ( 𝑤 − 𝐵 ) ) < 𝑧 ) → ( abs ‘ ( ( 𝐹 ‘ 𝑤 ) − 𝑥 ) ) < 𝑦 ) ) ∧ 𝑣 ∈ ℝ+ ∧ ∀ 𝑤 ∈ ( 𝐴 ∩ ( -∞ (,) 𝐵 ) ) ( ( 𝑤 ≠ 𝐵 ∧ ( abs ‘ ( 𝑤 − 𝐵 ) ) < 𝑣 ) → ( abs ‘ ( ( ( 𝐹 ↾ ( -∞ (,) 𝐵 ) ) ‘ 𝑤 ) − 𝐿 ) ) < 𝑦 ) ) → ∃ 𝑎 ∈ 𝐴 ( ( abs ‘ ( ( 𝐹 ‘ 𝑎 ) − 𝑥 ) ) < 𝑦 ∧ ( abs ‘ ( ( 𝐹 ‘ 𝑎 ) − 𝐿 ) ) < 𝑦 ) )
335 334 3exp ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ+ ) ∧ 𝑧 ∈ ℝ+ ∧ ∀ 𝑤 ∈ 𝐴 ( ( 𝑤 ≠ 𝐵 ∧ ( abs ‘ ( 𝑤 − 𝐵 ) ) < 𝑧 ) → ( abs ‘ ( ( 𝐹 ‘ 𝑤 ) − 𝑥 ) ) < 𝑦 ) ) → ( 𝑣 ∈ ℝ+ → ( ∀ 𝑤 ∈ ( 𝐴 ∩ ( -∞ (,) 𝐵 ) ) ( ( 𝑤 ≠ 𝐵 ∧ ( abs ‘ ( 𝑤 − 𝐵 ) ) < 𝑣 ) → ( abs ‘ ( ( ( 𝐹 ↾ ( -∞ (,) 𝐵 ) ) ‘ 𝑤 ) − 𝐿 ) ) < 𝑦 ) → ∃ 𝑎 ∈ 𝐴 ( ( abs ‘ ( ( 𝐹 ‘ 𝑎 ) − 𝑥 ) ) < 𝑦 ∧ ( abs ‘ ( ( 𝐹 ‘ 𝑎 ) − 𝐿 ) ) < 𝑦 ) ) ) )
336 335 rexlimdv ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ+ ) ∧ 𝑧 ∈ ℝ+ ∧ ∀ 𝑤 ∈ 𝐴 ( ( 𝑤 ≠ 𝐵 ∧ ( abs ‘ ( 𝑤 − 𝐵 ) ) < 𝑧 ) → ( abs ‘ ( ( 𝐹 ‘ 𝑤 ) − 𝑥 ) ) < 𝑦 ) ) → ( ∃ 𝑣 ∈ ℝ+ ∀ 𝑤 ∈ ( 𝐴 ∩ ( -∞ (,) 𝐵 ) ) ( ( 𝑤 ≠ 𝐵 ∧ ( abs ‘ ( 𝑤 − 𝐵 ) ) < 𝑣 ) → ( abs ‘ ( ( ( 𝐹 ↾ ( -∞ (,) 𝐵 ) ) ‘ 𝑤 ) − 𝐿 ) ) < 𝑦 ) → ∃ 𝑎 ∈ 𝐴 ( ( abs ‘ ( ( 𝐹 ‘ 𝑎 ) − 𝑥 ) ) < 𝑦 ∧ ( abs ‘ ( ( 𝐹 ‘ 𝑎 ) − 𝐿 ) ) < 𝑦 ) ) )
337 242 336 mpd ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ+ ) ∧ 𝑧 ∈ ℝ+ ∧ ∀ 𝑤 ∈ 𝐴 ( ( 𝑤 ≠ 𝐵 ∧ ( abs ‘ ( 𝑤 − 𝐵 ) ) < 𝑧 ) → ( abs ‘ ( ( 𝐹 ‘ 𝑤 ) − 𝑥 ) ) < 𝑦 ) ) → ∃ 𝑎 ∈ 𝐴 ( ( abs ‘ ( ( 𝐹 ‘ 𝑎 ) − 𝑥 ) ) < 𝑦 ∧ ( abs ‘ ( ( 𝐹 ‘ 𝑎 ) − 𝐿 ) ) < 𝑦 ) )
338 337 3exp ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ℝ+ ) → ( 𝑧 ∈ ℝ+ → ( ∀ 𝑤 ∈ 𝐴 ( ( 𝑤 ≠ 𝐵 ∧ ( abs ‘ ( 𝑤 − 𝐵 ) ) < 𝑧 ) → ( abs ‘ ( ( 𝐹 ‘ 𝑤 ) − 𝑥 ) ) < 𝑦 ) → ∃ 𝑎 ∈ 𝐴 ( ( abs ‘ ( ( 𝐹 ‘ 𝑎 ) − 𝑥 ) ) < 𝑦 ∧ ( abs ‘ ( ( 𝐹 ‘ 𝑎 ) − 𝐿 ) ) < 𝑦 ) ) ) )
339 338 rexlimdv ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ℝ+ ) → ( ∃ 𝑧 ∈ ℝ+ ∀ 𝑤 ∈ 𝐴 ( ( 𝑤 ≠ 𝐵 ∧ ( abs ‘ ( 𝑤 − 𝐵 ) ) < 𝑧 ) → ( abs ‘ ( ( 𝐹 ‘ 𝑤 ) − 𝑥 ) ) < 𝑦 ) → ∃ 𝑎 ∈ 𝐴 ( ( abs ‘ ( ( 𝐹 ‘ 𝑎 ) − 𝑥 ) ) < 𝑦 ∧ ( abs ‘ ( ( 𝐹 ‘ 𝑎 ) − 𝐿 ) ) < 𝑦 ) ) )
340 339 imp ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ+ ) ∧ ∃ 𝑧 ∈ ℝ+ ∀ 𝑤 ∈ 𝐴 ( ( 𝑤 ≠ 𝐵 ∧ ( abs ‘ ( 𝑤 − 𝐵 ) ) < 𝑧 ) → ( abs ‘ ( ( 𝐹 ‘ 𝑤 ) − 𝑥 ) ) < 𝑦 ) ) → ∃ 𝑎 ∈ 𝐴 ( ( abs ‘ ( ( 𝐹 ‘ 𝑎 ) − 𝑥 ) ) < 𝑦 ∧ ( abs ‘ ( ( 𝐹 ‘ 𝑎 ) − 𝐿 ) ) < 𝑦 ) )
341 340 adantllr ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ ℂ ) ∧ 𝑦 ∈ ℝ+ ) ∧ ∃ 𝑧 ∈ ℝ+ ∀ 𝑤 ∈ 𝐴 ( ( 𝑤 ≠ 𝐵 ∧ ( abs ‘ ( 𝑤 − 𝐵 ) ) < 𝑧 ) → ( abs ‘ ( ( 𝐹 ‘ 𝑤 ) − 𝑥 ) ) < 𝑦 ) ) → ∃ 𝑎 ∈ 𝐴 ( ( abs ‘ ( ( 𝐹 ‘ 𝑎 ) − 𝑥 ) ) < 𝑦 ∧ ( abs ‘ ( ( 𝐹 ‘ 𝑎 ) − 𝐿 ) ) < 𝑦 ) )
342 232 341 reximddv3 ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ ℂ ) ∧ 𝑦 ∈ ℝ+ ) ∧ ∃ 𝑧 ∈ ℝ+ ∀ 𝑤 ∈ 𝐴 ( ( 𝑤 ≠ 𝐵 ∧ ( abs ‘ ( 𝑤 − 𝐵 ) ) < 𝑧 ) → ( abs ‘ ( ( 𝐹 ‘ 𝑤 ) − 𝑥 ) ) < 𝑦 ) ) → ∃ 𝑎 ∈ 𝐴 ∃ 𝑏 ∈ 𝐴 ( abs ‘ ( 𝑅 − 𝐿 ) ) < ( 4 · 𝑦 ) )
343 38 39 41 342 syl21anc ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ ℂ ) ∧ ∀ 𝑦 ∈ ℝ+ ∃ 𝑧 ∈ ℝ+ ∀ 𝑤 ∈ 𝐴 ( ( 𝑤 ≠ 𝐵 ∧ ( abs ‘ ( 𝑤 − 𝐵 ) ) < 𝑧 ) → ( abs ‘ ( ( 𝐹 ‘ 𝑤 ) − 𝑥 ) ) < 𝑦 ) ) ∧ 𝑦 ∈ ℝ+ ) → ∃ 𝑎 ∈ 𝐴 ∃ 𝑏 ∈ 𝐴 ( abs ‘ ( 𝑅 − 𝐿 ) ) < ( 4 · 𝑦 ) )
344 343 ex ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℂ ) ∧ ∀ 𝑦 ∈ ℝ+ ∃ 𝑧 ∈ ℝ+ ∀ 𝑤 ∈ 𝐴 ( ( 𝑤 ≠ 𝐵 ∧ ( abs ‘ ( 𝑤 − 𝐵 ) ) < 𝑧 ) → ( abs ‘ ( ( 𝐹 ‘ 𝑤 ) − 𝑥 ) ) < 𝑦 ) ) → ( 𝑦 ∈ ℝ+ → ∃ 𝑎 ∈ 𝐴 ∃ 𝑏 ∈ 𝐴 ( abs ‘ ( 𝑅 − 𝐿 ) ) < ( 4 · 𝑦 ) ) )
345 30 31 37 344 vtoclf ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℂ ) ∧ ∀ 𝑦 ∈ ℝ+ ∃ 𝑧 ∈ ℝ+ ∀ 𝑤 ∈ 𝐴 ( ( 𝑤 ≠ 𝐵 ∧ ( abs ‘ ( 𝑤 − 𝐵 ) ) < 𝑧 ) → ( abs ‘ ( ( 𝐹 ‘ 𝑤 ) − 𝑥 ) ) < 𝑦 ) ) → ( ( ( abs ‘ ( 𝑅 − 𝐿 ) ) / 4 ) ∈ ℝ+ → ∃ 𝑎 ∈ 𝐴 ∃ 𝑏 ∈ 𝐴 ( abs ‘ ( 𝑅 − 𝐿 ) ) < ( 4 · ( ( abs ‘ ( 𝑅 − 𝐿 ) ) / 4 ) ) ) )
346 25 345 mpd ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℂ ) ∧ ∀ 𝑦 ∈ ℝ+ ∃ 𝑧 ∈ ℝ+ ∀ 𝑤 ∈ 𝐴 ( ( 𝑤 ≠ 𝐵 ∧ ( abs ‘ ( 𝑤 − 𝐵 ) ) < 𝑧 ) → ( abs ‘ ( ( 𝐹 ‘ 𝑤 ) − 𝑥 ) ) < 𝑦 ) ) → ∃ 𝑎 ∈ 𝐴 ∃ 𝑏 ∈ 𝐴 ( abs ‘ ( 𝑅 − 𝐿 ) ) < ( 4 · ( ( abs ‘ ( 𝑅 − 𝐿 ) ) / 4 ) ) )
347 simpr ⊢ ( ( 𝜑 ∧ ( abs ‘ ( 𝑅 − 𝐿 ) ) < ( 4 · ( ( abs ‘ ( 𝑅 − 𝐿 ) ) / 4 ) ) ) → ( abs ‘ ( 𝑅 − 𝐿 ) ) < ( 4 · ( ( abs ‘ ( 𝑅 − 𝐿 ) ) / 4 ) ) )
348 abssubrp ⊢ ( ( 𝑅 ∈ ℂ ∧ 𝐿 ∈ ℂ ∧ 𝑅 ≠ 𝐿 ) → ( abs ‘ ( 𝑅 − 𝐿 ) ) ∈ ℝ+ )
349 11 14 17 348 syl3anc ⊢ ( 𝜑 → ( abs ‘ ( 𝑅 − 𝐿 ) ) ∈ ℝ+ )
350 349 rpcnd ⊢ ( 𝜑 → ( abs ‘ ( 𝑅 − 𝐿 ) ) ∈ ℂ )
351 350 adantr ⊢ ( ( 𝜑 ∧ ( abs ‘ ( 𝑅 − 𝐿 ) ) < ( 4 · ( ( abs ‘ ( 𝑅 − 𝐿 ) ) / 4 ) ) ) → ( abs ‘ ( 𝑅 − 𝐿 ) ) ∈ ℂ )
352 4cn ⊢ 4 ∈ ℂ
353 352 a1i ⊢ ( ( 𝜑 ∧ ( abs ‘ ( 𝑅 − 𝐿 ) ) < ( 4 · ( ( abs ‘ ( 𝑅 − 𝐿 ) ) / 4 ) ) ) → 4 ∈ ℂ )
354 4ne0 ⊢ 4 ≠ 0
355 354 a1i ⊢ ( ( 𝜑 ∧ ( abs ‘ ( 𝑅 − 𝐿 ) ) < ( 4 · ( ( abs ‘ ( 𝑅 − 𝐿 ) ) / 4 ) ) ) → 4 ≠ 0 )
356 351 353 355 divcan2d ⊢ ( ( 𝜑 ∧ ( abs ‘ ( 𝑅 − 𝐿 ) ) < ( 4 · ( ( abs ‘ ( 𝑅 − 𝐿 ) ) / 4 ) ) ) → ( 4 · ( ( abs ‘ ( 𝑅 − 𝐿 ) ) / 4 ) ) = ( abs ‘ ( 𝑅 − 𝐿 ) ) )
357 347 356 breqtrd ⊢ ( ( 𝜑 ∧ ( abs ‘ ( 𝑅 − 𝐿 ) ) < ( 4 · ( ( abs ‘ ( 𝑅 − 𝐿 ) ) / 4 ) ) ) → ( abs ‘ ( 𝑅 − 𝐿 ) ) < ( abs ‘ ( 𝑅 − 𝐿 ) ) )
358 357 ex ⊢ ( 𝜑 → ( ( abs ‘ ( 𝑅 − 𝐿 ) ) < ( 4 · ( ( abs ‘ ( 𝑅 − 𝐿 ) ) / 4 ) ) → ( abs ‘ ( 𝑅 − 𝐿 ) ) < ( abs ‘ ( 𝑅 − 𝐿 ) ) ) )
359 358 a1d ⊢ ( 𝜑 → ( ( 𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐴 ) → ( ( abs ‘ ( 𝑅 − 𝐿 ) ) < ( 4 · ( ( abs ‘ ( 𝑅 − 𝐿 ) ) / 4 ) ) → ( abs ‘ ( 𝑅 − 𝐿 ) ) < ( abs ‘ ( 𝑅 − 𝐿 ) ) ) ) )
360 359 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℂ ) ∧ ∀ 𝑦 ∈ ℝ+ ∃ 𝑧 ∈ ℝ+ ∀ 𝑤 ∈ 𝐴 ( ( 𝑤 ≠ 𝐵 ∧ ( abs ‘ ( 𝑤 − 𝐵 ) ) < 𝑧 ) → ( abs ‘ ( ( 𝐹 ‘ 𝑤 ) − 𝑥 ) ) < 𝑦 ) ) → ( ( 𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐴 ) → ( ( abs ‘ ( 𝑅 − 𝐿 ) ) < ( 4 · ( ( abs ‘ ( 𝑅 − 𝐿 ) ) / 4 ) ) → ( abs ‘ ( 𝑅 − 𝐿 ) ) < ( abs ‘ ( 𝑅 − 𝐿 ) ) ) ) )
361 360 rexlimdvv ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℂ ) ∧ ∀ 𝑦 ∈ ℝ+ ∃ 𝑧 ∈ ℝ+ ∀ 𝑤 ∈ 𝐴 ( ( 𝑤 ≠ 𝐵 ∧ ( abs ‘ ( 𝑤 − 𝐵 ) ) < 𝑧 ) → ( abs ‘ ( ( 𝐹 ‘ 𝑤 ) − 𝑥 ) ) < 𝑦 ) ) → ( ∃ 𝑎 ∈ 𝐴 ∃ 𝑏 ∈ 𝐴 ( abs ‘ ( 𝑅 − 𝐿 ) ) < ( 4 · ( ( abs ‘ ( 𝑅 − 𝐿 ) ) / 4 ) ) → ( abs ‘ ( 𝑅 − 𝐿 ) ) < ( abs ‘ ( 𝑅 − 𝐿 ) ) ) )
362 346 361 mpd ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℂ ) ∧ ∀ 𝑦 ∈ ℝ+ ∃ 𝑧 ∈ ℝ+ ∀ 𝑤 ∈ 𝐴 ( ( 𝑤 ≠ 𝐵 ∧ ( abs ‘ ( 𝑤 − 𝐵 ) ) < 𝑧 ) → ( abs ‘ ( ( 𝐹 ‘ 𝑤 ) − 𝑥 ) ) < 𝑦 ) ) → ( abs ‘ ( 𝑅 − 𝐿 ) ) < ( abs ‘ ( 𝑅 − 𝐿 ) ) )
363 16 abscld ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℂ ) ∧ ∀ 𝑦 ∈ ℝ+ ∃ 𝑧 ∈ ℝ+ ∀ 𝑤 ∈ 𝐴 ( ( 𝑤 ≠ 𝐵 ∧ ( abs ‘ ( 𝑤 − 𝐵 ) ) < 𝑧 ) → ( abs ‘ ( ( 𝐹 ‘ 𝑤 ) − 𝑥 ) ) < 𝑦 ) ) → ( abs ‘ ( 𝑅 − 𝐿 ) ) ∈ ℝ )
364 363 ltnrd ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℂ ) ∧ ∀ 𝑦 ∈ ℝ+ ∃ 𝑧 ∈ ℝ+ ∀ 𝑤 ∈ 𝐴 ( ( 𝑤 ≠ 𝐵 ∧ ( abs ‘ ( 𝑤 − 𝐵 ) ) < 𝑧 ) → ( abs ‘ ( ( 𝐹 ‘ 𝑤 ) − 𝑥 ) ) < 𝑦 ) ) → ¬ ( abs ‘ ( 𝑅 − 𝐿 ) ) < ( abs ‘ ( 𝑅 − 𝐿 ) ) )
365 362 364 pm2.65da ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℂ ) → ¬ ∀ 𝑦 ∈ ℝ+ ∃ 𝑧 ∈ ℝ+ ∀ 𝑤 ∈ 𝐴 ( ( 𝑤 ≠ 𝐵 ∧ ( abs ‘ ( 𝑤 − 𝐵 ) ) < 𝑧 ) → ( abs ‘ ( ( 𝐹 ‘ 𝑤 ) − 𝑥 ) ) < 𝑦 ) )
366 365 ex ⊢ ( 𝜑 → ( 𝑥 ∈ ℂ → ¬ ∀ 𝑦 ∈ ℝ+ ∃ 𝑧 ∈ ℝ+ ∀ 𝑤 ∈ 𝐴 ( ( 𝑤 ≠ 𝐵 ∧ ( abs ‘ ( 𝑤 − 𝐵 ) ) < 𝑧 ) → ( abs ‘ ( ( 𝐹 ‘ 𝑤 ) − 𝑥 ) ) < 𝑦 ) ) )
367 imnan ⊢ ( ( 𝑥 ∈ ℂ → ¬ ∀ 𝑦 ∈ ℝ+ ∃ 𝑧 ∈ ℝ+ ∀ 𝑤 ∈ 𝐴 ( ( 𝑤 ≠ 𝐵 ∧ ( abs ‘ ( 𝑤 − 𝐵 ) ) < 𝑧 ) → ( abs ‘ ( ( 𝐹 ‘ 𝑤 ) − 𝑥 ) ) < 𝑦 ) ) ↔ ¬ ( 𝑥 ∈ ℂ ∧ ∀ 𝑦 ∈ ℝ+ ∃ 𝑧 ∈ ℝ+ ∀ 𝑤 ∈ 𝐴 ( ( 𝑤 ≠ 𝐵 ∧ ( abs ‘ ( 𝑤 − 𝐵 ) ) < 𝑧 ) → ( abs ‘ ( ( 𝐹 ‘ 𝑤 ) − 𝑥 ) ) < 𝑦 ) ) )
368 366 367 sylib ⊢ ( 𝜑 → ¬ ( 𝑥 ∈ ℂ ∧ ∀ 𝑦 ∈ ℝ+ ∃ 𝑧 ∈ ℝ+ ∀ 𝑤 ∈ 𝐴 ( ( 𝑤 ≠ 𝐵 ∧ ( abs ‘ ( 𝑤 − 𝐵 ) ) < 𝑧 ) → ( abs ‘ ( ( 𝐹 ‘ 𝑤 ) − 𝑥 ) ) < 𝑦 ) ) )
369 2 75 sstrd ⊢ ( 𝜑 → 𝐴 ⊆ ℂ )
370 4 369 59 ellimc3 ⊢ ( 𝜑 → ( 𝑥 ∈ ( 𝐹 limℂ 𝐵 ) ↔ ( 𝑥 ∈ ℂ ∧ ∀ 𝑦 ∈ ℝ+ ∃ 𝑧 ∈ ℝ+ ∀ 𝑤 ∈ 𝐴 ( ( 𝑤 ≠ 𝐵 ∧ ( abs ‘ ( 𝑤 − 𝐵 ) ) < 𝑧 ) → ( abs ‘ ( ( 𝐹 ‘ 𝑤 ) − 𝑥 ) ) < 𝑦 ) ) ) )
371 368 370 mtbird ⊢ ( 𝜑 → ¬ 𝑥 ∈ ( 𝐹 limℂ 𝐵 ) )
372 371 eq0rdv ⊢ ( 𝜑 → ( 𝐹 limℂ 𝐵 ) = ∅ )