limclner - Mathbox for Glauco Siliprandi

	Mathbox for Glauco Siliprandi		< Previous Next > Nearby theorems
Mirrors > Home > MPE Home > Th. List > Mathboxes > limclner		Structured version Visualization version GIF version

Theorem limclner 46223

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.)

**Hypotheses**
Ref	Expression
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**
Ref	Expression
limclner	⊢ (𝜑 → (𝐹 lim_ℂ 𝐵) = ∅)

Proof of Theorem limclner Dummy variables 𝑎 𝑏 𝑢 𝑣 𝑧 𝑤 𝑥 𝑦 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		limccl 25995	. . . . . . . . . . . . 13 ⊢ ((𝐹 ↾ (𝐵(,)+∞)) lim_ℂ 𝐵) ⊆ ℂ
2		limclner.r	. . . . . . . . . . . . 13 ⊢ (𝜑 → 𝑅 ∈ ((𝐹 ↾ (𝐵(,)+∞)) lim_ℂ 𝐵))
3	1, 2	sselid 3937	. . . . . . . . . . . 12 ⊢ (𝜑 → 𝑅 ∈ ℂ)
4	3	ad2antrr 738	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑥 ∈ ℂ) ∧ ∀𝑦 ∈ ℝ⁺ ∃𝑧 ∈ ℝ⁺ ∀𝑤 ∈ 𝐴 ((𝑤 ≠ 𝐵 ∧ (abs‘(𝑤 − 𝐵)) < 𝑧) → (abs‘((𝐹‘𝑤) − 𝑥)) < 𝑦)) → 𝑅 ∈ ℂ)
5		limccl 25995	. . . . . . . . . . . . 13 ⊢ ((𝐹 ↾ (-∞(,)𝐵)) lim_ℂ 𝐵) ⊆ ℂ
6		limclner.l	. . . . . . . . . . . . 13 ⊢ (𝜑 → 𝐿 ∈ ((𝐹 ↾ (-∞(,)𝐵)) lim_ℂ 𝐵))
7	5, 6	sselid 3937	. . . . . . . . . . . 12 ⊢ (𝜑 → 𝐿 ∈ ℂ)
8	7	ad2antrr 738	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑥 ∈ ℂ) ∧ ∀𝑦 ∈ ℝ⁺ ∃𝑧 ∈ ℝ⁺ ∀𝑤 ∈ 𝐴 ((𝑤 ≠ 𝐵 ∧ (abs‘(𝑤 − 𝐵)) < 𝑧) → (abs‘((𝐹‘𝑤) − 𝑥)) < 𝑦)) → 𝐿 ∈ ℂ)
9	4, 8	subcld 11557	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑥 ∈ ℂ) ∧ ∀𝑦 ∈ ℝ⁺ ∃𝑧 ∈ ℝ⁺ ∀𝑤 ∈ 𝐴 ((𝑤 ≠ 𝐵 ∧ (abs‘(𝑤 − 𝐵)) < 𝑧) → (abs‘((𝐹‘𝑤) − 𝑥)) < 𝑦)) → (𝑅 − 𝐿) ∈ ℂ)
10		limclner.lner	. . . . . . . . . . . . 13 ⊢ (𝜑 → 𝐿 ≠ 𝑅)
11	10	necomd 3015	. . . . . . . . . . . 12 ⊢ (𝜑 → 𝑅 ≠ 𝐿)
12	11	ad2antrr 738	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑥 ∈ ℂ) ∧ ∀𝑦 ∈ ℝ⁺ ∃𝑧 ∈ ℝ⁺ ∀𝑤 ∈ 𝐴 ((𝑤 ≠ 𝐵 ∧ (abs‘(𝑤 − 𝐵)) < 𝑧) → (abs‘((𝐹‘𝑤) − 𝑥)) < 𝑦)) → 𝑅 ≠ 𝐿)
13	4, 8, 12	subne0d 11566	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑥 ∈ ℂ) ∧ ∀𝑦 ∈ ℝ⁺ ∃𝑧 ∈ ℝ⁺ ∀𝑤 ∈ 𝐴 ((𝑤 ≠ 𝐵 ∧ (abs‘(𝑤 − 𝐵)) < 𝑧) → (abs‘((𝐹‘𝑤) − 𝑥)) < 𝑦)) → (𝑅 − 𝐿) ≠ 0)
14	9, 13	absrpcld 15492	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑥 ∈ ℂ) ∧ ∀𝑦 ∈ ℝ⁺ ∃𝑧 ∈ ℝ⁺ ∀𝑤 ∈ 𝐴 ((𝑤 ≠ 𝐵 ∧ (abs‘(𝑤 − 𝐵)) < 𝑧) → (abs‘((𝐹‘𝑤) − 𝑥)) < 𝑦)) → (abs‘(𝑅 − 𝐿)) ∈ ℝ⁺)
15		4re 12316	. . . . . . . . . . 11 ⊢ 4 ∈ ℝ
16		4pos 12342	. . . . . . . . . . 11 ⊢ 0 < 4
17	15, 16	elrpii 13010	. . . . . . . . . 10 ⊢ 4 ∈ ℝ⁺
18	17	a1i 11	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑥 ∈ ℂ) ∧ ∀𝑦 ∈ ℝ⁺ ∃𝑧 ∈ ℝ⁺ ∀𝑤 ∈ 𝐴 ((𝑤 ≠ 𝐵 ∧ (abs‘(𝑤 − 𝐵)) < 𝑧) → (abs‘((𝐹‘𝑤) − 𝑥)) < 𝑦)) → 4 ∈ ℝ⁺)
19	14, 18	rpdivcld 13068	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑥 ∈ ℂ) ∧ ∀𝑦 ∈ ℝ⁺ ∃𝑧 ∈ ℝ⁺ ∀𝑤 ∈ 𝐴 ((𝑤 ≠ 𝐵 ∧ (abs‘(𝑤 − 𝐵)) < 𝑧) → (abs‘((𝐹‘𝑤) − 𝑥)) < 𝑦)) → ((abs‘(𝑅 − 𝐿)) / 4) ∈ ℝ⁺)
20		nfv 1937	. . . . . . . . . . 11 ⊢ Ⅎ𝑦(𝜑 ∧ 𝑥 ∈ ℂ)
21		nfra1 3289	. . . . . . . . . . 11 ⊢ Ⅎ𝑦∀𝑦 ∈ ℝ⁺ ∃𝑧 ∈ ℝ⁺ ∀𝑤 ∈ 𝐴 ((𝑤 ≠ 𝐵 ∧ (abs‘(𝑤 − 𝐵)) < 𝑧) → (abs‘((𝐹‘𝑤) − 𝑥)) < 𝑦)
22	20, 21	nfan 1922	. . . . . . . . . 10 ⊢ Ⅎ𝑦((𝜑 ∧ 𝑥 ∈ ℂ) ∧ ∀𝑦 ∈ ℝ⁺ ∃𝑧 ∈ ℝ⁺ ∀𝑤 ∈ 𝐴 ((𝑤 ≠ 𝐵 ∧ (abs‘(𝑤 − 𝐵)) < 𝑧) → (abs‘((𝐹‘𝑤) − 𝑥)) < 𝑦))
23		nfv 1937	. . . . . . . . . 10 ⊢ Ⅎ𝑦(((abs‘(𝑅 − 𝐿)) / 4) ∈ ℝ⁺ → ∃𝑎 ∈ 𝐴 ∃𝑏 ∈ 𝐴 (abs‘(𝑅 − 𝐿)) < (4 · ((abs‘(𝑅 − 𝐿)) / 4)))
24	22, 23	nfim 1919	. . . . . . . . 9 ⊢ Ⅎ𝑦(((𝜑 ∧ 𝑥 ∈ ℂ) ∧ ∀𝑦 ∈ ℝ⁺ ∃𝑧 ∈ ℝ⁺ ∀𝑤 ∈ 𝐴 ((𝑤 ≠ 𝐵 ∧ (abs‘(𝑤 − 𝐵)) < 𝑧) → (abs‘((𝐹‘𝑤) − 𝑥)) < 𝑦)) → (((abs‘(𝑅 − 𝐿)) / 4) ∈ ℝ⁺ → ∃𝑎 ∈ 𝐴 ∃𝑏 ∈ 𝐴 (abs‘(𝑅 − 𝐿)) < (4 · ((abs‘(𝑅 − 𝐿)) / 4))))
25		ovex 7433	. . . . . . . . 9 ⊢ ((abs‘(𝑅 − 𝐿)) / 4) ∈ V
26		eleq1 2853	. . . . . . . . . . 11 ⊢ (𝑦 = ((abs‘(𝑅 − 𝐿)) / 4) → (𝑦 ∈ ℝ⁺ ↔ ((abs‘(𝑅 − 𝐿)) / 4) ∈ ℝ⁺))
27		oveq2 7408	. . . . . . . . . . . . 13 ⊢ (𝑦 = ((abs‘(𝑅 − 𝐿)) / 4) → (4 · 𝑦) = (4 · ((abs‘(𝑅 − 𝐿)) / 4)))
28	27	breq2d 5117	. . . . . . . . . . . 12 ⊢ (𝑦 = ((abs‘(𝑅 − 𝐿)) / 4) → ((abs‘(𝑅 − 𝐿)) < (4 · 𝑦) ↔ (abs‘(𝑅 − 𝐿)) < (4 · ((abs‘(𝑅 − 𝐿)) / 4))))
29	28	2rexbidv 3230	. . . . . . . . . . 11 ⊢ (𝑦 = ((abs‘(𝑅 − 𝐿)) / 4) → (∃𝑎 ∈ 𝐴 ∃𝑏 ∈ 𝐴 (abs‘(𝑅 − 𝐿)) < (4 · 𝑦) ↔ ∃𝑎 ∈ 𝐴 ∃𝑏 ∈ 𝐴 (abs‘(𝑅 − 𝐿)) < (4 · ((abs‘(𝑅 − 𝐿)) / 4))))
30	26, 29	imbi12d 347	. . . . . . . . . 10 ⊢ (𝑦 = ((abs‘(𝑅 − 𝐿)) / 4) → ((𝑦 ∈ ℝ⁺ → ∃𝑎 ∈ 𝐴 ∃𝑏 ∈ 𝐴 (abs‘(𝑅 − 𝐿)) < (4 · 𝑦)) ↔ (((abs‘(𝑅 − 𝐿)) / 4) ∈ ℝ⁺ → ∃𝑎 ∈ 𝐴 ∃𝑏 ∈ 𝐴 (abs‘(𝑅 − 𝐿)) < (4 · ((abs‘(𝑅 − 𝐿)) / 4)))))
31	30	imbi2d 343	. . . . . . . . 9 ⊢ (𝑦 = ((abs‘(𝑅 − 𝐿)) / 4) → ((((𝜑 ∧ 𝑥 ∈ ℂ) ∧ ∀𝑦 ∈ ℝ⁺ ∃𝑧 ∈ ℝ⁺ ∀𝑤 ∈ 𝐴 ((𝑤 ≠ 𝐵 ∧ (abs‘(𝑤 − 𝐵)) < 𝑧) → (abs‘((𝐹‘𝑤) − 𝑥)) < 𝑦)) → (𝑦 ∈ ℝ⁺ → ∃𝑎 ∈ 𝐴 ∃𝑏 ∈ 𝐴 (abs‘(𝑅 − 𝐿)) < (4 · 𝑦))) ↔ (((𝜑 ∧ 𝑥 ∈ ℂ) ∧ ∀𝑦 ∈ ℝ⁺ ∃𝑧 ∈ ℝ⁺ ∀𝑤 ∈ 𝐴 ((𝑤 ≠ 𝐵 ∧ (abs‘(𝑤 − 𝐵)) < 𝑧) → (abs‘((𝐹‘𝑤) − 𝑥)) < 𝑦)) → (((abs‘(𝑅 − 𝐿)) / 4) ∈ ℝ⁺ → ∃𝑎 ∈ 𝐴 ∃𝑏 ∈ 𝐴 (abs‘(𝑅 − 𝐿)) < (4 · ((abs‘(𝑅 − 𝐿)) / 4))))))
32		simpll 778	. . . . . . . . . . 11 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℂ) ∧ ∀𝑦 ∈ ℝ⁺ ∃𝑧 ∈ ℝ⁺ ∀𝑤 ∈ 𝐴 ((𝑤 ≠ 𝐵 ∧ (abs‘(𝑤 − 𝐵)) < 𝑧) → (abs‘((𝐹‘𝑤) − 𝑥)) < 𝑦)) ∧ 𝑦 ∈ ℝ⁺) → (𝜑 ∧ 𝑥 ∈ ℂ))
33		simpr 489	. . . . . . . . . . 11 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℂ) ∧ ∀𝑦 ∈ ℝ⁺ ∃𝑧 ∈ ℝ⁺ ∀𝑤 ∈ 𝐴 ((𝑤 ≠ 𝐵 ∧ (abs‘(𝑤 − 𝐵)) < 𝑧) → (abs‘((𝐹‘𝑤) − 𝑥)) < 𝑦)) ∧ 𝑦 ∈ ℝ⁺) → 𝑦 ∈ ℝ⁺)
34		rspa 3254	. . . . . . . . . . . 12 ⊢ ((∀𝑦 ∈ ℝ⁺ ∃𝑧 ∈ ℝ⁺ ∀𝑤 ∈ 𝐴 ((𝑤 ≠ 𝐵 ∧ (abs‘(𝑤 − 𝐵)) < 𝑧) → (abs‘((𝐹‘𝑤) − 𝑥)) < 𝑦) ∧ 𝑦 ∈ ℝ⁺) → ∃𝑧 ∈ ℝ⁺ ∀𝑤 ∈ 𝐴 ((𝑤 ≠ 𝐵 ∧ (abs‘(𝑤 − 𝐵)) < 𝑧) → (abs‘((𝐹‘𝑤) − 𝑥)) < 𝑦))
35	34	adantll 726	. . . . . . . . . . 11 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℂ) ∧ ∀𝑦 ∈ ℝ⁺ ∃𝑧 ∈ ℝ⁺ ∀𝑤 ∈ 𝐴 ((𝑤 ≠ 𝐵 ∧ (abs‘(𝑤 − 𝐵)) < 𝑧) → (abs‘((𝐹‘𝑤) − 𝑥)) < 𝑦)) ∧ 𝑦 ∈ ℝ⁺) → ∃𝑧 ∈ ℝ⁺ ∀𝑤 ∈ 𝐴 ((𝑤 ≠ 𝐵 ∧ (abs‘(𝑤 − 𝐵)) < 𝑧) → (abs‘((𝐹‘𝑤) − 𝑥)) < 𝑦))
36		limclner.f	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝜑 → 𝐹:𝐴⟶ℂ)
37		fresin 6737	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝐹:𝐴⟶ℂ → (𝐹 ↾ (𝐵(,)+∞)):(𝐴 ∩ (𝐵(,)+∞))⟶ℂ)
38	36, 37	syl 18	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝜑 → (𝐹 ↾ (𝐵(,)+∞)):(𝐴 ∩ (𝐵(,)+∞))⟶ℂ)
39		inss2 4192	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝐴 ∩ (𝐵(,)+∞)) ⊆ (𝐵(,)+∞)
40		ioosscn 13426	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝐵(,)+∞) ⊆ ℂ
41	39, 40	sstri 3948	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝐴 ∩ (𝐵(,)+∞)) ⊆ ℂ
42	41	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝜑 → (𝐴 ∩ (𝐵(,)+∞)) ⊆ ℂ)
43		limclner.j	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ 𝐽 = (topGen‘ran (,))
44		retop 24879	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (topGen‘ran (,)) ∈ Top
45	43, 44	eqeltri 2861	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ 𝐽 ∈ Top
46		inss2 4192	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (𝐴 ∩ (-∞(,)𝐵)) ⊆ (-∞(,)𝐵)
47		ioossre 13425	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (-∞(,)𝐵) ⊆ ℝ
48	46, 47	sstri 3948	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝐴 ∩ (-∞(,)𝐵)) ⊆ ℝ
49		uniretop 24880	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ ℝ = ∪ (topGen‘ran (,))
50	43	unieqi 4880	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ ∪ 𝐽 = ∪ (topGen‘ran (,))
51	49, 50	eqtr4i 2791	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ℝ = ∪ 𝐽
52	51	lpss 23260	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((𝐽 ∈ Top ∧ (𝐴 ∩ (-∞(,)𝐵)) ⊆ ℝ) → ((limPt‘𝐽)‘(𝐴 ∩ (-∞(,)𝐵))) ⊆ ℝ)
53	45, 48, 52	mp2an 704	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((limPt‘𝐽)‘(𝐴 ∩ (-∞(,)𝐵))) ⊆ ℝ
54		limclner.blp1	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝜑 → 𝐵 ∈ ((limPt‘𝐽)‘(𝐴 ∩ (-∞(,)𝐵))))
55	53, 54	sselid 3937	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝜑 → 𝐵 ∈ ℝ)
56	55	recnd 11225	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝜑 → 𝐵 ∈ ℂ)
57	38, 42, 56	ellimc3 25999	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝜑 → (𝑅 ∈ ((𝐹 ↾ (𝐵(,)+∞)) lim_ℂ 𝐵) ↔ (𝑅 ∈ ℂ ∧ ∀𝑦 ∈ ℝ⁺ ∃𝑣 ∈ ℝ⁺ ∀𝑤 ∈ (𝐴 ∩ (𝐵(,)+∞))((𝑤 ≠ 𝐵 ∧ (abs‘(𝑤 − 𝐵)) < 𝑣) → (abs‘(((𝐹 ↾ (𝐵(,)+∞))‘𝑤) − 𝑅)) < 𝑦))))
58	2, 57	mpbid 235	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝜑 → (𝑅 ∈ ℂ ∧ ∀𝑦 ∈ ℝ⁺ ∃𝑣 ∈ ℝ⁺ ∀𝑤 ∈ (𝐴 ∩ (𝐵(,)+∞))((𝑤 ≠ 𝐵 ∧ (abs‘(𝑤 − 𝐵)) < 𝑣) → (abs‘(((𝐹 ↾ (𝐵(,)+∞))‘𝑤) − 𝑅)) < 𝑦)))
59	58	simprd 500	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝜑 → ∀𝑦 ∈ ℝ⁺ ∃𝑣 ∈ ℝ⁺ ∀𝑤 ∈ (𝐴 ∩ (𝐵(,)+∞))((𝑤 ≠ 𝐵 ∧ (abs‘(𝑤 − 𝐵)) < 𝑣) → (abs‘(((𝐹 ↾ (𝐵(,)+∞))‘𝑤) − 𝑅)) < 𝑦))
60	59	r19.21bi 3257	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ 𝑦 ∈ ℝ⁺) → ∃𝑣 ∈ ℝ⁺ ∀𝑤 ∈ (𝐴 ∩ (𝐵(,)+∞))((𝑤 ≠ 𝐵 ∧ (abs‘(𝑤 − 𝐵)) < 𝑣) → (abs‘(((𝐹 ↾ (𝐵(,)+∞))‘𝑤) − 𝑅)) < 𝑦))
61	60	3ad2ant1 1149	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ 𝑦 ∈ ℝ⁺) ∧ 𝑧 ∈ ℝ⁺ ∧ ∀𝑤 ∈ 𝐴 ((𝑤 ≠ 𝐵 ∧ (abs‘(𝑤 − 𝐵)) < 𝑧) → (abs‘((𝐹‘𝑤) − 𝑥)) < 𝑦)) → ∃𝑣 ∈ ℝ⁺ ∀𝑤 ∈ (𝐴 ∩ (𝐵(,)+∞))((𝑤 ≠ 𝐵 ∧ (abs‘(𝑤 − 𝐵)) < 𝑣) → (abs‘(((𝐹 ↾ (𝐵(,)+∞))‘𝑤) − 𝑅)) < 𝑦))
62		simp11l 1301	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((((𝜑 ∧ 𝑦 ∈ ℝ⁺) ∧ 𝑧 ∈ ℝ⁺ ∧ ∀𝑤 ∈ 𝐴 ((𝑤 ≠ 𝐵 ∧ (abs‘(𝑤 − 𝐵)) < 𝑧) → (abs‘((𝐹‘𝑤) − 𝑥)) < 𝑦)) ∧ 𝑣 ∈ ℝ⁺ ∧ ∀𝑤 ∈ (𝐴 ∩ (𝐵(,)+∞))((𝑤 ≠ 𝐵 ∧ (abs‘(𝑤 − 𝐵)) < 𝑣) → (abs‘(((𝐹 ↾ (𝐵(,)+∞))‘𝑤) − 𝑅)) < 𝑦)) → 𝜑)
63		simp12 1221	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((((𝜑 ∧ 𝑦 ∈ ℝ⁺) ∧ 𝑧 ∈ ℝ⁺ ∧ ∀𝑤 ∈ 𝐴 ((𝑤 ≠ 𝐵 ∧ (abs‘(𝑤 − 𝐵)) < 𝑧) → (abs‘((𝐹‘𝑤) − 𝑥)) < 𝑦)) ∧ 𝑣 ∈ ℝ⁺ ∧ ∀𝑤 ∈ (𝐴 ∩ (𝐵(,)+∞))((𝑤 ≠ 𝐵 ∧ (abs‘(𝑤 − 𝐵)) < 𝑣) → (abs‘(((𝐹 ↾ (𝐵(,)+∞))‘𝑤) − 𝑅)) < 𝑦)) → 𝑧 ∈ ℝ⁺)
64		simp2 1153	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((((𝜑 ∧ 𝑦 ∈ ℝ⁺) ∧ 𝑧 ∈ ℝ⁺ ∧ ∀𝑤 ∈ 𝐴 ((𝑤 ≠ 𝐵 ∧ (abs‘(𝑤 − 𝐵)) < 𝑧) → (abs‘((𝐹‘𝑤) − 𝑥)) < 𝑦)) ∧ 𝑣 ∈ ℝ⁺ ∧ ∀𝑤 ∈ (𝐴 ∩ (𝐵(,)+∞))((𝑤 ≠ 𝐵 ∧ (abs‘(𝑤 − 𝐵)) < 𝑣) → (abs‘(((𝐹 ↾ (𝐵(,)+∞))‘𝑤) − 𝑅)) < 𝑦)) → 𝑣 ∈ ℝ⁺)
65		breq2 5109	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝑢 = if(𝑧 ≤ 𝑣, 𝑧, 𝑣) → ((abs‘(𝑏 − 𝐵)) < 𝑢 ↔ (abs‘(𝑏 − 𝐵)) < if(𝑧 ≤ 𝑣, 𝑧, 𝑣)))
66	65	rexbidv 3189	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑢 = if(𝑧 ≤ 𝑣, 𝑧, 𝑣) → (∃𝑏 ∈ ((𝐴 ∩ (𝐵(,)+∞)) ∖ {𝐵})(abs‘(𝑏 − 𝐵)) < 𝑢 ↔ ∃𝑏 ∈ ((𝐴 ∩ (𝐵(,)+∞)) ∖ {𝐵})(abs‘(𝑏 − 𝐵)) < if(𝑧 ≤ 𝑣, 𝑧, 𝑣)))
67		inss1 4191	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ (((limPt‘𝐾)‘(𝐴 ∩ (𝐵(,)+∞))) ∩ ℝ) ⊆ ((limPt‘𝐾)‘(𝐴 ∩ (𝐵(,)+∞)))
68	67	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (𝜑 → (((limPt‘𝐾)‘(𝐴 ∩ (𝐵(,)+∞))) ∩ ℝ) ⊆ ((limPt‘𝐾)‘(𝐴 ∩ (𝐵(,)+∞))))
69		limclner.k	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ 𝐾 = (TopOpen‘ℂ_fld)
70	69	cnfldtop 24901	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ 𝐾 ∈ Top
71	70	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ (𝜑 → 𝐾 ∈ Top)
72		ax-resscn 11145	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ ℝ ⊆ ℂ
73	72	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ (𝜑 → ℝ ⊆ ℂ)
74		ioossre 13425	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ (𝐵(,)+∞) ⊆ ℝ
75	39, 74	sstri 3948	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ (𝐴 ∩ (𝐵(,)+∞)) ⊆ ℝ
76	75	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ (𝜑 → (𝐴 ∩ (𝐵(,)+∞)) ⊆ ℝ)
77		unicntop 24903	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ ℂ = ∪ (TopOpen‘ℂ_fld)
78	69	unieqi 4880	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ ∪ 𝐾 = ∪ (TopOpen‘ℂ_fld)
79	77, 78	eqtr4i 2791	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ ℂ = ∪ 𝐾
80	69	tgioo2 24921	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ (topGen‘ran (,)) = (𝐾 ↾_t ℝ)
81	43, 80	eqtri 2788	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ 𝐽 = (𝐾 ↾_t ℝ)
82	79, 81	restlp 23301	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ ((𝐾 ∈ Top ∧ ℝ ⊆ ℂ ∧ (𝐴 ∩ (𝐵(,)+∞)) ⊆ ℝ) → ((limPt‘𝐽)‘(𝐴 ∩ (𝐵(,)+∞))) = (((limPt‘𝐾)‘(𝐴 ∩ (𝐵(,)+∞))) ∩ ℝ))
83	71, 73, 76, 82	syl3anc 1394	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (𝜑 → ((limPt‘𝐽)‘(𝐴 ∩ (𝐵(,)+∞))) = (((limPt‘𝐾)‘(𝐴 ∩ (𝐵(,)+∞))) ∩ ℝ))
84	69	eqcomi 2774	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ (TopOpen‘ℂ_fld) = 𝐾
85	84	fveq2i 6874	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ (limPt‘(TopOpen‘ℂ_fld)) = (limPt‘𝐾)
86	85	fveq1i 6872	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ ((limPt‘(TopOpen‘ℂ_fld))‘(𝐴 ∩ (𝐵(,)+∞))) = ((limPt‘𝐾)‘(𝐴 ∩ (𝐵(,)+∞)))
87	86	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (𝜑 → ((limPt‘(TopOpen‘ℂ_fld))‘(𝐴 ∩ (𝐵(,)+∞))) = ((limPt‘𝐾)‘(𝐴 ∩ (𝐵(,)+∞))))
88	68, 83, 87	3sstr4d 3994	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (𝜑 → ((limPt‘𝐽)‘(𝐴 ∩ (𝐵(,)+∞))) ⊆ ((limPt‘(TopOpen‘ℂ_fld))‘(𝐴 ∩ (𝐵(,)+∞))))
89		limclner.blp2	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (𝜑 → 𝐵 ∈ ((limPt‘𝐽)‘(𝐴 ∩ (𝐵(,)+∞))))
90	88, 89	sseldd 3940	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝜑 → 𝐵 ∈ ((limPt‘(TopOpen‘ℂ_fld))‘(𝐴 ∩ (𝐵(,)+∞))))
91	42, 56	islpcn 46211	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝜑 → (𝐵 ∈ ((limPt‘(TopOpen‘ℂ_fld))‘(𝐴 ∩ (𝐵(,)+∞))) ↔ ∀𝑢 ∈ ℝ⁺ ∃𝑏 ∈ ((𝐴 ∩ (𝐵(,)+∞)) ∖ {𝐵})(abs‘(𝑏 − 𝐵)) < 𝑢))
92	90, 91	mpbid 235	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝜑 → ∀𝑢 ∈ ℝ⁺ ∃𝑏 ∈ ((𝐴 ∩ (𝐵(,)+∞)) ∖ {𝐵})(abs‘(𝑏 − 𝐵)) < 𝑢)
93	92	3ad2ant1 1149	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((𝜑 ∧ 𝑧 ∈ ℝ⁺ ∧ 𝑣 ∈ ℝ⁺) → ∀𝑢 ∈ ℝ⁺ ∃𝑏 ∈ ((𝐴 ∩ (𝐵(,)+∞)) ∖ {𝐵})(abs‘(𝑏 − 𝐵)) < 𝑢)
94		ifcl 4529	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((𝑧 ∈ ℝ⁺ ∧ 𝑣 ∈ ℝ⁺) → if(𝑧 ≤ 𝑣, 𝑧, 𝑣) ∈ ℝ⁺)
95	94	3adant1 1146	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((𝜑 ∧ 𝑧 ∈ ℝ⁺ ∧ 𝑣 ∈ ℝ⁺) → if(𝑧 ≤ 𝑣, 𝑧, 𝑣) ∈ ℝ⁺)
96	66, 93, 95	rspcdva 3585	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝜑 ∧ 𝑧 ∈ ℝ⁺ ∧ 𝑣 ∈ ℝ⁺) → ∃𝑏 ∈ ((𝐴 ∩ (𝐵(,)+∞)) ∖ {𝐵})(abs‘(𝑏 − 𝐵)) < if(𝑧 ≤ 𝑣, 𝑧, 𝑣))
97		eldifi 4087	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝑏 ∈ ((𝐴 ∩ (𝐵(,)+∞)) ∖ {𝐵}) → 𝑏 ∈ (𝐴 ∩ (𝐵(,)+∞)))
98	75, 97	sselid 3937	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝑏 ∈ ((𝐴 ∩ (𝐵(,)+∞)) ∖ {𝐵}) → 𝑏 ∈ ℝ)
99	73	sselda 3939	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ ((𝜑 ∧ 𝑏 ∈ ℝ) → 𝑏 ∈ ℂ)
100	56	adantr 485	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ ((𝜑 ∧ 𝑏 ∈ ℝ) → 𝐵 ∈ ℂ)
101	99, 100	subcld 11557	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ ((𝜑 ∧ 𝑏 ∈ ℝ) → (𝑏 − 𝐵) ∈ ℂ)
102	101	abscld 15480	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ ((𝜑 ∧ 𝑏 ∈ ℝ) → (abs‘(𝑏 − 𝐵)) ∈ ℝ)
103	102	3ad2antl1 1202	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ (((𝜑 ∧ 𝑧 ∈ ℝ⁺ ∧ 𝑣 ∈ ℝ⁺) ∧ 𝑏 ∈ ℝ) → (abs‘(𝑏 − 𝐵)) ∈ ℝ)
104	103	adantr 485	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ ((((𝜑 ∧ 𝑧 ∈ ℝ⁺ ∧ 𝑣 ∈ ℝ⁺) ∧ 𝑏 ∈ ℝ) ∧ (abs‘(𝑏 − 𝐵)) < if(𝑧 ≤ 𝑣, 𝑧, 𝑣)) → (abs‘(𝑏 − 𝐵)) ∈ ℝ)
105	95	rpred 13051	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ ((𝜑 ∧ 𝑧 ∈ ℝ⁺ ∧ 𝑣 ∈ ℝ⁺) → if(𝑧 ≤ 𝑣, 𝑧, 𝑣) ∈ ℝ)
106	105	ad2antrr 738	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ ((((𝜑 ∧ 𝑧 ∈ ℝ⁺ ∧ 𝑣 ∈ ℝ⁺) ∧ 𝑏 ∈ ℝ) ∧ (abs‘(𝑏 − 𝐵)) < if(𝑧 ≤ 𝑣, 𝑧, 𝑣)) → if(𝑧 ≤ 𝑣, 𝑧, 𝑣) ∈ ℝ)
107		rpre 13016	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ (𝑧 ∈ ℝ⁺ → 𝑧 ∈ ℝ)
108	107	3ad2ant2 1150	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ ((𝜑 ∧ 𝑧 ∈ ℝ⁺ ∧ 𝑣 ∈ ℝ⁺) → 𝑧 ∈ ℝ)
109	108	ad2antrr 738	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ ((((𝜑 ∧ 𝑧 ∈ ℝ⁺ ∧ 𝑣 ∈ ℝ⁺) ∧ 𝑏 ∈ ℝ) ∧ (abs‘(𝑏 − 𝐵)) < if(𝑧 ≤ 𝑣, 𝑧, 𝑣)) → 𝑧 ∈ ℝ)
110		simpr 489	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ ((((𝜑 ∧ 𝑧 ∈ ℝ⁺ ∧ 𝑣 ∈ ℝ⁺) ∧ 𝑏 ∈ ℝ) ∧ (abs‘(𝑏 − 𝐵)) < if(𝑧 ≤ 𝑣, 𝑧, 𝑣)) → (abs‘(𝑏 − 𝐵)) < if(𝑧 ≤ 𝑣, 𝑧, 𝑣))
111		rpre 13016	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ (𝑣 ∈ ℝ⁺ → 𝑣 ∈ ℝ)
112		min1 13206	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ ((𝑧 ∈ ℝ ∧ 𝑣 ∈ ℝ) → if(𝑧 ≤ 𝑣, 𝑧, 𝑣) ≤ 𝑧)
113	107, 111, 112	syl2an 607	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ ((𝑧 ∈ ℝ⁺ ∧ 𝑣 ∈ ℝ⁺) → if(𝑧 ≤ 𝑣, 𝑧, 𝑣) ≤ 𝑧)
114	113	3adant1 1146	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ ((𝜑 ∧ 𝑧 ∈ ℝ⁺ ∧ 𝑣 ∈ ℝ⁺) → if(𝑧 ≤ 𝑣, 𝑧, 𝑣) ≤ 𝑧)
115	114	ad2antrr 738	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ ((((𝜑 ∧ 𝑧 ∈ ℝ⁺ ∧ 𝑣 ∈ ℝ⁺) ∧ 𝑏 ∈ ℝ) ∧ (abs‘(𝑏 − 𝐵)) < if(𝑧 ≤ 𝑣, 𝑧, 𝑣)) → if(𝑧 ≤ 𝑣, 𝑧, 𝑣) ≤ 𝑧)
116	104, 106, 109, 110, 115	ltletrd 11358	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ((((𝜑 ∧ 𝑧 ∈ ℝ⁺ ∧ 𝑣 ∈ ℝ⁺) ∧ 𝑏 ∈ ℝ) ∧ (abs‘(𝑏 − 𝐵)) < if(𝑧 ≤ 𝑣, 𝑧, 𝑣)) → (abs‘(𝑏 − 𝐵)) < 𝑧)
117	111	3ad2ant3 1151	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ ((𝜑 ∧ 𝑧 ∈ ℝ⁺ ∧ 𝑣 ∈ ℝ⁺) → 𝑣 ∈ ℝ)
118	117	ad2antrr 738	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ ((((𝜑 ∧ 𝑧 ∈ ℝ⁺ ∧ 𝑣 ∈ ℝ⁺) ∧ 𝑏 ∈ ℝ) ∧ (abs‘(𝑏 − 𝐵)) < if(𝑧 ≤ 𝑣, 𝑧, 𝑣)) → 𝑣 ∈ ℝ)
119	109, 118	min2d 46045	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ ((((𝜑 ∧ 𝑧 ∈ ℝ⁺ ∧ 𝑣 ∈ ℝ⁺) ∧ 𝑏 ∈ ℝ) ∧ (abs‘(𝑏 − 𝐵)) < if(𝑧 ≤ 𝑣, 𝑧, 𝑣)) → if(𝑧 ≤ 𝑣, 𝑧, 𝑣) ≤ 𝑣)
120	104, 106, 118, 110, 119	ltletrd 11358	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ((((𝜑 ∧ 𝑧 ∈ ℝ⁺ ∧ 𝑣 ∈ ℝ⁺) ∧ 𝑏 ∈ ℝ) ∧ (abs‘(𝑏 − 𝐵)) < if(𝑧 ≤ 𝑣, 𝑧, 𝑣)) → (abs‘(𝑏 − 𝐵)) < 𝑣)
121	116, 120	jca 520	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((((𝜑 ∧ 𝑧 ∈ ℝ⁺ ∧ 𝑣 ∈ ℝ⁺) ∧ 𝑏 ∈ ℝ) ∧ (abs‘(𝑏 − 𝐵)) < if(𝑧 ≤ 𝑣, 𝑧, 𝑣)) → ((abs‘(𝑏 − 𝐵)) < 𝑧 ∧ (abs‘(𝑏 − 𝐵)) < 𝑣))
122	121	ex 417	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (((𝜑 ∧ 𝑧 ∈ ℝ⁺ ∧ 𝑣 ∈ ℝ⁺) ∧ 𝑏 ∈ ℝ) → ((abs‘(𝑏 − 𝐵)) < if(𝑧 ≤ 𝑣, 𝑧, 𝑣) → ((abs‘(𝑏 − 𝐵)) < 𝑧 ∧ (abs‘(𝑏 − 𝐵)) < 𝑣)))
123	98, 122	sylan2 604	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((𝜑 ∧ 𝑧 ∈ ℝ⁺ ∧ 𝑣 ∈ ℝ⁺) ∧ 𝑏 ∈ ((𝐴 ∩ (𝐵(,)+∞)) ∖ {𝐵})) → ((abs‘(𝑏 − 𝐵)) < if(𝑧 ≤ 𝑣, 𝑧, 𝑣) → ((abs‘(𝑏 − 𝐵)) < 𝑧 ∧ (abs‘(𝑏 − 𝐵)) < 𝑣)))
124	123	reximdva 3178	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝜑 ∧ 𝑧 ∈ ℝ⁺ ∧ 𝑣 ∈ ℝ⁺) → (∃𝑏 ∈ ((𝐴 ∩ (𝐵(,)+∞)) ∖ {𝐵})(abs‘(𝑏 − 𝐵)) < if(𝑧 ≤ 𝑣, 𝑧, 𝑣) → ∃𝑏 ∈ ((𝐴 ∩ (𝐵(,)+∞)) ∖ {𝐵})((abs‘(𝑏 − 𝐵)) < 𝑧 ∧ (abs‘(𝑏 − 𝐵)) < 𝑣)))
125	96, 124	mpd 16	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝜑 ∧ 𝑧 ∈ ℝ⁺ ∧ 𝑣 ∈ ℝ⁺) → ∃𝑏 ∈ ((𝐴 ∩ (𝐵(,)+∞)) ∖ {𝐵})((abs‘(𝑏 − 𝐵)) < 𝑧 ∧ (abs‘(𝑏 − 𝐵)) < 𝑣))
126	62, 63, 64, 125	syl3anc 1394	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((𝜑 ∧ 𝑦 ∈ ℝ⁺) ∧ 𝑧 ∈ ℝ⁺ ∧ ∀𝑤 ∈ 𝐴 ((𝑤 ≠ 𝐵 ∧ (abs‘(𝑤 − 𝐵)) < 𝑧) → (abs‘((𝐹‘𝑤) − 𝑥)) < 𝑦)) ∧ 𝑣 ∈ ℝ⁺ ∧ ∀𝑤 ∈ (𝐴 ∩ (𝐵(,)+∞))((𝑤 ≠ 𝐵 ∧ (abs‘(𝑤 − 𝐵)) < 𝑣) → (abs‘(((𝐹 ↾ (𝐵(,)+∞))‘𝑤) − 𝑅)) < 𝑦)) → ∃𝑏 ∈ ((𝐴 ∩ (𝐵(,)+∞)) ∖ {𝐵})((abs‘(𝑏 − 𝐵)) < 𝑧 ∧ (abs‘(𝑏 − 𝐵)) < 𝑣))
127		nfv 1937	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ Ⅎ𝑏(((𝜑 ∧ 𝑦 ∈ ℝ⁺) ∧ 𝑧 ∈ ℝ⁺ ∧ ∀𝑤 ∈ 𝐴 ((𝑤 ≠ 𝐵 ∧ (abs‘(𝑤 − 𝐵)) < 𝑧) → (abs‘((𝐹‘𝑤) − 𝑥)) < 𝑦)) ∧ 𝑣 ∈ ℝ⁺ ∧ ∀𝑤 ∈ (𝐴 ∩ (𝐵(,)+∞))((𝑤 ≠ 𝐵 ∧ (abs‘(𝑤 − 𝐵)) < 𝑣) → (abs‘(((𝐹 ↾ (𝐵(,)+∞))‘𝑤) − 𝑅)) < 𝑦))
128		nfre1 3290	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ Ⅎ𝑏∃𝑏 ∈ 𝐴 ((abs‘((𝐹‘𝑏) − 𝑥)) < 𝑦 ∧ (abs‘((𝐹‘𝑏) − 𝑅)) < 𝑦)
129	97	elin1d 4159	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝑏 ∈ ((𝐴 ∩ (𝐵(,)+∞)) ∖ {𝐵}) → 𝑏 ∈ 𝐴)
130	129	3ad2ant2 1150	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((((𝜑 ∧ 𝑦 ∈ ℝ⁺) ∧ 𝑧 ∈ ℝ⁺ ∧ ∀𝑤 ∈ 𝐴 ((𝑤 ≠ 𝐵 ∧ (abs‘(𝑤 − 𝐵)) < 𝑧) → (abs‘((𝐹‘𝑤) − 𝑥)) < 𝑦)) ∧ 𝑣 ∈ ℝ⁺ ∧ ∀𝑤 ∈ (𝐴 ∩ (𝐵(,)+∞))((𝑤 ≠ 𝐵 ∧ (abs‘(𝑤 − 𝐵)) < 𝑣) → (abs‘(((𝐹 ↾ (𝐵(,)+∞))‘𝑤) − 𝑅)) < 𝑦)) ∧ 𝑏 ∈ ((𝐴 ∩ (𝐵(,)+∞)) ∖ {𝐵}) ∧ ((abs‘(𝑏 − 𝐵)) < 𝑧 ∧ (abs‘(𝑏 − 𝐵)) < 𝑣)) → 𝑏 ∈ 𝐴)
131		simp113 1321	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (((((𝜑 ∧ 𝑦 ∈ ℝ⁺) ∧ 𝑧 ∈ ℝ⁺ ∧ ∀𝑤 ∈ 𝐴 ((𝑤 ≠ 𝐵 ∧ (abs‘(𝑤 − 𝐵)) < 𝑧) → (abs‘((𝐹‘𝑤) − 𝑥)) < 𝑦)) ∧ 𝑣 ∈ ℝ⁺ ∧ ∀𝑤 ∈ (𝐴 ∩ (𝐵(,)+∞))((𝑤 ≠ 𝐵 ∧ (abs‘(𝑤 − 𝐵)) < 𝑣) → (abs‘(((𝐹 ↾ (𝐵(,)+∞))‘𝑤) − 𝑅)) < 𝑦)) ∧ 𝑏 ∈ ((𝐴 ∩ (𝐵(,)+∞)) ∖ {𝐵}) ∧ ((abs‘(𝑏 − 𝐵)) < 𝑧 ∧ (abs‘(𝑏 − 𝐵)) < 𝑣)) → ∀𝑤 ∈ 𝐴 ((𝑤 ≠ 𝐵 ∧ (abs‘(𝑤 − 𝐵)) < 𝑧) → (abs‘((𝐹‘𝑤) − 𝑥)) < 𝑦))
132		eldifsni 4753	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (𝑏 ∈ ((𝐴 ∩ (𝐵(,)+∞)) ∖ {𝐵}) → 𝑏 ≠ 𝐵)
133	132	adantr 485	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ((𝑏 ∈ ((𝐴 ∩ (𝐵(,)+∞)) ∖ {𝐵}) ∧ ((abs‘(𝑏 − 𝐵)) < 𝑧 ∧ (abs‘(𝑏 − 𝐵)) < 𝑣)) → 𝑏 ≠ 𝐵)
134		simprl 782	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ((𝑏 ∈ ((𝐴 ∩ (𝐵(,)+∞)) ∖ {𝐵}) ∧ ((abs‘(𝑏 − 𝐵)) < 𝑧 ∧ (abs‘(𝑏 − 𝐵)) < 𝑣)) → (abs‘(𝑏 − 𝐵)) < 𝑧)
135	133, 134	jca 520	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((𝑏 ∈ ((𝐴 ∩ (𝐵(,)+∞)) ∖ {𝐵}) ∧ ((abs‘(𝑏 − 𝐵)) < 𝑧 ∧ (abs‘(𝑏 − 𝐵)) < 𝑣)) → (𝑏 ≠ 𝐵 ∧ (abs‘(𝑏 − 𝐵)) < 𝑧))
136	135	3adant1 1146	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (((((𝜑 ∧ 𝑦 ∈ ℝ⁺) ∧ 𝑧 ∈ ℝ⁺ ∧ ∀𝑤 ∈ 𝐴 ((𝑤 ≠ 𝐵 ∧ (abs‘(𝑤 − 𝐵)) < 𝑧) → (abs‘((𝐹‘𝑤) − 𝑥)) < 𝑦)) ∧ 𝑣 ∈ ℝ⁺ ∧ ∀𝑤 ∈ (𝐴 ∩ (𝐵(,)+∞))((𝑤 ≠ 𝐵 ∧ (abs‘(𝑤 − 𝐵)) < 𝑣) → (abs‘(((𝐹 ↾ (𝐵(,)+∞))‘𝑤) − 𝑅)) < 𝑦)) ∧ 𝑏 ∈ ((𝐴 ∩ (𝐵(,)+∞)) ∖ {𝐵}) ∧ ((abs‘(𝑏 − 𝐵)) < 𝑧 ∧ (abs‘(𝑏 − 𝐵)) < 𝑣)) → (𝑏 ≠ 𝐵 ∧ (abs‘(𝑏 − 𝐵)) < 𝑧))
137		neeq1 3022	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ (𝑤 = 𝑏 → (𝑤 ≠ 𝐵 ↔ 𝑏 ≠ 𝐵))
138		fvoveq1 7423	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ (𝑤 = 𝑏 → (abs‘(𝑤 − 𝐵)) = (abs‘(𝑏 − 𝐵)))
139	138	breq1d 5115	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ (𝑤 = 𝑏 → ((abs‘(𝑤 − 𝐵)) < 𝑧 ↔ (abs‘(𝑏 − 𝐵)) < 𝑧))
140	137, 139	anbi12d 643	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (𝑤 = 𝑏 → ((𝑤 ≠ 𝐵 ∧ (abs‘(𝑤 − 𝐵)) < 𝑧) ↔ (𝑏 ≠ 𝐵 ∧ (abs‘(𝑏 − 𝐵)) < 𝑧)))
141	140	imbrov2fvoveq 7425	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (𝑤 = 𝑏 → (((𝑤 ≠ 𝐵 ∧ (abs‘(𝑤 − 𝐵)) < 𝑧) → (abs‘((𝐹‘𝑤) − 𝑥)) < 𝑦) ↔ ((𝑏 ≠ 𝐵 ∧ (abs‘(𝑏 − 𝐵)) < 𝑧) → (abs‘((𝐹‘𝑏) − 𝑥)) < 𝑦)))
142	141	rspcva 3582	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((𝑏 ∈ 𝐴 ∧ ∀𝑤 ∈ 𝐴 ((𝑤 ≠ 𝐵 ∧ (abs‘(𝑤 − 𝐵)) < 𝑧) → (abs‘((𝐹‘𝑤) − 𝑥)) < 𝑦)) → ((𝑏 ≠ 𝐵 ∧ (abs‘(𝑏 − 𝐵)) < 𝑧) → (abs‘((𝐹‘𝑏) − 𝑥)) < 𝑦))
143	142	imp 411	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (((𝑏 ∈ 𝐴 ∧ ∀𝑤 ∈ 𝐴 ((𝑤 ≠ 𝐵 ∧ (abs‘(𝑤 − 𝐵)) < 𝑧) → (abs‘((𝐹‘𝑤) − 𝑥)) < 𝑦)) ∧ (𝑏 ≠ 𝐵 ∧ (abs‘(𝑏 − 𝐵)) < 𝑧)) → (abs‘((𝐹‘𝑏) − 𝑥)) < 𝑦)
144	130, 131, 136, 143	syl21anc 850	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((((𝜑 ∧ 𝑦 ∈ ℝ⁺) ∧ 𝑧 ∈ ℝ⁺ ∧ ∀𝑤 ∈ 𝐴 ((𝑤 ≠ 𝐵 ∧ (abs‘(𝑤 − 𝐵)) < 𝑧) → (abs‘((𝐹‘𝑤) − 𝑥)) < 𝑦)) ∧ 𝑣 ∈ ℝ⁺ ∧ ∀𝑤 ∈ (𝐴 ∩ (𝐵(,)+∞))((𝑤 ≠ 𝐵 ∧ (abs‘(𝑤 − 𝐵)) < 𝑣) → (abs‘(((𝐹 ↾ (𝐵(,)+∞))‘𝑤) − 𝑅)) < 𝑦)) ∧ 𝑏 ∈ ((𝐴 ∩ (𝐵(,)+∞)) ∖ {𝐵}) ∧ ((abs‘(𝑏 − 𝐵)) < 𝑧 ∧ (abs‘(𝑏 − 𝐵)) < 𝑣)) → (abs‘((𝐹‘𝑏) − 𝑥)) < 𝑦)
145	97	3ad2ant2 1150	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (((((𝜑 ∧ 𝑦 ∈ ℝ⁺) ∧ 𝑧 ∈ ℝ⁺ ∧ ∀𝑤 ∈ 𝐴 ((𝑤 ≠ 𝐵 ∧ (abs‘(𝑤 − 𝐵)) < 𝑧) → (abs‘((𝐹‘𝑤) − 𝑥)) < 𝑦)) ∧ 𝑣 ∈ ℝ⁺ ∧ ∀𝑤 ∈ (𝐴 ∩ (𝐵(,)+∞))((𝑤 ≠ 𝐵 ∧ (abs‘(𝑤 − 𝐵)) < 𝑣) → (abs‘(((𝐹 ↾ (𝐵(,)+∞))‘𝑤) − 𝑅)) < 𝑦)) ∧ 𝑏 ∈ ((𝐴 ∩ (𝐵(,)+∞)) ∖ {𝐵}) ∧ ((abs‘(𝑏 − 𝐵)) < 𝑧 ∧ (abs‘(𝑏 − 𝐵)) < 𝑣)) → 𝑏 ∈ (𝐴 ∩ (𝐵(,)+∞)))
146	62	3ad2ant1 1149	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (((((𝜑 ∧ 𝑦 ∈ ℝ⁺) ∧ 𝑧 ∈ ℝ⁺ ∧ ∀𝑤 ∈ 𝐴 ((𝑤 ≠ 𝐵 ∧ (abs‘(𝑤 − 𝐵)) < 𝑧) → (abs‘((𝐹‘𝑤) − 𝑥)) < 𝑦)) ∧ 𝑣 ∈ ℝ⁺ ∧ ∀𝑤 ∈ (𝐴 ∩ (𝐵(,)+∞))((𝑤 ≠ 𝐵 ∧ (abs‘(𝑤 − 𝐵)) < 𝑣) → (abs‘(((𝐹 ↾ (𝐵(,)+∞))‘𝑤) − 𝑅)) < 𝑦)) ∧ 𝑏 ∈ ((𝐴 ∩ (𝐵(,)+∞)) ∖ {𝐵}) ∧ ((abs‘(𝑏 − 𝐵)) < 𝑧 ∧ (abs‘(𝑏 − 𝐵)) < 𝑣)) → 𝜑)
147		simp13 1222	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (((((𝜑 ∧ 𝑦 ∈ ℝ⁺) ∧ 𝑧 ∈ ℝ⁺ ∧ ∀𝑤 ∈ 𝐴 ((𝑤 ≠ 𝐵 ∧ (abs‘(𝑤 − 𝐵)) < 𝑧) → (abs‘((𝐹‘𝑤) − 𝑥)) < 𝑦)) ∧ 𝑣 ∈ ℝ⁺ ∧ ∀𝑤 ∈ (𝐴 ∩ (𝐵(,)+∞))((𝑤 ≠ 𝐵 ∧ (abs‘(𝑤 − 𝐵)) < 𝑣) → (abs‘(((𝐹 ↾ (𝐵(,)+∞))‘𝑤) − 𝑅)) < 𝑦)) ∧ 𝑏 ∈ ((𝐴 ∩ (𝐵(,)+∞)) ∖ {𝐵}) ∧ ((abs‘(𝑏 − 𝐵)) < 𝑧 ∧ (abs‘(𝑏 − 𝐵)) < 𝑣)) → ∀𝑤 ∈ (𝐴 ∩ (𝐵(,)+∞))((𝑤 ≠ 𝐵 ∧ (abs‘(𝑤 − 𝐵)) < 𝑣) → (abs‘(((𝐹 ↾ (𝐵(,)+∞))‘𝑤) − 𝑅)) < 𝑦))
148		nfv 1937	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ Ⅎ𝑤𝜑
149		nfra1 3289	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ Ⅎ𝑤∀𝑤 ∈ (𝐴 ∩ (𝐵(,)+∞))((𝑤 ≠ 𝐵 ∧ (abs‘(𝑤 − 𝐵)) < 𝑣) → (abs‘(((𝐹 ↾ (𝐵(,)+∞))‘𝑤) − 𝑅)) < 𝑦)
150	148, 149	nfan 1922	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ Ⅎ𝑤(𝜑 ∧ ∀𝑤 ∈ (𝐴 ∩ (𝐵(,)+∞))((𝑤 ≠ 𝐵 ∧ (abs‘(𝑤 − 𝐵)) < 𝑣) → (abs‘(((𝐹 ↾ (𝐵(,)+∞))‘𝑤) − 𝑅)) < 𝑦))
151		elinel2 4157	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ (𝑤 ∈ (𝐴 ∩ (𝐵(,)+∞)) → 𝑤 ∈ (𝐵(,)+∞))
152	151	fvresd 6891	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ (𝑤 ∈ (𝐴 ∩ (𝐵(,)+∞)) → ((𝐹 ↾ (𝐵(,)+∞))‘𝑤) = (𝐹‘𝑤))
153	152	eqcomd 2771	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ (𝑤 ∈ (𝐴 ∩ (𝐵(,)+∞)) → (𝐹‘𝑤) = ((𝐹 ↾ (𝐵(,)+∞))‘𝑤))
154	153	fvoveq1d 7422	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ (𝑤 ∈ (𝐴 ∩ (𝐵(,)+∞)) → (abs‘((𝐹‘𝑤) − 𝑅)) = (abs‘(((𝐹 ↾ (𝐵(,)+∞))‘𝑤) − 𝑅)))
155	154	3ad2ant2 1150	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ (((𝜑 ∧ ∀𝑤 ∈ (𝐴 ∩ (𝐵(,)+∞))((𝑤 ≠ 𝐵 ∧ (abs‘(𝑤 − 𝐵)) < 𝑣) → (abs‘(((𝐹 ↾ (𝐵(,)+∞))‘𝑤) − 𝑅)) < 𝑦)) ∧ 𝑤 ∈ (𝐴 ∩ (𝐵(,)+∞)) ∧ (𝑤 ≠ 𝐵 ∧ (abs‘(𝑤 − 𝐵)) < 𝑣)) → (abs‘((𝐹‘𝑤) − 𝑅)) = (abs‘(((𝐹 ↾ (𝐵(,)+∞))‘𝑤) − 𝑅)))
156		rspa 3254	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ ((∀𝑤 ∈ (𝐴 ∩ (𝐵(,)+∞))((𝑤 ≠ 𝐵 ∧ (abs‘(𝑤 − 𝐵)) < 𝑣) → (abs‘(((𝐹 ↾ (𝐵(,)+∞))‘𝑤) − 𝑅)) < 𝑦) ∧ 𝑤 ∈ (𝐴 ∩ (𝐵(,)+∞))) → ((𝑤 ≠ 𝐵 ∧ (abs‘(𝑤 − 𝐵)) < 𝑣) → (abs‘(((𝐹 ↾ (𝐵(,)+∞))‘𝑤) − 𝑅)) < 𝑦))
157	156	3impia 1133	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ ((∀𝑤 ∈ (𝐴 ∩ (𝐵(,)+∞))((𝑤 ≠ 𝐵 ∧ (abs‘(𝑤 − 𝐵)) < 𝑣) → (abs‘(((𝐹 ↾ (𝐵(,)+∞))‘𝑤) − 𝑅)) < 𝑦) ∧ 𝑤 ∈ (𝐴 ∩ (𝐵(,)+∞)) ∧ (𝑤 ≠ 𝐵 ∧ (abs‘(𝑤 − 𝐵)) < 𝑣)) → (abs‘(((𝐹 ↾ (𝐵(,)+∞))‘𝑤) − 𝑅)) < 𝑦)
158	157	3adant1l 1193	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ (((𝜑 ∧ ∀𝑤 ∈ (𝐴 ∩ (𝐵(,)+∞))((𝑤 ≠ 𝐵 ∧ (abs‘(𝑤 − 𝐵)) < 𝑣) → (abs‘(((𝐹 ↾ (𝐵(,)+∞))‘𝑤) − 𝑅)) < 𝑦)) ∧ 𝑤 ∈ (𝐴 ∩ (𝐵(,)+∞)) ∧ (𝑤 ≠ 𝐵 ∧ (abs‘(𝑤 − 𝐵)) < 𝑣)) → (abs‘(((𝐹 ↾ (𝐵(,)+∞))‘𝑤) − 𝑅)) < 𝑦)
159	155, 158	eqbrtrd 5127	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (((𝜑 ∧ ∀𝑤 ∈ (𝐴 ∩ (𝐵(,)+∞))((𝑤 ≠ 𝐵 ∧ (abs‘(𝑤 − 𝐵)) < 𝑣) → (abs‘(((𝐹 ↾ (𝐵(,)+∞))‘𝑤) − 𝑅)) < 𝑦)) ∧ 𝑤 ∈ (𝐴 ∩ (𝐵(,)+∞)) ∧ (𝑤 ≠ 𝐵 ∧ (abs‘(𝑤 − 𝐵)) < 𝑣)) → (abs‘((𝐹‘𝑤) − 𝑅)) < 𝑦)
160	159	3exp 1135	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ((𝜑 ∧ ∀𝑤 ∈ (𝐴 ∩ (𝐵(,)+∞))((𝑤 ≠ 𝐵 ∧ (abs‘(𝑤 − 𝐵)) < 𝑣) → (abs‘(((𝐹 ↾ (𝐵(,)+∞))‘𝑤) − 𝑅)) < 𝑦)) → (𝑤 ∈ (𝐴 ∩ (𝐵(,)+∞)) → ((𝑤 ≠ 𝐵 ∧ (abs‘(𝑤 − 𝐵)) < 𝑣) → (abs‘((𝐹‘𝑤) − 𝑅)) < 𝑦)))
161	150, 160	ralrimi 3263	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((𝜑 ∧ ∀𝑤 ∈ (𝐴 ∩ (𝐵(,)+∞))((𝑤 ≠ 𝐵 ∧ (abs‘(𝑤 − 𝐵)) < 𝑣) → (abs‘(((𝐹 ↾ (𝐵(,)+∞))‘𝑤) − 𝑅)) < 𝑦)) → ∀𝑤 ∈ (𝐴 ∩ (𝐵(,)+∞))((𝑤 ≠ 𝐵 ∧ (abs‘(𝑤 − 𝐵)) < 𝑣) → (abs‘((𝐹‘𝑤) − 𝑅)) < 𝑦))
162	146, 147, 161	syl2anc 595	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (((((𝜑 ∧ 𝑦 ∈ ℝ⁺) ∧ 𝑧 ∈ ℝ⁺ ∧ ∀𝑤 ∈ 𝐴 ((𝑤 ≠ 𝐵 ∧ (abs‘(𝑤 − 𝐵)) < 𝑧) → (abs‘((𝐹‘𝑤) − 𝑥)) < 𝑦)) ∧ 𝑣 ∈ ℝ⁺ ∧ ∀𝑤 ∈ (𝐴 ∩ (𝐵(,)+∞))((𝑤 ≠ 𝐵 ∧ (abs‘(𝑤 − 𝐵)) < 𝑣) → (abs‘(((𝐹 ↾ (𝐵(,)+∞))‘𝑤) − 𝑅)) < 𝑦)) ∧ 𝑏 ∈ ((𝐴 ∩ (𝐵(,)+∞)) ∖ {𝐵}) ∧ ((abs‘(𝑏 − 𝐵)) < 𝑧 ∧ (abs‘(𝑏 − 𝐵)) < 𝑣)) → ∀𝑤 ∈ (𝐴 ∩ (𝐵(,)+∞))((𝑤 ≠ 𝐵 ∧ (abs‘(𝑤 − 𝐵)) < 𝑣) → (abs‘((𝐹‘𝑤) − 𝑅)) < 𝑦))
163	132	anim1i 626	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ((𝑏 ∈ ((𝐴 ∩ (𝐵(,)+∞)) ∖ {𝐵}) ∧ (abs‘(𝑏 − 𝐵)) < 𝑣) → (𝑏 ≠ 𝐵 ∧ (abs‘(𝑏 − 𝐵)) < 𝑣))
164	163	adantrl 728	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((𝑏 ∈ ((𝐴 ∩ (𝐵(,)+∞)) ∖ {𝐵}) ∧ ((abs‘(𝑏 − 𝐵)) < 𝑧 ∧ (abs‘(𝑏 − 𝐵)) < 𝑣)) → (𝑏 ≠ 𝐵 ∧ (abs‘(𝑏 − 𝐵)) < 𝑣))
165	164	3adant1 1146	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (((((𝜑 ∧ 𝑦 ∈ ℝ⁺) ∧ 𝑧 ∈ ℝ⁺ ∧ ∀𝑤 ∈ 𝐴 ((𝑤 ≠ 𝐵 ∧ (abs‘(𝑤 − 𝐵)) < 𝑧) → (abs‘((𝐹‘𝑤) − 𝑥)) < 𝑦)) ∧ 𝑣 ∈ ℝ⁺ ∧ ∀𝑤 ∈ (𝐴 ∩ (𝐵(,)+∞))((𝑤 ≠ 𝐵 ∧ (abs‘(𝑤 − 𝐵)) < 𝑣) → (abs‘(((𝐹 ↾ (𝐵(,)+∞))‘𝑤) − 𝑅)) < 𝑦)) ∧ 𝑏 ∈ ((𝐴 ∩ (𝐵(,)+∞)) ∖ {𝐵}) ∧ ((abs‘(𝑏 − 𝐵)) < 𝑧 ∧ (abs‘(𝑏 − 𝐵)) < 𝑣)) → (𝑏 ≠ 𝐵 ∧ (abs‘(𝑏 − 𝐵)) < 𝑣))
166	138	breq1d 5115	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ (𝑤 = 𝑏 → ((abs‘(𝑤 − 𝐵)) < 𝑣 ↔ (abs‘(𝑏 − 𝐵)) < 𝑣))
167	137, 166	anbi12d 643	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (𝑤 = 𝑏 → ((𝑤 ≠ 𝐵 ∧ (abs‘(𝑤 − 𝐵)) < 𝑣) ↔ (𝑏 ≠ 𝐵 ∧ (abs‘(𝑏 − 𝐵)) < 𝑣)))
168	167	imbrov2fvoveq 7425	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (𝑤 = 𝑏 → (((𝑤 ≠ 𝐵 ∧ (abs‘(𝑤 − 𝐵)) < 𝑣) → (abs‘((𝐹‘𝑤) − 𝑅)) < 𝑦) ↔ ((𝑏 ≠ 𝐵 ∧ (abs‘(𝑏 − 𝐵)) < 𝑣) → (abs‘((𝐹‘𝑏) − 𝑅)) < 𝑦)))
169	168	rspcva 3582	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((𝑏 ∈ (𝐴 ∩ (𝐵(,)+∞)) ∧ ∀𝑤 ∈ (𝐴 ∩ (𝐵(,)+∞))((𝑤 ≠ 𝐵 ∧ (abs‘(𝑤 − 𝐵)) < 𝑣) → (abs‘((𝐹‘𝑤) − 𝑅)) < 𝑦)) → ((𝑏 ≠ 𝐵 ∧ (abs‘(𝑏 − 𝐵)) < 𝑣) → (abs‘((𝐹‘𝑏) − 𝑅)) < 𝑦))
170	169	imp 411	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (((𝑏 ∈ (𝐴 ∩ (𝐵(,)+∞)) ∧ ∀𝑤 ∈ (𝐴 ∩ (𝐵(,)+∞))((𝑤 ≠ 𝐵 ∧ (abs‘(𝑤 − 𝐵)) < 𝑣) → (abs‘((𝐹‘𝑤) − 𝑅)) < 𝑦)) ∧ (𝑏 ≠ 𝐵 ∧ (abs‘(𝑏 − 𝐵)) < 𝑣)) → (abs‘((𝐹‘𝑏) − 𝑅)) < 𝑦)
171	145, 162, 165, 170	syl21anc 850	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((((𝜑 ∧ 𝑦 ∈ ℝ⁺) ∧ 𝑧 ∈ ℝ⁺ ∧ ∀𝑤 ∈ 𝐴 ((𝑤 ≠ 𝐵 ∧ (abs‘(𝑤 − 𝐵)) < 𝑧) → (abs‘((𝐹‘𝑤) − 𝑥)) < 𝑦)) ∧ 𝑣 ∈ ℝ⁺ ∧ ∀𝑤 ∈ (𝐴 ∩ (𝐵(,)+∞))((𝑤 ≠ 𝐵 ∧ (abs‘(𝑤 − 𝐵)) < 𝑣) → (abs‘(((𝐹 ↾ (𝐵(,)+∞))‘𝑤) − 𝑅)) < 𝑦)) ∧ 𝑏 ∈ ((𝐴 ∩ (𝐵(,)+∞)) ∖ {𝐵}) ∧ ((abs‘(𝑏 − 𝐵)) < 𝑧 ∧ (abs‘(𝑏 − 𝐵)) < 𝑣)) → (abs‘((𝐹‘𝑏) − 𝑅)) < 𝑦)
172		rspe 3255	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((𝑏 ∈ 𝐴 ∧ ((abs‘((𝐹‘𝑏) − 𝑥)) < 𝑦 ∧ (abs‘((𝐹‘𝑏) − 𝑅)) < 𝑦)) → ∃𝑏 ∈ 𝐴 ((abs‘((𝐹‘𝑏) − 𝑥)) < 𝑦 ∧ (abs‘((𝐹‘𝑏) − 𝑅)) < 𝑦))
173	130, 144, 171, 172	syl12anc 849	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((((𝜑 ∧ 𝑦 ∈ ℝ⁺) ∧ 𝑧 ∈ ℝ⁺ ∧ ∀𝑤 ∈ 𝐴 ((𝑤 ≠ 𝐵 ∧ (abs‘(𝑤 − 𝐵)) < 𝑧) → (abs‘((𝐹‘𝑤) − 𝑥)) < 𝑦)) ∧ 𝑣 ∈ ℝ⁺ ∧ ∀𝑤 ∈ (𝐴 ∩ (𝐵(,)+∞))((𝑤 ≠ 𝐵 ∧ (abs‘(𝑤 − 𝐵)) < 𝑣) → (abs‘(((𝐹 ↾ (𝐵(,)+∞))‘𝑤) − 𝑅)) < 𝑦)) ∧ 𝑏 ∈ ((𝐴 ∩ (𝐵(,)+∞)) ∖ {𝐵}) ∧ ((abs‘(𝑏 − 𝐵)) < 𝑧 ∧ (abs‘(𝑏 − 𝐵)) < 𝑣)) → ∃𝑏 ∈ 𝐴 ((abs‘((𝐹‘𝑏) − 𝑥)) < 𝑦 ∧ (abs‘((𝐹‘𝑏) − 𝑅)) < 𝑦))
174	173	3exp 1135	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((((𝜑 ∧ 𝑦 ∈ ℝ⁺) ∧ 𝑧 ∈ ℝ⁺ ∧ ∀𝑤 ∈ 𝐴 ((𝑤 ≠ 𝐵 ∧ (abs‘(𝑤 − 𝐵)) < 𝑧) → (abs‘((𝐹‘𝑤) − 𝑥)) < 𝑦)) ∧ 𝑣 ∈ ℝ⁺ ∧ ∀𝑤 ∈ (𝐴 ∩ (𝐵(,)+∞))((𝑤 ≠ 𝐵 ∧ (abs‘(𝑤 − 𝐵)) < 𝑣) → (abs‘(((𝐹 ↾ (𝐵(,)+∞))‘𝑤) − 𝑅)) < 𝑦)) → (𝑏 ∈ ((𝐴 ∩ (𝐵(,)+∞)) ∖ {𝐵}) → (((abs‘(𝑏 − 𝐵)) < 𝑧 ∧ (abs‘(𝑏 − 𝐵)) < 𝑣) → ∃𝑏 ∈ 𝐴 ((abs‘((𝐹‘𝑏) − 𝑥)) < 𝑦 ∧ (abs‘((𝐹‘𝑏) − 𝑅)) < 𝑦))))
175	127, 128, 174	rexlimd 3272	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((𝜑 ∧ 𝑦 ∈ ℝ⁺) ∧ 𝑧 ∈ ℝ⁺ ∧ ∀𝑤 ∈ 𝐴 ((𝑤 ≠ 𝐵 ∧ (abs‘(𝑤 − 𝐵)) < 𝑧) → (abs‘((𝐹‘𝑤) − 𝑥)) < 𝑦)) ∧ 𝑣 ∈ ℝ⁺ ∧ ∀𝑤 ∈ (𝐴 ∩ (𝐵(,)+∞))((𝑤 ≠ 𝐵 ∧ (abs‘(𝑤 − 𝐵)) < 𝑣) → (abs‘(((𝐹 ↾ (𝐵(,)+∞))‘𝑤) − 𝑅)) < 𝑦)) → (∃𝑏 ∈ ((𝐴 ∩ (𝐵(,)+∞)) ∖ {𝐵})((abs‘(𝑏 − 𝐵)) < 𝑧 ∧ (abs‘(𝑏 − 𝐵)) < 𝑣) → ∃𝑏 ∈ 𝐴 ((abs‘((𝐹‘𝑏) − 𝑥)) < 𝑦 ∧ (abs‘((𝐹‘𝑏) − 𝑅)) < 𝑦)))
176	126, 175	mpd 16	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((𝜑 ∧ 𝑦 ∈ ℝ⁺) ∧ 𝑧 ∈ ℝ⁺ ∧ ∀𝑤 ∈ 𝐴 ((𝑤 ≠ 𝐵 ∧ (abs‘(𝑤 − 𝐵)) < 𝑧) → (abs‘((𝐹‘𝑤) − 𝑥)) < 𝑦)) ∧ 𝑣 ∈ ℝ⁺ ∧ ∀𝑤 ∈ (𝐴 ∩ (𝐵(,)+∞))((𝑤 ≠ 𝐵 ∧ (abs‘(𝑤 − 𝐵)) < 𝑣) → (abs‘(((𝐹 ↾ (𝐵(,)+∞))‘𝑤) − 𝑅)) < 𝑦)) → ∃𝑏 ∈ 𝐴 ((abs‘((𝐹‘𝑏) − 𝑥)) < 𝑦 ∧ (abs‘((𝐹‘𝑏) − 𝑅)) < 𝑦))
177	176	3exp 1135	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜑 ∧ 𝑦 ∈ ℝ⁺) ∧ 𝑧 ∈ ℝ⁺ ∧ ∀𝑤 ∈ 𝐴 ((𝑤 ≠ 𝐵 ∧ (abs‘(𝑤 − 𝐵)) < 𝑧) → (abs‘((𝐹‘𝑤) − 𝑥)) < 𝑦)) → (𝑣 ∈ ℝ⁺ → (∀𝑤 ∈ (𝐴 ∩ (𝐵(,)+∞))((𝑤 ≠ 𝐵 ∧ (abs‘(𝑤 − 𝐵)) < 𝑣) → (abs‘(((𝐹 ↾ (𝐵(,)+∞))‘𝑤) − 𝑅)) < 𝑦) → ∃𝑏 ∈ 𝐴 ((abs‘((𝐹‘𝑏) − 𝑥)) < 𝑦 ∧ (abs‘((𝐹‘𝑏) − 𝑅)) < 𝑦))))
178	177	rexlimdv 3164	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ 𝑦 ∈ ℝ⁺) ∧ 𝑧 ∈ ℝ⁺ ∧ ∀𝑤 ∈ 𝐴 ((𝑤 ≠ 𝐵 ∧ (abs‘(𝑤 − 𝐵)) < 𝑧) → (abs‘((𝐹‘𝑤) − 𝑥)) < 𝑦)) → (∃𝑣 ∈ ℝ⁺ ∀𝑤 ∈ (𝐴 ∩ (𝐵(,)+∞))((𝑤 ≠ 𝐵 ∧ (abs‘(𝑤 − 𝐵)) < 𝑣) → (abs‘(((𝐹 ↾ (𝐵(,)+∞))‘𝑤) − 𝑅)) < 𝑦) → ∃𝑏 ∈ 𝐴 ((abs‘((𝐹‘𝑏) − 𝑥)) < 𝑦 ∧ (abs‘((𝐹‘𝑏) − 𝑅)) < 𝑦)))
179	61, 178	mpd 16	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑦 ∈ ℝ⁺) ∧ 𝑧 ∈ ℝ⁺ ∧ ∀𝑤 ∈ 𝐴 ((𝑤 ≠ 𝐵 ∧ (abs‘(𝑤 − 𝐵)) < 𝑧) → (abs‘((𝐹‘𝑤) − 𝑥)) < 𝑦)) → ∃𝑏 ∈ 𝐴 ((abs‘((𝐹‘𝑏) − 𝑥)) < 𝑦 ∧ (abs‘((𝐹‘𝑏) − 𝑅)) < 𝑦))
180	179	3exp 1135	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑦 ∈ ℝ⁺) → (𝑧 ∈ ℝ⁺ → (∀𝑤 ∈ 𝐴 ((𝑤 ≠ 𝐵 ∧ (abs‘(𝑤 − 𝐵)) < 𝑧) → (abs‘((𝐹‘𝑤) − 𝑥)) < 𝑦) → ∃𝑏 ∈ 𝐴 ((abs‘((𝐹‘𝑏) − 𝑥)) < 𝑦 ∧ (abs‘((𝐹‘𝑏) − 𝑅)) < 𝑦))))
181	180	rexlimdv 3164	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑦 ∈ ℝ⁺) → (∃𝑧 ∈ ℝ⁺ ∀𝑤 ∈ 𝐴 ((𝑤 ≠ 𝐵 ∧ (abs‘(𝑤 − 𝐵)) < 𝑧) → (abs‘((𝐹‘𝑤) − 𝑥)) < 𝑦) → ∃𝑏 ∈ 𝐴 ((abs‘((𝐹‘𝑏) − 𝑥)) < 𝑦 ∧ (abs‘((𝐹‘𝑏) − 𝑅)) < 𝑦)))
182	181	imp 411	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑦 ∈ ℝ⁺) ∧ ∃𝑧 ∈ ℝ⁺ ∀𝑤 ∈ 𝐴 ((𝑤 ≠ 𝐵 ∧ (abs‘(𝑤 − 𝐵)) < 𝑧) → (abs‘((𝐹‘𝑤) − 𝑥)) < 𝑦)) → ∃𝑏 ∈ 𝐴 ((abs‘((𝐹‘𝑏) − 𝑥)) < 𝑦 ∧ (abs‘((𝐹‘𝑏) − 𝑅)) < 𝑦))
183	182	adantllr 731	. . . . . . . . . . . . . 14 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℂ) ∧ 𝑦 ∈ ℝ⁺) ∧ ∃𝑧 ∈ ℝ⁺ ∀𝑤 ∈ 𝐴 ((𝑤 ≠ 𝐵 ∧ (abs‘(𝑤 − 𝐵)) < 𝑧) → (abs‘((𝐹‘𝑤) − 𝑥)) < 𝑦)) → ∃𝑏 ∈ 𝐴 ((abs‘((𝐹‘𝑏) − 𝑥)) < 𝑦 ∧ (abs‘((𝐹‘𝑏) − 𝑅)) < 𝑦))
184	183	ad2antrr 738	. . . . . . . . . . . . 13 ⊢ ((((((𝜑 ∧ 𝑥 ∈ ℂ) ∧ 𝑦 ∈ ℝ⁺) ∧ ∃𝑧 ∈ ℝ⁺ ∀𝑤 ∈ 𝐴 ((𝑤 ≠ 𝐵 ∧ (abs‘(𝑤 − 𝐵)) < 𝑧) → (abs‘((𝐹‘𝑤) − 𝑥)) < 𝑦)) ∧ 𝑎 ∈ 𝐴) ∧ ((abs‘((𝐹‘𝑎) − 𝑥)) < 𝑦 ∧ (abs‘((𝐹‘𝑎) − 𝐿)) < 𝑦)) → ∃𝑏 ∈ 𝐴 ((abs‘((𝐹‘𝑏) − 𝑥)) < 𝑦 ∧ (abs‘((𝐹‘𝑏) − 𝑅)) < 𝑦))
185	3	ad6antr 748	. . . . . . . . . . . . . . . . . . 19 ⊢ (((((((𝜑 ∧ 𝑥 ∈ ℂ) ∧ 𝑦 ∈ ℝ⁺) ∧ 𝑎 ∈ 𝐴) ∧ ((abs‘((𝐹‘𝑎) − 𝑥)) < 𝑦 ∧ (abs‘((𝐹‘𝑎) − 𝐿)) < 𝑦)) ∧ 𝑏 ∈ 𝐴) ∧ ((abs‘((𝐹‘𝑏) − 𝑥)) < 𝑦 ∧ (abs‘((𝐹‘𝑏) − 𝑅)) < 𝑦)) → 𝑅 ∈ ℂ)
186	7	ad6antr 748	. . . . . . . . . . . . . . . . . . 19 ⊢ (((((((𝜑 ∧ 𝑥 ∈ ℂ) ∧ 𝑦 ∈ ℝ⁺) ∧ 𝑎 ∈ 𝐴) ∧ ((abs‘((𝐹‘𝑎) − 𝑥)) < 𝑦 ∧ (abs‘((𝐹‘𝑎) − 𝐿)) < 𝑦)) ∧ 𝑏 ∈ 𝐴) ∧ ((abs‘((𝐹‘𝑏) − 𝑥)) < 𝑦 ∧ (abs‘((𝐹‘𝑏) − 𝑅)) < 𝑦)) → 𝐿 ∈ ℂ)
187	185, 186	subcld 11557	. . . . . . . . . . . . . . . . . 18 ⊢ (((((((𝜑 ∧ 𝑥 ∈ ℂ) ∧ 𝑦 ∈ ℝ⁺) ∧ 𝑎 ∈ 𝐴) ∧ ((abs‘((𝐹‘𝑎) − 𝑥)) < 𝑦 ∧ (abs‘((𝐹‘𝑎) − 𝐿)) < 𝑦)) ∧ 𝑏 ∈ 𝐴) ∧ ((abs‘((𝐹‘𝑏) − 𝑥)) < 𝑦 ∧ (abs‘((𝐹‘𝑏) − 𝑅)) < 𝑦)) → (𝑅 − 𝐿) ∈ ℂ)
188	187	abscld 15480	. . . . . . . . . . . . . . . . 17 ⊢ (((((((𝜑 ∧ 𝑥 ∈ ℂ) ∧ 𝑦 ∈ ℝ⁺) ∧ 𝑎 ∈ 𝐴) ∧ ((abs‘((𝐹‘𝑎) − 𝑥)) < 𝑦 ∧ (abs‘((𝐹‘𝑎) − 𝐿)) < 𝑦)) ∧ 𝑏 ∈ 𝐴) ∧ ((abs‘((𝐹‘𝑏) − 𝑥)) < 𝑦 ∧ (abs‘((𝐹‘𝑏) − 𝑅)) < 𝑦)) → (abs‘(𝑅 − 𝐿)) ∈ ℝ)
189		simp-6l 798	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((((((𝜑 ∧ 𝑥 ∈ ℂ) ∧ 𝑦 ∈ ℝ⁺) ∧ 𝑎 ∈ 𝐴) ∧ ((abs‘((𝐹‘𝑎) − 𝑥)) < 𝑦 ∧ (abs‘((𝐹‘𝑎) − 𝐿)) < 𝑦)) ∧ 𝑏 ∈ 𝐴) ∧ ((abs‘((𝐹‘𝑏) − 𝑥)) < 𝑦 ∧ (abs‘((𝐹‘𝑏) − 𝑅)) < 𝑦)) → 𝜑)
190		simplr 780	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((((((𝜑 ∧ 𝑥 ∈ ℂ) ∧ 𝑦 ∈ ℝ⁺) ∧ 𝑎 ∈ 𝐴) ∧ ((abs‘((𝐹‘𝑎) − 𝑥)) < 𝑦 ∧ (abs‘((𝐹‘𝑎) − 𝐿)) < 𝑦)) ∧ 𝑏 ∈ 𝐴) ∧ ((abs‘((𝐹‘𝑏) − 𝑥)) < 𝑦 ∧ (abs‘((𝐹‘𝑏) − 𝑅)) < 𝑦)) → 𝑏 ∈ 𝐴)
191	36	ffvelcdmda 7069	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝜑 ∧ 𝑏 ∈ 𝐴) → (𝐹‘𝑏) ∈ ℂ)
192	189, 190, 191	syl2anc 595	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((((((𝜑 ∧ 𝑥 ∈ ℂ) ∧ 𝑦 ∈ ℝ⁺) ∧ 𝑎 ∈ 𝐴) ∧ ((abs‘((𝐹‘𝑎) − 𝑥)) < 𝑦 ∧ (abs‘((𝐹‘𝑎) − 𝐿)) < 𝑦)) ∧ 𝑏 ∈ 𝐴) ∧ ((abs‘((𝐹‘𝑏) − 𝑥)) < 𝑦 ∧ (abs‘((𝐹‘𝑏) − 𝑅)) < 𝑦)) → (𝐹‘𝑏) ∈ ℂ)
193	185, 192	subcld 11557	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((((((𝜑 ∧ 𝑥 ∈ ℂ) ∧ 𝑦 ∈ ℝ⁺) ∧ 𝑎 ∈ 𝐴) ∧ ((abs‘((𝐹‘𝑎) − 𝑥)) < 𝑦 ∧ (abs‘((𝐹‘𝑎) − 𝐿)) < 𝑦)) ∧ 𝑏 ∈ 𝐴) ∧ ((abs‘((𝐹‘𝑏) − 𝑥)) < 𝑦 ∧ (abs‘((𝐹‘𝑏) − 𝑅)) < 𝑦)) → (𝑅 − (𝐹‘𝑏)) ∈ ℂ)
194	193	abscld 15480	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((((((𝜑 ∧ 𝑥 ∈ ℂ) ∧ 𝑦 ∈ ℝ⁺) ∧ 𝑎 ∈ 𝐴) ∧ ((abs‘((𝐹‘𝑎) − 𝑥)) < 𝑦 ∧ (abs‘((𝐹‘𝑎) − 𝐿)) < 𝑦)) ∧ 𝑏 ∈ 𝐴) ∧ ((abs‘((𝐹‘𝑏) − 𝑥)) < 𝑦 ∧ (abs‘((𝐹‘𝑏) − 𝑅)) < 𝑦)) → (abs‘(𝑅 − (𝐹‘𝑏))) ∈ ℝ)
195		simp-6r 799	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((((((𝜑 ∧ 𝑥 ∈ ℂ) ∧ 𝑦 ∈ ℝ⁺) ∧ 𝑎 ∈ 𝐴) ∧ ((abs‘((𝐹‘𝑎) − 𝑥)) < 𝑦 ∧ (abs‘((𝐹‘𝑎) − 𝐿)) < 𝑦)) ∧ 𝑏 ∈ 𝐴) ∧ ((abs‘((𝐹‘𝑏) − 𝑥)) < 𝑦 ∧ (abs‘((𝐹‘𝑏) − 𝑅)) < 𝑦)) → 𝑥 ∈ ℂ)
196	192, 195	subcld 11557	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((((((𝜑 ∧ 𝑥 ∈ ℂ) ∧ 𝑦 ∈ ℝ⁺) ∧ 𝑎 ∈ 𝐴) ∧ ((abs‘((𝐹‘𝑎) − 𝑥)) < 𝑦 ∧ (abs‘((𝐹‘𝑎) − 𝐿)) < 𝑦)) ∧ 𝑏 ∈ 𝐴) ∧ ((abs‘((𝐹‘𝑏) − 𝑥)) < 𝑦 ∧ (abs‘((𝐹‘𝑏) − 𝑅)) < 𝑦)) → ((𝐹‘𝑏) − 𝑥) ∈ ℂ)
197	196	abscld 15480	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((((((𝜑 ∧ 𝑥 ∈ ℂ) ∧ 𝑦 ∈ ℝ⁺) ∧ 𝑎 ∈ 𝐴) ∧ ((abs‘((𝐹‘𝑎) − 𝑥)) < 𝑦 ∧ (abs‘((𝐹‘𝑎) − 𝐿)) < 𝑦)) ∧ 𝑏 ∈ 𝐴) ∧ ((abs‘((𝐹‘𝑏) − 𝑥)) < 𝑦 ∧ (abs‘((𝐹‘𝑏) − 𝑅)) < 𝑦)) → (abs‘((𝐹‘𝑏) − 𝑥)) ∈ ℝ)
198	194, 197	readdcld 11226	. . . . . . . . . . . . . . . . . . 19 ⊢ (((((((𝜑 ∧ 𝑥 ∈ ℂ) ∧ 𝑦 ∈ ℝ⁺) ∧ 𝑎 ∈ 𝐴) ∧ ((abs‘((𝐹‘𝑎) − 𝑥)) < 𝑦 ∧ (abs‘((𝐹‘𝑎) − 𝐿)) < 𝑦)) ∧ 𝑏 ∈ 𝐴) ∧ ((abs‘((𝐹‘𝑏) − 𝑥)) < 𝑦 ∧ (abs‘((𝐹‘𝑏) − 𝑅)) < 𝑦)) → ((abs‘(𝑅 − (𝐹‘𝑏))) + (abs‘((𝐹‘𝑏) − 𝑥))) ∈ ℝ)
199		simp-4r 795	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((((((𝜑 ∧ 𝑥 ∈ ℂ) ∧ 𝑦 ∈ ℝ⁺) ∧ 𝑎 ∈ 𝐴) ∧ ((abs‘((𝐹‘𝑎) − 𝑥)) < 𝑦 ∧ (abs‘((𝐹‘𝑎) − 𝐿)) < 𝑦)) ∧ 𝑏 ∈ 𝐴) ∧ ((abs‘((𝐹‘𝑏) − 𝑥)) < 𝑦 ∧ (abs‘((𝐹‘𝑏) − 𝑅)) < 𝑦)) → 𝑎 ∈ 𝐴)
200	36	ffvelcdmda 7069	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝜑 ∧ 𝑎 ∈ 𝐴) → (𝐹‘𝑎) ∈ ℂ)
201	189, 199, 200	syl2anc 595	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((((((𝜑 ∧ 𝑥 ∈ ℂ) ∧ 𝑦 ∈ ℝ⁺) ∧ 𝑎 ∈ 𝐴) ∧ ((abs‘((𝐹‘𝑎) − 𝑥)) < 𝑦 ∧ (abs‘((𝐹‘𝑎) − 𝐿)) < 𝑦)) ∧ 𝑏 ∈ 𝐴) ∧ ((abs‘((𝐹‘𝑏) − 𝑥)) < 𝑦 ∧ (abs‘((𝐹‘𝑏) − 𝑅)) < 𝑦)) → (𝐹‘𝑎) ∈ ℂ)
202	195, 201	subcld 11557	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((((((𝜑 ∧ 𝑥 ∈ ℂ) ∧ 𝑦 ∈ ℝ⁺) ∧ 𝑎 ∈ 𝐴) ∧ ((abs‘((𝐹‘𝑎) − 𝑥)) < 𝑦 ∧ (abs‘((𝐹‘𝑎) − 𝐿)) < 𝑦)) ∧ 𝑏 ∈ 𝐴) ∧ ((abs‘((𝐹‘𝑏) − 𝑥)) < 𝑦 ∧ (abs‘((𝐹‘𝑏) − 𝑅)) < 𝑦)) → (𝑥 − (𝐹‘𝑎)) ∈ ℂ)
203	202	abscld 15480	. . . . . . . . . . . . . . . . . . 19 ⊢ (((((((𝜑 ∧ 𝑥 ∈ ℂ) ∧ 𝑦 ∈ ℝ⁺) ∧ 𝑎 ∈ 𝐴) ∧ ((abs‘((𝐹‘𝑎) − 𝑥)) < 𝑦 ∧ (abs‘((𝐹‘𝑎) − 𝐿)) < 𝑦)) ∧ 𝑏 ∈ 𝐴) ∧ ((abs‘((𝐹‘𝑏) − 𝑥)) < 𝑦 ∧ (abs‘((𝐹‘𝑏) − 𝑅)) < 𝑦)) → (abs‘(𝑥 − (𝐹‘𝑎))) ∈ ℝ)
204	198, 203	readdcld 11226	. . . . . . . . . . . . . . . . . 18 ⊢ (((((((𝜑 ∧ 𝑥 ∈ ℂ) ∧ 𝑦 ∈ ℝ⁺) ∧ 𝑎 ∈ 𝐴) ∧ ((abs‘((𝐹‘𝑎) − 𝑥)) < 𝑦 ∧ (abs‘((𝐹‘𝑎) − 𝐿)) < 𝑦)) ∧ 𝑏 ∈ 𝐴) ∧ ((abs‘((𝐹‘𝑏) − 𝑥)) < 𝑦 ∧ (abs‘((𝐹‘𝑏) − 𝑅)) < 𝑦)) → (((abs‘(𝑅 − (𝐹‘𝑏))) + (abs‘((𝐹‘𝑏) − 𝑥))) + (abs‘(𝑥 − (𝐹‘𝑎)))) ∈ ℝ)
205	201, 186	subcld 11557	. . . . . . . . . . . . . . . . . . 19 ⊢ (((((((𝜑 ∧ 𝑥 ∈ ℂ) ∧ 𝑦 ∈ ℝ⁺) ∧ 𝑎 ∈ 𝐴) ∧ ((abs‘((𝐹‘𝑎) − 𝑥)) < 𝑦 ∧ (abs‘((𝐹‘𝑎) − 𝐿)) < 𝑦)) ∧ 𝑏 ∈ 𝐴) ∧ ((abs‘((𝐹‘𝑏) − 𝑥)) < 𝑦 ∧ (abs‘((𝐹‘𝑏) − 𝑅)) < 𝑦)) → ((𝐹‘𝑎) − 𝐿) ∈ ℂ)
206	205	abscld 15480	. . . . . . . . . . . . . . . . . 18 ⊢ (((((((𝜑 ∧ 𝑥 ∈ ℂ) ∧ 𝑦 ∈ ℝ⁺) ∧ 𝑎 ∈ 𝐴) ∧ ((abs‘((𝐹‘𝑎) − 𝑥)) < 𝑦 ∧ (abs‘((𝐹‘𝑎) − 𝐿)) < 𝑦)) ∧ 𝑏 ∈ 𝐴) ∧ ((abs‘((𝐹‘𝑏) − 𝑥)) < 𝑦 ∧ (abs‘((𝐹‘𝑏) − 𝑅)) < 𝑦)) → (abs‘((𝐹‘𝑎) − 𝐿)) ∈ ℝ)
207	204, 206	readdcld 11226	. . . . . . . . . . . . . . . . 17 ⊢ (((((((𝜑 ∧ 𝑥 ∈ ℂ) ∧ 𝑦 ∈ ℝ⁺) ∧ 𝑎 ∈ 𝐴) ∧ ((abs‘((𝐹‘𝑎) − 𝑥)) < 𝑦 ∧ (abs‘((𝐹‘𝑎) − 𝐿)) < 𝑦)) ∧ 𝑏 ∈ 𝐴) ∧ ((abs‘((𝐹‘𝑏) − 𝑥)) < 𝑦 ∧ (abs‘((𝐹‘𝑏) − 𝑅)) < 𝑦)) → ((((abs‘(𝑅 − (𝐹‘𝑏))) + (abs‘((𝐹‘𝑏) − 𝑥))) + (abs‘(𝑥 − (𝐹‘𝑎)))) + (abs‘((𝐹‘𝑎) − 𝐿))) ∈ ℝ)
208	15	a1i 11	. . . . . . . . . . . . . . . . . 18 ⊢ (((((((𝜑 ∧ 𝑥 ∈ ℂ) ∧ 𝑦 ∈ ℝ⁺) ∧ 𝑎 ∈ 𝐴) ∧ ((abs‘((𝐹‘𝑎) − 𝑥)) < 𝑦 ∧ (abs‘((𝐹‘𝑎) − 𝐿)) < 𝑦)) ∧ 𝑏 ∈ 𝐴) ∧ ((abs‘((𝐹‘𝑏) − 𝑥)) < 𝑦 ∧ (abs‘((𝐹‘𝑏) − 𝑅)) < 𝑦)) → 4 ∈ ℝ)
209		rpre 13016	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑦 ∈ ℝ⁺ → 𝑦 ∈ ℝ)
210	209	ad5antlr 747	. . . . . . . . . . . . . . . . . 18 ⊢ (((((((𝜑 ∧ 𝑥 ∈ ℂ) ∧ 𝑦 ∈ ℝ⁺) ∧ 𝑎 ∈ 𝐴) ∧ ((abs‘((𝐹‘𝑎) − 𝑥)) < 𝑦 ∧ (abs‘((𝐹‘𝑎) − 𝐿)) < 𝑦)) ∧ 𝑏 ∈ 𝐴) ∧ ((abs‘((𝐹‘𝑏) − 𝑥)) < 𝑦 ∧ (abs‘((𝐹‘𝑏) − 𝑅)) < 𝑦)) → 𝑦 ∈ ℝ)
211	208, 210	remulcld 11227	. . . . . . . . . . . . . . . . 17 ⊢ (((((((𝜑 ∧ 𝑥 ∈ ℂ) ∧ 𝑦 ∈ ℝ⁺) ∧ 𝑎 ∈ 𝐴) ∧ ((abs‘((𝐹‘𝑎) − 𝑥)) < 𝑦 ∧ (abs‘((𝐹‘𝑎) − 𝐿)) < 𝑦)) ∧ 𝑏 ∈ 𝐴) ∧ ((abs‘((𝐹‘𝑏) − 𝑥)) < 𝑦 ∧ (abs‘((𝐹‘𝑏) − 𝑅)) < 𝑦)) → (4 · 𝑦) ∈ ℝ)
212	185, 192, 195, 201, 186	absnpncan3d 45884	. . . . . . . . . . . . . . . . 17 ⊢ (((((((𝜑 ∧ 𝑥 ∈ ℂ) ∧ 𝑦 ∈ ℝ⁺) ∧ 𝑎 ∈ 𝐴) ∧ ((abs‘((𝐹‘𝑎) − 𝑥)) < 𝑦 ∧ (abs‘((𝐹‘𝑎) − 𝐿)) < 𝑦)) ∧ 𝑏 ∈ 𝐴) ∧ ((abs‘((𝐹‘𝑏) − 𝑥)) < 𝑦 ∧ (abs‘((𝐹‘𝑏) − 𝑅)) < 𝑦)) → (abs‘(𝑅 − 𝐿)) ≤ ((((abs‘(𝑅 − (𝐹‘𝑏))) + (abs‘((𝐹‘𝑏) − 𝑥))) + (abs‘(𝑥 − (𝐹‘𝑎)))) + (abs‘((𝐹‘𝑎) − 𝐿))))
213	185, 192	abssubd 15497	. . . . . . . . . . . . . . . . . . 19 ⊢ (((((((𝜑 ∧ 𝑥 ∈ ℂ) ∧ 𝑦 ∈ ℝ⁺) ∧ 𝑎 ∈ 𝐴) ∧ ((abs‘((𝐹‘𝑎) − 𝑥)) < 𝑦 ∧ (abs‘((𝐹‘𝑎) − 𝐿)) < 𝑦)) ∧ 𝑏 ∈ 𝐴) ∧ ((abs‘((𝐹‘𝑏) − 𝑥)) < 𝑦 ∧ (abs‘((𝐹‘𝑏) − 𝑅)) < 𝑦)) → (abs‘(𝑅 − (𝐹‘𝑏))) = (abs‘((𝐹‘𝑏) − 𝑅)))
214		simprr 784	. . . . . . . . . . . . . . . . . . 19 ⊢ (((((((𝜑 ∧ 𝑥 ∈ ℂ) ∧ 𝑦 ∈ ℝ⁺) ∧ 𝑎 ∈ 𝐴) ∧ ((abs‘((𝐹‘𝑎) − 𝑥)) < 𝑦 ∧ (abs‘((𝐹‘𝑎) − 𝐿)) < 𝑦)) ∧ 𝑏 ∈ 𝐴) ∧ ((abs‘((𝐹‘𝑏) − 𝑥)) < 𝑦 ∧ (abs‘((𝐹‘𝑏) − 𝑅)) < 𝑦)) → (abs‘((𝐹‘𝑏) − 𝑅)) < 𝑦)
215	213, 214	eqbrtrd 5127	. . . . . . . . . . . . . . . . . 18 ⊢ (((((((𝜑 ∧ 𝑥 ∈ ℂ) ∧ 𝑦 ∈ ℝ⁺) ∧ 𝑎 ∈ 𝐴) ∧ ((abs‘((𝐹‘𝑎) − 𝑥)) < 𝑦 ∧ (abs‘((𝐹‘𝑎) − 𝐿)) < 𝑦)) ∧ 𝑏 ∈ 𝐴) ∧ ((abs‘((𝐹‘𝑏) − 𝑥)) < 𝑦 ∧ (abs‘((𝐹‘𝑏) − 𝑅)) < 𝑦)) → (abs‘(𝑅 − (𝐹‘𝑏))) < 𝑦)
216		simprl 782	. . . . . . . . . . . . . . . . . 18 ⊢ (((((((𝜑 ∧ 𝑥 ∈ ℂ) ∧ 𝑦 ∈ ℝ⁺) ∧ 𝑎 ∈ 𝐴) ∧ ((abs‘((𝐹‘𝑎) − 𝑥)) < 𝑦 ∧ (abs‘((𝐹‘𝑎) − 𝐿)) < 𝑦)) ∧ 𝑏 ∈ 𝐴) ∧ ((abs‘((𝐹‘𝑏) − 𝑥)) < 𝑦 ∧ (abs‘((𝐹‘𝑏) − 𝑅)) < 𝑦)) → (abs‘((𝐹‘𝑏) − 𝑥)) < 𝑦)
217		simp-5r 797	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((((𝜑 ∧ 𝑥 ∈ ℂ) ∧ 𝑦 ∈ ℝ⁺) ∧ 𝑎 ∈ 𝐴) ∧ ((abs‘((𝐹‘𝑎) − 𝑥)) < 𝑦 ∧ (abs‘((𝐹‘𝑎) − 𝐿)) < 𝑦)) ∧ 𝑏 ∈ 𝐴) → 𝑥 ∈ ℂ)
218	200	ad5ant14 769	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((((𝜑 ∧ 𝑥 ∈ ℂ) ∧ 𝑦 ∈ ℝ⁺) ∧ 𝑎 ∈ 𝐴) ∧ ((abs‘((𝐹‘𝑎) − 𝑥)) < 𝑦 ∧ (abs‘((𝐹‘𝑎) − 𝐿)) < 𝑦)) → (𝐹‘𝑎) ∈ ℂ)
219	218	adantr 485	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((((𝜑 ∧ 𝑥 ∈ ℂ) ∧ 𝑦 ∈ ℝ⁺) ∧ 𝑎 ∈ 𝐴) ∧ ((abs‘((𝐹‘𝑎) − 𝑥)) < 𝑦 ∧ (abs‘((𝐹‘𝑎) − 𝐿)) < 𝑦)) ∧ 𝑏 ∈ 𝐴) → (𝐹‘𝑎) ∈ ℂ)
220	217, 219	abssubd 15497	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((((𝜑 ∧ 𝑥 ∈ ℂ) ∧ 𝑦 ∈ ℝ⁺) ∧ 𝑎 ∈ 𝐴) ∧ ((abs‘((𝐹‘𝑎) − 𝑥)) < 𝑦 ∧ (abs‘((𝐹‘𝑎) − 𝐿)) < 𝑦)) ∧ 𝑏 ∈ 𝐴) → (abs‘(𝑥 − (𝐹‘𝑎))) = (abs‘((𝐹‘𝑎) − 𝑥)))
221		simplrl 788	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((((𝜑 ∧ 𝑥 ∈ ℂ) ∧ 𝑦 ∈ ℝ⁺) ∧ 𝑎 ∈ 𝐴) ∧ ((abs‘((𝐹‘𝑎) − 𝑥)) < 𝑦 ∧ (abs‘((𝐹‘𝑎) − 𝐿)) < 𝑦)) ∧ 𝑏 ∈ 𝐴) → (abs‘((𝐹‘𝑎) − 𝑥)) < 𝑦)
222	220, 221	eqbrtrd 5127	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((((𝜑 ∧ 𝑥 ∈ ℂ) ∧ 𝑦 ∈ ℝ⁺) ∧ 𝑎 ∈ 𝐴) ∧ ((abs‘((𝐹‘𝑎) − 𝑥)) < 𝑦 ∧ (abs‘((𝐹‘𝑎) − 𝐿)) < 𝑦)) ∧ 𝑏 ∈ 𝐴) → (abs‘(𝑥 − (𝐹‘𝑎))) < 𝑦)
223	222	adantr 485	. . . . . . . . . . . . . . . . . 18 ⊢ (((((((𝜑 ∧ 𝑥 ∈ ℂ) ∧ 𝑦 ∈ ℝ⁺) ∧ 𝑎 ∈ 𝐴) ∧ ((abs‘((𝐹‘𝑎) − 𝑥)) < 𝑦 ∧ (abs‘((𝐹‘𝑎) − 𝐿)) < 𝑦)) ∧ 𝑏 ∈ 𝐴) ∧ ((abs‘((𝐹‘𝑏) − 𝑥)) < 𝑦 ∧ (abs‘((𝐹‘𝑏) − 𝑅)) < 𝑦)) → (abs‘(𝑥 − (𝐹‘𝑎))) < 𝑦)
224		simplrr 789	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((((𝜑 ∧ 𝑥 ∈ ℂ) ∧ 𝑦 ∈ ℝ⁺) ∧ 𝑎 ∈ 𝐴) ∧ ((abs‘((𝐹‘𝑎) − 𝑥)) < 𝑦 ∧ (abs‘((𝐹‘𝑎) − 𝐿)) < 𝑦)) ∧ 𝑏 ∈ 𝐴) → (abs‘((𝐹‘𝑎) − 𝐿)) < 𝑦)
225	224	adantr 485	. . . . . . . . . . . . . . . . . 18 ⊢ (((((((𝜑 ∧ 𝑥 ∈ ℂ) ∧ 𝑦 ∈ ℝ⁺) ∧ 𝑎 ∈ 𝐴) ∧ ((abs‘((𝐹‘𝑎) − 𝑥)) < 𝑦 ∧ (abs‘((𝐹‘𝑎) − 𝐿)) < 𝑦)) ∧ 𝑏 ∈ 𝐴) ∧ ((abs‘((𝐹‘𝑏) − 𝑥)) < 𝑦 ∧ (abs‘((𝐹‘𝑏) − 𝑅)) < 𝑦)) → (abs‘((𝐹‘𝑎) − 𝐿)) < 𝑦)
226	194, 197, 203, 206, 210, 215, 216, 223, 225	lt4addmuld 45883	. . . . . . . . . . . . . . . . 17 ⊢ (((((((𝜑 ∧ 𝑥 ∈ ℂ) ∧ 𝑦 ∈ ℝ⁺) ∧ 𝑎 ∈ 𝐴) ∧ ((abs‘((𝐹‘𝑎) − 𝑥)) < 𝑦 ∧ (abs‘((𝐹‘𝑎) − 𝐿)) < 𝑦)) ∧ 𝑏 ∈ 𝐴) ∧ ((abs‘((𝐹‘𝑏) − 𝑥)) < 𝑦 ∧ (abs‘((𝐹‘𝑏) − 𝑅)) < 𝑦)) → ((((abs‘(𝑅 − (𝐹‘𝑏))) + (abs‘((𝐹‘𝑏) − 𝑥))) + (abs‘(𝑥 − (𝐹‘𝑎)))) + (abs‘((𝐹‘𝑎) − 𝐿))) < (4 · 𝑦))
227	188, 207, 211, 212, 226	lelttrd 11356	. . . . . . . . . . . . . . . 16 ⊢ (((((((𝜑 ∧ 𝑥 ∈ ℂ) ∧ 𝑦 ∈ ℝ⁺) ∧ 𝑎 ∈ 𝐴) ∧ ((abs‘((𝐹‘𝑎) − 𝑥)) < 𝑦 ∧ (abs‘((𝐹‘𝑎) − 𝐿)) < 𝑦)) ∧ 𝑏 ∈ 𝐴) ∧ ((abs‘((𝐹‘𝑏) − 𝑥)) < 𝑦 ∧ (abs‘((𝐹‘𝑏) − 𝑅)) < 𝑦)) → (abs‘(𝑅 − 𝐿)) < (4 · 𝑦))
228	227	ex 417	. . . . . . . . . . . . . . 15 ⊢ ((((((𝜑 ∧ 𝑥 ∈ ℂ) ∧ 𝑦 ∈ ℝ⁺) ∧ 𝑎 ∈ 𝐴) ∧ ((abs‘((𝐹‘𝑎) − 𝑥)) < 𝑦 ∧ (abs‘((𝐹‘𝑎) − 𝐿)) < 𝑦)) ∧ 𝑏 ∈ 𝐴) → (((abs‘((𝐹‘𝑏) − 𝑥)) < 𝑦 ∧ (abs‘((𝐹‘𝑏) − 𝑅)) < 𝑦) → (abs‘(𝑅 − 𝐿)) < (4 · 𝑦)))
229	228	adantl3r 762	. . . . . . . . . . . . . 14 ⊢ (((((((𝜑 ∧ 𝑥 ∈ ℂ) ∧ 𝑦 ∈ ℝ⁺) ∧ ∃𝑧 ∈ ℝ⁺ ∀𝑤 ∈ 𝐴 ((𝑤 ≠ 𝐵 ∧ (abs‘(𝑤 − 𝐵)) < 𝑧) → (abs‘((𝐹‘𝑤) − 𝑥)) < 𝑦)) ∧ 𝑎 ∈ 𝐴) ∧ ((abs‘((𝐹‘𝑎) − 𝑥)) < 𝑦 ∧ (abs‘((𝐹‘𝑎) − 𝐿)) < 𝑦)) ∧ 𝑏 ∈ 𝐴) → (((abs‘((𝐹‘𝑏) − 𝑥)) < 𝑦 ∧ (abs‘((𝐹‘𝑏) − 𝑅)) < 𝑦) → (abs‘(𝑅 − 𝐿)) < (4 · 𝑦)))
230	229	reximdva 3178	. . . . . . . . . . . . 13 ⊢ ((((((𝜑 ∧ 𝑥 ∈ ℂ) ∧ 𝑦 ∈ ℝ⁺) ∧ ∃𝑧 ∈ ℝ⁺ ∀𝑤 ∈ 𝐴 ((𝑤 ≠ 𝐵 ∧ (abs‘(𝑤 − 𝐵)) < 𝑧) → (abs‘((𝐹‘𝑤) − 𝑥)) < 𝑦)) ∧ 𝑎 ∈ 𝐴) ∧ ((abs‘((𝐹‘𝑎) − 𝑥)) < 𝑦 ∧ (abs‘((𝐹‘𝑎) − 𝐿)) < 𝑦)) → (∃𝑏 ∈ 𝐴 ((abs‘((𝐹‘𝑏) − 𝑥)) < 𝑦 ∧ (abs‘((𝐹‘𝑏) − 𝑅)) < 𝑦) → ∃𝑏 ∈ 𝐴 (abs‘(𝑅 − 𝐿)) < (4 · 𝑦)))
231	184, 230	mpd 16	. . . . . . . . . . . 12 ⊢ ((((((𝜑 ∧ 𝑥 ∈ ℂ) ∧ 𝑦 ∈ ℝ⁺) ∧ ∃𝑧 ∈ ℝ⁺ ∀𝑤 ∈ 𝐴 ((𝑤 ≠ 𝐵 ∧ (abs‘(𝑤 − 𝐵)) < 𝑧) → (abs‘((𝐹‘𝑤) − 𝑥)) < 𝑦)) ∧ 𝑎 ∈ 𝐴) ∧ ((abs‘((𝐹‘𝑎) − 𝑥)) < 𝑦 ∧ (abs‘((𝐹‘𝑎) − 𝐿)) < 𝑦)) → ∃𝑏 ∈ 𝐴 (abs‘(𝑅 − 𝐿)) < (4 · 𝑦))
232		fresin 6737	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝐹:𝐴⟶ℂ → (𝐹 ↾ (-∞(,)𝐵)):(𝐴 ∩ (-∞(,)𝐵))⟶ℂ)
233	36, 232	syl 18	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝜑 → (𝐹 ↾ (-∞(,)𝐵)):(𝐴 ∩ (-∞(,)𝐵))⟶ℂ)
234		ioosscn 13426	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (-∞(,)𝐵) ⊆ ℂ
235	46, 234	sstri 3948	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝐴 ∩ (-∞(,)𝐵)) ⊆ ℂ
236	235	a1i 11	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝜑 → (𝐴 ∩ (-∞(,)𝐵)) ⊆ ℂ)
237	233, 236, 56	ellimc3 25999	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝜑 → (𝐿 ∈ ((𝐹 ↾ (-∞(,)𝐵)) lim_ℂ 𝐵) ↔ (𝐿 ∈ ℂ ∧ ∀𝑦 ∈ ℝ⁺ ∃𝑣 ∈ ℝ⁺ ∀𝑤 ∈ (𝐴 ∩ (-∞(,)𝐵))((𝑤 ≠ 𝐵 ∧ (abs‘(𝑤 − 𝐵)) < 𝑣) → (abs‘(((𝐹 ↾ (-∞(,)𝐵))‘𝑤) − 𝐿)) < 𝑦))))
238	6, 237	mpbid 235	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → (𝐿 ∈ ℂ ∧ ∀𝑦 ∈ ℝ⁺ ∃𝑣 ∈ ℝ⁺ ∀𝑤 ∈ (𝐴 ∩ (-∞(,)𝐵))((𝑤 ≠ 𝐵 ∧ (abs‘(𝑤 − 𝐵)) < 𝑣) → (abs‘(((𝐹 ↾ (-∞(,)𝐵))‘𝑤) − 𝐿)) < 𝑦)))
239	238	simprd 500	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → ∀𝑦 ∈ ℝ⁺ ∃𝑣 ∈ ℝ⁺ ∀𝑤 ∈ (𝐴 ∩ (-∞(,)𝐵))((𝑤 ≠ 𝐵 ∧ (abs‘(𝑤 − 𝐵)) < 𝑣) → (abs‘(((𝐹 ↾ (-∞(,)𝐵))‘𝑤) − 𝐿)) < 𝑦))
240	239	r19.21bi 3257	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑦 ∈ ℝ⁺) → ∃𝑣 ∈ ℝ⁺ ∀𝑤 ∈ (𝐴 ∩ (-∞(,)𝐵))((𝑤 ≠ 𝐵 ∧ (abs‘(𝑤 − 𝐵)) < 𝑣) → (abs‘(((𝐹 ↾ (-∞(,)𝐵))‘𝑤) − 𝐿)) < 𝑦))
241	240	3ad2ant1 1149	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑦 ∈ ℝ⁺) ∧ 𝑧 ∈ ℝ⁺ ∧ ∀𝑤 ∈ 𝐴 ((𝑤 ≠ 𝐵 ∧ (abs‘(𝑤 − 𝐵)) < 𝑧) → (abs‘((𝐹‘𝑤) − 𝑥)) < 𝑦)) → ∃𝑣 ∈ ℝ⁺ ∀𝑤 ∈ (𝐴 ∩ (-∞(,)𝐵))((𝑤 ≠ 𝐵 ∧ (abs‘(𝑤 − 𝐵)) < 𝑣) → (abs‘(((𝐹 ↾ (-∞(,)𝐵))‘𝑤) − 𝐿)) < 𝑦))
242		simp11l 1301	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((𝜑 ∧ 𝑦 ∈ ℝ⁺) ∧ 𝑧 ∈ ℝ⁺ ∧ ∀𝑤 ∈ 𝐴 ((𝑤 ≠ 𝐵 ∧ (abs‘(𝑤 − 𝐵)) < 𝑧) → (abs‘((𝐹‘𝑤) − 𝑥)) < 𝑦)) ∧ 𝑣 ∈ ℝ⁺ ∧ ∀𝑤 ∈ (𝐴 ∩ (-∞(,)𝐵))((𝑤 ≠ 𝐵 ∧ (abs‘(𝑤 − 𝐵)) < 𝑣) → (abs‘(((𝐹 ↾ (-∞(,)𝐵))‘𝑤) − 𝐿)) < 𝑦)) → 𝜑)
243		simp12 1221	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((𝜑 ∧ 𝑦 ∈ ℝ⁺) ∧ 𝑧 ∈ ℝ⁺ ∧ ∀𝑤 ∈ 𝐴 ((𝑤 ≠ 𝐵 ∧ (abs‘(𝑤 − 𝐵)) < 𝑧) → (abs‘((𝐹‘𝑤) − 𝑥)) < 𝑦)) ∧ 𝑣 ∈ ℝ⁺ ∧ ∀𝑤 ∈ (𝐴 ∩ (-∞(,)𝐵))((𝑤 ≠ 𝐵 ∧ (abs‘(𝑤 − 𝐵)) < 𝑣) → (abs‘(((𝐹 ↾ (-∞(,)𝐵))‘𝑤) − 𝐿)) < 𝑦)) → 𝑧 ∈ ℝ⁺)
244		simp2 1153	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((𝜑 ∧ 𝑦 ∈ ℝ⁺) ∧ 𝑧 ∈ ℝ⁺ ∧ ∀𝑤 ∈ 𝐴 ((𝑤 ≠ 𝐵 ∧ (abs‘(𝑤 − 𝐵)) < 𝑧) → (abs‘((𝐹‘𝑤) − 𝑥)) < 𝑦)) ∧ 𝑣 ∈ ℝ⁺ ∧ ∀𝑤 ∈ (𝐴 ∩ (-∞(,)𝐵))((𝑤 ≠ 𝐵 ∧ (abs‘(𝑤 − 𝐵)) < 𝑣) → (abs‘(((𝐹 ↾ (-∞(,)𝐵))‘𝑤) − 𝐿)) < 𝑦)) → 𝑣 ∈ ℝ⁺)
245		breq2 5109	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑢 = if(𝑧 ≤ 𝑣, 𝑧, 𝑣) → ((abs‘(𝑎 − 𝐵)) < 𝑢 ↔ (abs‘(𝑎 − 𝐵)) < if(𝑧 ≤ 𝑣, 𝑧, 𝑣)))
246	245	rexbidv 3189	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑢 = if(𝑧 ≤ 𝑣, 𝑧, 𝑣) → (∃𝑎 ∈ ((𝐴 ∩ (-∞(,)𝐵)) ∖ {𝐵})(abs‘(𝑎 − 𝐵)) < 𝑢 ↔ ∃𝑎 ∈ ((𝐴 ∩ (-∞(,)𝐵)) ∖ {𝐵})(abs‘(𝑎 − 𝐵)) < if(𝑧 ≤ 𝑣, 𝑧, 𝑣)))
247		inss1 4191	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (((limPt‘𝐾)‘(𝐴 ∩ (-∞(,)𝐵))) ∩ ℝ) ⊆ ((limPt‘𝐾)‘(𝐴 ∩ (-∞(,)𝐵)))
248	247	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝜑 → (((limPt‘𝐾)‘(𝐴 ∩ (-∞(,)𝐵))) ∩ ℝ) ⊆ ((limPt‘𝐾)‘(𝐴 ∩ (-∞(,)𝐵))))
249	48	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (𝜑 → (𝐴 ∩ (-∞(,)𝐵)) ⊆ ℝ)
250	79, 81	restlp 23301	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ((𝐾 ∈ Top ∧ ℝ ⊆ ℂ ∧ (𝐴 ∩ (-∞(,)𝐵)) ⊆ ℝ) → ((limPt‘𝐽)‘(𝐴 ∩ (-∞(,)𝐵))) = (((limPt‘𝐾)‘(𝐴 ∩ (-∞(,)𝐵))) ∩ ℝ))
251	71, 73, 249, 250	syl3anc 1394	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝜑 → ((limPt‘𝐽)‘(𝐴 ∩ (-∞(,)𝐵))) = (((limPt‘𝐾)‘(𝐴 ∩ (-∞(,)𝐵))) ∩ ℝ))
252	85	fveq1i 6872	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ((limPt‘(TopOpen‘ℂ_fld))‘(𝐴 ∩ (-∞(,)𝐵))) = ((limPt‘𝐾)‘(𝐴 ∩ (-∞(,)𝐵)))
253	252	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝜑 → ((limPt‘(TopOpen‘ℂ_fld))‘(𝐴 ∩ (-∞(,)𝐵))) = ((limPt‘𝐾)‘(𝐴 ∩ (-∞(,)𝐵))))
254	248, 251, 253	3sstr4d 3994	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝜑 → ((limPt‘𝐽)‘(𝐴 ∩ (-∞(,)𝐵))) ⊆ ((limPt‘(TopOpen‘ℂ_fld))‘(𝐴 ∩ (-∞(,)𝐵))))
255	254, 54	sseldd 3940	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝜑 → 𝐵 ∈ ((limPt‘(TopOpen‘ℂ_fld))‘(𝐴 ∩ (-∞(,)𝐵))))
256	236, 56	islpcn 46211	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝜑 → (𝐵 ∈ ((limPt‘(TopOpen‘ℂ_fld))‘(𝐴 ∩ (-∞(,)𝐵))) ↔ ∀𝑢 ∈ ℝ⁺ ∃𝑎 ∈ ((𝐴 ∩ (-∞(,)𝐵)) ∖ {𝐵})(abs‘(𝑎 − 𝐵)) < 𝑢))
257	255, 256	mpbid 235	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝜑 → ∀𝑢 ∈ ℝ⁺ ∃𝑎 ∈ ((𝐴 ∩ (-∞(,)𝐵)) ∖ {𝐵})(abs‘(𝑎 − 𝐵)) < 𝑢)
258	257	3ad2ant1 1149	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝜑 ∧ 𝑧 ∈ ℝ⁺ ∧ 𝑣 ∈ ℝ⁺) → ∀𝑢 ∈ ℝ⁺ ∃𝑎 ∈ ((𝐴 ∩ (-∞(,)𝐵)) ∖ {𝐵})(abs‘(𝑎 − 𝐵)) < 𝑢)
259	246, 258, 95	rspcdva 3585	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝜑 ∧ 𝑧 ∈ ℝ⁺ ∧ 𝑣 ∈ ℝ⁺) → ∃𝑎 ∈ ((𝐴 ∩ (-∞(,)𝐵)) ∖ {𝐵})(abs‘(𝑎 − 𝐵)) < if(𝑧 ≤ 𝑣, 𝑧, 𝑣))
260		eldifi 4087	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑎 ∈ ((𝐴 ∩ (-∞(,)𝐵)) ∖ {𝐵}) → 𝑎 ∈ (𝐴 ∩ (-∞(,)𝐵)))
261	48, 260	sselid 3937	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑎 ∈ ((𝐴 ∩ (-∞(,)𝐵)) ∖ {𝐵}) → 𝑎 ∈ ℝ)
262	73	sselda 3939	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ ((𝜑 ∧ 𝑎 ∈ ℝ) → 𝑎 ∈ ℂ)
263	56	adantr 485	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ ((𝜑 ∧ 𝑎 ∈ ℝ) → 𝐵 ∈ ℂ)
264	262, 263	subcld 11557	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ ((𝜑 ∧ 𝑎 ∈ ℝ) → (𝑎 − 𝐵) ∈ ℂ)
265	264	abscld 15480	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ ((𝜑 ∧ 𝑎 ∈ ℝ) → (abs‘(𝑎 − 𝐵)) ∈ ℝ)
266	265	3ad2antl1 1202	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (((𝜑 ∧ 𝑧 ∈ ℝ⁺ ∧ 𝑣 ∈ ℝ⁺) ∧ 𝑎 ∈ ℝ) → (abs‘(𝑎 − 𝐵)) ∈ ℝ)
267	266	adantr 485	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((((𝜑 ∧ 𝑧 ∈ ℝ⁺ ∧ 𝑣 ∈ ℝ⁺) ∧ 𝑎 ∈ ℝ) ∧ (abs‘(𝑎 − 𝐵)) < if(𝑧 ≤ 𝑣, 𝑧, 𝑣)) → (abs‘(𝑎 − 𝐵)) ∈ ℝ)
268	105	ad2antrr 738	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((((𝜑 ∧ 𝑧 ∈ ℝ⁺ ∧ 𝑣 ∈ ℝ⁺) ∧ 𝑎 ∈ ℝ) ∧ (abs‘(𝑎 − 𝐵)) < if(𝑧 ≤ 𝑣, 𝑧, 𝑣)) → if(𝑧 ≤ 𝑣, 𝑧, 𝑣) ∈ ℝ)
269	108	ad2antrr 738	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((((𝜑 ∧ 𝑧 ∈ ℝ⁺ ∧ 𝑣 ∈ ℝ⁺) ∧ 𝑎 ∈ ℝ) ∧ (abs‘(𝑎 − 𝐵)) < if(𝑧 ≤ 𝑣, 𝑧, 𝑣)) → 𝑧 ∈ ℝ)
270		simpr 489	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((((𝜑 ∧ 𝑧 ∈ ℝ⁺ ∧ 𝑣 ∈ ℝ⁺) ∧ 𝑎 ∈ ℝ) ∧ (abs‘(𝑎 − 𝐵)) < if(𝑧 ≤ 𝑣, 𝑧, 𝑣)) → (abs‘(𝑎 − 𝐵)) < if(𝑧 ≤ 𝑣, 𝑧, 𝑣))
271	114	ad2antrr 738	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((((𝜑 ∧ 𝑧 ∈ ℝ⁺ ∧ 𝑣 ∈ ℝ⁺) ∧ 𝑎 ∈ ℝ) ∧ (abs‘(𝑎 − 𝐵)) < if(𝑧 ≤ 𝑣, 𝑧, 𝑣)) → if(𝑧 ≤ 𝑣, 𝑧, 𝑣) ≤ 𝑧)
272	267, 268, 269, 270, 271	ltletrd 11358	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((((𝜑 ∧ 𝑧 ∈ ℝ⁺ ∧ 𝑣 ∈ ℝ⁺) ∧ 𝑎 ∈ ℝ) ∧ (abs‘(𝑎 − 𝐵)) < if(𝑧 ≤ 𝑣, 𝑧, 𝑣)) → (abs‘(𝑎 − 𝐵)) < 𝑧)
273	117	ad2antrr 738	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((((𝜑 ∧ 𝑧 ∈ ℝ⁺ ∧ 𝑣 ∈ ℝ⁺) ∧ 𝑎 ∈ ℝ) ∧ (abs‘(𝑎 − 𝐵)) < if(𝑧 ≤ 𝑣, 𝑧, 𝑣)) → 𝑣 ∈ ℝ)
274		min2 13207	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ ((𝑧 ∈ ℝ ∧ 𝑣 ∈ ℝ) → if(𝑧 ≤ 𝑣, 𝑧, 𝑣) ≤ 𝑣)
275	107, 111, 274	syl2an 607	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ ((𝑧 ∈ ℝ⁺ ∧ 𝑣 ∈ ℝ⁺) → if(𝑧 ≤ 𝑣, 𝑧, 𝑣) ≤ 𝑣)
276	275	3adant1 1146	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ((𝜑 ∧ 𝑧 ∈ ℝ⁺ ∧ 𝑣 ∈ ℝ⁺) → if(𝑧 ≤ 𝑣, 𝑧, 𝑣) ≤ 𝑣)
277	276	ad2antrr 738	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((((𝜑 ∧ 𝑧 ∈ ℝ⁺ ∧ 𝑣 ∈ ℝ⁺) ∧ 𝑎 ∈ ℝ) ∧ (abs‘(𝑎 − 𝐵)) < if(𝑧 ≤ 𝑣, 𝑧, 𝑣)) → if(𝑧 ≤ 𝑣, 𝑧, 𝑣) ≤ 𝑣)
278	267, 268, 273, 270, 277	ltletrd 11358	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((((𝜑 ∧ 𝑧 ∈ ℝ⁺ ∧ 𝑣 ∈ ℝ⁺) ∧ 𝑎 ∈ ℝ) ∧ (abs‘(𝑎 − 𝐵)) < if(𝑧 ≤ 𝑣, 𝑧, 𝑣)) → (abs‘(𝑎 − 𝐵)) < 𝑣)
279	272, 278	jca 520	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((((𝜑 ∧ 𝑧 ∈ ℝ⁺ ∧ 𝑣 ∈ ℝ⁺) ∧ 𝑎 ∈ ℝ) ∧ (abs‘(𝑎 − 𝐵)) < if(𝑧 ≤ 𝑣, 𝑧, 𝑣)) → ((abs‘(𝑎 − 𝐵)) < 𝑧 ∧ (abs‘(𝑎 − 𝐵)) < 𝑣))
280	279	ex 417	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((𝜑 ∧ 𝑧 ∈ ℝ⁺ ∧ 𝑣 ∈ ℝ⁺) ∧ 𝑎 ∈ ℝ) → ((abs‘(𝑎 − 𝐵)) < if(𝑧 ≤ 𝑣, 𝑧, 𝑣) → ((abs‘(𝑎 − 𝐵)) < 𝑧 ∧ (abs‘(𝑎 − 𝐵)) < 𝑣)))
281	261, 280	sylan2 604	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((𝜑 ∧ 𝑧 ∈ ℝ⁺ ∧ 𝑣 ∈ ℝ⁺) ∧ 𝑎 ∈ ((𝐴 ∩ (-∞(,)𝐵)) ∖ {𝐵})) → ((abs‘(𝑎 − 𝐵)) < if(𝑧 ≤ 𝑣, 𝑧, 𝑣) → ((abs‘(𝑎 − 𝐵)) < 𝑧 ∧ (abs‘(𝑎 − 𝐵)) < 𝑣)))
282	281	reximdva 3178	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝜑 ∧ 𝑧 ∈ ℝ⁺ ∧ 𝑣 ∈ ℝ⁺) → (∃𝑎 ∈ ((𝐴 ∩ (-∞(,)𝐵)) ∖ {𝐵})(abs‘(𝑎 − 𝐵)) < if(𝑧 ≤ 𝑣, 𝑧, 𝑣) → ∃𝑎 ∈ ((𝐴 ∩ (-∞(,)𝐵)) ∖ {𝐵})((abs‘(𝑎 − 𝐵)) < 𝑧 ∧ (abs‘(𝑎 − 𝐵)) < 𝑣)))
283	259, 282	mpd 16	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝜑 ∧ 𝑧 ∈ ℝ⁺ ∧ 𝑣 ∈ ℝ⁺) → ∃𝑎 ∈ ((𝐴 ∩ (-∞(,)𝐵)) ∖ {𝐵})((abs‘(𝑎 − 𝐵)) < 𝑧 ∧ (abs‘(𝑎 − 𝐵)) < 𝑣))
284	242, 243, 244, 283	syl3anc 1394	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝜑 ∧ 𝑦 ∈ ℝ⁺) ∧ 𝑧 ∈ ℝ⁺ ∧ ∀𝑤 ∈ 𝐴 ((𝑤 ≠ 𝐵 ∧ (abs‘(𝑤 − 𝐵)) < 𝑧) → (abs‘((𝐹‘𝑤) − 𝑥)) < 𝑦)) ∧ 𝑣 ∈ ℝ⁺ ∧ ∀𝑤 ∈ (𝐴 ∩ (-∞(,)𝐵))((𝑤 ≠ 𝐵 ∧ (abs‘(𝑤 − 𝐵)) < 𝑣) → (abs‘(((𝐹 ↾ (-∞(,)𝐵))‘𝑤) − 𝐿)) < 𝑦)) → ∃𝑎 ∈ ((𝐴 ∩ (-∞(,)𝐵)) ∖ {𝐵})((abs‘(𝑎 − 𝐵)) < 𝑧 ∧ (abs‘(𝑎 − 𝐵)) < 𝑣))
285		nfv 1937	. . . . . . . . . . . . . . . . . . . . 21 ⊢ Ⅎ𝑎(((𝜑 ∧ 𝑦 ∈ ℝ⁺) ∧ 𝑧 ∈ ℝ⁺ ∧ ∀𝑤 ∈ 𝐴 ((𝑤 ≠ 𝐵 ∧ (abs‘(𝑤 − 𝐵)) < 𝑧) → (abs‘((𝐹‘𝑤) − 𝑥)) < 𝑦)) ∧ 𝑣 ∈ ℝ⁺ ∧ ∀𝑤 ∈ (𝐴 ∩ (-∞(,)𝐵))((𝑤 ≠ 𝐵 ∧ (abs‘(𝑤 − 𝐵)) < 𝑣) → (abs‘(((𝐹 ↾ (-∞(,)𝐵))‘𝑤) − 𝐿)) < 𝑦))
286		nfre1 3290	. . . . . . . . . . . . . . . . . . . . 21 ⊢ Ⅎ𝑎∃𝑎 ∈ 𝐴 ((abs‘((𝐹‘𝑎) − 𝑥)) < 𝑦 ∧ (abs‘((𝐹‘𝑎) − 𝐿)) < 𝑦)
287	260	elin1d 4159	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑎 ∈ ((𝐴 ∩ (-∞(,)𝐵)) ∖ {𝐵}) → 𝑎 ∈ 𝐴)
288	287	3ad2ant2 1150	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((((𝜑 ∧ 𝑦 ∈ ℝ⁺) ∧ 𝑧 ∈ ℝ⁺ ∧ ∀𝑤 ∈ 𝐴 ((𝑤 ≠ 𝐵 ∧ (abs‘(𝑤 − 𝐵)) < 𝑧) → (abs‘((𝐹‘𝑤) − 𝑥)) < 𝑦)) ∧ 𝑣 ∈ ℝ⁺ ∧ ∀𝑤 ∈ (𝐴 ∩ (-∞(,)𝐵))((𝑤 ≠ 𝐵 ∧ (abs‘(𝑤 − 𝐵)) < 𝑣) → (abs‘(((𝐹 ↾ (-∞(,)𝐵))‘𝑤) − 𝐿)) < 𝑦)) ∧ 𝑎 ∈ ((𝐴 ∩ (-∞(,)𝐵)) ∖ {𝐵}) ∧ ((abs‘(𝑎 − 𝐵)) < 𝑧 ∧ (abs‘(𝑎 − 𝐵)) < 𝑣)) → 𝑎 ∈ 𝐴)
289		simp113 1321	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((((𝜑 ∧ 𝑦 ∈ ℝ⁺) ∧ 𝑧 ∈ ℝ⁺ ∧ ∀𝑤 ∈ 𝐴 ((𝑤 ≠ 𝐵 ∧ (abs‘(𝑤 − 𝐵)) < 𝑧) → (abs‘((𝐹‘𝑤) − 𝑥)) < 𝑦)) ∧ 𝑣 ∈ ℝ⁺ ∧ ∀𝑤 ∈ (𝐴 ∩ (-∞(,)𝐵))((𝑤 ≠ 𝐵 ∧ (abs‘(𝑤 − 𝐵)) < 𝑣) → (abs‘(((𝐹 ↾ (-∞(,)𝐵))‘𝑤) − 𝐿)) < 𝑦)) ∧ 𝑎 ∈ ((𝐴 ∩ (-∞(,)𝐵)) ∖ {𝐵}) ∧ ((abs‘(𝑎 − 𝐵)) < 𝑧 ∧ (abs‘(𝑎 − 𝐵)) < 𝑣)) → ∀𝑤 ∈ 𝐴 ((𝑤 ≠ 𝐵 ∧ (abs‘(𝑤 − 𝐵)) < 𝑧) → (abs‘((𝐹‘𝑤) − 𝑥)) < 𝑦))
290		eldifsni 4753	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝑎 ∈ ((𝐴 ∩ (-∞(,)𝐵)) ∖ {𝐵}) → 𝑎 ≠ 𝐵)
291	290	adantr 485	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((𝑎 ∈ ((𝐴 ∩ (-∞(,)𝐵)) ∖ {𝐵}) ∧ ((abs‘(𝑎 − 𝐵)) < 𝑧 ∧ (abs‘(𝑎 − 𝐵)) < 𝑣)) → 𝑎 ≠ 𝐵)
292		simprl 782	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((𝑎 ∈ ((𝐴 ∩ (-∞(,)𝐵)) ∖ {𝐵}) ∧ ((abs‘(𝑎 − 𝐵)) < 𝑧 ∧ (abs‘(𝑎 − 𝐵)) < 𝑣)) → (abs‘(𝑎 − 𝐵)) < 𝑧)
293	291, 292	jca 520	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((𝑎 ∈ ((𝐴 ∩ (-∞(,)𝐵)) ∖ {𝐵}) ∧ ((abs‘(𝑎 − 𝐵)) < 𝑧 ∧ (abs‘(𝑎 − 𝐵)) < 𝑣)) → (𝑎 ≠ 𝐵 ∧ (abs‘(𝑎 − 𝐵)) < 𝑧))
294	293	3adant1 1146	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((((𝜑 ∧ 𝑦 ∈ ℝ⁺) ∧ 𝑧 ∈ ℝ⁺ ∧ ∀𝑤 ∈ 𝐴 ((𝑤 ≠ 𝐵 ∧ (abs‘(𝑤 − 𝐵)) < 𝑧) → (abs‘((𝐹‘𝑤) − 𝑥)) < 𝑦)) ∧ 𝑣 ∈ ℝ⁺ ∧ ∀𝑤 ∈ (𝐴 ∩ (-∞(,)𝐵))((𝑤 ≠ 𝐵 ∧ (abs‘(𝑤 − 𝐵)) < 𝑣) → (abs‘(((𝐹 ↾ (-∞(,)𝐵))‘𝑤) − 𝐿)) < 𝑦)) ∧ 𝑎 ∈ ((𝐴 ∩ (-∞(,)𝐵)) ∖ {𝐵}) ∧ ((abs‘(𝑎 − 𝐵)) < 𝑧 ∧ (abs‘(𝑎 − 𝐵)) < 𝑣)) → (𝑎 ≠ 𝐵 ∧ (abs‘(𝑎 − 𝐵)) < 𝑧))
295		neeq1 3022	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (𝑤 = 𝑎 → (𝑤 ≠ 𝐵 ↔ 𝑎 ≠ 𝐵))
296		fvoveq1 7423	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (𝑤 = 𝑎 → (abs‘(𝑤 − 𝐵)) = (abs‘(𝑎 − 𝐵)))
297	296	breq1d 5115	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (𝑤 = 𝑎 → ((abs‘(𝑤 − 𝐵)) < 𝑧 ↔ (abs‘(𝑎 − 𝐵)) < 𝑧))
298	295, 297	anbi12d 643	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝑤 = 𝑎 → ((𝑤 ≠ 𝐵 ∧ (abs‘(𝑤 − 𝐵)) < 𝑧) ↔ (𝑎 ≠ 𝐵 ∧ (abs‘(𝑎 − 𝐵)) < 𝑧)))
299	298	imbrov2fvoveq 7425	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝑤 = 𝑎 → (((𝑤 ≠ 𝐵 ∧ (abs‘(𝑤 − 𝐵)) < 𝑧) → (abs‘((𝐹‘𝑤) − 𝑥)) < 𝑦) ↔ ((𝑎 ≠ 𝐵 ∧ (abs‘(𝑎 − 𝐵)) < 𝑧) → (abs‘((𝐹‘𝑎) − 𝑥)) < 𝑦)))
300	299	rspcva 3582	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((𝑎 ∈ 𝐴 ∧ ∀𝑤 ∈ 𝐴 ((𝑤 ≠ 𝐵 ∧ (abs‘(𝑤 − 𝐵)) < 𝑧) → (abs‘((𝐹‘𝑤) − 𝑥)) < 𝑦)) → ((𝑎 ≠ 𝐵 ∧ (abs‘(𝑎 − 𝐵)) < 𝑧) → (abs‘((𝐹‘𝑎) − 𝑥)) < 𝑦))
301	300	imp 411	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((𝑎 ∈ 𝐴 ∧ ∀𝑤 ∈ 𝐴 ((𝑤 ≠ 𝐵 ∧ (abs‘(𝑤 − 𝐵)) < 𝑧) → (abs‘((𝐹‘𝑤) − 𝑥)) < 𝑦)) ∧ (𝑎 ≠ 𝐵 ∧ (abs‘(𝑎 − 𝐵)) < 𝑧)) → (abs‘((𝐹‘𝑎) − 𝑥)) < 𝑦)
302	288, 289, 294, 301	syl21anc 850	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((((𝜑 ∧ 𝑦 ∈ ℝ⁺) ∧ 𝑧 ∈ ℝ⁺ ∧ ∀𝑤 ∈ 𝐴 ((𝑤 ≠ 𝐵 ∧ (abs‘(𝑤 − 𝐵)) < 𝑧) → (abs‘((𝐹‘𝑤) − 𝑥)) < 𝑦)) ∧ 𝑣 ∈ ℝ⁺ ∧ ∀𝑤 ∈ (𝐴 ∩ (-∞(,)𝐵))((𝑤 ≠ 𝐵 ∧ (abs‘(𝑤 − 𝐵)) < 𝑣) → (abs‘(((𝐹 ↾ (-∞(,)𝐵))‘𝑤) − 𝐿)) < 𝑦)) ∧ 𝑎 ∈ ((𝐴 ∩ (-∞(,)𝐵)) ∖ {𝐵}) ∧ ((abs‘(𝑎 − 𝐵)) < 𝑧 ∧ (abs‘(𝑎 − 𝐵)) < 𝑣)) → (abs‘((𝐹‘𝑎) − 𝑥)) < 𝑦)
303	260	3ad2ant2 1150	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((((𝜑 ∧ 𝑦 ∈ ℝ⁺) ∧ 𝑧 ∈ ℝ⁺ ∧ ∀𝑤 ∈ 𝐴 ((𝑤 ≠ 𝐵 ∧ (abs‘(𝑤 − 𝐵)) < 𝑧) → (abs‘((𝐹‘𝑤) − 𝑥)) < 𝑦)) ∧ 𝑣 ∈ ℝ⁺ ∧ ∀𝑤 ∈ (𝐴 ∩ (-∞(,)𝐵))((𝑤 ≠ 𝐵 ∧ (abs‘(𝑤 − 𝐵)) < 𝑣) → (abs‘(((𝐹 ↾ (-∞(,)𝐵))‘𝑤) − 𝐿)) < 𝑦)) ∧ 𝑎 ∈ ((𝐴 ∩ (-∞(,)𝐵)) ∖ {𝐵}) ∧ ((abs‘(𝑎 − 𝐵)) < 𝑧 ∧ (abs‘(𝑎 − 𝐵)) < 𝑣)) → 𝑎 ∈ (𝐴 ∩ (-∞(,)𝐵)))
304	242	3ad2ant1 1149	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((((𝜑 ∧ 𝑦 ∈ ℝ⁺) ∧ 𝑧 ∈ ℝ⁺ ∧ ∀𝑤 ∈ 𝐴 ((𝑤 ≠ 𝐵 ∧ (abs‘(𝑤 − 𝐵)) < 𝑧) → (abs‘((𝐹‘𝑤) − 𝑥)) < 𝑦)) ∧ 𝑣 ∈ ℝ⁺ ∧ ∀𝑤 ∈ (𝐴 ∩ (-∞(,)𝐵))((𝑤 ≠ 𝐵 ∧ (abs‘(𝑤 − 𝐵)) < 𝑣) → (abs‘(((𝐹 ↾ (-∞(,)𝐵))‘𝑤) − 𝐿)) < 𝑦)) ∧ 𝑎 ∈ ((𝐴 ∩ (-∞(,)𝐵)) ∖ {𝐵}) ∧ ((abs‘(𝑎 − 𝐵)) < 𝑧 ∧ (abs‘(𝑎 − 𝐵)) < 𝑣)) → 𝜑)
305		simp13 1222	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((((𝜑 ∧ 𝑦 ∈ ℝ⁺) ∧ 𝑧 ∈ ℝ⁺ ∧ ∀𝑤 ∈ 𝐴 ((𝑤 ≠ 𝐵 ∧ (abs‘(𝑤 − 𝐵)) < 𝑧) → (abs‘((𝐹‘𝑤) − 𝑥)) < 𝑦)) ∧ 𝑣 ∈ ℝ⁺ ∧ ∀𝑤 ∈ (𝐴 ∩ (-∞(,)𝐵))((𝑤 ≠ 𝐵 ∧ (abs‘(𝑤 − 𝐵)) < 𝑣) → (abs‘(((𝐹 ↾ (-∞(,)𝐵))‘𝑤) − 𝐿)) < 𝑦)) ∧ 𝑎 ∈ ((𝐴 ∩ (-∞(,)𝐵)) ∖ {𝐵}) ∧ ((abs‘(𝑎 − 𝐵)) < 𝑧 ∧ (abs‘(𝑎 − 𝐵)) < 𝑣)) → ∀𝑤 ∈ (𝐴 ∩ (-∞(,)𝐵))((𝑤 ≠ 𝐵 ∧ (abs‘(𝑤 − 𝐵)) < 𝑣) → (abs‘(((𝐹 ↾ (-∞(,)𝐵))‘𝑤) − 𝐿)) < 𝑦))
306		nfra1 3289	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ Ⅎ𝑤∀𝑤 ∈ (𝐴 ∩ (-∞(,)𝐵))((𝑤 ≠ 𝐵 ∧ (abs‘(𝑤 − 𝐵)) < 𝑣) → (abs‘(((𝐹 ↾ (-∞(,)𝐵))‘𝑤) − 𝐿)) < 𝑦)
307	148, 306	nfan 1922	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ Ⅎ𝑤(𝜑 ∧ ∀𝑤 ∈ (𝐴 ∩ (-∞(,)𝐵))((𝑤 ≠ 𝐵 ∧ (abs‘(𝑤 − 𝐵)) < 𝑣) → (abs‘(((𝐹 ↾ (-∞(,)𝐵))‘𝑤) − 𝐿)) < 𝑦))
308		elinel2 4157	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ (𝑤 ∈ (𝐴 ∩ (-∞(,)𝐵)) → 𝑤 ∈ (-∞(,)𝐵))
309	308	fvresd 6891	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ (𝑤 ∈ (𝐴 ∩ (-∞(,)𝐵)) → ((𝐹 ↾ (-∞(,)𝐵))‘𝑤) = (𝐹‘𝑤))
310	309	eqcomd 2771	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ (𝑤 ∈ (𝐴 ∩ (-∞(,)𝐵)) → (𝐹‘𝑤) = ((𝐹 ↾ (-∞(,)𝐵))‘𝑤))
311	310	fvoveq1d 7422	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (𝑤 ∈ (𝐴 ∩ (-∞(,)𝐵)) → (abs‘((𝐹‘𝑤) − 𝐿)) = (abs‘(((𝐹 ↾ (-∞(,)𝐵))‘𝑤) − 𝐿)))
312	311	3ad2ant2 1150	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (((𝜑 ∧ ∀𝑤 ∈ (𝐴 ∩ (-∞(,)𝐵))((𝑤 ≠ 𝐵 ∧ (abs‘(𝑤 − 𝐵)) < 𝑣) → (abs‘(((𝐹 ↾ (-∞(,)𝐵))‘𝑤) − 𝐿)) < 𝑦)) ∧ 𝑤 ∈ (𝐴 ∩ (-∞(,)𝐵)) ∧ (𝑤 ≠ 𝐵 ∧ (abs‘(𝑤 − 𝐵)) < 𝑣)) → (abs‘((𝐹‘𝑤) − 𝐿)) = (abs‘(((𝐹 ↾ (-∞(,)𝐵))‘𝑤) − 𝐿)))
313		rspa 3254	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ ((∀𝑤 ∈ (𝐴 ∩ (-∞(,)𝐵))((𝑤 ≠ 𝐵 ∧ (abs‘(𝑤 − 𝐵)) < 𝑣) → (abs‘(((𝐹 ↾ (-∞(,)𝐵))‘𝑤) − 𝐿)) < 𝑦) ∧ 𝑤 ∈ (𝐴 ∩ (-∞(,)𝐵))) → ((𝑤 ≠ 𝐵 ∧ (abs‘(𝑤 − 𝐵)) < 𝑣) → (abs‘(((𝐹 ↾ (-∞(,)𝐵))‘𝑤) − 𝐿)) < 𝑦))
314	313	3impia 1133	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ ((∀𝑤 ∈ (𝐴 ∩ (-∞(,)𝐵))((𝑤 ≠ 𝐵 ∧ (abs‘(𝑤 − 𝐵)) < 𝑣) → (abs‘(((𝐹 ↾ (-∞(,)𝐵))‘𝑤) − 𝐿)) < 𝑦) ∧ 𝑤 ∈ (𝐴 ∩ (-∞(,)𝐵)) ∧ (𝑤 ≠ 𝐵 ∧ (abs‘(𝑤 − 𝐵)) < 𝑣)) → (abs‘(((𝐹 ↾ (-∞(,)𝐵))‘𝑤) − 𝐿)) < 𝑦)
315	314	3adant1l 1193	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (((𝜑 ∧ ∀𝑤 ∈ (𝐴 ∩ (-∞(,)𝐵))((𝑤 ≠ 𝐵 ∧ (abs‘(𝑤 − 𝐵)) < 𝑣) → (abs‘(((𝐹 ↾ (-∞(,)𝐵))‘𝑤) − 𝐿)) < 𝑦)) ∧ 𝑤 ∈ (𝐴 ∩ (-∞(,)𝐵)) ∧ (𝑤 ≠ 𝐵 ∧ (abs‘(𝑤 − 𝐵)) < 𝑣)) → (abs‘(((𝐹 ↾ (-∞(,)𝐵))‘𝑤) − 𝐿)) < 𝑦)
316	312, 315	eqbrtrd 5127	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (((𝜑 ∧ ∀𝑤 ∈ (𝐴 ∩ (-∞(,)𝐵))((𝑤 ≠ 𝐵 ∧ (abs‘(𝑤 − 𝐵)) < 𝑣) → (abs‘(((𝐹 ↾ (-∞(,)𝐵))‘𝑤) − 𝐿)) < 𝑦)) ∧ 𝑤 ∈ (𝐴 ∩ (-∞(,)𝐵)) ∧ (𝑤 ≠ 𝐵 ∧ (abs‘(𝑤 − 𝐵)) < 𝑣)) → (abs‘((𝐹‘𝑤) − 𝐿)) < 𝑦)
317	316	3exp 1135	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((𝜑 ∧ ∀𝑤 ∈ (𝐴 ∩ (-∞(,)𝐵))((𝑤 ≠ 𝐵 ∧ (abs‘(𝑤 − 𝐵)) < 𝑣) → (abs‘(((𝐹 ↾ (-∞(,)𝐵))‘𝑤) − 𝐿)) < 𝑦)) → (𝑤 ∈ (𝐴 ∩ (-∞(,)𝐵)) → ((𝑤 ≠ 𝐵 ∧ (abs‘(𝑤 − 𝐵)) < 𝑣) → (abs‘((𝐹‘𝑤) − 𝐿)) < 𝑦)))
318	307, 317	ralrimi 3263	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((𝜑 ∧ ∀𝑤 ∈ (𝐴 ∩ (-∞(,)𝐵))((𝑤 ≠ 𝐵 ∧ (abs‘(𝑤 − 𝐵)) < 𝑣) → (abs‘(((𝐹 ↾ (-∞(,)𝐵))‘𝑤) − 𝐿)) < 𝑦)) → ∀𝑤 ∈ (𝐴 ∩ (-∞(,)𝐵))((𝑤 ≠ 𝐵 ∧ (abs‘(𝑤 − 𝐵)) < 𝑣) → (abs‘((𝐹‘𝑤) − 𝐿)) < 𝑦))
319	304, 305, 318	syl2anc 595	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((((𝜑 ∧ 𝑦 ∈ ℝ⁺) ∧ 𝑧 ∈ ℝ⁺ ∧ ∀𝑤 ∈ 𝐴 ((𝑤 ≠ 𝐵 ∧ (abs‘(𝑤 − 𝐵)) < 𝑧) → (abs‘((𝐹‘𝑤) − 𝑥)) < 𝑦)) ∧ 𝑣 ∈ ℝ⁺ ∧ ∀𝑤 ∈ (𝐴 ∩ (-∞(,)𝐵))((𝑤 ≠ 𝐵 ∧ (abs‘(𝑤 − 𝐵)) < 𝑣) → (abs‘(((𝐹 ↾ (-∞(,)𝐵))‘𝑤) − 𝐿)) < 𝑦)) ∧ 𝑎 ∈ ((𝐴 ∩ (-∞(,)𝐵)) ∖ {𝐵}) ∧ ((abs‘(𝑎 − 𝐵)) < 𝑧 ∧ (abs‘(𝑎 − 𝐵)) < 𝑣)) → ∀𝑤 ∈ (𝐴 ∩ (-∞(,)𝐵))((𝑤 ≠ 𝐵 ∧ (abs‘(𝑤 − 𝐵)) < 𝑣) → (abs‘((𝐹‘𝑤) − 𝐿)) < 𝑦))
320	290	anim1i 626	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((𝑎 ∈ ((𝐴 ∩ (-∞(,)𝐵)) ∖ {𝐵}) ∧ (abs‘(𝑎 − 𝐵)) < 𝑣) → (𝑎 ≠ 𝐵 ∧ (abs‘(𝑎 − 𝐵)) < 𝑣))
321	320	adantrl 728	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((𝑎 ∈ ((𝐴 ∩ (-∞(,)𝐵)) ∖ {𝐵}) ∧ ((abs‘(𝑎 − 𝐵)) < 𝑧 ∧ (abs‘(𝑎 − 𝐵)) < 𝑣)) → (𝑎 ≠ 𝐵 ∧ (abs‘(𝑎 − 𝐵)) < 𝑣))
322	321	3adant1 1146	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((((𝜑 ∧ 𝑦 ∈ ℝ⁺) ∧ 𝑧 ∈ ℝ⁺ ∧ ∀𝑤 ∈ 𝐴 ((𝑤 ≠ 𝐵 ∧ (abs‘(𝑤 − 𝐵)) < 𝑧) → (abs‘((𝐹‘𝑤) − 𝑥)) < 𝑦)) ∧ 𝑣 ∈ ℝ⁺ ∧ ∀𝑤 ∈ (𝐴 ∩ (-∞(,)𝐵))((𝑤 ≠ 𝐵 ∧ (abs‘(𝑤 − 𝐵)) < 𝑣) → (abs‘(((𝐹 ↾ (-∞(,)𝐵))‘𝑤) − 𝐿)) < 𝑦)) ∧ 𝑎 ∈ ((𝐴 ∩ (-∞(,)𝐵)) ∖ {𝐵}) ∧ ((abs‘(𝑎 − 𝐵)) < 𝑧 ∧ (abs‘(𝑎 − 𝐵)) < 𝑣)) → (𝑎 ≠ 𝐵 ∧ (abs‘(𝑎 − 𝐵)) < 𝑣))
323	296	breq1d 5115	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (𝑤 = 𝑎 → ((abs‘(𝑤 − 𝐵)) < 𝑣 ↔ (abs‘(𝑎 − 𝐵)) < 𝑣))
324	295, 323	anbi12d 643	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝑤 = 𝑎 → ((𝑤 ≠ 𝐵 ∧ (abs‘(𝑤 − 𝐵)) < 𝑣) ↔ (𝑎 ≠ 𝐵 ∧ (abs‘(𝑎 − 𝐵)) < 𝑣)))
325	324	imbrov2fvoveq 7425	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝑤 = 𝑎 → (((𝑤 ≠ 𝐵 ∧ (abs‘(𝑤 − 𝐵)) < 𝑣) → (abs‘((𝐹‘𝑤) − 𝐿)) < 𝑦) ↔ ((𝑎 ≠ 𝐵 ∧ (abs‘(𝑎 − 𝐵)) < 𝑣) → (abs‘((𝐹‘𝑎) − 𝐿)) < 𝑦)))
326	325	rspcva 3582	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((𝑎 ∈ (𝐴 ∩ (-∞(,)𝐵)) ∧ ∀𝑤 ∈ (𝐴 ∩ (-∞(,)𝐵))((𝑤 ≠ 𝐵 ∧ (abs‘(𝑤 − 𝐵)) < 𝑣) → (abs‘((𝐹‘𝑤) − 𝐿)) < 𝑦)) → ((𝑎 ≠ 𝐵 ∧ (abs‘(𝑎 − 𝐵)) < 𝑣) → (abs‘((𝐹‘𝑎) − 𝐿)) < 𝑦))
327	326	imp 411	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((𝑎 ∈ (𝐴 ∩ (-∞(,)𝐵)) ∧ ∀𝑤 ∈ (𝐴 ∩ (-∞(,)𝐵))((𝑤 ≠ 𝐵 ∧ (abs‘(𝑤 − 𝐵)) < 𝑣) → (abs‘((𝐹‘𝑤) − 𝐿)) < 𝑦)) ∧ (𝑎 ≠ 𝐵 ∧ (abs‘(𝑎 − 𝐵)) < 𝑣)) → (abs‘((𝐹‘𝑎) − 𝐿)) < 𝑦)
328	303, 319, 322, 327	syl21anc 850	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((((𝜑 ∧ 𝑦 ∈ ℝ⁺) ∧ 𝑧 ∈ ℝ⁺ ∧ ∀𝑤 ∈ 𝐴 ((𝑤 ≠ 𝐵 ∧ (abs‘(𝑤 − 𝐵)) < 𝑧) → (abs‘((𝐹‘𝑤) − 𝑥)) < 𝑦)) ∧ 𝑣 ∈ ℝ⁺ ∧ ∀𝑤 ∈ (𝐴 ∩ (-∞(,)𝐵))((𝑤 ≠ 𝐵 ∧ (abs‘(𝑤 − 𝐵)) < 𝑣) → (abs‘(((𝐹 ↾ (-∞(,)𝐵))‘𝑤) − 𝐿)) < 𝑦)) ∧ 𝑎 ∈ ((𝐴 ∩ (-∞(,)𝐵)) ∖ {𝐵}) ∧ ((abs‘(𝑎 − 𝐵)) < 𝑧 ∧ (abs‘(𝑎 − 𝐵)) < 𝑣)) → (abs‘((𝐹‘𝑎) − 𝐿)) < 𝑦)
329		rspe 3255	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝑎 ∈ 𝐴 ∧ ((abs‘((𝐹‘𝑎) − 𝑥)) < 𝑦 ∧ (abs‘((𝐹‘𝑎) − 𝐿)) < 𝑦)) → ∃𝑎 ∈ 𝐴 ((abs‘((𝐹‘𝑎) − 𝑥)) < 𝑦 ∧ (abs‘((𝐹‘𝑎) − 𝐿)) < 𝑦))
330	288, 302, 328, 329	syl12anc 849	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((((𝜑 ∧ 𝑦 ∈ ℝ⁺) ∧ 𝑧 ∈ ℝ⁺ ∧ ∀𝑤 ∈ 𝐴 ((𝑤 ≠ 𝐵 ∧ (abs‘(𝑤 − 𝐵)) < 𝑧) → (abs‘((𝐹‘𝑤) − 𝑥)) < 𝑦)) ∧ 𝑣 ∈ ℝ⁺ ∧ ∀𝑤 ∈ (𝐴 ∩ (-∞(,)𝐵))((𝑤 ≠ 𝐵 ∧ (abs‘(𝑤 − 𝐵)) < 𝑣) → (abs‘(((𝐹 ↾ (-∞(,)𝐵))‘𝑤) − 𝐿)) < 𝑦)) ∧ 𝑎 ∈ ((𝐴 ∩ (-∞(,)𝐵)) ∖ {𝐵}) ∧ ((abs‘(𝑎 − 𝐵)) < 𝑧 ∧ (abs‘(𝑎 − 𝐵)) < 𝑣)) → ∃𝑎 ∈ 𝐴 ((abs‘((𝐹‘𝑎) − 𝑥)) < 𝑦 ∧ (abs‘((𝐹‘𝑎) − 𝐿)) < 𝑦))
331	330	3exp 1135	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((𝜑 ∧ 𝑦 ∈ ℝ⁺) ∧ 𝑧 ∈ ℝ⁺ ∧ ∀𝑤 ∈ 𝐴 ((𝑤 ≠ 𝐵 ∧ (abs‘(𝑤 − 𝐵)) < 𝑧) → (abs‘((𝐹‘𝑤) − 𝑥)) < 𝑦)) ∧ 𝑣 ∈ ℝ⁺ ∧ ∀𝑤 ∈ (𝐴 ∩ (-∞(,)𝐵))((𝑤 ≠ 𝐵 ∧ (abs‘(𝑤 − 𝐵)) < 𝑣) → (abs‘(((𝐹 ↾ (-∞(,)𝐵))‘𝑤) − 𝐿)) < 𝑦)) → (𝑎 ∈ ((𝐴 ∩ (-∞(,)𝐵)) ∖ {𝐵}) → (((abs‘(𝑎 − 𝐵)) < 𝑧 ∧ (abs‘(𝑎 − 𝐵)) < 𝑣) → ∃𝑎 ∈ 𝐴 ((abs‘((𝐹‘𝑎) − 𝑥)) < 𝑦 ∧ (abs‘((𝐹‘𝑎) − 𝐿)) < 𝑦))))
332	285, 286, 331	rexlimd 3272	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝜑 ∧ 𝑦 ∈ ℝ⁺) ∧ 𝑧 ∈ ℝ⁺ ∧ ∀𝑤 ∈ 𝐴 ((𝑤 ≠ 𝐵 ∧ (abs‘(𝑤 − 𝐵)) < 𝑧) → (abs‘((𝐹‘𝑤) − 𝑥)) < 𝑦)) ∧ 𝑣 ∈ ℝ⁺ ∧ ∀𝑤 ∈ (𝐴 ∩ (-∞(,)𝐵))((𝑤 ≠ 𝐵 ∧ (abs‘(𝑤 − 𝐵)) < 𝑣) → (abs‘(((𝐹 ↾ (-∞(,)𝐵))‘𝑤) − 𝐿)) < 𝑦)) → (∃𝑎 ∈ ((𝐴 ∩ (-∞(,)𝐵)) ∖ {𝐵})((abs‘(𝑎 − 𝐵)) < 𝑧 ∧ (abs‘(𝑎 − 𝐵)) < 𝑣) → ∃𝑎 ∈ 𝐴 ((abs‘((𝐹‘𝑎) − 𝑥)) < 𝑦 ∧ (abs‘((𝐹‘𝑎) − 𝐿)) < 𝑦)))
333	284, 332	mpd 16	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝜑 ∧ 𝑦 ∈ ℝ⁺) ∧ 𝑧 ∈ ℝ⁺ ∧ ∀𝑤 ∈ 𝐴 ((𝑤 ≠ 𝐵 ∧ (abs‘(𝑤 − 𝐵)) < 𝑧) → (abs‘((𝐹‘𝑤) − 𝑥)) < 𝑦)) ∧ 𝑣 ∈ ℝ⁺ ∧ ∀𝑤 ∈ (𝐴 ∩ (-∞(,)𝐵))((𝑤 ≠ 𝐵 ∧ (abs‘(𝑤 − 𝐵)) < 𝑣) → (abs‘(((𝐹 ↾ (-∞(,)𝐵))‘𝑤) − 𝐿)) < 𝑦)) → ∃𝑎 ∈ 𝐴 ((abs‘((𝐹‘𝑎) − 𝑥)) < 𝑦 ∧ (abs‘((𝐹‘𝑎) − 𝐿)) < 𝑦))
334	333	3exp 1135	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑦 ∈ ℝ⁺) ∧ 𝑧 ∈ ℝ⁺ ∧ ∀𝑤 ∈ 𝐴 ((𝑤 ≠ 𝐵 ∧ (abs‘(𝑤 − 𝐵)) < 𝑧) → (abs‘((𝐹‘𝑤) − 𝑥)) < 𝑦)) → (𝑣 ∈ ℝ⁺ → (∀𝑤 ∈ (𝐴 ∩ (-∞(,)𝐵))((𝑤 ≠ 𝐵 ∧ (abs‘(𝑤 − 𝐵)) < 𝑣) → (abs‘(((𝐹 ↾ (-∞(,)𝐵))‘𝑤) − 𝐿)) < 𝑦) → ∃𝑎 ∈ 𝐴 ((abs‘((𝐹‘𝑎) − 𝑥)) < 𝑦 ∧ (abs‘((𝐹‘𝑎) − 𝐿)) < 𝑦))))
335	334	rexlimdv 3164	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑦 ∈ ℝ⁺) ∧ 𝑧 ∈ ℝ⁺ ∧ ∀𝑤 ∈ 𝐴 ((𝑤 ≠ 𝐵 ∧ (abs‘(𝑤 − 𝐵)) < 𝑧) → (abs‘((𝐹‘𝑤) − 𝑥)) < 𝑦)) → (∃𝑣 ∈ ℝ⁺ ∀𝑤 ∈ (𝐴 ∩ (-∞(,)𝐵))((𝑤 ≠ 𝐵 ∧ (abs‘(𝑤 − 𝐵)) < 𝑣) → (abs‘(((𝐹 ↾ (-∞(,)𝐵))‘𝑤) − 𝐿)) < 𝑦) → ∃𝑎 ∈ 𝐴 ((abs‘((𝐹‘𝑎) − 𝑥)) < 𝑦 ∧ (abs‘((𝐹‘𝑎) − 𝐿)) < 𝑦)))
336	241, 335	mpd 16	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑦 ∈ ℝ⁺) ∧ 𝑧 ∈ ℝ⁺ ∧ ∀𝑤 ∈ 𝐴 ((𝑤 ≠ 𝐵 ∧ (abs‘(𝑤 − 𝐵)) < 𝑧) → (abs‘((𝐹‘𝑤) − 𝑥)) < 𝑦)) → ∃𝑎 ∈ 𝐴 ((abs‘((𝐹‘𝑎) − 𝑥)) < 𝑦 ∧ (abs‘((𝐹‘𝑎) − 𝐿)) < 𝑦))
337	336	3exp 1135	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑦 ∈ ℝ⁺) → (𝑧 ∈ ℝ⁺ → (∀𝑤 ∈ 𝐴 ((𝑤 ≠ 𝐵 ∧ (abs‘(𝑤 − 𝐵)) < 𝑧) → (abs‘((𝐹‘𝑤) − 𝑥)) < 𝑦) → ∃𝑎 ∈ 𝐴 ((abs‘((𝐹‘𝑎) − 𝑥)) < 𝑦 ∧ (abs‘((𝐹‘𝑎) − 𝐿)) < 𝑦))))
338	337	rexlimdv 3164	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑦 ∈ ℝ⁺) → (∃𝑧 ∈ ℝ⁺ ∀𝑤 ∈ 𝐴 ((𝑤 ≠ 𝐵 ∧ (abs‘(𝑤 − 𝐵)) < 𝑧) → (abs‘((𝐹‘𝑤) − 𝑥)) < 𝑦) → ∃𝑎 ∈ 𝐴 ((abs‘((𝐹‘𝑎) − 𝑥)) < 𝑦 ∧ (abs‘((𝐹‘𝑎) − 𝐿)) < 𝑦)))
339	338	imp 411	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑦 ∈ ℝ⁺) ∧ ∃𝑧 ∈ ℝ⁺ ∀𝑤 ∈ 𝐴 ((𝑤 ≠ 𝐵 ∧ (abs‘(𝑤 − 𝐵)) < 𝑧) → (abs‘((𝐹‘𝑤) − 𝑥)) < 𝑦)) → ∃𝑎 ∈ 𝐴 ((abs‘((𝐹‘𝑎) − 𝑥)) < 𝑦 ∧ (abs‘((𝐹‘𝑎) − 𝐿)) < 𝑦))
340	339	adantllr 731	. . . . . . . . . . . 12 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℂ) ∧ 𝑦 ∈ ℝ⁺) ∧ ∃𝑧 ∈ ℝ⁺ ∀𝑤 ∈ 𝐴 ((𝑤 ≠ 𝐵 ∧ (abs‘(𝑤 − 𝐵)) < 𝑧) → (abs‘((𝐹‘𝑤) − 𝑥)) < 𝑦)) → ∃𝑎 ∈ 𝐴 ((abs‘((𝐹‘𝑎) − 𝑥)) < 𝑦 ∧ (abs‘((𝐹‘𝑎) − 𝐿)) < 𝑦))
341	231, 340	reximddv3 3182	. . . . . . . . . . 11 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℂ) ∧ 𝑦 ∈ ℝ⁺) ∧ ∃𝑧 ∈ ℝ⁺ ∀𝑤 ∈ 𝐴 ((𝑤 ≠ 𝐵 ∧ (abs‘(𝑤 − 𝐵)) < 𝑧) → (abs‘((𝐹‘𝑤) − 𝑥)) < 𝑦)) → ∃𝑎 ∈ 𝐴 ∃𝑏 ∈ 𝐴 (abs‘(𝑅 − 𝐿)) < (4 · 𝑦))
342	32, 33, 35, 341	syl21anc 850	. . . . . . . . . 10 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℂ) ∧ ∀𝑦 ∈ ℝ⁺ ∃𝑧 ∈ ℝ⁺ ∀𝑤 ∈ 𝐴 ((𝑤 ≠ 𝐵 ∧ (abs‘(𝑤 − 𝐵)) < 𝑧) → (abs‘((𝐹‘𝑤) − 𝑥)) < 𝑦)) ∧ 𝑦 ∈ ℝ⁺) → ∃𝑎 ∈ 𝐴 ∃𝑏 ∈ 𝐴 (abs‘(𝑅 − 𝐿)) < (4 · 𝑦))
343	342	ex 417	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑥 ∈ ℂ) ∧ ∀𝑦 ∈ ℝ⁺ ∃𝑧 ∈ ℝ⁺ ∀𝑤 ∈ 𝐴 ((𝑤 ≠ 𝐵 ∧ (abs‘(𝑤 − 𝐵)) < 𝑧) → (abs‘((𝐹‘𝑤) − 𝑥)) < 𝑦)) → (𝑦 ∈ ℝ⁺ → ∃𝑎 ∈ 𝐴 ∃𝑏 ∈ 𝐴 (abs‘(𝑅 − 𝐿)) < (4 · 𝑦)))
344	24, 25, 31, 343	vtoclf 3533	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑥 ∈ ℂ) ∧ ∀𝑦 ∈ ℝ⁺ ∃𝑧 ∈ ℝ⁺ ∀𝑤 ∈ 𝐴 ((𝑤 ≠ 𝐵 ∧ (abs‘(𝑤 − 𝐵)) < 𝑧) → (abs‘((𝐹‘𝑤) − 𝑥)) < 𝑦)) → (((abs‘(𝑅 − 𝐿)) / 4) ∈ ℝ⁺ → ∃𝑎 ∈ 𝐴 ∃𝑏 ∈ 𝐴 (abs‘(𝑅 − 𝐿)) < (4 · ((abs‘(𝑅 − 𝐿)) / 4))))
345	19, 344	mpd 16	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑥 ∈ ℂ) ∧ ∀𝑦 ∈ ℝ⁺ ∃𝑧 ∈ ℝ⁺ ∀𝑤 ∈ 𝐴 ((𝑤 ≠ 𝐵 ∧ (abs‘(𝑤 − 𝐵)) < 𝑧) → (abs‘((𝐹‘𝑤) − 𝑥)) < 𝑦)) → ∃𝑎 ∈ 𝐴 ∃𝑏 ∈ 𝐴 (abs‘(𝑅 − 𝐿)) < (4 · ((abs‘(𝑅 − 𝐿)) / 4)))
346		simpr 489	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (abs‘(𝑅 − 𝐿)) < (4 · ((abs‘(𝑅 − 𝐿)) / 4))) → (abs‘(𝑅 − 𝐿)) < (4 · ((abs‘(𝑅 − 𝐿)) / 4)))
347		abssubrp 45853	. . . . . . . . . . . . . . . 16 ⊢ ((𝑅 ∈ ℂ ∧ 𝐿 ∈ ℂ ∧ 𝑅 ≠ 𝐿) → (abs‘(𝑅 − 𝐿)) ∈ ℝ⁺)
348	3, 7, 11, 347	syl3anc 1394	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (abs‘(𝑅 − 𝐿)) ∈ ℝ⁺)
349	348	rpcnd 13053	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (abs‘(𝑅 − 𝐿)) ∈ ℂ)
350	349	adantr 485	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ (abs‘(𝑅 − 𝐿)) < (4 · ((abs‘(𝑅 − 𝐿)) / 4))) → (abs‘(𝑅 − 𝐿)) ∈ ℂ)
351		4cn 12317	. . . . . . . . . . . . . 14 ⊢ 4 ∈ ℂ
352	351	a1i 11	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ (abs‘(𝑅 − 𝐿)) < (4 · ((abs‘(𝑅 − 𝐿)) / 4))) → 4 ∈ ℂ)
353		4ne0 12343	. . . . . . . . . . . . . 14 ⊢ 4 ≠ 0
354	353	a1i 11	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ (abs‘(𝑅 − 𝐿)) < (4 · ((abs‘(𝑅 − 𝐿)) / 4))) → 4 ≠ 0)
355	350, 352, 354	divcan2d 11984	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (abs‘(𝑅 − 𝐿)) < (4 · ((abs‘(𝑅 − 𝐿)) / 4))) → (4 · ((abs‘(𝑅 − 𝐿)) / 4)) = (abs‘(𝑅 − 𝐿)))
356	346, 355	breqtrd 5131	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (abs‘(𝑅 − 𝐿)) < (4 · ((abs‘(𝑅 − 𝐿)) / 4))) → (abs‘(𝑅 − 𝐿)) < (abs‘(𝑅 − 𝐿)))
357	356	ex 417	. . . . . . . . . 10 ⊢ (𝜑 → ((abs‘(𝑅 − 𝐿)) < (4 · ((abs‘(𝑅 − 𝐿)) / 4)) → (abs‘(𝑅 − 𝐿)) < (abs‘(𝑅 − 𝐿))))
358	357	a1d 26	. . . . . . . . 9 ⊢ (𝜑 → ((𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐴) → ((abs‘(𝑅 − 𝐿)) < (4 · ((abs‘(𝑅 − 𝐿)) / 4)) → (abs‘(𝑅 − 𝐿)) < (abs‘(𝑅 − 𝐿)))))
359	358	ad2antrr 738	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑥 ∈ ℂ) ∧ ∀𝑦 ∈ ℝ⁺ ∃𝑧 ∈ ℝ⁺ ∀𝑤 ∈ 𝐴 ((𝑤 ≠ 𝐵 ∧ (abs‘(𝑤 − 𝐵)) < 𝑧) → (abs‘((𝐹‘𝑤) − 𝑥)) < 𝑦)) → ((𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐴) → ((abs‘(𝑅 − 𝐿)) < (4 · ((abs‘(𝑅 − 𝐿)) / 4)) → (abs‘(𝑅 − 𝐿)) < (abs‘(𝑅 − 𝐿)))))
360	359	rexlimdvv 3221	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑥 ∈ ℂ) ∧ ∀𝑦 ∈ ℝ⁺ ∃𝑧 ∈ ℝ⁺ ∀𝑤 ∈ 𝐴 ((𝑤 ≠ 𝐵 ∧ (abs‘(𝑤 − 𝐵)) < 𝑧) → (abs‘((𝐹‘𝑤) − 𝑥)) < 𝑦)) → (∃𝑎 ∈ 𝐴 ∃𝑏 ∈ 𝐴 (abs‘(𝑅 − 𝐿)) < (4 · ((abs‘(𝑅 − 𝐿)) / 4)) → (abs‘(𝑅 − 𝐿)) < (abs‘(𝑅 − 𝐿))))
361	345, 360	mpd 16	. . . . . 6 ⊢ (((𝜑 ∧ 𝑥 ∈ ℂ) ∧ ∀𝑦 ∈ ℝ⁺ ∃𝑧 ∈ ℝ⁺ ∀𝑤 ∈ 𝐴 ((𝑤 ≠ 𝐵 ∧ (abs‘(𝑤 − 𝐵)) < 𝑧) → (abs‘((𝐹‘𝑤) − 𝑥)) < 𝑦)) → (abs‘(𝑅 − 𝐿)) < (abs‘(𝑅 − 𝐿)))
362	9	abscld 15480	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑥 ∈ ℂ) ∧ ∀𝑦 ∈ ℝ⁺ ∃𝑧 ∈ ℝ⁺ ∀𝑤 ∈ 𝐴 ((𝑤 ≠ 𝐵 ∧ (abs‘(𝑤 − 𝐵)) < 𝑧) → (abs‘((𝐹‘𝑤) − 𝑥)) < 𝑦)) → (abs‘(𝑅 − 𝐿)) ∈ ℝ)
363	362	ltnrd 11332	. . . . . 6 ⊢ (((𝜑 ∧ 𝑥 ∈ ℂ) ∧ ∀𝑦 ∈ ℝ⁺ ∃𝑧 ∈ ℝ⁺ ∀𝑤 ∈ 𝐴 ((𝑤 ≠ 𝐵 ∧ (abs‘(𝑤 − 𝐵)) < 𝑧) → (abs‘((𝐹‘𝑤) − 𝑥)) < 𝑦)) → ¬ (abs‘(𝑅 − 𝐿)) < (abs‘(𝑅 − 𝐿)))
364	361, 363	pm2.65da 828	. . . . 5 ⊢ ((𝜑 ∧ 𝑥 ∈ ℂ) → ¬ ∀𝑦 ∈ ℝ⁺ ∃𝑧 ∈ ℝ⁺ ∀𝑤 ∈ 𝐴 ((𝑤 ≠ 𝐵 ∧ (abs‘(𝑤 − 𝐵)) < 𝑧) → (abs‘((𝐹‘𝑤) − 𝑥)) < 𝑦))
365	364	ex 417	. . . 4 ⊢ (𝜑 → (𝑥 ∈ ℂ → ¬ ∀𝑦 ∈ ℝ⁺ ∃𝑧 ∈ ℝ⁺ ∀𝑤 ∈ 𝐴 ((𝑤 ≠ 𝐵 ∧ (abs‘(𝑤 − 𝐵)) < 𝑧) → (abs‘((𝐹‘𝑤) − 𝑥)) < 𝑦)))
366		imnan 404	. . . 4 ⊢ ((𝑥 ∈ ℂ → ¬ ∀𝑦 ∈ ℝ⁺ ∃𝑧 ∈ ℝ⁺ ∀𝑤 ∈ 𝐴 ((𝑤 ≠ 𝐵 ∧ (abs‘(𝑤 − 𝐵)) < 𝑧) → (abs‘((𝐹‘𝑤) − 𝑥)) < 𝑦)) ↔ ¬ (𝑥 ∈ ℂ ∧ ∀𝑦 ∈ ℝ⁺ ∃𝑧 ∈ ℝ⁺ ∀𝑤 ∈ 𝐴 ((𝑤 ≠ 𝐵 ∧ (abs‘(𝑤 − 𝐵)) < 𝑧) → (abs‘((𝐹‘𝑤) − 𝑥)) < 𝑦)))
367	365, 366	sylib 221	. . 3 ⊢ (𝜑 → ¬ (𝑥 ∈ ℂ ∧ ∀𝑦 ∈ ℝ⁺ ∃𝑧 ∈ ℝ⁺ ∀𝑤 ∈ 𝐴 ((𝑤 ≠ 𝐵 ∧ (abs‘(𝑤 − 𝐵)) < 𝑧) → (abs‘((𝐹‘𝑤) − 𝑥)) < 𝑦)))
368		limclner.a	. . . . 5 ⊢ (𝜑 → 𝐴 ⊆ ℝ)
369	368, 73	sstrd 3949	. . . 4 ⊢ (𝜑 → 𝐴 ⊆ ℂ)
370	36, 369, 56	ellimc3 25999	. . 3 ⊢ (𝜑 → (𝑥 ∈ (𝐹 lim_ℂ 𝐵) ↔ (𝑥 ∈ ℂ ∧ ∀𝑦 ∈ ℝ⁺ ∃𝑧 ∈ ℝ⁺ ∀𝑤 ∈ 𝐴 ((𝑤 ≠ 𝐵 ∧ (abs‘(𝑤 − 𝐵)) < 𝑧) → (abs‘((𝐹‘𝑤) − 𝑥)) < 𝑦))))
371	367, 370	mtbird 328	. 2 ⊢ (𝜑 → ¬ 𝑥 ∈ (𝐹 lim_ℂ 𝐵))
372	371	eq0rdv 4364	1 ⊢ (𝜑 → (𝐹 lim_ℂ 𝐵) = ∅)

