Theorem limclner 44357

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 25391	. . . . . . . . . . . . 13 ⊢ ((𝐹 ↾ (𝐵(,)+∞)) limℂ 𝐵) ⊆ ℂ
2		limclner.r	. . . . . . . . . . . . 13 ⊢ (𝜑 → 𝑅 ∈ ((𝐹 ↾ (𝐵(,)+∞)) limℂ 𝐵))
3	1, 2	sselid 3980	. . . . . . . . . . . 12 ⊢ (𝜑 → 𝑅 ∈ ℂ)
4	3	ad2antrr 724	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑥 ∈ ℂ) ∧ ∀𝑦 ∈ ℝ+ ∃𝑧 ∈ ℝ+ ∀𝑤 ∈ 𝐴 ((𝑤 ≠ 𝐵 ∧ (abs‘(𝑤 − 𝐵)) < 𝑧) → (abs‘((𝐹‘𝑤) − 𝑥)) < 𝑦)) → 𝑅 ∈ ℂ)
5		limccl 25391	. . . . . . . . . . . . 13 ⊢ ((𝐹 ↾ (-∞(,)𝐵)) limℂ 𝐵) ⊆ ℂ
6		limclner.l	. . . . . . . . . . . . 13 ⊢ (𝜑 → 𝐿 ∈ ((𝐹 ↾ (-∞(,)𝐵)) limℂ 𝐵))
7	5, 6	sselid 3980	. . . . . . . . . . . 12 ⊢ (𝜑 → 𝐿 ∈ ℂ)
8	7	ad2antrr 724	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑥 ∈ ℂ) ∧ ∀𝑦 ∈ ℝ+ ∃𝑧 ∈ ℝ+ ∀𝑤 ∈ 𝐴 ((𝑤 ≠ 𝐵 ∧ (abs‘(𝑤 − 𝐵)) < 𝑧) → (abs‘((𝐹‘𝑤) − 𝑥)) < 𝑦)) → 𝐿 ∈ ℂ)
9	4, 8	subcld 11570	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑥 ∈ ℂ) ∧ ∀𝑦 ∈ ℝ+ ∃𝑧 ∈ ℝ+ ∀𝑤 ∈ 𝐴 ((𝑤 ≠ 𝐵 ∧ (abs‘(𝑤 − 𝐵)) < 𝑧) → (abs‘((𝐹‘𝑤) − 𝑥)) < 𝑦)) → (𝑅 − 𝐿) ∈ ℂ)
10		limclner.lner	. . . . . . . . . . . . 13 ⊢ (𝜑 → 𝐿 ≠ 𝑅)
11	10	necomd 2996	. . . . . . . . . . . 12 ⊢ (𝜑 → 𝑅 ≠ 𝐿)
12	11	ad2antrr 724	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑥 ∈ ℂ) ∧ ∀𝑦 ∈ ℝ+ ∃𝑧 ∈ ℝ+ ∀𝑤 ∈ 𝐴 ((𝑤 ≠ 𝐵 ∧ (abs‘(𝑤 − 𝐵)) < 𝑧) → (abs‘((𝐹‘𝑤) − 𝑥)) < 𝑦)) → 𝑅 ≠ 𝐿)
13	4, 8, 12	subne0d 11579	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑥 ∈ ℂ) ∧ ∀𝑦 ∈ ℝ+ ∃𝑧 ∈ ℝ+ ∀𝑤 ∈ 𝐴 ((𝑤 ≠ 𝐵 ∧ (abs‘(𝑤 − 𝐵)) < 𝑧) → (abs‘((𝐹‘𝑤) − 𝑥)) < 𝑦)) → (𝑅 − 𝐿) ≠ 0)
14	9, 13	absrpcld 15394	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑥 ∈ ℂ) ∧ ∀𝑦 ∈ ℝ+ ∃𝑧 ∈ ℝ+ ∀𝑤 ∈ 𝐴 ((𝑤 ≠ 𝐵 ∧ (abs‘(𝑤 − 𝐵)) < 𝑧) → (abs‘((𝐹‘𝑤) − 𝑥)) < 𝑦)) → (abs‘(𝑅 − 𝐿)) ∈ ℝ+)
15		4re 12295	. . . . . . . . . . 11 ⊢ 4 ∈ ℝ
16		4pos 12318	. . . . . . . . . . 11 ⊢ 0 < 4
17	15, 16	elrpii 12976	. . . . . . . . . 10 ⊢ 4 ∈ ℝ+
18	17	a1i 11	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑥 ∈ ℂ) ∧ ∀𝑦 ∈ ℝ+ ∃𝑧 ∈ ℝ+ ∀𝑤 ∈ 𝐴 ((𝑤 ≠ 𝐵 ∧ (abs‘(𝑤 − 𝐵)) < 𝑧) → (abs‘((𝐹‘𝑤) − 𝑥)) < 𝑦)) → 4 ∈ ℝ+)
19	14, 18	rpdivcld 13032	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑥 ∈ ℂ) ∧ ∀𝑦 ∈ ℝ+ ∃𝑧 ∈ ℝ+ ∀𝑤 ∈ 𝐴 ((𝑤 ≠ 𝐵 ∧ (abs‘(𝑤 − 𝐵)) < 𝑧) → (abs‘((𝐹‘𝑤) − 𝑥)) < 𝑦)) → ((abs‘(𝑅 − 𝐿)) / 4) ∈ ℝ+)
20		nfv 1917	. . . . . . . . . . 11 ⊢ Ⅎ𝑦(𝜑 ∧ 𝑥 ∈ ℂ)
21		nfra1 3281	. . . . . . . . . . 11 ⊢ Ⅎ𝑦∀𝑦 ∈ ℝ+ ∃𝑧 ∈ ℝ+ ∀𝑤 ∈ 𝐴 ((𝑤 ≠ 𝐵 ∧ (abs‘(𝑤 − 𝐵)) < 𝑧) → (abs‘((𝐹‘𝑤) − 𝑥)) < 𝑦)
22	20, 21	nfan 1902	. . . . . . . . . 10 ⊢ Ⅎ𝑦((𝜑 ∧ 𝑥 ∈ ℂ) ∧ ∀𝑦 ∈ ℝ+ ∃𝑧 ∈ ℝ+ ∀𝑤 ∈ 𝐴 ((𝑤 ≠ 𝐵 ∧ (abs‘(𝑤 − 𝐵)) < 𝑧) → (abs‘((𝐹‘𝑤) − 𝑥)) < 𝑦))
23		nfv 1917	. . . . . . . . . 10 ⊢ Ⅎ𝑦(((abs‘(𝑅 − 𝐿)) / 4) ∈ ℝ+ → ∃𝑎 ∈ 𝐴 ∃𝑏 ∈ 𝐴 (abs‘(𝑅 − 𝐿)) < (4 · ((abs‘(𝑅 − 𝐿)) / 4)))
24	22, 23	nfim 1899	. . . . . . . . 9 ⊢ Ⅎ𝑦(((𝜑 ∧ 𝑥 ∈ ℂ) ∧ ∀𝑦 ∈ ℝ+ ∃𝑧 ∈ ℝ+ ∀𝑤 ∈ 𝐴 ((𝑤 ≠ 𝐵 ∧ (abs‘(𝑤 − 𝐵)) < 𝑧) → (abs‘((𝐹‘𝑤) − 𝑥)) < 𝑦)) → (((abs‘(𝑅 − 𝐿)) / 4) ∈ ℝ+ → ∃𝑎 ∈ 𝐴 ∃𝑏 ∈ 𝐴 (abs‘(𝑅 − 𝐿)) < (4 · ((abs‘(𝑅 − 𝐿)) / 4))))
25		ovex 7441	. . . . . . . . 9 ⊢ ((abs‘(𝑅 − 𝐿)) / 4) ∈ V
26		eleq1 2821	. . . . . . . . . . 11 ⊢ (𝑦 = ((abs‘(𝑅 − 𝐿)) / 4) → (𝑦 ∈ ℝ+ ↔ ((abs‘(𝑅 − 𝐿)) / 4) ∈ ℝ+))
27		oveq2 7416	. . . . . . . . . . . . 13 ⊢ (𝑦 = ((abs‘(𝑅 − 𝐿)) / 4) → (4 · 𝑦) = (4 · ((abs‘(𝑅 − 𝐿)) / 4)))
28	27	breq2d 5160	. . . . . . . . . . . 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 765	. . . . . . . . . . 11 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℂ) ∧ ∀𝑦 ∈ ℝ+ ∃𝑧 ∈ ℝ+ ∀𝑤 ∈ 𝐴 ((𝑤 ≠ 𝐵 ∧ (abs‘(𝑤 − 𝐵)) < 𝑧) → (abs‘((𝐹‘𝑤) − 𝑥)) < 𝑦)) ∧ 𝑦 ∈ ℝ+) → (𝜑 ∧ 𝑥 ∈ ℂ))
33		simpr 485	. . . . . . . . . . 11 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℂ) ∧ ∀𝑦 ∈ ℝ+ ∃𝑧 ∈ ℝ+ ∀𝑤 ∈ 𝐴 ((𝑤 ≠ 𝐵 ∧ (abs‘(𝑤 − 𝐵)) < 𝑧) → (abs‘((𝐹‘𝑤) − 𝑥)) < 𝑦)) ∧ 𝑦 ∈ ℝ+) → 𝑦 ∈ ℝ+)
34		rspa 3245	. . . . . . . . . . . 12 ⊢ ((∀𝑦 ∈ ℝ+ ∃𝑧 ∈ ℝ+ ∀𝑤 ∈ 𝐴 ((𝑤 ≠ 𝐵 ∧ (abs‘(𝑤 − 𝐵)) < 𝑧) → (abs‘((𝐹‘𝑤) − 𝑥)) < 𝑦) ∧ 𝑦 ∈ ℝ+) → ∃𝑧 ∈ ℝ+ ∀𝑤 ∈ 𝐴 ((𝑤 ≠ 𝐵 ∧ (abs‘(𝑤 − 𝐵)) < 𝑧) → (abs‘((𝐹‘𝑤) − 𝑥)) < 𝑦))
35	34	adantll 712	. . . . . . . . . . 11 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℂ) ∧ ∀𝑦 ∈ ℝ+ ∃𝑧 ∈ ℝ+ ∀𝑤 ∈ 𝐴 ((𝑤 ≠ 𝐵 ∧ (abs‘(𝑤 − 𝐵)) < 𝑧) → (abs‘((𝐹‘𝑤) − 𝑥)) < 𝑦)) ∧ 𝑦 ∈ ℝ+) → ∃𝑧 ∈ ℝ+ ∀𝑤 ∈ 𝐴 ((𝑤 ≠ 𝐵 ∧ (abs‘(𝑤 − 𝐵)) < 𝑧) → (abs‘((𝐹‘𝑤) − 𝑥)) < 𝑦))
36		limclner.f	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝜑 → 𝐹:𝐴⟶ℂ)
37		fresin 6760	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝐹:𝐴⟶ℂ → (𝐹 ↾ (𝐵(,)+∞)):(𝐴 ∩ (𝐵(,)+∞))⟶ℂ)
38	36, 37	syl 17	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝜑 → (𝐹 ↾ (𝐵(,)+∞)):(𝐴 ∩ (𝐵(,)+∞))⟶ℂ)
39		inss2 4229	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝐴 ∩ (𝐵(,)+∞)) ⊆ (𝐵(,)+∞)
40		ioosscn 13385	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝐵(,)+∞) ⊆ ℂ
41	39, 40	sstri 3991	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝐴 ∩ (𝐵(,)+∞)) ⊆ ℂ
42	41	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝜑 → (𝐴 ∩ (𝐵(,)+∞)) ⊆ ℂ)
43		limclner.j	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ 𝐽 = (topGen‘ran (,))
44		retop 24277	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (topGen‘ran (,)) ∈ Top
45	43, 44	eqeltri 2829	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ 𝐽 ∈ Top
46		inss2 4229	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (𝐴 ∩ (-∞(,)𝐵)) ⊆ (-∞(,)𝐵)
47		ioossre 13384	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (-∞(,)𝐵) ⊆ ℝ
48	46, 47	sstri 3991	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝐴 ∩ (-∞(,)𝐵)) ⊆ ℝ
49		uniretop 24278	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ ℝ = ∪ (topGen‘ran (,))
50	43	unieqi 4921	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ ∪ 𝐽 = ∪ (topGen‘ran (,))
51	49, 50	eqtr4i 2763	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ℝ = ∪ 𝐽
52	51	lpss 22645	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((𝐽 ∈ Top ∧ (𝐴 ∩ (-∞(,)𝐵)) ⊆ ℝ) → ((limPt‘𝐽)‘(𝐴 ∩ (-∞(,)𝐵))) ⊆ ℝ)
53	45, 48, 52	mp2an 690	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((limPt‘𝐽)‘(𝐴 ∩ (-∞(,)𝐵))) ⊆ ℝ
54		limclner.blp1	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝜑 → 𝐵 ∈ ((limPt‘𝐽)‘(𝐴 ∩ (-∞(,)𝐵))))
55	53, 54	sselid 3980	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝜑 → 𝐵 ∈ ℝ)
56	55	recnd 11241	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝜑 → 𝐵 ∈ ℂ)
57	38, 42, 56	ellimc3 25395	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝜑 → (𝑅 ∈ ((𝐹 ↾ (𝐵(,)+∞)) limℂ 𝐵) ↔ (𝑅 ∈ ℂ ∧ ∀𝑦 ∈ ℝ+ ∃𝑣 ∈ ℝ+ ∀𝑤 ∈ (𝐴 ∩ (𝐵(,)+∞))((𝑤 ≠ 𝐵 ∧ (abs‘(𝑤 − 𝐵)) < 𝑣) → (abs‘(((𝐹 ↾ (𝐵(,)+∞))‘𝑤) − 𝑅)) < 𝑦))))
58	2, 57	mpbid 231	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝜑 → (𝑅 ∈ ℂ ∧ ∀𝑦 ∈ ℝ+ ∃𝑣 ∈ ℝ+ ∀𝑤 ∈ (𝐴 ∩ (𝐵(,)+∞))((𝑤 ≠ 𝐵 ∧ (abs‘(𝑤 − 𝐵)) < 𝑣) → (abs‘(((𝐹 ↾ (𝐵(,)+∞))‘𝑤) − 𝑅)) < 𝑦)))
59	58	simprd 496	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝜑 → ∀𝑦 ∈ ℝ+ ∃𝑣 ∈ ℝ+ ∀𝑤 ∈ (𝐴 ∩ (𝐵(,)+∞))((𝑤 ≠ 𝐵 ∧ (abs‘(𝑤 − 𝐵)) < 𝑣) → (abs‘(((𝐹 ↾ (𝐵(,)+∞))‘𝑤) − 𝑅)) < 𝑦))
60	59	r19.21bi 3248	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ 𝑦 ∈ ℝ+) → ∃𝑣 ∈ ℝ+ ∀𝑤 ∈ (𝐴 ∩ (𝐵(,)+∞))((𝑤 ≠ 𝐵 ∧ (abs‘(𝑤 − 𝐵)) < 𝑣) → (abs‘(((𝐹 ↾ (𝐵(,)+∞))‘𝑤) − 𝑅)) < 𝑦))
61	60	3ad2ant1 1133	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ 𝑦 ∈ ℝ+) ∧ 𝑧 ∈ ℝ+ ∧ ∀𝑤 ∈ 𝐴 ((𝑤 ≠ 𝐵 ∧ (abs‘(𝑤 − 𝐵)) < 𝑧) → (abs‘((𝐹‘𝑤) − 𝑥)) < 𝑦)) → ∃𝑣 ∈ ℝ+ ∀𝑤 ∈ (𝐴 ∩ (𝐵(,)+∞))((𝑤 ≠ 𝐵 ∧ (abs‘(𝑤 − 𝐵)) < 𝑣) → (abs‘(((𝐹 ↾ (𝐵(,)+∞))‘𝑤) − 𝑅)) < 𝑦))
62		simp11l 1284	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((((𝜑 ∧ 𝑦 ∈ ℝ+) ∧ 𝑧 ∈ ℝ+ ∧ ∀𝑤 ∈ 𝐴 ((𝑤 ≠ 𝐵 ∧ (abs‘(𝑤 − 𝐵)) < 𝑧) → (abs‘((𝐹‘𝑤) − 𝑥)) < 𝑦)) ∧ 𝑣 ∈ ℝ+ ∧ ∀𝑤 ∈ (𝐴 ∩ (𝐵(,)+∞))((𝑤 ≠ 𝐵 ∧ (abs‘(𝑤 − 𝐵)) < 𝑣) → (abs‘(((𝐹 ↾ (𝐵(,)+∞))‘𝑤) − 𝑅)) < 𝑦)) → 𝜑)
63		simp12 1204	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((((𝜑 ∧ 𝑦 ∈ ℝ+) ∧ 𝑧 ∈ ℝ+ ∧ ∀𝑤 ∈ 𝐴 ((𝑤 ≠ 𝐵 ∧ (abs‘(𝑤 − 𝐵)) < 𝑧) → (abs‘((𝐹‘𝑤) − 𝑥)) < 𝑦)) ∧ 𝑣 ∈ ℝ+ ∧ ∀𝑤 ∈ (𝐴 ∩ (𝐵(,)+∞))((𝑤 ≠ 𝐵 ∧ (abs‘(𝑤 − 𝐵)) < 𝑣) → (abs‘(((𝐹 ↾ (𝐵(,)+∞))‘𝑤) − 𝑅)) < 𝑦)) → 𝑧 ∈ ℝ+)
64		simp2 1137	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((((𝜑 ∧ 𝑦 ∈ ℝ+) ∧ 𝑧 ∈ ℝ+ ∧ ∀𝑤 ∈ 𝐴 ((𝑤 ≠ 𝐵 ∧ (abs‘(𝑤 − 𝐵)) < 𝑧) → (abs‘((𝐹‘𝑤) − 𝑥)) < 𝑦)) ∧ 𝑣 ∈ ℝ+ ∧ ∀𝑤 ∈ (𝐴 ∩ (𝐵(,)+∞))((𝑤 ≠ 𝐵 ∧ (abs‘(𝑤 − 𝐵)) < 𝑣) → (abs‘(((𝐹 ↾ (𝐵(,)+∞))‘𝑤) − 𝑅)) < 𝑦)) → 𝑣 ∈ ℝ+)
65		breq2 5152	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝑢 = if(𝑧 ≤ 𝑣, 𝑧, 𝑣) → ((abs‘(𝑏 − 𝐵)) < 𝑢 ↔ (abs‘(𝑏 − 𝐵)) < if(𝑧 ≤ 𝑣, 𝑧, 𝑣)))
66	65	rexbidv 3178	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑢 = if(𝑧 ≤ 𝑣, 𝑧, 𝑣) → (∃𝑏 ∈ ((𝐴 ∩ (𝐵(,)+∞)) ∖ {𝐵})(abs‘(𝑏 − 𝐵)) < 𝑢 ↔ ∃𝑏 ∈ ((𝐴 ∩ (𝐵(,)+∞)) ∖ {𝐵})(abs‘(𝑏 − 𝐵)) < if(𝑧 ≤ 𝑣, 𝑧, 𝑣)))
67		inss1 4228	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ (((limPt‘𝐾)‘(𝐴 ∩ (𝐵(,)+∞))) ∩ ℝ) ⊆ ((limPt‘𝐾)‘(𝐴 ∩ (𝐵(,)+∞)))
68	67	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (𝜑 → (((limPt‘𝐾)‘(𝐴 ∩ (𝐵(,)+∞))) ∩ ℝ) ⊆ ((limPt‘𝐾)‘(𝐴 ∩ (𝐵(,)+∞))))
69		limclner.k	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ 𝐾 = (TopOpen‘ℂfld)
70	69	cnfldtop 24299	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ 𝐾 ∈ Top
71	70	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ (𝜑 → 𝐾 ∈ Top)
72		ax-resscn 11166	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ ℝ ⊆ ℂ
73	72	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ (𝜑 → ℝ ⊆ ℂ)
74		ioossre 13384	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ (𝐵(,)+∞) ⊆ ℝ
75	39, 74	sstri 3991	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ (𝐴 ∩ (𝐵(,)+∞)) ⊆ ℝ
76	75	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ (𝜑 → (𝐴 ∩ (𝐵(,)+∞)) ⊆ ℝ)
77		unicntop 24301	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ ℂ = ∪ (TopOpen‘ℂfld)
78	69	unieqi 4921	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ ∪ 𝐾 = ∪ (TopOpen‘ℂfld)
79	77, 78	eqtr4i 2763	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ ℂ = ∪ 𝐾
80	69	tgioo2 24318	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ (topGen‘ran (,)) = (𝐾 ↾t ℝ)
81	43, 80	eqtri 2760	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ 𝐽 = (𝐾 ↾t ℝ)
82	79, 81	restlp 22686	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ ((𝐾 ∈ Top ∧ ℝ ⊆ ℂ ∧ (𝐴 ∩ (𝐵(,)+∞)) ⊆ ℝ) → ((limPt‘𝐽)‘(𝐴 ∩ (𝐵(,)+∞))) = (((limPt‘𝐾)‘(𝐴 ∩ (𝐵(,)+∞))) ∩ ℝ))
83	71, 73, 76, 82	syl3anc 1371	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (𝜑 → ((limPt‘𝐽)‘(𝐴 ∩ (𝐵(,)+∞))) = (((limPt‘𝐾)‘(𝐴 ∩ (𝐵(,)+∞))) ∩ ℝ))
84	69	eqcomi 2741	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ (TopOpen‘ℂfld) = 𝐾
85	84	fveq2i 6894	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ (limPt‘(TopOpen‘ℂfld)) = (limPt‘𝐾)
86	85	fveq1i 6892	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ ((limPt‘(TopOpen‘ℂfld))‘(𝐴 ∩ (𝐵(,)+∞))) = ((limPt‘𝐾)‘(𝐴 ∩ (𝐵(,)+∞)))
87	86	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (𝜑 → ((limPt‘(TopOpen‘ℂfld))‘(𝐴 ∩ (𝐵(,)+∞))) = ((limPt‘𝐾)‘(𝐴 ∩ (𝐵(,)+∞))))
88	68, 83, 87	3sstr4d 4029	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (𝜑 → ((limPt‘𝐽)‘(𝐴 ∩ (𝐵(,)+∞))) ⊆ ((limPt‘(TopOpen‘ℂfld))‘(𝐴 ∩ (𝐵(,)+∞))))
89		limclner.blp2	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (𝜑 → 𝐵 ∈ ((limPt‘𝐽)‘(𝐴 ∩ (𝐵(,)+∞))))
90	88, 89	sseldd 3983	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝜑 → 𝐵 ∈ ((limPt‘(TopOpen‘ℂfld))‘(𝐴 ∩ (𝐵(,)+∞))))
91	42, 56	islpcn 44345	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝜑 → (𝐵 ∈ ((limPt‘(TopOpen‘ℂfld))‘(𝐴 ∩ (𝐵(,)+∞))) ↔ ∀𝑢 ∈ ℝ+ ∃𝑏 ∈ ((𝐴 ∩ (𝐵(,)+∞)) ∖ {𝐵})(abs‘(𝑏 − 𝐵)) < 𝑢))
92	90, 91	mpbid 231	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝜑 → ∀𝑢 ∈ ℝ+ ∃𝑏 ∈ ((𝐴 ∩ (𝐵(,)+∞)) ∖ {𝐵})(abs‘(𝑏 − 𝐵)) < 𝑢)
93	92	3ad2ant1 1133	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((𝜑 ∧ 𝑧 ∈ ℝ+ ∧ 𝑣 ∈ ℝ+) → ∀𝑢 ∈ ℝ+ ∃𝑏 ∈ ((𝐴 ∩ (𝐵(,)+∞)) ∖ {𝐵})(abs‘(𝑏 − 𝐵)) < 𝑢)
94		ifcl 4573	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((𝑧 ∈ ℝ+ ∧ 𝑣 ∈ ℝ+) → if(𝑧 ≤ 𝑣, 𝑧, 𝑣) ∈ ℝ+)
95	94	3adant1 1130	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((𝜑 ∧ 𝑧 ∈ ℝ+ ∧ 𝑣 ∈ ℝ+) → if(𝑧 ≤ 𝑣, 𝑧, 𝑣) ∈ ℝ+)
96	66, 93, 95	rspcdva 3613	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝜑 ∧ 𝑧 ∈ ℝ+ ∧ 𝑣 ∈ ℝ+) → ∃𝑏 ∈ ((𝐴 ∩ (𝐵(,)+∞)) ∖ {𝐵})(abs‘(𝑏 − 𝐵)) < if(𝑧 ≤ 𝑣, 𝑧, 𝑣))
97		eldifi 4126	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝑏 ∈ ((𝐴 ∩ (𝐵(,)+∞)) ∖ {𝐵}) → 𝑏 ∈ (𝐴 ∩ (𝐵(,)+∞)))
98	75, 97	sselid 3980	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝑏 ∈ ((𝐴 ∩ (𝐵(,)+∞)) ∖ {𝐵}) → 𝑏 ∈ ℝ)
99	73	sselda 3982	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ ((𝜑 ∧ 𝑏 ∈ ℝ) → 𝑏 ∈ ℂ)
100	56	adantr 481	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ ((𝜑 ∧ 𝑏 ∈ ℝ) → 𝐵 ∈ ℂ)
101	99, 100	subcld 11570	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ ((𝜑 ∧ 𝑏 ∈ ℝ) → (𝑏 − 𝐵) ∈ ℂ)
102	101	abscld 15382	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ ((𝜑 ∧ 𝑏 ∈ ℝ) → (abs‘(𝑏 − 𝐵)) ∈ ℝ)
103	102	3ad2antl1 1185	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ (((𝜑 ∧ 𝑧 ∈ ℝ+ ∧ 𝑣 ∈ ℝ+) ∧ 𝑏 ∈ ℝ) → (abs‘(𝑏 − 𝐵)) ∈ ℝ)
104	103	adantr 481	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ ((((𝜑 ∧ 𝑧 ∈ ℝ+ ∧ 𝑣 ∈ ℝ+) ∧ 𝑏 ∈ ℝ) ∧ (abs‘(𝑏 − 𝐵)) < if(𝑧 ≤ 𝑣, 𝑧, 𝑣)) → (abs‘(𝑏 − 𝐵)) ∈ ℝ)
105	95	rpred 13015	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ ((𝜑 ∧ 𝑧 ∈ ℝ+ ∧ 𝑣 ∈ ℝ+) → if(𝑧 ≤ 𝑣, 𝑧, 𝑣) ∈ ℝ)
106	105	ad2antrr 724	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ ((((𝜑 ∧ 𝑧 ∈ ℝ+ ∧ 𝑣 ∈ ℝ+) ∧ 𝑏 ∈ ℝ) ∧ (abs‘(𝑏 − 𝐵)) < if(𝑧 ≤ 𝑣, 𝑧, 𝑣)) → if(𝑧 ≤ 𝑣, 𝑧, 𝑣) ∈ ℝ)
107		rpre 12981	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ (𝑧 ∈ ℝ+ → 𝑧 ∈ ℝ)
108	107	3ad2ant2 1134	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ ((𝜑 ∧ 𝑧 ∈ ℝ+ ∧ 𝑣 ∈ ℝ+) → 𝑧 ∈ ℝ)
109	108	ad2antrr 724	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ ((((𝜑 ∧ 𝑧 ∈ ℝ+ ∧ 𝑣 ∈ ℝ+) ∧ 𝑏 ∈ ℝ) ∧ (abs‘(𝑏 − 𝐵)) < if(𝑧 ≤ 𝑣, 𝑧, 𝑣)) → 𝑧 ∈ ℝ)
110		simpr 485	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ ((((𝜑 ∧ 𝑧 ∈ ℝ+ ∧ 𝑣 ∈ ℝ+) ∧ 𝑏 ∈ ℝ) ∧ (abs‘(𝑏 − 𝐵)) < if(𝑧 ≤ 𝑣, 𝑧, 𝑣)) → (abs‘(𝑏 − 𝐵)) < if(𝑧 ≤ 𝑣, 𝑧, 𝑣))
111		rpre 12981	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ (𝑣 ∈ ℝ+ → 𝑣 ∈ ℝ)
112		min1 13167	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ ((𝑧 ∈ ℝ ∧ 𝑣 ∈ ℝ) → if(𝑧 ≤ 𝑣, 𝑧, 𝑣) ≤ 𝑧)
113	107, 111, 112	syl2an 596	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ ((𝑧 ∈ ℝ+ ∧ 𝑣 ∈ ℝ+) → if(𝑧 ≤ 𝑣, 𝑧, 𝑣) ≤ 𝑧)
114	113	3adant1 1130	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ ((𝜑 ∧ 𝑧 ∈ ℝ+ ∧ 𝑣 ∈ ℝ+) → if(𝑧 ≤ 𝑣, 𝑧, 𝑣) ≤ 𝑧)
115	114	ad2antrr 724	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ ((((𝜑 ∧ 𝑧 ∈ ℝ+ ∧ 𝑣 ∈ ℝ+) ∧ 𝑏 ∈ ℝ) ∧ (abs‘(𝑏 − 𝐵)) < if(𝑧 ≤ 𝑣, 𝑧, 𝑣)) → if(𝑧 ≤ 𝑣, 𝑧, 𝑣) ≤ 𝑧)
116	104, 106, 109, 110, 115	ltletrd 11373	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ((((𝜑 ∧ 𝑧 ∈ ℝ+ ∧ 𝑣 ∈ ℝ+) ∧ 𝑏 ∈ ℝ) ∧ (abs‘(𝑏 − 𝐵)) < if(𝑧 ≤ 𝑣, 𝑧, 𝑣)) → (abs‘(𝑏 − 𝐵)) < 𝑧)
117	111	3ad2ant3 1135	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ ((𝜑 ∧ 𝑧 ∈ ℝ+ ∧ 𝑣 ∈ ℝ+) → 𝑣 ∈ ℝ)
118	117	ad2antrr 724	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ ((((𝜑 ∧ 𝑧 ∈ ℝ+ ∧ 𝑣 ∈ ℝ+) ∧ 𝑏 ∈ ℝ) ∧ (abs‘(𝑏 − 𝐵)) < if(𝑧 ≤ 𝑣, 𝑧, 𝑣)) → 𝑣 ∈ ℝ)
119	109, 118	min2d 44173	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ ((((𝜑 ∧ 𝑧 ∈ ℝ+ ∧ 𝑣 ∈ ℝ+) ∧ 𝑏 ∈ ℝ) ∧ (abs‘(𝑏 − 𝐵)) < if(𝑧 ≤ 𝑣, 𝑧, 𝑣)) → if(𝑧 ≤ 𝑣, 𝑧, 𝑣) ≤ 𝑣)
120	104, 106, 118, 110, 119	ltletrd 11373	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ((((𝜑 ∧ 𝑧 ∈ ℝ+ ∧ 𝑣 ∈ ℝ+) ∧ 𝑏 ∈ ℝ) ∧ (abs‘(𝑏 − 𝐵)) < if(𝑧 ≤ 𝑣, 𝑧, 𝑣)) → (abs‘(𝑏 − 𝐵)) < 𝑣)
121	116, 120	jca 512	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((((𝜑 ∧ 𝑧 ∈ ℝ+ ∧ 𝑣 ∈ ℝ+) ∧ 𝑏 ∈ ℝ) ∧ (abs‘(𝑏 − 𝐵)) < if(𝑧 ≤ 𝑣, 𝑧, 𝑣)) → ((abs‘(𝑏 − 𝐵)) < 𝑧 ∧ (abs‘(𝑏 − 𝐵)) < 𝑣))
122	121	ex 413	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (((𝜑 ∧ 𝑧 ∈ ℝ+ ∧ 𝑣 ∈ ℝ+) ∧ 𝑏 ∈ ℝ) → ((abs‘(𝑏 − 𝐵)) < if(𝑧 ≤ 𝑣, 𝑧, 𝑣) → ((abs‘(𝑏 − 𝐵)) < 𝑧 ∧ (abs‘(𝑏 − 𝐵)) < 𝑣)))
123	98, 122	sylan2 593	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((𝜑 ∧ 𝑧 ∈ ℝ+ ∧ 𝑣 ∈ ℝ+) ∧ 𝑏 ∈ ((𝐴 ∩ (𝐵(,)+∞)) ∖ {𝐵})) → ((abs‘(𝑏 − 𝐵)) < if(𝑧 ≤ 𝑣, 𝑧, 𝑣) → ((abs‘(𝑏 − 𝐵)) < 𝑧 ∧ (abs‘(𝑏 − 𝐵)) < 𝑣)))
124	123	reximdva 3168	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝜑 ∧ 𝑧 ∈ ℝ+ ∧ 𝑣 ∈ ℝ+) → (∃𝑏 ∈ ((𝐴 ∩ (𝐵(,)+∞)) ∖ {𝐵})(abs‘(𝑏 − 𝐵)) < if(𝑧 ≤ 𝑣, 𝑧, 𝑣) → ∃𝑏 ∈ ((𝐴 ∩ (𝐵(,)+∞)) ∖ {𝐵})((abs‘(𝑏 − 𝐵)) < 𝑧 ∧ (abs‘(𝑏 − 𝐵)) < 𝑣)))
125	96, 124	mpd 15	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝜑 ∧ 𝑧 ∈ ℝ+ ∧ 𝑣 ∈ ℝ+) → ∃𝑏 ∈ ((𝐴 ∩ (𝐵(,)+∞)) ∖ {𝐵})((abs‘(𝑏 − 𝐵)) < 𝑧 ∧ (abs‘(𝑏 − 𝐵)) < 𝑣))
126	62, 63, 64, 125	syl3anc 1371	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((𝜑 ∧ 𝑦 ∈ ℝ+) ∧ 𝑧 ∈ ℝ+ ∧ ∀𝑤 ∈ 𝐴 ((𝑤 ≠ 𝐵 ∧ (abs‘(𝑤 − 𝐵)) < 𝑧) → (abs‘((𝐹‘𝑤) − 𝑥)) < 𝑦)) ∧ 𝑣 ∈ ℝ+ ∧ ∀𝑤 ∈ (𝐴 ∩ (𝐵(,)+∞))((𝑤 ≠ 𝐵 ∧ (abs‘(𝑤 − 𝐵)) < 𝑣) → (abs‘(((𝐹 ↾ (𝐵(,)+∞))‘𝑤) − 𝑅)) < 𝑦)) → ∃𝑏 ∈ ((𝐴 ∩ (𝐵(,)+∞)) ∖ {𝐵})((abs‘(𝑏 − 𝐵)) < 𝑧 ∧ (abs‘(𝑏 − 𝐵)) < 𝑣))
127		nfv 1917	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ Ⅎ𝑏(((𝜑 ∧ 𝑦 ∈ ℝ+) ∧ 𝑧 ∈ ℝ+ ∧ ∀𝑤 ∈ 𝐴 ((𝑤 ≠ 𝐵 ∧ (abs‘(𝑤 − 𝐵)) < 𝑧) → (abs‘((𝐹‘𝑤) − 𝑥)) < 𝑦)) ∧ 𝑣 ∈ ℝ+ ∧ ∀𝑤 ∈ (𝐴 ∩ (𝐵(,)+∞))((𝑤 ≠ 𝐵 ∧ (abs‘(𝑤 − 𝐵)) < 𝑣) → (abs‘(((𝐹 ↾ (𝐵(,)+∞))‘𝑤) − 𝑅)) < 𝑦))
128		nfre1 3282	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ Ⅎ𝑏∃𝑏 ∈ 𝐴 ((abs‘((𝐹‘𝑏) − 𝑥)) < 𝑦 ∧ (abs‘((𝐹‘𝑏) − 𝑅)) < 𝑦)
129	97	elin1d 4198	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝑏 ∈ ((𝐴 ∩ (𝐵(,)+∞)) ∖ {𝐵}) → 𝑏 ∈ 𝐴)
130	129	3ad2ant2 1134	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((((𝜑 ∧ 𝑦 ∈ ℝ+) ∧ 𝑧 ∈ ℝ+ ∧ ∀𝑤 ∈ 𝐴 ((𝑤 ≠ 𝐵 ∧ (abs‘(𝑤 − 𝐵)) < 𝑧) → (abs‘((𝐹‘𝑤) − 𝑥)) < 𝑦)) ∧ 𝑣 ∈ ℝ+ ∧ ∀𝑤 ∈ (𝐴 ∩ (𝐵(,)+∞))((𝑤 ≠ 𝐵 ∧ (abs‘(𝑤 − 𝐵)) < 𝑣) → (abs‘(((𝐹 ↾ (𝐵(,)+∞))‘𝑤) − 𝑅)) < 𝑦)) ∧ 𝑏 ∈ ((𝐴 ∩ (𝐵(,)+∞)) ∖ {𝐵}) ∧ ((abs‘(𝑏 − 𝐵)) < 𝑧 ∧ (abs‘(𝑏 − 𝐵)) < 𝑣)) → 𝑏 ∈ 𝐴)
131		simp113 1304	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (((((𝜑 ∧ 𝑦 ∈ ℝ+) ∧ 𝑧 ∈ ℝ+ ∧ ∀𝑤 ∈ 𝐴 ((𝑤 ≠ 𝐵 ∧ (abs‘(𝑤 − 𝐵)) < 𝑧) → (abs‘((𝐹‘𝑤) − 𝑥)) < 𝑦)) ∧ 𝑣 ∈ ℝ+ ∧ ∀𝑤 ∈ (𝐴 ∩ (𝐵(,)+∞))((𝑤 ≠ 𝐵 ∧ (abs‘(𝑤 − 𝐵)) < 𝑣) → (abs‘(((𝐹 ↾ (𝐵(,)+∞))‘𝑤) − 𝑅)) < 𝑦)) ∧ 𝑏 ∈ ((𝐴 ∩ (𝐵(,)+∞)) ∖ {𝐵}) ∧ ((abs‘(𝑏 − 𝐵)) < 𝑧 ∧ (abs‘(𝑏 − 𝐵)) < 𝑣)) → ∀𝑤 ∈ 𝐴 ((𝑤 ≠ 𝐵 ∧ (abs‘(𝑤 − 𝐵)) < 𝑧) → (abs‘((𝐹‘𝑤) − 𝑥)) < 𝑦))
132		eldifsni 4793	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (𝑏 ∈ ((𝐴 ∩ (𝐵(,)+∞)) ∖ {𝐵}) → 𝑏 ≠ 𝐵)
133	132	adantr 481	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ((𝑏 ∈ ((𝐴 ∩ (𝐵(,)+∞)) ∖ {𝐵}) ∧ ((abs‘(𝑏 − 𝐵)) < 𝑧 ∧ (abs‘(𝑏 − 𝐵)) < 𝑣)) → 𝑏 ≠ 𝐵)
134		simprl 769	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ((𝑏 ∈ ((𝐴 ∩ (𝐵(,)+∞)) ∖ {𝐵}) ∧ ((abs‘(𝑏 − 𝐵)) < 𝑧 ∧ (abs‘(𝑏 − 𝐵)) < 𝑣)) → (abs‘(𝑏 − 𝐵)) < 𝑧)
135	133, 134	jca 512	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((𝑏 ∈ ((𝐴 ∩ (𝐵(,)+∞)) ∖ {𝐵}) ∧ ((abs‘(𝑏 − 𝐵)) < 𝑧 ∧ (abs‘(𝑏 − 𝐵)) < 𝑣)) → (𝑏 ≠ 𝐵 ∧ (abs‘(𝑏 − 𝐵)) < 𝑧))
136	135	3adant1 1130	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (((((𝜑 ∧ 𝑦 ∈ ℝ+) ∧ 𝑧 ∈ ℝ+ ∧ ∀𝑤 ∈ 𝐴 ((𝑤 ≠ 𝐵 ∧ (abs‘(𝑤 − 𝐵)) < 𝑧) → (abs‘((𝐹‘𝑤) − 𝑥)) < 𝑦)) ∧ 𝑣 ∈ ℝ+ ∧ ∀𝑤 ∈ (𝐴 ∩ (𝐵(,)+∞))((𝑤 ≠ 𝐵 ∧ (abs‘(𝑤 − 𝐵)) < 𝑣) → (abs‘(((𝐹 ↾ (𝐵(,)+∞))‘𝑤) − 𝑅)) < 𝑦)) ∧ 𝑏 ∈ ((𝐴 ∩ (𝐵(,)+∞)) ∖ {𝐵}) ∧ ((abs‘(𝑏 − 𝐵)) < 𝑧 ∧ (abs‘(𝑏 − 𝐵)) < 𝑣)) → (𝑏 ≠ 𝐵 ∧ (abs‘(𝑏 − 𝐵)) < 𝑧))
137		neeq1 3003	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ (𝑤 = 𝑏 → (𝑤 ≠ 𝐵 ↔ 𝑏 ≠ 𝐵))
138		fvoveq1 7431	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ (𝑤 = 𝑏 → (abs‘(𝑤 − 𝐵)) = (abs‘(𝑏 − 𝐵)))
139	138	breq1d 5158	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ (𝑤 = 𝑏 → ((abs‘(𝑤 − 𝐵)) < 𝑧 ↔ (abs‘(𝑏 − 𝐵)) < 𝑧))
140	137, 139	anbi12d 631	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (𝑤 = 𝑏 → ((𝑤 ≠ 𝐵 ∧ (abs‘(𝑤 − 𝐵)) < 𝑧) ↔ (𝑏 ≠ 𝐵 ∧ (abs‘(𝑏 − 𝐵)) < 𝑧)))
141	140	imbrov2fvoveq 7433	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (𝑤 = 𝑏 → (((𝑤 ≠ 𝐵 ∧ (abs‘(𝑤 − 𝐵)) < 𝑧) → (abs‘((𝐹‘𝑤) − 𝑥)) < 𝑦) ↔ ((𝑏 ≠ 𝐵 ∧ (abs‘(𝑏 − 𝐵)) < 𝑧) → (abs‘((𝐹‘𝑏) − 𝑥)) < 𝑦)))
142	141	rspcva 3610	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((𝑏 ∈ 𝐴 ∧ ∀𝑤 ∈ 𝐴 ((𝑤 ≠ 𝐵 ∧ (abs‘(𝑤 − 𝐵)) < 𝑧) → (abs‘((𝐹‘𝑤) − 𝑥)) < 𝑦)) → ((𝑏 ≠ 𝐵 ∧ (abs‘(𝑏 − 𝐵)) < 𝑧) → (abs‘((𝐹‘𝑏) − 𝑥)) < 𝑦))
143	142	imp 407	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (((𝑏 ∈ 𝐴 ∧ ∀𝑤 ∈ 𝐴 ((𝑤 ≠ 𝐵 ∧ (abs‘(𝑤 − 𝐵)) < 𝑧) → (abs‘((𝐹‘𝑤) − 𝑥)) < 𝑦)) ∧ (𝑏 ≠ 𝐵 ∧ (abs‘(𝑏 − 𝐵)) < 𝑧)) → (abs‘((𝐹‘𝑏) − 𝑥)) < 𝑦)
144	130, 131, 136, 143	syl21anc 836	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((((𝜑 ∧ 𝑦 ∈ ℝ+) ∧ 𝑧 ∈ ℝ+ ∧ ∀𝑤 ∈ 𝐴 ((𝑤 ≠ 𝐵 ∧ (abs‘(𝑤 − 𝐵)) < 𝑧) → (abs‘((𝐹‘𝑤) − 𝑥)) < 𝑦)) ∧ 𝑣 ∈ ℝ+ ∧ ∀𝑤 ∈ (𝐴 ∩ (𝐵(,)+∞))((𝑤 ≠ 𝐵 ∧ (abs‘(𝑤 − 𝐵)) < 𝑣) → (abs‘(((𝐹 ↾ (𝐵(,)+∞))‘𝑤) − 𝑅)) < 𝑦)) ∧ 𝑏 ∈ ((𝐴 ∩ (𝐵(,)+∞)) ∖ {𝐵}) ∧ ((abs‘(𝑏 − 𝐵)) < 𝑧 ∧ (abs‘(𝑏 − 𝐵)) < 𝑣)) → (abs‘((𝐹‘𝑏) − 𝑥)) < 𝑦)
145	97	3ad2ant2 1134	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (((((𝜑 ∧ 𝑦 ∈ ℝ+) ∧ 𝑧 ∈ ℝ+ ∧ ∀𝑤 ∈ 𝐴 ((𝑤 ≠ 𝐵 ∧ (abs‘(𝑤 − 𝐵)) < 𝑧) → (abs‘((𝐹‘𝑤) − 𝑥)) < 𝑦)) ∧ 𝑣 ∈ ℝ+ ∧ ∀𝑤 ∈ (𝐴 ∩ (𝐵(,)+∞))((𝑤 ≠ 𝐵 ∧ (abs‘(𝑤 − 𝐵)) < 𝑣) → (abs‘(((𝐹 ↾ (𝐵(,)+∞))‘𝑤) − 𝑅)) < 𝑦)) ∧ 𝑏 ∈ ((𝐴 ∩ (𝐵(,)+∞)) ∖ {𝐵}) ∧ ((abs‘(𝑏 − 𝐵)) < 𝑧 ∧ (abs‘(𝑏 − 𝐵)) < 𝑣)) → 𝑏 ∈ (𝐴 ∩ (𝐵(,)+∞)))
146	62	3ad2ant1 1133	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (((((𝜑 ∧ 𝑦 ∈ ℝ+) ∧ 𝑧 ∈ ℝ+ ∧ ∀𝑤 ∈ 𝐴 ((𝑤 ≠ 𝐵 ∧ (abs‘(𝑤 − 𝐵)) < 𝑧) → (abs‘((𝐹‘𝑤) − 𝑥)) < 𝑦)) ∧ 𝑣 ∈ ℝ+ ∧ ∀𝑤 ∈ (𝐴 ∩ (𝐵(,)+∞))((𝑤 ≠ 𝐵 ∧ (abs‘(𝑤 − 𝐵)) < 𝑣) → (abs‘(((𝐹 ↾ (𝐵(,)+∞))‘𝑤) − 𝑅)) < 𝑦)) ∧ 𝑏 ∈ ((𝐴 ∩ (𝐵(,)+∞)) ∖ {𝐵}) ∧ ((abs‘(𝑏 − 𝐵)) < 𝑧 ∧ (abs‘(𝑏 − 𝐵)) < 𝑣)) → 𝜑)
147		simp13 1205	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (((((𝜑 ∧ 𝑦 ∈ ℝ+) ∧ 𝑧 ∈ ℝ+ ∧ ∀𝑤 ∈ 𝐴 ((𝑤 ≠ 𝐵 ∧ (abs‘(𝑤 − 𝐵)) < 𝑧) → (abs‘((𝐹‘𝑤) − 𝑥)) < 𝑦)) ∧ 𝑣 ∈ ℝ+ ∧ ∀𝑤 ∈ (𝐴 ∩ (𝐵(,)+∞))((𝑤 ≠ 𝐵 ∧ (abs‘(𝑤 − 𝐵)) < 𝑣) → (abs‘(((𝐹 ↾ (𝐵(,)+∞))‘𝑤) − 𝑅)) < 𝑦)) ∧ 𝑏 ∈ ((𝐴 ∩ (𝐵(,)+∞)) ∖ {𝐵}) ∧ ((abs‘(𝑏 − 𝐵)) < 𝑧 ∧ (abs‘(𝑏 − 𝐵)) < 𝑣)) → ∀𝑤 ∈ (𝐴 ∩ (𝐵(,)+∞))((𝑤 ≠ 𝐵 ∧ (abs‘(𝑤 − 𝐵)) < 𝑣) → (abs‘(((𝐹 ↾ (𝐵(,)+∞))‘𝑤) − 𝑅)) < 𝑦))
148		nfv 1917	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ Ⅎ𝑤𝜑
149		nfra1 3281	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ Ⅎ𝑤∀𝑤 ∈ (𝐴 ∩ (𝐵(,)+∞))((𝑤 ≠ 𝐵 ∧ (abs‘(𝑤 − 𝐵)) < 𝑣) → (abs‘(((𝐹 ↾ (𝐵(,)+∞))‘𝑤) − 𝑅)) < 𝑦)
150	148, 149	nfan 1902	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ Ⅎ𝑤(𝜑 ∧ ∀𝑤 ∈ (𝐴 ∩ (𝐵(,)+∞))((𝑤 ≠ 𝐵 ∧ (abs‘(𝑤 − 𝐵)) < 𝑣) → (abs‘(((𝐹 ↾ (𝐵(,)+∞))‘𝑤) − 𝑅)) < 𝑦))
151		elinel2 4196	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ (𝑤 ∈ (𝐴 ∩ (𝐵(,)+∞)) → 𝑤 ∈ (𝐵(,)+∞))
152	151	fvresd 6911	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ (𝑤 ∈ (𝐴 ∩ (𝐵(,)+∞)) → ((𝐹 ↾ (𝐵(,)+∞))‘𝑤) = (𝐹‘𝑤))
153	152	eqcomd 2738	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ (𝑤 ∈ (𝐴 ∩ (𝐵(,)+∞)) → (𝐹‘𝑤) = ((𝐹 ↾ (𝐵(,)+∞))‘𝑤))
154	153	fvoveq1d 7430	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ (𝑤 ∈ (𝐴 ∩ (𝐵(,)+∞)) → (abs‘((𝐹‘𝑤) − 𝑅)) = (abs‘(((𝐹 ↾ (𝐵(,)+∞))‘𝑤) − 𝑅)))
155	154	3ad2ant2 1134	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ (((𝜑 ∧ ∀𝑤 ∈ (𝐴 ∩ (𝐵(,)+∞))((𝑤 ≠ 𝐵 ∧ (abs‘(𝑤 − 𝐵)) < 𝑣) → (abs‘(((𝐹 ↾ (𝐵(,)+∞))‘𝑤) − 𝑅)) < 𝑦)) ∧ 𝑤 ∈ (𝐴 ∩ (𝐵(,)+∞)) ∧ (𝑤 ≠ 𝐵 ∧ (abs‘(𝑤 − 𝐵)) < 𝑣)) → (abs‘((𝐹‘𝑤) − 𝑅)) = (abs‘(((𝐹 ↾ (𝐵(,)+∞))‘𝑤) − 𝑅)))
156		rspa 3245	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ ((∀𝑤 ∈ (𝐴 ∩ (𝐵(,)+∞))((𝑤 ≠ 𝐵 ∧ (abs‘(𝑤 − 𝐵)) < 𝑣) → (abs‘(((𝐹 ↾ (𝐵(,)+∞))‘𝑤) − 𝑅)) < 𝑦) ∧ 𝑤 ∈ (𝐴 ∩ (𝐵(,)+∞))) → ((𝑤 ≠ 𝐵 ∧ (abs‘(𝑤 − 𝐵)) < 𝑣) → (abs‘(((𝐹 ↾ (𝐵(,)+∞))‘𝑤) − 𝑅)) < 𝑦))
157	156	3impia 1117	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ ((∀𝑤 ∈ (𝐴 ∩ (𝐵(,)+∞))((𝑤 ≠ 𝐵 ∧ (abs‘(𝑤 − 𝐵)) < 𝑣) → (abs‘(((𝐹 ↾ (𝐵(,)+∞))‘𝑤) − 𝑅)) < 𝑦) ∧ 𝑤 ∈ (𝐴 ∩ (𝐵(,)+∞)) ∧ (𝑤 ≠ 𝐵 ∧ (abs‘(𝑤 − 𝐵)) < 𝑣)) → (abs‘(((𝐹 ↾ (𝐵(,)+∞))‘𝑤) − 𝑅)) < 𝑦)
158	157	3adant1l 1176	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ (((𝜑 ∧ ∀𝑤 ∈ (𝐴 ∩ (𝐵(,)+∞))((𝑤 ≠ 𝐵 ∧ (abs‘(𝑤 − 𝐵)) < 𝑣) → (abs‘(((𝐹 ↾ (𝐵(,)+∞))‘𝑤) − 𝑅)) < 𝑦)) ∧ 𝑤 ∈ (𝐴 ∩ (𝐵(,)+∞)) ∧ (𝑤 ≠ 𝐵 ∧ (abs‘(𝑤 − 𝐵)) < 𝑣)) → (abs‘(((𝐹 ↾ (𝐵(,)+∞))‘𝑤) − 𝑅)) < 𝑦)
159	155, 158	eqbrtrd 5170	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (((𝜑 ∧ ∀𝑤 ∈ (𝐴 ∩ (𝐵(,)+∞))((𝑤 ≠ 𝐵 ∧ (abs‘(𝑤 − 𝐵)) < 𝑣) → (abs‘(((𝐹 ↾ (𝐵(,)+∞))‘𝑤) − 𝑅)) < 𝑦)) ∧ 𝑤 ∈ (𝐴 ∩ (𝐵(,)+∞)) ∧ (𝑤 ≠ 𝐵 ∧ (abs‘(𝑤 − 𝐵)) < 𝑣)) → (abs‘((𝐹‘𝑤) − 𝑅)) < 𝑦)
160	159	3exp 1119	. . . . . . . . . . . . . . . . . . . . . . . . . . . 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 714	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((𝑏 ∈ ((𝐴 ∩ (𝐵(,)+∞)) ∖ {𝐵}) ∧ ((abs‘(𝑏 − 𝐵)) < 𝑧 ∧ (abs‘(𝑏 − 𝐵)) < 𝑣)) → (𝑏 ≠ 𝐵 ∧ (abs‘(𝑏 − 𝐵)) < 𝑣))
165	164	3adant1 1130	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (((((𝜑 ∧ 𝑦 ∈ ℝ+) ∧ 𝑧 ∈ ℝ+ ∧ ∀𝑤 ∈ 𝐴 ((𝑤 ≠ 𝐵 ∧ (abs‘(𝑤 − 𝐵)) < 𝑧) → (abs‘((𝐹‘𝑤) − 𝑥)) < 𝑦)) ∧ 𝑣 ∈ ℝ+ ∧ ∀𝑤 ∈ (𝐴 ∩ (𝐵(,)+∞))((𝑤 ≠ 𝐵 ∧ (abs‘(𝑤 − 𝐵)) < 𝑣) → (abs‘(((𝐹 ↾ (𝐵(,)+∞))‘𝑤) − 𝑅)) < 𝑦)) ∧ 𝑏 ∈ ((𝐴 ∩ (𝐵(,)+∞)) ∖ {𝐵}) ∧ ((abs‘(𝑏 − 𝐵)) < 𝑧 ∧ (abs‘(𝑏 − 𝐵)) < 𝑣)) → (𝑏 ≠ 𝐵 ∧ (abs‘(𝑏 − 𝐵)) < 𝑣))
166	138	breq1d 5158	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ (𝑤 = 𝑏 → ((abs‘(𝑤 − 𝐵)) < 𝑣 ↔ (abs‘(𝑏 − 𝐵)) < 𝑣))
167	137, 166	anbi12d 631	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (𝑤 = 𝑏 → ((𝑤 ≠ 𝐵 ∧ (abs‘(𝑤 − 𝐵)) < 𝑣) ↔ (𝑏 ≠ 𝐵 ∧ (abs‘(𝑏 − 𝐵)) < 𝑣)))
168	167	imbrov2fvoveq 7433	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (𝑤 = 𝑏 → (((𝑤 ≠ 𝐵 ∧ (abs‘(𝑤 − 𝐵)) < 𝑣) → (abs‘((𝐹‘𝑤) − 𝑅)) < 𝑦) ↔ ((𝑏 ≠ 𝐵 ∧ (abs‘(𝑏 − 𝐵)) < 𝑣) → (abs‘((𝐹‘𝑏) − 𝑅)) < 𝑦)))
169	168	rspcva 3610	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((𝑏 ∈ (𝐴 ∩ (𝐵(,)+∞)) ∧ ∀𝑤 ∈ (𝐴 ∩ (𝐵(,)+∞))((𝑤 ≠ 𝐵 ∧ (abs‘(𝑤 − 𝐵)) < 𝑣) → (abs‘((𝐹‘𝑤) − 𝑅)) < 𝑦)) → ((𝑏 ≠ 𝐵 ∧ (abs‘(𝑏 − 𝐵)) < 𝑣) → (abs‘((𝐹‘𝑏) − 𝑅)) < 𝑦))
170	169	imp 407	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (((𝑏 ∈ (𝐴 ∩ (𝐵(,)+∞)) ∧ ∀𝑤 ∈ (𝐴 ∩ (𝐵(,)+∞))((𝑤 ≠ 𝐵 ∧ (abs‘(𝑤 − 𝐵)) < 𝑣) → (abs‘((𝐹‘𝑤) − 𝑅)) < 𝑦)) ∧ (𝑏 ≠ 𝐵 ∧ (abs‘(𝑏 − 𝐵)) < 𝑣)) → (abs‘((𝐹‘𝑏) − 𝑅)) < 𝑦)
171	145, 162, 165, 170	syl21anc 836	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((((𝜑 ∧ 𝑦 ∈ ℝ+) ∧ 𝑧 ∈ ℝ+ ∧ ∀𝑤 ∈ 𝐴 ((𝑤 ≠ 𝐵 ∧ (abs‘(𝑤 − 𝐵)) < 𝑧) → (abs‘((𝐹‘𝑤) − 𝑥)) < 𝑦)) ∧ 𝑣 ∈ ℝ+ ∧ ∀𝑤 ∈ (𝐴 ∩ (𝐵(,)+∞))((𝑤 ≠ 𝐵 ∧ (abs‘(𝑤 − 𝐵)) < 𝑣) → (abs‘(((𝐹 ↾ (𝐵(,)+∞))‘𝑤) − 𝑅)) < 𝑦)) ∧ 𝑏 ∈ ((𝐴 ∩ (𝐵(,)+∞)) ∖ {𝐵}) ∧ ((abs‘(𝑏 − 𝐵)) < 𝑧 ∧ (abs‘(𝑏 − 𝐵)) < 𝑣)) → (abs‘((𝐹‘𝑏) − 𝑅)) < 𝑦)
172		rspe 3246	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((𝑏 ∈ 𝐴 ∧ ((abs‘((𝐹‘𝑏) − 𝑥)) < 𝑦 ∧ (abs‘((𝐹‘𝑏) − 𝑅)) < 𝑦)) → ∃𝑏 ∈ 𝐴 ((abs‘((𝐹‘𝑏) − 𝑥)) < 𝑦 ∧ (abs‘((𝐹‘𝑏) − 𝑅)) < 𝑦))
173	130, 144, 171, 172	syl12anc 835	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((((𝜑 ∧ 𝑦 ∈ ℝ+) ∧ 𝑧 ∈ ℝ+ ∧ ∀𝑤 ∈ 𝐴 ((𝑤 ≠ 𝐵 ∧ (abs‘(𝑤 − 𝐵)) < 𝑧) → (abs‘((𝐹‘𝑤) − 𝑥)) < 𝑦)) ∧ 𝑣 ∈ ℝ+ ∧ ∀𝑤 ∈ (𝐴 ∩ (𝐵(,)+∞))((𝑤 ≠ 𝐵 ∧ (abs‘(𝑤 − 𝐵)) < 𝑣) → (abs‘(((𝐹 ↾ (𝐵(,)+∞))‘𝑤) − 𝑅)) < 𝑦)) ∧ 𝑏 ∈ ((𝐴 ∩ (𝐵(,)+∞)) ∖ {𝐵}) ∧ ((abs‘(𝑏 − 𝐵)) < 𝑧 ∧ (abs‘(𝑏 − 𝐵)) < 𝑣)) → ∃𝑏 ∈ 𝐴 ((abs‘((𝐹‘𝑏) − 𝑥)) < 𝑦 ∧ (abs‘((𝐹‘𝑏) − 𝑅)) < 𝑦))
174	173	3exp 1119	. . . . . . . . . . . . . . . . . . . . . . 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 1119	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜑 ∧ 𝑦 ∈ ℝ+) ∧ 𝑧 ∈ ℝ+ ∧ ∀𝑤 ∈ 𝐴 ((𝑤 ≠ 𝐵 ∧ (abs‘(𝑤 − 𝐵)) < 𝑧) → (abs‘((𝐹‘𝑤) − 𝑥)) < 𝑦)) → (𝑣 ∈ ℝ+ → (∀𝑤 ∈ (𝐴 ∩ (𝐵(,)+∞))((𝑤 ≠ 𝐵 ∧ (abs‘(𝑤 − 𝐵)) < 𝑣) → (abs‘(((𝐹 ↾ (𝐵(,)+∞))‘𝑤) − 𝑅)) < 𝑦) → ∃𝑏 ∈ 𝐴 ((abs‘((𝐹‘𝑏) − 𝑥)) < 𝑦 ∧ (abs‘((𝐹‘𝑏) − 𝑅)) < 𝑦))))
178	177	rexlimdv 3153	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ 𝑦 ∈ ℝ+) ∧ 𝑧 ∈ ℝ+ ∧ ∀𝑤 ∈ 𝐴 ((𝑤 ≠ 𝐵 ∧ (abs‘(𝑤 − 𝐵)) < 𝑧) → (abs‘((𝐹‘𝑤) − 𝑥)) < 𝑦)) → (∃𝑣 ∈ ℝ+ ∀𝑤 ∈ (𝐴 ∩ (𝐵(,)+∞))((𝑤 ≠ 𝐵 ∧ (abs‘(𝑤 − 𝐵)) < 𝑣) → (abs‘(((𝐹 ↾ (𝐵(,)+∞))‘𝑤) − 𝑅)) < 𝑦) → ∃𝑏 ∈ 𝐴 ((abs‘((𝐹‘𝑏) − 𝑥)) < 𝑦 ∧ (abs‘((𝐹‘𝑏) − 𝑅)) < 𝑦)))
179	61, 178	mpd 15	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑦 ∈ ℝ+) ∧ 𝑧 ∈ ℝ+ ∧ ∀𝑤 ∈ 𝐴 ((𝑤 ≠ 𝐵 ∧ (abs‘(𝑤 − 𝐵)) < 𝑧) → (abs‘((𝐹‘𝑤) − 𝑥)) < 𝑦)) → ∃𝑏 ∈ 𝐴 ((abs‘((𝐹‘𝑏) − 𝑥)) < 𝑦 ∧ (abs‘((𝐹‘𝑏) − 𝑅)) < 𝑦))
180	179	3exp 1119	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑦 ∈ ℝ+) → (𝑧 ∈ ℝ+ → (∀𝑤 ∈ 𝐴 ((𝑤 ≠ 𝐵 ∧ (abs‘(𝑤 − 𝐵)) < 𝑧) → (abs‘((𝐹‘𝑤) − 𝑥)) < 𝑦) → ∃𝑏 ∈ 𝐴 ((abs‘((𝐹‘𝑏) − 𝑥)) < 𝑦 ∧ (abs‘((𝐹‘𝑏) − 𝑅)) < 𝑦))))
181	180	rexlimdv 3153	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑦 ∈ ℝ+) → (∃𝑧 ∈ ℝ+ ∀𝑤 ∈ 𝐴 ((𝑤 ≠ 𝐵 ∧ (abs‘(𝑤 − 𝐵)) < 𝑧) → (abs‘((𝐹‘𝑤) − 𝑥)) < 𝑦) → ∃𝑏 ∈ 𝐴 ((abs‘((𝐹‘𝑏) − 𝑥)) < 𝑦 ∧ (abs‘((𝐹‘𝑏) − 𝑅)) < 𝑦)))
182	181	imp 407	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑦 ∈ ℝ+) ∧ ∃𝑧 ∈ ℝ+ ∀𝑤 ∈ 𝐴 ((𝑤 ≠ 𝐵 ∧ (abs‘(𝑤 − 𝐵)) < 𝑧) → (abs‘((𝐹‘𝑤) − 𝑥)) < 𝑦)) → ∃𝑏 ∈ 𝐴 ((abs‘((𝐹‘𝑏) − 𝑥)) < 𝑦 ∧ (abs‘((𝐹‘𝑏) − 𝑅)) < 𝑦))
183	182	adantllr 717	. . . . . . . . . . . . . 14 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℂ) ∧ 𝑦 ∈ ℝ+) ∧ ∃𝑧 ∈ ℝ+ ∀𝑤 ∈ 𝐴 ((𝑤 ≠ 𝐵 ∧ (abs‘(𝑤 − 𝐵)) < 𝑧) → (abs‘((𝐹‘𝑤) − 𝑥)) < 𝑦)) → ∃𝑏 ∈ 𝐴 ((abs‘((𝐹‘𝑏) − 𝑥)) < 𝑦 ∧ (abs‘((𝐹‘𝑏) − 𝑅)) < 𝑦))
184	183	ad2antrr 724	. . . . . . . . . . . . 13 ⊢ ((((((𝜑 ∧ 𝑥 ∈ ℂ) ∧ 𝑦 ∈ ℝ+) ∧ ∃𝑧 ∈ ℝ+ ∀𝑤 ∈ 𝐴 ((𝑤 ≠ 𝐵 ∧ (abs‘(𝑤 − 𝐵)) < 𝑧) → (abs‘((𝐹‘𝑤) − 𝑥)) < 𝑦)) ∧ 𝑎 ∈ 𝐴) ∧ ((abs‘((𝐹‘𝑎) − 𝑥)) < 𝑦 ∧ (abs‘((𝐹‘𝑎) − 𝐿)) < 𝑦)) → ∃𝑏 ∈ 𝐴 ((abs‘((𝐹‘𝑏) − 𝑥)) < 𝑦 ∧ (abs‘((𝐹‘𝑏) − 𝑅)) < 𝑦))
185	3	ad6antr 734	. . . . . . . . . . . . . . . . . . 19 ⊢ (((((((𝜑 ∧ 𝑥 ∈ ℂ) ∧ 𝑦 ∈ ℝ+) ∧ 𝑎 ∈ 𝐴) ∧ ((abs‘((𝐹‘𝑎) − 𝑥)) < 𝑦 ∧ (abs‘((𝐹‘𝑎) − 𝐿)) < 𝑦)) ∧ 𝑏 ∈ 𝐴) ∧ ((abs‘((𝐹‘𝑏) − 𝑥)) < 𝑦 ∧ (abs‘((𝐹‘𝑏) − 𝑅)) < 𝑦)) → 𝑅 ∈ ℂ)
186	7	ad6antr 734	. . . . . . . . . . . . . . . . . . 19 ⊢ (((((((𝜑 ∧ 𝑥 ∈ ℂ) ∧ 𝑦 ∈ ℝ+) ∧ 𝑎 ∈ 𝐴) ∧ ((abs‘((𝐹‘𝑎) − 𝑥)) < 𝑦 ∧ (abs‘((𝐹‘𝑎) − 𝐿)) < 𝑦)) ∧ 𝑏 ∈ 𝐴) ∧ ((abs‘((𝐹‘𝑏) − 𝑥)) < 𝑦 ∧ (abs‘((𝐹‘𝑏) − 𝑅)) < 𝑦)) → 𝐿 ∈ ℂ)
187	185, 186	subcld 11570	. . . . . . . . . . . . . . . . . 18 ⊢ (((((((𝜑 ∧ 𝑥 ∈ ℂ) ∧ 𝑦 ∈ ℝ+) ∧ 𝑎 ∈ 𝐴) ∧ ((abs‘((𝐹‘𝑎) − 𝑥)) < 𝑦 ∧ (abs‘((𝐹‘𝑎) − 𝐿)) < 𝑦)) ∧ 𝑏 ∈ 𝐴) ∧ ((abs‘((𝐹‘𝑏) − 𝑥)) < 𝑦 ∧ (abs‘((𝐹‘𝑏) − 𝑅)) < 𝑦)) → (𝑅 − 𝐿) ∈ ℂ)
188	187	abscld 15382	. . . . . . . . . . . . . . . . 17 ⊢ (((((((𝜑 ∧ 𝑥 ∈ ℂ) ∧ 𝑦 ∈ ℝ+) ∧ 𝑎 ∈ 𝐴) ∧ ((abs‘((𝐹‘𝑎) − 𝑥)) < 𝑦 ∧ (abs‘((𝐹‘𝑎) − 𝐿)) < 𝑦)) ∧ 𝑏 ∈ 𝐴) ∧ ((abs‘((𝐹‘𝑏) − 𝑥)) < 𝑦 ∧ (abs‘((𝐹‘𝑏) − 𝑅)) < 𝑦)) → (abs‘(𝑅 − 𝐿)) ∈ ℝ)
189		simp-6l 785	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((((((𝜑 ∧ 𝑥 ∈ ℂ) ∧ 𝑦 ∈ ℝ+) ∧ 𝑎 ∈ 𝐴) ∧ ((abs‘((𝐹‘𝑎) − 𝑥)) < 𝑦 ∧ (abs‘((𝐹‘𝑎) − 𝐿)) < 𝑦)) ∧ 𝑏 ∈ 𝐴) ∧ ((abs‘((𝐹‘𝑏) − 𝑥)) < 𝑦 ∧ (abs‘((𝐹‘𝑏) − 𝑅)) < 𝑦)) → 𝜑)
190		simplr 767	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((((((𝜑 ∧ 𝑥 ∈ ℂ) ∧ 𝑦 ∈ ℝ+) ∧ 𝑎 ∈ 𝐴) ∧ ((abs‘((𝐹‘𝑎) − 𝑥)) < 𝑦 ∧ (abs‘((𝐹‘𝑎) − 𝐿)) < 𝑦)) ∧ 𝑏 ∈ 𝐴) ∧ ((abs‘((𝐹‘𝑏) − 𝑥)) < 𝑦 ∧ (abs‘((𝐹‘𝑏) − 𝑅)) < 𝑦)) → 𝑏 ∈ 𝐴)
191	36	ffvelcdmda 7086	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝜑 ∧ 𝑏 ∈ 𝐴) → (𝐹‘𝑏) ∈ ℂ)
192	189, 190, 191	syl2anc 584	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((((((𝜑 ∧ 𝑥 ∈ ℂ) ∧ 𝑦 ∈ ℝ+) ∧ 𝑎 ∈ 𝐴) ∧ ((abs‘((𝐹‘𝑎) − 𝑥)) < 𝑦 ∧ (abs‘((𝐹‘𝑎) − 𝐿)) < 𝑦)) ∧ 𝑏 ∈ 𝐴) ∧ ((abs‘((𝐹‘𝑏) − 𝑥)) < 𝑦 ∧ (abs‘((𝐹‘𝑏) − 𝑅)) < 𝑦)) → (𝐹‘𝑏) ∈ ℂ)
193	185, 192	subcld 11570	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((((((𝜑 ∧ 𝑥 ∈ ℂ) ∧ 𝑦 ∈ ℝ+) ∧ 𝑎 ∈ 𝐴) ∧ ((abs‘((𝐹‘𝑎) − 𝑥)) < 𝑦 ∧ (abs‘((𝐹‘𝑎) − 𝐿)) < 𝑦)) ∧ 𝑏 ∈ 𝐴) ∧ ((abs‘((𝐹‘𝑏) − 𝑥)) < 𝑦 ∧ (abs‘((𝐹‘𝑏) − 𝑅)) < 𝑦)) → (𝑅 − (𝐹‘𝑏)) ∈ ℂ)
194	193	abscld 15382	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((((((𝜑 ∧ 𝑥 ∈ ℂ) ∧ 𝑦 ∈ ℝ+) ∧ 𝑎 ∈ 𝐴) ∧ ((abs‘((𝐹‘𝑎) − 𝑥)) < 𝑦 ∧ (abs‘((𝐹‘𝑎) − 𝐿)) < 𝑦)) ∧ 𝑏 ∈ 𝐴) ∧ ((abs‘((𝐹‘𝑏) − 𝑥)) < 𝑦 ∧ (abs‘((𝐹‘𝑏) − 𝑅)) < 𝑦)) → (abs‘(𝑅 − (𝐹‘𝑏))) ∈ ℝ)
195		simp-6r 786	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((((((𝜑 ∧ 𝑥 ∈ ℂ) ∧ 𝑦 ∈ ℝ+) ∧ 𝑎 ∈ 𝐴) ∧ ((abs‘((𝐹‘𝑎) − 𝑥)) < 𝑦 ∧ (abs‘((𝐹‘𝑎) − 𝐿)) < 𝑦)) ∧ 𝑏 ∈ 𝐴) ∧ ((abs‘((𝐹‘𝑏) − 𝑥)) < 𝑦 ∧ (abs‘((𝐹‘𝑏) − 𝑅)) < 𝑦)) → 𝑥 ∈ ℂ)
196	192, 195	subcld 11570	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((((((𝜑 ∧ 𝑥 ∈ ℂ) ∧ 𝑦 ∈ ℝ+) ∧ 𝑎 ∈ 𝐴) ∧ ((abs‘((𝐹‘𝑎) − 𝑥)) < 𝑦 ∧ (abs‘((𝐹‘𝑎) − 𝐿)) < 𝑦)) ∧ 𝑏 ∈ 𝐴) ∧ ((abs‘((𝐹‘𝑏) − 𝑥)) < 𝑦 ∧ (abs‘((𝐹‘𝑏) − 𝑅)) < 𝑦)) → ((𝐹‘𝑏) − 𝑥) ∈ ℂ)
197	196	abscld 15382	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((((((𝜑 ∧ 𝑥 ∈ ℂ) ∧ 𝑦 ∈ ℝ+) ∧ 𝑎 ∈ 𝐴) ∧ ((abs‘((𝐹‘𝑎) − 𝑥)) < 𝑦 ∧ (abs‘((𝐹‘𝑎) − 𝐿)) < 𝑦)) ∧ 𝑏 ∈ 𝐴) ∧ ((abs‘((𝐹‘𝑏) − 𝑥)) < 𝑦 ∧ (abs‘((𝐹‘𝑏) − 𝑅)) < 𝑦)) → (abs‘((𝐹‘𝑏) − 𝑥)) ∈ ℝ)
198	194, 197	readdcld 11242	. . . . . . . . . . . . . . . . . . 19 ⊢ (((((((𝜑 ∧ 𝑥 ∈ ℂ) ∧ 𝑦 ∈ ℝ+) ∧ 𝑎 ∈ 𝐴) ∧ ((abs‘((𝐹‘𝑎) − 𝑥)) < 𝑦 ∧ (abs‘((𝐹‘𝑎) − 𝐿)) < 𝑦)) ∧ 𝑏 ∈ 𝐴) ∧ ((abs‘((𝐹‘𝑏) − 𝑥)) < 𝑦 ∧ (abs‘((𝐹‘𝑏) − 𝑅)) < 𝑦)) → ((abs‘(𝑅 − (𝐹‘𝑏))) + (abs‘((𝐹‘𝑏) − 𝑥))) ∈ ℝ)
199		simp-4r 782	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((((((𝜑 ∧ 𝑥 ∈ ℂ) ∧ 𝑦 ∈ ℝ+) ∧ 𝑎 ∈ 𝐴) ∧ ((abs‘((𝐹‘𝑎) − 𝑥)) < 𝑦 ∧ (abs‘((𝐹‘𝑎) − 𝐿)) < 𝑦)) ∧ 𝑏 ∈ 𝐴) ∧ ((abs‘((𝐹‘𝑏) − 𝑥)) < 𝑦 ∧ (abs‘((𝐹‘𝑏) − 𝑅)) < 𝑦)) → 𝑎 ∈ 𝐴)
200	36	ffvelcdmda 7086	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝜑 ∧ 𝑎 ∈ 𝐴) → (𝐹‘𝑎) ∈ ℂ)
201	189, 199, 200	syl2anc 584	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((((((𝜑 ∧ 𝑥 ∈ ℂ) ∧ 𝑦 ∈ ℝ+) ∧ 𝑎 ∈ 𝐴) ∧ ((abs‘((𝐹‘𝑎) − 𝑥)) < 𝑦 ∧ (abs‘((𝐹‘𝑎) − 𝐿)) < 𝑦)) ∧ 𝑏 ∈ 𝐴) ∧ ((abs‘((𝐹‘𝑏) − 𝑥)) < 𝑦 ∧ (abs‘((𝐹‘𝑏) − 𝑅)) < 𝑦)) → (𝐹‘𝑎) ∈ ℂ)
202	195, 201	subcld 11570	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((((((𝜑 ∧ 𝑥 ∈ ℂ) ∧ 𝑦 ∈ ℝ+) ∧ 𝑎 ∈ 𝐴) ∧ ((abs‘((𝐹‘𝑎) − 𝑥)) < 𝑦 ∧ (abs‘((𝐹‘𝑎) − 𝐿)) < 𝑦)) ∧ 𝑏 ∈ 𝐴) ∧ ((abs‘((𝐹‘𝑏) − 𝑥)) < 𝑦 ∧ (abs‘((𝐹‘𝑏) − 𝑅)) < 𝑦)) → (𝑥 − (𝐹‘𝑎)) ∈ ℂ)
203	202	abscld 15382	. . . . . . . . . . . . . . . . . . 19 ⊢ (((((((𝜑 ∧ 𝑥 ∈ ℂ) ∧ 𝑦 ∈ ℝ+) ∧ 𝑎 ∈ 𝐴) ∧ ((abs‘((𝐹‘𝑎) − 𝑥)) < 𝑦 ∧ (abs‘((𝐹‘𝑎) − 𝐿)) < 𝑦)) ∧ 𝑏 ∈ 𝐴) ∧ ((abs‘((𝐹‘𝑏) − 𝑥)) < 𝑦 ∧ (abs‘((𝐹‘𝑏) − 𝑅)) < 𝑦)) → (abs‘(𝑥 − (𝐹‘𝑎))) ∈ ℝ)
204	198, 203	readdcld 11242	. . . . . . . . . . . . . . . . . 18 ⊢ (((((((𝜑 ∧ 𝑥 ∈ ℂ) ∧ 𝑦 ∈ ℝ+) ∧ 𝑎 ∈ 𝐴) ∧ ((abs‘((𝐹‘𝑎) − 𝑥)) < 𝑦 ∧ (abs‘((𝐹‘𝑎) − 𝐿)) < 𝑦)) ∧ 𝑏 ∈ 𝐴) ∧ ((abs‘((𝐹‘𝑏) − 𝑥)) < 𝑦 ∧ (abs‘((𝐹‘𝑏) − 𝑅)) < 𝑦)) → (((abs‘(𝑅 − (𝐹‘𝑏))) + (abs‘((𝐹‘𝑏) − 𝑥))) + (abs‘(𝑥 − (𝐹‘𝑎)))) ∈ ℝ)
205	201, 186	subcld 11570	. . . . . . . . . . . . . . . . . . 19 ⊢ (((((((𝜑 ∧ 𝑥 ∈ ℂ) ∧ 𝑦 ∈ ℝ+) ∧ 𝑎 ∈ 𝐴) ∧ ((abs‘((𝐹‘𝑎) − 𝑥)) < 𝑦 ∧ (abs‘((𝐹‘𝑎) − 𝐿)) < 𝑦)) ∧ 𝑏 ∈ 𝐴) ∧ ((abs‘((𝐹‘𝑏) − 𝑥)) < 𝑦 ∧ (abs‘((𝐹‘𝑏) − 𝑅)) < 𝑦)) → ((𝐹‘𝑎) − 𝐿) ∈ ℂ)
206	205	abscld 15382	. . . . . . . . . . . . . . . . . 18 ⊢ (((((((𝜑 ∧ 𝑥 ∈ ℂ) ∧ 𝑦 ∈ ℝ+) ∧ 𝑎 ∈ 𝐴) ∧ ((abs‘((𝐹‘𝑎) − 𝑥)) < 𝑦 ∧ (abs‘((𝐹‘𝑎) − 𝐿)) < 𝑦)) ∧ 𝑏 ∈ 𝐴) ∧ ((abs‘((𝐹‘𝑏) − 𝑥)) < 𝑦 ∧ (abs‘((𝐹‘𝑏) − 𝑅)) < 𝑦)) → (abs‘((𝐹‘𝑎) − 𝐿)) ∈ ℝ)
207	204, 206	readdcld 11242	. . . . . . . . . . . . . . . . 17 ⊢ (((((((𝜑 ∧ 𝑥 ∈ ℂ) ∧ 𝑦 ∈ ℝ+) ∧ 𝑎 ∈ 𝐴) ∧ ((abs‘((𝐹‘𝑎) − 𝑥)) < 𝑦 ∧ (abs‘((𝐹‘𝑎) − 𝐿)) < 𝑦)) ∧ 𝑏 ∈ 𝐴) ∧ ((abs‘((𝐹‘𝑏) − 𝑥)) < 𝑦 ∧ (abs‘((𝐹‘𝑏) − 𝑅)) < 𝑦)) → ((((abs‘(𝑅 − (𝐹‘𝑏))) + (abs‘((𝐹‘𝑏) − 𝑥))) + (abs‘(𝑥 − (𝐹‘𝑎)))) + (abs‘((𝐹‘𝑎) − 𝐿))) ∈ ℝ)
208	15	a1i 11	. . . . . . . . . . . . . . . . . 18 ⊢ (((((((𝜑 ∧ 𝑥 ∈ ℂ) ∧ 𝑦 ∈ ℝ+) ∧ 𝑎 ∈ 𝐴) ∧ ((abs‘((𝐹‘𝑎) − 𝑥)) < 𝑦 ∧ (abs‘((𝐹‘𝑎) − 𝐿)) < 𝑦)) ∧ 𝑏 ∈ 𝐴) ∧ ((abs‘((𝐹‘𝑏) − 𝑥)) < 𝑦 ∧ (abs‘((𝐹‘𝑏) − 𝑅)) < 𝑦)) → 4 ∈ ℝ)
209		rpre 12981	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑦 ∈ ℝ+ → 𝑦 ∈ ℝ)
210	209	ad5antlr 733	. . . . . . . . . . . . . . . . . 18 ⊢ (((((((𝜑 ∧ 𝑥 ∈ ℂ) ∧ 𝑦 ∈ ℝ+) ∧ 𝑎 ∈ 𝐴) ∧ ((abs‘((𝐹‘𝑎) − 𝑥)) < 𝑦 ∧ (abs‘((𝐹‘𝑎) − 𝐿)) < 𝑦)) ∧ 𝑏 ∈ 𝐴) ∧ ((abs‘((𝐹‘𝑏) − 𝑥)) < 𝑦 ∧ (abs‘((𝐹‘𝑏) − 𝑅)) < 𝑦)) → 𝑦 ∈ ℝ)
211	208, 210	remulcld 11243	. . . . . . . . . . . . . . . . 17 ⊢ (((((((𝜑 ∧ 𝑥 ∈ ℂ) ∧ 𝑦 ∈ ℝ+) ∧ 𝑎 ∈ 𝐴) ∧ ((abs‘((𝐹‘𝑎) − 𝑥)) < 𝑦 ∧ (abs‘((𝐹‘𝑎) − 𝐿)) < 𝑦)) ∧ 𝑏 ∈ 𝐴) ∧ ((abs‘((𝐹‘𝑏) − 𝑥)) < 𝑦 ∧ (abs‘((𝐹‘𝑏) − 𝑅)) < 𝑦)) → (4 · 𝑦) ∈ ℝ)
212	185, 192, 195, 201, 186	absnpncan3d 44007	. . . . . . . . . . . . . . . . 17 ⊢ (((((((𝜑 ∧ 𝑥 ∈ ℂ) ∧ 𝑦 ∈ ℝ+) ∧ 𝑎 ∈ 𝐴) ∧ ((abs‘((𝐹‘𝑎) − 𝑥)) < 𝑦 ∧ (abs‘((𝐹‘𝑎) − 𝐿)) < 𝑦)) ∧ 𝑏 ∈ 𝐴) ∧ ((abs‘((𝐹‘𝑏) − 𝑥)) < 𝑦 ∧ (abs‘((𝐹‘𝑏) − 𝑅)) < 𝑦)) → (abs‘(𝑅 − 𝐿)) ≤ ((((abs‘(𝑅 − (𝐹‘𝑏))) + (abs‘((𝐹‘𝑏) − 𝑥))) + (abs‘(𝑥 − (𝐹‘𝑎)))) + (abs‘((𝐹‘𝑎) − 𝐿))))
213	185, 192	abssubd 15399	. . . . . . . . . . . . . . . . . . 19 ⊢ (((((((𝜑 ∧ 𝑥 ∈ ℂ) ∧ 𝑦 ∈ ℝ+) ∧ 𝑎 ∈ 𝐴) ∧ ((abs‘((𝐹‘𝑎) − 𝑥)) < 𝑦 ∧ (abs‘((𝐹‘𝑎) − 𝐿)) < 𝑦)) ∧ 𝑏 ∈ 𝐴) ∧ ((abs‘((𝐹‘𝑏) − 𝑥)) < 𝑦 ∧ (abs‘((𝐹‘𝑏) − 𝑅)) < 𝑦)) → (abs‘(𝑅 − (𝐹‘𝑏))) = (abs‘((𝐹‘𝑏) − 𝑅)))
214		simprr 771	. . . . . . . . . . . . . . . . . . 19 ⊢ (((((((𝜑 ∧ 𝑥 ∈ ℂ) ∧ 𝑦 ∈ ℝ+) ∧ 𝑎 ∈ 𝐴) ∧ ((abs‘((𝐹‘𝑎) − 𝑥)) < 𝑦 ∧ (abs‘((𝐹‘𝑎) − 𝐿)) < 𝑦)) ∧ 𝑏 ∈ 𝐴) ∧ ((abs‘((𝐹‘𝑏) − 𝑥)) < 𝑦 ∧ (abs‘((𝐹‘𝑏) − 𝑅)) < 𝑦)) → (abs‘((𝐹‘𝑏) − 𝑅)) < 𝑦)
215	213, 214	eqbrtrd 5170	. . . . . . . . . . . . . . . . . 18 ⊢ (((((((𝜑 ∧ 𝑥 ∈ ℂ) ∧ 𝑦 ∈ ℝ+) ∧ 𝑎 ∈ 𝐴) ∧ ((abs‘((𝐹‘𝑎) − 𝑥)) < 𝑦 ∧ (abs‘((𝐹‘𝑎) − 𝐿)) < 𝑦)) ∧ 𝑏 ∈ 𝐴) ∧ ((abs‘((𝐹‘𝑏) − 𝑥)) < 𝑦 ∧ (abs‘((𝐹‘𝑏) − 𝑅)) < 𝑦)) → (abs‘(𝑅 − (𝐹‘𝑏))) < 𝑦)
216		simprl 769	. . . . . . . . . . . . . . . . . 18 ⊢ (((((((𝜑 ∧ 𝑥 ∈ ℂ) ∧ 𝑦 ∈ ℝ+) ∧ 𝑎 ∈ 𝐴) ∧ ((abs‘((𝐹‘𝑎) − 𝑥)) < 𝑦 ∧ (abs‘((𝐹‘𝑎) − 𝐿)) < 𝑦)) ∧ 𝑏 ∈ 𝐴) ∧ ((abs‘((𝐹‘𝑏) − 𝑥)) < 𝑦 ∧ (abs‘((𝐹‘𝑏) − 𝑅)) < 𝑦)) → (abs‘((𝐹‘𝑏) − 𝑥)) < 𝑦)
217		simp-5r 784	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((((𝜑 ∧ 𝑥 ∈ ℂ) ∧ 𝑦 ∈ ℝ+) ∧ 𝑎 ∈ 𝐴) ∧ ((abs‘((𝐹‘𝑎) − 𝑥)) < 𝑦 ∧ (abs‘((𝐹‘𝑎) − 𝐿)) < 𝑦)) ∧ 𝑏 ∈ 𝐴) → 𝑥 ∈ ℂ)
218	200	ad5ant14 756	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((((𝜑 ∧ 𝑥 ∈ ℂ) ∧ 𝑦 ∈ ℝ+) ∧ 𝑎 ∈ 𝐴) ∧ ((abs‘((𝐹‘𝑎) − 𝑥)) < 𝑦 ∧ (abs‘((𝐹‘𝑎) − 𝐿)) < 𝑦)) → (𝐹‘𝑎) ∈ ℂ)
219	218	adantr 481	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((((𝜑 ∧ 𝑥 ∈ ℂ) ∧ 𝑦 ∈ ℝ+) ∧ 𝑎 ∈ 𝐴) ∧ ((abs‘((𝐹‘𝑎) − 𝑥)) < 𝑦 ∧ (abs‘((𝐹‘𝑎) − 𝐿)) < 𝑦)) ∧ 𝑏 ∈ 𝐴) → (𝐹‘𝑎) ∈ ℂ)
220	217, 219	abssubd 15399	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((((𝜑 ∧ 𝑥 ∈ ℂ) ∧ 𝑦 ∈ ℝ+) ∧ 𝑎 ∈ 𝐴) ∧ ((abs‘((𝐹‘𝑎) − 𝑥)) < 𝑦 ∧ (abs‘((𝐹‘𝑎) − 𝐿)) < 𝑦)) ∧ 𝑏 ∈ 𝐴) → (abs‘(𝑥 − (𝐹‘𝑎))) = (abs‘((𝐹‘𝑎) − 𝑥)))
221		simplrl 775	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((((𝜑 ∧ 𝑥 ∈ ℂ) ∧ 𝑦 ∈ ℝ+) ∧ 𝑎 ∈ 𝐴) ∧ ((abs‘((𝐹‘𝑎) − 𝑥)) < 𝑦 ∧ (abs‘((𝐹‘𝑎) − 𝐿)) < 𝑦)) ∧ 𝑏 ∈ 𝐴) → (abs‘((𝐹‘𝑎) − 𝑥)) < 𝑦)
222	220, 221	eqbrtrd 5170	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((((𝜑 ∧ 𝑥 ∈ ℂ) ∧ 𝑦 ∈ ℝ+) ∧ 𝑎 ∈ 𝐴) ∧ ((abs‘((𝐹‘𝑎) − 𝑥)) < 𝑦 ∧ (abs‘((𝐹‘𝑎) − 𝐿)) < 𝑦)) ∧ 𝑏 ∈ 𝐴) → (abs‘(𝑥 − (𝐹‘𝑎))) < 𝑦)
223	222	adantr 481	. . . . . . . . . . . . . . . . . 18 ⊢ (((((((𝜑 ∧ 𝑥 ∈ ℂ) ∧ 𝑦 ∈ ℝ+) ∧ 𝑎 ∈ 𝐴) ∧ ((abs‘((𝐹‘𝑎) − 𝑥)) < 𝑦 ∧ (abs‘((𝐹‘𝑎) − 𝐿)) < 𝑦)) ∧ 𝑏 ∈ 𝐴) ∧ ((abs‘((𝐹‘𝑏) − 𝑥)) < 𝑦 ∧ (abs‘((𝐹‘𝑏) − 𝑅)) < 𝑦)) → (abs‘(𝑥 − (𝐹‘𝑎))) < 𝑦)
224		simplrr 776	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((((𝜑 ∧ 𝑥 ∈ ℂ) ∧ 𝑦 ∈ ℝ+) ∧ 𝑎 ∈ 𝐴) ∧ ((abs‘((𝐹‘𝑎) − 𝑥)) < 𝑦 ∧ (abs‘((𝐹‘𝑎) − 𝐿)) < 𝑦)) ∧ 𝑏 ∈ 𝐴) → (abs‘((𝐹‘𝑎) − 𝐿)) < 𝑦)
225	224	adantr 481	. . . . . . . . . . . . . . . . . 18 ⊢ (((((((𝜑 ∧ 𝑥 ∈ ℂ) ∧ 𝑦 ∈ ℝ+) ∧ 𝑎 ∈ 𝐴) ∧ ((abs‘((𝐹‘𝑎) − 𝑥)) < 𝑦 ∧ (abs‘((𝐹‘𝑎) − 𝐿)) < 𝑦)) ∧ 𝑏 ∈ 𝐴) ∧ ((abs‘((𝐹‘𝑏) − 𝑥)) < 𝑦 ∧ (abs‘((𝐹‘𝑏) − 𝑅)) < 𝑦)) → (abs‘((𝐹‘𝑎) − 𝐿)) < 𝑦)
226	194, 197, 203, 206, 210, 215, 216, 223, 225	lt4addmuld 44006	. . . . . . . . . . . . . . . . 17 ⊢ (((((((𝜑 ∧ 𝑥 ∈ ℂ) ∧ 𝑦 ∈ ℝ+) ∧ 𝑎 ∈ 𝐴) ∧ ((abs‘((𝐹‘𝑎) − 𝑥)) < 𝑦 ∧ (abs‘((𝐹‘𝑎) − 𝐿)) < 𝑦)) ∧ 𝑏 ∈ 𝐴) ∧ ((abs‘((𝐹‘𝑏) − 𝑥)) < 𝑦 ∧ (abs‘((𝐹‘𝑏) − 𝑅)) < 𝑦)) → ((((abs‘(𝑅 − (𝐹‘𝑏))) + (abs‘((𝐹‘𝑏) − 𝑥))) + (abs‘(𝑥 − (𝐹‘𝑎)))) + (abs‘((𝐹‘𝑎) − 𝐿))) < (4 · 𝑦))
227	188, 207, 211, 212, 226	lelttrd 11371	. . . . . . . . . . . . . . . 16 ⊢ (((((((𝜑 ∧ 𝑥 ∈ ℂ) ∧ 𝑦 ∈ ℝ+) ∧ 𝑎 ∈ 𝐴) ∧ ((abs‘((𝐹‘𝑎) − 𝑥)) < 𝑦 ∧ (abs‘((𝐹‘𝑎) − 𝐿)) < 𝑦)) ∧ 𝑏 ∈ 𝐴) ∧ ((abs‘((𝐹‘𝑏) − 𝑥)) < 𝑦 ∧ (abs‘((𝐹‘𝑏) − 𝑅)) < 𝑦)) → (abs‘(𝑅 − 𝐿)) < (4 · 𝑦))
228	227	ex 413	. . . . . . . . . . . . . . 15 ⊢ ((((((𝜑 ∧ 𝑥 ∈ ℂ) ∧ 𝑦 ∈ ℝ+) ∧ 𝑎 ∈ 𝐴) ∧ ((abs‘((𝐹‘𝑎) − 𝑥)) < 𝑦 ∧ (abs‘((𝐹‘𝑎) − 𝐿)) < 𝑦)) ∧ 𝑏 ∈ 𝐴) → (((abs‘((𝐹‘𝑏) − 𝑥)) < 𝑦 ∧ (abs‘((𝐹‘𝑏) − 𝑅)) < 𝑦) → (abs‘(𝑅 − 𝐿)) < (4 · 𝑦)))
229	228	adantl3r 748	. . . . . . . . . . . . . 14 ⊢ (((((((𝜑 ∧ 𝑥 ∈ ℂ) ∧ 𝑦 ∈ ℝ+) ∧ ∃𝑧 ∈ ℝ+ ∀𝑤 ∈ 𝐴 ((𝑤 ≠ 𝐵 ∧ (abs‘(𝑤 − 𝐵)) < 𝑧) → (abs‘((𝐹‘𝑤) − 𝑥)) < 𝑦)) ∧ 𝑎 ∈ 𝐴) ∧ ((abs‘((𝐹‘𝑎) − 𝑥)) < 𝑦 ∧ (abs‘((𝐹‘𝑎) − 𝐿)) < 𝑦)) ∧ 𝑏 ∈ 𝐴) → (((abs‘((𝐹‘𝑏) − 𝑥)) < 𝑦 ∧ (abs‘((𝐹‘𝑏) − 𝑅)) < 𝑦) → (abs‘(𝑅 − 𝐿)) < (4 · 𝑦)))
230	229	reximdva 3168	. . . . . . . . . . . . 13 ⊢ ((((((𝜑 ∧ 𝑥 ∈ ℂ) ∧ 𝑦 ∈ ℝ+) ∧ ∃𝑧 ∈ ℝ+ ∀𝑤 ∈ 𝐴 ((𝑤 ≠ 𝐵 ∧ (abs‘(𝑤 − 𝐵)) < 𝑧) → (abs‘((𝐹‘𝑤) − 𝑥)) < 𝑦)) ∧ 𝑎 ∈ 𝐴) ∧ ((abs‘((𝐹‘𝑎) − 𝑥)) < 𝑦 ∧ (abs‘((𝐹‘𝑎) − 𝐿)) < 𝑦)) → (∃𝑏 ∈ 𝐴 ((abs‘((𝐹‘𝑏) − 𝑥)) < 𝑦 ∧ (abs‘((𝐹‘𝑏) − 𝑅)) < 𝑦) → ∃𝑏 ∈ 𝐴 (abs‘(𝑅 − 𝐿)) < (4 · 𝑦)))
231	184, 230	mpd 15	. . . . . . . . . . . 12 ⊢ ((((((𝜑 ∧ 𝑥 ∈ ℂ) ∧ 𝑦 ∈ ℝ+) ∧ ∃𝑧 ∈ ℝ+ ∀𝑤 ∈ 𝐴 ((𝑤 ≠ 𝐵 ∧ (abs‘(𝑤 − 𝐵)) < 𝑧) → (abs‘((𝐹‘𝑤) − 𝑥)) < 𝑦)) ∧ 𝑎 ∈ 𝐴) ∧ ((abs‘((𝐹‘𝑎) − 𝑥)) < 𝑦 ∧ (abs‘((𝐹‘𝑎) − 𝐿)) < 𝑦)) → ∃𝑏 ∈ 𝐴 (abs‘(𝑅 − 𝐿)) < (4 · 𝑦))
232		fresin 6760	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝐹:𝐴⟶ℂ → (𝐹 ↾ (-∞(,)𝐵)):(𝐴 ∩ (-∞(,)𝐵))⟶ℂ)
233	36, 232	syl 17	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝜑 → (𝐹 ↾ (-∞(,)𝐵)):(𝐴 ∩ (-∞(,)𝐵))⟶ℂ)
234		ioosscn 13385	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (-∞(,)𝐵) ⊆ ℂ
235	46, 234	sstri 3991	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝐴 ∩ (-∞(,)𝐵)) ⊆ ℂ
236	235	a1i 11	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝜑 → (𝐴 ∩ (-∞(,)𝐵)) ⊆ ℂ)
237	233, 236, 56	ellimc3 25395	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝜑 → (𝐿 ∈ ((𝐹 ↾ (-∞(,)𝐵)) limℂ 𝐵) ↔ (𝐿 ∈ ℂ ∧ ∀𝑦 ∈ ℝ+ ∃𝑣 ∈ ℝ+ ∀𝑤 ∈ (𝐴 ∩ (-∞(,)𝐵))((𝑤 ≠ 𝐵 ∧ (abs‘(𝑤 − 𝐵)) < 𝑣) → (abs‘(((𝐹 ↾ (-∞(,)𝐵))‘𝑤) − 𝐿)) < 𝑦))))
238	6, 237	mpbid 231	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → (𝐿 ∈ ℂ ∧ ∀𝑦 ∈ ℝ+ ∃𝑣 ∈ ℝ+ ∀𝑤 ∈ (𝐴 ∩ (-∞(,)𝐵))((𝑤 ≠ 𝐵 ∧ (abs‘(𝑤 − 𝐵)) < 𝑣) → (abs‘(((𝐹 ↾ (-∞(,)𝐵))‘𝑤) − 𝐿)) < 𝑦)))
239	238	simprd 496	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → ∀𝑦 ∈ ℝ+ ∃𝑣 ∈ ℝ+ ∀𝑤 ∈ (𝐴 ∩ (-∞(,)𝐵))((𝑤 ≠ 𝐵 ∧ (abs‘(𝑤 − 𝐵)) < 𝑣) → (abs‘(((𝐹 ↾ (-∞(,)𝐵))‘𝑤) − 𝐿)) < 𝑦))
240	239	r19.21bi 3248	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑦 ∈ ℝ+) → ∃𝑣 ∈ ℝ+ ∀𝑤 ∈ (𝐴 ∩ (-∞(,)𝐵))((𝑤 ≠ 𝐵 ∧ (abs‘(𝑤 − 𝐵)) < 𝑣) → (abs‘(((𝐹 ↾ (-∞(,)𝐵))‘𝑤) − 𝐿)) < 𝑦))
241	240	3ad2ant1 1133	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑦 ∈ ℝ+) ∧ 𝑧 ∈ ℝ+ ∧ ∀𝑤 ∈ 𝐴 ((𝑤 ≠ 𝐵 ∧ (abs‘(𝑤 − 𝐵)) < 𝑧) → (abs‘((𝐹‘𝑤) − 𝑥)) < 𝑦)) → ∃𝑣 ∈ ℝ+ ∀𝑤 ∈ (𝐴 ∩ (-∞(,)𝐵))((𝑤 ≠ 𝐵 ∧ (abs‘(𝑤 − 𝐵)) < 𝑣) → (abs‘(((𝐹 ↾ (-∞(,)𝐵))‘𝑤) − 𝐿)) < 𝑦))
242		simp11l 1284	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((𝜑 ∧ 𝑦 ∈ ℝ+) ∧ 𝑧 ∈ ℝ+ ∧ ∀𝑤 ∈ 𝐴 ((𝑤 ≠ 𝐵 ∧ (abs‘(𝑤 − 𝐵)) < 𝑧) → (abs‘((𝐹‘𝑤) − 𝑥)) < 𝑦)) ∧ 𝑣 ∈ ℝ+ ∧ ∀𝑤 ∈ (𝐴 ∩ (-∞(,)𝐵))((𝑤 ≠ 𝐵 ∧ (abs‘(𝑤 − 𝐵)) < 𝑣) → (abs‘(((𝐹 ↾ (-∞(,)𝐵))‘𝑤) − 𝐿)) < 𝑦)) → 𝜑)
243		simp12 1204	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((𝜑 ∧ 𝑦 ∈ ℝ+) ∧ 𝑧 ∈ ℝ+ ∧ ∀𝑤 ∈ 𝐴 ((𝑤 ≠ 𝐵 ∧ (abs‘(𝑤 − 𝐵)) < 𝑧) → (abs‘((𝐹‘𝑤) − 𝑥)) < 𝑦)) ∧ 𝑣 ∈ ℝ+ ∧ ∀𝑤 ∈ (𝐴 ∩ (-∞(,)𝐵))((𝑤 ≠ 𝐵 ∧ (abs‘(𝑤 − 𝐵)) < 𝑣) → (abs‘(((𝐹 ↾ (-∞(,)𝐵))‘𝑤) − 𝐿)) < 𝑦)) → 𝑧 ∈ ℝ+)
244		simp2 1137	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((𝜑 ∧ 𝑦 ∈ ℝ+) ∧ 𝑧 ∈ ℝ+ ∧ ∀𝑤 ∈ 𝐴 ((𝑤 ≠ 𝐵 ∧ (abs‘(𝑤 − 𝐵)) < 𝑧) → (abs‘((𝐹‘𝑤) − 𝑥)) < 𝑦)) ∧ 𝑣 ∈ ℝ+ ∧ ∀𝑤 ∈ (𝐴 ∩ (-∞(,)𝐵))((𝑤 ≠ 𝐵 ∧ (abs‘(𝑤 − 𝐵)) < 𝑣) → (abs‘(((𝐹 ↾ (-∞(,)𝐵))‘𝑤) − 𝐿)) < 𝑦)) → 𝑣 ∈ ℝ+)
245		breq2 5152	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑢 = if(𝑧 ≤ 𝑣, 𝑧, 𝑣) → ((abs‘(𝑎 − 𝐵)) < 𝑢 ↔ (abs‘(𝑎 − 𝐵)) < if(𝑧 ≤ 𝑣, 𝑧, 𝑣)))
246	245	rexbidv 3178	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑢 = if(𝑧 ≤ 𝑣, 𝑧, 𝑣) → (∃𝑎 ∈ ((𝐴 ∩ (-∞(,)𝐵)) ∖ {𝐵})(abs‘(𝑎 − 𝐵)) < 𝑢 ↔ ∃𝑎 ∈ ((𝐴 ∩ (-∞(,)𝐵)) ∖ {𝐵})(abs‘(𝑎 − 𝐵)) < if(𝑧 ≤ 𝑣, 𝑧, 𝑣)))
247		inss1 4228	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (((limPt‘𝐾)‘(𝐴 ∩ (-∞(,)𝐵))) ∩ ℝ) ⊆ ((limPt‘𝐾)‘(𝐴 ∩ (-∞(,)𝐵)))
248	247	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝜑 → (((limPt‘𝐾)‘(𝐴 ∩ (-∞(,)𝐵))) ∩ ℝ) ⊆ ((limPt‘𝐾)‘(𝐴 ∩ (-∞(,)𝐵))))
249	48	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (𝜑 → (𝐴 ∩ (-∞(,)𝐵)) ⊆ ℝ)
250	79, 81	restlp 22686	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ((𝐾 ∈ Top ∧ ℝ ⊆ ℂ ∧ (𝐴 ∩ (-∞(,)𝐵)) ⊆ ℝ) → ((limPt‘𝐽)‘(𝐴 ∩ (-∞(,)𝐵))) = (((limPt‘𝐾)‘(𝐴 ∩ (-∞(,)𝐵))) ∩ ℝ))
251	71, 73, 249, 250	syl3anc 1371	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝜑 → ((limPt‘𝐽)‘(𝐴 ∩ (-∞(,)𝐵))) = (((limPt‘𝐾)‘(𝐴 ∩ (-∞(,)𝐵))) ∩ ℝ))
252	85	fveq1i 6892	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ((limPt‘(TopOpen‘ℂfld))‘(𝐴 ∩ (-∞(,)𝐵))) = ((limPt‘𝐾)‘(𝐴 ∩ (-∞(,)𝐵)))
253	252	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝜑 → ((limPt‘(TopOpen‘ℂfld))‘(𝐴 ∩ (-∞(,)𝐵))) = ((limPt‘𝐾)‘(𝐴 ∩ (-∞(,)𝐵))))
254	248, 251, 253	3sstr4d 4029	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝜑 → ((limPt‘𝐽)‘(𝐴 ∩ (-∞(,)𝐵))) ⊆ ((limPt‘(TopOpen‘ℂfld))‘(𝐴 ∩ (-∞(,)𝐵))))
255	254, 54	sseldd 3983	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝜑 → 𝐵 ∈ ((limPt‘(TopOpen‘ℂfld))‘(𝐴 ∩ (-∞(,)𝐵))))
256	236, 56	islpcn 44345	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝜑 → (𝐵 ∈ ((limPt‘(TopOpen‘ℂfld))‘(𝐴 ∩ (-∞(,)𝐵))) ↔ ∀𝑢 ∈ ℝ+ ∃𝑎 ∈ ((𝐴 ∩ (-∞(,)𝐵)) ∖ {𝐵})(abs‘(𝑎 − 𝐵)) < 𝑢))
257	255, 256	mpbid 231	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝜑 → ∀𝑢 ∈ ℝ+ ∃𝑎 ∈ ((𝐴 ∩ (-∞(,)𝐵)) ∖ {𝐵})(abs‘(𝑎 − 𝐵)) < 𝑢)
258	257	3ad2ant1 1133	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝜑 ∧ 𝑧 ∈ ℝ+ ∧ 𝑣 ∈ ℝ+) → ∀𝑢 ∈ ℝ+ ∃𝑎 ∈ ((𝐴 ∩ (-∞(,)𝐵)) ∖ {𝐵})(abs‘(𝑎 − 𝐵)) < 𝑢)
259	246, 258, 95	rspcdva 3613	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝜑 ∧ 𝑧 ∈ ℝ+ ∧ 𝑣 ∈ ℝ+) → ∃𝑎 ∈ ((𝐴 ∩ (-∞(,)𝐵)) ∖ {𝐵})(abs‘(𝑎 − 𝐵)) < if(𝑧 ≤ 𝑣, 𝑧, 𝑣))
260		eldifi 4126	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑎 ∈ ((𝐴 ∩ (-∞(,)𝐵)) ∖ {𝐵}) → 𝑎 ∈ (𝐴 ∩ (-∞(,)𝐵)))
261	48, 260	sselid 3980	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑎 ∈ ((𝐴 ∩ (-∞(,)𝐵)) ∖ {𝐵}) → 𝑎 ∈ ℝ)
262	73	sselda 3982	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ ((𝜑 ∧ 𝑎 ∈ ℝ) → 𝑎 ∈ ℂ)
263	56	adantr 481	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ ((𝜑 ∧ 𝑎 ∈ ℝ) → 𝐵 ∈ ℂ)
264	262, 263	subcld 11570	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ ((𝜑 ∧ 𝑎 ∈ ℝ) → (𝑎 − 𝐵) ∈ ℂ)
265	264	abscld 15382	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ ((𝜑 ∧ 𝑎 ∈ ℝ) → (abs‘(𝑎 − 𝐵)) ∈ ℝ)
266	265	3ad2antl1 1185	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (((𝜑 ∧ 𝑧 ∈ ℝ+ ∧ 𝑣 ∈ ℝ+) ∧ 𝑎 ∈ ℝ) → (abs‘(𝑎 − 𝐵)) ∈ ℝ)
267	266	adantr 481	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((((𝜑 ∧ 𝑧 ∈ ℝ+ ∧ 𝑣 ∈ ℝ+) ∧ 𝑎 ∈ ℝ) ∧ (abs‘(𝑎 − 𝐵)) < if(𝑧 ≤ 𝑣, 𝑧, 𝑣)) → (abs‘(𝑎 − 𝐵)) ∈ ℝ)
268	105	ad2antrr 724	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((((𝜑 ∧ 𝑧 ∈ ℝ+ ∧ 𝑣 ∈ ℝ+) ∧ 𝑎 ∈ ℝ) ∧ (abs‘(𝑎 − 𝐵)) < if(𝑧 ≤ 𝑣, 𝑧, 𝑣)) → if(𝑧 ≤ 𝑣, 𝑧, 𝑣) ∈ ℝ)
269	108	ad2antrr 724	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((((𝜑 ∧ 𝑧 ∈ ℝ+ ∧ 𝑣 ∈ ℝ+) ∧ 𝑎 ∈ ℝ) ∧ (abs‘(𝑎 − 𝐵)) < if(𝑧 ≤ 𝑣, 𝑧, 𝑣)) → 𝑧 ∈ ℝ)
270		simpr 485	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((((𝜑 ∧ 𝑧 ∈ ℝ+ ∧ 𝑣 ∈ ℝ+) ∧ 𝑎 ∈ ℝ) ∧ (abs‘(𝑎 − 𝐵)) < if(𝑧 ≤ 𝑣, 𝑧, 𝑣)) → (abs‘(𝑎 − 𝐵)) < if(𝑧 ≤ 𝑣, 𝑧, 𝑣))
271	114	ad2antrr 724	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((((𝜑 ∧ 𝑧 ∈ ℝ+ ∧ 𝑣 ∈ ℝ+) ∧ 𝑎 ∈ ℝ) ∧ (abs‘(𝑎 − 𝐵)) < if(𝑧 ≤ 𝑣, 𝑧, 𝑣)) → if(𝑧 ≤ 𝑣, 𝑧, 𝑣) ≤ 𝑧)
272	267, 268, 269, 270, 271	ltletrd 11373	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((((𝜑 ∧ 𝑧 ∈ ℝ+ ∧ 𝑣 ∈ ℝ+) ∧ 𝑎 ∈ ℝ) ∧ (abs‘(𝑎 − 𝐵)) < if(𝑧 ≤ 𝑣, 𝑧, 𝑣)) → (abs‘(𝑎 − 𝐵)) < 𝑧)
273	117	ad2antrr 724	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((((𝜑 ∧ 𝑧 ∈ ℝ+ ∧ 𝑣 ∈ ℝ+) ∧ 𝑎 ∈ ℝ) ∧ (abs‘(𝑎 − 𝐵)) < if(𝑧 ≤ 𝑣, 𝑧, 𝑣)) → 𝑣 ∈ ℝ)
274		min2 13168	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ ((𝑧 ∈ ℝ ∧ 𝑣 ∈ ℝ) → if(𝑧 ≤ 𝑣, 𝑧, 𝑣) ≤ 𝑣)
275	107, 111, 274	syl2an 596	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ ((𝑧 ∈ ℝ+ ∧ 𝑣 ∈ ℝ+) → if(𝑧 ≤ 𝑣, 𝑧, 𝑣) ≤ 𝑣)
276	275	3adant1 1130	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ((𝜑 ∧ 𝑧 ∈ ℝ+ ∧ 𝑣 ∈ ℝ+) → if(𝑧 ≤ 𝑣, 𝑧, 𝑣) ≤ 𝑣)
277	276	ad2antrr 724	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((((𝜑 ∧ 𝑧 ∈ ℝ+ ∧ 𝑣 ∈ ℝ+) ∧ 𝑎 ∈ ℝ) ∧ (abs‘(𝑎 − 𝐵)) < if(𝑧 ≤ 𝑣, 𝑧, 𝑣)) → if(𝑧 ≤ 𝑣, 𝑧, 𝑣) ≤ 𝑣)
278	267, 268, 273, 270, 277	ltletrd 11373	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((((𝜑 ∧ 𝑧 ∈ ℝ+ ∧ 𝑣 ∈ ℝ+) ∧ 𝑎 ∈ ℝ) ∧ (abs‘(𝑎 − 𝐵)) < if(𝑧 ≤ 𝑣, 𝑧, 𝑣)) → (abs‘(𝑎 − 𝐵)) < 𝑣)
279	272, 278	jca 512	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((((𝜑 ∧ 𝑧 ∈ ℝ+ ∧ 𝑣 ∈ ℝ+) ∧ 𝑎 ∈ ℝ) ∧ (abs‘(𝑎 − 𝐵)) < if(𝑧 ≤ 𝑣, 𝑧, 𝑣)) → ((abs‘(𝑎 − 𝐵)) < 𝑧 ∧ (abs‘(𝑎 − 𝐵)) < 𝑣))
280	279	ex 413	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((𝜑 ∧ 𝑧 ∈ ℝ+ ∧ 𝑣 ∈ ℝ+) ∧ 𝑎 ∈ ℝ) → ((abs‘(𝑎 − 𝐵)) < if(𝑧 ≤ 𝑣, 𝑧, 𝑣) → ((abs‘(𝑎 − 𝐵)) < 𝑧 ∧ (abs‘(𝑎 − 𝐵)) < 𝑣)))
281	261, 280	sylan2 593	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((𝜑 ∧ 𝑧 ∈ ℝ+ ∧ 𝑣 ∈ ℝ+) ∧ 𝑎 ∈ ((𝐴 ∩ (-∞(,)𝐵)) ∖ {𝐵})) → ((abs‘(𝑎 − 𝐵)) < if(𝑧 ≤ 𝑣, 𝑧, 𝑣) → ((abs‘(𝑎 − 𝐵)) < 𝑧 ∧ (abs‘(𝑎 − 𝐵)) < 𝑣)))
282	281	reximdva 3168	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝜑 ∧ 𝑧 ∈ ℝ+ ∧ 𝑣 ∈ ℝ+) → (∃𝑎 ∈ ((𝐴 ∩ (-∞(,)𝐵)) ∖ {𝐵})(abs‘(𝑎 − 𝐵)) < if(𝑧 ≤ 𝑣, 𝑧, 𝑣) → ∃𝑎 ∈ ((𝐴 ∩ (-∞(,)𝐵)) ∖ {𝐵})((abs‘(𝑎 − 𝐵)) < 𝑧 ∧ (abs‘(𝑎 − 𝐵)) < 𝑣)))
283	259, 282	mpd 15	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝜑 ∧ 𝑧 ∈ ℝ+ ∧ 𝑣 ∈ ℝ+) → ∃𝑎 ∈ ((𝐴 ∩ (-∞(,)𝐵)) ∖ {𝐵})((abs‘(𝑎 − 𝐵)) < 𝑧 ∧ (abs‘(𝑎 − 𝐵)) < 𝑣))
284	242, 243, 244, 283	syl3anc 1371	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝜑 ∧ 𝑦 ∈ ℝ+) ∧ 𝑧 ∈ ℝ+ ∧ ∀𝑤 ∈ 𝐴 ((𝑤 ≠ 𝐵 ∧ (abs‘(𝑤 − 𝐵)) < 𝑧) → (abs‘((𝐹‘𝑤) − 𝑥)) < 𝑦)) ∧ 𝑣 ∈ ℝ+ ∧ ∀𝑤 ∈ (𝐴 ∩ (-∞(,)𝐵))((𝑤 ≠ 𝐵 ∧ (abs‘(𝑤 − 𝐵)) < 𝑣) → (abs‘(((𝐹 ↾ (-∞(,)𝐵))‘𝑤) − 𝐿)) < 𝑦)) → ∃𝑎 ∈ ((𝐴 ∩ (-∞(,)𝐵)) ∖ {𝐵})((abs‘(𝑎 − 𝐵)) < 𝑧 ∧ (abs‘(𝑎 − 𝐵)) < 𝑣))
285		nfv 1917	. . . . . . . . . . . . . . . . . . . . 21 ⊢ Ⅎ𝑎(((𝜑 ∧ 𝑦 ∈ ℝ+) ∧ 𝑧 ∈ ℝ+ ∧ ∀𝑤 ∈ 𝐴 ((𝑤 ≠ 𝐵 ∧ (abs‘(𝑤 − 𝐵)) < 𝑧) → (abs‘((𝐹‘𝑤) − 𝑥)) < 𝑦)) ∧ 𝑣 ∈ ℝ+ ∧ ∀𝑤 ∈ (𝐴 ∩ (-∞(,)𝐵))((𝑤 ≠ 𝐵 ∧ (abs‘(𝑤 − 𝐵)) < 𝑣) → (abs‘(((𝐹 ↾ (-∞(,)𝐵))‘𝑤) − 𝐿)) < 𝑦))
286		nfre1 3282	. . . . . . . . . . . . . . . . . . . . 21 ⊢ Ⅎ𝑎∃𝑎 ∈ 𝐴 ((abs‘((𝐹‘𝑎) − 𝑥)) < 𝑦 ∧ (abs‘((𝐹‘𝑎) − 𝐿)) < 𝑦)
287	260	elin1d 4198	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑎 ∈ ((𝐴 ∩ (-∞(,)𝐵)) ∖ {𝐵}) → 𝑎 ∈ 𝐴)
288	287	3ad2ant2 1134	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((((𝜑 ∧ 𝑦 ∈ ℝ+) ∧ 𝑧 ∈ ℝ+ ∧ ∀𝑤 ∈ 𝐴 ((𝑤 ≠ 𝐵 ∧ (abs‘(𝑤 − 𝐵)) < 𝑧) → (abs‘((𝐹‘𝑤) − 𝑥)) < 𝑦)) ∧ 𝑣 ∈ ℝ+ ∧ ∀𝑤 ∈ (𝐴 ∩ (-∞(,)𝐵))((𝑤 ≠ 𝐵 ∧ (abs‘(𝑤 − 𝐵)) < 𝑣) → (abs‘(((𝐹 ↾ (-∞(,)𝐵))‘𝑤) − 𝐿)) < 𝑦)) ∧ 𝑎 ∈ ((𝐴 ∩ (-∞(,)𝐵)) ∖ {𝐵}) ∧ ((abs‘(𝑎 − 𝐵)) < 𝑧 ∧ (abs‘(𝑎 − 𝐵)) < 𝑣)) → 𝑎 ∈ 𝐴)
289		simp113 1304	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((((𝜑 ∧ 𝑦 ∈ ℝ+) ∧ 𝑧 ∈ ℝ+ ∧ ∀𝑤 ∈ 𝐴 ((𝑤 ≠ 𝐵 ∧ (abs‘(𝑤 − 𝐵)) < 𝑧) → (abs‘((𝐹‘𝑤) − 𝑥)) < 𝑦)) ∧ 𝑣 ∈ ℝ+ ∧ ∀𝑤 ∈ (𝐴 ∩ (-∞(,)𝐵))((𝑤 ≠ 𝐵 ∧ (abs‘(𝑤 − 𝐵)) < 𝑣) → (abs‘(((𝐹 ↾ (-∞(,)𝐵))‘𝑤) − 𝐿)) < 𝑦)) ∧ 𝑎 ∈ ((𝐴 ∩ (-∞(,)𝐵)) ∖ {𝐵}) ∧ ((abs‘(𝑎 − 𝐵)) < 𝑧 ∧ (abs‘(𝑎 − 𝐵)) < 𝑣)) → ∀𝑤 ∈ 𝐴 ((𝑤 ≠ 𝐵 ∧ (abs‘(𝑤 − 𝐵)) < 𝑧) → (abs‘((𝐹‘𝑤) − 𝑥)) < 𝑦))
290		eldifsni 4793	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝑎 ∈ ((𝐴 ∩ (-∞(,)𝐵)) ∖ {𝐵}) → 𝑎 ≠ 𝐵)
291	290	adantr 481	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((𝑎 ∈ ((𝐴 ∩ (-∞(,)𝐵)) ∖ {𝐵}) ∧ ((abs‘(𝑎 − 𝐵)) < 𝑧 ∧ (abs‘(𝑎 − 𝐵)) < 𝑣)) → 𝑎 ≠ 𝐵)
292		simprl 769	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((𝑎 ∈ ((𝐴 ∩ (-∞(,)𝐵)) ∖ {𝐵}) ∧ ((abs‘(𝑎 − 𝐵)) < 𝑧 ∧ (abs‘(𝑎 − 𝐵)) < 𝑣)) → (abs‘(𝑎 − 𝐵)) < 𝑧)
293	291, 292	jca 512	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((𝑎 ∈ ((𝐴 ∩ (-∞(,)𝐵)) ∖ {𝐵}) ∧ ((abs‘(𝑎 − 𝐵)) < 𝑧 ∧ (abs‘(𝑎 − 𝐵)) < 𝑣)) → (𝑎 ≠ 𝐵 ∧ (abs‘(𝑎 − 𝐵)) < 𝑧))
294	293	3adant1 1130	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((((𝜑 ∧ 𝑦 ∈ ℝ+) ∧ 𝑧 ∈ ℝ+ ∧ ∀𝑤 ∈ 𝐴 ((𝑤 ≠ 𝐵 ∧ (abs‘(𝑤 − 𝐵)) < 𝑧) → (abs‘((𝐹‘𝑤) − 𝑥)) < 𝑦)) ∧ 𝑣 ∈ ℝ+ ∧ ∀𝑤 ∈ (𝐴 ∩ (-∞(,)𝐵))((𝑤 ≠ 𝐵 ∧ (abs‘(𝑤 − 𝐵)) < 𝑣) → (abs‘(((𝐹 ↾ (-∞(,)𝐵))‘𝑤) − 𝐿)) < 𝑦)) ∧ 𝑎 ∈ ((𝐴 ∩ (-∞(,)𝐵)) ∖ {𝐵}) ∧ ((abs‘(𝑎 − 𝐵)) < 𝑧 ∧ (abs‘(𝑎 − 𝐵)) < 𝑣)) → (𝑎 ≠ 𝐵 ∧ (abs‘(𝑎 − 𝐵)) < 𝑧))
295		neeq1 3003	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (𝑤 = 𝑎 → (𝑤 ≠ 𝐵 ↔ 𝑎 ≠ 𝐵))
296		fvoveq1 7431	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (𝑤 = 𝑎 → (abs‘(𝑤 − 𝐵)) = (abs‘(𝑎 − 𝐵)))
297	296	breq1d 5158	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (𝑤 = 𝑎 → ((abs‘(𝑤 − 𝐵)) < 𝑧 ↔ (abs‘(𝑎 − 𝐵)) < 𝑧))
298	295, 297	anbi12d 631	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝑤 = 𝑎 → ((𝑤 ≠ 𝐵 ∧ (abs‘(𝑤 − 𝐵)) < 𝑧) ↔ (𝑎 ≠ 𝐵 ∧ (abs‘(𝑎 − 𝐵)) < 𝑧)))
299	298	imbrov2fvoveq 7433	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝑤 = 𝑎 → (((𝑤 ≠ 𝐵 ∧ (abs‘(𝑤 − 𝐵)) < 𝑧) → (abs‘((𝐹‘𝑤) − 𝑥)) < 𝑦) ↔ ((𝑎 ≠ 𝐵 ∧ (abs‘(𝑎 − 𝐵)) < 𝑧) → (abs‘((𝐹‘𝑎) − 𝑥)) < 𝑦)))
300	299	rspcva 3610	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((𝑎 ∈ 𝐴 ∧ ∀𝑤 ∈ 𝐴 ((𝑤 ≠ 𝐵 ∧ (abs‘(𝑤 − 𝐵)) < 𝑧) → (abs‘((𝐹‘𝑤) − 𝑥)) < 𝑦)) → ((𝑎 ≠ 𝐵 ∧ (abs‘(𝑎 − 𝐵)) < 𝑧) → (abs‘((𝐹‘𝑎) − 𝑥)) < 𝑦))
301	300	imp 407	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((𝑎 ∈ 𝐴 ∧ ∀𝑤 ∈ 𝐴 ((𝑤 ≠ 𝐵 ∧ (abs‘(𝑤 − 𝐵)) < 𝑧) → (abs‘((𝐹‘𝑤) − 𝑥)) < 𝑦)) ∧ (𝑎 ≠ 𝐵 ∧ (abs‘(𝑎 − 𝐵)) < 𝑧)) → (abs‘((𝐹‘𝑎) − 𝑥)) < 𝑦)
302	288, 289, 294, 301	syl21anc 836	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((((𝜑 ∧ 𝑦 ∈ ℝ+) ∧ 𝑧 ∈ ℝ+ ∧ ∀𝑤 ∈ 𝐴 ((𝑤 ≠ 𝐵 ∧ (abs‘(𝑤 − 𝐵)) < 𝑧) → (abs‘((𝐹‘𝑤) − 𝑥)) < 𝑦)) ∧ 𝑣 ∈ ℝ+ ∧ ∀𝑤 ∈ (𝐴 ∩ (-∞(,)𝐵))((𝑤 ≠ 𝐵 ∧ (abs‘(𝑤 − 𝐵)) < 𝑣) → (abs‘(((𝐹 ↾ (-∞(,)𝐵))‘𝑤) − 𝐿)) < 𝑦)) ∧ 𝑎 ∈ ((𝐴 ∩ (-∞(,)𝐵)) ∖ {𝐵}) ∧ ((abs‘(𝑎 − 𝐵)) < 𝑧 ∧ (abs‘(𝑎 − 𝐵)) < 𝑣)) → (abs‘((𝐹‘𝑎) − 𝑥)) < 𝑦)
303	260	3ad2ant2 1134	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((((𝜑 ∧ 𝑦 ∈ ℝ+) ∧ 𝑧 ∈ ℝ+ ∧ ∀𝑤 ∈ 𝐴 ((𝑤 ≠ 𝐵 ∧ (abs‘(𝑤 − 𝐵)) < 𝑧) → (abs‘((𝐹‘𝑤) − 𝑥)) < 𝑦)) ∧ 𝑣 ∈ ℝ+ ∧ ∀𝑤 ∈ (𝐴 ∩ (-∞(,)𝐵))((𝑤 ≠ 𝐵 ∧ (abs‘(𝑤 − 𝐵)) < 𝑣) → (abs‘(((𝐹 ↾ (-∞(,)𝐵))‘𝑤) − 𝐿)) < 𝑦)) ∧ 𝑎 ∈ ((𝐴 ∩ (-∞(,)𝐵)) ∖ {𝐵}) ∧ ((abs‘(𝑎 − 𝐵)) < 𝑧 ∧ (abs‘(𝑎 − 𝐵)) < 𝑣)) → 𝑎 ∈ (𝐴 ∩ (-∞(,)𝐵)))
304	242	3ad2ant1 1133	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((((𝜑 ∧ 𝑦 ∈ ℝ+) ∧ 𝑧 ∈ ℝ+ ∧ ∀𝑤 ∈ 𝐴 ((𝑤 ≠ 𝐵 ∧ (abs‘(𝑤 − 𝐵)) < 𝑧) → (abs‘((𝐹‘𝑤) − 𝑥)) < 𝑦)) ∧ 𝑣 ∈ ℝ+ ∧ ∀𝑤 ∈ (𝐴 ∩ (-∞(,)𝐵))((𝑤 ≠ 𝐵 ∧ (abs‘(𝑤 − 𝐵)) < 𝑣) → (abs‘(((𝐹 ↾ (-∞(,)𝐵))‘𝑤) − 𝐿)) < 𝑦)) ∧ 𝑎 ∈ ((𝐴 ∩ (-∞(,)𝐵)) ∖ {𝐵}) ∧ ((abs‘(𝑎 − 𝐵)) < 𝑧 ∧ (abs‘(𝑎 − 𝐵)) < 𝑣)) → 𝜑)
305		simp13 1205	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((((𝜑 ∧ 𝑦 ∈ ℝ+) ∧ 𝑧 ∈ ℝ+ ∧ ∀𝑤 ∈ 𝐴 ((𝑤 ≠ 𝐵 ∧ (abs‘(𝑤 − 𝐵)) < 𝑧) → (abs‘((𝐹‘𝑤) − 𝑥)) < 𝑦)) ∧ 𝑣 ∈ ℝ+ ∧ ∀𝑤 ∈ (𝐴 ∩ (-∞(,)𝐵))((𝑤 ≠ 𝐵 ∧ (abs‘(𝑤 − 𝐵)) < 𝑣) → (abs‘(((𝐹 ↾ (-∞(,)𝐵))‘𝑤) − 𝐿)) < 𝑦)) ∧ 𝑎 ∈ ((𝐴 ∩ (-∞(,)𝐵)) ∖ {𝐵}) ∧ ((abs‘(𝑎 − 𝐵)) < 𝑧 ∧ (abs‘(𝑎 − 𝐵)) < 𝑣)) → ∀𝑤 ∈ (𝐴 ∩ (-∞(,)𝐵))((𝑤 ≠ 𝐵 ∧ (abs‘(𝑤 − 𝐵)) < 𝑣) → (abs‘(((𝐹 ↾ (-∞(,)𝐵))‘𝑤) − 𝐿)) < 𝑦))
306		nfra1 3281	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ Ⅎ𝑤∀𝑤 ∈ (𝐴 ∩ (-∞(,)𝐵))((𝑤 ≠ 𝐵 ∧ (abs‘(𝑤 − 𝐵)) < 𝑣) → (abs‘(((𝐹 ↾ (-∞(,)𝐵))‘𝑤) − 𝐿)) < 𝑦)
307	148, 306	nfan 1902	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ Ⅎ𝑤(𝜑 ∧ ∀𝑤 ∈ (𝐴 ∩ (-∞(,)𝐵))((𝑤 ≠ 𝐵 ∧ (abs‘(𝑤 − 𝐵)) < 𝑣) → (abs‘(((𝐹 ↾ (-∞(,)𝐵))‘𝑤) − 𝐿)) < 𝑦))
308		elinel2 4196	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ (𝑤 ∈ (𝐴 ∩ (-∞(,)𝐵)) → 𝑤 ∈ (-∞(,)𝐵))
309	308	fvresd 6911	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ (𝑤 ∈ (𝐴 ∩ (-∞(,)𝐵)) → ((𝐹 ↾ (-∞(,)𝐵))‘𝑤) = (𝐹‘𝑤))
310	309	eqcomd 2738	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ (𝑤 ∈ (𝐴 ∩ (-∞(,)𝐵)) → (𝐹‘𝑤) = ((𝐹 ↾ (-∞(,)𝐵))‘𝑤))
311	310	fvoveq1d 7430	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (𝑤 ∈ (𝐴 ∩ (-∞(,)𝐵)) → (abs‘((𝐹‘𝑤) − 𝐿)) = (abs‘(((𝐹 ↾ (-∞(,)𝐵))‘𝑤) − 𝐿)))
312	311	3ad2ant2 1134	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (((𝜑 ∧ ∀𝑤 ∈ (𝐴 ∩ (-∞(,)𝐵))((𝑤 ≠ 𝐵 ∧ (abs‘(𝑤 − 𝐵)) < 𝑣) → (abs‘(((𝐹 ↾ (-∞(,)𝐵))‘𝑤) − 𝐿)) < 𝑦)) ∧ 𝑤 ∈ (𝐴 ∩ (-∞(,)𝐵)) ∧ (𝑤 ≠ 𝐵 ∧ (abs‘(𝑤 − 𝐵)) < 𝑣)) → (abs‘((𝐹‘𝑤) − 𝐿)) = (abs‘(((𝐹 ↾ (-∞(,)𝐵))‘𝑤) − 𝐿)))
313		rspa 3245	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ ((∀𝑤 ∈ (𝐴 ∩ (-∞(,)𝐵))((𝑤 ≠ 𝐵 ∧ (abs‘(𝑤 − 𝐵)) < 𝑣) → (abs‘(((𝐹 ↾ (-∞(,)𝐵))‘𝑤) − 𝐿)) < 𝑦) ∧ 𝑤 ∈ (𝐴 ∩ (-∞(,)𝐵))) → ((𝑤 ≠ 𝐵 ∧ (abs‘(𝑤 − 𝐵)) < 𝑣) → (abs‘(((𝐹 ↾ (-∞(,)𝐵))‘𝑤) − 𝐿)) < 𝑦))
314	313	3impia 1117	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ ((∀𝑤 ∈ (𝐴 ∩ (-∞(,)𝐵))((𝑤 ≠ 𝐵 ∧ (abs‘(𝑤 − 𝐵)) < 𝑣) → (abs‘(((𝐹 ↾ (-∞(,)𝐵))‘𝑤) − 𝐿)) < 𝑦) ∧ 𝑤 ∈ (𝐴 ∩ (-∞(,)𝐵)) ∧ (𝑤 ≠ 𝐵 ∧ (abs‘(𝑤 − 𝐵)) < 𝑣)) → (abs‘(((𝐹 ↾ (-∞(,)𝐵))‘𝑤) − 𝐿)) < 𝑦)
315	314	3adant1l 1176	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (((𝜑 ∧ ∀𝑤 ∈ (𝐴 ∩ (-∞(,)𝐵))((𝑤 ≠ 𝐵 ∧ (abs‘(𝑤 − 𝐵)) < 𝑣) → (abs‘(((𝐹 ↾ (-∞(,)𝐵))‘𝑤) − 𝐿)) < 𝑦)) ∧ 𝑤 ∈ (𝐴 ∩ (-∞(,)𝐵)) ∧ (𝑤 ≠ 𝐵 ∧ (abs‘(𝑤 − 𝐵)) < 𝑣)) → (abs‘(((𝐹 ↾ (-∞(,)𝐵))‘𝑤) − 𝐿)) < 𝑦)
316	312, 315	eqbrtrd 5170	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (((𝜑 ∧ ∀𝑤 ∈ (𝐴 ∩ (-∞(,)𝐵))((𝑤 ≠ 𝐵 ∧ (abs‘(𝑤 − 𝐵)) < 𝑣) → (abs‘(((𝐹 ↾ (-∞(,)𝐵))‘𝑤) − 𝐿)) < 𝑦)) ∧ 𝑤 ∈ (𝐴 ∩ (-∞(,)𝐵)) ∧ (𝑤 ≠ 𝐵 ∧ (abs‘(𝑤 − 𝐵)) < 𝑣)) → (abs‘((𝐹‘𝑤) − 𝐿)) < 𝑦)
317	316	3exp 1119	. . . . . . . . . . . . . . . . . . . . . . . . . 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 714	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((𝑎 ∈ ((𝐴 ∩ (-∞(,)𝐵)) ∖ {𝐵}) ∧ ((abs‘(𝑎 − 𝐵)) < 𝑧 ∧ (abs‘(𝑎 − 𝐵)) < 𝑣)) → (𝑎 ≠ 𝐵 ∧ (abs‘(𝑎 − 𝐵)) < 𝑣))
322	321	3adant1 1130	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((((𝜑 ∧ 𝑦 ∈ ℝ+) ∧ 𝑧 ∈ ℝ+ ∧ ∀𝑤 ∈ 𝐴 ((𝑤 ≠ 𝐵 ∧ (abs‘(𝑤 − 𝐵)) < 𝑧) → (abs‘((𝐹‘𝑤) − 𝑥)) < 𝑦)) ∧ 𝑣 ∈ ℝ+ ∧ ∀𝑤 ∈ (𝐴 ∩ (-∞(,)𝐵))((𝑤 ≠ 𝐵 ∧ (abs‘(𝑤 − 𝐵)) < 𝑣) → (abs‘(((𝐹 ↾ (-∞(,)𝐵))‘𝑤) − 𝐿)) < 𝑦)) ∧ 𝑎 ∈ ((𝐴 ∩ (-∞(,)𝐵)) ∖ {𝐵}) ∧ ((abs‘(𝑎 − 𝐵)) < 𝑧 ∧ (abs‘(𝑎 − 𝐵)) < 𝑣)) → (𝑎 ≠ 𝐵 ∧ (abs‘(𝑎 − 𝐵)) < 𝑣))
323	296	breq1d 5158	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (𝑤 = 𝑎 → ((abs‘(𝑤 − 𝐵)) < 𝑣 ↔ (abs‘(𝑎 − 𝐵)) < 𝑣))
324	295, 323	anbi12d 631	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝑤 = 𝑎 → ((𝑤 ≠ 𝐵 ∧ (abs‘(𝑤 − 𝐵)) < 𝑣) ↔ (𝑎 ≠ 𝐵 ∧ (abs‘(𝑎 − 𝐵)) < 𝑣)))
325	324	imbrov2fvoveq 7433	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝑤 = 𝑎 → (((𝑤 ≠ 𝐵 ∧ (abs‘(𝑤 − 𝐵)) < 𝑣) → (abs‘((𝐹‘𝑤) − 𝐿)) < 𝑦) ↔ ((𝑎 ≠ 𝐵 ∧ (abs‘(𝑎 − 𝐵)) < 𝑣) → (abs‘((𝐹‘𝑎) − 𝐿)) < 𝑦)))
326	325	rspcva 3610	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((𝑎 ∈ (𝐴 ∩ (-∞(,)𝐵)) ∧ ∀𝑤 ∈ (𝐴 ∩ (-∞(,)𝐵))((𝑤 ≠ 𝐵 ∧ (abs‘(𝑤 − 𝐵)) < 𝑣) → (abs‘((𝐹‘𝑤) − 𝐿)) < 𝑦)) → ((𝑎 ≠ 𝐵 ∧ (abs‘(𝑎 − 𝐵)) < 𝑣) → (abs‘((𝐹‘𝑎) − 𝐿)) < 𝑦))
327	326	imp 407	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((𝑎 ∈ (𝐴 ∩ (-∞(,)𝐵)) ∧ ∀𝑤 ∈ (𝐴 ∩ (-∞(,)𝐵))((𝑤 ≠ 𝐵 ∧ (abs‘(𝑤 − 𝐵)) < 𝑣) → (abs‘((𝐹‘𝑤) − 𝐿)) < 𝑦)) ∧ (𝑎 ≠ 𝐵 ∧ (abs‘(𝑎 − 𝐵)) < 𝑣)) → (abs‘((𝐹‘𝑎) − 𝐿)) < 𝑦)
328	303, 319, 322, 327	syl21anc 836	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((((𝜑 ∧ 𝑦 ∈ ℝ+) ∧ 𝑧 ∈ ℝ+ ∧ ∀𝑤 ∈ 𝐴 ((𝑤 ≠ 𝐵 ∧ (abs‘(𝑤 − 𝐵)) < 𝑧) → (abs‘((𝐹‘𝑤) − 𝑥)) < 𝑦)) ∧ 𝑣 ∈ ℝ+ ∧ ∀𝑤 ∈ (𝐴 ∩ (-∞(,)𝐵))((𝑤 ≠ 𝐵 ∧ (abs‘(𝑤 − 𝐵)) < 𝑣) → (abs‘(((𝐹 ↾ (-∞(,)𝐵))‘𝑤) − 𝐿)) < 𝑦)) ∧ 𝑎 ∈ ((𝐴 ∩ (-∞(,)𝐵)) ∖ {𝐵}) ∧ ((abs‘(𝑎 − 𝐵)) < 𝑧 ∧ (abs‘(𝑎 − 𝐵)) < 𝑣)) → (abs‘((𝐹‘𝑎) − 𝐿)) < 𝑦)
329		rspe 3246	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝑎 ∈ 𝐴 ∧ ((abs‘((𝐹‘𝑎) − 𝑥)) < 𝑦 ∧ (abs‘((𝐹‘𝑎) − 𝐿)) < 𝑦)) → ∃𝑎 ∈ 𝐴 ((abs‘((𝐹‘𝑎) − 𝑥)) < 𝑦 ∧ (abs‘((𝐹‘𝑎) − 𝐿)) < 𝑦))
330	288, 302, 328, 329	syl12anc 835	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((((𝜑 ∧ 𝑦 ∈ ℝ+) ∧ 𝑧 ∈ ℝ+ ∧ ∀𝑤 ∈ 𝐴 ((𝑤 ≠ 𝐵 ∧ (abs‘(𝑤 − 𝐵)) < 𝑧) → (abs‘((𝐹‘𝑤) − 𝑥)) < 𝑦)) ∧ 𝑣 ∈ ℝ+ ∧ ∀𝑤 ∈ (𝐴 ∩ (-∞(,)𝐵))((𝑤 ≠ 𝐵 ∧ (abs‘(𝑤 − 𝐵)) < 𝑣) → (abs‘(((𝐹 ↾ (-∞(,)𝐵))‘𝑤) − 𝐿)) < 𝑦)) ∧ 𝑎 ∈ ((𝐴 ∩ (-∞(,)𝐵)) ∖ {𝐵}) ∧ ((abs‘(𝑎 − 𝐵)) < 𝑧 ∧ (abs‘(𝑎 − 𝐵)) < 𝑣)) → ∃𝑎 ∈ 𝐴 ((abs‘((𝐹‘𝑎) − 𝑥)) < 𝑦 ∧ (abs‘((𝐹‘𝑎) − 𝐿)) < 𝑦))
331	330	3exp 1119	. . . . . . . . . . . . . . . . . . . . 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 1119	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑦 ∈ ℝ+) ∧ 𝑧 ∈ ℝ+ ∧ ∀𝑤 ∈ 𝐴 ((𝑤 ≠ 𝐵 ∧ (abs‘(𝑤 − 𝐵)) < 𝑧) → (abs‘((𝐹‘𝑤) − 𝑥)) < 𝑦)) → (𝑣 ∈ ℝ+ → (∀𝑤 ∈ (𝐴 ∩ (-∞(,)𝐵))((𝑤 ≠ 𝐵 ∧ (abs‘(𝑤 − 𝐵)) < 𝑣) → (abs‘(((𝐹 ↾ (-∞(,)𝐵))‘𝑤) − 𝐿)) < 𝑦) → ∃𝑎 ∈ 𝐴 ((abs‘((𝐹‘𝑎) − 𝑥)) < 𝑦 ∧ (abs‘((𝐹‘𝑎) − 𝐿)) < 𝑦))))
335	334	rexlimdv 3153	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑦 ∈ ℝ+) ∧ 𝑧 ∈ ℝ+ ∧ ∀𝑤 ∈ 𝐴 ((𝑤 ≠ 𝐵 ∧ (abs‘(𝑤 − 𝐵)) < 𝑧) → (abs‘((𝐹‘𝑤) − 𝑥)) < 𝑦)) → (∃𝑣 ∈ ℝ+ ∀𝑤 ∈ (𝐴 ∩ (-∞(,)𝐵))((𝑤 ≠ 𝐵 ∧ (abs‘(𝑤 − 𝐵)) < 𝑣) → (abs‘(((𝐹 ↾ (-∞(,)𝐵))‘𝑤) − 𝐿)) < 𝑦) → ∃𝑎 ∈ 𝐴 ((abs‘((𝐹‘𝑎) − 𝑥)) < 𝑦 ∧ (abs‘((𝐹‘𝑎) − 𝐿)) < 𝑦)))
336	241, 335	mpd 15	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑦 ∈ ℝ+) ∧ 𝑧 ∈ ℝ+ ∧ ∀𝑤 ∈ 𝐴 ((𝑤 ≠ 𝐵 ∧ (abs‘(𝑤 − 𝐵)) < 𝑧) → (abs‘((𝐹‘𝑤) − 𝑥)) < 𝑦)) → ∃𝑎 ∈ 𝐴 ((abs‘((𝐹‘𝑎) − 𝑥)) < 𝑦 ∧ (abs‘((𝐹‘𝑎) − 𝐿)) < 𝑦))
337	336	3exp 1119	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑦 ∈ ℝ+) → (𝑧 ∈ ℝ+ → (∀𝑤 ∈ 𝐴 ((𝑤 ≠ 𝐵 ∧ (abs‘(𝑤 − 𝐵)) < 𝑧) → (abs‘((𝐹‘𝑤) − 𝑥)) < 𝑦) → ∃𝑎 ∈ 𝐴 ((abs‘((𝐹‘𝑎) − 𝑥)) < 𝑦 ∧ (abs‘((𝐹‘𝑎) − 𝐿)) < 𝑦))))
338	337	rexlimdv 3153	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑦 ∈ ℝ+) → (∃𝑧 ∈ ℝ+ ∀𝑤 ∈ 𝐴 ((𝑤 ≠ 𝐵 ∧ (abs‘(𝑤 − 𝐵)) < 𝑧) → (abs‘((𝐹‘𝑤) − 𝑥)) < 𝑦) → ∃𝑎 ∈ 𝐴 ((abs‘((𝐹‘𝑎) − 𝑥)) < 𝑦 ∧ (abs‘((𝐹‘𝑎) − 𝐿)) < 𝑦)))
339	338	imp 407	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑦 ∈ ℝ+) ∧ ∃𝑧 ∈ ℝ+ ∀𝑤 ∈ 𝐴 ((𝑤 ≠ 𝐵 ∧ (abs‘(𝑤 − 𝐵)) < 𝑧) → (abs‘((𝐹‘𝑤) − 𝑥)) < 𝑦)) → ∃𝑎 ∈ 𝐴 ((abs‘((𝐹‘𝑎) − 𝑥)) < 𝑦 ∧ (abs‘((𝐹‘𝑎) − 𝐿)) < 𝑦))
340	339	adantllr 717	. . . . . . . . . . . 12 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℂ) ∧ 𝑦 ∈ ℝ+) ∧ ∃𝑧 ∈ ℝ+ ∀𝑤 ∈ 𝐴 ((𝑤 ≠ 𝐵 ∧ (abs‘(𝑤 − 𝐵)) < 𝑧) → (abs‘((𝐹‘𝑤) − 𝑥)) < 𝑦)) → ∃𝑎 ∈ 𝐴 ((abs‘((𝐹‘𝑎) − 𝑥)) < 𝑦 ∧ (abs‘((𝐹‘𝑎) − 𝐿)) < 𝑦))
341	231, 340	reximddv3 43830	. . . . . . . . . . 11 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℂ) ∧ 𝑦 ∈ ℝ+) ∧ ∃𝑧 ∈ ℝ+ ∀𝑤 ∈ 𝐴 ((𝑤 ≠ 𝐵 ∧ (abs‘(𝑤 − 𝐵)) < 𝑧) → (abs‘((𝐹‘𝑤) − 𝑥)) < 𝑦)) → ∃𝑎 ∈ 𝐴 ∃𝑏 ∈ 𝐴 (abs‘(𝑅 − 𝐿)) < (4 · 𝑦))
342	32, 33, 35, 341	syl21anc 836	. . . . . . . . . 10 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℂ) ∧ ∀𝑦 ∈ ℝ+ ∃𝑧 ∈ ℝ+ ∀𝑤 ∈ 𝐴 ((𝑤 ≠ 𝐵 ∧ (abs‘(𝑤 − 𝐵)) < 𝑧) → (abs‘((𝐹‘𝑤) − 𝑥)) < 𝑦)) ∧ 𝑦 ∈ ℝ+) → ∃𝑎 ∈ 𝐴 ∃𝑏 ∈ 𝐴 (abs‘(𝑅 − 𝐿)) < (4 · 𝑦))
343	342	ex 413	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑥 ∈ ℂ) ∧ ∀𝑦 ∈ ℝ+ ∃𝑧 ∈ ℝ+ ∀𝑤 ∈ 𝐴 ((𝑤 ≠ 𝐵 ∧ (abs‘(𝑤 − 𝐵)) < 𝑧) → (abs‘((𝐹‘𝑤) − 𝑥)) < 𝑦)) → (𝑦 ∈ ℝ+ → ∃𝑎 ∈ 𝐴 ∃𝑏 ∈ 𝐴 (abs‘(𝑅 − 𝐿)) < (4 · 𝑦)))
344	24, 25, 31, 343	vtoclf 3547	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑥 ∈ ℂ) ∧ ∀𝑦 ∈ ℝ+ ∃𝑧 ∈ ℝ+ ∀𝑤 ∈ 𝐴 ((𝑤 ≠ 𝐵 ∧ (abs‘(𝑤 − 𝐵)) < 𝑧) → (abs‘((𝐹‘𝑤) − 𝑥)) < 𝑦)) → (((abs‘(𝑅 − 𝐿)) / 4) ∈ ℝ+ → ∃𝑎 ∈ 𝐴 ∃𝑏 ∈ 𝐴 (abs‘(𝑅 − 𝐿)) < (4 · ((abs‘(𝑅 − 𝐿)) / 4))))
345	19, 344	mpd 15	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑥 ∈ ℂ) ∧ ∀𝑦 ∈ ℝ+ ∃𝑧 ∈ ℝ+ ∀𝑤 ∈ 𝐴 ((𝑤 ≠ 𝐵 ∧ (abs‘(𝑤 − 𝐵)) < 𝑧) → (abs‘((𝐹‘𝑤) − 𝑥)) < 𝑦)) → ∃𝑎 ∈ 𝐴 ∃𝑏 ∈ 𝐴 (abs‘(𝑅 − 𝐿)) < (4 · ((abs‘(𝑅 − 𝐿)) / 4)))
346		simpr 485	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (abs‘(𝑅 − 𝐿)) < (4 · ((abs‘(𝑅 − 𝐿)) / 4))) → (abs‘(𝑅 − 𝐿)) < (4 · ((abs‘(𝑅 − 𝐿)) / 4)))
347		abssubrp 43975	. . . . . . . . . . . . . . . 16 ⊢ ((𝑅 ∈ ℂ ∧ 𝐿 ∈ ℂ ∧ 𝑅 ≠ 𝐿) → (abs‘(𝑅 − 𝐿)) ∈ ℝ+)
348	3, 7, 11, 347	syl3anc 1371	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (abs‘(𝑅 − 𝐿)) ∈ ℝ+)
349	348	rpcnd 13017	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (abs‘(𝑅 − 𝐿)) ∈ ℂ)
350	349	adantr 481	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ (abs‘(𝑅 − 𝐿)) < (4 · ((abs‘(𝑅 − 𝐿)) / 4))) → (abs‘(𝑅 − 𝐿)) ∈ ℂ)
351		4cn 12296	. . . . . . . . . . . . . 14 ⊢ 4 ∈ ℂ
352	351	a1i 11	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ (abs‘(𝑅 − 𝐿)) < (4 · ((abs‘(𝑅 − 𝐿)) / 4))) → 4 ∈ ℂ)
353		4ne0 12319	. . . . . . . . . . . . . 14 ⊢ 4 ≠ 0
354	353	a1i 11	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ (abs‘(𝑅 − 𝐿)) < (4 · ((abs‘(𝑅 − 𝐿)) / 4))) → 4 ≠ 0)
355	350, 352, 354	divcan2d 11991	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (abs‘(𝑅 − 𝐿)) < (4 · ((abs‘(𝑅 − 𝐿)) / 4))) → (4 · ((abs‘(𝑅 − 𝐿)) / 4)) = (abs‘(𝑅 − 𝐿)))
356	346, 355	breqtrd 5174	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (abs‘(𝑅 − 𝐿)) < (4 · ((abs‘(𝑅 − 𝐿)) / 4))) → (abs‘(𝑅 − 𝐿)) < (abs‘(𝑅 − 𝐿)))
357	356	ex 413	. . . . . . . . . 10 ⊢ (𝜑 → ((abs‘(𝑅 − 𝐿)) < (4 · ((abs‘(𝑅 − 𝐿)) / 4)) → (abs‘(𝑅 − 𝐿)) < (abs‘(𝑅 − 𝐿))))
358	357	a1d 25	. . . . . . . . 9 ⊢ (𝜑 → ((𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐴) → ((abs‘(𝑅 − 𝐿)) < (4 · ((abs‘(𝑅 − 𝐿)) / 4)) → (abs‘(𝑅 − 𝐿)) < (abs‘(𝑅 − 𝐿)))))
359	358	ad2antrr 724	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑥 ∈ ℂ) ∧ ∀𝑦 ∈ ℝ+ ∃𝑧 ∈ ℝ+ ∀𝑤 ∈ 𝐴 ((𝑤 ≠ 𝐵 ∧ (abs‘(𝑤 − 𝐵)) < 𝑧) → (abs‘((𝐹‘𝑤) − 𝑥)) < 𝑦)) → ((𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐴) → ((abs‘(𝑅 − 𝐿)) < (4 · ((abs‘(𝑅 − 𝐿)) / 4)) → (abs‘(𝑅 − 𝐿)) < (abs‘(𝑅 − 𝐿)))))
360	359	rexlimdvv 3210	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑥 ∈ ℂ) ∧ ∀𝑦 ∈ ℝ+ ∃𝑧 ∈ ℝ+ ∀𝑤 ∈ 𝐴 ((𝑤 ≠ 𝐵 ∧ (abs‘(𝑤 − 𝐵)) < 𝑧) → (abs‘((𝐹‘𝑤) − 𝑥)) < 𝑦)) → (∃𝑎 ∈ 𝐴 ∃𝑏 ∈ 𝐴 (abs‘(𝑅 − 𝐿)) < (4 · ((abs‘(𝑅 − 𝐿)) / 4)) → (abs‘(𝑅 − 𝐿)) < (abs‘(𝑅 − 𝐿))))
361	345, 360	mpd 15	. . . . . 6 ⊢ (((𝜑 ∧ 𝑥 ∈ ℂ) ∧ ∀𝑦 ∈ ℝ+ ∃𝑧 ∈ ℝ+ ∀𝑤 ∈ 𝐴 ((𝑤 ≠ 𝐵 ∧ (abs‘(𝑤 − 𝐵)) < 𝑧) → (abs‘((𝐹‘𝑤) − 𝑥)) < 𝑦)) → (abs‘(𝑅 − 𝐿)) < (abs‘(𝑅 − 𝐿)))
362	9	abscld 15382	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑥 ∈ ℂ) ∧ ∀𝑦 ∈ ℝ+ ∃𝑧 ∈ ℝ+ ∀𝑤 ∈ 𝐴 ((𝑤 ≠ 𝐵 ∧ (abs‘(𝑤 − 𝐵)) < 𝑧) → (abs‘((𝐹‘𝑤) − 𝑥)) < 𝑦)) → (abs‘(𝑅 − 𝐿)) ∈ ℝ)
363	362	ltnrd 11347	. . . . . 6 ⊢ (((𝜑 ∧ 𝑥 ∈ ℂ) ∧ ∀𝑦 ∈ ℝ+ ∃𝑧 ∈ ℝ+ ∀𝑤 ∈ 𝐴 ((𝑤 ≠ 𝐵 ∧ (abs‘(𝑤 − 𝐵)) < 𝑧) → (abs‘((𝐹‘𝑤) − 𝑥)) < 𝑦)) → ¬ (abs‘(𝑅 − 𝐿)) < (abs‘(𝑅 − 𝐿)))
364	361, 363	pm2.65da 815	. . . . 5 ⊢ ((𝜑 ∧ 𝑥 ∈ ℂ) → ¬ ∀𝑦 ∈ ℝ+ ∃𝑧 ∈ ℝ+ ∀𝑤 ∈ 𝐴 ((𝑤 ≠ 𝐵 ∧ (abs‘(𝑤 − 𝐵)) < 𝑧) → (abs‘((𝐹‘𝑤) − 𝑥)) < 𝑦))
365	364	ex 413	. . . 4 ⊢ (𝜑 → (𝑥 ∈ ℂ → ¬ ∀𝑦 ∈ ℝ+ ∃𝑧 ∈ ℝ+ ∀𝑤 ∈ 𝐴 ((𝑤 ≠ 𝐵 ∧ (abs‘(𝑤 − 𝐵)) < 𝑧) → (abs‘((𝐹‘𝑤) − 𝑥)) < 𝑦)))
366		imnan 400	. . . 4 ⊢ ((𝑥 ∈ ℂ → ¬ ∀𝑦 ∈ ℝ+ ∃𝑧 ∈ ℝ+ ∀𝑤 ∈ 𝐴 ((𝑤 ≠ 𝐵 ∧ (abs‘(𝑤 − 𝐵)) < 𝑧) → (abs‘((𝐹‘𝑤) − 𝑥)) < 𝑦)) ↔ ¬ (𝑥 ∈ ℂ ∧ ∀𝑦 ∈ ℝ+ ∃𝑧 ∈ ℝ+ ∀𝑤 ∈ 𝐴 ((𝑤 ≠ 𝐵 ∧ (abs‘(𝑤 − 𝐵)) < 𝑧) → (abs‘((𝐹‘𝑤) − 𝑥)) < 𝑦)))
367	365, 366	sylib 217	. . 3 ⊢ (𝜑 → ¬ (𝑥 ∈ ℂ ∧ ∀𝑦 ∈ ℝ+ ∃𝑧 ∈ ℝ+ ∀𝑤 ∈ 𝐴 ((𝑤 ≠ 𝐵 ∧ (abs‘(𝑤 − 𝐵)) < 𝑧) → (abs‘((𝐹‘𝑤) − 𝑥)) < 𝑦)))
368		limclner.a	. . . . 5 ⊢ (𝜑 → 𝐴 ⊆ ℝ)
369	368, 73	sstrd 3992	. . . 4 ⊢ (𝜑 → 𝐴 ⊆ ℂ)
370	36, 369, 56	ellimc3 25395	. . 3 ⊢ (𝜑 → (𝑥 ∈ (𝐹 limℂ 𝐵) ↔ (𝑥 ∈ ℂ ∧ ∀𝑦 ∈ ℝ+ ∃𝑧 ∈ ℝ+ ∀𝑤 ∈ 𝐴 ((𝑤 ≠ 𝐵 ∧ (abs‘(𝑤 − 𝐵)) < 𝑧) → (abs‘((𝐹‘𝑤) − 𝑥)) < 𝑦))))
371	367, 370	mtbird 324	. 2 ⊢ (𝜑 → ¬ 𝑥 ∈ (𝐹 limℂ 𝐵))
372	371	eq0rdv 4404	1 ⊢ (𝜑 → (𝐹 limℂ 𝐵) = ∅)

