Theorem limclner 45606

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 25924	. . . . . . . . . . . . 13 ⊢ ((𝐹 ↾ (𝐵(,)+∞)) limℂ 𝐵) ⊆ ℂ
2		limclner.r	. . . . . . . . . . . . 13 ⊢ (𝜑 → 𝑅 ∈ ((𝐹 ↾ (𝐵(,)+∞)) limℂ 𝐵))
3	1, 2	sselid 3992	. . . . . . . . . . . 12 ⊢ (𝜑 → 𝑅 ∈ ℂ)
4	3	ad2antrr 726	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑥 ∈ ℂ) ∧ ∀𝑦 ∈ ℝ+ ∃𝑧 ∈ ℝ+ ∀𝑤 ∈ 𝐴 ((𝑤 ≠ 𝐵 ∧ (abs‘(𝑤 − 𝐵)) < 𝑧) → (abs‘((𝐹‘𝑤) − 𝑥)) < 𝑦)) → 𝑅 ∈ ℂ)
5		limccl 25924	. . . . . . . . . . . . 13 ⊢ ((𝐹 ↾ (-∞(,)𝐵)) limℂ 𝐵) ⊆ ℂ
6		limclner.l	. . . . . . . . . . . . 13 ⊢ (𝜑 → 𝐿 ∈ ((𝐹 ↾ (-∞(,)𝐵)) limℂ 𝐵))
7	5, 6	sselid 3992	. . . . . . . . . . . 12 ⊢ (𝜑 → 𝐿 ∈ ℂ)
8	7	ad2antrr 726	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑥 ∈ ℂ) ∧ ∀𝑦 ∈ ℝ+ ∃𝑧 ∈ ℝ+ ∀𝑤 ∈ 𝐴 ((𝑤 ≠ 𝐵 ∧ (abs‘(𝑤 − 𝐵)) < 𝑧) → (abs‘((𝐹‘𝑤) − 𝑥)) < 𝑦)) → 𝐿 ∈ ℂ)
9	4, 8	subcld 11617	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑥 ∈ ℂ) ∧ ∀𝑦 ∈ ℝ+ ∃𝑧 ∈ ℝ+ ∀𝑤 ∈ 𝐴 ((𝑤 ≠ 𝐵 ∧ (abs‘(𝑤 − 𝐵)) < 𝑧) → (abs‘((𝐹‘𝑤) − 𝑥)) < 𝑦)) → (𝑅 − 𝐿) ∈ ℂ)
10		limclner.lner	. . . . . . . . . . . . 13 ⊢ (𝜑 → 𝐿 ≠ 𝑅)
11	10	necomd 2993	. . . . . . . . . . . 12 ⊢ (𝜑 → 𝑅 ≠ 𝐿)
12	11	ad2antrr 726	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑥 ∈ ℂ) ∧ ∀𝑦 ∈ ℝ+ ∃𝑧 ∈ ℝ+ ∀𝑤 ∈ 𝐴 ((𝑤 ≠ 𝐵 ∧ (abs‘(𝑤 − 𝐵)) < 𝑧) → (abs‘((𝐹‘𝑤) − 𝑥)) < 𝑦)) → 𝑅 ≠ 𝐿)
13	4, 8, 12	subne0d 11626	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑥 ∈ ℂ) ∧ ∀𝑦 ∈ ℝ+ ∃𝑧 ∈ ℝ+ ∀𝑤 ∈ 𝐴 ((𝑤 ≠ 𝐵 ∧ (abs‘(𝑤 − 𝐵)) < 𝑧) → (abs‘((𝐹‘𝑤) − 𝑥)) < 𝑦)) → (𝑅 − 𝐿) ≠ 0)
14	9, 13	absrpcld 15483	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑥 ∈ ℂ) ∧ ∀𝑦 ∈ ℝ+ ∃𝑧 ∈ ℝ+ ∀𝑤 ∈ 𝐴 ((𝑤 ≠ 𝐵 ∧ (abs‘(𝑤 − 𝐵)) < 𝑧) → (abs‘((𝐹‘𝑤) − 𝑥)) < 𝑦)) → (abs‘(𝑅 − 𝐿)) ∈ ℝ+)
15		4re 12347	. . . . . . . . . . 11 ⊢ 4 ∈ ℝ
16		4pos 12370	. . . . . . . . . . 11 ⊢ 0 < 4
17	15, 16	elrpii 13034	. . . . . . . . . 10 ⊢ 4 ∈ ℝ+
18	17	a1i 11	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑥 ∈ ℂ) ∧ ∀𝑦 ∈ ℝ+ ∃𝑧 ∈ ℝ+ ∀𝑤 ∈ 𝐴 ((𝑤 ≠ 𝐵 ∧ (abs‘(𝑤 − 𝐵)) < 𝑧) → (abs‘((𝐹‘𝑤) − 𝑥)) < 𝑦)) → 4 ∈ ℝ+)
19	14, 18	rpdivcld 13091	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑥 ∈ ℂ) ∧ ∀𝑦 ∈ ℝ+ ∃𝑧 ∈ ℝ+ ∀𝑤 ∈ 𝐴 ((𝑤 ≠ 𝐵 ∧ (abs‘(𝑤 − 𝐵)) < 𝑧) → (abs‘((𝐹‘𝑤) − 𝑥)) < 𝑦)) → ((abs‘(𝑅 − 𝐿)) / 4) ∈ ℝ+)
20		nfv 1911	. . . . . . . . . . 11 ⊢ Ⅎ𝑦(𝜑 ∧ 𝑥 ∈ ℂ)
21		nfra1 3281	. . . . . . . . . . 11 ⊢ Ⅎ𝑦∀𝑦 ∈ ℝ+ ∃𝑧 ∈ ℝ+ ∀𝑤 ∈ 𝐴 ((𝑤 ≠ 𝐵 ∧ (abs‘(𝑤 − 𝐵)) < 𝑧) → (abs‘((𝐹‘𝑤) − 𝑥)) < 𝑦)
22	20, 21	nfan 1896	. . . . . . . . . 10 ⊢ Ⅎ𝑦((𝜑 ∧ 𝑥 ∈ ℂ) ∧ ∀𝑦 ∈ ℝ+ ∃𝑧 ∈ ℝ+ ∀𝑤 ∈ 𝐴 ((𝑤 ≠ 𝐵 ∧ (abs‘(𝑤 − 𝐵)) < 𝑧) → (abs‘((𝐹‘𝑤) − 𝑥)) < 𝑦))
23		nfv 1911	. . . . . . . . . 10 ⊢ Ⅎ𝑦(((abs‘(𝑅 − 𝐿)) / 4) ∈ ℝ+ → ∃𝑎 ∈ 𝐴 ∃𝑏 ∈ 𝐴 (abs‘(𝑅 − 𝐿)) < (4 · ((abs‘(𝑅 − 𝐿)) / 4)))
24	22, 23	nfim 1893	. . . . . . . . 9 ⊢ Ⅎ𝑦(((𝜑 ∧ 𝑥 ∈ ℂ) ∧ ∀𝑦 ∈ ℝ+ ∃𝑧 ∈ ℝ+ ∀𝑤 ∈ 𝐴 ((𝑤 ≠ 𝐵 ∧ (abs‘(𝑤 − 𝐵)) < 𝑧) → (abs‘((𝐹‘𝑤) − 𝑥)) < 𝑦)) → (((abs‘(𝑅 − 𝐿)) / 4) ∈ ℝ+ → ∃𝑎 ∈ 𝐴 ∃𝑏 ∈ 𝐴 (abs‘(𝑅 − 𝐿)) < (4 · ((abs‘(𝑅 − 𝐿)) / 4))))
25		ovex 7463	. . . . . . . . 9 ⊢ ((abs‘(𝑅 − 𝐿)) / 4) ∈ V
26		eleq1 2826	. . . . . . . . . . 11 ⊢ (𝑦 = ((abs‘(𝑅 − 𝐿)) / 4) → (𝑦 ∈ ℝ+ ↔ ((abs‘(𝑅 − 𝐿)) / 4) ∈ ℝ+))
27		oveq2 7438	. . . . . . . . . . . . 13 ⊢ (𝑦 = ((abs‘(𝑅 − 𝐿)) / 4) → (4 · 𝑦) = (4 · ((abs‘(𝑅 − 𝐿)) / 4)))
28	27	breq2d 5159	. . . . . . . . . . . 12 ⊢ (𝑦 = ((abs‘(𝑅 − 𝐿)) / 4) → ((abs‘(𝑅 − 𝐿)) < (4 · 𝑦) ↔ (abs‘(𝑅 − 𝐿)) < (4 · ((abs‘(𝑅 − 𝐿)) / 4))))
29	28	2rexbidv 3219	. . . . . . . . . . 11 ⊢ (𝑦 = ((abs‘(𝑅 − 𝐿)) / 4) → (∃𝑎 ∈ 𝐴 ∃𝑏 ∈ 𝐴 (abs‘(𝑅 − 𝐿)) < (4 · 𝑦) ↔ ∃𝑎 ∈ 𝐴 ∃𝑏 ∈ 𝐴 (abs‘(𝑅 − 𝐿)) < (4 · ((abs‘(𝑅 − 𝐿)) / 4))))
30	26, 29	imbi12d 344	. . . . . . . . . 10 ⊢ (𝑦 = ((abs‘(𝑅 − 𝐿)) / 4) → ((𝑦 ∈ ℝ+ → ∃𝑎 ∈ 𝐴 ∃𝑏 ∈ 𝐴 (abs‘(𝑅 − 𝐿)) < (4 · 𝑦)) ↔ (((abs‘(𝑅 − 𝐿)) / 4) ∈ ℝ+ → ∃𝑎 ∈ 𝐴 ∃𝑏 ∈ 𝐴 (abs‘(𝑅 − 𝐿)) < (4 · ((abs‘(𝑅 − 𝐿)) / 4)))))
31	30	imbi2d 340	. . . . . . . . 9 ⊢ (𝑦 = ((abs‘(𝑅 − 𝐿)) / 4) → ((((𝜑 ∧ 𝑥 ∈ ℂ) ∧ ∀𝑦 ∈ ℝ+ ∃𝑧 ∈ ℝ+ ∀𝑤 ∈ 𝐴 ((𝑤 ≠ 𝐵 ∧ (abs‘(𝑤 − 𝐵)) < 𝑧) → (abs‘((𝐹‘𝑤) − 𝑥)) < 𝑦)) → (𝑦 ∈ ℝ+ → ∃𝑎 ∈ 𝐴 ∃𝑏 ∈ 𝐴 (abs‘(𝑅 − 𝐿)) < (4 · 𝑦))) ↔ (((𝜑 ∧ 𝑥 ∈ ℂ) ∧ ∀𝑦 ∈ ℝ+ ∃𝑧 ∈ ℝ+ ∀𝑤 ∈ 𝐴 ((𝑤 ≠ 𝐵 ∧ (abs‘(𝑤 − 𝐵)) < 𝑧) → (abs‘((𝐹‘𝑤) − 𝑥)) < 𝑦)) → (((abs‘(𝑅 − 𝐿)) / 4) ∈ ℝ+ → ∃𝑎 ∈ 𝐴 ∃𝑏 ∈ 𝐴 (abs‘(𝑅 − 𝐿)) < (4 · ((abs‘(𝑅 − 𝐿)) / 4))))))
32		simpll 767	. . . . . . . . . . 11 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℂ) ∧ ∀𝑦 ∈ ℝ+ ∃𝑧 ∈ ℝ+ ∀𝑤 ∈ 𝐴 ((𝑤 ≠ 𝐵 ∧ (abs‘(𝑤 − 𝐵)) < 𝑧) → (abs‘((𝐹‘𝑤) − 𝑥)) < 𝑦)) ∧ 𝑦 ∈ ℝ+) → (𝜑 ∧ 𝑥 ∈ ℂ))
33		simpr 484	. . . . . . . . . . 11 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℂ) ∧ ∀𝑦 ∈ ℝ+ ∃𝑧 ∈ ℝ+ ∀𝑤 ∈ 𝐴 ((𝑤 ≠ 𝐵 ∧ (abs‘(𝑤 − 𝐵)) < 𝑧) → (abs‘((𝐹‘𝑤) − 𝑥)) < 𝑦)) ∧ 𝑦 ∈ ℝ+) → 𝑦 ∈ ℝ+)
34		rspa 3245	. . . . . . . . . . . 12 ⊢ ((∀𝑦 ∈ ℝ+ ∃𝑧 ∈ ℝ+ ∀𝑤 ∈ 𝐴 ((𝑤 ≠ 𝐵 ∧ (abs‘(𝑤 − 𝐵)) < 𝑧) → (abs‘((𝐹‘𝑤) − 𝑥)) < 𝑦) ∧ 𝑦 ∈ ℝ+) → ∃𝑧 ∈ ℝ+ ∀𝑤 ∈ 𝐴 ((𝑤 ≠ 𝐵 ∧ (abs‘(𝑤 − 𝐵)) < 𝑧) → (abs‘((𝐹‘𝑤) − 𝑥)) < 𝑦))
35	34	adantll 714	. . . . . . . . . . 11 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℂ) ∧ ∀𝑦 ∈ ℝ+ ∃𝑧 ∈ ℝ+ ∀𝑤 ∈ 𝐴 ((𝑤 ≠ 𝐵 ∧ (abs‘(𝑤 − 𝐵)) < 𝑧) → (abs‘((𝐹‘𝑤) − 𝑥)) < 𝑦)) ∧ 𝑦 ∈ ℝ+) → ∃𝑧 ∈ ℝ+ ∀𝑤 ∈ 𝐴 ((𝑤 ≠ 𝐵 ∧ (abs‘(𝑤 − 𝐵)) < 𝑧) → (abs‘((𝐹‘𝑤) − 𝑥)) < 𝑦))
36		limclner.f	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝜑 → 𝐹:𝐴⟶ℂ)
37		fresin 6777	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝐹:𝐴⟶ℂ → (𝐹 ↾ (𝐵(,)+∞)):(𝐴 ∩ (𝐵(,)+∞))⟶ℂ)
38	36, 37	syl 17	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝜑 → (𝐹 ↾ (𝐵(,)+∞)):(𝐴 ∩ (𝐵(,)+∞))⟶ℂ)
39		inss2 4245	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝐴 ∩ (𝐵(,)+∞)) ⊆ (𝐵(,)+∞)
40		ioosscn 13445	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝐵(,)+∞) ⊆ ℂ
41	39, 40	sstri 4004	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝐴 ∩ (𝐵(,)+∞)) ⊆ ℂ
42	41	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝜑 → (𝐴 ∩ (𝐵(,)+∞)) ⊆ ℂ)
43		limclner.j	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ 𝐽 = (topGen‘ran (,))
44		retop 24797	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (topGen‘ran (,)) ∈ Top
45	43, 44	eqeltri 2834	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ 𝐽 ∈ Top
46		inss2 4245	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (𝐴 ∩ (-∞(,)𝐵)) ⊆ (-∞(,)𝐵)
47		ioossre 13444	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (-∞(,)𝐵) ⊆ ℝ
48	46, 47	sstri 4004	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝐴 ∩ (-∞(,)𝐵)) ⊆ ℝ
49		uniretop 24798	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ ℝ = ∪ (topGen‘ran (,))
50	43	unieqi 4923	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ ∪ 𝐽 = ∪ (topGen‘ran (,))
51	49, 50	eqtr4i 2765	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ℝ = ∪ 𝐽
52	51	lpss 23165	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((𝐽 ∈ Top ∧ (𝐴 ∩ (-∞(,)𝐵)) ⊆ ℝ) → ((limPt‘𝐽)‘(𝐴 ∩ (-∞(,)𝐵))) ⊆ ℝ)
53	45, 48, 52	mp2an 692	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((limPt‘𝐽)‘(𝐴 ∩ (-∞(,)𝐵))) ⊆ ℝ
54		limclner.blp1	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝜑 → 𝐵 ∈ ((limPt‘𝐽)‘(𝐴 ∩ (-∞(,)𝐵))))
55	53, 54	sselid 3992	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝜑 → 𝐵 ∈ ℝ)
56	55	recnd 11286	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝜑 → 𝐵 ∈ ℂ)
57	38, 42, 56	ellimc3 25928	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝜑 → (𝑅 ∈ ((𝐹 ↾ (𝐵(,)+∞)) limℂ 𝐵) ↔ (𝑅 ∈ ℂ ∧ ∀𝑦 ∈ ℝ+ ∃𝑣 ∈ ℝ+ ∀𝑤 ∈ (𝐴 ∩ (𝐵(,)+∞))((𝑤 ≠ 𝐵 ∧ (abs‘(𝑤 − 𝐵)) < 𝑣) → (abs‘(((𝐹 ↾ (𝐵(,)+∞))‘𝑤) − 𝑅)) < 𝑦))))
58	2, 57	mpbid 232	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝜑 → (𝑅 ∈ ℂ ∧ ∀𝑦 ∈ ℝ+ ∃𝑣 ∈ ℝ+ ∀𝑤 ∈ (𝐴 ∩ (𝐵(,)+∞))((𝑤 ≠ 𝐵 ∧ (abs‘(𝑤 − 𝐵)) < 𝑣) → (abs‘(((𝐹 ↾ (𝐵(,)+∞))‘𝑤) − 𝑅)) < 𝑦)))
59	58	simprd 495	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝜑 → ∀𝑦 ∈ ℝ+ ∃𝑣 ∈ ℝ+ ∀𝑤 ∈ (𝐴 ∩ (𝐵(,)+∞))((𝑤 ≠ 𝐵 ∧ (abs‘(𝑤 − 𝐵)) < 𝑣) → (abs‘(((𝐹 ↾ (𝐵(,)+∞))‘𝑤) − 𝑅)) < 𝑦))
60	59	r19.21bi 3248	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ 𝑦 ∈ ℝ+) → ∃𝑣 ∈ ℝ+ ∀𝑤 ∈ (𝐴 ∩ (𝐵(,)+∞))((𝑤 ≠ 𝐵 ∧ (abs‘(𝑤 − 𝐵)) < 𝑣) → (abs‘(((𝐹 ↾ (𝐵(,)+∞))‘𝑤) − 𝑅)) < 𝑦))
61	60	3ad2ant1 1132	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ 𝑦 ∈ ℝ+) ∧ 𝑧 ∈ ℝ+ ∧ ∀𝑤 ∈ 𝐴 ((𝑤 ≠ 𝐵 ∧ (abs‘(𝑤 − 𝐵)) < 𝑧) → (abs‘((𝐹‘𝑤) − 𝑥)) < 𝑦)) → ∃𝑣 ∈ ℝ+ ∀𝑤 ∈ (𝐴 ∩ (𝐵(,)+∞))((𝑤 ≠ 𝐵 ∧ (abs‘(𝑤 − 𝐵)) < 𝑣) → (abs‘(((𝐹 ↾ (𝐵(,)+∞))‘𝑤) − 𝑅)) < 𝑦))
62		simp11l 1283	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((((𝜑 ∧ 𝑦 ∈ ℝ+) ∧ 𝑧 ∈ ℝ+ ∧ ∀𝑤 ∈ 𝐴 ((𝑤 ≠ 𝐵 ∧ (abs‘(𝑤 − 𝐵)) < 𝑧) → (abs‘((𝐹‘𝑤) − 𝑥)) < 𝑦)) ∧ 𝑣 ∈ ℝ+ ∧ ∀𝑤 ∈ (𝐴 ∩ (𝐵(,)+∞))((𝑤 ≠ 𝐵 ∧ (abs‘(𝑤 − 𝐵)) < 𝑣) → (abs‘(((𝐹 ↾ (𝐵(,)+∞))‘𝑤) − 𝑅)) < 𝑦)) → 𝜑)
63		simp12 1203	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((((𝜑 ∧ 𝑦 ∈ ℝ+) ∧ 𝑧 ∈ ℝ+ ∧ ∀𝑤 ∈ 𝐴 ((𝑤 ≠ 𝐵 ∧ (abs‘(𝑤 − 𝐵)) < 𝑧) → (abs‘((𝐹‘𝑤) − 𝑥)) < 𝑦)) ∧ 𝑣 ∈ ℝ+ ∧ ∀𝑤 ∈ (𝐴 ∩ (𝐵(,)+∞))((𝑤 ≠ 𝐵 ∧ (abs‘(𝑤 − 𝐵)) < 𝑣) → (abs‘(((𝐹 ↾ (𝐵(,)+∞))‘𝑤) − 𝑅)) < 𝑦)) → 𝑧 ∈ ℝ+)
64		simp2 1136	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((((𝜑 ∧ 𝑦 ∈ ℝ+) ∧ 𝑧 ∈ ℝ+ ∧ ∀𝑤 ∈ 𝐴 ((𝑤 ≠ 𝐵 ∧ (abs‘(𝑤 − 𝐵)) < 𝑧) → (abs‘((𝐹‘𝑤) − 𝑥)) < 𝑦)) ∧ 𝑣 ∈ ℝ+ ∧ ∀𝑤 ∈ (𝐴 ∩ (𝐵(,)+∞))((𝑤 ≠ 𝐵 ∧ (abs‘(𝑤 − 𝐵)) < 𝑣) → (abs‘(((𝐹 ↾ (𝐵(,)+∞))‘𝑤) − 𝑅)) < 𝑦)) → 𝑣 ∈ ℝ+)
65		breq2 5151	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝑢 = if(𝑧 ≤ 𝑣, 𝑧, 𝑣) → ((abs‘(𝑏 − 𝐵)) < 𝑢 ↔ (abs‘(𝑏 − 𝐵)) < if(𝑧 ≤ 𝑣, 𝑧, 𝑣)))
66	65	rexbidv 3176	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑢 = if(𝑧 ≤ 𝑣, 𝑧, 𝑣) → (∃𝑏 ∈ ((𝐴 ∩ (𝐵(,)+∞)) ∖ {𝐵})(abs‘(𝑏 − 𝐵)) < 𝑢 ↔ ∃𝑏 ∈ ((𝐴 ∩ (𝐵(,)+∞)) ∖ {𝐵})(abs‘(𝑏 − 𝐵)) < if(𝑧 ≤ 𝑣, 𝑧, 𝑣)))
67		inss1 4244	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ (((limPt‘𝐾)‘(𝐴 ∩ (𝐵(,)+∞))) ∩ ℝ) ⊆ ((limPt‘𝐾)‘(𝐴 ∩ (𝐵(,)+∞)))
68	67	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (𝜑 → (((limPt‘𝐾)‘(𝐴 ∩ (𝐵(,)+∞))) ∩ ℝ) ⊆ ((limPt‘𝐾)‘(𝐴 ∩ (𝐵(,)+∞))))
69		limclner.k	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ 𝐾 = (TopOpen‘ℂfld)
70	69	cnfldtop 24819	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ 𝐾 ∈ Top
71	70	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ (𝜑 → 𝐾 ∈ Top)
72		ax-resscn 11209	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ ℝ ⊆ ℂ
73	72	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ (𝜑 → ℝ ⊆ ℂ)
74		ioossre 13444	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ (𝐵(,)+∞) ⊆ ℝ
75	39, 74	sstri 4004	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ (𝐴 ∩ (𝐵(,)+∞)) ⊆ ℝ
76	75	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ (𝜑 → (𝐴 ∩ (𝐵(,)+∞)) ⊆ ℝ)
77		unicntop 24821	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ ℂ = ∪ (TopOpen‘ℂfld)
78	69	unieqi 4923	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ ∪ 𝐾 = ∪ (TopOpen‘ℂfld)
79	77, 78	eqtr4i 2765	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ ℂ = ∪ 𝐾
80	69	tgioo2 24838	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ (topGen‘ran (,)) = (𝐾 ↾t ℝ)
81	43, 80	eqtri 2762	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ 𝐽 = (𝐾 ↾t ℝ)
82	79, 81	restlp 23206	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ ((𝐾 ∈ Top ∧ ℝ ⊆ ℂ ∧ (𝐴 ∩ (𝐵(,)+∞)) ⊆ ℝ) → ((limPt‘𝐽)‘(𝐴 ∩ (𝐵(,)+∞))) = (((limPt‘𝐾)‘(𝐴 ∩ (𝐵(,)+∞))) ∩ ℝ))
83	71, 73, 76, 82	syl3anc 1370	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (𝜑 → ((limPt‘𝐽)‘(𝐴 ∩ (𝐵(,)+∞))) = (((limPt‘𝐾)‘(𝐴 ∩ (𝐵(,)+∞))) ∩ ℝ))
84	69	eqcomi 2743	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ (TopOpen‘ℂfld) = 𝐾
85	84	fveq2i 6909	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ (limPt‘(TopOpen‘ℂfld)) = (limPt‘𝐾)
86	85	fveq1i 6907	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ ((limPt‘(TopOpen‘ℂfld))‘(𝐴 ∩ (𝐵(,)+∞))) = ((limPt‘𝐾)‘(𝐴 ∩ (𝐵(,)+∞)))
87	86	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (𝜑 → ((limPt‘(TopOpen‘ℂfld))‘(𝐴 ∩ (𝐵(,)+∞))) = ((limPt‘𝐾)‘(𝐴 ∩ (𝐵(,)+∞))))
88	68, 83, 87	3sstr4d 4042	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (𝜑 → ((limPt‘𝐽)‘(𝐴 ∩ (𝐵(,)+∞))) ⊆ ((limPt‘(TopOpen‘ℂfld))‘(𝐴 ∩ (𝐵(,)+∞))))
89		limclner.blp2	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (𝜑 → 𝐵 ∈ ((limPt‘𝐽)‘(𝐴 ∩ (𝐵(,)+∞))))
90	88, 89	sseldd 3995	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝜑 → 𝐵 ∈ ((limPt‘(TopOpen‘ℂfld))‘(𝐴 ∩ (𝐵(,)+∞))))
91	42, 56	islpcn 45594	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝜑 → (𝐵 ∈ ((limPt‘(TopOpen‘ℂfld))‘(𝐴 ∩ (𝐵(,)+∞))) ↔ ∀𝑢 ∈ ℝ+ ∃𝑏 ∈ ((𝐴 ∩ (𝐵(,)+∞)) ∖ {𝐵})(abs‘(𝑏 − 𝐵)) < 𝑢))
92	90, 91	mpbid 232	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝜑 → ∀𝑢 ∈ ℝ+ ∃𝑏 ∈ ((𝐴 ∩ (𝐵(,)+∞)) ∖ {𝐵})(abs‘(𝑏 − 𝐵)) < 𝑢)
93	92	3ad2ant1 1132	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((𝜑 ∧ 𝑧 ∈ ℝ+ ∧ 𝑣 ∈ ℝ+) → ∀𝑢 ∈ ℝ+ ∃𝑏 ∈ ((𝐴 ∩ (𝐵(,)+∞)) ∖ {𝐵})(abs‘(𝑏 − 𝐵)) < 𝑢)
94		ifcl 4575	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((𝑧 ∈ ℝ+ ∧ 𝑣 ∈ ℝ+) → if(𝑧 ≤ 𝑣, 𝑧, 𝑣) ∈ ℝ+)
95	94	3adant1 1129	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((𝜑 ∧ 𝑧 ∈ ℝ+ ∧ 𝑣 ∈ ℝ+) → if(𝑧 ≤ 𝑣, 𝑧, 𝑣) ∈ ℝ+)
96	66, 93, 95	rspcdva 3622	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝜑 ∧ 𝑧 ∈ ℝ+ ∧ 𝑣 ∈ ℝ+) → ∃𝑏 ∈ ((𝐴 ∩ (𝐵(,)+∞)) ∖ {𝐵})(abs‘(𝑏 − 𝐵)) < if(𝑧 ≤ 𝑣, 𝑧, 𝑣))
97		eldifi 4140	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝑏 ∈ ((𝐴 ∩ (𝐵(,)+∞)) ∖ {𝐵}) → 𝑏 ∈ (𝐴 ∩ (𝐵(,)+∞)))
98	75, 97	sselid 3992	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝑏 ∈ ((𝐴 ∩ (𝐵(,)+∞)) ∖ {𝐵}) → 𝑏 ∈ ℝ)
99	73	sselda 3994	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ ((𝜑 ∧ 𝑏 ∈ ℝ) → 𝑏 ∈ ℂ)
100	56	adantr 480	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ ((𝜑 ∧ 𝑏 ∈ ℝ) → 𝐵 ∈ ℂ)
101	99, 100	subcld 11617	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ ((𝜑 ∧ 𝑏 ∈ ℝ) → (𝑏 − 𝐵) ∈ ℂ)
102	101	abscld 15471	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ ((𝜑 ∧ 𝑏 ∈ ℝ) → (abs‘(𝑏 − 𝐵)) ∈ ℝ)
103	102	3ad2antl1 1184	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ (((𝜑 ∧ 𝑧 ∈ ℝ+ ∧ 𝑣 ∈ ℝ+) ∧ 𝑏 ∈ ℝ) → (abs‘(𝑏 − 𝐵)) ∈ ℝ)
104	103	adantr 480	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ ((((𝜑 ∧ 𝑧 ∈ ℝ+ ∧ 𝑣 ∈ ℝ+) ∧ 𝑏 ∈ ℝ) ∧ (abs‘(𝑏 − 𝐵)) < if(𝑧 ≤ 𝑣, 𝑧, 𝑣)) → (abs‘(𝑏 − 𝐵)) ∈ ℝ)
105	95	rpred 13074	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ ((𝜑 ∧ 𝑧 ∈ ℝ+ ∧ 𝑣 ∈ ℝ+) → if(𝑧 ≤ 𝑣, 𝑧, 𝑣) ∈ ℝ)
106	105	ad2antrr 726	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ ((((𝜑 ∧ 𝑧 ∈ ℝ+ ∧ 𝑣 ∈ ℝ+) ∧ 𝑏 ∈ ℝ) ∧ (abs‘(𝑏 − 𝐵)) < if(𝑧 ≤ 𝑣, 𝑧, 𝑣)) → if(𝑧 ≤ 𝑣, 𝑧, 𝑣) ∈ ℝ)
107		rpre 13040	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ (𝑧 ∈ ℝ+ → 𝑧 ∈ ℝ)
108	107	3ad2ant2 1133	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ ((𝜑 ∧ 𝑧 ∈ ℝ+ ∧ 𝑣 ∈ ℝ+) → 𝑧 ∈ ℝ)
109	108	ad2antrr 726	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ ((((𝜑 ∧ 𝑧 ∈ ℝ+ ∧ 𝑣 ∈ ℝ+) ∧ 𝑏 ∈ ℝ) ∧ (abs‘(𝑏 − 𝐵)) < if(𝑧 ≤ 𝑣, 𝑧, 𝑣)) → 𝑧 ∈ ℝ)
110		simpr 484	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ ((((𝜑 ∧ 𝑧 ∈ ℝ+ ∧ 𝑣 ∈ ℝ+) ∧ 𝑏 ∈ ℝ) ∧ (abs‘(𝑏 − 𝐵)) < if(𝑧 ≤ 𝑣, 𝑧, 𝑣)) → (abs‘(𝑏 − 𝐵)) < if(𝑧 ≤ 𝑣, 𝑧, 𝑣))
111		rpre 13040	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ (𝑣 ∈ ℝ+ → 𝑣 ∈ ℝ)
112		min1 13227	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ ((𝑧 ∈ ℝ ∧ 𝑣 ∈ ℝ) → if(𝑧 ≤ 𝑣, 𝑧, 𝑣) ≤ 𝑧)
113	107, 111, 112	syl2an 596	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ ((𝑧 ∈ ℝ+ ∧ 𝑣 ∈ ℝ+) → if(𝑧 ≤ 𝑣, 𝑧, 𝑣) ≤ 𝑧)
114	113	3adant1 1129	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ ((𝜑 ∧ 𝑧 ∈ ℝ+ ∧ 𝑣 ∈ ℝ+) → if(𝑧 ≤ 𝑣, 𝑧, 𝑣) ≤ 𝑧)
115	114	ad2antrr 726	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ ((((𝜑 ∧ 𝑧 ∈ ℝ+ ∧ 𝑣 ∈ ℝ+) ∧ 𝑏 ∈ ℝ) ∧ (abs‘(𝑏 − 𝐵)) < if(𝑧 ≤ 𝑣, 𝑧, 𝑣)) → if(𝑧 ≤ 𝑣, 𝑧, 𝑣) ≤ 𝑧)
116	104, 106, 109, 110, 115	ltletrd 11418	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ((((𝜑 ∧ 𝑧 ∈ ℝ+ ∧ 𝑣 ∈ ℝ+) ∧ 𝑏 ∈ ℝ) ∧ (abs‘(𝑏 − 𝐵)) < if(𝑧 ≤ 𝑣, 𝑧, 𝑣)) → (abs‘(𝑏 − 𝐵)) < 𝑧)
117	111	3ad2ant3 1134	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ ((𝜑 ∧ 𝑧 ∈ ℝ+ ∧ 𝑣 ∈ ℝ+) → 𝑣 ∈ ℝ)
118	117	ad2antrr 726	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ ((((𝜑 ∧ 𝑧 ∈ ℝ+ ∧ 𝑣 ∈ ℝ+) ∧ 𝑏 ∈ ℝ) ∧ (abs‘(𝑏 − 𝐵)) < if(𝑧 ≤ 𝑣, 𝑧, 𝑣)) → 𝑣 ∈ ℝ)
119	109, 118	min2d 45422	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ ((((𝜑 ∧ 𝑧 ∈ ℝ+ ∧ 𝑣 ∈ ℝ+) ∧ 𝑏 ∈ ℝ) ∧ (abs‘(𝑏 − 𝐵)) < if(𝑧 ≤ 𝑣, 𝑧, 𝑣)) → if(𝑧 ≤ 𝑣, 𝑧, 𝑣) ≤ 𝑣)
120	104, 106, 118, 110, 119	ltletrd 11418	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ((((𝜑 ∧ 𝑧 ∈ ℝ+ ∧ 𝑣 ∈ ℝ+) ∧ 𝑏 ∈ ℝ) ∧ (abs‘(𝑏 − 𝐵)) < if(𝑧 ≤ 𝑣, 𝑧, 𝑣)) → (abs‘(𝑏 − 𝐵)) < 𝑣)
121	116, 120	jca 511	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((((𝜑 ∧ 𝑧 ∈ ℝ+ ∧ 𝑣 ∈ ℝ+) ∧ 𝑏 ∈ ℝ) ∧ (abs‘(𝑏 − 𝐵)) < if(𝑧 ≤ 𝑣, 𝑧, 𝑣)) → ((abs‘(𝑏 − 𝐵)) < 𝑧 ∧ (abs‘(𝑏 − 𝐵)) < 𝑣))
122	121	ex 412	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (((𝜑 ∧ 𝑧 ∈ ℝ+ ∧ 𝑣 ∈ ℝ+) ∧ 𝑏 ∈ ℝ) → ((abs‘(𝑏 − 𝐵)) < if(𝑧 ≤ 𝑣, 𝑧, 𝑣) → ((abs‘(𝑏 − 𝐵)) < 𝑧 ∧ (abs‘(𝑏 − 𝐵)) < 𝑣)))
123	98, 122	sylan2 593	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((𝜑 ∧ 𝑧 ∈ ℝ+ ∧ 𝑣 ∈ ℝ+) ∧ 𝑏 ∈ ((𝐴 ∩ (𝐵(,)+∞)) ∖ {𝐵})) → ((abs‘(𝑏 − 𝐵)) < if(𝑧 ≤ 𝑣, 𝑧, 𝑣) → ((abs‘(𝑏 − 𝐵)) < 𝑧 ∧ (abs‘(𝑏 − 𝐵)) < 𝑣)))
124	123	reximdva 3165	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝜑 ∧ 𝑧 ∈ ℝ+ ∧ 𝑣 ∈ ℝ+) → (∃𝑏 ∈ ((𝐴 ∩ (𝐵(,)+∞)) ∖ {𝐵})(abs‘(𝑏 − 𝐵)) < if(𝑧 ≤ 𝑣, 𝑧, 𝑣) → ∃𝑏 ∈ ((𝐴 ∩ (𝐵(,)+∞)) ∖ {𝐵})((abs‘(𝑏 − 𝐵)) < 𝑧 ∧ (abs‘(𝑏 − 𝐵)) < 𝑣)))
125	96, 124	mpd 15	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝜑 ∧ 𝑧 ∈ ℝ+ ∧ 𝑣 ∈ ℝ+) → ∃𝑏 ∈ ((𝐴 ∩ (𝐵(,)+∞)) ∖ {𝐵})((abs‘(𝑏 − 𝐵)) < 𝑧 ∧ (abs‘(𝑏 − 𝐵)) < 𝑣))
126	62, 63, 64, 125	syl3anc 1370	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((𝜑 ∧ 𝑦 ∈ ℝ+) ∧ 𝑧 ∈ ℝ+ ∧ ∀𝑤 ∈ 𝐴 ((𝑤 ≠ 𝐵 ∧ (abs‘(𝑤 − 𝐵)) < 𝑧) → (abs‘((𝐹‘𝑤) − 𝑥)) < 𝑦)) ∧ 𝑣 ∈ ℝ+ ∧ ∀𝑤 ∈ (𝐴 ∩ (𝐵(,)+∞))((𝑤 ≠ 𝐵 ∧ (abs‘(𝑤 − 𝐵)) < 𝑣) → (abs‘(((𝐹 ↾ (𝐵(,)+∞))‘𝑤) − 𝑅)) < 𝑦)) → ∃𝑏 ∈ ((𝐴 ∩ (𝐵(,)+∞)) ∖ {𝐵})((abs‘(𝑏 − 𝐵)) < 𝑧 ∧ (abs‘(𝑏 − 𝐵)) < 𝑣))
127		nfv 1911	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ Ⅎ𝑏(((𝜑 ∧ 𝑦 ∈ ℝ+) ∧ 𝑧 ∈ ℝ+ ∧ ∀𝑤 ∈ 𝐴 ((𝑤 ≠ 𝐵 ∧ (abs‘(𝑤 − 𝐵)) < 𝑧) → (abs‘((𝐹‘𝑤) − 𝑥)) < 𝑦)) ∧ 𝑣 ∈ ℝ+ ∧ ∀𝑤 ∈ (𝐴 ∩ (𝐵(,)+∞))((𝑤 ≠ 𝐵 ∧ (abs‘(𝑤 − 𝐵)) < 𝑣) → (abs‘(((𝐹 ↾ (𝐵(,)+∞))‘𝑤) − 𝑅)) < 𝑦))
128		nfre1 3282	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ Ⅎ𝑏∃𝑏 ∈ 𝐴 ((abs‘((𝐹‘𝑏) − 𝑥)) < 𝑦 ∧ (abs‘((𝐹‘𝑏) − 𝑅)) < 𝑦)
129	97	elin1d 4213	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝑏 ∈ ((𝐴 ∩ (𝐵(,)+∞)) ∖ {𝐵}) → 𝑏 ∈ 𝐴)
130	129	3ad2ant2 1133	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((((𝜑 ∧ 𝑦 ∈ ℝ+) ∧ 𝑧 ∈ ℝ+ ∧ ∀𝑤 ∈ 𝐴 ((𝑤 ≠ 𝐵 ∧ (abs‘(𝑤 − 𝐵)) < 𝑧) → (abs‘((𝐹‘𝑤) − 𝑥)) < 𝑦)) ∧ 𝑣 ∈ ℝ+ ∧ ∀𝑤 ∈ (𝐴 ∩ (𝐵(,)+∞))((𝑤 ≠ 𝐵 ∧ (abs‘(𝑤 − 𝐵)) < 𝑣) → (abs‘(((𝐹 ↾ (𝐵(,)+∞))‘𝑤) − 𝑅)) < 𝑦)) ∧ 𝑏 ∈ ((𝐴 ∩ (𝐵(,)+∞)) ∖ {𝐵}) ∧ ((abs‘(𝑏 − 𝐵)) < 𝑧 ∧ (abs‘(𝑏 − 𝐵)) < 𝑣)) → 𝑏 ∈ 𝐴)
131		simp113 1303	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (((((𝜑 ∧ 𝑦 ∈ ℝ+) ∧ 𝑧 ∈ ℝ+ ∧ ∀𝑤 ∈ 𝐴 ((𝑤 ≠ 𝐵 ∧ (abs‘(𝑤 − 𝐵)) < 𝑧) → (abs‘((𝐹‘𝑤) − 𝑥)) < 𝑦)) ∧ 𝑣 ∈ ℝ+ ∧ ∀𝑤 ∈ (𝐴 ∩ (𝐵(,)+∞))((𝑤 ≠ 𝐵 ∧ (abs‘(𝑤 − 𝐵)) < 𝑣) → (abs‘(((𝐹 ↾ (𝐵(,)+∞))‘𝑤) − 𝑅)) < 𝑦)) ∧ 𝑏 ∈ ((𝐴 ∩ (𝐵(,)+∞)) ∖ {𝐵}) ∧ ((abs‘(𝑏 − 𝐵)) < 𝑧 ∧ (abs‘(𝑏 − 𝐵)) < 𝑣)) → ∀𝑤 ∈ 𝐴 ((𝑤 ≠ 𝐵 ∧ (abs‘(𝑤 − 𝐵)) < 𝑧) → (abs‘((𝐹‘𝑤) − 𝑥)) < 𝑦))
132		eldifsni 4794	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (𝑏 ∈ ((𝐴 ∩ (𝐵(,)+∞)) ∖ {𝐵}) → 𝑏 ≠ 𝐵)
133	132	adantr 480	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ((𝑏 ∈ ((𝐴 ∩ (𝐵(,)+∞)) ∖ {𝐵}) ∧ ((abs‘(𝑏 − 𝐵)) < 𝑧 ∧ (abs‘(𝑏 − 𝐵)) < 𝑣)) → 𝑏 ≠ 𝐵)
134		simprl 771	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ((𝑏 ∈ ((𝐴 ∩ (𝐵(,)+∞)) ∖ {𝐵}) ∧ ((abs‘(𝑏 − 𝐵)) < 𝑧 ∧ (abs‘(𝑏 − 𝐵)) < 𝑣)) → (abs‘(𝑏 − 𝐵)) < 𝑧)
135	133, 134	jca 511	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((𝑏 ∈ ((𝐴 ∩ (𝐵(,)+∞)) ∖ {𝐵}) ∧ ((abs‘(𝑏 − 𝐵)) < 𝑧 ∧ (abs‘(𝑏 − 𝐵)) < 𝑣)) → (𝑏 ≠ 𝐵 ∧ (abs‘(𝑏 − 𝐵)) < 𝑧))
136	135	3adant1 1129	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (((((𝜑 ∧ 𝑦 ∈ ℝ+) ∧ 𝑧 ∈ ℝ+ ∧ ∀𝑤 ∈ 𝐴 ((𝑤 ≠ 𝐵 ∧ (abs‘(𝑤 − 𝐵)) < 𝑧) → (abs‘((𝐹‘𝑤) − 𝑥)) < 𝑦)) ∧ 𝑣 ∈ ℝ+ ∧ ∀𝑤 ∈ (𝐴 ∩ (𝐵(,)+∞))((𝑤 ≠ 𝐵 ∧ (abs‘(𝑤 − 𝐵)) < 𝑣) → (abs‘(((𝐹 ↾ (𝐵(,)+∞))‘𝑤) − 𝑅)) < 𝑦)) ∧ 𝑏 ∈ ((𝐴 ∩ (𝐵(,)+∞)) ∖ {𝐵}) ∧ ((abs‘(𝑏 − 𝐵)) < 𝑧 ∧ (abs‘(𝑏 − 𝐵)) < 𝑣)) → (𝑏 ≠ 𝐵 ∧ (abs‘(𝑏 − 𝐵)) < 𝑧))
137		neeq1 3000	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ (𝑤 = 𝑏 → (𝑤 ≠ 𝐵 ↔ 𝑏 ≠ 𝐵))
138		fvoveq1 7453	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ (𝑤 = 𝑏 → (abs‘(𝑤 − 𝐵)) = (abs‘(𝑏 − 𝐵)))
139	138	breq1d 5157	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ (𝑤 = 𝑏 → ((abs‘(𝑤 − 𝐵)) < 𝑧 ↔ (abs‘(𝑏 − 𝐵)) < 𝑧))
140	137, 139	anbi12d 632	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (𝑤 = 𝑏 → ((𝑤 ≠ 𝐵 ∧ (abs‘(𝑤 − 𝐵)) < 𝑧) ↔ (𝑏 ≠ 𝐵 ∧ (abs‘(𝑏 − 𝐵)) < 𝑧)))
141	140	imbrov2fvoveq 7455	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (𝑤 = 𝑏 → (((𝑤 ≠ 𝐵 ∧ (abs‘(𝑤 − 𝐵)) < 𝑧) → (abs‘((𝐹‘𝑤) − 𝑥)) < 𝑦) ↔ ((𝑏 ≠ 𝐵 ∧ (abs‘(𝑏 − 𝐵)) < 𝑧) → (abs‘((𝐹‘𝑏) − 𝑥)) < 𝑦)))
142	141	rspcva 3619	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((𝑏 ∈ 𝐴 ∧ ∀𝑤 ∈ 𝐴 ((𝑤 ≠ 𝐵 ∧ (abs‘(𝑤 − 𝐵)) < 𝑧) → (abs‘((𝐹‘𝑤) − 𝑥)) < 𝑦)) → ((𝑏 ≠ 𝐵 ∧ (abs‘(𝑏 − 𝐵)) < 𝑧) → (abs‘((𝐹‘𝑏) − 𝑥)) < 𝑦))
143	142	imp 406	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (((𝑏 ∈ 𝐴 ∧ ∀𝑤 ∈ 𝐴 ((𝑤 ≠ 𝐵 ∧ (abs‘(𝑤 − 𝐵)) < 𝑧) → (abs‘((𝐹‘𝑤) − 𝑥)) < 𝑦)) ∧ (𝑏 ≠ 𝐵 ∧ (abs‘(𝑏 − 𝐵)) < 𝑧)) → (abs‘((𝐹‘𝑏) − 𝑥)) < 𝑦)
144	130, 131, 136, 143	syl21anc 838	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((((𝜑 ∧ 𝑦 ∈ ℝ+) ∧ 𝑧 ∈ ℝ+ ∧ ∀𝑤 ∈ 𝐴 ((𝑤 ≠ 𝐵 ∧ (abs‘(𝑤 − 𝐵)) < 𝑧) → (abs‘((𝐹‘𝑤) − 𝑥)) < 𝑦)) ∧ 𝑣 ∈ ℝ+ ∧ ∀𝑤 ∈ (𝐴 ∩ (𝐵(,)+∞))((𝑤 ≠ 𝐵 ∧ (abs‘(𝑤 − 𝐵)) < 𝑣) → (abs‘(((𝐹 ↾ (𝐵(,)+∞))‘𝑤) − 𝑅)) < 𝑦)) ∧ 𝑏 ∈ ((𝐴 ∩ (𝐵(,)+∞)) ∖ {𝐵}) ∧ ((abs‘(𝑏 − 𝐵)) < 𝑧 ∧ (abs‘(𝑏 − 𝐵)) < 𝑣)) → (abs‘((𝐹‘𝑏) − 𝑥)) < 𝑦)
145	97	3ad2ant2 1133	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (((((𝜑 ∧ 𝑦 ∈ ℝ+) ∧ 𝑧 ∈ ℝ+ ∧ ∀𝑤 ∈ 𝐴 ((𝑤 ≠ 𝐵 ∧ (abs‘(𝑤 − 𝐵)) < 𝑧) → (abs‘((𝐹‘𝑤) − 𝑥)) < 𝑦)) ∧ 𝑣 ∈ ℝ+ ∧ ∀𝑤 ∈ (𝐴 ∩ (𝐵(,)+∞))((𝑤 ≠ 𝐵 ∧ (abs‘(𝑤 − 𝐵)) < 𝑣) → (abs‘(((𝐹 ↾ (𝐵(,)+∞))‘𝑤) − 𝑅)) < 𝑦)) ∧ 𝑏 ∈ ((𝐴 ∩ (𝐵(,)+∞)) ∖ {𝐵}) ∧ ((abs‘(𝑏 − 𝐵)) < 𝑧 ∧ (abs‘(𝑏 − 𝐵)) < 𝑣)) → 𝑏 ∈ (𝐴 ∩ (𝐵(,)+∞)))
146	62	3ad2ant1 1132	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (((((𝜑 ∧ 𝑦 ∈ ℝ+) ∧ 𝑧 ∈ ℝ+ ∧ ∀𝑤 ∈ 𝐴 ((𝑤 ≠ 𝐵 ∧ (abs‘(𝑤 − 𝐵)) < 𝑧) → (abs‘((𝐹‘𝑤) − 𝑥)) < 𝑦)) ∧ 𝑣 ∈ ℝ+ ∧ ∀𝑤 ∈ (𝐴 ∩ (𝐵(,)+∞))((𝑤 ≠ 𝐵 ∧ (abs‘(𝑤 − 𝐵)) < 𝑣) → (abs‘(((𝐹 ↾ (𝐵(,)+∞))‘𝑤) − 𝑅)) < 𝑦)) ∧ 𝑏 ∈ ((𝐴 ∩ (𝐵(,)+∞)) ∖ {𝐵}) ∧ ((abs‘(𝑏 − 𝐵)) < 𝑧 ∧ (abs‘(𝑏 − 𝐵)) < 𝑣)) → 𝜑)
147		simp13 1204	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (((((𝜑 ∧ 𝑦 ∈ ℝ+) ∧ 𝑧 ∈ ℝ+ ∧ ∀𝑤 ∈ 𝐴 ((𝑤 ≠ 𝐵 ∧ (abs‘(𝑤 − 𝐵)) < 𝑧) → (abs‘((𝐹‘𝑤) − 𝑥)) < 𝑦)) ∧ 𝑣 ∈ ℝ+ ∧ ∀𝑤 ∈ (𝐴 ∩ (𝐵(,)+∞))((𝑤 ≠ 𝐵 ∧ (abs‘(𝑤 − 𝐵)) < 𝑣) → (abs‘(((𝐹 ↾ (𝐵(,)+∞))‘𝑤) − 𝑅)) < 𝑦)) ∧ 𝑏 ∈ ((𝐴 ∩ (𝐵(,)+∞)) ∖ {𝐵}) ∧ ((abs‘(𝑏 − 𝐵)) < 𝑧 ∧ (abs‘(𝑏 − 𝐵)) < 𝑣)) → ∀𝑤 ∈ (𝐴 ∩ (𝐵(,)+∞))((𝑤 ≠ 𝐵 ∧ (abs‘(𝑤 − 𝐵)) < 𝑣) → (abs‘(((𝐹 ↾ (𝐵(,)+∞))‘𝑤) − 𝑅)) < 𝑦))
148		nfv 1911	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ Ⅎ𝑤𝜑
149		nfra1 3281	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ Ⅎ𝑤∀𝑤 ∈ (𝐴 ∩ (𝐵(,)+∞))((𝑤 ≠ 𝐵 ∧ (abs‘(𝑤 − 𝐵)) < 𝑣) → (abs‘(((𝐹 ↾ (𝐵(,)+∞))‘𝑤) − 𝑅)) < 𝑦)
150	148, 149	nfan 1896	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ Ⅎ𝑤(𝜑 ∧ ∀𝑤 ∈ (𝐴 ∩ (𝐵(,)+∞))((𝑤 ≠ 𝐵 ∧ (abs‘(𝑤 − 𝐵)) < 𝑣) → (abs‘(((𝐹 ↾ (𝐵(,)+∞))‘𝑤) − 𝑅)) < 𝑦))
151		elinel2 4211	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ (𝑤 ∈ (𝐴 ∩ (𝐵(,)+∞)) → 𝑤 ∈ (𝐵(,)+∞))
152	151	fvresd 6926	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ (𝑤 ∈ (𝐴 ∩ (𝐵(,)+∞)) → ((𝐹 ↾ (𝐵(,)+∞))‘𝑤) = (𝐹‘𝑤))
153	152	eqcomd 2740	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ (𝑤 ∈ (𝐴 ∩ (𝐵(,)+∞)) → (𝐹‘𝑤) = ((𝐹 ↾ (𝐵(,)+∞))‘𝑤))
154	153	fvoveq1d 7452	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ (𝑤 ∈ (𝐴 ∩ (𝐵(,)+∞)) → (abs‘((𝐹‘𝑤) − 𝑅)) = (abs‘(((𝐹 ↾ (𝐵(,)+∞))‘𝑤) − 𝑅)))
155	154	3ad2ant2 1133	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ (((𝜑 ∧ ∀𝑤 ∈ (𝐴 ∩ (𝐵(,)+∞))((𝑤 ≠ 𝐵 ∧ (abs‘(𝑤 − 𝐵)) < 𝑣) → (abs‘(((𝐹 ↾ (𝐵(,)+∞))‘𝑤) − 𝑅)) < 𝑦)) ∧ 𝑤 ∈ (𝐴 ∩ (𝐵(,)+∞)) ∧ (𝑤 ≠ 𝐵 ∧ (abs‘(𝑤 − 𝐵)) < 𝑣)) → (abs‘((𝐹‘𝑤) − 𝑅)) = (abs‘(((𝐹 ↾ (𝐵(,)+∞))‘𝑤) − 𝑅)))
156		rspa 3245	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ ((∀𝑤 ∈ (𝐴 ∩ (𝐵(,)+∞))((𝑤 ≠ 𝐵 ∧ (abs‘(𝑤 − 𝐵)) < 𝑣) → (abs‘(((𝐹 ↾ (𝐵(,)+∞))‘𝑤) − 𝑅)) < 𝑦) ∧ 𝑤 ∈ (𝐴 ∩ (𝐵(,)+∞))) → ((𝑤 ≠ 𝐵 ∧ (abs‘(𝑤 − 𝐵)) < 𝑣) → (abs‘(((𝐹 ↾ (𝐵(,)+∞))‘𝑤) − 𝑅)) < 𝑦))
157	156	3impia 1116	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ ((∀𝑤 ∈ (𝐴 ∩ (𝐵(,)+∞))((𝑤 ≠ 𝐵 ∧ (abs‘(𝑤 − 𝐵)) < 𝑣) → (abs‘(((𝐹 ↾ (𝐵(,)+∞))‘𝑤) − 𝑅)) < 𝑦) ∧ 𝑤 ∈ (𝐴 ∩ (𝐵(,)+∞)) ∧ (𝑤 ≠ 𝐵 ∧ (abs‘(𝑤 − 𝐵)) < 𝑣)) → (abs‘(((𝐹 ↾ (𝐵(,)+∞))‘𝑤) − 𝑅)) < 𝑦)
158	157	3adant1l 1175	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ (((𝜑 ∧ ∀𝑤 ∈ (𝐴 ∩ (𝐵(,)+∞))((𝑤 ≠ 𝐵 ∧ (abs‘(𝑤 − 𝐵)) < 𝑣) → (abs‘(((𝐹 ↾ (𝐵(,)+∞))‘𝑤) − 𝑅)) < 𝑦)) ∧ 𝑤 ∈ (𝐴 ∩ (𝐵(,)+∞)) ∧ (𝑤 ≠ 𝐵 ∧ (abs‘(𝑤 − 𝐵)) < 𝑣)) → (abs‘(((𝐹 ↾ (𝐵(,)+∞))‘𝑤) − 𝑅)) < 𝑦)
159	155, 158	eqbrtrd 5169	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (((𝜑 ∧ ∀𝑤 ∈ (𝐴 ∩ (𝐵(,)+∞))((𝑤 ≠ 𝐵 ∧ (abs‘(𝑤 − 𝐵)) < 𝑣) → (abs‘(((𝐹 ↾ (𝐵(,)+∞))‘𝑤) − 𝑅)) < 𝑦)) ∧ 𝑤 ∈ (𝐴 ∩ (𝐵(,)+∞)) ∧ (𝑤 ≠ 𝐵 ∧ (abs‘(𝑤 − 𝐵)) < 𝑣)) → (abs‘((𝐹‘𝑤) − 𝑅)) < 𝑦)
160	159	3exp 1118	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ((𝜑 ∧ ∀𝑤 ∈ (𝐴 ∩ (𝐵(,)+∞))((𝑤 ≠ 𝐵 ∧ (abs‘(𝑤 − 𝐵)) < 𝑣) → (abs‘(((𝐹 ↾ (𝐵(,)+∞))‘𝑤) − 𝑅)) < 𝑦)) → (𝑤 ∈ (𝐴 ∩ (𝐵(,)+∞)) → ((𝑤 ≠ 𝐵 ∧ (abs‘(𝑤 − 𝐵)) < 𝑣) → (abs‘((𝐹‘𝑤) − 𝑅)) < 𝑦)))
161	150, 160	ralrimi 3254	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((𝜑 ∧ ∀𝑤 ∈ (𝐴 ∩ (𝐵(,)+∞))((𝑤 ≠ 𝐵 ∧ (abs‘(𝑤 − 𝐵)) < 𝑣) → (abs‘(((𝐹 ↾ (𝐵(,)+∞))‘𝑤) − 𝑅)) < 𝑦)) → ∀𝑤 ∈ (𝐴 ∩ (𝐵(,)+∞))((𝑤 ≠ 𝐵 ∧ (abs‘(𝑤 − 𝐵)) < 𝑣) → (abs‘((𝐹‘𝑤) − 𝑅)) < 𝑦))
162	146, 147, 161	syl2anc 584	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (((((𝜑 ∧ 𝑦 ∈ ℝ+) ∧ 𝑧 ∈ ℝ+ ∧ ∀𝑤 ∈ 𝐴 ((𝑤 ≠ 𝐵 ∧ (abs‘(𝑤 − 𝐵)) < 𝑧) → (abs‘((𝐹‘𝑤) − 𝑥)) < 𝑦)) ∧ 𝑣 ∈ ℝ+ ∧ ∀𝑤 ∈ (𝐴 ∩ (𝐵(,)+∞))((𝑤 ≠ 𝐵 ∧ (abs‘(𝑤 − 𝐵)) < 𝑣) → (abs‘(((𝐹 ↾ (𝐵(,)+∞))‘𝑤) − 𝑅)) < 𝑦)) ∧ 𝑏 ∈ ((𝐴 ∩ (𝐵(,)+∞)) ∖ {𝐵}) ∧ ((abs‘(𝑏 − 𝐵)) < 𝑧 ∧ (abs‘(𝑏 − 𝐵)) < 𝑣)) → ∀𝑤 ∈ (𝐴 ∩ (𝐵(,)+∞))((𝑤 ≠ 𝐵 ∧ (abs‘(𝑤 − 𝐵)) < 𝑣) → (abs‘((𝐹‘𝑤) − 𝑅)) < 𝑦))
163	132	anim1i 615	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ((𝑏 ∈ ((𝐴 ∩ (𝐵(,)+∞)) ∖ {𝐵}) ∧ (abs‘(𝑏 − 𝐵)) < 𝑣) → (𝑏 ≠ 𝐵 ∧ (abs‘(𝑏 − 𝐵)) < 𝑣))
164	163	adantrl 716	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((𝑏 ∈ ((𝐴 ∩ (𝐵(,)+∞)) ∖ {𝐵}) ∧ ((abs‘(𝑏 − 𝐵)) < 𝑧 ∧ (abs‘(𝑏 − 𝐵)) < 𝑣)) → (𝑏 ≠ 𝐵 ∧ (abs‘(𝑏 − 𝐵)) < 𝑣))
165	164	3adant1 1129	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (((((𝜑 ∧ 𝑦 ∈ ℝ+) ∧ 𝑧 ∈ ℝ+ ∧ ∀𝑤 ∈ 𝐴 ((𝑤 ≠ 𝐵 ∧ (abs‘(𝑤 − 𝐵)) < 𝑧) → (abs‘((𝐹‘𝑤) − 𝑥)) < 𝑦)) ∧ 𝑣 ∈ ℝ+ ∧ ∀𝑤 ∈ (𝐴 ∩ (𝐵(,)+∞))((𝑤 ≠ 𝐵 ∧ (abs‘(𝑤 − 𝐵)) < 𝑣) → (abs‘(((𝐹 ↾ (𝐵(,)+∞))‘𝑤) − 𝑅)) < 𝑦)) ∧ 𝑏 ∈ ((𝐴 ∩ (𝐵(,)+∞)) ∖ {𝐵}) ∧ ((abs‘(𝑏 − 𝐵)) < 𝑧 ∧ (abs‘(𝑏 − 𝐵)) < 𝑣)) → (𝑏 ≠ 𝐵 ∧ (abs‘(𝑏 − 𝐵)) < 𝑣))
166	138	breq1d 5157	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ (𝑤 = 𝑏 → ((abs‘(𝑤 − 𝐵)) < 𝑣 ↔ (abs‘(𝑏 − 𝐵)) < 𝑣))
167	137, 166	anbi12d 632	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (𝑤 = 𝑏 → ((𝑤 ≠ 𝐵 ∧ (abs‘(𝑤 − 𝐵)) < 𝑣) ↔ (𝑏 ≠ 𝐵 ∧ (abs‘(𝑏 − 𝐵)) < 𝑣)))
168	167	imbrov2fvoveq 7455	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (𝑤 = 𝑏 → (((𝑤 ≠ 𝐵 ∧ (abs‘(𝑤 − 𝐵)) < 𝑣) → (abs‘((𝐹‘𝑤) − 𝑅)) < 𝑦) ↔ ((𝑏 ≠ 𝐵 ∧ (abs‘(𝑏 − 𝐵)) < 𝑣) → (abs‘((𝐹‘𝑏) − 𝑅)) < 𝑦)))
169	168	rspcva 3619	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((𝑏 ∈ (𝐴 ∩ (𝐵(,)+∞)) ∧ ∀𝑤 ∈ (𝐴 ∩ (𝐵(,)+∞))((𝑤 ≠ 𝐵 ∧ (abs‘(𝑤 − 𝐵)) < 𝑣) → (abs‘((𝐹‘𝑤) − 𝑅)) < 𝑦)) → ((𝑏 ≠ 𝐵 ∧ (abs‘(𝑏 − 𝐵)) < 𝑣) → (abs‘((𝐹‘𝑏) − 𝑅)) < 𝑦))
170	169	imp 406	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (((𝑏 ∈ (𝐴 ∩ (𝐵(,)+∞)) ∧ ∀𝑤 ∈ (𝐴 ∩ (𝐵(,)+∞))((𝑤 ≠ 𝐵 ∧ (abs‘(𝑤 − 𝐵)) < 𝑣) → (abs‘((𝐹‘𝑤) − 𝑅)) < 𝑦)) ∧ (𝑏 ≠ 𝐵 ∧ (abs‘(𝑏 − 𝐵)) < 𝑣)) → (abs‘((𝐹‘𝑏) − 𝑅)) < 𝑦)
171	145, 162, 165, 170	syl21anc 838	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((((𝜑 ∧ 𝑦 ∈ ℝ+) ∧ 𝑧 ∈ ℝ+ ∧ ∀𝑤 ∈ 𝐴 ((𝑤 ≠ 𝐵 ∧ (abs‘(𝑤 − 𝐵)) < 𝑧) → (abs‘((𝐹‘𝑤) − 𝑥)) < 𝑦)) ∧ 𝑣 ∈ ℝ+ ∧ ∀𝑤 ∈ (𝐴 ∩ (𝐵(,)+∞))((𝑤 ≠ 𝐵 ∧ (abs‘(𝑤 − 𝐵)) < 𝑣) → (abs‘(((𝐹 ↾ (𝐵(,)+∞))‘𝑤) − 𝑅)) < 𝑦)) ∧ 𝑏 ∈ ((𝐴 ∩ (𝐵(,)+∞)) ∖ {𝐵}) ∧ ((abs‘(𝑏 − 𝐵)) < 𝑧 ∧ (abs‘(𝑏 − 𝐵)) < 𝑣)) → (abs‘((𝐹‘𝑏) − 𝑅)) < 𝑦)
172		rspe 3246	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((𝑏 ∈ 𝐴 ∧ ((abs‘((𝐹‘𝑏) − 𝑥)) < 𝑦 ∧ (abs‘((𝐹‘𝑏) − 𝑅)) < 𝑦)) → ∃𝑏 ∈ 𝐴 ((abs‘((𝐹‘𝑏) − 𝑥)) < 𝑦 ∧ (abs‘((𝐹‘𝑏) − 𝑅)) < 𝑦))
173	130, 144, 171, 172	syl12anc 837	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((((𝜑 ∧ 𝑦 ∈ ℝ+) ∧ 𝑧 ∈ ℝ+ ∧ ∀𝑤 ∈ 𝐴 ((𝑤 ≠ 𝐵 ∧ (abs‘(𝑤 − 𝐵)) < 𝑧) → (abs‘((𝐹‘𝑤) − 𝑥)) < 𝑦)) ∧ 𝑣 ∈ ℝ+ ∧ ∀𝑤 ∈ (𝐴 ∩ (𝐵(,)+∞))((𝑤 ≠ 𝐵 ∧ (abs‘(𝑤 − 𝐵)) < 𝑣) → (abs‘(((𝐹 ↾ (𝐵(,)+∞))‘𝑤) − 𝑅)) < 𝑦)) ∧ 𝑏 ∈ ((𝐴 ∩ (𝐵(,)+∞)) ∖ {𝐵}) ∧ ((abs‘(𝑏 − 𝐵)) < 𝑧 ∧ (abs‘(𝑏 − 𝐵)) < 𝑣)) → ∃𝑏 ∈ 𝐴 ((abs‘((𝐹‘𝑏) − 𝑥)) < 𝑦 ∧ (abs‘((𝐹‘𝑏) − 𝑅)) < 𝑦))
174	173	3exp 1118	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((((𝜑 ∧ 𝑦 ∈ ℝ+) ∧ 𝑧 ∈ ℝ+ ∧ ∀𝑤 ∈ 𝐴 ((𝑤 ≠ 𝐵 ∧ (abs‘(𝑤 − 𝐵)) < 𝑧) → (abs‘((𝐹‘𝑤) − 𝑥)) < 𝑦)) ∧ 𝑣 ∈ ℝ+ ∧ ∀𝑤 ∈ (𝐴 ∩ (𝐵(,)+∞))((𝑤 ≠ 𝐵 ∧ (abs‘(𝑤 − 𝐵)) < 𝑣) → (abs‘(((𝐹 ↾ (𝐵(,)+∞))‘𝑤) − 𝑅)) < 𝑦)) → (𝑏 ∈ ((𝐴 ∩ (𝐵(,)+∞)) ∖ {𝐵}) → (((abs‘(𝑏 − 𝐵)) < 𝑧 ∧ (abs‘(𝑏 − 𝐵)) < 𝑣) → ∃𝑏 ∈ 𝐴 ((abs‘((𝐹‘𝑏) − 𝑥)) < 𝑦 ∧ (abs‘((𝐹‘𝑏) − 𝑅)) < 𝑦))))
175	127, 128, 174	rexlimd 3263	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((𝜑 ∧ 𝑦 ∈ ℝ+) ∧ 𝑧 ∈ ℝ+ ∧ ∀𝑤 ∈ 𝐴 ((𝑤 ≠ 𝐵 ∧ (abs‘(𝑤 − 𝐵)) < 𝑧) → (abs‘((𝐹‘𝑤) − 𝑥)) < 𝑦)) ∧ 𝑣 ∈ ℝ+ ∧ ∀𝑤 ∈ (𝐴 ∩ (𝐵(,)+∞))((𝑤 ≠ 𝐵 ∧ (abs‘(𝑤 − 𝐵)) < 𝑣) → (abs‘(((𝐹 ↾ (𝐵(,)+∞))‘𝑤) − 𝑅)) < 𝑦)) → (∃𝑏 ∈ ((𝐴 ∩ (𝐵(,)+∞)) ∖ {𝐵})((abs‘(𝑏 − 𝐵)) < 𝑧 ∧ (abs‘(𝑏 − 𝐵)) < 𝑣) → ∃𝑏 ∈ 𝐴 ((abs‘((𝐹‘𝑏) − 𝑥)) < 𝑦 ∧ (abs‘((𝐹‘𝑏) − 𝑅)) < 𝑦)))
176	126, 175	mpd 15	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((𝜑 ∧ 𝑦 ∈ ℝ+) ∧ 𝑧 ∈ ℝ+ ∧ ∀𝑤 ∈ 𝐴 ((𝑤 ≠ 𝐵 ∧ (abs‘(𝑤 − 𝐵)) < 𝑧) → (abs‘((𝐹‘𝑤) − 𝑥)) < 𝑦)) ∧ 𝑣 ∈ ℝ+ ∧ ∀𝑤 ∈ (𝐴 ∩ (𝐵(,)+∞))((𝑤 ≠ 𝐵 ∧ (abs‘(𝑤 − 𝐵)) < 𝑣) → (abs‘(((𝐹 ↾ (𝐵(,)+∞))‘𝑤) − 𝑅)) < 𝑦)) → ∃𝑏 ∈ 𝐴 ((abs‘((𝐹‘𝑏) − 𝑥)) < 𝑦 ∧ (abs‘((𝐹‘𝑏) − 𝑅)) < 𝑦))
177	176	3exp 1118	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜑 ∧ 𝑦 ∈ ℝ+) ∧ 𝑧 ∈ ℝ+ ∧ ∀𝑤 ∈ 𝐴 ((𝑤 ≠ 𝐵 ∧ (abs‘(𝑤 − 𝐵)) < 𝑧) → (abs‘((𝐹‘𝑤) − 𝑥)) < 𝑦)) → (𝑣 ∈ ℝ+ → (∀𝑤 ∈ (𝐴 ∩ (𝐵(,)+∞))((𝑤 ≠ 𝐵 ∧ (abs‘(𝑤 − 𝐵)) < 𝑣) → (abs‘(((𝐹 ↾ (𝐵(,)+∞))‘𝑤) − 𝑅)) < 𝑦) → ∃𝑏 ∈ 𝐴 ((abs‘((𝐹‘𝑏) − 𝑥)) < 𝑦 ∧ (abs‘((𝐹‘𝑏) − 𝑅)) < 𝑦))))
178	177	rexlimdv 3150	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ 𝑦 ∈ ℝ+) ∧ 𝑧 ∈ ℝ+ ∧ ∀𝑤 ∈ 𝐴 ((𝑤 ≠ 𝐵 ∧ (abs‘(𝑤 − 𝐵)) < 𝑧) → (abs‘((𝐹‘𝑤) − 𝑥)) < 𝑦)) → (∃𝑣 ∈ ℝ+ ∀𝑤 ∈ (𝐴 ∩ (𝐵(,)+∞))((𝑤 ≠ 𝐵 ∧ (abs‘(𝑤 − 𝐵)) < 𝑣) → (abs‘(((𝐹 ↾ (𝐵(,)+∞))‘𝑤) − 𝑅)) < 𝑦) → ∃𝑏 ∈ 𝐴 ((abs‘((𝐹‘𝑏) − 𝑥)) < 𝑦 ∧ (abs‘((𝐹‘𝑏) − 𝑅)) < 𝑦)))
179	61, 178	mpd 15	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑦 ∈ ℝ+) ∧ 𝑧 ∈ ℝ+ ∧ ∀𝑤 ∈ 𝐴 ((𝑤 ≠ 𝐵 ∧ (abs‘(𝑤 − 𝐵)) < 𝑧) → (abs‘((𝐹‘𝑤) − 𝑥)) < 𝑦)) → ∃𝑏 ∈ 𝐴 ((abs‘((𝐹‘𝑏) − 𝑥)) < 𝑦 ∧ (abs‘((𝐹‘𝑏) − 𝑅)) < 𝑦))
180	179	3exp 1118	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑦 ∈ ℝ+) → (𝑧 ∈ ℝ+ → (∀𝑤 ∈ 𝐴 ((𝑤 ≠ 𝐵 ∧ (abs‘(𝑤 − 𝐵)) < 𝑧) → (abs‘((𝐹‘𝑤) − 𝑥)) < 𝑦) → ∃𝑏 ∈ 𝐴 ((abs‘((𝐹‘𝑏) − 𝑥)) < 𝑦 ∧ (abs‘((𝐹‘𝑏) − 𝑅)) < 𝑦))))
181	180	rexlimdv 3150	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑦 ∈ ℝ+) → (∃𝑧 ∈ ℝ+ ∀𝑤 ∈ 𝐴 ((𝑤 ≠ 𝐵 ∧ (abs‘(𝑤 − 𝐵)) < 𝑧) → (abs‘((𝐹‘𝑤) − 𝑥)) < 𝑦) → ∃𝑏 ∈ 𝐴 ((abs‘((𝐹‘𝑏) − 𝑥)) < 𝑦 ∧ (abs‘((𝐹‘𝑏) − 𝑅)) < 𝑦)))
182	181	imp 406	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑦 ∈ ℝ+) ∧ ∃𝑧 ∈ ℝ+ ∀𝑤 ∈ 𝐴 ((𝑤 ≠ 𝐵 ∧ (abs‘(𝑤 − 𝐵)) < 𝑧) → (abs‘((𝐹‘𝑤) − 𝑥)) < 𝑦)) → ∃𝑏 ∈ 𝐴 ((abs‘((𝐹‘𝑏) − 𝑥)) < 𝑦 ∧ (abs‘((𝐹‘𝑏) − 𝑅)) < 𝑦))
183	182	adantllr 719	. . . . . . . . . . . . . 14 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℂ) ∧ 𝑦 ∈ ℝ+) ∧ ∃𝑧 ∈ ℝ+ ∀𝑤 ∈ 𝐴 ((𝑤 ≠ 𝐵 ∧ (abs‘(𝑤 − 𝐵)) < 𝑧) → (abs‘((𝐹‘𝑤) − 𝑥)) < 𝑦)) → ∃𝑏 ∈ 𝐴 ((abs‘((𝐹‘𝑏) − 𝑥)) < 𝑦 ∧ (abs‘((𝐹‘𝑏) − 𝑅)) < 𝑦))
184	183	ad2antrr 726	. . . . . . . . . . . . 13 ⊢ ((((((𝜑 ∧ 𝑥 ∈ ℂ) ∧ 𝑦 ∈ ℝ+) ∧ ∃𝑧 ∈ ℝ+ ∀𝑤 ∈ 𝐴 ((𝑤 ≠ 𝐵 ∧ (abs‘(𝑤 − 𝐵)) < 𝑧) → (abs‘((𝐹‘𝑤) − 𝑥)) < 𝑦)) ∧ 𝑎 ∈ 𝐴) ∧ ((abs‘((𝐹‘𝑎) − 𝑥)) < 𝑦 ∧ (abs‘((𝐹‘𝑎) − 𝐿)) < 𝑦)) → ∃𝑏 ∈ 𝐴 ((abs‘((𝐹‘𝑏) − 𝑥)) < 𝑦 ∧ (abs‘((𝐹‘𝑏) − 𝑅)) < 𝑦))
185	3	ad6antr 736	. . . . . . . . . . . . . . . . . . 19 ⊢ (((((((𝜑 ∧ 𝑥 ∈ ℂ) ∧ 𝑦 ∈ ℝ+) ∧ 𝑎 ∈ 𝐴) ∧ ((abs‘((𝐹‘𝑎) − 𝑥)) < 𝑦 ∧ (abs‘((𝐹‘𝑎) − 𝐿)) < 𝑦)) ∧ 𝑏 ∈ 𝐴) ∧ ((abs‘((𝐹‘𝑏) − 𝑥)) < 𝑦 ∧ (abs‘((𝐹‘𝑏) − 𝑅)) < 𝑦)) → 𝑅 ∈ ℂ)
186	7	ad6antr 736	. . . . . . . . . . . . . . . . . . 19 ⊢ (((((((𝜑 ∧ 𝑥 ∈ ℂ) ∧ 𝑦 ∈ ℝ+) ∧ 𝑎 ∈ 𝐴) ∧ ((abs‘((𝐹‘𝑎) − 𝑥)) < 𝑦 ∧ (abs‘((𝐹‘𝑎) − 𝐿)) < 𝑦)) ∧ 𝑏 ∈ 𝐴) ∧ ((abs‘((𝐹‘𝑏) − 𝑥)) < 𝑦 ∧ (abs‘((𝐹‘𝑏) − 𝑅)) < 𝑦)) → 𝐿 ∈ ℂ)
187	185, 186	subcld 11617	. . . . . . . . . . . . . . . . . 18 ⊢ (((((((𝜑 ∧ 𝑥 ∈ ℂ) ∧ 𝑦 ∈ ℝ+) ∧ 𝑎 ∈ 𝐴) ∧ ((abs‘((𝐹‘𝑎) − 𝑥)) < 𝑦 ∧ (abs‘((𝐹‘𝑎) − 𝐿)) < 𝑦)) ∧ 𝑏 ∈ 𝐴) ∧ ((abs‘((𝐹‘𝑏) − 𝑥)) < 𝑦 ∧ (abs‘((𝐹‘𝑏) − 𝑅)) < 𝑦)) → (𝑅 − 𝐿) ∈ ℂ)
188	187	abscld 15471	. . . . . . . . . . . . . . . . 17 ⊢ (((((((𝜑 ∧ 𝑥 ∈ ℂ) ∧ 𝑦 ∈ ℝ+) ∧ 𝑎 ∈ 𝐴) ∧ ((abs‘((𝐹‘𝑎) − 𝑥)) < 𝑦 ∧ (abs‘((𝐹‘𝑎) − 𝐿)) < 𝑦)) ∧ 𝑏 ∈ 𝐴) ∧ ((abs‘((𝐹‘𝑏) − 𝑥)) < 𝑦 ∧ (abs‘((𝐹‘𝑏) − 𝑅)) < 𝑦)) → (abs‘(𝑅 − 𝐿)) ∈ ℝ)
189		simp-6l 787	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((((((𝜑 ∧ 𝑥 ∈ ℂ) ∧ 𝑦 ∈ ℝ+) ∧ 𝑎 ∈ 𝐴) ∧ ((abs‘((𝐹‘𝑎) − 𝑥)) < 𝑦 ∧ (abs‘((𝐹‘𝑎) − 𝐿)) < 𝑦)) ∧ 𝑏 ∈ 𝐴) ∧ ((abs‘((𝐹‘𝑏) − 𝑥)) < 𝑦 ∧ (abs‘((𝐹‘𝑏) − 𝑅)) < 𝑦)) → 𝜑)
190		simplr 769	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((((((𝜑 ∧ 𝑥 ∈ ℂ) ∧ 𝑦 ∈ ℝ+) ∧ 𝑎 ∈ 𝐴) ∧ ((abs‘((𝐹‘𝑎) − 𝑥)) < 𝑦 ∧ (abs‘((𝐹‘𝑎) − 𝐿)) < 𝑦)) ∧ 𝑏 ∈ 𝐴) ∧ ((abs‘((𝐹‘𝑏) − 𝑥)) < 𝑦 ∧ (abs‘((𝐹‘𝑏) − 𝑅)) < 𝑦)) → 𝑏 ∈ 𝐴)
191	36	ffvelcdmda 7103	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝜑 ∧ 𝑏 ∈ 𝐴) → (𝐹‘𝑏) ∈ ℂ)
192	189, 190, 191	syl2anc 584	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((((((𝜑 ∧ 𝑥 ∈ ℂ) ∧ 𝑦 ∈ ℝ+) ∧ 𝑎 ∈ 𝐴) ∧ ((abs‘((𝐹‘𝑎) − 𝑥)) < 𝑦 ∧ (abs‘((𝐹‘𝑎) − 𝐿)) < 𝑦)) ∧ 𝑏 ∈ 𝐴) ∧ ((abs‘((𝐹‘𝑏) − 𝑥)) < 𝑦 ∧ (abs‘((𝐹‘𝑏) − 𝑅)) < 𝑦)) → (𝐹‘𝑏) ∈ ℂ)
193	185, 192	subcld 11617	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((((((𝜑 ∧ 𝑥 ∈ ℂ) ∧ 𝑦 ∈ ℝ+) ∧ 𝑎 ∈ 𝐴) ∧ ((abs‘((𝐹‘𝑎) − 𝑥)) < 𝑦 ∧ (abs‘((𝐹‘𝑎) − 𝐿)) < 𝑦)) ∧ 𝑏 ∈ 𝐴) ∧ ((abs‘((𝐹‘𝑏) − 𝑥)) < 𝑦 ∧ (abs‘((𝐹‘𝑏) − 𝑅)) < 𝑦)) → (𝑅 − (𝐹‘𝑏)) ∈ ℂ)
194	193	abscld 15471	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((((((𝜑 ∧ 𝑥 ∈ ℂ) ∧ 𝑦 ∈ ℝ+) ∧ 𝑎 ∈ 𝐴) ∧ ((abs‘((𝐹‘𝑎) − 𝑥)) < 𝑦 ∧ (abs‘((𝐹‘𝑎) − 𝐿)) < 𝑦)) ∧ 𝑏 ∈ 𝐴) ∧ ((abs‘((𝐹‘𝑏) − 𝑥)) < 𝑦 ∧ (abs‘((𝐹‘𝑏) − 𝑅)) < 𝑦)) → (abs‘(𝑅 − (𝐹‘𝑏))) ∈ ℝ)
195		simp-6r 788	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((((((𝜑 ∧ 𝑥 ∈ ℂ) ∧ 𝑦 ∈ ℝ+) ∧ 𝑎 ∈ 𝐴) ∧ ((abs‘((𝐹‘𝑎) − 𝑥)) < 𝑦 ∧ (abs‘((𝐹‘𝑎) − 𝐿)) < 𝑦)) ∧ 𝑏 ∈ 𝐴) ∧ ((abs‘((𝐹‘𝑏) − 𝑥)) < 𝑦 ∧ (abs‘((𝐹‘𝑏) − 𝑅)) < 𝑦)) → 𝑥 ∈ ℂ)
196	192, 195	subcld 11617	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((((((𝜑 ∧ 𝑥 ∈ ℂ) ∧ 𝑦 ∈ ℝ+) ∧ 𝑎 ∈ 𝐴) ∧ ((abs‘((𝐹‘𝑎) − 𝑥)) < 𝑦 ∧ (abs‘((𝐹‘𝑎) − 𝐿)) < 𝑦)) ∧ 𝑏 ∈ 𝐴) ∧ ((abs‘((𝐹‘𝑏) − 𝑥)) < 𝑦 ∧ (abs‘((𝐹‘𝑏) − 𝑅)) < 𝑦)) → ((𝐹‘𝑏) − 𝑥) ∈ ℂ)
197	196	abscld 15471	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((((((𝜑 ∧ 𝑥 ∈ ℂ) ∧ 𝑦 ∈ ℝ+) ∧ 𝑎 ∈ 𝐴) ∧ ((abs‘((𝐹‘𝑎) − 𝑥)) < 𝑦 ∧ (abs‘((𝐹‘𝑎) − 𝐿)) < 𝑦)) ∧ 𝑏 ∈ 𝐴) ∧ ((abs‘((𝐹‘𝑏) − 𝑥)) < 𝑦 ∧ (abs‘((𝐹‘𝑏) − 𝑅)) < 𝑦)) → (abs‘((𝐹‘𝑏) − 𝑥)) ∈ ℝ)
198	194, 197	readdcld 11287	. . . . . . . . . . . . . . . . . . 19 ⊢ (((((((𝜑 ∧ 𝑥 ∈ ℂ) ∧ 𝑦 ∈ ℝ+) ∧ 𝑎 ∈ 𝐴) ∧ ((abs‘((𝐹‘𝑎) − 𝑥)) < 𝑦 ∧ (abs‘((𝐹‘𝑎) − 𝐿)) < 𝑦)) ∧ 𝑏 ∈ 𝐴) ∧ ((abs‘((𝐹‘𝑏) − 𝑥)) < 𝑦 ∧ (abs‘((𝐹‘𝑏) − 𝑅)) < 𝑦)) → ((abs‘(𝑅 − (𝐹‘𝑏))) + (abs‘((𝐹‘𝑏) − 𝑥))) ∈ ℝ)
199		simp-4r 784	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((((((𝜑 ∧ 𝑥 ∈ ℂ) ∧ 𝑦 ∈ ℝ+) ∧ 𝑎 ∈ 𝐴) ∧ ((abs‘((𝐹‘𝑎) − 𝑥)) < 𝑦 ∧ (abs‘((𝐹‘𝑎) − 𝐿)) < 𝑦)) ∧ 𝑏 ∈ 𝐴) ∧ ((abs‘((𝐹‘𝑏) − 𝑥)) < 𝑦 ∧ (abs‘((𝐹‘𝑏) − 𝑅)) < 𝑦)) → 𝑎 ∈ 𝐴)
200	36	ffvelcdmda 7103	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝜑 ∧ 𝑎 ∈ 𝐴) → (𝐹‘𝑎) ∈ ℂ)
201	189, 199, 200	syl2anc 584	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((((((𝜑 ∧ 𝑥 ∈ ℂ) ∧ 𝑦 ∈ ℝ+) ∧ 𝑎 ∈ 𝐴) ∧ ((abs‘((𝐹‘𝑎) − 𝑥)) < 𝑦 ∧ (abs‘((𝐹‘𝑎) − 𝐿)) < 𝑦)) ∧ 𝑏 ∈ 𝐴) ∧ ((abs‘((𝐹‘𝑏) − 𝑥)) < 𝑦 ∧ (abs‘((𝐹‘𝑏) − 𝑅)) < 𝑦)) → (𝐹‘𝑎) ∈ ℂ)
202	195, 201	subcld 11617	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((((((𝜑 ∧ 𝑥 ∈ ℂ) ∧ 𝑦 ∈ ℝ+) ∧ 𝑎 ∈ 𝐴) ∧ ((abs‘((𝐹‘𝑎) − 𝑥)) < 𝑦 ∧ (abs‘((𝐹‘𝑎) − 𝐿)) < 𝑦)) ∧ 𝑏 ∈ 𝐴) ∧ ((abs‘((𝐹‘𝑏) − 𝑥)) < 𝑦 ∧ (abs‘((𝐹‘𝑏) − 𝑅)) < 𝑦)) → (𝑥 − (𝐹‘𝑎)) ∈ ℂ)
203	202	abscld 15471	. . . . . . . . . . . . . . . . . . 19 ⊢ (((((((𝜑 ∧ 𝑥 ∈ ℂ) ∧ 𝑦 ∈ ℝ+) ∧ 𝑎 ∈ 𝐴) ∧ ((abs‘((𝐹‘𝑎) − 𝑥)) < 𝑦 ∧ (abs‘((𝐹‘𝑎) − 𝐿)) < 𝑦)) ∧ 𝑏 ∈ 𝐴) ∧ ((abs‘((𝐹‘𝑏) − 𝑥)) < 𝑦 ∧ (abs‘((𝐹‘𝑏) − 𝑅)) < 𝑦)) → (abs‘(𝑥 − (𝐹‘𝑎))) ∈ ℝ)
204	198, 203	readdcld 11287	. . . . . . . . . . . . . . . . . 18 ⊢ (((((((𝜑 ∧ 𝑥 ∈ ℂ) ∧ 𝑦 ∈ ℝ+) ∧ 𝑎 ∈ 𝐴) ∧ ((abs‘((𝐹‘𝑎) − 𝑥)) < 𝑦 ∧ (abs‘((𝐹‘𝑎) − 𝐿)) < 𝑦)) ∧ 𝑏 ∈ 𝐴) ∧ ((abs‘((𝐹‘𝑏) − 𝑥)) < 𝑦 ∧ (abs‘((𝐹‘𝑏) − 𝑅)) < 𝑦)) → (((abs‘(𝑅 − (𝐹‘𝑏))) + (abs‘((𝐹‘𝑏) − 𝑥))) + (abs‘(𝑥 − (𝐹‘𝑎)))) ∈ ℝ)
205	201, 186	subcld 11617	. . . . . . . . . . . . . . . . . . 19 ⊢ (((((((𝜑 ∧ 𝑥 ∈ ℂ) ∧ 𝑦 ∈ ℝ+) ∧ 𝑎 ∈ 𝐴) ∧ ((abs‘((𝐹‘𝑎) − 𝑥)) < 𝑦 ∧ (abs‘((𝐹‘𝑎) − 𝐿)) < 𝑦)) ∧ 𝑏 ∈ 𝐴) ∧ ((abs‘((𝐹‘𝑏) − 𝑥)) < 𝑦 ∧ (abs‘((𝐹‘𝑏) − 𝑅)) < 𝑦)) → ((𝐹‘𝑎) − 𝐿) ∈ ℂ)
206	205	abscld 15471	. . . . . . . . . . . . . . . . . 18 ⊢ (((((((𝜑 ∧ 𝑥 ∈ ℂ) ∧ 𝑦 ∈ ℝ+) ∧ 𝑎 ∈ 𝐴) ∧ ((abs‘((𝐹‘𝑎) − 𝑥)) < 𝑦 ∧ (abs‘((𝐹‘𝑎) − 𝐿)) < 𝑦)) ∧ 𝑏 ∈ 𝐴) ∧ ((abs‘((𝐹‘𝑏) − 𝑥)) < 𝑦 ∧ (abs‘((𝐹‘𝑏) − 𝑅)) < 𝑦)) → (abs‘((𝐹‘𝑎) − 𝐿)) ∈ ℝ)
207	204, 206	readdcld 11287	. . . . . . . . . . . . . . . . 17 ⊢ (((((((𝜑 ∧ 𝑥 ∈ ℂ) ∧ 𝑦 ∈ ℝ+) ∧ 𝑎 ∈ 𝐴) ∧ ((abs‘((𝐹‘𝑎) − 𝑥)) < 𝑦 ∧ (abs‘((𝐹‘𝑎) − 𝐿)) < 𝑦)) ∧ 𝑏 ∈ 𝐴) ∧ ((abs‘((𝐹‘𝑏) − 𝑥)) < 𝑦 ∧ (abs‘((𝐹‘𝑏) − 𝑅)) < 𝑦)) → ((((abs‘(𝑅 − (𝐹‘𝑏))) + (abs‘((𝐹‘𝑏) − 𝑥))) + (abs‘(𝑥 − (𝐹‘𝑎)))) + (abs‘((𝐹‘𝑎) − 𝐿))) ∈ ℝ)
208	15	a1i 11	. . . . . . . . . . . . . . . . . 18 ⊢ (((((((𝜑 ∧ 𝑥 ∈ ℂ) ∧ 𝑦 ∈ ℝ+) ∧ 𝑎 ∈ 𝐴) ∧ ((abs‘((𝐹‘𝑎) − 𝑥)) < 𝑦 ∧ (abs‘((𝐹‘𝑎) − 𝐿)) < 𝑦)) ∧ 𝑏 ∈ 𝐴) ∧ ((abs‘((𝐹‘𝑏) − 𝑥)) < 𝑦 ∧ (abs‘((𝐹‘𝑏) − 𝑅)) < 𝑦)) → 4 ∈ ℝ)
209		rpre 13040	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑦 ∈ ℝ+ → 𝑦 ∈ ℝ)
210	209	ad5antlr 735	. . . . . . . . . . . . . . . . . 18 ⊢ (((((((𝜑 ∧ 𝑥 ∈ ℂ) ∧ 𝑦 ∈ ℝ+) ∧ 𝑎 ∈ 𝐴) ∧ ((abs‘((𝐹‘𝑎) − 𝑥)) < 𝑦 ∧ (abs‘((𝐹‘𝑎) − 𝐿)) < 𝑦)) ∧ 𝑏 ∈ 𝐴) ∧ ((abs‘((𝐹‘𝑏) − 𝑥)) < 𝑦 ∧ (abs‘((𝐹‘𝑏) − 𝑅)) < 𝑦)) → 𝑦 ∈ ℝ)
211	208, 210	remulcld 11288	. . . . . . . . . . . . . . . . 17 ⊢ (((((((𝜑 ∧ 𝑥 ∈ ℂ) ∧ 𝑦 ∈ ℝ+) ∧ 𝑎 ∈ 𝐴) ∧ ((abs‘((𝐹‘𝑎) − 𝑥)) < 𝑦 ∧ (abs‘((𝐹‘𝑎) − 𝐿)) < 𝑦)) ∧ 𝑏 ∈ 𝐴) ∧ ((abs‘((𝐹‘𝑏) − 𝑥)) < 𝑦 ∧ (abs‘((𝐹‘𝑏) − 𝑅)) < 𝑦)) → (4 · 𝑦) ∈ ℝ)
212	185, 192, 195, 201, 186	absnpncan3d 45257	. . . . . . . . . . . . . . . . 17 ⊢ (((((((𝜑 ∧ 𝑥 ∈ ℂ) ∧ 𝑦 ∈ ℝ+) ∧ 𝑎 ∈ 𝐴) ∧ ((abs‘((𝐹‘𝑎) − 𝑥)) < 𝑦 ∧ (abs‘((𝐹‘𝑎) − 𝐿)) < 𝑦)) ∧ 𝑏 ∈ 𝐴) ∧ ((abs‘((𝐹‘𝑏) − 𝑥)) < 𝑦 ∧ (abs‘((𝐹‘𝑏) − 𝑅)) < 𝑦)) → (abs‘(𝑅 − 𝐿)) ≤ ((((abs‘(𝑅 − (𝐹‘𝑏))) + (abs‘((𝐹‘𝑏) − 𝑥))) + (abs‘(𝑥 − (𝐹‘𝑎)))) + (abs‘((𝐹‘𝑎) − 𝐿))))
213	185, 192	abssubd 15488	. . . . . . . . . . . . . . . . . . 19 ⊢ (((((((𝜑 ∧ 𝑥 ∈ ℂ) ∧ 𝑦 ∈ ℝ+) ∧ 𝑎 ∈ 𝐴) ∧ ((abs‘((𝐹‘𝑎) − 𝑥)) < 𝑦 ∧ (abs‘((𝐹‘𝑎) − 𝐿)) < 𝑦)) ∧ 𝑏 ∈ 𝐴) ∧ ((abs‘((𝐹‘𝑏) − 𝑥)) < 𝑦 ∧ (abs‘((𝐹‘𝑏) − 𝑅)) < 𝑦)) → (abs‘(𝑅 − (𝐹‘𝑏))) = (abs‘((𝐹‘𝑏) − 𝑅)))
214		simprr 773	. . . . . . . . . . . . . . . . . . 19 ⊢ (((((((𝜑 ∧ 𝑥 ∈ ℂ) ∧ 𝑦 ∈ ℝ+) ∧ 𝑎 ∈ 𝐴) ∧ ((abs‘((𝐹‘𝑎) − 𝑥)) < 𝑦 ∧ (abs‘((𝐹‘𝑎) − 𝐿)) < 𝑦)) ∧ 𝑏 ∈ 𝐴) ∧ ((abs‘((𝐹‘𝑏) − 𝑥)) < 𝑦 ∧ (abs‘((𝐹‘𝑏) − 𝑅)) < 𝑦)) → (abs‘((𝐹‘𝑏) − 𝑅)) < 𝑦)
215	213, 214	eqbrtrd 5169	. . . . . . . . . . . . . . . . . 18 ⊢ (((((((𝜑 ∧ 𝑥 ∈ ℂ) ∧ 𝑦 ∈ ℝ+) ∧ 𝑎 ∈ 𝐴) ∧ ((abs‘((𝐹‘𝑎) − 𝑥)) < 𝑦 ∧ (abs‘((𝐹‘𝑎) − 𝐿)) < 𝑦)) ∧ 𝑏 ∈ 𝐴) ∧ ((abs‘((𝐹‘𝑏) − 𝑥)) < 𝑦 ∧ (abs‘((𝐹‘𝑏) − 𝑅)) < 𝑦)) → (abs‘(𝑅 − (𝐹‘𝑏))) < 𝑦)
216		simprl 771	. . . . . . . . . . . . . . . . . 18 ⊢ (((((((𝜑 ∧ 𝑥 ∈ ℂ) ∧ 𝑦 ∈ ℝ+) ∧ 𝑎 ∈ 𝐴) ∧ ((abs‘((𝐹‘𝑎) − 𝑥)) < 𝑦 ∧ (abs‘((𝐹‘𝑎) − 𝐿)) < 𝑦)) ∧ 𝑏 ∈ 𝐴) ∧ ((abs‘((𝐹‘𝑏) − 𝑥)) < 𝑦 ∧ (abs‘((𝐹‘𝑏) − 𝑅)) < 𝑦)) → (abs‘((𝐹‘𝑏) − 𝑥)) < 𝑦)
217		simp-5r 786	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((((𝜑 ∧ 𝑥 ∈ ℂ) ∧ 𝑦 ∈ ℝ+) ∧ 𝑎 ∈ 𝐴) ∧ ((abs‘((𝐹‘𝑎) − 𝑥)) < 𝑦 ∧ (abs‘((𝐹‘𝑎) − 𝐿)) < 𝑦)) ∧ 𝑏 ∈ 𝐴) → 𝑥 ∈ ℂ)
218	200	ad5ant14 758	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((((𝜑 ∧ 𝑥 ∈ ℂ) ∧ 𝑦 ∈ ℝ+) ∧ 𝑎 ∈ 𝐴) ∧ ((abs‘((𝐹‘𝑎) − 𝑥)) < 𝑦 ∧ (abs‘((𝐹‘𝑎) − 𝐿)) < 𝑦)) → (𝐹‘𝑎) ∈ ℂ)
219	218	adantr 480	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((((𝜑 ∧ 𝑥 ∈ ℂ) ∧ 𝑦 ∈ ℝ+) ∧ 𝑎 ∈ 𝐴) ∧ ((abs‘((𝐹‘𝑎) − 𝑥)) < 𝑦 ∧ (abs‘((𝐹‘𝑎) − 𝐿)) < 𝑦)) ∧ 𝑏 ∈ 𝐴) → (𝐹‘𝑎) ∈ ℂ)
220	217, 219	abssubd 15488	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((((𝜑 ∧ 𝑥 ∈ ℂ) ∧ 𝑦 ∈ ℝ+) ∧ 𝑎 ∈ 𝐴) ∧ ((abs‘((𝐹‘𝑎) − 𝑥)) < 𝑦 ∧ (abs‘((𝐹‘𝑎) − 𝐿)) < 𝑦)) ∧ 𝑏 ∈ 𝐴) → (abs‘(𝑥 − (𝐹‘𝑎))) = (abs‘((𝐹‘𝑎) − 𝑥)))
221		simplrl 777	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((((𝜑 ∧ 𝑥 ∈ ℂ) ∧ 𝑦 ∈ ℝ+) ∧ 𝑎 ∈ 𝐴) ∧ ((abs‘((𝐹‘𝑎) − 𝑥)) < 𝑦 ∧ (abs‘((𝐹‘𝑎) − 𝐿)) < 𝑦)) ∧ 𝑏 ∈ 𝐴) → (abs‘((𝐹‘𝑎) − 𝑥)) < 𝑦)
222	220, 221	eqbrtrd 5169	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((((𝜑 ∧ 𝑥 ∈ ℂ) ∧ 𝑦 ∈ ℝ+) ∧ 𝑎 ∈ 𝐴) ∧ ((abs‘((𝐹‘𝑎) − 𝑥)) < 𝑦 ∧ (abs‘((𝐹‘𝑎) − 𝐿)) < 𝑦)) ∧ 𝑏 ∈ 𝐴) → (abs‘(𝑥 − (𝐹‘𝑎))) < 𝑦)
223	222	adantr 480	. . . . . . . . . . . . . . . . . 18 ⊢ (((((((𝜑 ∧ 𝑥 ∈ ℂ) ∧ 𝑦 ∈ ℝ+) ∧ 𝑎 ∈ 𝐴) ∧ ((abs‘((𝐹‘𝑎) − 𝑥)) < 𝑦 ∧ (abs‘((𝐹‘𝑎) − 𝐿)) < 𝑦)) ∧ 𝑏 ∈ 𝐴) ∧ ((abs‘((𝐹‘𝑏) − 𝑥)) < 𝑦 ∧ (abs‘((𝐹‘𝑏) − 𝑅)) < 𝑦)) → (abs‘(𝑥 − (𝐹‘𝑎))) < 𝑦)
224		simplrr 778	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((((𝜑 ∧ 𝑥 ∈ ℂ) ∧ 𝑦 ∈ ℝ+) ∧ 𝑎 ∈ 𝐴) ∧ ((abs‘((𝐹‘𝑎) − 𝑥)) < 𝑦 ∧ (abs‘((𝐹‘𝑎) − 𝐿)) < 𝑦)) ∧ 𝑏 ∈ 𝐴) → (abs‘((𝐹‘𝑎) − 𝐿)) < 𝑦)
225	224	adantr 480	. . . . . . . . . . . . . . . . . 18 ⊢ (((((((𝜑 ∧ 𝑥 ∈ ℂ) ∧ 𝑦 ∈ ℝ+) ∧ 𝑎 ∈ 𝐴) ∧ ((abs‘((𝐹‘𝑎) − 𝑥)) < 𝑦 ∧ (abs‘((𝐹‘𝑎) − 𝐿)) < 𝑦)) ∧ 𝑏 ∈ 𝐴) ∧ ((abs‘((𝐹‘𝑏) − 𝑥)) < 𝑦 ∧ (abs‘((𝐹‘𝑏) − 𝑅)) < 𝑦)) → (abs‘((𝐹‘𝑎) − 𝐿)) < 𝑦)
226	194, 197, 203, 206, 210, 215, 216, 223, 225	lt4addmuld 45256	. . . . . . . . . . . . . . . . 17 ⊢ (((((((𝜑 ∧ 𝑥 ∈ ℂ) ∧ 𝑦 ∈ ℝ+) ∧ 𝑎 ∈ 𝐴) ∧ ((abs‘((𝐹‘𝑎) − 𝑥)) < 𝑦 ∧ (abs‘((𝐹‘𝑎) − 𝐿)) < 𝑦)) ∧ 𝑏 ∈ 𝐴) ∧ ((abs‘((𝐹‘𝑏) − 𝑥)) < 𝑦 ∧ (abs‘((𝐹‘𝑏) − 𝑅)) < 𝑦)) → ((((abs‘(𝑅 − (𝐹‘𝑏))) + (abs‘((𝐹‘𝑏) − 𝑥))) + (abs‘(𝑥 − (𝐹‘𝑎)))) + (abs‘((𝐹‘𝑎) − 𝐿))) < (4 · 𝑦))
227	188, 207, 211, 212, 226	lelttrd 11416	. . . . . . . . . . . . . . . 16 ⊢ (((((((𝜑 ∧ 𝑥 ∈ ℂ) ∧ 𝑦 ∈ ℝ+) ∧ 𝑎 ∈ 𝐴) ∧ ((abs‘((𝐹‘𝑎) − 𝑥)) < 𝑦 ∧ (abs‘((𝐹‘𝑎) − 𝐿)) < 𝑦)) ∧ 𝑏 ∈ 𝐴) ∧ ((abs‘((𝐹‘𝑏) − 𝑥)) < 𝑦 ∧ (abs‘((𝐹‘𝑏) − 𝑅)) < 𝑦)) → (abs‘(𝑅 − 𝐿)) < (4 · 𝑦))
228	227	ex 412	. . . . . . . . . . . . . . 15 ⊢ ((((((𝜑 ∧ 𝑥 ∈ ℂ) ∧ 𝑦 ∈ ℝ+) ∧ 𝑎 ∈ 𝐴) ∧ ((abs‘((𝐹‘𝑎) − 𝑥)) < 𝑦 ∧ (abs‘((𝐹‘𝑎) − 𝐿)) < 𝑦)) ∧ 𝑏 ∈ 𝐴) → (((abs‘((𝐹‘𝑏) − 𝑥)) < 𝑦 ∧ (abs‘((𝐹‘𝑏) − 𝑅)) < 𝑦) → (abs‘(𝑅 − 𝐿)) < (4 · 𝑦)))
229	228	adantl3r 750	. . . . . . . . . . . . . 14 ⊢ (((((((𝜑 ∧ 𝑥 ∈ ℂ) ∧ 𝑦 ∈ ℝ+) ∧ ∃𝑧 ∈ ℝ+ ∀𝑤 ∈ 𝐴 ((𝑤 ≠ 𝐵 ∧ (abs‘(𝑤 − 𝐵)) < 𝑧) → (abs‘((𝐹‘𝑤) − 𝑥)) < 𝑦)) ∧ 𝑎 ∈ 𝐴) ∧ ((abs‘((𝐹‘𝑎) − 𝑥)) < 𝑦 ∧ (abs‘((𝐹‘𝑎) − 𝐿)) < 𝑦)) ∧ 𝑏 ∈ 𝐴) → (((abs‘((𝐹‘𝑏) − 𝑥)) < 𝑦 ∧ (abs‘((𝐹‘𝑏) − 𝑅)) < 𝑦) → (abs‘(𝑅 − 𝐿)) < (4 · 𝑦)))
230	229	reximdva 3165	. . . . . . . . . . . . 13 ⊢ ((((((𝜑 ∧ 𝑥 ∈ ℂ) ∧ 𝑦 ∈ ℝ+) ∧ ∃𝑧 ∈ ℝ+ ∀𝑤 ∈ 𝐴 ((𝑤 ≠ 𝐵 ∧ (abs‘(𝑤 − 𝐵)) < 𝑧) → (abs‘((𝐹‘𝑤) − 𝑥)) < 𝑦)) ∧ 𝑎 ∈ 𝐴) ∧ ((abs‘((𝐹‘𝑎) − 𝑥)) < 𝑦 ∧ (abs‘((𝐹‘𝑎) − 𝐿)) < 𝑦)) → (∃𝑏 ∈ 𝐴 ((abs‘((𝐹‘𝑏) − 𝑥)) < 𝑦 ∧ (abs‘((𝐹‘𝑏) − 𝑅)) < 𝑦) → ∃𝑏 ∈ 𝐴 (abs‘(𝑅 − 𝐿)) < (4 · 𝑦)))
231	184, 230	mpd 15	. . . . . . . . . . . 12 ⊢ ((((((𝜑 ∧ 𝑥 ∈ ℂ) ∧ 𝑦 ∈ ℝ+) ∧ ∃𝑧 ∈ ℝ+ ∀𝑤 ∈ 𝐴 ((𝑤 ≠ 𝐵 ∧ (abs‘(𝑤 − 𝐵)) < 𝑧) → (abs‘((𝐹‘𝑤) − 𝑥)) < 𝑦)) ∧ 𝑎 ∈ 𝐴) ∧ ((abs‘((𝐹‘𝑎) − 𝑥)) < 𝑦 ∧ (abs‘((𝐹‘𝑎) − 𝐿)) < 𝑦)) → ∃𝑏 ∈ 𝐴 (abs‘(𝑅 − 𝐿)) < (4 · 𝑦))
232		fresin 6777	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝐹:𝐴⟶ℂ → (𝐹 ↾ (-∞(,)𝐵)):(𝐴 ∩ (-∞(,)𝐵))⟶ℂ)
233	36, 232	syl 17	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝜑 → (𝐹 ↾ (-∞(,)𝐵)):(𝐴 ∩ (-∞(,)𝐵))⟶ℂ)
234		ioosscn 13445	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (-∞(,)𝐵) ⊆ ℂ
235	46, 234	sstri 4004	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝐴 ∩ (-∞(,)𝐵)) ⊆ ℂ
236	235	a1i 11	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝜑 → (𝐴 ∩ (-∞(,)𝐵)) ⊆ ℂ)
237	233, 236, 56	ellimc3 25928	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝜑 → (𝐿 ∈ ((𝐹 ↾ (-∞(,)𝐵)) limℂ 𝐵) ↔ (𝐿 ∈ ℂ ∧ ∀𝑦 ∈ ℝ+ ∃𝑣 ∈ ℝ+ ∀𝑤 ∈ (𝐴 ∩ (-∞(,)𝐵))((𝑤 ≠ 𝐵 ∧ (abs‘(𝑤 − 𝐵)) < 𝑣) → (abs‘(((𝐹 ↾ (-∞(,)𝐵))‘𝑤) − 𝐿)) < 𝑦))))
238	6, 237	mpbid 232	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → (𝐿 ∈ ℂ ∧ ∀𝑦 ∈ ℝ+ ∃𝑣 ∈ ℝ+ ∀𝑤 ∈ (𝐴 ∩ (-∞(,)𝐵))((𝑤 ≠ 𝐵 ∧ (abs‘(𝑤 − 𝐵)) < 𝑣) → (abs‘(((𝐹 ↾ (-∞(,)𝐵))‘𝑤) − 𝐿)) < 𝑦)))
239	238	simprd 495	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → ∀𝑦 ∈ ℝ+ ∃𝑣 ∈ ℝ+ ∀𝑤 ∈ (𝐴 ∩ (-∞(,)𝐵))((𝑤 ≠ 𝐵 ∧ (abs‘(𝑤 − 𝐵)) < 𝑣) → (abs‘(((𝐹 ↾ (-∞(,)𝐵))‘𝑤) − 𝐿)) < 𝑦))
240	239	r19.21bi 3248	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑦 ∈ ℝ+) → ∃𝑣 ∈ ℝ+ ∀𝑤 ∈ (𝐴 ∩ (-∞(,)𝐵))((𝑤 ≠ 𝐵 ∧ (abs‘(𝑤 − 𝐵)) < 𝑣) → (abs‘(((𝐹 ↾ (-∞(,)𝐵))‘𝑤) − 𝐿)) < 𝑦))
241	240	3ad2ant1 1132	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑦 ∈ ℝ+) ∧ 𝑧 ∈ ℝ+ ∧ ∀𝑤 ∈ 𝐴 ((𝑤 ≠ 𝐵 ∧ (abs‘(𝑤 − 𝐵)) < 𝑧) → (abs‘((𝐹‘𝑤) − 𝑥)) < 𝑦)) → ∃𝑣 ∈ ℝ+ ∀𝑤 ∈ (𝐴 ∩ (-∞(,)𝐵))((𝑤 ≠ 𝐵 ∧ (abs‘(𝑤 − 𝐵)) < 𝑣) → (abs‘(((𝐹 ↾ (-∞(,)𝐵))‘𝑤) − 𝐿)) < 𝑦))
242		simp11l 1283	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((𝜑 ∧ 𝑦 ∈ ℝ+) ∧ 𝑧 ∈ ℝ+ ∧ ∀𝑤 ∈ 𝐴 ((𝑤 ≠ 𝐵 ∧ (abs‘(𝑤 − 𝐵)) < 𝑧) → (abs‘((𝐹‘𝑤) − 𝑥)) < 𝑦)) ∧ 𝑣 ∈ ℝ+ ∧ ∀𝑤 ∈ (𝐴 ∩ (-∞(,)𝐵))((𝑤 ≠ 𝐵 ∧ (abs‘(𝑤 − 𝐵)) < 𝑣) → (abs‘(((𝐹 ↾ (-∞(,)𝐵))‘𝑤) − 𝐿)) < 𝑦)) → 𝜑)
243		simp12 1203	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((𝜑 ∧ 𝑦 ∈ ℝ+) ∧ 𝑧 ∈ ℝ+ ∧ ∀𝑤 ∈ 𝐴 ((𝑤 ≠ 𝐵 ∧ (abs‘(𝑤 − 𝐵)) < 𝑧) → (abs‘((𝐹‘𝑤) − 𝑥)) < 𝑦)) ∧ 𝑣 ∈ ℝ+ ∧ ∀𝑤 ∈ (𝐴 ∩ (-∞(,)𝐵))((𝑤 ≠ 𝐵 ∧ (abs‘(𝑤 − 𝐵)) < 𝑣) → (abs‘(((𝐹 ↾ (-∞(,)𝐵))‘𝑤) − 𝐿)) < 𝑦)) → 𝑧 ∈ ℝ+)
244		simp2 1136	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((𝜑 ∧ 𝑦 ∈ ℝ+) ∧ 𝑧 ∈ ℝ+ ∧ ∀𝑤 ∈ 𝐴 ((𝑤 ≠ 𝐵 ∧ (abs‘(𝑤 − 𝐵)) < 𝑧) → (abs‘((𝐹‘𝑤) − 𝑥)) < 𝑦)) ∧ 𝑣 ∈ ℝ+ ∧ ∀𝑤 ∈ (𝐴 ∩ (-∞(,)𝐵))((𝑤 ≠ 𝐵 ∧ (abs‘(𝑤 − 𝐵)) < 𝑣) → (abs‘(((𝐹 ↾ (-∞(,)𝐵))‘𝑤) − 𝐿)) < 𝑦)) → 𝑣 ∈ ℝ+)
245		breq2 5151	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑢 = if(𝑧 ≤ 𝑣, 𝑧, 𝑣) → ((abs‘(𝑎 − 𝐵)) < 𝑢 ↔ (abs‘(𝑎 − 𝐵)) < if(𝑧 ≤ 𝑣, 𝑧, 𝑣)))
246	245	rexbidv 3176	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑢 = if(𝑧 ≤ 𝑣, 𝑧, 𝑣) → (∃𝑎 ∈ ((𝐴 ∩ (-∞(,)𝐵)) ∖ {𝐵})(abs‘(𝑎 − 𝐵)) < 𝑢 ↔ ∃𝑎 ∈ ((𝐴 ∩ (-∞(,)𝐵)) ∖ {𝐵})(abs‘(𝑎 − 𝐵)) < if(𝑧 ≤ 𝑣, 𝑧, 𝑣)))
247		inss1 4244	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (((limPt‘𝐾)‘(𝐴 ∩ (-∞(,)𝐵))) ∩ ℝ) ⊆ ((limPt‘𝐾)‘(𝐴 ∩ (-∞(,)𝐵)))
248	247	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝜑 → (((limPt‘𝐾)‘(𝐴 ∩ (-∞(,)𝐵))) ∩ ℝ) ⊆ ((limPt‘𝐾)‘(𝐴 ∩ (-∞(,)𝐵))))
249	48	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (𝜑 → (𝐴 ∩ (-∞(,)𝐵)) ⊆ ℝ)
250	79, 81	restlp 23206	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ((𝐾 ∈ Top ∧ ℝ ⊆ ℂ ∧ (𝐴 ∩ (-∞(,)𝐵)) ⊆ ℝ) → ((limPt‘𝐽)‘(𝐴 ∩ (-∞(,)𝐵))) = (((limPt‘𝐾)‘(𝐴 ∩ (-∞(,)𝐵))) ∩ ℝ))
251	71, 73, 249, 250	syl3anc 1370	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝜑 → ((limPt‘𝐽)‘(𝐴 ∩ (-∞(,)𝐵))) = (((limPt‘𝐾)‘(𝐴 ∩ (-∞(,)𝐵))) ∩ ℝ))
252	85	fveq1i 6907	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ((limPt‘(TopOpen‘ℂfld))‘(𝐴 ∩ (-∞(,)𝐵))) = ((limPt‘𝐾)‘(𝐴 ∩ (-∞(,)𝐵)))
253	252	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝜑 → ((limPt‘(TopOpen‘ℂfld))‘(𝐴 ∩ (-∞(,)𝐵))) = ((limPt‘𝐾)‘(𝐴 ∩ (-∞(,)𝐵))))
254	248, 251, 253	3sstr4d 4042	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝜑 → ((limPt‘𝐽)‘(𝐴 ∩ (-∞(,)𝐵))) ⊆ ((limPt‘(TopOpen‘ℂfld))‘(𝐴 ∩ (-∞(,)𝐵))))
255	254, 54	sseldd 3995	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝜑 → 𝐵 ∈ ((limPt‘(TopOpen‘ℂfld))‘(𝐴 ∩ (-∞(,)𝐵))))
256	236, 56	islpcn 45594	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝜑 → (𝐵 ∈ ((limPt‘(TopOpen‘ℂfld))‘(𝐴 ∩ (-∞(,)𝐵))) ↔ ∀𝑢 ∈ ℝ+ ∃𝑎 ∈ ((𝐴 ∩ (-∞(,)𝐵)) ∖ {𝐵})(abs‘(𝑎 − 𝐵)) < 𝑢))
257	255, 256	mpbid 232	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝜑 → ∀𝑢 ∈ ℝ+ ∃𝑎 ∈ ((𝐴 ∩ (-∞(,)𝐵)) ∖ {𝐵})(abs‘(𝑎 − 𝐵)) < 𝑢)
258	257	3ad2ant1 1132	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝜑 ∧ 𝑧 ∈ ℝ+ ∧ 𝑣 ∈ ℝ+) → ∀𝑢 ∈ ℝ+ ∃𝑎 ∈ ((𝐴 ∩ (-∞(,)𝐵)) ∖ {𝐵})(abs‘(𝑎 − 𝐵)) < 𝑢)
259	246, 258, 95	rspcdva 3622	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝜑 ∧ 𝑧 ∈ ℝ+ ∧ 𝑣 ∈ ℝ+) → ∃𝑎 ∈ ((𝐴 ∩ (-∞(,)𝐵)) ∖ {𝐵})(abs‘(𝑎 − 𝐵)) < if(𝑧 ≤ 𝑣, 𝑧, 𝑣))
260		eldifi 4140	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑎 ∈ ((𝐴 ∩ (-∞(,)𝐵)) ∖ {𝐵}) → 𝑎 ∈ (𝐴 ∩ (-∞(,)𝐵)))
261	48, 260	sselid 3992	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑎 ∈ ((𝐴 ∩ (-∞(,)𝐵)) ∖ {𝐵}) → 𝑎 ∈ ℝ)
262	73	sselda 3994	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ ((𝜑 ∧ 𝑎 ∈ ℝ) → 𝑎 ∈ ℂ)
263	56	adantr 480	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ ((𝜑 ∧ 𝑎 ∈ ℝ) → 𝐵 ∈ ℂ)
264	262, 263	subcld 11617	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ ((𝜑 ∧ 𝑎 ∈ ℝ) → (𝑎 − 𝐵) ∈ ℂ)
265	264	abscld 15471	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ ((𝜑 ∧ 𝑎 ∈ ℝ) → (abs‘(𝑎 − 𝐵)) ∈ ℝ)
266	265	3ad2antl1 1184	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (((𝜑 ∧ 𝑧 ∈ ℝ+ ∧ 𝑣 ∈ ℝ+) ∧ 𝑎 ∈ ℝ) → (abs‘(𝑎 − 𝐵)) ∈ ℝ)
267	266	adantr 480	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((((𝜑 ∧ 𝑧 ∈ ℝ+ ∧ 𝑣 ∈ ℝ+) ∧ 𝑎 ∈ ℝ) ∧ (abs‘(𝑎 − 𝐵)) < if(𝑧 ≤ 𝑣, 𝑧, 𝑣)) → (abs‘(𝑎 − 𝐵)) ∈ ℝ)
268	105	ad2antrr 726	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((((𝜑 ∧ 𝑧 ∈ ℝ+ ∧ 𝑣 ∈ ℝ+) ∧ 𝑎 ∈ ℝ) ∧ (abs‘(𝑎 − 𝐵)) < if(𝑧 ≤ 𝑣, 𝑧, 𝑣)) → if(𝑧 ≤ 𝑣, 𝑧, 𝑣) ∈ ℝ)
269	108	ad2antrr 726	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((((𝜑 ∧ 𝑧 ∈ ℝ+ ∧ 𝑣 ∈ ℝ+) ∧ 𝑎 ∈ ℝ) ∧ (abs‘(𝑎 − 𝐵)) < if(𝑧 ≤ 𝑣, 𝑧, 𝑣)) → 𝑧 ∈ ℝ)
270		simpr 484	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((((𝜑 ∧ 𝑧 ∈ ℝ+ ∧ 𝑣 ∈ ℝ+) ∧ 𝑎 ∈ ℝ) ∧ (abs‘(𝑎 − 𝐵)) < if(𝑧 ≤ 𝑣, 𝑧, 𝑣)) → (abs‘(𝑎 − 𝐵)) < if(𝑧 ≤ 𝑣, 𝑧, 𝑣))
271	114	ad2antrr 726	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((((𝜑 ∧ 𝑧 ∈ ℝ+ ∧ 𝑣 ∈ ℝ+) ∧ 𝑎 ∈ ℝ) ∧ (abs‘(𝑎 − 𝐵)) < if(𝑧 ≤ 𝑣, 𝑧, 𝑣)) → if(𝑧 ≤ 𝑣, 𝑧, 𝑣) ≤ 𝑧)
272	267, 268, 269, 270, 271	ltletrd 11418	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((((𝜑 ∧ 𝑧 ∈ ℝ+ ∧ 𝑣 ∈ ℝ+) ∧ 𝑎 ∈ ℝ) ∧ (abs‘(𝑎 − 𝐵)) < if(𝑧 ≤ 𝑣, 𝑧, 𝑣)) → (abs‘(𝑎 − 𝐵)) < 𝑧)
273	117	ad2antrr 726	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((((𝜑 ∧ 𝑧 ∈ ℝ+ ∧ 𝑣 ∈ ℝ+) ∧ 𝑎 ∈ ℝ) ∧ (abs‘(𝑎 − 𝐵)) < if(𝑧 ≤ 𝑣, 𝑧, 𝑣)) → 𝑣 ∈ ℝ)
274		min2 13228	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ ((𝑧 ∈ ℝ ∧ 𝑣 ∈ ℝ) → if(𝑧 ≤ 𝑣, 𝑧, 𝑣) ≤ 𝑣)
275	107, 111, 274	syl2an 596	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ ((𝑧 ∈ ℝ+ ∧ 𝑣 ∈ ℝ+) → if(𝑧 ≤ 𝑣, 𝑧, 𝑣) ≤ 𝑣)
276	275	3adant1 1129	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ((𝜑 ∧ 𝑧 ∈ ℝ+ ∧ 𝑣 ∈ ℝ+) → if(𝑧 ≤ 𝑣, 𝑧, 𝑣) ≤ 𝑣)
277	276	ad2antrr 726	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((((𝜑 ∧ 𝑧 ∈ ℝ+ ∧ 𝑣 ∈ ℝ+) ∧ 𝑎 ∈ ℝ) ∧ (abs‘(𝑎 − 𝐵)) < if(𝑧 ≤ 𝑣, 𝑧, 𝑣)) → if(𝑧 ≤ 𝑣, 𝑧, 𝑣) ≤ 𝑣)
278	267, 268, 273, 270, 277	ltletrd 11418	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((((𝜑 ∧ 𝑧 ∈ ℝ+ ∧ 𝑣 ∈ ℝ+) ∧ 𝑎 ∈ ℝ) ∧ (abs‘(𝑎 − 𝐵)) < if(𝑧 ≤ 𝑣, 𝑧, 𝑣)) → (abs‘(𝑎 − 𝐵)) < 𝑣)
279	272, 278	jca 511	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((((𝜑 ∧ 𝑧 ∈ ℝ+ ∧ 𝑣 ∈ ℝ+) ∧ 𝑎 ∈ ℝ) ∧ (abs‘(𝑎 − 𝐵)) < if(𝑧 ≤ 𝑣, 𝑧, 𝑣)) → ((abs‘(𝑎 − 𝐵)) < 𝑧 ∧ (abs‘(𝑎 − 𝐵)) < 𝑣))
280	279	ex 412	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((𝜑 ∧ 𝑧 ∈ ℝ+ ∧ 𝑣 ∈ ℝ+) ∧ 𝑎 ∈ ℝ) → ((abs‘(𝑎 − 𝐵)) < if(𝑧 ≤ 𝑣, 𝑧, 𝑣) → ((abs‘(𝑎 − 𝐵)) < 𝑧 ∧ (abs‘(𝑎 − 𝐵)) < 𝑣)))
281	261, 280	sylan2 593	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((𝜑 ∧ 𝑧 ∈ ℝ+ ∧ 𝑣 ∈ ℝ+) ∧ 𝑎 ∈ ((𝐴 ∩ (-∞(,)𝐵)) ∖ {𝐵})) → ((abs‘(𝑎 − 𝐵)) < if(𝑧 ≤ 𝑣, 𝑧, 𝑣) → ((abs‘(𝑎 − 𝐵)) < 𝑧 ∧ (abs‘(𝑎 − 𝐵)) < 𝑣)))
282	281	reximdva 3165	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝜑 ∧ 𝑧 ∈ ℝ+ ∧ 𝑣 ∈ ℝ+) → (∃𝑎 ∈ ((𝐴 ∩ (-∞(,)𝐵)) ∖ {𝐵})(abs‘(𝑎 − 𝐵)) < if(𝑧 ≤ 𝑣, 𝑧, 𝑣) → ∃𝑎 ∈ ((𝐴 ∩ (-∞(,)𝐵)) ∖ {𝐵})((abs‘(𝑎 − 𝐵)) < 𝑧 ∧ (abs‘(𝑎 − 𝐵)) < 𝑣)))
283	259, 282	mpd 15	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝜑 ∧ 𝑧 ∈ ℝ+ ∧ 𝑣 ∈ ℝ+) → ∃𝑎 ∈ ((𝐴 ∩ (-∞(,)𝐵)) ∖ {𝐵})((abs‘(𝑎 − 𝐵)) < 𝑧 ∧ (abs‘(𝑎 − 𝐵)) < 𝑣))
284	242, 243, 244, 283	syl3anc 1370	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝜑 ∧ 𝑦 ∈ ℝ+) ∧ 𝑧 ∈ ℝ+ ∧ ∀𝑤 ∈ 𝐴 ((𝑤 ≠ 𝐵 ∧ (abs‘(𝑤 − 𝐵)) < 𝑧) → (abs‘((𝐹‘𝑤) − 𝑥)) < 𝑦)) ∧ 𝑣 ∈ ℝ+ ∧ ∀𝑤 ∈ (𝐴 ∩ (-∞(,)𝐵))((𝑤 ≠ 𝐵 ∧ (abs‘(𝑤 − 𝐵)) < 𝑣) → (abs‘(((𝐹 ↾ (-∞(,)𝐵))‘𝑤) − 𝐿)) < 𝑦)) → ∃𝑎 ∈ ((𝐴 ∩ (-∞(,)𝐵)) ∖ {𝐵})((abs‘(𝑎 − 𝐵)) < 𝑧 ∧ (abs‘(𝑎 − 𝐵)) < 𝑣))
285		nfv 1911	. . . . . . . . . . . . . . . . . . . . 21 ⊢ Ⅎ𝑎(((𝜑 ∧ 𝑦 ∈ ℝ+) ∧ 𝑧 ∈ ℝ+ ∧ ∀𝑤 ∈ 𝐴 ((𝑤 ≠ 𝐵 ∧ (abs‘(𝑤 − 𝐵)) < 𝑧) → (abs‘((𝐹‘𝑤) − 𝑥)) < 𝑦)) ∧ 𝑣 ∈ ℝ+ ∧ ∀𝑤 ∈ (𝐴 ∩ (-∞(,)𝐵))((𝑤 ≠ 𝐵 ∧ (abs‘(𝑤 − 𝐵)) < 𝑣) → (abs‘(((𝐹 ↾ (-∞(,)𝐵))‘𝑤) − 𝐿)) < 𝑦))
286		nfre1 3282	. . . . . . . . . . . . . . . . . . . . 21 ⊢ Ⅎ𝑎∃𝑎 ∈ 𝐴 ((abs‘((𝐹‘𝑎) − 𝑥)) < 𝑦 ∧ (abs‘((𝐹‘𝑎) − 𝐿)) < 𝑦)
287	260	elin1d 4213	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑎 ∈ ((𝐴 ∩ (-∞(,)𝐵)) ∖ {𝐵}) → 𝑎 ∈ 𝐴)
288	287	3ad2ant2 1133	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((((𝜑 ∧ 𝑦 ∈ ℝ+) ∧ 𝑧 ∈ ℝ+ ∧ ∀𝑤 ∈ 𝐴 ((𝑤 ≠ 𝐵 ∧ (abs‘(𝑤 − 𝐵)) < 𝑧) → (abs‘((𝐹‘𝑤) − 𝑥)) < 𝑦)) ∧ 𝑣 ∈ ℝ+ ∧ ∀𝑤 ∈ (𝐴 ∩ (-∞(,)𝐵))((𝑤 ≠ 𝐵 ∧ (abs‘(𝑤 − 𝐵)) < 𝑣) → (abs‘(((𝐹 ↾ (-∞(,)𝐵))‘𝑤) − 𝐿)) < 𝑦)) ∧ 𝑎 ∈ ((𝐴 ∩ (-∞(,)𝐵)) ∖ {𝐵}) ∧ ((abs‘(𝑎 − 𝐵)) < 𝑧 ∧ (abs‘(𝑎 − 𝐵)) < 𝑣)) → 𝑎 ∈ 𝐴)
289		simp113 1303	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((((𝜑 ∧ 𝑦 ∈ ℝ+) ∧ 𝑧 ∈ ℝ+ ∧ ∀𝑤 ∈ 𝐴 ((𝑤 ≠ 𝐵 ∧ (abs‘(𝑤 − 𝐵)) < 𝑧) → (abs‘((𝐹‘𝑤) − 𝑥)) < 𝑦)) ∧ 𝑣 ∈ ℝ+ ∧ ∀𝑤 ∈ (𝐴 ∩ (-∞(,)𝐵))((𝑤 ≠ 𝐵 ∧ (abs‘(𝑤 − 𝐵)) < 𝑣) → (abs‘(((𝐹 ↾ (-∞(,)𝐵))‘𝑤) − 𝐿)) < 𝑦)) ∧ 𝑎 ∈ ((𝐴 ∩ (-∞(,)𝐵)) ∖ {𝐵}) ∧ ((abs‘(𝑎 − 𝐵)) < 𝑧 ∧ (abs‘(𝑎 − 𝐵)) < 𝑣)) → ∀𝑤 ∈ 𝐴 ((𝑤 ≠ 𝐵 ∧ (abs‘(𝑤 − 𝐵)) < 𝑧) → (abs‘((𝐹‘𝑤) − 𝑥)) < 𝑦))
290		eldifsni 4794	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝑎 ∈ ((𝐴 ∩ (-∞(,)𝐵)) ∖ {𝐵}) → 𝑎 ≠ 𝐵)
291	290	adantr 480	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((𝑎 ∈ ((𝐴 ∩ (-∞(,)𝐵)) ∖ {𝐵}) ∧ ((abs‘(𝑎 − 𝐵)) < 𝑧 ∧ (abs‘(𝑎 − 𝐵)) < 𝑣)) → 𝑎 ≠ 𝐵)
292		simprl 771	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((𝑎 ∈ ((𝐴 ∩ (-∞(,)𝐵)) ∖ {𝐵}) ∧ ((abs‘(𝑎 − 𝐵)) < 𝑧 ∧ (abs‘(𝑎 − 𝐵)) < 𝑣)) → (abs‘(𝑎 − 𝐵)) < 𝑧)
293	291, 292	jca 511	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((𝑎 ∈ ((𝐴 ∩ (-∞(,)𝐵)) ∖ {𝐵}) ∧ ((abs‘(𝑎 − 𝐵)) < 𝑧 ∧ (abs‘(𝑎 − 𝐵)) < 𝑣)) → (𝑎 ≠ 𝐵 ∧ (abs‘(𝑎 − 𝐵)) < 𝑧))
294	293	3adant1 1129	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((((𝜑 ∧ 𝑦 ∈ ℝ+) ∧ 𝑧 ∈ ℝ+ ∧ ∀𝑤 ∈ 𝐴 ((𝑤 ≠ 𝐵 ∧ (abs‘(𝑤 − 𝐵)) < 𝑧) → (abs‘((𝐹‘𝑤) − 𝑥)) < 𝑦)) ∧ 𝑣 ∈ ℝ+ ∧ ∀𝑤 ∈ (𝐴 ∩ (-∞(,)𝐵))((𝑤 ≠ 𝐵 ∧ (abs‘(𝑤 − 𝐵)) < 𝑣) → (abs‘(((𝐹 ↾ (-∞(,)𝐵))‘𝑤) − 𝐿)) < 𝑦)) ∧ 𝑎 ∈ ((𝐴 ∩ (-∞(,)𝐵)) ∖ {𝐵}) ∧ ((abs‘(𝑎 − 𝐵)) < 𝑧 ∧ (abs‘(𝑎 − 𝐵)) < 𝑣)) → (𝑎 ≠ 𝐵 ∧ (abs‘(𝑎 − 𝐵)) < 𝑧))
295		neeq1 3000	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (𝑤 = 𝑎 → (𝑤 ≠ 𝐵 ↔ 𝑎 ≠ 𝐵))
296		fvoveq1 7453	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (𝑤 = 𝑎 → (abs‘(𝑤 − 𝐵)) = (abs‘(𝑎 − 𝐵)))
297	296	breq1d 5157	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (𝑤 = 𝑎 → ((abs‘(𝑤 − 𝐵)) < 𝑧 ↔ (abs‘(𝑎 − 𝐵)) < 𝑧))
298	295, 297	anbi12d 632	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝑤 = 𝑎 → ((𝑤 ≠ 𝐵 ∧ (abs‘(𝑤 − 𝐵)) < 𝑧) ↔ (𝑎 ≠ 𝐵 ∧ (abs‘(𝑎 − 𝐵)) < 𝑧)))
299	298	imbrov2fvoveq 7455	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝑤 = 𝑎 → (((𝑤 ≠ 𝐵 ∧ (abs‘(𝑤 − 𝐵)) < 𝑧) → (abs‘((𝐹‘𝑤) − 𝑥)) < 𝑦) ↔ ((𝑎 ≠ 𝐵 ∧ (abs‘(𝑎 − 𝐵)) < 𝑧) → (abs‘((𝐹‘𝑎) − 𝑥)) < 𝑦)))
300	299	rspcva 3619	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((𝑎 ∈ 𝐴 ∧ ∀𝑤 ∈ 𝐴 ((𝑤 ≠ 𝐵 ∧ (abs‘(𝑤 − 𝐵)) < 𝑧) → (abs‘((𝐹‘𝑤) − 𝑥)) < 𝑦)) → ((𝑎 ≠ 𝐵 ∧ (abs‘(𝑎 − 𝐵)) < 𝑧) → (abs‘((𝐹‘𝑎) − 𝑥)) < 𝑦))
301	300	imp 406	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((𝑎 ∈ 𝐴 ∧ ∀𝑤 ∈ 𝐴 ((𝑤 ≠ 𝐵 ∧ (abs‘(𝑤 − 𝐵)) < 𝑧) → (abs‘((𝐹‘𝑤) − 𝑥)) < 𝑦)) ∧ (𝑎 ≠ 𝐵 ∧ (abs‘(𝑎 − 𝐵)) < 𝑧)) → (abs‘((𝐹‘𝑎) − 𝑥)) < 𝑦)
302	288, 289, 294, 301	syl21anc 838	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((((𝜑 ∧ 𝑦 ∈ ℝ+) ∧ 𝑧 ∈ ℝ+ ∧ ∀𝑤 ∈ 𝐴 ((𝑤 ≠ 𝐵 ∧ (abs‘(𝑤 − 𝐵)) < 𝑧) → (abs‘((𝐹‘𝑤) − 𝑥)) < 𝑦)) ∧ 𝑣 ∈ ℝ+ ∧ ∀𝑤 ∈ (𝐴 ∩ (-∞(,)𝐵))((𝑤 ≠ 𝐵 ∧ (abs‘(𝑤 − 𝐵)) < 𝑣) → (abs‘(((𝐹 ↾ (-∞(,)𝐵))‘𝑤) − 𝐿)) < 𝑦)) ∧ 𝑎 ∈ ((𝐴 ∩ (-∞(,)𝐵)) ∖ {𝐵}) ∧ ((abs‘(𝑎 − 𝐵)) < 𝑧 ∧ (abs‘(𝑎 − 𝐵)) < 𝑣)) → (abs‘((𝐹‘𝑎) − 𝑥)) < 𝑦)
303	260	3ad2ant2 1133	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((((𝜑 ∧ 𝑦 ∈ ℝ+) ∧ 𝑧 ∈ ℝ+ ∧ ∀𝑤 ∈ 𝐴 ((𝑤 ≠ 𝐵 ∧ (abs‘(𝑤 − 𝐵)) < 𝑧) → (abs‘((𝐹‘𝑤) − 𝑥)) < 𝑦)) ∧ 𝑣 ∈ ℝ+ ∧ ∀𝑤 ∈ (𝐴 ∩ (-∞(,)𝐵))((𝑤 ≠ 𝐵 ∧ (abs‘(𝑤 − 𝐵)) < 𝑣) → (abs‘(((𝐹 ↾ (-∞(,)𝐵))‘𝑤) − 𝐿)) < 𝑦)) ∧ 𝑎 ∈ ((𝐴 ∩ (-∞(,)𝐵)) ∖ {𝐵}) ∧ ((abs‘(𝑎 − 𝐵)) < 𝑧 ∧ (abs‘(𝑎 − 𝐵)) < 𝑣)) → 𝑎 ∈ (𝐴 ∩ (-∞(,)𝐵)))
304	242	3ad2ant1 1132	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((((𝜑 ∧ 𝑦 ∈ ℝ+) ∧ 𝑧 ∈ ℝ+ ∧ ∀𝑤 ∈ 𝐴 ((𝑤 ≠ 𝐵 ∧ (abs‘(𝑤 − 𝐵)) < 𝑧) → (abs‘((𝐹‘𝑤) − 𝑥)) < 𝑦)) ∧ 𝑣 ∈ ℝ+ ∧ ∀𝑤 ∈ (𝐴 ∩ (-∞(,)𝐵))((𝑤 ≠ 𝐵 ∧ (abs‘(𝑤 − 𝐵)) < 𝑣) → (abs‘(((𝐹 ↾ (-∞(,)𝐵))‘𝑤) − 𝐿)) < 𝑦)) ∧ 𝑎 ∈ ((𝐴 ∩ (-∞(,)𝐵)) ∖ {𝐵}) ∧ ((abs‘(𝑎 − 𝐵)) < 𝑧 ∧ (abs‘(𝑎 − 𝐵)) < 𝑣)) → 𝜑)
305		simp13 1204	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((((𝜑 ∧ 𝑦 ∈ ℝ+) ∧ 𝑧 ∈ ℝ+ ∧ ∀𝑤 ∈ 𝐴 ((𝑤 ≠ 𝐵 ∧ (abs‘(𝑤 − 𝐵)) < 𝑧) → (abs‘((𝐹‘𝑤) − 𝑥)) < 𝑦)) ∧ 𝑣 ∈ ℝ+ ∧ ∀𝑤 ∈ (𝐴 ∩ (-∞(,)𝐵))((𝑤 ≠ 𝐵 ∧ (abs‘(𝑤 − 𝐵)) < 𝑣) → (abs‘(((𝐹 ↾ (-∞(,)𝐵))‘𝑤) − 𝐿)) < 𝑦)) ∧ 𝑎 ∈ ((𝐴 ∩ (-∞(,)𝐵)) ∖ {𝐵}) ∧ ((abs‘(𝑎 − 𝐵)) < 𝑧 ∧ (abs‘(𝑎 − 𝐵)) < 𝑣)) → ∀𝑤 ∈ (𝐴 ∩ (-∞(,)𝐵))((𝑤 ≠ 𝐵 ∧ (abs‘(𝑤 − 𝐵)) < 𝑣) → (abs‘(((𝐹 ↾ (-∞(,)𝐵))‘𝑤) − 𝐿)) < 𝑦))
306		nfra1 3281	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ Ⅎ𝑤∀𝑤 ∈ (𝐴 ∩ (-∞(,)𝐵))((𝑤 ≠ 𝐵 ∧ (abs‘(𝑤 − 𝐵)) < 𝑣) → (abs‘(((𝐹 ↾ (-∞(,)𝐵))‘𝑤) − 𝐿)) < 𝑦)
307	148, 306	nfan 1896	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ Ⅎ𝑤(𝜑 ∧ ∀𝑤 ∈ (𝐴 ∩ (-∞(,)𝐵))((𝑤 ≠ 𝐵 ∧ (abs‘(𝑤 − 𝐵)) < 𝑣) → (abs‘(((𝐹 ↾ (-∞(,)𝐵))‘𝑤) − 𝐿)) < 𝑦))
308		elinel2 4211	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ (𝑤 ∈ (𝐴 ∩ (-∞(,)𝐵)) → 𝑤 ∈ (-∞(,)𝐵))
309	308	fvresd 6926	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ (𝑤 ∈ (𝐴 ∩ (-∞(,)𝐵)) → ((𝐹 ↾ (-∞(,)𝐵))‘𝑤) = (𝐹‘𝑤))
310	309	eqcomd 2740	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ (𝑤 ∈ (𝐴 ∩ (-∞(,)𝐵)) → (𝐹‘𝑤) = ((𝐹 ↾ (-∞(,)𝐵))‘𝑤))
311	310	fvoveq1d 7452	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (𝑤 ∈ (𝐴 ∩ (-∞(,)𝐵)) → (abs‘((𝐹‘𝑤) − 𝐿)) = (abs‘(((𝐹 ↾ (-∞(,)𝐵))‘𝑤) − 𝐿)))
312	311	3ad2ant2 1133	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (((𝜑 ∧ ∀𝑤 ∈ (𝐴 ∩ (-∞(,)𝐵))((𝑤 ≠ 𝐵 ∧ (abs‘(𝑤 − 𝐵)) < 𝑣) → (abs‘(((𝐹 ↾ (-∞(,)𝐵))‘𝑤) − 𝐿)) < 𝑦)) ∧ 𝑤 ∈ (𝐴 ∩ (-∞(,)𝐵)) ∧ (𝑤 ≠ 𝐵 ∧ (abs‘(𝑤 − 𝐵)) < 𝑣)) → (abs‘((𝐹‘𝑤) − 𝐿)) = (abs‘(((𝐹 ↾ (-∞(,)𝐵))‘𝑤) − 𝐿)))
313		rspa 3245	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ ((∀𝑤 ∈ (𝐴 ∩ (-∞(,)𝐵))((𝑤 ≠ 𝐵 ∧ (abs‘(𝑤 − 𝐵)) < 𝑣) → (abs‘(((𝐹 ↾ (-∞(,)𝐵))‘𝑤) − 𝐿)) < 𝑦) ∧ 𝑤 ∈ (𝐴 ∩ (-∞(,)𝐵))) → ((𝑤 ≠ 𝐵 ∧ (abs‘(𝑤 − 𝐵)) < 𝑣) → (abs‘(((𝐹 ↾ (-∞(,)𝐵))‘𝑤) − 𝐿)) < 𝑦))
314	313	3impia 1116	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ ((∀𝑤 ∈ (𝐴 ∩ (-∞(,)𝐵))((𝑤 ≠ 𝐵 ∧ (abs‘(𝑤 − 𝐵)) < 𝑣) → (abs‘(((𝐹 ↾ (-∞(,)𝐵))‘𝑤) − 𝐿)) < 𝑦) ∧ 𝑤 ∈ (𝐴 ∩ (-∞(,)𝐵)) ∧ (𝑤 ≠ 𝐵 ∧ (abs‘(𝑤 − 𝐵)) < 𝑣)) → (abs‘(((𝐹 ↾ (-∞(,)𝐵))‘𝑤) − 𝐿)) < 𝑦)
315	314	3adant1l 1175	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (((𝜑 ∧ ∀𝑤 ∈ (𝐴 ∩ (-∞(,)𝐵))((𝑤 ≠ 𝐵 ∧ (abs‘(𝑤 − 𝐵)) < 𝑣) → (abs‘(((𝐹 ↾ (-∞(,)𝐵))‘𝑤) − 𝐿)) < 𝑦)) ∧ 𝑤 ∈ (𝐴 ∩ (-∞(,)𝐵)) ∧ (𝑤 ≠ 𝐵 ∧ (abs‘(𝑤 − 𝐵)) < 𝑣)) → (abs‘(((𝐹 ↾ (-∞(,)𝐵))‘𝑤) − 𝐿)) < 𝑦)
316	312, 315	eqbrtrd 5169	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (((𝜑 ∧ ∀𝑤 ∈ (𝐴 ∩ (-∞(,)𝐵))((𝑤 ≠ 𝐵 ∧ (abs‘(𝑤 − 𝐵)) < 𝑣) → (abs‘(((𝐹 ↾ (-∞(,)𝐵))‘𝑤) − 𝐿)) < 𝑦)) ∧ 𝑤 ∈ (𝐴 ∩ (-∞(,)𝐵)) ∧ (𝑤 ≠ 𝐵 ∧ (abs‘(𝑤 − 𝐵)) < 𝑣)) → (abs‘((𝐹‘𝑤) − 𝐿)) < 𝑦)
317	316	3exp 1118	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((𝜑 ∧ ∀𝑤 ∈ (𝐴 ∩ (-∞(,)𝐵))((𝑤 ≠ 𝐵 ∧ (abs‘(𝑤 − 𝐵)) < 𝑣) → (abs‘(((𝐹 ↾ (-∞(,)𝐵))‘𝑤) − 𝐿)) < 𝑦)) → (𝑤 ∈ (𝐴 ∩ (-∞(,)𝐵)) → ((𝑤 ≠ 𝐵 ∧ (abs‘(𝑤 − 𝐵)) < 𝑣) → (abs‘((𝐹‘𝑤) − 𝐿)) < 𝑦)))
318	307, 317	ralrimi 3254	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((𝜑 ∧ ∀𝑤 ∈ (𝐴 ∩ (-∞(,)𝐵))((𝑤 ≠ 𝐵 ∧ (abs‘(𝑤 − 𝐵)) < 𝑣) → (abs‘(((𝐹 ↾ (-∞(,)𝐵))‘𝑤) − 𝐿)) < 𝑦)) → ∀𝑤 ∈ (𝐴 ∩ (-∞(,)𝐵))((𝑤 ≠ 𝐵 ∧ (abs‘(𝑤 − 𝐵)) < 𝑣) → (abs‘((𝐹‘𝑤) − 𝐿)) < 𝑦))
319	304, 305, 318	syl2anc 584	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((((𝜑 ∧ 𝑦 ∈ ℝ+) ∧ 𝑧 ∈ ℝ+ ∧ ∀𝑤 ∈ 𝐴 ((𝑤 ≠ 𝐵 ∧ (abs‘(𝑤 − 𝐵)) < 𝑧) → (abs‘((𝐹‘𝑤) − 𝑥)) < 𝑦)) ∧ 𝑣 ∈ ℝ+ ∧ ∀𝑤 ∈ (𝐴 ∩ (-∞(,)𝐵))((𝑤 ≠ 𝐵 ∧ (abs‘(𝑤 − 𝐵)) < 𝑣) → (abs‘(((𝐹 ↾ (-∞(,)𝐵))‘𝑤) − 𝐿)) < 𝑦)) ∧ 𝑎 ∈ ((𝐴 ∩ (-∞(,)𝐵)) ∖ {𝐵}) ∧ ((abs‘(𝑎 − 𝐵)) < 𝑧 ∧ (abs‘(𝑎 − 𝐵)) < 𝑣)) → ∀𝑤 ∈ (𝐴 ∩ (-∞(,)𝐵))((𝑤 ≠ 𝐵 ∧ (abs‘(𝑤 − 𝐵)) < 𝑣) → (abs‘((𝐹‘𝑤) − 𝐿)) < 𝑦))
320	290	anim1i 615	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((𝑎 ∈ ((𝐴 ∩ (-∞(,)𝐵)) ∖ {𝐵}) ∧ (abs‘(𝑎 − 𝐵)) < 𝑣) → (𝑎 ≠ 𝐵 ∧ (abs‘(𝑎 − 𝐵)) < 𝑣))
321	320	adantrl 716	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((𝑎 ∈ ((𝐴 ∩ (-∞(,)𝐵)) ∖ {𝐵}) ∧ ((abs‘(𝑎 − 𝐵)) < 𝑧 ∧ (abs‘(𝑎 − 𝐵)) < 𝑣)) → (𝑎 ≠ 𝐵 ∧ (abs‘(𝑎 − 𝐵)) < 𝑣))
322	321	3adant1 1129	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((((𝜑 ∧ 𝑦 ∈ ℝ+) ∧ 𝑧 ∈ ℝ+ ∧ ∀𝑤 ∈ 𝐴 ((𝑤 ≠ 𝐵 ∧ (abs‘(𝑤 − 𝐵)) < 𝑧) → (abs‘((𝐹‘𝑤) − 𝑥)) < 𝑦)) ∧ 𝑣 ∈ ℝ+ ∧ ∀𝑤 ∈ (𝐴 ∩ (-∞(,)𝐵))((𝑤 ≠ 𝐵 ∧ (abs‘(𝑤 − 𝐵)) < 𝑣) → (abs‘(((𝐹 ↾ (-∞(,)𝐵))‘𝑤) − 𝐿)) < 𝑦)) ∧ 𝑎 ∈ ((𝐴 ∩ (-∞(,)𝐵)) ∖ {𝐵}) ∧ ((abs‘(𝑎 − 𝐵)) < 𝑧 ∧ (abs‘(𝑎 − 𝐵)) < 𝑣)) → (𝑎 ≠ 𝐵 ∧ (abs‘(𝑎 − 𝐵)) < 𝑣))
323	296	breq1d 5157	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (𝑤 = 𝑎 → ((abs‘(𝑤 − 𝐵)) < 𝑣 ↔ (abs‘(𝑎 − 𝐵)) < 𝑣))
324	295, 323	anbi12d 632	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝑤 = 𝑎 → ((𝑤 ≠ 𝐵 ∧ (abs‘(𝑤 − 𝐵)) < 𝑣) ↔ (𝑎 ≠ 𝐵 ∧ (abs‘(𝑎 − 𝐵)) < 𝑣)))
325	324	imbrov2fvoveq 7455	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝑤 = 𝑎 → (((𝑤 ≠ 𝐵 ∧ (abs‘(𝑤 − 𝐵)) < 𝑣) → (abs‘((𝐹‘𝑤) − 𝐿)) < 𝑦) ↔ ((𝑎 ≠ 𝐵 ∧ (abs‘(𝑎 − 𝐵)) < 𝑣) → (abs‘((𝐹‘𝑎) − 𝐿)) < 𝑦)))
326	325	rspcva 3619	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((𝑎 ∈ (𝐴 ∩ (-∞(,)𝐵)) ∧ ∀𝑤 ∈ (𝐴 ∩ (-∞(,)𝐵))((𝑤 ≠ 𝐵 ∧ (abs‘(𝑤 − 𝐵)) < 𝑣) → (abs‘((𝐹‘𝑤) − 𝐿)) < 𝑦)) → ((𝑎 ≠ 𝐵 ∧ (abs‘(𝑎 − 𝐵)) < 𝑣) → (abs‘((𝐹‘𝑎) − 𝐿)) < 𝑦))
327	326	imp 406	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((𝑎 ∈ (𝐴 ∩ (-∞(,)𝐵)) ∧ ∀𝑤 ∈ (𝐴 ∩ (-∞(,)𝐵))((𝑤 ≠ 𝐵 ∧ (abs‘(𝑤 − 𝐵)) < 𝑣) → (abs‘((𝐹‘𝑤) − 𝐿)) < 𝑦)) ∧ (𝑎 ≠ 𝐵 ∧ (abs‘(𝑎 − 𝐵)) < 𝑣)) → (abs‘((𝐹‘𝑎) − 𝐿)) < 𝑦)
328	303, 319, 322, 327	syl21anc 838	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((((𝜑 ∧ 𝑦 ∈ ℝ+) ∧ 𝑧 ∈ ℝ+ ∧ ∀𝑤 ∈ 𝐴 ((𝑤 ≠ 𝐵 ∧ (abs‘(𝑤 − 𝐵)) < 𝑧) → (abs‘((𝐹‘𝑤) − 𝑥)) < 𝑦)) ∧ 𝑣 ∈ ℝ+ ∧ ∀𝑤 ∈ (𝐴 ∩ (-∞(,)𝐵))((𝑤 ≠ 𝐵 ∧ (abs‘(𝑤 − 𝐵)) < 𝑣) → (abs‘(((𝐹 ↾ (-∞(,)𝐵))‘𝑤) − 𝐿)) < 𝑦)) ∧ 𝑎 ∈ ((𝐴 ∩ (-∞(,)𝐵)) ∖ {𝐵}) ∧ ((abs‘(𝑎 − 𝐵)) < 𝑧 ∧ (abs‘(𝑎 − 𝐵)) < 𝑣)) → (abs‘((𝐹‘𝑎) − 𝐿)) < 𝑦)
329		rspe 3246	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝑎 ∈ 𝐴 ∧ ((abs‘((𝐹‘𝑎) − 𝑥)) < 𝑦 ∧ (abs‘((𝐹‘𝑎) − 𝐿)) < 𝑦)) → ∃𝑎 ∈ 𝐴 ((abs‘((𝐹‘𝑎) − 𝑥)) < 𝑦 ∧ (abs‘((𝐹‘𝑎) − 𝐿)) < 𝑦))
330	288, 302, 328, 329	syl12anc 837	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((((𝜑 ∧ 𝑦 ∈ ℝ+) ∧ 𝑧 ∈ ℝ+ ∧ ∀𝑤 ∈ 𝐴 ((𝑤 ≠ 𝐵 ∧ (abs‘(𝑤 − 𝐵)) < 𝑧) → (abs‘((𝐹‘𝑤) − 𝑥)) < 𝑦)) ∧ 𝑣 ∈ ℝ+ ∧ ∀𝑤 ∈ (𝐴 ∩ (-∞(,)𝐵))((𝑤 ≠ 𝐵 ∧ (abs‘(𝑤 − 𝐵)) < 𝑣) → (abs‘(((𝐹 ↾ (-∞(,)𝐵))‘𝑤) − 𝐿)) < 𝑦)) ∧ 𝑎 ∈ ((𝐴 ∩ (-∞(,)𝐵)) ∖ {𝐵}) ∧ ((abs‘(𝑎 − 𝐵)) < 𝑧 ∧ (abs‘(𝑎 − 𝐵)) < 𝑣)) → ∃𝑎 ∈ 𝐴 ((abs‘((𝐹‘𝑎) − 𝑥)) < 𝑦 ∧ (abs‘((𝐹‘𝑎) − 𝐿)) < 𝑦))
331	330	3exp 1118	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((𝜑 ∧ 𝑦 ∈ ℝ+) ∧ 𝑧 ∈ ℝ+ ∧ ∀𝑤 ∈ 𝐴 ((𝑤 ≠ 𝐵 ∧ (abs‘(𝑤 − 𝐵)) < 𝑧) → (abs‘((𝐹‘𝑤) − 𝑥)) < 𝑦)) ∧ 𝑣 ∈ ℝ+ ∧ ∀𝑤 ∈ (𝐴 ∩ (-∞(,)𝐵))((𝑤 ≠ 𝐵 ∧ (abs‘(𝑤 − 𝐵)) < 𝑣) → (abs‘(((𝐹 ↾ (-∞(,)𝐵))‘𝑤) − 𝐿)) < 𝑦)) → (𝑎 ∈ ((𝐴 ∩ (-∞(,)𝐵)) ∖ {𝐵}) → (((abs‘(𝑎 − 𝐵)) < 𝑧 ∧ (abs‘(𝑎 − 𝐵)) < 𝑣) → ∃𝑎 ∈ 𝐴 ((abs‘((𝐹‘𝑎) − 𝑥)) < 𝑦 ∧ (abs‘((𝐹‘𝑎) − 𝐿)) < 𝑦))))
332	285, 286, 331	rexlimd 3263	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝜑 ∧ 𝑦 ∈ ℝ+) ∧ 𝑧 ∈ ℝ+ ∧ ∀𝑤 ∈ 𝐴 ((𝑤 ≠ 𝐵 ∧ (abs‘(𝑤 − 𝐵)) < 𝑧) → (abs‘((𝐹‘𝑤) − 𝑥)) < 𝑦)) ∧ 𝑣 ∈ ℝ+ ∧ ∀𝑤 ∈ (𝐴 ∩ (-∞(,)𝐵))((𝑤 ≠ 𝐵 ∧ (abs‘(𝑤 − 𝐵)) < 𝑣) → (abs‘(((𝐹 ↾ (-∞(,)𝐵))‘𝑤) − 𝐿)) < 𝑦)) → (∃𝑎 ∈ ((𝐴 ∩ (-∞(,)𝐵)) ∖ {𝐵})((abs‘(𝑎 − 𝐵)) < 𝑧 ∧ (abs‘(𝑎 − 𝐵)) < 𝑣) → ∃𝑎 ∈ 𝐴 ((abs‘((𝐹‘𝑎) − 𝑥)) < 𝑦 ∧ (abs‘((𝐹‘𝑎) − 𝐿)) < 𝑦)))
333	284, 332	mpd 15	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝜑 ∧ 𝑦 ∈ ℝ+) ∧ 𝑧 ∈ ℝ+ ∧ ∀𝑤 ∈ 𝐴 ((𝑤 ≠ 𝐵 ∧ (abs‘(𝑤 − 𝐵)) < 𝑧) → (abs‘((𝐹‘𝑤) − 𝑥)) < 𝑦)) ∧ 𝑣 ∈ ℝ+ ∧ ∀𝑤 ∈ (𝐴 ∩ (-∞(,)𝐵))((𝑤 ≠ 𝐵 ∧ (abs‘(𝑤 − 𝐵)) < 𝑣) → (abs‘(((𝐹 ↾ (-∞(,)𝐵))‘𝑤) − 𝐿)) < 𝑦)) → ∃𝑎 ∈ 𝐴 ((abs‘((𝐹‘𝑎) − 𝑥)) < 𝑦 ∧ (abs‘((𝐹‘𝑎) − 𝐿)) < 𝑦))
334	333	3exp 1118	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑦 ∈ ℝ+) ∧ 𝑧 ∈ ℝ+ ∧ ∀𝑤 ∈ 𝐴 ((𝑤 ≠ 𝐵 ∧ (abs‘(𝑤 − 𝐵)) < 𝑧) → (abs‘((𝐹‘𝑤) − 𝑥)) < 𝑦)) → (𝑣 ∈ ℝ+ → (∀𝑤 ∈ (𝐴 ∩ (-∞(,)𝐵))((𝑤 ≠ 𝐵 ∧ (abs‘(𝑤 − 𝐵)) < 𝑣) → (abs‘(((𝐹 ↾ (-∞(,)𝐵))‘𝑤) − 𝐿)) < 𝑦) → ∃𝑎 ∈ 𝐴 ((abs‘((𝐹‘𝑎) − 𝑥)) < 𝑦 ∧ (abs‘((𝐹‘𝑎) − 𝐿)) < 𝑦))))
335	334	rexlimdv 3150	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑦 ∈ ℝ+) ∧ 𝑧 ∈ ℝ+ ∧ ∀𝑤 ∈ 𝐴 ((𝑤 ≠ 𝐵 ∧ (abs‘(𝑤 − 𝐵)) < 𝑧) → (abs‘((𝐹‘𝑤) − 𝑥)) < 𝑦)) → (∃𝑣 ∈ ℝ+ ∀𝑤 ∈ (𝐴 ∩ (-∞(,)𝐵))((𝑤 ≠ 𝐵 ∧ (abs‘(𝑤 − 𝐵)) < 𝑣) → (abs‘(((𝐹 ↾ (-∞(,)𝐵))‘𝑤) − 𝐿)) < 𝑦) → ∃𝑎 ∈ 𝐴 ((abs‘((𝐹‘𝑎) − 𝑥)) < 𝑦 ∧ (abs‘((𝐹‘𝑎) − 𝐿)) < 𝑦)))
336	241, 335	mpd 15	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑦 ∈ ℝ+) ∧ 𝑧 ∈ ℝ+ ∧ ∀𝑤 ∈ 𝐴 ((𝑤 ≠ 𝐵 ∧ (abs‘(𝑤 − 𝐵)) < 𝑧) → (abs‘((𝐹‘𝑤) − 𝑥)) < 𝑦)) → ∃𝑎 ∈ 𝐴 ((abs‘((𝐹‘𝑎) − 𝑥)) < 𝑦 ∧ (abs‘((𝐹‘𝑎) − 𝐿)) < 𝑦))
337	336	3exp 1118	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑦 ∈ ℝ+) → (𝑧 ∈ ℝ+ → (∀𝑤 ∈ 𝐴 ((𝑤 ≠ 𝐵 ∧ (abs‘(𝑤 − 𝐵)) < 𝑧) → (abs‘((𝐹‘𝑤) − 𝑥)) < 𝑦) → ∃𝑎 ∈ 𝐴 ((abs‘((𝐹‘𝑎) − 𝑥)) < 𝑦 ∧ (abs‘((𝐹‘𝑎) − 𝐿)) < 𝑦))))
338	337	rexlimdv 3150	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑦 ∈ ℝ+) → (∃𝑧 ∈ ℝ+ ∀𝑤 ∈ 𝐴 ((𝑤 ≠ 𝐵 ∧ (abs‘(𝑤 − 𝐵)) < 𝑧) → (abs‘((𝐹‘𝑤) − 𝑥)) < 𝑦) → ∃𝑎 ∈ 𝐴 ((abs‘((𝐹‘𝑎) − 𝑥)) < 𝑦 ∧ (abs‘((𝐹‘𝑎) − 𝐿)) < 𝑦)))
339	338	imp 406	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑦 ∈ ℝ+) ∧ ∃𝑧 ∈ ℝ+ ∀𝑤 ∈ 𝐴 ((𝑤 ≠ 𝐵 ∧ (abs‘(𝑤 − 𝐵)) < 𝑧) → (abs‘((𝐹‘𝑤) − 𝑥)) < 𝑦)) → ∃𝑎 ∈ 𝐴 ((abs‘((𝐹‘𝑎) − 𝑥)) < 𝑦 ∧ (abs‘((𝐹‘𝑎) − 𝐿)) < 𝑦))
340	339	adantllr 719	. . . . . . . . . . . 12 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℂ) ∧ 𝑦 ∈ ℝ+) ∧ ∃𝑧 ∈ ℝ+ ∀𝑤 ∈ 𝐴 ((𝑤 ≠ 𝐵 ∧ (abs‘(𝑤 − 𝐵)) < 𝑧) → (abs‘((𝐹‘𝑤) − 𝑥)) < 𝑦)) → ∃𝑎 ∈ 𝐴 ((abs‘((𝐹‘𝑎) − 𝑥)) < 𝑦 ∧ (abs‘((𝐹‘𝑎) − 𝐿)) < 𝑦))
341	231, 340	reximddv3 3169	. . . . . . . . . . 11 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℂ) ∧ 𝑦 ∈ ℝ+) ∧ ∃𝑧 ∈ ℝ+ ∀𝑤 ∈ 𝐴 ((𝑤 ≠ 𝐵 ∧ (abs‘(𝑤 − 𝐵)) < 𝑧) → (abs‘((𝐹‘𝑤) − 𝑥)) < 𝑦)) → ∃𝑎 ∈ 𝐴 ∃𝑏 ∈ 𝐴 (abs‘(𝑅 − 𝐿)) < (4 · 𝑦))
342	32, 33, 35, 341	syl21anc 838	. . . . . . . . . 10 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℂ) ∧ ∀𝑦 ∈ ℝ+ ∃𝑧 ∈ ℝ+ ∀𝑤 ∈ 𝐴 ((𝑤 ≠ 𝐵 ∧ (abs‘(𝑤 − 𝐵)) < 𝑧) → (abs‘((𝐹‘𝑤) − 𝑥)) < 𝑦)) ∧ 𝑦 ∈ ℝ+) → ∃𝑎 ∈ 𝐴 ∃𝑏 ∈ 𝐴 (abs‘(𝑅 − 𝐿)) < (4 · 𝑦))
343	342	ex 412	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑥 ∈ ℂ) ∧ ∀𝑦 ∈ ℝ+ ∃𝑧 ∈ ℝ+ ∀𝑤 ∈ 𝐴 ((𝑤 ≠ 𝐵 ∧ (abs‘(𝑤 − 𝐵)) < 𝑧) → (abs‘((𝐹‘𝑤) − 𝑥)) < 𝑦)) → (𝑦 ∈ ℝ+ → ∃𝑎 ∈ 𝐴 ∃𝑏 ∈ 𝐴 (abs‘(𝑅 − 𝐿)) < (4 · 𝑦)))
344	24, 25, 31, 343	vtoclf 3563	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑥 ∈ ℂ) ∧ ∀𝑦 ∈ ℝ+ ∃𝑧 ∈ ℝ+ ∀𝑤 ∈ 𝐴 ((𝑤 ≠ 𝐵 ∧ (abs‘(𝑤 − 𝐵)) < 𝑧) → (abs‘((𝐹‘𝑤) − 𝑥)) < 𝑦)) → (((abs‘(𝑅 − 𝐿)) / 4) ∈ ℝ+ → ∃𝑎 ∈ 𝐴 ∃𝑏 ∈ 𝐴 (abs‘(𝑅 − 𝐿)) < (4 · ((abs‘(𝑅 − 𝐿)) / 4))))
345	19, 344	mpd 15	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑥 ∈ ℂ) ∧ ∀𝑦 ∈ ℝ+ ∃𝑧 ∈ ℝ+ ∀𝑤 ∈ 𝐴 ((𝑤 ≠ 𝐵 ∧ (abs‘(𝑤 − 𝐵)) < 𝑧) → (abs‘((𝐹‘𝑤) − 𝑥)) < 𝑦)) → ∃𝑎 ∈ 𝐴 ∃𝑏 ∈ 𝐴 (abs‘(𝑅 − 𝐿)) < (4 · ((abs‘(𝑅 − 𝐿)) / 4)))
346		simpr 484	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (abs‘(𝑅 − 𝐿)) < (4 · ((abs‘(𝑅 − 𝐿)) / 4))) → (abs‘(𝑅 − 𝐿)) < (4 · ((abs‘(𝑅 − 𝐿)) / 4)))
347		abssubrp 45225	. . . . . . . . . . . . . . . 16 ⊢ ((𝑅 ∈ ℂ ∧ 𝐿 ∈ ℂ ∧ 𝑅 ≠ 𝐿) → (abs‘(𝑅 − 𝐿)) ∈ ℝ+)
348	3, 7, 11, 347	syl3anc 1370	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (abs‘(𝑅 − 𝐿)) ∈ ℝ+)
349	348	rpcnd 13076	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (abs‘(𝑅 − 𝐿)) ∈ ℂ)
350	349	adantr 480	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ (abs‘(𝑅 − 𝐿)) < (4 · ((abs‘(𝑅 − 𝐿)) / 4))) → (abs‘(𝑅 − 𝐿)) ∈ ℂ)
351		4cn 12348	. . . . . . . . . . . . . 14 ⊢ 4 ∈ ℂ
352	351	a1i 11	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ (abs‘(𝑅 − 𝐿)) < (4 · ((abs‘(𝑅 − 𝐿)) / 4))) → 4 ∈ ℂ)
353		4ne0 12371	. . . . . . . . . . . . . 14 ⊢ 4 ≠ 0
354	353	a1i 11	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ (abs‘(𝑅 − 𝐿)) < (4 · ((abs‘(𝑅 − 𝐿)) / 4))) → 4 ≠ 0)
355	350, 352, 354	divcan2d 12042	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (abs‘(𝑅 − 𝐿)) < (4 · ((abs‘(𝑅 − 𝐿)) / 4))) → (4 · ((abs‘(𝑅 − 𝐿)) / 4)) = (abs‘(𝑅 − 𝐿)))
356	346, 355	breqtrd 5173	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (abs‘(𝑅 − 𝐿)) < (4 · ((abs‘(𝑅 − 𝐿)) / 4))) → (abs‘(𝑅 − 𝐿)) < (abs‘(𝑅 − 𝐿)))
357	356	ex 412	. . . . . . . . . 10 ⊢ (𝜑 → ((abs‘(𝑅 − 𝐿)) < (4 · ((abs‘(𝑅 − 𝐿)) / 4)) → (abs‘(𝑅 − 𝐿)) < (abs‘(𝑅 − 𝐿))))
358	357	a1d 25	. . . . . . . . 9 ⊢ (𝜑 → ((𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐴) → ((abs‘(𝑅 − 𝐿)) < (4 · ((abs‘(𝑅 − 𝐿)) / 4)) → (abs‘(𝑅 − 𝐿)) < (abs‘(𝑅 − 𝐿)))))
359	358	ad2antrr 726	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑥 ∈ ℂ) ∧ ∀𝑦 ∈ ℝ+ ∃𝑧 ∈ ℝ+ ∀𝑤 ∈ 𝐴 ((𝑤 ≠ 𝐵 ∧ (abs‘(𝑤 − 𝐵)) < 𝑧) → (abs‘((𝐹‘𝑤) − 𝑥)) < 𝑦)) → ((𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐴) → ((abs‘(𝑅 − 𝐿)) < (4 · ((abs‘(𝑅 − 𝐿)) / 4)) → (abs‘(𝑅 − 𝐿)) < (abs‘(𝑅 − 𝐿)))))
360	359	rexlimdvv 3209	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑥 ∈ ℂ) ∧ ∀𝑦 ∈ ℝ+ ∃𝑧 ∈ ℝ+ ∀𝑤 ∈ 𝐴 ((𝑤 ≠ 𝐵 ∧ (abs‘(𝑤 − 𝐵)) < 𝑧) → (abs‘((𝐹‘𝑤) − 𝑥)) < 𝑦)) → (∃𝑎 ∈ 𝐴 ∃𝑏 ∈ 𝐴 (abs‘(𝑅 − 𝐿)) < (4 · ((abs‘(𝑅 − 𝐿)) / 4)) → (abs‘(𝑅 − 𝐿)) < (abs‘(𝑅 − 𝐿))))
361	345, 360	mpd 15	. . . . . 6 ⊢ (((𝜑 ∧ 𝑥 ∈ ℂ) ∧ ∀𝑦 ∈ ℝ+ ∃𝑧 ∈ ℝ+ ∀𝑤 ∈ 𝐴 ((𝑤 ≠ 𝐵 ∧ (abs‘(𝑤 − 𝐵)) < 𝑧) → (abs‘((𝐹‘𝑤) − 𝑥)) < 𝑦)) → (abs‘(𝑅 − 𝐿)) < (abs‘(𝑅 − 𝐿)))
362	9	abscld 15471	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑥 ∈ ℂ) ∧ ∀𝑦 ∈ ℝ+ ∃𝑧 ∈ ℝ+ ∀𝑤 ∈ 𝐴 ((𝑤 ≠ 𝐵 ∧ (abs‘(𝑤 − 𝐵)) < 𝑧) → (abs‘((𝐹‘𝑤) − 𝑥)) < 𝑦)) → (abs‘(𝑅 − 𝐿)) ∈ ℝ)
363	362	ltnrd 11392	. . . . . 6 ⊢ (((𝜑 ∧ 𝑥 ∈ ℂ) ∧ ∀𝑦 ∈ ℝ+ ∃𝑧 ∈ ℝ+ ∀𝑤 ∈ 𝐴 ((𝑤 ≠ 𝐵 ∧ (abs‘(𝑤 − 𝐵)) < 𝑧) → (abs‘((𝐹‘𝑤) − 𝑥)) < 𝑦)) → ¬ (abs‘(𝑅 − 𝐿)) < (abs‘(𝑅 − 𝐿)))
364	361, 363	pm2.65da 817	. . . . 5 ⊢ ((𝜑 ∧ 𝑥 ∈ ℂ) → ¬ ∀𝑦 ∈ ℝ+ ∃𝑧 ∈ ℝ+ ∀𝑤 ∈ 𝐴 ((𝑤 ≠ 𝐵 ∧ (abs‘(𝑤 − 𝐵)) < 𝑧) → (abs‘((𝐹‘𝑤) − 𝑥)) < 𝑦))
365	364	ex 412	. . . 4 ⊢ (𝜑 → (𝑥 ∈ ℂ → ¬ ∀𝑦 ∈ ℝ+ ∃𝑧 ∈ ℝ+ ∀𝑤 ∈ 𝐴 ((𝑤 ≠ 𝐵 ∧ (abs‘(𝑤 − 𝐵)) < 𝑧) → (abs‘((𝐹‘𝑤) − 𝑥)) < 𝑦)))
366		imnan 399	. . . 4 ⊢ ((𝑥 ∈ ℂ → ¬ ∀𝑦 ∈ ℝ+ ∃𝑧 ∈ ℝ+ ∀𝑤 ∈ 𝐴 ((𝑤 ≠ 𝐵 ∧ (abs‘(𝑤 − 𝐵)) < 𝑧) → (abs‘((𝐹‘𝑤) − 𝑥)) < 𝑦)) ↔ ¬ (𝑥 ∈ ℂ ∧ ∀𝑦 ∈ ℝ+ ∃𝑧 ∈ ℝ+ ∀𝑤 ∈ 𝐴 ((𝑤 ≠ 𝐵 ∧ (abs‘(𝑤 − 𝐵)) < 𝑧) → (abs‘((𝐹‘𝑤) − 𝑥)) < 𝑦)))
367	365, 366	sylib 218	. . 3 ⊢ (𝜑 → ¬ (𝑥 ∈ ℂ ∧ ∀𝑦 ∈ ℝ+ ∃𝑧 ∈ ℝ+ ∀𝑤 ∈ 𝐴 ((𝑤 ≠ 𝐵 ∧ (abs‘(𝑤 − 𝐵)) < 𝑧) → (abs‘((𝐹‘𝑤) − 𝑥)) < 𝑦)))
368		limclner.a	. . . . 5 ⊢ (𝜑 → 𝐴 ⊆ ℝ)
369	368, 73	sstrd 4005	. . . 4 ⊢ (𝜑 → 𝐴 ⊆ ℂ)
370	36, 369, 56	ellimc3 25928	. . 3 ⊢ (𝜑 → (𝑥 ∈ (𝐹 limℂ 𝐵) ↔ (𝑥 ∈ ℂ ∧ ∀𝑦 ∈ ℝ+ ∃𝑧 ∈ ℝ+ ∀𝑤 ∈ 𝐴 ((𝑤 ≠ 𝐵 ∧ (abs‘(𝑤 − 𝐵)) < 𝑧) → (abs‘((𝐹‘𝑤) − 𝑥)) < 𝑦))))
371	367, 370	mtbird 325	. 2 ⊢ (𝜑 → ¬ 𝑥 ∈ (𝐹 limℂ 𝐵))
372	371	eq0rdv 4412	1 ⊢ (𝜑 → (𝐹 limℂ 𝐵) = ∅)