Colors of variables: wff setvar class

Syntax hints: ¬ wn 3 → wi 4 ∧ wa 400 ∧ w3a 1101 = wceq 1563 ∈ wcel 2145 ≠ wne 2960 ∀wral 3079 ∃wrex 3089 ∖ cdif 3904 ∩ cin 3906 ⊆ wss 3907 ∅c0 4288 ifcif 4483 {csn 4585 ∪ cuni 4868 class class class wbr 5105 ran crn 5653 ↾ cres 5654 ⟶wf 6521 ‘cfv 6525 (class class class)co 7400 ℂcc 11086 ℝcr 11087 0cc0 11088 + caddc 11091 · cmul 11093 +∞cpnf 11228 -∞cmnf 11229 < clt 11231 ≤ cle 11232 − cmin 11429 / cdiv 11859 4c4 12288 ℝ⁺crp 13007 (,)cioo 13363 abscabs 15275 ↾_t crest 17463 TopOpenctopn 17464 topGenctg 17480 ℂ_fldccnfld 21482 Topctop 23011 limPtclp 23252 lim_ℂ climc 25982

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1818 ax-4 1832 ax-5 1933 ax-6 1990 ax-7 2031 ax-8 2147 ax-9 2155 ax-10 2178 ax-11 2194 ax-12 2215 ax-ext 2737 ax-rep 5232 ax-sep 5251 ax-nul 5261 ax-pow 5327 ax-pr 5395 ax-un 7722 ax-cnex 11144 ax-resscn 11145 ax-1cn 11146 ax-icn 11147 ax-addcl 11148 ax-addrcl 11149 ax-mulcl 11150 ax-mulrcl 11151 ax-mulcom 11152 ax-addass 11153 ax-mulass 11154 ax-distr 11155 ax-i2m1 11156 ax-1ne0 11157 ax-1rid 11158 ax-rnegex 11159 ax-rrecex 11160 ax-cnre 11161 ax-pre-lttri 11162 ax-pre-lttrn 11163 ax-pre-ltadd 11164 ax-pre-mulgt0 11165 ax-pre-sup 11166

This theorem depends on definitions: df-bi 210 df-an 401 df-or 861 df-3or 1102 df-3an 1103 df-tru 1566 df-fal 1576 df-ex 1803 df-nf 1807 df-sb 2094 df-mo 2569 df-eu 2599 df-clab 2744 df-cleq 2757 df-clel 2840 df-nfc 2914 df-ne 2961 df-nel 3065 df-ral 3080 df-rex 3090 df-rmo 3370 df-reu 3371 df-rab 3418 df-v 3459 df-sbc 3748 df-csb 3856 df-dif 3910 df-un 3912 df-in 3914 df-ss 3924 df-pss 3927 df-nul 4289 df-if 4484 df-pw 4560 df-sn 4586 df-pr 4588 df-tp 4590 df-op 4592 df-uni 4869 df-int 4909 df-iun 4954 df-iin 4955 df-br 5106 df-opab 5168 df-mpt 5187 df-tr 5213 df-id 5547 df-eprel 5552 df-po 5560 df-so 5561 df-fr 5605 df-we 5607 df-xp 5658 df-rel 5659 df-cnv 5660 df-co 5661 df-dm 5662 df-rn 5663 df-res 5664 df-ima 5665 df-pred 6292 df-ord 6353 df-on 6354 df-lim 6355 df-suc 6356 df-iota 6481 df-fun 6527 df-fn 6528 df-f 6529 df-f1 6530 df-fo 6531 df-f1o 6532 df-fv 6533 df-riota 7357 df-ov 7403 df-oprab 7404 df-mpo 7405 df-om 7851 df-1st 7974 df-2nd 7975 df-frecs 8266 df-wrecs 8297 df-recs 8346 df-rdg 8385 df-1o 8441 df-er 8682 df-map 8814 df-pm 8815 df-en 8932 df-dom 8933 df-sdom 8934 df-fin 8935 df-fi 9359 df-sup 9390 df-inf 9391 df-pnf 11233 df-mnf 11234 df-xr 11235 df-ltxr 11236 df-le 11237 df-sub 11431 df-neg 11432 df-div 11860 df-nn 12225 df-2 12294 df-3 12295 df-4 12296 df-5 12297 df-6 12298 df-7 12299 df-8 12300 df-9 12301 df-n0 12496 df-z 12583 df-dec 12703 df-uz 12854 df-q 12964 df-rp 13008 df-xneg 13128 df-xadd 13129 df-xmul 13130 df-ioo 13367 df-fz 13527 df-seq 14029 df-exp 14089 df-cj 15140 df-re 15141 df-im 15142 df-sqrt 15276 df-abs 15277 df-struct 17197 df-slot 17232 df-ndx 17244 df-base 17260 df-plusg 17313 df-mulr 17314 df-starv 17315 df-tset 17319 df-ple 17320 df-ds 17322 df-unif 17323 df-rest 17465 df-topn 17466 df-topgen 17486 df-psmet 21474 df-xmet 21475 df-met 21476 df-bl 21477 df-mopn 21478 df-cnfld 21483 df-top 23012 df-topon 23029 df-topsp 23051 df-bases 23064 df-cld 23137 df-ntr 23138 df-cls 23139 df-nei 23216 df-lp 23254 df-cnp 23346 df-xms 24438 df-ms 24439 df-limc 25986

This theorem is referenced by: limclr 46227 jumpncnp 46470

W3C validator