Syntax hints:  ¬ wn 3   → wi 4   ∧ wa 396   ∧ w3a 1087   = wceq 1541   ∈ wcel 2106   ≠ wne 2940  ∀wral 3061  ∃wrex 3070   ∖ cdif 3945   ∩ cin 3947   ⊆ wss 3948  ∅c0 4322  ifcif 4528  {csn 4628  ∪ cuni 4908   class class class wbr 5148  ran crn 5677   ↾ cres 5678  ⟶wf 6539  ‘cfv 6543  (class class class)co 7408  ℂcc 11107  ℝcr 11108  0cc0 11109   + caddc 11112   · cmul 11114  +∞cpnf 11244  -∞cmnf 11245   < clt 11247   ≤ cle 11248   − cmin 11443   / cdiv 11870  4c4 12268  ℝ⁺crp 12973  (,)cioo 13323  abscabs 15180   ↾_t crest 17365  TopOpenctopn 17366  topGenctg 17382  ℂ_fldccnfld 20943  Topctop 22394  limPtclp 22637   lim_ℂ climc 25378

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-10 2137  ax-11 2154  ax-12 2171  ax-ext 2703  ax-rep 5285  ax-sep 5299  ax-nul 5306  ax-pow 5363  ax-pr 5427  ax-un 7724  ax-cnex 11165  ax-resscn 11166  ax-1cn 11167  ax-icn 11168  ax-addcl 11169  ax-addrcl 11170  ax-mulcl 11171  ax-mulrcl 11172  ax-mulcom 11173  ax-addass 11174  ax-mulass 11175  ax-distr 11176  ax-i2m1 11177  ax-1ne0 11178  ax-1rid 11179  ax-rnegex 11180  ax-rrecex 11181  ax-cnre 11182  ax-pre-lttri 11183  ax-pre-lttrn 11184  ax-pre-ltadd 11185  ax-pre-mulgt0 11186  ax-pre-sup 11187

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 846  df-3or 1088  df-3an 1089  df-tru 1544  df-fal 1554  df-ex 1782  df-nf 1786  df-sb 2068  df-mo 2534  df-eu 2563  df-clab 2710  df-cleq 2724  df-clel 2810  df-nfc 2885  df-ne 2941  df-nel 3047  df-ral 3062  df-rex 3071  df-rmo 3376  df-reu 3377  df-rab 3433  df-v 3476  df-sbc 3778  df-csb 3894  df-dif 3951  df-un 3953  df-in 3955  df-ss 3965  df-pss 3967  df-nul 4323  df-if 4529  df-pw 4604  df-sn 4629  df-pr 4631  df-tp 4633  df-op 4635  df-uni 4909  df-int 4951  df-iun 4999  df-iin 5000  df-br 5149  df-opab 5211  df-mpt 5232  df-tr 5266  df-id 5574  df-eprel 5580  df-po 5588  df-so 5589  df-fr 5631  df-we 5633  df-xp 5682  df-rel 5683  df-cnv 5684  df-co 5685  df-dm 5686  df-rn 5687  df-res 5688  df-ima 5689  df-pred 6300  df-ord 6367  df-on 6368  df-lim 6369  df-suc 6370  df-iota 6495  df-fun 6545  df-fn 6546  df-f 6547  df-f1 6548  df-fo 6549  df-f1o 6550  df-fv 6551  df-riota 7364  df-ov 7411  df-oprab 7412  df-mpo 7413  df-om 7855  df-1st 7974  df-2nd 7975  df-frecs 8265  df-wrecs 8296  df-recs 8370  df-rdg 8409  df-1o 8465  df-er 8702  df-map 8821  df-pm 8822  df-en 8939  df-dom 8940  df-sdom 8941  df-fin 8942  df-fi 9405  df-sup 9436  df-inf 9437  df-pnf 11249  df-mnf 11250  df-xr 11251  df-ltxr 11252  df-le 11253  df-sub 11445  df-neg 11446  df-div 11871  df-nn 12212  df-2 12274  df-3 12275  df-4 12276  df-5 12277  df-6 12278  df-7 12279  df-8 12280  df-9 12281  df-n0 12472  df-z 12558  df-dec 12677  df-uz 12822  df-q 12932  df-rp 12974  df-xneg 13091  df-xadd 13092  df-xmul 13093  df-ioo 13327  df-fz 13484  df-seq 13966  df-exp 14027  df-cj 15045  df-re 15046  df-im 15047  df-sqrt 15181  df-abs 15182  df-struct 17079  df-slot 17114  df-ndx 17126  df-base 17144  df-plusg 17209  df-mulr 17210  df-starv 17211  df-tset 17215  df-ple 17216  df-ds 17218  df-unif 17219  df-rest 17367  df-topn 17368  df-topgen 17388  df-psmet 20935  df-xmet 20936  df-met 20937  df-bl 20938  df-mopn 20939  df-cnfld 20944  df-top 22395  df-topon 22412  df-topsp 22434  df-bases 22448  df-cld 22522  df-ntr 22523  df-cls 22524  df-nei 22601  df-lp 22639  df-cnp 22731  df-xms 23825  df-ms 23826  df-limc 25382

This theorem is referenced by:  limclr  44361  jumpncnp  44604