Syntax hints:  ¬ wn 3   → wi 4   ∧ wa 395   ∧ w3a 1086   = wceq 1536   ∈ wcel 2105   ≠ wne 2937  ∀wral 3058  ∃wrex 3067   ∖ cdif 3959   ∩ cin 3961   ⊆ wss 3962  ∅c0 4338  ifcif 4530  {csn 4630  ∪ cuni 4911   class class class wbr 5147  ran crn 5689   ↾ cres 5690  ⟶wf 6558  ‘cfv 6562  (class class class)co 7430  ℂcc 11150  ℝcr 11151  0cc0 11152   + caddc 11155   · cmul 11157  +∞cpnf 11289  -∞cmnf 11290   < clt 11292   ≤ cle 11293   − cmin 11489   / cdiv 11917  4c4 12320  ℝ⁺crp 13031  (,)cioo 13383  abscabs 15269   ↾_t crest 17466  TopOpenctopn 17467  topGenctg 17483  ℂ_fldccnfld 21381  Topctop 22914  limPtclp 23157   lim_ℂ climc 25911

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1791  ax-4 1805  ax-5 1907  ax-6 1964  ax-7 2004  ax-8 2107  ax-9 2115  ax-10 2138  ax-11 2154  ax-12 2174  ax-ext 2705  ax-rep 5284  ax-sep 5301  ax-nul 5311  ax-pow 5370  ax-pr 5437  ax-un 7753  ax-cnex 11208  ax-resscn 11209  ax-1cn 11210  ax-icn 11211  ax-addcl 11212  ax-addrcl 11213  ax-mulcl 11214  ax-mulrcl 11215  ax-mulcom 11216  ax-addass 11217  ax-mulass 11218  ax-distr 11219  ax-i2m1 11220  ax-1ne0 11221  ax-1rid 11222  ax-rnegex 11223  ax-rrecex 11224  ax-cnre 11225  ax-pre-lttri 11226  ax-pre-lttrn 11227  ax-pre-ltadd 11228  ax-pre-mulgt0 11229  ax-pre-sup 11230

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3or 1087  df-3an 1088  df-tru 1539  df-fal 1549  df-ex 1776  df-nf 1780  df-sb 2062  df-mo 2537  df-eu 2566  df-clab 2712  df-cleq 2726  df-clel 2813  df-nfc 2889  df-ne 2938  df-nel 3044  df-ral 3059  df-rex 3068  df-rmo 3377  df-reu 3378  df-rab 3433  df-v 3479  df-sbc 3791  df-csb 3908  df-dif 3965  df-un 3967  df-in 3969  df-ss 3979  df-pss 3982  df-nul 4339  df-if 4531  df-pw 4606  df-sn 4631  df-pr 4633  df-tp 4635  df-op 4637  df-uni 4912  df-int 4951  df-iun 4997  df-iin 4998  df-br 5148  df-opab 5210  df-mpt 5231  df-tr 5265  df-id 5582  df-eprel 5588  df-po 5596  df-so 5597  df-fr 5640  df-we 5642  df-xp 5694  df-rel 5695  df-cnv 5696  df-co 5697  df-dm 5698  df-rn 5699  df-res 5700  df-ima 5701  df-pred 6322  df-ord 6388  df-on 6389  df-lim 6390  df-suc 6391  df-iota 6515  df-fun 6564  df-fn 6565  df-f 6566  df-f1 6567  df-fo 6568  df-f1o 6569  df-fv 6570  df-riota 7387  df-ov 7433  df-oprab 7434  df-mpo 7435  df-om 7887  df-1st 8012  df-2nd 8013  df-frecs 8304  df-wrecs 8335  df-recs 8409  df-rdg 8448  df-1o 8504  df-er 8743  df-map 8866  df-pm 8867  df-en 8984  df-dom 8985  df-sdom 8986  df-fin 8987  df-fi 9448  df-sup 9479  df-inf 9480  df-pnf 11294  df-mnf 11295  df-xr 11296  df-ltxr 11297  df-le 11298  df-sub 11491  df-neg 11492  df-div 11918  df-nn 12264  df-2 12326  df-3 12327  df-4 12328  df-5 12329  df-6 12330  df-7 12331  df-8 12332  df-9 12333  df-n0 12524  df-z 12611  df-dec 12731  df-uz 12876  df-q 12988  df-rp 13032  df-xneg 13151  df-xadd 13152  df-xmul 13153  df-ioo 13387  df-fz 13544  df-seq 14039  df-exp 14099  df-cj 15134  df-re 15135  df-im 15136  df-sqrt 15270  df-abs 15271  df-struct 17180  df-slot 17215  df-ndx 17227  df-base 17245  df-plusg 17310  df-mulr 17311  df-starv 17312  df-tset 17316  df-ple 17317  df-ds 17319  df-unif 17320  df-rest 17468  df-topn 17469  df-topgen 17489  df-psmet 21373  df-xmet 21374  df-met 21375  df-bl 21376  df-mopn 21377  df-cnfld 21382  df-top 22915  df-topon 22932  df-topsp 22954  df-bases 22968  df-cld 23042  df-ntr 23043  df-cls 23044  df-nei 23121  df-lp 23159  df-cnp 23251  df-xms 24345  df-ms 24346  df-limc 25915

This theorem is referenced by:  limclr  45610  jumpncnp  45853