Theorem limclner 45068

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 25824	. . . . . . . . . . . . 13 ⊢ ((𝐹 ↾ (𝐵(,)+∞)) limℂ 𝐵) ⊆ ℂ
2		limclner.r	. . . . . . . . . . . . 13 ⊢ (𝜑 → 𝑅 ∈ ((𝐹 ↾ (𝐵(,)+∞)) limℂ 𝐵))
3	1, 2	sselid 3980	. . . . . . . . . . . 12 ⊢ (𝜑 → 𝑅 ∈ ℂ)
4	3	ad2antrr 724	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑥 ∈ ℂ) ∧ ∀𝑦 ∈ ℝ+ ∃𝑧 ∈ ℝ+ ∀𝑤 ∈ 𝐴 ((𝑤 ≠ 𝐵 ∧ (abs‘(𝑤 − 𝐵)) < 𝑧) → (abs‘((𝐹‘𝑤) − 𝑥)) < 𝑦)) → 𝑅 ∈ ℂ)
5		limccl 25824	. . . . . . . . . . . . 13 ⊢ ((𝐹 ↾ (-∞(,)𝐵)) limℂ 𝐵) ⊆ ℂ
6		limclner.l	. . . . . . . . . . . . 13 ⊢ (𝜑 → 𝐿 ∈ ((𝐹 ↾ (-∞(,)𝐵)) limℂ 𝐵))
7	5, 6	sselid 3980	. . . . . . . . . . . 12 ⊢ (𝜑 → 𝐿 ∈ ℂ)
8	7	ad2antrr 724	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑥 ∈ ℂ) ∧ ∀𝑦 ∈ ℝ+ ∃𝑧 ∈ ℝ+ ∀𝑤 ∈ 𝐴 ((𝑤 ≠ 𝐵 ∧ (abs‘(𝑤 − 𝐵)) < 𝑧) → (abs‘((𝐹‘𝑤) − 𝑥)) < 𝑦)) → 𝐿 ∈ ℂ)
9	4, 8	subcld 11609	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑥 ∈ ℂ) ∧ ∀𝑦 ∈ ℝ+ ∃𝑧 ∈ ℝ+ ∀𝑤 ∈ 𝐴 ((𝑤 ≠ 𝐵 ∧ (abs‘(𝑤 − 𝐵)) < 𝑧) → (abs‘((𝐹‘𝑤) − 𝑥)) < 𝑦)) → (𝑅 − 𝐿) ∈ ℂ)
10		limclner.lner	. . . . . . . . . . . . 13 ⊢ (𝜑 → 𝐿 ≠ 𝑅)
11	10	necomd 2993	. . . . . . . . . . . 12 ⊢ (𝜑 → 𝑅 ≠ 𝐿)
12	11	ad2antrr 724	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑥 ∈ ℂ) ∧ ∀𝑦 ∈ ℝ+ ∃𝑧 ∈ ℝ+ ∀𝑤 ∈ 𝐴 ((𝑤 ≠ 𝐵 ∧ (abs‘(𝑤 − 𝐵)) < 𝑧) → (abs‘((𝐹‘𝑤) − 𝑥)) < 𝑦)) → 𝑅 ≠ 𝐿)
13	4, 8, 12	subne0d 11618	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑥 ∈ ℂ) ∧ ∀𝑦 ∈ ℝ+ ∃𝑧 ∈ ℝ+ ∀𝑤 ∈ 𝐴 ((𝑤 ≠ 𝐵 ∧ (abs‘(𝑤 − 𝐵)) < 𝑧) → (abs‘((𝐹‘𝑤) − 𝑥)) < 𝑦)) → (𝑅 − 𝐿) ≠ 0)
14	9, 13	absrpcld 15435	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑥 ∈ ℂ) ∧ ∀𝑦 ∈ ℝ+ ∃𝑧 ∈ ℝ+ ∀𝑤 ∈ 𝐴 ((𝑤 ≠ 𝐵 ∧ (abs‘(𝑤 − 𝐵)) < 𝑧) → (abs‘((𝐹‘𝑤) − 𝑥)) < 𝑦)) → (abs‘(𝑅 − 𝐿)) ∈ ℝ+)
15		4re 12334	. . . . . . . . . . 11 ⊢ 4 ∈ ℝ
16		4pos 12357	. . . . . . . . . . 11 ⊢ 0 < 4
17	15, 16	elrpii 13017	. . . . . . . . . 10 ⊢ 4 ∈ ℝ+
18	17	a1i 11	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑥 ∈ ℂ) ∧ ∀𝑦 ∈ ℝ+ ∃𝑧 ∈ ℝ+ ∀𝑤 ∈ 𝐴 ((𝑤 ≠ 𝐵 ∧ (abs‘(𝑤 − 𝐵)) < 𝑧) → (abs‘((𝐹‘𝑤) − 𝑥)) < 𝑦)) → 4 ∈ ℝ+)
19	14, 18	rpdivcld 13073	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑥 ∈ ℂ) ∧ ∀𝑦 ∈ ℝ+ ∃𝑧 ∈ ℝ+ ∀𝑤 ∈ 𝐴 ((𝑤 ≠ 𝐵 ∧ (abs‘(𝑤 − 𝐵)) < 𝑧) → (abs‘((𝐹‘𝑤) − 𝑥)) < 𝑦)) → ((abs‘(𝑅 − 𝐿)) / 4) ∈ ℝ+)
20		nfv 1909	. . . . . . . . . . 11 ⊢ Ⅎ𝑦(𝜑 ∧ 𝑥 ∈ ℂ)
21		nfra1 3279	. . . . . . . . . . 11 ⊢ Ⅎ𝑦∀𝑦 ∈ ℝ+ ∃𝑧 ∈ ℝ+ ∀𝑤 ∈ 𝐴 ((𝑤 ≠ 𝐵 ∧ (abs‘(𝑤 − 𝐵)) < 𝑧) → (abs‘((𝐹‘𝑤) − 𝑥)) < 𝑦)
22	20, 21	nfan 1894	. . . . . . . . . 10 ⊢ Ⅎ𝑦((𝜑 ∧ 𝑥 ∈ ℂ) ∧ ∀𝑦 ∈ ℝ+ ∃𝑧 ∈ ℝ+ ∀𝑤 ∈ 𝐴 ((𝑤 ≠ 𝐵 ∧ (abs‘(𝑤 − 𝐵)) < 𝑧) → (abs‘((𝐹‘𝑤) − 𝑥)) < 𝑦))
23		nfv 1909	. . . . . . . . . 10 ⊢ Ⅎ𝑦(((abs‘(𝑅 − 𝐿)) / 4) ∈ ℝ+ → ∃𝑎 ∈ 𝐴 ∃𝑏 ∈ 𝐴 (abs‘(𝑅 − 𝐿)) < (4 · ((abs‘(𝑅 − 𝐿)) / 4)))
24	22, 23	nfim 1891	. . . . . . . . 9 ⊢ Ⅎ𝑦(((𝜑 ∧ 𝑥 ∈ ℂ) ∧ ∀𝑦 ∈ ℝ+ ∃𝑧 ∈ ℝ+ ∀𝑤 ∈ 𝐴 ((𝑤 ≠ 𝐵 ∧ (abs‘(𝑤 − 𝐵)) < 𝑧) → (abs‘((𝐹‘𝑤) − 𝑥)) < 𝑦)) → (((abs‘(𝑅 − 𝐿)) / 4) ∈ ℝ+ → ∃𝑎 ∈ 𝐴 ∃𝑏 ∈ 𝐴 (abs‘(𝑅 − 𝐿)) < (4 · ((abs‘(𝑅 − 𝐿)) / 4))))
25		ovex 7459	. . . . . . . . 9 ⊢ ((abs‘(𝑅 − 𝐿)) / 4) ∈ V
26		eleq1 2817	. . . . . . . . . . 11 ⊢ (𝑦 = ((abs‘(𝑅 − 𝐿)) / 4) → (𝑦 ∈ ℝ+ ↔ ((abs‘(𝑅 − 𝐿)) / 4) ∈ ℝ+))
27		oveq2 7434	. . . . . . . . . . . . 13 ⊢ (𝑦 = ((abs‘(𝑅 − 𝐿)) / 4) → (4 · 𝑦) = (4 · ((abs‘(𝑅 − 𝐿)) / 4)))
28	27	breq2d 5164	. . . . . . . . . . . 12 ⊢ (𝑦 = ((abs‘(𝑅 − 𝐿)) / 4) → ((abs‘(𝑅 − 𝐿)) < (4 · 𝑦) ↔ (abs‘(𝑅 − 𝐿)) < (4 · ((abs‘(𝑅 − 𝐿)) / 4))))
29	28	2rexbidv 3217	. . . . . . . . . . 11 ⊢ (𝑦 = ((abs‘(𝑅 − 𝐿)) / 4) → (∃𝑎 ∈ 𝐴 ∃𝑏 ∈ 𝐴 (abs‘(𝑅 − 𝐿)) < (4 · 𝑦) ↔ ∃𝑎 ∈ 𝐴 ∃𝑏 ∈ 𝐴 (abs‘(𝑅 − 𝐿)) < (4 · ((abs‘(𝑅 − 𝐿)) / 4))))
30	26, 29	imbi12d 343	. . . . . . . . . 10 ⊢ (𝑦 = ((abs‘(𝑅 − 𝐿)) / 4) → ((𝑦 ∈ ℝ+ → ∃𝑎 ∈ 𝐴 ∃𝑏 ∈ 𝐴 (abs‘(𝑅 − 𝐿)) < (4 · 𝑦)) ↔ (((abs‘(𝑅 − 𝐿)) / 4) ∈ ℝ+ → ∃𝑎 ∈ 𝐴 ∃𝑏 ∈ 𝐴 (abs‘(𝑅 − 𝐿)) < (4 · ((abs‘(𝑅 − 𝐿)) / 4)))))
31	30	imbi2d 339	. . . . . . . . 9 ⊢ (𝑦 = ((abs‘(𝑅 − 𝐿)) / 4) → ((((𝜑 ∧ 𝑥 ∈ ℂ) ∧ ∀𝑦 ∈ ℝ+ ∃𝑧 ∈ ℝ+ ∀𝑤 ∈ 𝐴 ((𝑤 ≠ 𝐵 ∧ (abs‘(𝑤 − 𝐵)) < 𝑧) → (abs‘((𝐹‘𝑤) − 𝑥)) < 𝑦)) → (𝑦 ∈ ℝ+ → ∃𝑎 ∈ 𝐴 ∃𝑏 ∈ 𝐴 (abs‘(𝑅 − 𝐿)) < (4 · 𝑦))) ↔ (((𝜑 ∧ 𝑥 ∈ ℂ) ∧ ∀𝑦 ∈ ℝ+ ∃𝑧 ∈ ℝ+ ∀𝑤 ∈ 𝐴 ((𝑤 ≠ 𝐵 ∧ (abs‘(𝑤 − 𝐵)) < 𝑧) → (abs‘((𝐹‘𝑤) − 𝑥)) < 𝑦)) → (((abs‘(𝑅 − 𝐿)) / 4) ∈ ℝ+ → ∃𝑎 ∈ 𝐴 ∃𝑏 ∈ 𝐴 (abs‘(𝑅 − 𝐿)) < (4 · ((abs‘(𝑅 − 𝐿)) / 4))))))
32		simpll 765	. . . . . . . . . . 11 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℂ) ∧ ∀𝑦 ∈ ℝ+ ∃𝑧 ∈ ℝ+ ∀𝑤 ∈ 𝐴 ((𝑤 ≠ 𝐵 ∧ (abs‘(𝑤 − 𝐵)) < 𝑧) → (abs‘((𝐹‘𝑤) − 𝑥)) < 𝑦)) ∧ 𝑦 ∈ ℝ+) → (𝜑 ∧ 𝑥 ∈ ℂ))
33		simpr 483	. . . . . . . . . . 11 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℂ) ∧ ∀𝑦 ∈ ℝ+ ∃𝑧 ∈ ℝ+ ∀𝑤 ∈ 𝐴 ((𝑤 ≠ 𝐵 ∧ (abs‘(𝑤 − 𝐵)) < 𝑧) → (abs‘((𝐹‘𝑤) − 𝑥)) < 𝑦)) ∧ 𝑦 ∈ ℝ+) → 𝑦 ∈ ℝ+)
34		rspa 3243	. . . . . . . . . . . 12 ⊢ ((∀𝑦 ∈ ℝ+ ∃𝑧 ∈ ℝ+ ∀𝑤 ∈ 𝐴 ((𝑤 ≠ 𝐵 ∧ (abs‘(𝑤 − 𝐵)) < 𝑧) → (abs‘((𝐹‘𝑤) − 𝑥)) < 𝑦) ∧ 𝑦 ∈ ℝ+) → ∃𝑧 ∈ ℝ+ ∀𝑤 ∈ 𝐴 ((𝑤 ≠ 𝐵 ∧ (abs‘(𝑤 − 𝐵)) < 𝑧) → (abs‘((𝐹‘𝑤) − 𝑥)) < 𝑦))
35	34	adantll 712	. . . . . . . . . . 11 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℂ) ∧ ∀𝑦 ∈ ℝ+ ∃𝑧 ∈ ℝ+ ∀𝑤 ∈ 𝐴 ((𝑤 ≠ 𝐵 ∧ (abs‘(𝑤 − 𝐵)) < 𝑧) → (abs‘((𝐹‘𝑤) − 𝑥)) < 𝑦)) ∧ 𝑦 ∈ ℝ+) → ∃𝑧 ∈ ℝ+ ∀𝑤 ∈ 𝐴 ((𝑤 ≠ 𝐵 ∧ (abs‘(𝑤 − 𝐵)) < 𝑧) → (abs‘((𝐹‘𝑤) − 𝑥)) < 𝑦))
36		limclner.f	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝜑 → 𝐹:𝐴⟶ℂ)
37		fresin 6771	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝐹:𝐴⟶ℂ → (𝐹 ↾ (𝐵(,)+∞)):(𝐴 ∩ (𝐵(,)+∞))⟶ℂ)
38	36, 37	syl 17	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝜑 → (𝐹 ↾ (𝐵(,)+∞)):(𝐴 ∩ (𝐵(,)+∞))⟶ℂ)
39		inss2 4232	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝐴 ∩ (𝐵(,)+∞)) ⊆ (𝐵(,)+∞)
40		ioosscn 13426	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝐵(,)+∞) ⊆ ℂ
41	39, 40	sstri 3991	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝐴 ∩ (𝐵(,)+∞)) ⊆ ℂ
42	41	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝜑 → (𝐴 ∩ (𝐵(,)+∞)) ⊆ ℂ)
43		limclner.j	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ 𝐽 = (topGen‘ran (,))
44		retop 24698	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (topGen‘ran (,)) ∈ Top
45	43, 44	eqeltri 2825	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ 𝐽 ∈ Top
46		inss2 4232	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (𝐴 ∩ (-∞(,)𝐵)) ⊆ (-∞(,)𝐵)
47		ioossre 13425	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (-∞(,)𝐵) ⊆ ℝ
48	46, 47	sstri 3991	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝐴 ∩ (-∞(,)𝐵)) ⊆ ℝ
49		uniretop 24699	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ ℝ = ∪ (topGen‘ran (,))
50	43	unieqi 4924	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ ∪ 𝐽 = ∪ (topGen‘ran (,))
51	49, 50	eqtr4i 2759	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ℝ = ∪ 𝐽
52	51	lpss 23066	. . . . . . . . . . . . . . . . . . . . . . . . . . 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 11280	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝜑 → 𝐵 ∈ ℂ)
57	38, 42, 56	ellimc3 25828	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝜑 → (𝑅 ∈ ((𝐹 ↾ (𝐵(,)+∞)) limℂ 𝐵) ↔ (𝑅 ∈ ℂ ∧ ∀𝑦 ∈ ℝ+ ∃𝑣 ∈ ℝ+ ∀𝑤 ∈ (𝐴 ∩ (𝐵(,)+∞))((𝑤 ≠ 𝐵 ∧ (abs‘(𝑤 − 𝐵)) < 𝑣) → (abs‘(((𝐹 ↾ (𝐵(,)+∞))‘𝑤) − 𝑅)) < 𝑦))))
58	2, 57	mpbid 231	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝜑 → (𝑅 ∈ ℂ ∧ ∀𝑦 ∈ ℝ+ ∃𝑣 ∈ ℝ+ ∀𝑤 ∈ (𝐴 ∩ (𝐵(,)+∞))((𝑤 ≠ 𝐵 ∧ (abs‘(𝑤 − 𝐵)) < 𝑣) → (abs‘(((𝐹 ↾ (𝐵(,)+∞))‘𝑤) − 𝑅)) < 𝑦)))
59	58	simprd 494	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝜑 → ∀𝑦 ∈ ℝ+ ∃𝑣 ∈ ℝ+ ∀𝑤 ∈ (𝐴 ∩ (𝐵(,)+∞))((𝑤 ≠ 𝐵 ∧ (abs‘(𝑤 − 𝐵)) < 𝑣) → (abs‘(((𝐹 ↾ (𝐵(,)+∞))‘𝑤) − 𝑅)) < 𝑦))
60	59	r19.21bi 3246	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ 𝑦 ∈ ℝ+) → ∃𝑣 ∈ ℝ+ ∀𝑤 ∈ (𝐴 ∩ (𝐵(,)+∞))((𝑤 ≠ 𝐵 ∧ (abs‘(𝑤 − 𝐵)) < 𝑣) → (abs‘(((𝐹 ↾ (𝐵(,)+∞))‘𝑤) − 𝑅)) < 𝑦))
61	60	3ad2ant1 1130	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ 𝑦 ∈ ℝ+) ∧ 𝑧 ∈ ℝ+ ∧ ∀𝑤 ∈ 𝐴 ((𝑤 ≠ 𝐵 ∧ (abs‘(𝑤 − 𝐵)) < 𝑧) → (abs‘((𝐹‘𝑤) − 𝑥)) < 𝑦)) → ∃𝑣 ∈ ℝ+ ∀𝑤 ∈ (𝐴 ∩ (𝐵(,)+∞))((𝑤 ≠ 𝐵 ∧ (abs‘(𝑤 − 𝐵)) < 𝑣) → (abs‘(((𝐹 ↾ (𝐵(,)+∞))‘𝑤) − 𝑅)) < 𝑦))
62		simp11l 1281	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((((𝜑 ∧ 𝑦 ∈ ℝ+) ∧ 𝑧 ∈ ℝ+ ∧ ∀𝑤 ∈ 𝐴 ((𝑤 ≠ 𝐵 ∧ (abs‘(𝑤 − 𝐵)) < 𝑧) → (abs‘((𝐹‘𝑤) − 𝑥)) < 𝑦)) ∧ 𝑣 ∈ ℝ+ ∧ ∀𝑤 ∈ (𝐴 ∩ (𝐵(,)+∞))((𝑤 ≠ 𝐵 ∧ (abs‘(𝑤 − 𝐵)) < 𝑣) → (abs‘(((𝐹 ↾ (𝐵(,)+∞))‘𝑤) − 𝑅)) < 𝑦)) → 𝜑)
63		simp12 1201	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((((𝜑 ∧ 𝑦 ∈ ℝ+) ∧ 𝑧 ∈ ℝ+ ∧ ∀𝑤 ∈ 𝐴 ((𝑤 ≠ 𝐵 ∧ (abs‘(𝑤 − 𝐵)) < 𝑧) → (abs‘((𝐹‘𝑤) − 𝑥)) < 𝑦)) ∧ 𝑣 ∈ ℝ+ ∧ ∀𝑤 ∈ (𝐴 ∩ (𝐵(,)+∞))((𝑤 ≠ 𝐵 ∧ (abs‘(𝑤 − 𝐵)) < 𝑣) → (abs‘(((𝐹 ↾ (𝐵(,)+∞))‘𝑤) − 𝑅)) < 𝑦)) → 𝑧 ∈ ℝ+)
64		simp2 1134	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((((𝜑 ∧ 𝑦 ∈ ℝ+) ∧ 𝑧 ∈ ℝ+ ∧ ∀𝑤 ∈ 𝐴 ((𝑤 ≠ 𝐵 ∧ (abs‘(𝑤 − 𝐵)) < 𝑧) → (abs‘((𝐹‘𝑤) − 𝑥)) < 𝑦)) ∧ 𝑣 ∈ ℝ+ ∧ ∀𝑤 ∈ (𝐴 ∩ (𝐵(,)+∞))((𝑤 ≠ 𝐵 ∧ (abs‘(𝑤 − 𝐵)) < 𝑣) → (abs‘(((𝐹 ↾ (𝐵(,)+∞))‘𝑤) − 𝑅)) < 𝑦)) → 𝑣 ∈ ℝ+)
65		breq2 5156	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝑢 = if(𝑧 ≤ 𝑣, 𝑧, 𝑣) → ((abs‘(𝑏 − 𝐵)) < 𝑢 ↔ (abs‘(𝑏 − 𝐵)) < if(𝑧 ≤ 𝑣, 𝑧, 𝑣)))
66	65	rexbidv 3176	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑢 = if(𝑧 ≤ 𝑣, 𝑧, 𝑣) → (∃𝑏 ∈ ((𝐴 ∩ (𝐵(,)+∞)) ∖ {𝐵})(abs‘(𝑏 − 𝐵)) < 𝑢 ↔ ∃𝑏 ∈ ((𝐴 ∩ (𝐵(,)+∞)) ∖ {𝐵})(abs‘(𝑏 − 𝐵)) < if(𝑧 ≤ 𝑣, 𝑧, 𝑣)))
67		inss1 4231	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ (((limPt‘𝐾)‘(𝐴 ∩ (𝐵(,)+∞))) ∩ ℝ) ⊆ ((limPt‘𝐾)‘(𝐴 ∩ (𝐵(,)+∞)))
68	67	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (𝜑 → (((limPt‘𝐾)‘(𝐴 ∩ (𝐵(,)+∞))) ∩ ℝ) ⊆ ((limPt‘𝐾)‘(𝐴 ∩ (𝐵(,)+∞))))
69		limclner.k	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ 𝐾 = (TopOpen‘ℂfld)
70	69	cnfldtop 24720	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ 𝐾 ∈ Top
71	70	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ (𝜑 → 𝐾 ∈ Top)
72		ax-resscn 11203	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ ℝ ⊆ ℂ
73	72	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ (𝜑 → ℝ ⊆ ℂ)
74		ioossre 13425	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ (𝐵(,)+∞) ⊆ ℝ
75	39, 74	sstri 3991	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ (𝐴 ∩ (𝐵(,)+∞)) ⊆ ℝ
76	75	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ (𝜑 → (𝐴 ∩ (𝐵(,)+∞)) ⊆ ℝ)
77		unicntop 24722	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ ℂ = ∪ (TopOpen‘ℂfld)
78	69	unieqi 4924	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ ∪ 𝐾 = ∪ (TopOpen‘ℂfld)
79	77, 78	eqtr4i 2759	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ ℂ = ∪ 𝐾
80	69	tgioo2 24739	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ (topGen‘ran (,)) = (𝐾 ↾t ℝ)
81	43, 80	eqtri 2756	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ 𝐽 = (𝐾 ↾t ℝ)
82	79, 81	restlp 23107	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ ((𝐾 ∈ Top ∧ ℝ ⊆ ℂ ∧ (𝐴 ∩ (𝐵(,)+∞)) ⊆ ℝ) → ((limPt‘𝐽)‘(𝐴 ∩ (𝐵(,)+∞))) = (((limPt‘𝐾)‘(𝐴 ∩ (𝐵(,)+∞))) ∩ ℝ))
83	71, 73, 76, 82	syl3anc 1368	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (𝜑 → ((limPt‘𝐽)‘(𝐴 ∩ (𝐵(,)+∞))) = (((limPt‘𝐾)‘(𝐴 ∩ (𝐵(,)+∞))) ∩ ℝ))
84	69	eqcomi 2737	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ (TopOpen‘ℂfld) = 𝐾
85	84	fveq2i 6905	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ (limPt‘(TopOpen‘ℂfld)) = (limPt‘𝐾)
86	85	fveq1i 6903	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 45056	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝜑 → (𝐵 ∈ ((limPt‘(TopOpen‘ℂfld))‘(𝐴 ∩ (𝐵(,)+∞))) ↔ ∀𝑢 ∈ ℝ+ ∃𝑏 ∈ ((𝐴 ∩ (𝐵(,)+∞)) ∖ {𝐵})(abs‘(𝑏 − 𝐵)) < 𝑢))
92	90, 91	mpbid 231	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝜑 → ∀𝑢 ∈ ℝ+ ∃𝑏 ∈ ((𝐴 ∩ (𝐵(,)+∞)) ∖ {𝐵})(abs‘(𝑏 − 𝐵)) < 𝑢)
93	92	3ad2ant1 1130	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((𝜑 ∧ 𝑧 ∈ ℝ+ ∧ 𝑣 ∈ ℝ+) → ∀𝑢 ∈ ℝ+ ∃𝑏 ∈ ((𝐴 ∩ (𝐵(,)+∞)) ∖ {𝐵})(abs‘(𝑏 − 𝐵)) < 𝑢)
94		ifcl 4577	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((𝑧 ∈ ℝ+ ∧ 𝑣 ∈ ℝ+) → if(𝑧 ≤ 𝑣, 𝑧, 𝑣) ∈ ℝ+)
95	94	3adant1 1127	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((𝜑 ∧ 𝑧 ∈ ℝ+ ∧ 𝑣 ∈ ℝ+) → if(𝑧 ≤ 𝑣, 𝑧, 𝑣) ∈ ℝ+)
96	66, 93, 95	rspcdva 3612	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝜑 ∧ 𝑧 ∈ ℝ+ ∧ 𝑣 ∈ ℝ+) → ∃𝑏 ∈ ((𝐴 ∩ (𝐵(,)+∞)) ∖ {𝐵})(abs‘(𝑏 − 𝐵)) < if(𝑧 ≤ 𝑣, 𝑧, 𝑣))
97		eldifi 4127	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝑏 ∈ ((𝐴 ∩ (𝐵(,)+∞)) ∖ {𝐵}) → 𝑏 ∈ (𝐴 ∩ (𝐵(,)+∞)))
98	75, 97	sselid 3980	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝑏 ∈ ((𝐴 ∩ (𝐵(,)+∞)) ∖ {𝐵}) → 𝑏 ∈ ℝ)
99	73	sselda 3982	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ ((𝜑 ∧ 𝑏 ∈ ℝ) → 𝑏 ∈ ℂ)
100	56	adantr 479	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ ((𝜑 ∧ 𝑏 ∈ ℝ) → 𝐵 ∈ ℂ)
101	99, 100	subcld 11609	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ ((𝜑 ∧ 𝑏 ∈ ℝ) → (𝑏 − 𝐵) ∈ ℂ)
102	101	abscld 15423	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ ((𝜑 ∧ 𝑏 ∈ ℝ) → (abs‘(𝑏 − 𝐵)) ∈ ℝ)
103	102	3ad2antl1 1182	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ (((𝜑 ∧ 𝑧 ∈ ℝ+ ∧ 𝑣 ∈ ℝ+) ∧ 𝑏 ∈ ℝ) → (abs‘(𝑏 − 𝐵)) ∈ ℝ)
104	103	adantr 479	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ ((((𝜑 ∧ 𝑧 ∈ ℝ+ ∧ 𝑣 ∈ ℝ+) ∧ 𝑏 ∈ ℝ) ∧ (abs‘(𝑏 − 𝐵)) < if(𝑧 ≤ 𝑣, 𝑧, 𝑣)) → (abs‘(𝑏 − 𝐵)) ∈ ℝ)
105	95	rpred 13056	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ ((𝜑 ∧ 𝑧 ∈ ℝ+ ∧ 𝑣 ∈ ℝ+) → if(𝑧 ≤ 𝑣, 𝑧, 𝑣) ∈ ℝ)
106	105	ad2antrr 724	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ ((((𝜑 ∧ 𝑧 ∈ ℝ+ ∧ 𝑣 ∈ ℝ+) ∧ 𝑏 ∈ ℝ) ∧ (abs‘(𝑏 − 𝐵)) < if(𝑧 ≤ 𝑣, 𝑧, 𝑣)) → if(𝑧 ≤ 𝑣, 𝑧, 𝑣) ∈ ℝ)
107		rpre 13022	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ (𝑧 ∈ ℝ+ → 𝑧 ∈ ℝ)
108	107	3ad2ant2 1131	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ ((𝜑 ∧ 𝑧 ∈ ℝ+ ∧ 𝑣 ∈ ℝ+) → 𝑧 ∈ ℝ)
109	108	ad2antrr 724	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ ((((𝜑 ∧ 𝑧 ∈ ℝ+ ∧ 𝑣 ∈ ℝ+) ∧ 𝑏 ∈ ℝ) ∧ (abs‘(𝑏 − 𝐵)) < if(𝑧 ≤ 𝑣, 𝑧, 𝑣)) → 𝑧 ∈ ℝ)
110		simpr 483	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ ((((𝜑 ∧ 𝑧 ∈ ℝ+ ∧ 𝑣 ∈ ℝ+) ∧ 𝑏 ∈ ℝ) ∧ (abs‘(𝑏 − 𝐵)) < if(𝑧 ≤ 𝑣, 𝑧, 𝑣)) → (abs‘(𝑏 − 𝐵)) < if(𝑧 ≤ 𝑣, 𝑧, 𝑣))
111		rpre 13022	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ (𝑣 ∈ ℝ+ → 𝑣 ∈ ℝ)
112		min1 13208	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ ((𝑧 ∈ ℝ ∧ 𝑣 ∈ ℝ) → if(𝑧 ≤ 𝑣, 𝑧, 𝑣) ≤ 𝑧)
113	107, 111, 112	syl2an 594	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ ((𝑧 ∈ ℝ+ ∧ 𝑣 ∈ ℝ+) → if(𝑧 ≤ 𝑣, 𝑧, 𝑣) ≤ 𝑧)
114	113	3adant1 1127	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ ((𝜑 ∧ 𝑧 ∈ ℝ+ ∧ 𝑣 ∈ ℝ+) → if(𝑧 ≤ 𝑣, 𝑧, 𝑣) ≤ 𝑧)
115	114	ad2antrr 724	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ ((((𝜑 ∧ 𝑧 ∈ ℝ+ ∧ 𝑣 ∈ ℝ+) ∧ 𝑏 ∈ ℝ) ∧ (abs‘(𝑏 − 𝐵)) < if(𝑧 ≤ 𝑣, 𝑧, 𝑣)) → if(𝑧 ≤ 𝑣, 𝑧, 𝑣) ≤ 𝑧)
116	104, 106, 109, 110, 115	ltletrd 11412	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ((((𝜑 ∧ 𝑧 ∈ ℝ+ ∧ 𝑣 ∈ ℝ+) ∧ 𝑏 ∈ ℝ) ∧ (abs‘(𝑏 − 𝐵)) < if(𝑧 ≤ 𝑣, 𝑧, 𝑣)) → (abs‘(𝑏 − 𝐵)) < 𝑧)
117	111	3ad2ant3 1132	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ ((𝜑 ∧ 𝑧 ∈ ℝ+ ∧ 𝑣 ∈ ℝ+) → 𝑣 ∈ ℝ)
118	117	ad2antrr 724	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ ((((𝜑 ∧ 𝑧 ∈ ℝ+ ∧ 𝑣 ∈ ℝ+) ∧ 𝑏 ∈ ℝ) ∧ (abs‘(𝑏 − 𝐵)) < if(𝑧 ≤ 𝑣, 𝑧, 𝑣)) → 𝑣 ∈ ℝ)
119	109, 118	min2d 44884	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ ((((𝜑 ∧ 𝑧 ∈ ℝ+ ∧ 𝑣 ∈ ℝ+) ∧ 𝑏 ∈ ℝ) ∧ (abs‘(𝑏 − 𝐵)) < if(𝑧 ≤ 𝑣, 𝑧, 𝑣)) → if(𝑧 ≤ 𝑣, 𝑧, 𝑣) ≤ 𝑣)
120	104, 106, 118, 110, 119	ltletrd 11412	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ((((𝜑 ∧ 𝑧 ∈ ℝ+ ∧ 𝑣 ∈ ℝ+) ∧ 𝑏 ∈ ℝ) ∧ (abs‘(𝑏 − 𝐵)) < if(𝑧 ≤ 𝑣, 𝑧, 𝑣)) → (abs‘(𝑏 − 𝐵)) < 𝑣)
121	116, 120	jca 510	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((((𝜑 ∧ 𝑧 ∈ ℝ+ ∧ 𝑣 ∈ ℝ+) ∧ 𝑏 ∈ ℝ) ∧ (abs‘(𝑏 − 𝐵)) < if(𝑧 ≤ 𝑣, 𝑧, 𝑣)) → ((abs‘(𝑏 − 𝐵)) < 𝑧 ∧ (abs‘(𝑏 − 𝐵)) < 𝑣))
122	121	ex 411	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (((𝜑 ∧ 𝑧 ∈ ℝ+ ∧ 𝑣 ∈ ℝ+) ∧ 𝑏 ∈ ℝ) → ((abs‘(𝑏 − 𝐵)) < if(𝑧 ≤ 𝑣, 𝑧, 𝑣) → ((abs‘(𝑏 − 𝐵)) < 𝑧 ∧ (abs‘(𝑏 − 𝐵)) < 𝑣)))
123	98, 122	sylan2 591	. . . . . . . . . . . . . . . . . . . . . . . . 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 1368	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((𝜑 ∧ 𝑦 ∈ ℝ+) ∧ 𝑧 ∈ ℝ+ ∧ ∀𝑤 ∈ 𝐴 ((𝑤 ≠ 𝐵 ∧ (abs‘(𝑤 − 𝐵)) < 𝑧) → (abs‘((𝐹‘𝑤) − 𝑥)) < 𝑦)) ∧ 𝑣 ∈ ℝ+ ∧ ∀𝑤 ∈ (𝐴 ∩ (𝐵(,)+∞))((𝑤 ≠ 𝐵 ∧ (abs‘(𝑤 − 𝐵)) < 𝑣) → (abs‘(((𝐹 ↾ (𝐵(,)+∞))‘𝑤) − 𝑅)) < 𝑦)) → ∃𝑏 ∈ ((𝐴 ∩ (𝐵(,)+∞)) ∖ {𝐵})((abs‘(𝑏 − 𝐵)) < 𝑧 ∧ (abs‘(𝑏 − 𝐵)) < 𝑣))
127		nfv 1909	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ Ⅎ𝑏(((𝜑 ∧ 𝑦 ∈ ℝ+) ∧ 𝑧 ∈ ℝ+ ∧ ∀𝑤 ∈ 𝐴 ((𝑤 ≠ 𝐵 ∧ (abs‘(𝑤 − 𝐵)) < 𝑧) → (abs‘((𝐹‘𝑤) − 𝑥)) < 𝑦)) ∧ 𝑣 ∈ ℝ+ ∧ ∀𝑤 ∈ (𝐴 ∩ (𝐵(,)+∞))((𝑤 ≠ 𝐵 ∧ (abs‘(𝑤 − 𝐵)) < 𝑣) → (abs‘(((𝐹 ↾ (𝐵(,)+∞))‘𝑤) − 𝑅)) < 𝑦))
128		nfre1 3280	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ Ⅎ𝑏∃𝑏 ∈ 𝐴 ((abs‘((𝐹‘𝑏) − 𝑥)) < 𝑦 ∧ (abs‘((𝐹‘𝑏) − 𝑅)) < 𝑦)
129	97	elin1d 4200	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝑏 ∈ ((𝐴 ∩ (𝐵(,)+∞)) ∖ {𝐵}) → 𝑏 ∈ 𝐴)
130	129	3ad2ant2 1131	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((((𝜑 ∧ 𝑦 ∈ ℝ+) ∧ 𝑧 ∈ ℝ+ ∧ ∀𝑤 ∈ 𝐴 ((𝑤 ≠ 𝐵 ∧ (abs‘(𝑤 − 𝐵)) < 𝑧) → (abs‘((𝐹‘𝑤) − 𝑥)) < 𝑦)) ∧ 𝑣 ∈ ℝ+ ∧ ∀𝑤 ∈ (𝐴 ∩ (𝐵(,)+∞))((𝑤 ≠ 𝐵 ∧ (abs‘(𝑤 − 𝐵)) < 𝑣) → (abs‘(((𝐹 ↾ (𝐵(,)+∞))‘𝑤) − 𝑅)) < 𝑦)) ∧ 𝑏 ∈ ((𝐴 ∩ (𝐵(,)+∞)) ∖ {𝐵}) ∧ ((abs‘(𝑏 − 𝐵)) < 𝑧 ∧ (abs‘(𝑏 − 𝐵)) < 𝑣)) → 𝑏 ∈ 𝐴)
131		simp113 1301	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (((((𝜑 ∧ 𝑦 ∈ ℝ+) ∧ 𝑧 ∈ ℝ+ ∧ ∀𝑤 ∈ 𝐴 ((𝑤 ≠ 𝐵 ∧ (abs‘(𝑤 − 𝐵)) < 𝑧) → (abs‘((𝐹‘𝑤) − 𝑥)) < 𝑦)) ∧ 𝑣 ∈ ℝ+ ∧ ∀𝑤 ∈ (𝐴 ∩ (𝐵(,)+∞))((𝑤 ≠ 𝐵 ∧ (abs‘(𝑤 − 𝐵)) < 𝑣) → (abs‘(((𝐹 ↾ (𝐵(,)+∞))‘𝑤) − 𝑅)) < 𝑦)) ∧ 𝑏 ∈ ((𝐴 ∩ (𝐵(,)+∞)) ∖ {𝐵}) ∧ ((abs‘(𝑏 − 𝐵)) < 𝑧 ∧ (abs‘(𝑏 − 𝐵)) < 𝑣)) → ∀𝑤 ∈ 𝐴 ((𝑤 ≠ 𝐵 ∧ (abs‘(𝑤 − 𝐵)) < 𝑧) → (abs‘((𝐹‘𝑤) − 𝑥)) < 𝑦))
132		eldifsni 4798	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (𝑏 ∈ ((𝐴 ∩ (𝐵(,)+∞)) ∖ {𝐵}) → 𝑏 ≠ 𝐵)
133	132	adantr 479	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ((𝑏 ∈ ((𝐴 ∩ (𝐵(,)+∞)) ∖ {𝐵}) ∧ ((abs‘(𝑏 − 𝐵)) < 𝑧 ∧ (abs‘(𝑏 − 𝐵)) < 𝑣)) → 𝑏 ≠ 𝐵)
134		simprl 769	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ((𝑏 ∈ ((𝐴 ∩ (𝐵(,)+∞)) ∖ {𝐵}) ∧ ((abs‘(𝑏 − 𝐵)) < 𝑧 ∧ (abs‘(𝑏 − 𝐵)) < 𝑣)) → (abs‘(𝑏 − 𝐵)) < 𝑧)
135	133, 134	jca 510	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((𝑏 ∈ ((𝐴 ∩ (𝐵(,)+∞)) ∖ {𝐵}) ∧ ((abs‘(𝑏 − 𝐵)) < 𝑧 ∧ (abs‘(𝑏 − 𝐵)) < 𝑣)) → (𝑏 ≠ 𝐵 ∧ (abs‘(𝑏 − 𝐵)) < 𝑧))
136	135	3adant1 1127	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (((((𝜑 ∧ 𝑦 ∈ ℝ+) ∧ 𝑧 ∈ ℝ+ ∧ ∀𝑤 ∈ 𝐴 ((𝑤 ≠ 𝐵 ∧ (abs‘(𝑤 − 𝐵)) < 𝑧) → (abs‘((𝐹‘𝑤) − 𝑥)) < 𝑦)) ∧ 𝑣 ∈ ℝ+ ∧ ∀𝑤 ∈ (𝐴 ∩ (𝐵(,)+∞))((𝑤 ≠ 𝐵 ∧ (abs‘(𝑤 − 𝐵)) < 𝑣) → (abs‘(((𝐹 ↾ (𝐵(,)+∞))‘𝑤) − 𝑅)) < 𝑦)) ∧ 𝑏 ∈ ((𝐴 ∩ (𝐵(,)+∞)) ∖ {𝐵}) ∧ ((abs‘(𝑏 − 𝐵)) < 𝑧 ∧ (abs‘(𝑏 − 𝐵)) < 𝑣)) → (𝑏 ≠ 𝐵 ∧ (abs‘(𝑏 − 𝐵)) < 𝑧))
137		neeq1 3000	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ (𝑤 = 𝑏 → (𝑤 ≠ 𝐵 ↔ 𝑏 ≠ 𝐵))
138		fvoveq1 7449	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ (𝑤 = 𝑏 → (abs‘(𝑤 − 𝐵)) = (abs‘(𝑏 − 𝐵)))
139	138	breq1d 5162	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ (𝑤 = 𝑏 → ((abs‘(𝑤 − 𝐵)) < 𝑧 ↔ (abs‘(𝑏 − 𝐵)) < 𝑧))
140	137, 139	anbi12d 630	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (𝑤 = 𝑏 → ((𝑤 ≠ 𝐵 ∧ (abs‘(𝑤 − 𝐵)) < 𝑧) ↔ (𝑏 ≠ 𝐵 ∧ (abs‘(𝑏 − 𝐵)) < 𝑧)))
141	140	imbrov2fvoveq 7451	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (𝑤 = 𝑏 → (((𝑤 ≠ 𝐵 ∧ (abs‘(𝑤 − 𝐵)) < 𝑧) → (abs‘((𝐹‘𝑤) − 𝑥)) < 𝑦) ↔ ((𝑏 ≠ 𝐵 ∧ (abs‘(𝑏 − 𝐵)) < 𝑧) → (abs‘((𝐹‘𝑏) − 𝑥)) < 𝑦)))
142	141	rspcva 3609	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((𝑏 ∈ 𝐴 ∧ ∀𝑤 ∈ 𝐴 ((𝑤 ≠ 𝐵 ∧ (abs‘(𝑤 − 𝐵)) < 𝑧) → (abs‘((𝐹‘𝑤) − 𝑥)) < 𝑦)) → ((𝑏 ≠ 𝐵 ∧ (abs‘(𝑏 − 𝐵)) < 𝑧) → (abs‘((𝐹‘𝑏) − 𝑥)) < 𝑦))
143	142	imp 405	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (((𝑏 ∈ 𝐴 ∧ ∀𝑤 ∈ 𝐴 ((𝑤 ≠ 𝐵 ∧ (abs‘(𝑤 − 𝐵)) < 𝑧) → (abs‘((𝐹‘𝑤) − 𝑥)) < 𝑦)) ∧ (𝑏 ≠ 𝐵 ∧ (abs‘(𝑏 − 𝐵)) < 𝑧)) → (abs‘((𝐹‘𝑏) − 𝑥)) < 𝑦)
144	130, 131, 136, 143	syl21anc 836	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((((𝜑 ∧ 𝑦 ∈ ℝ+) ∧ 𝑧 ∈ ℝ+ ∧ ∀𝑤 ∈ 𝐴 ((𝑤 ≠ 𝐵 ∧ (abs‘(𝑤 − 𝐵)) < 𝑧) → (abs‘((𝐹‘𝑤) − 𝑥)) < 𝑦)) ∧ 𝑣 ∈ ℝ+ ∧ ∀𝑤 ∈ (𝐴 ∩ (𝐵(,)+∞))((𝑤 ≠ 𝐵 ∧ (abs‘(𝑤 − 𝐵)) < 𝑣) → (abs‘(((𝐹 ↾ (𝐵(,)+∞))‘𝑤) − 𝑅)) < 𝑦)) ∧ 𝑏 ∈ ((𝐴 ∩ (𝐵(,)+∞)) ∖ {𝐵}) ∧ ((abs‘(𝑏 − 𝐵)) < 𝑧 ∧ (abs‘(𝑏 − 𝐵)) < 𝑣)) → (abs‘((𝐹‘𝑏) − 𝑥)) < 𝑦)
145	97	3ad2ant2 1131	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (((((𝜑 ∧ 𝑦 ∈ ℝ+) ∧ 𝑧 ∈ ℝ+ ∧ ∀𝑤 ∈ 𝐴 ((𝑤 ≠ 𝐵 ∧ (abs‘(𝑤 − 𝐵)) < 𝑧) → (abs‘((𝐹‘𝑤) − 𝑥)) < 𝑦)) ∧ 𝑣 ∈ ℝ+ ∧ ∀𝑤 ∈ (𝐴 ∩ (𝐵(,)+∞))((𝑤 ≠ 𝐵 ∧ (abs‘(𝑤 − 𝐵)) < 𝑣) → (abs‘(((𝐹 ↾ (𝐵(,)+∞))‘𝑤) − 𝑅)) < 𝑦)) ∧ 𝑏 ∈ ((𝐴 ∩ (𝐵(,)+∞)) ∖ {𝐵}) ∧ ((abs‘(𝑏 − 𝐵)) < 𝑧 ∧ (abs‘(𝑏 − 𝐵)) < 𝑣)) → 𝑏 ∈ (𝐴 ∩ (𝐵(,)+∞)))
146	62	3ad2ant1 1130	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (((((𝜑 ∧ 𝑦 ∈ ℝ+) ∧ 𝑧 ∈ ℝ+ ∧ ∀𝑤 ∈ 𝐴 ((𝑤 ≠ 𝐵 ∧ (abs‘(𝑤 − 𝐵)) < 𝑧) → (abs‘((𝐹‘𝑤) − 𝑥)) < 𝑦)) ∧ 𝑣 ∈ ℝ+ ∧ ∀𝑤 ∈ (𝐴 ∩ (𝐵(,)+∞))((𝑤 ≠ 𝐵 ∧ (abs‘(𝑤 − 𝐵)) < 𝑣) → (abs‘(((𝐹 ↾ (𝐵(,)+∞))‘𝑤) − 𝑅)) < 𝑦)) ∧ 𝑏 ∈ ((𝐴 ∩ (𝐵(,)+∞)) ∖ {𝐵}) ∧ ((abs‘(𝑏 − 𝐵)) < 𝑧 ∧ (abs‘(𝑏 − 𝐵)) < 𝑣)) → 𝜑)
147		simp13 1202	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (((((𝜑 ∧ 𝑦 ∈ ℝ+) ∧ 𝑧 ∈ ℝ+ ∧ ∀𝑤 ∈ 𝐴 ((𝑤 ≠ 𝐵 ∧ (abs‘(𝑤 − 𝐵)) < 𝑧) → (abs‘((𝐹‘𝑤) − 𝑥)) < 𝑦)) ∧ 𝑣 ∈ ℝ+ ∧ ∀𝑤 ∈ (𝐴 ∩ (𝐵(,)+∞))((𝑤 ≠ 𝐵 ∧ (abs‘(𝑤 − 𝐵)) < 𝑣) → (abs‘(((𝐹 ↾ (𝐵(,)+∞))‘𝑤) − 𝑅)) < 𝑦)) ∧ 𝑏 ∈ ((𝐴 ∩ (𝐵(,)+∞)) ∖ {𝐵}) ∧ ((abs‘(𝑏 − 𝐵)) < 𝑧 ∧ (abs‘(𝑏 − 𝐵)) < 𝑣)) → ∀𝑤 ∈ (𝐴 ∩ (𝐵(,)+∞))((𝑤 ≠ 𝐵 ∧ (abs‘(𝑤 − 𝐵)) < 𝑣) → (abs‘(((𝐹 ↾ (𝐵(,)+∞))‘𝑤) − 𝑅)) < 𝑦))
148		nfv 1909	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ Ⅎ𝑤𝜑
149		nfra1 3279	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ Ⅎ𝑤∀𝑤 ∈ (𝐴 ∩ (𝐵(,)+∞))((𝑤 ≠ 𝐵 ∧ (abs‘(𝑤 − 𝐵)) < 𝑣) → (abs‘(((𝐹 ↾ (𝐵(,)+∞))‘𝑤) − 𝑅)) < 𝑦)
150	148, 149	nfan 1894	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ Ⅎ𝑤(𝜑 ∧ ∀𝑤 ∈ (𝐴 ∩ (𝐵(,)+∞))((𝑤 ≠ 𝐵 ∧ (abs‘(𝑤 − 𝐵)) < 𝑣) → (abs‘(((𝐹 ↾ (𝐵(,)+∞))‘𝑤) − 𝑅)) < 𝑦))
151		elinel2 4198	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ (𝑤 ∈ (𝐴 ∩ (𝐵(,)+∞)) → 𝑤 ∈ (𝐵(,)+∞))
152	151	fvresd 6922	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ (𝑤 ∈ (𝐴 ∩ (𝐵(,)+∞)) → ((𝐹 ↾ (𝐵(,)+∞))‘𝑤) = (𝐹‘𝑤))
153	152	eqcomd 2734	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ (𝑤 ∈ (𝐴 ∩ (𝐵(,)+∞)) → (𝐹‘𝑤) = ((𝐹 ↾ (𝐵(,)+∞))‘𝑤))
154	153	fvoveq1d 7448	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ (𝑤 ∈ (𝐴 ∩ (𝐵(,)+∞)) → (abs‘((𝐹‘𝑤) − 𝑅)) = (abs‘(((𝐹 ↾ (𝐵(,)+∞))‘𝑤) − 𝑅)))
155	154	3ad2ant2 1131	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ (((𝜑 ∧ ∀𝑤 ∈ (𝐴 ∩ (𝐵(,)+∞))((𝑤 ≠ 𝐵 ∧ (abs‘(𝑤 − 𝐵)) < 𝑣) → (abs‘(((𝐹 ↾ (𝐵(,)+∞))‘𝑤) − 𝑅)) < 𝑦)) ∧ 𝑤 ∈ (𝐴 ∩ (𝐵(,)+∞)) ∧ (𝑤 ≠ 𝐵 ∧ (abs‘(𝑤 − 𝐵)) < 𝑣)) → (abs‘((𝐹‘𝑤) − 𝑅)) = (abs‘(((𝐹 ↾ (𝐵(,)+∞))‘𝑤) − 𝑅)))
156		rspa 3243	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ ((∀𝑤 ∈ (𝐴 ∩ (𝐵(,)+∞))((𝑤 ≠ 𝐵 ∧ (abs‘(𝑤 − 𝐵)) < 𝑣) → (abs‘(((𝐹 ↾ (𝐵(,)+∞))‘𝑤) − 𝑅)) < 𝑦) ∧ 𝑤 ∈ (𝐴 ∩ (𝐵(,)+∞))) → ((𝑤 ≠ 𝐵 ∧ (abs‘(𝑤 − 𝐵)) < 𝑣) → (abs‘(((𝐹 ↾ (𝐵(,)+∞))‘𝑤) − 𝑅)) < 𝑦))
157	156	3impia 1114	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ ((∀𝑤 ∈ (𝐴 ∩ (𝐵(,)+∞))((𝑤 ≠ 𝐵 ∧ (abs‘(𝑤 − 𝐵)) < 𝑣) → (abs‘(((𝐹 ↾ (𝐵(,)+∞))‘𝑤) − 𝑅)) < 𝑦) ∧ 𝑤 ∈ (𝐴 ∩ (𝐵(,)+∞)) ∧ (𝑤 ≠ 𝐵 ∧ (abs‘(𝑤 − 𝐵)) < 𝑣)) → (abs‘(((𝐹 ↾ (𝐵(,)+∞))‘𝑤) − 𝑅)) < 𝑦)
158	157	3adant1l 1173	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ (((𝜑 ∧ ∀𝑤 ∈ (𝐴 ∩ (𝐵(,)+∞))((𝑤 ≠ 𝐵 ∧ (abs‘(𝑤 − 𝐵)) < 𝑣) → (abs‘(((𝐹 ↾ (𝐵(,)+∞))‘𝑤) − 𝑅)) < 𝑦)) ∧ 𝑤 ∈ (𝐴 ∩ (𝐵(,)+∞)) ∧ (𝑤 ≠ 𝐵 ∧ (abs‘(𝑤 − 𝐵)) < 𝑣)) → (abs‘(((𝐹 ↾ (𝐵(,)+∞))‘𝑤) − 𝑅)) < 𝑦)
159	155, 158	eqbrtrd 5174	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (((𝜑 ∧ ∀𝑤 ∈ (𝐴 ∩ (𝐵(,)+∞))((𝑤 ≠ 𝐵 ∧ (abs‘(𝑤 − 𝐵)) < 𝑣) → (abs‘(((𝐹 ↾ (𝐵(,)+∞))‘𝑤) − 𝑅)) < 𝑦)) ∧ 𝑤 ∈ (𝐴 ∩ (𝐵(,)+∞)) ∧ (𝑤 ≠ 𝐵 ∧ (abs‘(𝑤 − 𝐵)) < 𝑣)) → (abs‘((𝐹‘𝑤) − 𝑅)) < 𝑦)
160	159	3exp 1116	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ((𝜑 ∧ ∀𝑤 ∈ (𝐴 ∩ (𝐵(,)+∞))((𝑤 ≠ 𝐵 ∧ (abs‘(𝑤 − 𝐵)) < 𝑣) → (abs‘(((𝐹 ↾ (𝐵(,)+∞))‘𝑤) − 𝑅)) < 𝑦)) → (𝑤 ∈ (𝐴 ∩ (𝐵(,)+∞)) → ((𝑤 ≠ 𝐵 ∧ (abs‘(𝑤 − 𝐵)) < 𝑣) → (abs‘((𝐹‘𝑤) − 𝑅)) < 𝑦)))
161	150, 160	ralrimi 3252	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((𝜑 ∧ ∀𝑤 ∈ (𝐴 ∩ (𝐵(,)+∞))((𝑤 ≠ 𝐵 ∧ (abs‘(𝑤 − 𝐵)) < 𝑣) → (abs‘(((𝐹 ↾ (𝐵(,)+∞))‘𝑤) − 𝑅)) < 𝑦)) → ∀𝑤 ∈ (𝐴 ∩ (𝐵(,)+∞))((𝑤 ≠ 𝐵 ∧ (abs‘(𝑤 − 𝐵)) < 𝑣) → (abs‘((𝐹‘𝑤) − 𝑅)) < 𝑦))
162	146, 147, 161	syl2anc 582	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (((((𝜑 ∧ 𝑦 ∈ ℝ+) ∧ 𝑧 ∈ ℝ+ ∧ ∀𝑤 ∈ 𝐴 ((𝑤 ≠ 𝐵 ∧ (abs‘(𝑤 − 𝐵)) < 𝑧) → (abs‘((𝐹‘𝑤) − 𝑥)) < 𝑦)) ∧ 𝑣 ∈ ℝ+ ∧ ∀𝑤 ∈ (𝐴 ∩ (𝐵(,)+∞))((𝑤 ≠ 𝐵 ∧ (abs‘(𝑤 − 𝐵)) < 𝑣) → (abs‘(((𝐹 ↾ (𝐵(,)+∞))‘𝑤) − 𝑅)) < 𝑦)) ∧ 𝑏 ∈ ((𝐴 ∩ (𝐵(,)+∞)) ∖ {𝐵}) ∧ ((abs‘(𝑏 − 𝐵)) < 𝑧 ∧ (abs‘(𝑏 − 𝐵)) < 𝑣)) → ∀𝑤 ∈ (𝐴 ∩ (𝐵(,)+∞))((𝑤 ≠ 𝐵 ∧ (abs‘(𝑤 − 𝐵)) < 𝑣) → (abs‘((𝐹‘𝑤) − 𝑅)) < 𝑦))
163	132	anim1i 613	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ((𝑏 ∈ ((𝐴 ∩ (𝐵(,)+∞)) ∖ {𝐵}) ∧ (abs‘(𝑏 − 𝐵)) < 𝑣) → (𝑏 ≠ 𝐵 ∧ (abs‘(𝑏 − 𝐵)) < 𝑣))
164	163	adantrl 714	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((𝑏 ∈ ((𝐴 ∩ (𝐵(,)+∞)) ∖ {𝐵}) ∧ ((abs‘(𝑏 − 𝐵)) < 𝑧 ∧ (abs‘(𝑏 − 𝐵)) < 𝑣)) → (𝑏 ≠ 𝐵 ∧ (abs‘(𝑏 − 𝐵)) < 𝑣))
165	164	3adant1 1127	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (((((𝜑 ∧ 𝑦 ∈ ℝ+) ∧ 𝑧 ∈ ℝ+ ∧ ∀𝑤 ∈ 𝐴 ((𝑤 ≠ 𝐵 ∧ (abs‘(𝑤 − 𝐵)) < 𝑧) → (abs‘((𝐹‘𝑤) − 𝑥)) < 𝑦)) ∧ 𝑣 ∈ ℝ+ ∧ ∀𝑤 ∈ (𝐴 ∩ (𝐵(,)+∞))((𝑤 ≠ 𝐵 ∧ (abs‘(𝑤 − 𝐵)) < 𝑣) → (abs‘(((𝐹 ↾ (𝐵(,)+∞))‘𝑤) − 𝑅)) < 𝑦)) ∧ 𝑏 ∈ ((𝐴 ∩ (𝐵(,)+∞)) ∖ {𝐵}) ∧ ((abs‘(𝑏 − 𝐵)) < 𝑧 ∧ (abs‘(𝑏 − 𝐵)) < 𝑣)) → (𝑏 ≠ 𝐵 ∧ (abs‘(𝑏 − 𝐵)) < 𝑣))
166	138	breq1d 5162	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ (𝑤 = 𝑏 → ((abs‘(𝑤 − 𝐵)) < 𝑣 ↔ (abs‘(𝑏 − 𝐵)) < 𝑣))
167	137, 166	anbi12d 630	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (𝑤 = 𝑏 → ((𝑤 ≠ 𝐵 ∧ (abs‘(𝑤 − 𝐵)) < 𝑣) ↔ (𝑏 ≠ 𝐵 ∧ (abs‘(𝑏 − 𝐵)) < 𝑣)))
168	167	imbrov2fvoveq 7451	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (𝑤 = 𝑏 → (((𝑤 ≠ 𝐵 ∧ (abs‘(𝑤 − 𝐵)) < 𝑣) → (abs‘((𝐹‘𝑤) − 𝑅)) < 𝑦) ↔ ((𝑏 ≠ 𝐵 ∧ (abs‘(𝑏 − 𝐵)) < 𝑣) → (abs‘((𝐹‘𝑏) − 𝑅)) < 𝑦)))
169	168	rspcva 3609	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((𝑏 ∈ (𝐴 ∩ (𝐵(,)+∞)) ∧ ∀𝑤 ∈ (𝐴 ∩ (𝐵(,)+∞))((𝑤 ≠ 𝐵 ∧ (abs‘(𝑤 − 𝐵)) < 𝑣) → (abs‘((𝐹‘𝑤) − 𝑅)) < 𝑦)) → ((𝑏 ≠ 𝐵 ∧ (abs‘(𝑏 − 𝐵)) < 𝑣) → (abs‘((𝐹‘𝑏) − 𝑅)) < 𝑦))
170	169	imp 405	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (((𝑏 ∈ (𝐴 ∩ (𝐵(,)+∞)) ∧ ∀𝑤 ∈ (𝐴 ∩ (𝐵(,)+∞))((𝑤 ≠ 𝐵 ∧ (abs‘(𝑤 − 𝐵)) < 𝑣) → (abs‘((𝐹‘𝑤) − 𝑅)) < 𝑦)) ∧ (𝑏 ≠ 𝐵 ∧ (abs‘(𝑏 − 𝐵)) < 𝑣)) → (abs‘((𝐹‘𝑏) − 𝑅)) < 𝑦)
171	145, 162, 165, 170	syl21anc 836	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((((𝜑 ∧ 𝑦 ∈ ℝ+) ∧ 𝑧 ∈ ℝ+ ∧ ∀𝑤 ∈ 𝐴 ((𝑤 ≠ 𝐵 ∧ (abs‘(𝑤 − 𝐵)) < 𝑧) → (abs‘((𝐹‘𝑤) − 𝑥)) < 𝑦)) ∧ 𝑣 ∈ ℝ+ ∧ ∀𝑤 ∈ (𝐴 ∩ (𝐵(,)+∞))((𝑤 ≠ 𝐵 ∧ (abs‘(𝑤 − 𝐵)) < 𝑣) → (abs‘(((𝐹 ↾ (𝐵(,)+∞))‘𝑤) − 𝑅)) < 𝑦)) ∧ 𝑏 ∈ ((𝐴 ∩ (𝐵(,)+∞)) ∖ {𝐵}) ∧ ((abs‘(𝑏 − 𝐵)) < 𝑧 ∧ (abs‘(𝑏 − 𝐵)) < 𝑣)) → (abs‘((𝐹‘𝑏) − 𝑅)) < 𝑦)
172		rspe 3244	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((𝑏 ∈ 𝐴 ∧ ((abs‘((𝐹‘𝑏) − 𝑥)) < 𝑦 ∧ (abs‘((𝐹‘𝑏) − 𝑅)) < 𝑦)) → ∃𝑏 ∈ 𝐴 ((abs‘((𝐹‘𝑏) − 𝑥)) < 𝑦 ∧ (abs‘((𝐹‘𝑏) − 𝑅)) < 𝑦))
173	130, 144, 171, 172	syl12anc 835	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((((𝜑 ∧ 𝑦 ∈ ℝ+) ∧ 𝑧 ∈ ℝ+ ∧ ∀𝑤 ∈ 𝐴 ((𝑤 ≠ 𝐵 ∧ (abs‘(𝑤 − 𝐵)) < 𝑧) → (abs‘((𝐹‘𝑤) − 𝑥)) < 𝑦)) ∧ 𝑣 ∈ ℝ+ ∧ ∀𝑤 ∈ (𝐴 ∩ (𝐵(,)+∞))((𝑤 ≠ 𝐵 ∧ (abs‘(𝑤 − 𝐵)) < 𝑣) → (abs‘(((𝐹 ↾ (𝐵(,)+∞))‘𝑤) − 𝑅)) < 𝑦)) ∧ 𝑏 ∈ ((𝐴 ∩ (𝐵(,)+∞)) ∖ {𝐵}) ∧ ((abs‘(𝑏 − 𝐵)) < 𝑧 ∧ (abs‘(𝑏 − 𝐵)) < 𝑣)) → ∃𝑏 ∈ 𝐴 ((abs‘((𝐹‘𝑏) − 𝑥)) < 𝑦 ∧ (abs‘((𝐹‘𝑏) − 𝑅)) < 𝑦))
174	173	3exp 1116	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((((𝜑 ∧ 𝑦 ∈ ℝ+) ∧ 𝑧 ∈ ℝ+ ∧ ∀𝑤 ∈ 𝐴 ((𝑤 ≠ 𝐵 ∧ (abs‘(𝑤 − 𝐵)) < 𝑧) → (abs‘((𝐹‘𝑤) − 𝑥)) < 𝑦)) ∧ 𝑣 ∈ ℝ+ ∧ ∀𝑤 ∈ (𝐴 ∩ (𝐵(,)+∞))((𝑤 ≠ 𝐵 ∧ (abs‘(𝑤 − 𝐵)) < 𝑣) → (abs‘(((𝐹 ↾ (𝐵(,)+∞))‘𝑤) − 𝑅)) < 𝑦)) → (𝑏 ∈ ((𝐴 ∩ (𝐵(,)+∞)) ∖ {𝐵}) → (((abs‘(𝑏 − 𝐵)) < 𝑧 ∧ (abs‘(𝑏 − 𝐵)) < 𝑣) → ∃𝑏 ∈ 𝐴 ((abs‘((𝐹‘𝑏) − 𝑥)) < 𝑦 ∧ (abs‘((𝐹‘𝑏) − 𝑅)) < 𝑦))))
175	127, 128, 174	rexlimd 3261	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((𝜑 ∧ 𝑦 ∈ ℝ+) ∧ 𝑧 ∈ ℝ+ ∧ ∀𝑤 ∈ 𝐴 ((𝑤 ≠ 𝐵 ∧ (abs‘(𝑤 − 𝐵)) < 𝑧) → (abs‘((𝐹‘𝑤) − 𝑥)) < 𝑦)) ∧ 𝑣 ∈ ℝ+ ∧ ∀𝑤 ∈ (𝐴 ∩ (𝐵(,)+∞))((𝑤 ≠ 𝐵 ∧ (abs‘(𝑤 − 𝐵)) < 𝑣) → (abs‘(((𝐹 ↾ (𝐵(,)+∞))‘𝑤) − 𝑅)) < 𝑦)) → (∃𝑏 ∈ ((𝐴 ∩ (𝐵(,)+∞)) ∖ {𝐵})((abs‘(𝑏 − 𝐵)) < 𝑧 ∧ (abs‘(𝑏 − 𝐵)) < 𝑣) → ∃𝑏 ∈ 𝐴 ((abs‘((𝐹‘𝑏) − 𝑥)) < 𝑦 ∧ (abs‘((𝐹‘𝑏) − 𝑅)) < 𝑦)))
176	126, 175	mpd 15	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((𝜑 ∧ 𝑦 ∈ ℝ+) ∧ 𝑧 ∈ ℝ+ ∧ ∀𝑤 ∈ 𝐴 ((𝑤 ≠ 𝐵 ∧ (abs‘(𝑤 − 𝐵)) < 𝑧) → (abs‘((𝐹‘𝑤) − 𝑥)) < 𝑦)) ∧ 𝑣 ∈ ℝ+ ∧ ∀𝑤 ∈ (𝐴 ∩ (𝐵(,)+∞))((𝑤 ≠ 𝐵 ∧ (abs‘(𝑤 − 𝐵)) < 𝑣) → (abs‘(((𝐹 ↾ (𝐵(,)+∞))‘𝑤) − 𝑅)) < 𝑦)) → ∃𝑏 ∈ 𝐴 ((abs‘((𝐹‘𝑏) − 𝑥)) < 𝑦 ∧ (abs‘((𝐹‘𝑏) − 𝑅)) < 𝑦))
177	176	3exp 1116	. . . . . . . . . . . . . . . . . . . 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 1116	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑦 ∈ ℝ+) → (𝑧 ∈ ℝ+ → (∀𝑤 ∈ 𝐴 ((𝑤 ≠ 𝐵 ∧ (abs‘(𝑤 − 𝐵)) < 𝑧) → (abs‘((𝐹‘𝑤) − 𝑥)) < 𝑦) → ∃𝑏 ∈ 𝐴 ((abs‘((𝐹‘𝑏) − 𝑥)) < 𝑦 ∧ (abs‘((𝐹‘𝑏) − 𝑅)) < 𝑦))))
181	180	rexlimdv 3150	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑦 ∈ ℝ+) → (∃𝑧 ∈ ℝ+ ∀𝑤 ∈ 𝐴 ((𝑤 ≠ 𝐵 ∧ (abs‘(𝑤 − 𝐵)) < 𝑧) → (abs‘((𝐹‘𝑤) − 𝑥)) < 𝑦) → ∃𝑏 ∈ 𝐴 ((abs‘((𝐹‘𝑏) − 𝑥)) < 𝑦 ∧ (abs‘((𝐹‘𝑏) − 𝑅)) < 𝑦)))
182	181	imp 405	. . . . . . . . . . . . . . 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 11609	. . . . . . . . . . . . . . . . . 18 ⊢ (((((((𝜑 ∧ 𝑥 ∈ ℂ) ∧ 𝑦 ∈ ℝ+) ∧ 𝑎 ∈ 𝐴) ∧ ((abs‘((𝐹‘𝑎) − 𝑥)) < 𝑦 ∧ (abs‘((𝐹‘𝑎) − 𝐿)) < 𝑦)) ∧ 𝑏 ∈ 𝐴) ∧ ((abs‘((𝐹‘𝑏) − 𝑥)) < 𝑦 ∧ (abs‘((𝐹‘𝑏) − 𝑅)) < 𝑦)) → (𝑅 − 𝐿) ∈ ℂ)
188	187	abscld 15423	. . . . . . . . . . . . . . . . 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 7099	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝜑 ∧ 𝑏 ∈ 𝐴) → (𝐹‘𝑏) ∈ ℂ)
192	189, 190, 191	syl2anc 582	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((((((𝜑 ∧ 𝑥 ∈ ℂ) ∧ 𝑦 ∈ ℝ+) ∧ 𝑎 ∈ 𝐴) ∧ ((abs‘((𝐹‘𝑎) − 𝑥)) < 𝑦 ∧ (abs‘((𝐹‘𝑎) − 𝐿)) < 𝑦)) ∧ 𝑏 ∈ 𝐴) ∧ ((abs‘((𝐹‘𝑏) − 𝑥)) < 𝑦 ∧ (abs‘((𝐹‘𝑏) − 𝑅)) < 𝑦)) → (𝐹‘𝑏) ∈ ℂ)
193	185, 192	subcld 11609	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((((((𝜑 ∧ 𝑥 ∈ ℂ) ∧ 𝑦 ∈ ℝ+) ∧ 𝑎 ∈ 𝐴) ∧ ((abs‘((𝐹‘𝑎) − 𝑥)) < 𝑦 ∧ (abs‘((𝐹‘𝑎) − 𝐿)) < 𝑦)) ∧ 𝑏 ∈ 𝐴) ∧ ((abs‘((𝐹‘𝑏) − 𝑥)) < 𝑦 ∧ (abs‘((𝐹‘𝑏) − 𝑅)) < 𝑦)) → (𝑅 − (𝐹‘𝑏)) ∈ ℂ)
194	193	abscld 15423	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((((((𝜑 ∧ 𝑥 ∈ ℂ) ∧ 𝑦 ∈ ℝ+) ∧ 𝑎 ∈ 𝐴) ∧ ((abs‘((𝐹‘𝑎) − 𝑥)) < 𝑦 ∧ (abs‘((𝐹‘𝑎) − 𝐿)) < 𝑦)) ∧ 𝑏 ∈ 𝐴) ∧ ((abs‘((𝐹‘𝑏) − 𝑥)) < 𝑦 ∧ (abs‘((𝐹‘𝑏) − 𝑅)) < 𝑦)) → (abs‘(𝑅 − (𝐹‘𝑏))) ∈ ℝ)
195		simp-6r 786	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((((((𝜑 ∧ 𝑥 ∈ ℂ) ∧ 𝑦 ∈ ℝ+) ∧ 𝑎 ∈ 𝐴) ∧ ((abs‘((𝐹‘𝑎) − 𝑥)) < 𝑦 ∧ (abs‘((𝐹‘𝑎) − 𝐿)) < 𝑦)) ∧ 𝑏 ∈ 𝐴) ∧ ((abs‘((𝐹‘𝑏) − 𝑥)) < 𝑦 ∧ (abs‘((𝐹‘𝑏) − 𝑅)) < 𝑦)) → 𝑥 ∈ ℂ)
196	192, 195	subcld 11609	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((((((𝜑 ∧ 𝑥 ∈ ℂ) ∧ 𝑦 ∈ ℝ+) ∧ 𝑎 ∈ 𝐴) ∧ ((abs‘((𝐹‘𝑎) − 𝑥)) < 𝑦 ∧ (abs‘((𝐹‘𝑎) − 𝐿)) < 𝑦)) ∧ 𝑏 ∈ 𝐴) ∧ ((abs‘((𝐹‘𝑏) − 𝑥)) < 𝑦 ∧ (abs‘((𝐹‘𝑏) − 𝑅)) < 𝑦)) → ((𝐹‘𝑏) − 𝑥) ∈ ℂ)
197	196	abscld 15423	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((((((𝜑 ∧ 𝑥 ∈ ℂ) ∧ 𝑦 ∈ ℝ+) ∧ 𝑎 ∈ 𝐴) ∧ ((abs‘((𝐹‘𝑎) − 𝑥)) < 𝑦 ∧ (abs‘((𝐹‘𝑎) − 𝐿)) < 𝑦)) ∧ 𝑏 ∈ 𝐴) ∧ ((abs‘((𝐹‘𝑏) − 𝑥)) < 𝑦 ∧ (abs‘((𝐹‘𝑏) − 𝑅)) < 𝑦)) → (abs‘((𝐹‘𝑏) − 𝑥)) ∈ ℝ)
198	194, 197	readdcld 11281	. . . . . . . . . . . . . . . . . . 19 ⊢ (((((((𝜑 ∧ 𝑥 ∈ ℂ) ∧ 𝑦 ∈ ℝ+) ∧ 𝑎 ∈ 𝐴) ∧ ((abs‘((𝐹‘𝑎) − 𝑥)) < 𝑦 ∧ (abs‘((𝐹‘𝑎) − 𝐿)) < 𝑦)) ∧ 𝑏 ∈ 𝐴) ∧ ((abs‘((𝐹‘𝑏) − 𝑥)) < 𝑦 ∧ (abs‘((𝐹‘𝑏) − 𝑅)) < 𝑦)) → ((abs‘(𝑅 − (𝐹‘𝑏))) + (abs‘((𝐹‘𝑏) − 𝑥))) ∈ ℝ)
199		simp-4r 782	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((((((𝜑 ∧ 𝑥 ∈ ℂ) ∧ 𝑦 ∈ ℝ+) ∧ 𝑎 ∈ 𝐴) ∧ ((abs‘((𝐹‘𝑎) − 𝑥)) < 𝑦 ∧ (abs‘((𝐹‘𝑎) − 𝐿)) < 𝑦)) ∧ 𝑏 ∈ 𝐴) ∧ ((abs‘((𝐹‘𝑏) − 𝑥)) < 𝑦 ∧ (abs‘((𝐹‘𝑏) − 𝑅)) < 𝑦)) → 𝑎 ∈ 𝐴)
200	36	ffvelcdmda 7099	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝜑 ∧ 𝑎 ∈ 𝐴) → (𝐹‘𝑎) ∈ ℂ)
201	189, 199, 200	syl2anc 582	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((((((𝜑 ∧ 𝑥 ∈ ℂ) ∧ 𝑦 ∈ ℝ+) ∧ 𝑎 ∈ 𝐴) ∧ ((abs‘((𝐹‘𝑎) − 𝑥)) < 𝑦 ∧ (abs‘((𝐹‘𝑎) − 𝐿)) < 𝑦)) ∧ 𝑏 ∈ 𝐴) ∧ ((abs‘((𝐹‘𝑏) − 𝑥)) < 𝑦 ∧ (abs‘((𝐹‘𝑏) − 𝑅)) < 𝑦)) → (𝐹‘𝑎) ∈ ℂ)
202	195, 201	subcld 11609	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((((((𝜑 ∧ 𝑥 ∈ ℂ) ∧ 𝑦 ∈ ℝ+) ∧ 𝑎 ∈ 𝐴) ∧ ((abs‘((𝐹‘𝑎) − 𝑥)) < 𝑦 ∧ (abs‘((𝐹‘𝑎) − 𝐿)) < 𝑦)) ∧ 𝑏 ∈ 𝐴) ∧ ((abs‘((𝐹‘𝑏) − 𝑥)) < 𝑦 ∧ (abs‘((𝐹‘𝑏) − 𝑅)) < 𝑦)) → (𝑥 − (𝐹‘𝑎)) ∈ ℂ)
203	202	abscld 15423	. . . . . . . . . . . . . . . . . . 19 ⊢ (((((((𝜑 ∧ 𝑥 ∈ ℂ) ∧ 𝑦 ∈ ℝ+) ∧ 𝑎 ∈ 𝐴) ∧ ((abs‘((𝐹‘𝑎) − 𝑥)) < 𝑦 ∧ (abs‘((𝐹‘𝑎) − 𝐿)) < 𝑦)) ∧ 𝑏 ∈ 𝐴) ∧ ((abs‘((𝐹‘𝑏) − 𝑥)) < 𝑦 ∧ (abs‘((𝐹‘𝑏) − 𝑅)) < 𝑦)) → (abs‘(𝑥 − (𝐹‘𝑎))) ∈ ℝ)
204	198, 203	readdcld 11281	. . . . . . . . . . . . . . . . . 18 ⊢ (((((((𝜑 ∧ 𝑥 ∈ ℂ) ∧ 𝑦 ∈ ℝ+) ∧ 𝑎 ∈ 𝐴) ∧ ((abs‘((𝐹‘𝑎) − 𝑥)) < 𝑦 ∧ (abs‘((𝐹‘𝑎) − 𝐿)) < 𝑦)) ∧ 𝑏 ∈ 𝐴) ∧ ((abs‘((𝐹‘𝑏) − 𝑥)) < 𝑦 ∧ (abs‘((𝐹‘𝑏) − 𝑅)) < 𝑦)) → (((abs‘(𝑅 − (𝐹‘𝑏))) + (abs‘((𝐹‘𝑏) − 𝑥))) + (abs‘(𝑥 − (𝐹‘𝑎)))) ∈ ℝ)
205	201, 186	subcld 11609	. . . . . . . . . . . . . . . . . . 19 ⊢ (((((((𝜑 ∧ 𝑥 ∈ ℂ) ∧ 𝑦 ∈ ℝ+) ∧ 𝑎 ∈ 𝐴) ∧ ((abs‘((𝐹‘𝑎) − 𝑥)) < 𝑦 ∧ (abs‘((𝐹‘𝑎) − 𝐿)) < 𝑦)) ∧ 𝑏 ∈ 𝐴) ∧ ((abs‘((𝐹‘𝑏) − 𝑥)) < 𝑦 ∧ (abs‘((𝐹‘𝑏) − 𝑅)) < 𝑦)) → ((𝐹‘𝑎) − 𝐿) ∈ ℂ)
206	205	abscld 15423	. . . . . . . . . . . . . . . . . 18 ⊢ (((((((𝜑 ∧ 𝑥 ∈ ℂ) ∧ 𝑦 ∈ ℝ+) ∧ 𝑎 ∈ 𝐴) ∧ ((abs‘((𝐹‘𝑎) − 𝑥)) < 𝑦 ∧ (abs‘((𝐹‘𝑎) − 𝐿)) < 𝑦)) ∧ 𝑏 ∈ 𝐴) ∧ ((abs‘((𝐹‘𝑏) − 𝑥)) < 𝑦 ∧ (abs‘((𝐹‘𝑏) − 𝑅)) < 𝑦)) → (abs‘((𝐹‘𝑎) − 𝐿)) ∈ ℝ)
207	204, 206	readdcld 11281	. . . . . . . . . . . . . . . . 17 ⊢ (((((((𝜑 ∧ 𝑥 ∈ ℂ) ∧ 𝑦 ∈ ℝ+) ∧ 𝑎 ∈ 𝐴) ∧ ((abs‘((𝐹‘𝑎) − 𝑥)) < 𝑦 ∧ (abs‘((𝐹‘𝑎) − 𝐿)) < 𝑦)) ∧ 𝑏 ∈ 𝐴) ∧ ((abs‘((𝐹‘𝑏) − 𝑥)) < 𝑦 ∧ (abs‘((𝐹‘𝑏) − 𝑅)) < 𝑦)) → ((((abs‘(𝑅 − (𝐹‘𝑏))) + (abs‘((𝐹‘𝑏) − 𝑥))) + (abs‘(𝑥 − (𝐹‘𝑎)))) + (abs‘((𝐹‘𝑎) − 𝐿))) ∈ ℝ)
208	15	a1i 11	. . . . . . . . . . . . . . . . . 18 ⊢ (((((((𝜑 ∧ 𝑥 ∈ ℂ) ∧ 𝑦 ∈ ℝ+) ∧ 𝑎 ∈ 𝐴) ∧ ((abs‘((𝐹‘𝑎) − 𝑥)) < 𝑦 ∧ (abs‘((𝐹‘𝑎) − 𝐿)) < 𝑦)) ∧ 𝑏 ∈ 𝐴) ∧ ((abs‘((𝐹‘𝑏) − 𝑥)) < 𝑦 ∧ (abs‘((𝐹‘𝑏) − 𝑅)) < 𝑦)) → 4 ∈ ℝ)
209		rpre 13022	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑦 ∈ ℝ+ → 𝑦 ∈ ℝ)
210	209	ad5antlr 733	. . . . . . . . . . . . . . . . . 18 ⊢ (((((((𝜑 ∧ 𝑥 ∈ ℂ) ∧ 𝑦 ∈ ℝ+) ∧ 𝑎 ∈ 𝐴) ∧ ((abs‘((𝐹‘𝑎) − 𝑥)) < 𝑦 ∧ (abs‘((𝐹‘𝑎) − 𝐿)) < 𝑦)) ∧ 𝑏 ∈ 𝐴) ∧ ((abs‘((𝐹‘𝑏) − 𝑥)) < 𝑦 ∧ (abs‘((𝐹‘𝑏) − 𝑅)) < 𝑦)) → 𝑦 ∈ ℝ)
211	208, 210	remulcld 11282	. . . . . . . . . . . . . . . . 17 ⊢ (((((((𝜑 ∧ 𝑥 ∈ ℂ) ∧ 𝑦 ∈ ℝ+) ∧ 𝑎 ∈ 𝐴) ∧ ((abs‘((𝐹‘𝑎) − 𝑥)) < 𝑦 ∧ (abs‘((𝐹‘𝑎) − 𝐿)) < 𝑦)) ∧ 𝑏 ∈ 𝐴) ∧ ((abs‘((𝐹‘𝑏) − 𝑥)) < 𝑦 ∧ (abs‘((𝐹‘𝑏) − 𝑅)) < 𝑦)) → (4 · 𝑦) ∈ ℝ)
212	185, 192, 195, 201, 186	absnpncan3d 44718	. . . . . . . . . . . . . . . . 17 ⊢ (((((((𝜑 ∧ 𝑥 ∈ ℂ) ∧ 𝑦 ∈ ℝ+) ∧ 𝑎 ∈ 𝐴) ∧ ((abs‘((𝐹‘𝑎) − 𝑥)) < 𝑦 ∧ (abs‘((𝐹‘𝑎) − 𝐿)) < 𝑦)) ∧ 𝑏 ∈ 𝐴) ∧ ((abs‘((𝐹‘𝑏) − 𝑥)) < 𝑦 ∧ (abs‘((𝐹‘𝑏) − 𝑅)) < 𝑦)) → (abs‘(𝑅 − 𝐿)) ≤ ((((abs‘(𝑅 − (𝐹‘𝑏))) + (abs‘((𝐹‘𝑏) − 𝑥))) + (abs‘(𝑥 − (𝐹‘𝑎)))) + (abs‘((𝐹‘𝑎) − 𝐿))))
213	185, 192	abssubd 15440	. . . . . . . . . . . . . . . . . . 19 ⊢ (((((((𝜑 ∧ 𝑥 ∈ ℂ) ∧ 𝑦 ∈ ℝ+) ∧ 𝑎 ∈ 𝐴) ∧ ((abs‘((𝐹‘𝑎) − 𝑥)) < 𝑦 ∧ (abs‘((𝐹‘𝑎) − 𝐿)) < 𝑦)) ∧ 𝑏 ∈ 𝐴) ∧ ((abs‘((𝐹‘𝑏) − 𝑥)) < 𝑦 ∧ (abs‘((𝐹‘𝑏) − 𝑅)) < 𝑦)) → (abs‘(𝑅 − (𝐹‘𝑏))) = (abs‘((𝐹‘𝑏) − 𝑅)))
214		simprr 771	. . . . . . . . . . . . . . . . . . 19 ⊢ (((((((𝜑 ∧ 𝑥 ∈ ℂ) ∧ 𝑦 ∈ ℝ+) ∧ 𝑎 ∈ 𝐴) ∧ ((abs‘((𝐹‘𝑎) − 𝑥)) < 𝑦 ∧ (abs‘((𝐹‘𝑎) − 𝐿)) < 𝑦)) ∧ 𝑏 ∈ 𝐴) ∧ ((abs‘((𝐹‘𝑏) − 𝑥)) < 𝑦 ∧ (abs‘((𝐹‘𝑏) − 𝑅)) < 𝑦)) → (abs‘((𝐹‘𝑏) − 𝑅)) < 𝑦)
215	213, 214	eqbrtrd 5174	. . . . . . . . . . . . . . . . . 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 479	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((((𝜑 ∧ 𝑥 ∈ ℂ) ∧ 𝑦 ∈ ℝ+) ∧ 𝑎 ∈ 𝐴) ∧ ((abs‘((𝐹‘𝑎) − 𝑥)) < 𝑦 ∧ (abs‘((𝐹‘𝑎) − 𝐿)) < 𝑦)) ∧ 𝑏 ∈ 𝐴) → (𝐹‘𝑎) ∈ ℂ)
220	217, 219	abssubd 15440	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((((𝜑 ∧ 𝑥 ∈ ℂ) ∧ 𝑦 ∈ ℝ+) ∧ 𝑎 ∈ 𝐴) ∧ ((abs‘((𝐹‘𝑎) − 𝑥)) < 𝑦 ∧ (abs‘((𝐹‘𝑎) − 𝐿)) < 𝑦)) ∧ 𝑏 ∈ 𝐴) → (abs‘(𝑥 − (𝐹‘𝑎))) = (abs‘((𝐹‘𝑎) − 𝑥)))
221		simplrl 775	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((((𝜑 ∧ 𝑥 ∈ ℂ) ∧ 𝑦 ∈ ℝ+) ∧ 𝑎 ∈ 𝐴) ∧ ((abs‘((𝐹‘𝑎) − 𝑥)) < 𝑦 ∧ (abs‘((𝐹‘𝑎) − 𝐿)) < 𝑦)) ∧ 𝑏 ∈ 𝐴) → (abs‘((𝐹‘𝑎) − 𝑥)) < 𝑦)
222	220, 221	eqbrtrd 5174	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((((𝜑 ∧ 𝑥 ∈ ℂ) ∧ 𝑦 ∈ ℝ+) ∧ 𝑎 ∈ 𝐴) ∧ ((abs‘((𝐹‘𝑎) − 𝑥)) < 𝑦 ∧ (abs‘((𝐹‘𝑎) − 𝐿)) < 𝑦)) ∧ 𝑏 ∈ 𝐴) → (abs‘(𝑥 − (𝐹‘𝑎))) < 𝑦)
223	222	adantr 479	. . . . . . . . . . . . . . . . . 18 ⊢ (((((((𝜑 ∧ 𝑥 ∈ ℂ) ∧ 𝑦 ∈ ℝ+) ∧ 𝑎 ∈ 𝐴) ∧ ((abs‘((𝐹‘𝑎) − 𝑥)) < 𝑦 ∧ (abs‘((𝐹‘𝑎) − 𝐿)) < 𝑦)) ∧ 𝑏 ∈ 𝐴) ∧ ((abs‘((𝐹‘𝑏) − 𝑥)) < 𝑦 ∧ (abs‘((𝐹‘𝑏) − 𝑅)) < 𝑦)) → (abs‘(𝑥 − (𝐹‘𝑎))) < 𝑦)
224		simplrr 776	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((((𝜑 ∧ 𝑥 ∈ ℂ) ∧ 𝑦 ∈ ℝ+) ∧ 𝑎 ∈ 𝐴) ∧ ((abs‘((𝐹‘𝑎) − 𝑥)) < 𝑦 ∧ (abs‘((𝐹‘𝑎) − 𝐿)) < 𝑦)) ∧ 𝑏 ∈ 𝐴) → (abs‘((𝐹‘𝑎) − 𝐿)) < 𝑦)
225	224	adantr 479	. . . . . . . . . . . . . . . . . 18 ⊢ (((((((𝜑 ∧ 𝑥 ∈ ℂ) ∧ 𝑦 ∈ ℝ+) ∧ 𝑎 ∈ 𝐴) ∧ ((abs‘((𝐹‘𝑎) − 𝑥)) < 𝑦 ∧ (abs‘((𝐹‘𝑎) − 𝐿)) < 𝑦)) ∧ 𝑏 ∈ 𝐴) ∧ ((abs‘((𝐹‘𝑏) − 𝑥)) < 𝑦 ∧ (abs‘((𝐹‘𝑏) − 𝑅)) < 𝑦)) → (abs‘((𝐹‘𝑎) − 𝐿)) < 𝑦)
226	194, 197, 203, 206, 210, 215, 216, 223, 225	lt4addmuld 44717	. . . . . . . . . . . . . . . . 17 ⊢ (((((((𝜑 ∧ 𝑥 ∈ ℂ) ∧ 𝑦 ∈ ℝ+) ∧ 𝑎 ∈ 𝐴) ∧ ((abs‘((𝐹‘𝑎) − 𝑥)) < 𝑦 ∧ (abs‘((𝐹‘𝑎) − 𝐿)) < 𝑦)) ∧ 𝑏 ∈ 𝐴) ∧ ((abs‘((𝐹‘𝑏) − 𝑥)) < 𝑦 ∧ (abs‘((𝐹‘𝑏) − 𝑅)) < 𝑦)) → ((((abs‘(𝑅 − (𝐹‘𝑏))) + (abs‘((𝐹‘𝑏) − 𝑥))) + (abs‘(𝑥 − (𝐹‘𝑎)))) + (abs‘((𝐹‘𝑎) − 𝐿))) < (4 · 𝑦))
227	188, 207, 211, 212, 226	lelttrd 11410	. . . . . . . . . . . . . . . 16 ⊢ (((((((𝜑 ∧ 𝑥 ∈ ℂ) ∧ 𝑦 ∈ ℝ+) ∧ 𝑎 ∈ 𝐴) ∧ ((abs‘((𝐹‘𝑎) − 𝑥)) < 𝑦 ∧ (abs‘((𝐹‘𝑎) − 𝐿)) < 𝑦)) ∧ 𝑏 ∈ 𝐴) ∧ ((abs‘((𝐹‘𝑏) − 𝑥)) < 𝑦 ∧ (abs‘((𝐹‘𝑏) − 𝑅)) < 𝑦)) → (abs‘(𝑅 − 𝐿)) < (4 · 𝑦))
228	227	ex 411	. . . . . . . . . . . . . . 15 ⊢ ((((((𝜑 ∧ 𝑥 ∈ ℂ) ∧ 𝑦 ∈ ℝ+) ∧ 𝑎 ∈ 𝐴) ∧ ((abs‘((𝐹‘𝑎) − 𝑥)) < 𝑦 ∧ (abs‘((𝐹‘𝑎) − 𝐿)) < 𝑦)) ∧ 𝑏 ∈ 𝐴) → (((abs‘((𝐹‘𝑏) − 𝑥)) < 𝑦 ∧ (abs‘((𝐹‘𝑏) − 𝑅)) < 𝑦) → (abs‘(𝑅 − 𝐿)) < (4 · 𝑦)))
229	228	adantl3r 748	. . . . . . . . . . . . . 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 6771	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝐹:𝐴⟶ℂ → (𝐹 ↾ (-∞(,)𝐵)):(𝐴 ∩ (-∞(,)𝐵))⟶ℂ)
233	36, 232	syl 17	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝜑 → (𝐹 ↾ (-∞(,)𝐵)):(𝐴 ∩ (-∞(,)𝐵))⟶ℂ)
234		ioosscn 13426	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (-∞(,)𝐵) ⊆ ℂ
235	46, 234	sstri 3991	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝐴 ∩ (-∞(,)𝐵)) ⊆ ℂ
236	235	a1i 11	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝜑 → (𝐴 ∩ (-∞(,)𝐵)) ⊆ ℂ)
237	233, 236, 56	ellimc3 25828	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝜑 → (𝐿 ∈ ((𝐹 ↾ (-∞(,)𝐵)) limℂ 𝐵) ↔ (𝐿 ∈ ℂ ∧ ∀𝑦 ∈ ℝ+ ∃𝑣 ∈ ℝ+ ∀𝑤 ∈ (𝐴 ∩ (-∞(,)𝐵))((𝑤 ≠ 𝐵 ∧ (abs‘(𝑤 − 𝐵)) < 𝑣) → (abs‘(((𝐹 ↾ (-∞(,)𝐵))‘𝑤) − 𝐿)) < 𝑦))))
238	6, 237	mpbid 231	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → (𝐿 ∈ ℂ ∧ ∀𝑦 ∈ ℝ+ ∃𝑣 ∈ ℝ+ ∀𝑤 ∈ (𝐴 ∩ (-∞(,)𝐵))((𝑤 ≠ 𝐵 ∧ (abs‘(𝑤 − 𝐵)) < 𝑣) → (abs‘(((𝐹 ↾ (-∞(,)𝐵))‘𝑤) − 𝐿)) < 𝑦)))
239	238	simprd 494	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → ∀𝑦 ∈ ℝ+ ∃𝑣 ∈ ℝ+ ∀𝑤 ∈ (𝐴 ∩ (-∞(,)𝐵))((𝑤 ≠ 𝐵 ∧ (abs‘(𝑤 − 𝐵)) < 𝑣) → (abs‘(((𝐹 ↾ (-∞(,)𝐵))‘𝑤) − 𝐿)) < 𝑦))
240	239	r19.21bi 3246	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑦 ∈ ℝ+) → ∃𝑣 ∈ ℝ+ ∀𝑤 ∈ (𝐴 ∩ (-∞(,)𝐵))((𝑤 ≠ 𝐵 ∧ (abs‘(𝑤 − 𝐵)) < 𝑣) → (abs‘(((𝐹 ↾ (-∞(,)𝐵))‘𝑤) − 𝐿)) < 𝑦))
241	240	3ad2ant1 1130	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑦 ∈ ℝ+) ∧ 𝑧 ∈ ℝ+ ∧ ∀𝑤 ∈ 𝐴 ((𝑤 ≠ 𝐵 ∧ (abs‘(𝑤 − 𝐵)) < 𝑧) → (abs‘((𝐹‘𝑤) − 𝑥)) < 𝑦)) → ∃𝑣 ∈ ℝ+ ∀𝑤 ∈ (𝐴 ∩ (-∞(,)𝐵))((𝑤 ≠ 𝐵 ∧ (abs‘(𝑤 − 𝐵)) < 𝑣) → (abs‘(((𝐹 ↾ (-∞(,)𝐵))‘𝑤) − 𝐿)) < 𝑦))
242		simp11l 1281	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((𝜑 ∧ 𝑦 ∈ ℝ+) ∧ 𝑧 ∈ ℝ+ ∧ ∀𝑤 ∈ 𝐴 ((𝑤 ≠ 𝐵 ∧ (abs‘(𝑤 − 𝐵)) < 𝑧) → (abs‘((𝐹‘𝑤) − 𝑥)) < 𝑦)) ∧ 𝑣 ∈ ℝ+ ∧ ∀𝑤 ∈ (𝐴 ∩ (-∞(,)𝐵))((𝑤 ≠ 𝐵 ∧ (abs‘(𝑤 − 𝐵)) < 𝑣) → (abs‘(((𝐹 ↾ (-∞(,)𝐵))‘𝑤) − 𝐿)) < 𝑦)) → 𝜑)
243		simp12 1201	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((𝜑 ∧ 𝑦 ∈ ℝ+) ∧ 𝑧 ∈ ℝ+ ∧ ∀𝑤 ∈ 𝐴 ((𝑤 ≠ 𝐵 ∧ (abs‘(𝑤 − 𝐵)) < 𝑧) → (abs‘((𝐹‘𝑤) − 𝑥)) < 𝑦)) ∧ 𝑣 ∈ ℝ+ ∧ ∀𝑤 ∈ (𝐴 ∩ (-∞(,)𝐵))((𝑤 ≠ 𝐵 ∧ (abs‘(𝑤 − 𝐵)) < 𝑣) → (abs‘(((𝐹 ↾ (-∞(,)𝐵))‘𝑤) − 𝐿)) < 𝑦)) → 𝑧 ∈ ℝ+)
244		simp2 1134	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((𝜑 ∧ 𝑦 ∈ ℝ+) ∧ 𝑧 ∈ ℝ+ ∧ ∀𝑤 ∈ 𝐴 ((𝑤 ≠ 𝐵 ∧ (abs‘(𝑤 − 𝐵)) < 𝑧) → (abs‘((𝐹‘𝑤) − 𝑥)) < 𝑦)) ∧ 𝑣 ∈ ℝ+ ∧ ∀𝑤 ∈ (𝐴 ∩ (-∞(,)𝐵))((𝑤 ≠ 𝐵 ∧ (abs‘(𝑤 − 𝐵)) < 𝑣) → (abs‘(((𝐹 ↾ (-∞(,)𝐵))‘𝑤) − 𝐿)) < 𝑦)) → 𝑣 ∈ ℝ+)
245		breq2 5156	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑢 = if(𝑧 ≤ 𝑣, 𝑧, 𝑣) → ((abs‘(𝑎 − 𝐵)) < 𝑢 ↔ (abs‘(𝑎 − 𝐵)) < if(𝑧 ≤ 𝑣, 𝑧, 𝑣)))
246	245	rexbidv 3176	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑢 = if(𝑧 ≤ 𝑣, 𝑧, 𝑣) → (∃𝑎 ∈ ((𝐴 ∩ (-∞(,)𝐵)) ∖ {𝐵})(abs‘(𝑎 − 𝐵)) < 𝑢 ↔ ∃𝑎 ∈ ((𝐴 ∩ (-∞(,)𝐵)) ∖ {𝐵})(abs‘(𝑎 − 𝐵)) < if(𝑧 ≤ 𝑣, 𝑧, 𝑣)))
247		inss1 4231	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (((limPt‘𝐾)‘(𝐴 ∩ (-∞(,)𝐵))) ∩ ℝ) ⊆ ((limPt‘𝐾)‘(𝐴 ∩ (-∞(,)𝐵)))
248	247	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝜑 → (((limPt‘𝐾)‘(𝐴 ∩ (-∞(,)𝐵))) ∩ ℝ) ⊆ ((limPt‘𝐾)‘(𝐴 ∩ (-∞(,)𝐵))))
249	48	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (𝜑 → (𝐴 ∩ (-∞(,)𝐵)) ⊆ ℝ)
250	79, 81	restlp 23107	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ((𝐾 ∈ Top ∧ ℝ ⊆ ℂ ∧ (𝐴 ∩ (-∞(,)𝐵)) ⊆ ℝ) → ((limPt‘𝐽)‘(𝐴 ∩ (-∞(,)𝐵))) = (((limPt‘𝐾)‘(𝐴 ∩ (-∞(,)𝐵))) ∩ ℝ))
251	71, 73, 249, 250	syl3anc 1368	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝜑 → ((limPt‘𝐽)‘(𝐴 ∩ (-∞(,)𝐵))) = (((limPt‘𝐾)‘(𝐴 ∩ (-∞(,)𝐵))) ∩ ℝ))
252	85	fveq1i 6903	. . . . . . . . . . . . . . . . . . . . . . . . . . . 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 45056	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝜑 → (𝐵 ∈ ((limPt‘(TopOpen‘ℂfld))‘(𝐴 ∩ (-∞(,)𝐵))) ↔ ∀𝑢 ∈ ℝ+ ∃𝑎 ∈ ((𝐴 ∩ (-∞(,)𝐵)) ∖ {𝐵})(abs‘(𝑎 − 𝐵)) < 𝑢))
257	255, 256	mpbid 231	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝜑 → ∀𝑢 ∈ ℝ+ ∃𝑎 ∈ ((𝐴 ∩ (-∞(,)𝐵)) ∖ {𝐵})(abs‘(𝑎 − 𝐵)) < 𝑢)
258	257	3ad2ant1 1130	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝜑 ∧ 𝑧 ∈ ℝ+ ∧ 𝑣 ∈ ℝ+) → ∀𝑢 ∈ ℝ+ ∃𝑎 ∈ ((𝐴 ∩ (-∞(,)𝐵)) ∖ {𝐵})(abs‘(𝑎 − 𝐵)) < 𝑢)
259	246, 258, 95	rspcdva 3612	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝜑 ∧ 𝑧 ∈ ℝ+ ∧ 𝑣 ∈ ℝ+) → ∃𝑎 ∈ ((𝐴 ∩ (-∞(,)𝐵)) ∖ {𝐵})(abs‘(𝑎 − 𝐵)) < if(𝑧 ≤ 𝑣, 𝑧, 𝑣))
260		eldifi 4127	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑎 ∈ ((𝐴 ∩ (-∞(,)𝐵)) ∖ {𝐵}) → 𝑎 ∈ (𝐴 ∩ (-∞(,)𝐵)))
261	48, 260	sselid 3980	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑎 ∈ ((𝐴 ∩ (-∞(,)𝐵)) ∖ {𝐵}) → 𝑎 ∈ ℝ)
262	73	sselda 3982	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ ((𝜑 ∧ 𝑎 ∈ ℝ) → 𝑎 ∈ ℂ)
263	56	adantr 479	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ ((𝜑 ∧ 𝑎 ∈ ℝ) → 𝐵 ∈ ℂ)
264	262, 263	subcld 11609	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ ((𝜑 ∧ 𝑎 ∈ ℝ) → (𝑎 − 𝐵) ∈ ℂ)
265	264	abscld 15423	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ ((𝜑 ∧ 𝑎 ∈ ℝ) → (abs‘(𝑎 − 𝐵)) ∈ ℝ)
266	265	3ad2antl1 1182	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (((𝜑 ∧ 𝑧 ∈ ℝ+ ∧ 𝑣 ∈ ℝ+) ∧ 𝑎 ∈ ℝ) → (abs‘(𝑎 − 𝐵)) ∈ ℝ)
267	266	adantr 479	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((((𝜑 ∧ 𝑧 ∈ ℝ+ ∧ 𝑣 ∈ ℝ+) ∧ 𝑎 ∈ ℝ) ∧ (abs‘(𝑎 − 𝐵)) < if(𝑧 ≤ 𝑣, 𝑧, 𝑣)) → (abs‘(𝑎 − 𝐵)) ∈ ℝ)
268	105	ad2antrr 724	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((((𝜑 ∧ 𝑧 ∈ ℝ+ ∧ 𝑣 ∈ ℝ+) ∧ 𝑎 ∈ ℝ) ∧ (abs‘(𝑎 − 𝐵)) < if(𝑧 ≤ 𝑣, 𝑧, 𝑣)) → if(𝑧 ≤ 𝑣, 𝑧, 𝑣) ∈ ℝ)
269	108	ad2antrr 724	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((((𝜑 ∧ 𝑧 ∈ ℝ+ ∧ 𝑣 ∈ ℝ+) ∧ 𝑎 ∈ ℝ) ∧ (abs‘(𝑎 − 𝐵)) < if(𝑧 ≤ 𝑣, 𝑧, 𝑣)) → 𝑧 ∈ ℝ)
270		simpr 483	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((((𝜑 ∧ 𝑧 ∈ ℝ+ ∧ 𝑣 ∈ ℝ+) ∧ 𝑎 ∈ ℝ) ∧ (abs‘(𝑎 − 𝐵)) < if(𝑧 ≤ 𝑣, 𝑧, 𝑣)) → (abs‘(𝑎 − 𝐵)) < if(𝑧 ≤ 𝑣, 𝑧, 𝑣))
271	114	ad2antrr 724	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((((𝜑 ∧ 𝑧 ∈ ℝ+ ∧ 𝑣 ∈ ℝ+) ∧ 𝑎 ∈ ℝ) ∧ (abs‘(𝑎 − 𝐵)) < if(𝑧 ≤ 𝑣, 𝑧, 𝑣)) → if(𝑧 ≤ 𝑣, 𝑧, 𝑣) ≤ 𝑧)
272	267, 268, 269, 270, 271	ltletrd 11412	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((((𝜑 ∧ 𝑧 ∈ ℝ+ ∧ 𝑣 ∈ ℝ+) ∧ 𝑎 ∈ ℝ) ∧ (abs‘(𝑎 − 𝐵)) < if(𝑧 ≤ 𝑣, 𝑧, 𝑣)) → (abs‘(𝑎 − 𝐵)) < 𝑧)
273	117	ad2antrr 724	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((((𝜑 ∧ 𝑧 ∈ ℝ+ ∧ 𝑣 ∈ ℝ+) ∧ 𝑎 ∈ ℝ) ∧ (abs‘(𝑎 − 𝐵)) < if(𝑧 ≤ 𝑣, 𝑧, 𝑣)) → 𝑣 ∈ ℝ)
274		min2 13209	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ ((𝑧 ∈ ℝ ∧ 𝑣 ∈ ℝ) → if(𝑧 ≤ 𝑣, 𝑧, 𝑣) ≤ 𝑣)
275	107, 111, 274	syl2an 594	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ ((𝑧 ∈ ℝ+ ∧ 𝑣 ∈ ℝ+) → if(𝑧 ≤ 𝑣, 𝑧, 𝑣) ≤ 𝑣)
276	275	3adant1 1127	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ((𝜑 ∧ 𝑧 ∈ ℝ+ ∧ 𝑣 ∈ ℝ+) → if(𝑧 ≤ 𝑣, 𝑧, 𝑣) ≤ 𝑣)
277	276	ad2antrr 724	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((((𝜑 ∧ 𝑧 ∈ ℝ+ ∧ 𝑣 ∈ ℝ+) ∧ 𝑎 ∈ ℝ) ∧ (abs‘(𝑎 − 𝐵)) < if(𝑧 ≤ 𝑣, 𝑧, 𝑣)) → if(𝑧 ≤ 𝑣, 𝑧, 𝑣) ≤ 𝑣)
278	267, 268, 273, 270, 277	ltletrd 11412	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((((𝜑 ∧ 𝑧 ∈ ℝ+ ∧ 𝑣 ∈ ℝ+) ∧ 𝑎 ∈ ℝ) ∧ (abs‘(𝑎 − 𝐵)) < if(𝑧 ≤ 𝑣, 𝑧, 𝑣)) → (abs‘(𝑎 − 𝐵)) < 𝑣)
279	272, 278	jca 510	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((((𝜑 ∧ 𝑧 ∈ ℝ+ ∧ 𝑣 ∈ ℝ+) ∧ 𝑎 ∈ ℝ) ∧ (abs‘(𝑎 − 𝐵)) < if(𝑧 ≤ 𝑣, 𝑧, 𝑣)) → ((abs‘(𝑎 − 𝐵)) < 𝑧 ∧ (abs‘(𝑎 − 𝐵)) < 𝑣))
280	279	ex 411	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((𝜑 ∧ 𝑧 ∈ ℝ+ ∧ 𝑣 ∈ ℝ+) ∧ 𝑎 ∈ ℝ) → ((abs‘(𝑎 − 𝐵)) < if(𝑧 ≤ 𝑣, 𝑧, 𝑣) → ((abs‘(𝑎 − 𝐵)) < 𝑧 ∧ (abs‘(𝑎 − 𝐵)) < 𝑣)))
281	261, 280	sylan2 591	. . . . . . . . . . . . . . . . . . . . . . 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 1368	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝜑 ∧ 𝑦 ∈ ℝ+) ∧ 𝑧 ∈ ℝ+ ∧ ∀𝑤 ∈ 𝐴 ((𝑤 ≠ 𝐵 ∧ (abs‘(𝑤 − 𝐵)) < 𝑧) → (abs‘((𝐹‘𝑤) − 𝑥)) < 𝑦)) ∧ 𝑣 ∈ ℝ+ ∧ ∀𝑤 ∈ (𝐴 ∩ (-∞(,)𝐵))((𝑤 ≠ 𝐵 ∧ (abs‘(𝑤 − 𝐵)) < 𝑣) → (abs‘(((𝐹 ↾ (-∞(,)𝐵))‘𝑤) − 𝐿)) < 𝑦)) → ∃𝑎 ∈ ((𝐴 ∩ (-∞(,)𝐵)) ∖ {𝐵})((abs‘(𝑎 − 𝐵)) < 𝑧 ∧ (abs‘(𝑎 − 𝐵)) < 𝑣))
285		nfv 1909	. . . . . . . . . . . . . . . . . . . . 21 ⊢ Ⅎ𝑎(((𝜑 ∧ 𝑦 ∈ ℝ+) ∧ 𝑧 ∈ ℝ+ ∧ ∀𝑤 ∈ 𝐴 ((𝑤 ≠ 𝐵 ∧ (abs‘(𝑤 − 𝐵)) < 𝑧) → (abs‘((𝐹‘𝑤) − 𝑥)) < 𝑦)) ∧ 𝑣 ∈ ℝ+ ∧ ∀𝑤 ∈ (𝐴 ∩ (-∞(,)𝐵))((𝑤 ≠ 𝐵 ∧ (abs‘(𝑤 − 𝐵)) < 𝑣) → (abs‘(((𝐹 ↾ (-∞(,)𝐵))‘𝑤) − 𝐿)) < 𝑦))
286		nfre1 3280	. . . . . . . . . . . . . . . . . . . . 21 ⊢ Ⅎ𝑎∃𝑎 ∈ 𝐴 ((abs‘((𝐹‘𝑎) − 𝑥)) < 𝑦 ∧ (abs‘((𝐹‘𝑎) − 𝐿)) < 𝑦)
287	260	elin1d 4200	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑎 ∈ ((𝐴 ∩ (-∞(,)𝐵)) ∖ {𝐵}) → 𝑎 ∈ 𝐴)
288	287	3ad2ant2 1131	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((((𝜑 ∧ 𝑦 ∈ ℝ+) ∧ 𝑧 ∈ ℝ+ ∧ ∀𝑤 ∈ 𝐴 ((𝑤 ≠ 𝐵 ∧ (abs‘(𝑤 − 𝐵)) < 𝑧) → (abs‘((𝐹‘𝑤) − 𝑥)) < 𝑦)) ∧ 𝑣 ∈ ℝ+ ∧ ∀𝑤 ∈ (𝐴 ∩ (-∞(,)𝐵))((𝑤 ≠ 𝐵 ∧ (abs‘(𝑤 − 𝐵)) < 𝑣) → (abs‘(((𝐹 ↾ (-∞(,)𝐵))‘𝑤) − 𝐿)) < 𝑦)) ∧ 𝑎 ∈ ((𝐴 ∩ (-∞(,)𝐵)) ∖ {𝐵}) ∧ ((abs‘(𝑎 − 𝐵)) < 𝑧 ∧ (abs‘(𝑎 − 𝐵)) < 𝑣)) → 𝑎 ∈ 𝐴)
289		simp113 1301	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((((𝜑 ∧ 𝑦 ∈ ℝ+) ∧ 𝑧 ∈ ℝ+ ∧ ∀𝑤 ∈ 𝐴 ((𝑤 ≠ 𝐵 ∧ (abs‘(𝑤 − 𝐵)) < 𝑧) → (abs‘((𝐹‘𝑤) − 𝑥)) < 𝑦)) ∧ 𝑣 ∈ ℝ+ ∧ ∀𝑤 ∈ (𝐴 ∩ (-∞(,)𝐵))((𝑤 ≠ 𝐵 ∧ (abs‘(𝑤 − 𝐵)) < 𝑣) → (abs‘(((𝐹 ↾ (-∞(,)𝐵))‘𝑤) − 𝐿)) < 𝑦)) ∧ 𝑎 ∈ ((𝐴 ∩ (-∞(,)𝐵)) ∖ {𝐵}) ∧ ((abs‘(𝑎 − 𝐵)) < 𝑧 ∧ (abs‘(𝑎 − 𝐵)) < 𝑣)) → ∀𝑤 ∈ 𝐴 ((𝑤 ≠ 𝐵 ∧ (abs‘(𝑤 − 𝐵)) < 𝑧) → (abs‘((𝐹‘𝑤) − 𝑥)) < 𝑦))
290		eldifsni 4798	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝑎 ∈ ((𝐴 ∩ (-∞(,)𝐵)) ∖ {𝐵}) → 𝑎 ≠ 𝐵)
291	290	adantr 479	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((𝑎 ∈ ((𝐴 ∩ (-∞(,)𝐵)) ∖ {𝐵}) ∧ ((abs‘(𝑎 − 𝐵)) < 𝑧 ∧ (abs‘(𝑎 − 𝐵)) < 𝑣)) → 𝑎 ≠ 𝐵)
292		simprl 769	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((𝑎 ∈ ((𝐴 ∩ (-∞(,)𝐵)) ∖ {𝐵}) ∧ ((abs‘(𝑎 − 𝐵)) < 𝑧 ∧ (abs‘(𝑎 − 𝐵)) < 𝑣)) → (abs‘(𝑎 − 𝐵)) < 𝑧)
293	291, 292	jca 510	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((𝑎 ∈ ((𝐴 ∩ (-∞(,)𝐵)) ∖ {𝐵}) ∧ ((abs‘(𝑎 − 𝐵)) < 𝑧 ∧ (abs‘(𝑎 − 𝐵)) < 𝑣)) → (𝑎 ≠ 𝐵 ∧ (abs‘(𝑎 − 𝐵)) < 𝑧))
294	293	3adant1 1127	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((((𝜑 ∧ 𝑦 ∈ ℝ+) ∧ 𝑧 ∈ ℝ+ ∧ ∀𝑤 ∈ 𝐴 ((𝑤 ≠ 𝐵 ∧ (abs‘(𝑤 − 𝐵)) < 𝑧) → (abs‘((𝐹‘𝑤) − 𝑥)) < 𝑦)) ∧ 𝑣 ∈ ℝ+ ∧ ∀𝑤 ∈ (𝐴 ∩ (-∞(,)𝐵))((𝑤 ≠ 𝐵 ∧ (abs‘(𝑤 − 𝐵)) < 𝑣) → (abs‘(((𝐹 ↾ (-∞(,)𝐵))‘𝑤) − 𝐿)) < 𝑦)) ∧ 𝑎 ∈ ((𝐴 ∩ (-∞(,)𝐵)) ∖ {𝐵}) ∧ ((abs‘(𝑎 − 𝐵)) < 𝑧 ∧ (abs‘(𝑎 − 𝐵)) < 𝑣)) → (𝑎 ≠ 𝐵 ∧ (abs‘(𝑎 − 𝐵)) < 𝑧))
295		neeq1 3000	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (𝑤 = 𝑎 → (𝑤 ≠ 𝐵 ↔ 𝑎 ≠ 𝐵))
296		fvoveq1 7449	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (𝑤 = 𝑎 → (abs‘(𝑤 − 𝐵)) = (abs‘(𝑎 − 𝐵)))
297	296	breq1d 5162	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (𝑤 = 𝑎 → ((abs‘(𝑤 − 𝐵)) < 𝑧 ↔ (abs‘(𝑎 − 𝐵)) < 𝑧))
298	295, 297	anbi12d 630	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝑤 = 𝑎 → ((𝑤 ≠ 𝐵 ∧ (abs‘(𝑤 − 𝐵)) < 𝑧) ↔ (𝑎 ≠ 𝐵 ∧ (abs‘(𝑎 − 𝐵)) < 𝑧)))
299	298	imbrov2fvoveq 7451	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝑤 = 𝑎 → (((𝑤 ≠ 𝐵 ∧ (abs‘(𝑤 − 𝐵)) < 𝑧) → (abs‘((𝐹‘𝑤) − 𝑥)) < 𝑦) ↔ ((𝑎 ≠ 𝐵 ∧ (abs‘(𝑎 − 𝐵)) < 𝑧) → (abs‘((𝐹‘𝑎) − 𝑥)) < 𝑦)))
300	299	rspcva 3609	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((𝑎 ∈ 𝐴 ∧ ∀𝑤 ∈ 𝐴 ((𝑤 ≠ 𝐵 ∧ (abs‘(𝑤 − 𝐵)) < 𝑧) → (abs‘((𝐹‘𝑤) − 𝑥)) < 𝑦)) → ((𝑎 ≠ 𝐵 ∧ (abs‘(𝑎 − 𝐵)) < 𝑧) → (abs‘((𝐹‘𝑎) − 𝑥)) < 𝑦))
301	300	imp 405	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((𝑎 ∈ 𝐴 ∧ ∀𝑤 ∈ 𝐴 ((𝑤 ≠ 𝐵 ∧ (abs‘(𝑤 − 𝐵)) < 𝑧) → (abs‘((𝐹‘𝑤) − 𝑥)) < 𝑦)) ∧ (𝑎 ≠ 𝐵 ∧ (abs‘(𝑎 − 𝐵)) < 𝑧)) → (abs‘((𝐹‘𝑎) − 𝑥)) < 𝑦)
302	288, 289, 294, 301	syl21anc 836	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((((𝜑 ∧ 𝑦 ∈ ℝ+) ∧ 𝑧 ∈ ℝ+ ∧ ∀𝑤 ∈ 𝐴 ((𝑤 ≠ 𝐵 ∧ (abs‘(𝑤 − 𝐵)) < 𝑧) → (abs‘((𝐹‘𝑤) − 𝑥)) < 𝑦)) ∧ 𝑣 ∈ ℝ+ ∧ ∀𝑤 ∈ (𝐴 ∩ (-∞(,)𝐵))((𝑤 ≠ 𝐵 ∧ (abs‘(𝑤 − 𝐵)) < 𝑣) → (abs‘(((𝐹 ↾ (-∞(,)𝐵))‘𝑤) − 𝐿)) < 𝑦)) ∧ 𝑎 ∈ ((𝐴 ∩ (-∞(,)𝐵)) ∖ {𝐵}) ∧ ((abs‘(𝑎 − 𝐵)) < 𝑧 ∧ (abs‘(𝑎 − 𝐵)) < 𝑣)) → (abs‘((𝐹‘𝑎) − 𝑥)) < 𝑦)
303	260	3ad2ant2 1131	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((((𝜑 ∧ 𝑦 ∈ ℝ+) ∧ 𝑧 ∈ ℝ+ ∧ ∀𝑤 ∈ 𝐴 ((𝑤 ≠ 𝐵 ∧ (abs‘(𝑤 − 𝐵)) < 𝑧) → (abs‘((𝐹‘𝑤) − 𝑥)) < 𝑦)) ∧ 𝑣 ∈ ℝ+ ∧ ∀𝑤 ∈ (𝐴 ∩ (-∞(,)𝐵))((𝑤 ≠ 𝐵 ∧ (abs‘(𝑤 − 𝐵)) < 𝑣) → (abs‘(((𝐹 ↾ (-∞(,)𝐵))‘𝑤) − 𝐿)) < 𝑦)) ∧ 𝑎 ∈ ((𝐴 ∩ (-∞(,)𝐵)) ∖ {𝐵}) ∧ ((abs‘(𝑎 − 𝐵)) < 𝑧 ∧ (abs‘(𝑎 − 𝐵)) < 𝑣)) → 𝑎 ∈ (𝐴 ∩ (-∞(,)𝐵)))
304	242	3ad2ant1 1130	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((((𝜑 ∧ 𝑦 ∈ ℝ+) ∧ 𝑧 ∈ ℝ+ ∧ ∀𝑤 ∈ 𝐴 ((𝑤 ≠ 𝐵 ∧ (abs‘(𝑤 − 𝐵)) < 𝑧) → (abs‘((𝐹‘𝑤) − 𝑥)) < 𝑦)) ∧ 𝑣 ∈ ℝ+ ∧ ∀𝑤 ∈ (𝐴 ∩ (-∞(,)𝐵))((𝑤 ≠ 𝐵 ∧ (abs‘(𝑤 − 𝐵)) < 𝑣) → (abs‘(((𝐹 ↾ (-∞(,)𝐵))‘𝑤) − 𝐿)) < 𝑦)) ∧ 𝑎 ∈ ((𝐴 ∩ (-∞(,)𝐵)) ∖ {𝐵}) ∧ ((abs‘(𝑎 − 𝐵)) < 𝑧 ∧ (abs‘(𝑎 − 𝐵)) < 𝑣)) → 𝜑)
305		simp13 1202	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((((𝜑 ∧ 𝑦 ∈ ℝ+) ∧ 𝑧 ∈ ℝ+ ∧ ∀𝑤 ∈ 𝐴 ((𝑤 ≠ 𝐵 ∧ (abs‘(𝑤 − 𝐵)) < 𝑧) → (abs‘((𝐹‘𝑤) − 𝑥)) < 𝑦)) ∧ 𝑣 ∈ ℝ+ ∧ ∀𝑤 ∈ (𝐴 ∩ (-∞(,)𝐵))((𝑤 ≠ 𝐵 ∧ (abs‘(𝑤 − 𝐵)) < 𝑣) → (abs‘(((𝐹 ↾ (-∞(,)𝐵))‘𝑤) − 𝐿)) < 𝑦)) ∧ 𝑎 ∈ ((𝐴 ∩ (-∞(,)𝐵)) ∖ {𝐵}) ∧ ((abs‘(𝑎 − 𝐵)) < 𝑧 ∧ (abs‘(𝑎 − 𝐵)) < 𝑣)) → ∀𝑤 ∈ (𝐴 ∩ (-∞(,)𝐵))((𝑤 ≠ 𝐵 ∧ (abs‘(𝑤 − 𝐵)) < 𝑣) → (abs‘(((𝐹 ↾ (-∞(,)𝐵))‘𝑤) − 𝐿)) < 𝑦))
306		nfra1 3279	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ Ⅎ𝑤∀𝑤 ∈ (𝐴 ∩ (-∞(,)𝐵))((𝑤 ≠ 𝐵 ∧ (abs‘(𝑤 − 𝐵)) < 𝑣) → (abs‘(((𝐹 ↾ (-∞(,)𝐵))‘𝑤) − 𝐿)) < 𝑦)
307	148, 306	nfan 1894	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ Ⅎ𝑤(𝜑 ∧ ∀𝑤 ∈ (𝐴 ∩ (-∞(,)𝐵))((𝑤 ≠ 𝐵 ∧ (abs‘(𝑤 − 𝐵)) < 𝑣) → (abs‘(((𝐹 ↾ (-∞(,)𝐵))‘𝑤) − 𝐿)) < 𝑦))
308		elinel2 4198	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ (𝑤 ∈ (𝐴 ∩ (-∞(,)𝐵)) → 𝑤 ∈ (-∞(,)𝐵))
309	308	fvresd 6922	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ (𝑤 ∈ (𝐴 ∩ (-∞(,)𝐵)) → ((𝐹 ↾ (-∞(,)𝐵))‘𝑤) = (𝐹‘𝑤))
310	309	eqcomd 2734	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ (𝑤 ∈ (𝐴 ∩ (-∞(,)𝐵)) → (𝐹‘𝑤) = ((𝐹 ↾ (-∞(,)𝐵))‘𝑤))
311	310	fvoveq1d 7448	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (𝑤 ∈ (𝐴 ∩ (-∞(,)𝐵)) → (abs‘((𝐹‘𝑤) − 𝐿)) = (abs‘(((𝐹 ↾ (-∞(,)𝐵))‘𝑤) − 𝐿)))
312	311	3ad2ant2 1131	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (((𝜑 ∧ ∀𝑤 ∈ (𝐴 ∩ (-∞(,)𝐵))((𝑤 ≠ 𝐵 ∧ (abs‘(𝑤 − 𝐵)) < 𝑣) → (abs‘(((𝐹 ↾ (-∞(,)𝐵))‘𝑤) − 𝐿)) < 𝑦)) ∧ 𝑤 ∈ (𝐴 ∩ (-∞(,)𝐵)) ∧ (𝑤 ≠ 𝐵 ∧ (abs‘(𝑤 − 𝐵)) < 𝑣)) → (abs‘((𝐹‘𝑤) − 𝐿)) = (abs‘(((𝐹 ↾ (-∞(,)𝐵))‘𝑤) − 𝐿)))
313		rspa 3243	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ ((∀𝑤 ∈ (𝐴 ∩ (-∞(,)𝐵))((𝑤 ≠ 𝐵 ∧ (abs‘(𝑤 − 𝐵)) < 𝑣) → (abs‘(((𝐹 ↾ (-∞(,)𝐵))‘𝑤) − 𝐿)) < 𝑦) ∧ 𝑤 ∈ (𝐴 ∩ (-∞(,)𝐵))) → ((𝑤 ≠ 𝐵 ∧ (abs‘(𝑤 − 𝐵)) < 𝑣) → (abs‘(((𝐹 ↾ (-∞(,)𝐵))‘𝑤) − 𝐿)) < 𝑦))
314	313	3impia 1114	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ ((∀𝑤 ∈ (𝐴 ∩ (-∞(,)𝐵))((𝑤 ≠ 𝐵 ∧ (abs‘(𝑤 − 𝐵)) < 𝑣) → (abs‘(((𝐹 ↾ (-∞(,)𝐵))‘𝑤) − 𝐿)) < 𝑦) ∧ 𝑤 ∈ (𝐴 ∩ (-∞(,)𝐵)) ∧ (𝑤 ≠ 𝐵 ∧ (abs‘(𝑤 − 𝐵)) < 𝑣)) → (abs‘(((𝐹 ↾ (-∞(,)𝐵))‘𝑤) − 𝐿)) < 𝑦)
315	314	3adant1l 1173	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (((𝜑 ∧ ∀𝑤 ∈ (𝐴 ∩ (-∞(,)𝐵))((𝑤 ≠ 𝐵 ∧ (abs‘(𝑤 − 𝐵)) < 𝑣) → (abs‘(((𝐹 ↾ (-∞(,)𝐵))‘𝑤) − 𝐿)) < 𝑦)) ∧ 𝑤 ∈ (𝐴 ∩ (-∞(,)𝐵)) ∧ (𝑤 ≠ 𝐵 ∧ (abs‘(𝑤 − 𝐵)) < 𝑣)) → (abs‘(((𝐹 ↾ (-∞(,)𝐵))‘𝑤) − 𝐿)) < 𝑦)
316	312, 315	eqbrtrd 5174	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (((𝜑 ∧ ∀𝑤 ∈ (𝐴 ∩ (-∞(,)𝐵))((𝑤 ≠ 𝐵 ∧ (abs‘(𝑤 − 𝐵)) < 𝑣) → (abs‘(((𝐹 ↾ (-∞(,)𝐵))‘𝑤) − 𝐿)) < 𝑦)) ∧ 𝑤 ∈ (𝐴 ∩ (-∞(,)𝐵)) ∧ (𝑤 ≠ 𝐵 ∧ (abs‘(𝑤 − 𝐵)) < 𝑣)) → (abs‘((𝐹‘𝑤) − 𝐿)) < 𝑦)
317	316	3exp 1116	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((𝜑 ∧ ∀𝑤 ∈ (𝐴 ∩ (-∞(,)𝐵))((𝑤 ≠ 𝐵 ∧ (abs‘(𝑤 − 𝐵)) < 𝑣) → (abs‘(((𝐹 ↾ (-∞(,)𝐵))‘𝑤) − 𝐿)) < 𝑦)) → (𝑤 ∈ (𝐴 ∩ (-∞(,)𝐵)) → ((𝑤 ≠ 𝐵 ∧ (abs‘(𝑤 − 𝐵)) < 𝑣) → (abs‘((𝐹‘𝑤) − 𝐿)) < 𝑦)))
318	307, 317	ralrimi 3252	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((𝜑 ∧ ∀𝑤 ∈ (𝐴 ∩ (-∞(,)𝐵))((𝑤 ≠ 𝐵 ∧ (abs‘(𝑤 − 𝐵)) < 𝑣) → (abs‘(((𝐹 ↾ (-∞(,)𝐵))‘𝑤) − 𝐿)) < 𝑦)) → ∀𝑤 ∈ (𝐴 ∩ (-∞(,)𝐵))((𝑤 ≠ 𝐵 ∧ (abs‘(𝑤 − 𝐵)) < 𝑣) → (abs‘((𝐹‘𝑤) − 𝐿)) < 𝑦))
319	304, 305, 318	syl2anc 582	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((((𝜑 ∧ 𝑦 ∈ ℝ+) ∧ 𝑧 ∈ ℝ+ ∧ ∀𝑤 ∈ 𝐴 ((𝑤 ≠ 𝐵 ∧ (abs‘(𝑤 − 𝐵)) < 𝑧) → (abs‘((𝐹‘𝑤) − 𝑥)) < 𝑦)) ∧ 𝑣 ∈ ℝ+ ∧ ∀𝑤 ∈ (𝐴 ∩ (-∞(,)𝐵))((𝑤 ≠ 𝐵 ∧ (abs‘(𝑤 − 𝐵)) < 𝑣) → (abs‘(((𝐹 ↾ (-∞(,)𝐵))‘𝑤) − 𝐿)) < 𝑦)) ∧ 𝑎 ∈ ((𝐴 ∩ (-∞(,)𝐵)) ∖ {𝐵}) ∧ ((abs‘(𝑎 − 𝐵)) < 𝑧 ∧ (abs‘(𝑎 − 𝐵)) < 𝑣)) → ∀𝑤 ∈ (𝐴 ∩ (-∞(,)𝐵))((𝑤 ≠ 𝐵 ∧ (abs‘(𝑤 − 𝐵)) < 𝑣) → (abs‘((𝐹‘𝑤) − 𝐿)) < 𝑦))
320	290	anim1i 613	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((𝑎 ∈ ((𝐴 ∩ (-∞(,)𝐵)) ∖ {𝐵}) ∧ (abs‘(𝑎 − 𝐵)) < 𝑣) → (𝑎 ≠ 𝐵 ∧ (abs‘(𝑎 − 𝐵)) < 𝑣))
321	320	adantrl 714	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((𝑎 ∈ ((𝐴 ∩ (-∞(,)𝐵)) ∖ {𝐵}) ∧ ((abs‘(𝑎 − 𝐵)) < 𝑧 ∧ (abs‘(𝑎 − 𝐵)) < 𝑣)) → (𝑎 ≠ 𝐵 ∧ (abs‘(𝑎 − 𝐵)) < 𝑣))
322	321	3adant1 1127	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((((𝜑 ∧ 𝑦 ∈ ℝ+) ∧ 𝑧 ∈ ℝ+ ∧ ∀𝑤 ∈ 𝐴 ((𝑤 ≠ 𝐵 ∧ (abs‘(𝑤 − 𝐵)) < 𝑧) → (abs‘((𝐹‘𝑤) − 𝑥)) < 𝑦)) ∧ 𝑣 ∈ ℝ+ ∧ ∀𝑤 ∈ (𝐴 ∩ (-∞(,)𝐵))((𝑤 ≠ 𝐵 ∧ (abs‘(𝑤 − 𝐵)) < 𝑣) → (abs‘(((𝐹 ↾ (-∞(,)𝐵))‘𝑤) − 𝐿)) < 𝑦)) ∧ 𝑎 ∈ ((𝐴 ∩ (-∞(,)𝐵)) ∖ {𝐵}) ∧ ((abs‘(𝑎 − 𝐵)) < 𝑧 ∧ (abs‘(𝑎 − 𝐵)) < 𝑣)) → (𝑎 ≠ 𝐵 ∧ (abs‘(𝑎 − 𝐵)) < 𝑣))
323	296	breq1d 5162	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (𝑤 = 𝑎 → ((abs‘(𝑤 − 𝐵)) < 𝑣 ↔ (abs‘(𝑎 − 𝐵)) < 𝑣))
324	295, 323	anbi12d 630	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝑤 = 𝑎 → ((𝑤 ≠ 𝐵 ∧ (abs‘(𝑤 − 𝐵)) < 𝑣) ↔ (𝑎 ≠ 𝐵 ∧ (abs‘(𝑎 − 𝐵)) < 𝑣)))
325	324	imbrov2fvoveq 7451	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝑤 = 𝑎 → (((𝑤 ≠ 𝐵 ∧ (abs‘(𝑤 − 𝐵)) < 𝑣) → (abs‘((𝐹‘𝑤) − 𝐿)) < 𝑦) ↔ ((𝑎 ≠ 𝐵 ∧ (abs‘(𝑎 − 𝐵)) < 𝑣) → (abs‘((𝐹‘𝑎) − 𝐿)) < 𝑦)))
326	325	rspcva 3609	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((𝑎 ∈ (𝐴 ∩ (-∞(,)𝐵)) ∧ ∀𝑤 ∈ (𝐴 ∩ (-∞(,)𝐵))((𝑤 ≠ 𝐵 ∧ (abs‘(𝑤 − 𝐵)) < 𝑣) → (abs‘((𝐹‘𝑤) − 𝐿)) < 𝑦)) → ((𝑎 ≠ 𝐵 ∧ (abs‘(𝑎 − 𝐵)) < 𝑣) → (abs‘((𝐹‘𝑎) − 𝐿)) < 𝑦))
327	326	imp 405	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((𝑎 ∈ (𝐴 ∩ (-∞(,)𝐵)) ∧ ∀𝑤 ∈ (𝐴 ∩ (-∞(,)𝐵))((𝑤 ≠ 𝐵 ∧ (abs‘(𝑤 − 𝐵)) < 𝑣) → (abs‘((𝐹‘𝑤) − 𝐿)) < 𝑦)) ∧ (𝑎 ≠ 𝐵 ∧ (abs‘(𝑎 − 𝐵)) < 𝑣)) → (abs‘((𝐹‘𝑎) − 𝐿)) < 𝑦)
328	303, 319, 322, 327	syl21anc 836	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((((𝜑 ∧ 𝑦 ∈ ℝ+) ∧ 𝑧 ∈ ℝ+ ∧ ∀𝑤 ∈ 𝐴 ((𝑤 ≠ 𝐵 ∧ (abs‘(𝑤 − 𝐵)) < 𝑧) → (abs‘((𝐹‘𝑤) − 𝑥)) < 𝑦)) ∧ 𝑣 ∈ ℝ+ ∧ ∀𝑤 ∈ (𝐴 ∩ (-∞(,)𝐵))((𝑤 ≠ 𝐵 ∧ (abs‘(𝑤 − 𝐵)) < 𝑣) → (abs‘(((𝐹 ↾ (-∞(,)𝐵))‘𝑤) − 𝐿)) < 𝑦)) ∧ 𝑎 ∈ ((𝐴 ∩ (-∞(,)𝐵)) ∖ {𝐵}) ∧ ((abs‘(𝑎 − 𝐵)) < 𝑧 ∧ (abs‘(𝑎 − 𝐵)) < 𝑣)) → (abs‘((𝐹‘𝑎) − 𝐿)) < 𝑦)
329		rspe 3244	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝑎 ∈ 𝐴 ∧ ((abs‘((𝐹‘𝑎) − 𝑥)) < 𝑦 ∧ (abs‘((𝐹‘𝑎) − 𝐿)) < 𝑦)) → ∃𝑎 ∈ 𝐴 ((abs‘((𝐹‘𝑎) − 𝑥)) < 𝑦 ∧ (abs‘((𝐹‘𝑎) − 𝐿)) < 𝑦))
330	288, 302, 328, 329	syl12anc 835	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((((𝜑 ∧ 𝑦 ∈ ℝ+) ∧ 𝑧 ∈ ℝ+ ∧ ∀𝑤 ∈ 𝐴 ((𝑤 ≠ 𝐵 ∧ (abs‘(𝑤 − 𝐵)) < 𝑧) → (abs‘((𝐹‘𝑤) − 𝑥)) < 𝑦)) ∧ 𝑣 ∈ ℝ+ ∧ ∀𝑤 ∈ (𝐴 ∩ (-∞(,)𝐵))((𝑤 ≠ 𝐵 ∧ (abs‘(𝑤 − 𝐵)) < 𝑣) → (abs‘(((𝐹 ↾ (-∞(,)𝐵))‘𝑤) − 𝐿)) < 𝑦)) ∧ 𝑎 ∈ ((𝐴 ∩ (-∞(,)𝐵)) ∖ {𝐵}) ∧ ((abs‘(𝑎 − 𝐵)) < 𝑧 ∧ (abs‘(𝑎 − 𝐵)) < 𝑣)) → ∃𝑎 ∈ 𝐴 ((abs‘((𝐹‘𝑎) − 𝑥)) < 𝑦 ∧ (abs‘((𝐹‘𝑎) − 𝐿)) < 𝑦))
331	330	3exp 1116	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((𝜑 ∧ 𝑦 ∈ ℝ+) ∧ 𝑧 ∈ ℝ+ ∧ ∀𝑤 ∈ 𝐴 ((𝑤 ≠ 𝐵 ∧ (abs‘(𝑤 − 𝐵)) < 𝑧) → (abs‘((𝐹‘𝑤) − 𝑥)) < 𝑦)) ∧ 𝑣 ∈ ℝ+ ∧ ∀𝑤 ∈ (𝐴 ∩ (-∞(,)𝐵))((𝑤 ≠ 𝐵 ∧ (abs‘(𝑤 − 𝐵)) < 𝑣) → (abs‘(((𝐹 ↾ (-∞(,)𝐵))‘𝑤) − 𝐿)) < 𝑦)) → (𝑎 ∈ ((𝐴 ∩ (-∞(,)𝐵)) ∖ {𝐵}) → (((abs‘(𝑎 − 𝐵)) < 𝑧 ∧ (abs‘(𝑎 − 𝐵)) < 𝑣) → ∃𝑎 ∈ 𝐴 ((abs‘((𝐹‘𝑎) − 𝑥)) < 𝑦 ∧ (abs‘((𝐹‘𝑎) − 𝐿)) < 𝑦))))
332	285, 286, 331	rexlimd 3261	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝜑 ∧ 𝑦 ∈ ℝ+) ∧ 𝑧 ∈ ℝ+ ∧ ∀𝑤 ∈ 𝐴 ((𝑤 ≠ 𝐵 ∧ (abs‘(𝑤 − 𝐵)) < 𝑧) → (abs‘((𝐹‘𝑤) − 𝑥)) < 𝑦)) ∧ 𝑣 ∈ ℝ+ ∧ ∀𝑤 ∈ (𝐴 ∩ (-∞(,)𝐵))((𝑤 ≠ 𝐵 ∧ (abs‘(𝑤 − 𝐵)) < 𝑣) → (abs‘(((𝐹 ↾ (-∞(,)𝐵))‘𝑤) − 𝐿)) < 𝑦)) → (∃𝑎 ∈ ((𝐴 ∩ (-∞(,)𝐵)) ∖ {𝐵})((abs‘(𝑎 − 𝐵)) < 𝑧 ∧ (abs‘(𝑎 − 𝐵)) < 𝑣) → ∃𝑎 ∈ 𝐴 ((abs‘((𝐹‘𝑎) − 𝑥)) < 𝑦 ∧ (abs‘((𝐹‘𝑎) − 𝐿)) < 𝑦)))
333	284, 332	mpd 15	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝜑 ∧ 𝑦 ∈ ℝ+) ∧ 𝑧 ∈ ℝ+ ∧ ∀𝑤 ∈ 𝐴 ((𝑤 ≠ 𝐵 ∧ (abs‘(𝑤 − 𝐵)) < 𝑧) → (abs‘((𝐹‘𝑤) − 𝑥)) < 𝑦)) ∧ 𝑣 ∈ ℝ+ ∧ ∀𝑤 ∈ (𝐴 ∩ (-∞(,)𝐵))((𝑤 ≠ 𝐵 ∧ (abs‘(𝑤 − 𝐵)) < 𝑣) → (abs‘(((𝐹 ↾ (-∞(,)𝐵))‘𝑤) − 𝐿)) < 𝑦)) → ∃𝑎 ∈ 𝐴 ((abs‘((𝐹‘𝑎) − 𝑥)) < 𝑦 ∧ (abs‘((𝐹‘𝑎) − 𝐿)) < 𝑦))
334	333	3exp 1116	. . . . . . . . . . . . . . . . . 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 1116	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑦 ∈ ℝ+) → (𝑧 ∈ ℝ+ → (∀𝑤 ∈ 𝐴 ((𝑤 ≠ 𝐵 ∧ (abs‘(𝑤 − 𝐵)) < 𝑧) → (abs‘((𝐹‘𝑤) − 𝑥)) < 𝑦) → ∃𝑎 ∈ 𝐴 ((abs‘((𝐹‘𝑎) − 𝑥)) < 𝑦 ∧ (abs‘((𝐹‘𝑎) − 𝐿)) < 𝑦))))
338	337	rexlimdv 3150	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑦 ∈ ℝ+) → (∃𝑧 ∈ ℝ+ ∀𝑤 ∈ 𝐴 ((𝑤 ≠ 𝐵 ∧ (abs‘(𝑤 − 𝐵)) < 𝑧) → (abs‘((𝐹‘𝑤) − 𝑥)) < 𝑦) → ∃𝑎 ∈ 𝐴 ((abs‘((𝐹‘𝑎) − 𝑥)) < 𝑦 ∧ (abs‘((𝐹‘𝑎) − 𝐿)) < 𝑦)))
339	338	imp 405	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑦 ∈ ℝ+) ∧ ∃𝑧 ∈ ℝ+ ∀𝑤 ∈ 𝐴 ((𝑤 ≠ 𝐵 ∧ (abs‘(𝑤 − 𝐵)) < 𝑧) → (abs‘((𝐹‘𝑤) − 𝑥)) < 𝑦)) → ∃𝑎 ∈ 𝐴 ((abs‘((𝐹‘𝑎) − 𝑥)) < 𝑦 ∧ (abs‘((𝐹‘𝑎) − 𝐿)) < 𝑦))
340	339	adantllr 717	. . . . . . . . . . . 12 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℂ) ∧ 𝑦 ∈ ℝ+) ∧ ∃𝑧 ∈ ℝ+ ∀𝑤 ∈ 𝐴 ((𝑤 ≠ 𝐵 ∧ (abs‘(𝑤 − 𝐵)) < 𝑧) → (abs‘((𝐹‘𝑤) − 𝑥)) < 𝑦)) → ∃𝑎 ∈ 𝐴 ((abs‘((𝐹‘𝑎) − 𝑥)) < 𝑦 ∧ (abs‘((𝐹‘𝑎) − 𝐿)) < 𝑦))
341	231, 340	reximddv3 3169	. . . . . . . . . . 11 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℂ) ∧ 𝑦 ∈ ℝ+) ∧ ∃𝑧 ∈ ℝ+ ∀𝑤 ∈ 𝐴 ((𝑤 ≠ 𝐵 ∧ (abs‘(𝑤 − 𝐵)) < 𝑧) → (abs‘((𝐹‘𝑤) − 𝑥)) < 𝑦)) → ∃𝑎 ∈ 𝐴 ∃𝑏 ∈ 𝐴 (abs‘(𝑅 − 𝐿)) < (4 · 𝑦))
342	32, 33, 35, 341	syl21anc 836	. . . . . . . . . 10 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℂ) ∧ ∀𝑦 ∈ ℝ+ ∃𝑧 ∈ ℝ+ ∀𝑤 ∈ 𝐴 ((𝑤 ≠ 𝐵 ∧ (abs‘(𝑤 − 𝐵)) < 𝑧) → (abs‘((𝐹‘𝑤) − 𝑥)) < 𝑦)) ∧ 𝑦 ∈ ℝ+) → ∃𝑎 ∈ 𝐴 ∃𝑏 ∈ 𝐴 (abs‘(𝑅 − 𝐿)) < (4 · 𝑦))
343	342	ex 411	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑥 ∈ ℂ) ∧ ∀𝑦 ∈ ℝ+ ∃𝑧 ∈ ℝ+ ∀𝑤 ∈ 𝐴 ((𝑤 ≠ 𝐵 ∧ (abs‘(𝑤 − 𝐵)) < 𝑧) → (abs‘((𝐹‘𝑤) − 𝑥)) < 𝑦)) → (𝑦 ∈ ℝ+ → ∃𝑎 ∈ 𝐴 ∃𝑏 ∈ 𝐴 (abs‘(𝑅 − 𝐿)) < (4 · 𝑦)))
344	24, 25, 31, 343	vtoclf 3551	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑥 ∈ ℂ) ∧ ∀𝑦 ∈ ℝ+ ∃𝑧 ∈ ℝ+ ∀𝑤 ∈ 𝐴 ((𝑤 ≠ 𝐵 ∧ (abs‘(𝑤 − 𝐵)) < 𝑧) → (abs‘((𝐹‘𝑤) − 𝑥)) < 𝑦)) → (((abs‘(𝑅 − 𝐿)) / 4) ∈ ℝ+ → ∃𝑎 ∈ 𝐴 ∃𝑏 ∈ 𝐴 (abs‘(𝑅 − 𝐿)) < (4 · ((abs‘(𝑅 − 𝐿)) / 4))))
345	19, 344	mpd 15	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑥 ∈ ℂ) ∧ ∀𝑦 ∈ ℝ+ ∃𝑧 ∈ ℝ+ ∀𝑤 ∈ 𝐴 ((𝑤 ≠ 𝐵 ∧ (abs‘(𝑤 − 𝐵)) < 𝑧) → (abs‘((𝐹‘𝑤) − 𝑥)) < 𝑦)) → ∃𝑎 ∈ 𝐴 ∃𝑏 ∈ 𝐴 (abs‘(𝑅 − 𝐿)) < (4 · ((abs‘(𝑅 − 𝐿)) / 4)))
346		simpr 483	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (abs‘(𝑅 − 𝐿)) < (4 · ((abs‘(𝑅 − 𝐿)) / 4))) → (abs‘(𝑅 − 𝐿)) < (4 · ((abs‘(𝑅 − 𝐿)) / 4)))
347		abssubrp 44686	. . . . . . . . . . . . . . . 16 ⊢ ((𝑅 ∈ ℂ ∧ 𝐿 ∈ ℂ ∧ 𝑅 ≠ 𝐿) → (abs‘(𝑅 − 𝐿)) ∈ ℝ+)
348	3, 7, 11, 347	syl3anc 1368	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (abs‘(𝑅 − 𝐿)) ∈ ℝ+)
349	348	rpcnd 13058	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (abs‘(𝑅 − 𝐿)) ∈ ℂ)
350	349	adantr 479	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ (abs‘(𝑅 − 𝐿)) < (4 · ((abs‘(𝑅 − 𝐿)) / 4))) → (abs‘(𝑅 − 𝐿)) ∈ ℂ)
351		4cn 12335	. . . . . . . . . . . . . 14 ⊢ 4 ∈ ℂ
352	351	a1i 11	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ (abs‘(𝑅 − 𝐿)) < (4 · ((abs‘(𝑅 − 𝐿)) / 4))) → 4 ∈ ℂ)
353		4ne0 12358	. . . . . . . . . . . . . 14 ⊢ 4 ≠ 0
354	353	a1i 11	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ (abs‘(𝑅 − 𝐿)) < (4 · ((abs‘(𝑅 − 𝐿)) / 4))) → 4 ≠ 0)
355	350, 352, 354	divcan2d 12030	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (abs‘(𝑅 − 𝐿)) < (4 · ((abs‘(𝑅 − 𝐿)) / 4))) → (4 · ((abs‘(𝑅 − 𝐿)) / 4)) = (abs‘(𝑅 − 𝐿)))
356	346, 355	breqtrd 5178	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (abs‘(𝑅 − 𝐿)) < (4 · ((abs‘(𝑅 − 𝐿)) / 4))) → (abs‘(𝑅 − 𝐿)) < (abs‘(𝑅 − 𝐿)))
357	356	ex 411	. . . . . . . . . 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 3208	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑥 ∈ ℂ) ∧ ∀𝑦 ∈ ℝ+ ∃𝑧 ∈ ℝ+ ∀𝑤 ∈ 𝐴 ((𝑤 ≠ 𝐵 ∧ (abs‘(𝑤 − 𝐵)) < 𝑧) → (abs‘((𝐹‘𝑤) − 𝑥)) < 𝑦)) → (∃𝑎 ∈ 𝐴 ∃𝑏 ∈ 𝐴 (abs‘(𝑅 − 𝐿)) < (4 · ((abs‘(𝑅 − 𝐿)) / 4)) → (abs‘(𝑅 − 𝐿)) < (abs‘(𝑅 − 𝐿))))
361	345, 360	mpd 15	. . . . . 6 ⊢ (((𝜑 ∧ 𝑥 ∈ ℂ) ∧ ∀𝑦 ∈ ℝ+ ∃𝑧 ∈ ℝ+ ∀𝑤 ∈ 𝐴 ((𝑤 ≠ 𝐵 ∧ (abs‘(𝑤 − 𝐵)) < 𝑧) → (abs‘((𝐹‘𝑤) − 𝑥)) < 𝑦)) → (abs‘(𝑅 − 𝐿)) < (abs‘(𝑅 − 𝐿)))
362	9	abscld 15423	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑥 ∈ ℂ) ∧ ∀𝑦 ∈ ℝ+ ∃𝑧 ∈ ℝ+ ∀𝑤 ∈ 𝐴 ((𝑤 ≠ 𝐵 ∧ (abs‘(𝑤 − 𝐵)) < 𝑧) → (abs‘((𝐹‘𝑤) − 𝑥)) < 𝑦)) → (abs‘(𝑅 − 𝐿)) ∈ ℝ)
363	362	ltnrd 11386	. . . . . 6 ⊢ (((𝜑 ∧ 𝑥 ∈ ℂ) ∧ ∀𝑦 ∈ ℝ+ ∃𝑧 ∈ ℝ+ ∀𝑤 ∈ 𝐴 ((𝑤 ≠ 𝐵 ∧ (abs‘(𝑤 − 𝐵)) < 𝑧) → (abs‘((𝐹‘𝑤) − 𝑥)) < 𝑦)) → ¬ (abs‘(𝑅 − 𝐿)) < (abs‘(𝑅 − 𝐿)))
364	361, 363	pm2.65da 815	. . . . 5 ⊢ ((𝜑 ∧ 𝑥 ∈ ℂ) → ¬ ∀𝑦 ∈ ℝ+ ∃𝑧 ∈ ℝ+ ∀𝑤 ∈ 𝐴 ((𝑤 ≠ 𝐵 ∧ (abs‘(𝑤 − 𝐵)) < 𝑧) → (abs‘((𝐹‘𝑤) − 𝑥)) < 𝑦))
365	364	ex 411	. . . 4 ⊢ (𝜑 → (𝑥 ∈ ℂ → ¬ ∀𝑦 ∈ ℝ+ ∃𝑧 ∈ ℝ+ ∀𝑤 ∈ 𝐴 ((𝑤 ≠ 𝐵 ∧ (abs‘(𝑤 − 𝐵)) < 𝑧) → (abs‘((𝐹‘𝑤) − 𝑥)) < 𝑦)))
366		imnan 398	. . . 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 25828	. . 3 ⊢ (𝜑 → (𝑥 ∈ (𝐹 limℂ 𝐵) ↔ (𝑥 ∈ ℂ ∧ ∀𝑦 ∈ ℝ+ ∃𝑧 ∈ ℝ+ ∀𝑤 ∈ 𝐴 ((𝑤 ≠ 𝐵 ∧ (abs‘(𝑤 − 𝐵)) < 𝑧) → (abs‘((𝐹‘𝑤) − 𝑥)) < 𝑦))))
371	367, 370	mtbird 324	. 2 ⊢ (𝜑 → ¬ 𝑥 ∈ (𝐹 limℂ 𝐵))
372	371	eq0rdv 4408	1 ⊢ (𝜑 → (𝐹 limℂ 𝐵) = ∅)

Syntax hints:  ¬ wn 3   → wi 4   ∧ wa 394   ∧ w3a 1084   = wceq 1533   ∈ wcel 2098   ≠ wne 2937  ∀wral 3058  ∃wrex 3067   ∖ cdif 3946   ∩ cin 3948   ⊆ wss 3949  ∅c0 4326  ifcif 4532  {csn 4632  ∪ cuni 4912   class class class wbr 5152  ran crn 5683   ↾ cres 5684  ⟶wf 6549  ‘cfv 6553  (class class class)co 7426  ℂcc 11144  ℝcr 11145  0cc0 11146   + caddc 11149   · cmul 11151  +∞cpnf 11283  -∞cmnf 11284   < clt 11286   ≤ cle 11287   − cmin 11482   / cdiv 11909  4c4 12307  ℝ⁺crp 13014  (,)cioo 13364  abscabs 15221   ↾_t crest 17409  TopOpenctopn 17410  topGenctg 17426  ℂ_fldccnfld 21286  Topctop 22815  limPtclp 23058   lim_ℂ climc 25811

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1905  ax-6 1963  ax-7 2003  ax-8 2100  ax-9 2108  ax-10 2129  ax-11 2146  ax-12 2166  ax-ext 2699  ax-rep 5289  ax-sep 5303  ax-nul 5310  ax-pow 5369  ax-pr 5433  ax-un 7746  ax-cnex 11202  ax-resscn 11203  ax-1cn 11204  ax-icn 11205  ax-addcl 11206  ax-addrcl 11207  ax-mulcl 11208  ax-mulrcl 11209  ax-mulcom 11210  ax-addass 11211  ax-mulass 11212  ax-distr 11213  ax-i2m1 11214  ax-1ne0 11215  ax-1rid 11216  ax-rnegex 11217  ax-rrecex 11218  ax-cnre 11219  ax-pre-lttri 11220  ax-pre-lttrn 11221  ax-pre-ltadd 11222  ax-pre-mulgt0 11223  ax-pre-sup 11224

This theorem depends on definitions:  df-bi 206  df-an 395  df-or 846  df-3or 1085  df-3an 1086  df-tru 1536  df-fal 1546  df-ex 1774  df-nf 1778  df-sb 2060  df-mo 2529  df-eu 2558  df-clab 2706  df-cleq 2720  df-clel 2806  df-nfc 2881  df-ne 2938  df-nel 3044  df-ral 3059  df-rex 3068  df-rmo 3374  df-reu 3375  df-rab 3431  df-v 3475  df-sbc 3779  df-csb 3895  df-dif 3952  df-un 3954  df-in 3956  df-ss 3966  df-pss 3968  df-nul 4327  df-if 4533  df-pw 4608  df-sn 4633  df-pr 4635  df-tp 4637  df-op 4639  df-uni 4913  df-int 4954  df-iun 5002  df-iin 5003  df-br 5153  df-opab 5215  df-mpt 5236  df-tr 5270  df-id 5580  df-eprel 5586  df-po 5594  df-so 5595  df-fr 5637  df-we 5639  df-xp 5688  df-rel 5689  df-cnv 5690  df-co 5691  df-dm 5692  df-rn 5693  df-res 5694  df-ima 5695  df-pred 6310  df-ord 6377  df-on 6378  df-lim 6379  df-suc 6380  df-iota 6505  df-fun 6555  df-fn 6556  df-f 6557  df-f1 6558  df-fo 6559  df-f1o 6560  df-fv 6561  df-riota 7382  df-ov 7429  df-oprab 7430  df-mpo 7431  df-om 7877  df-1st 7999  df-2nd 8000  df-frecs 8293  df-wrecs 8324  df-recs 8398  df-rdg 8437  df-1o 8493  df-er 8731  df-map 8853  df-pm 8854  df-en 8971  df-dom 8972  df-sdom 8973  df-fin 8974  df-fi 9442  df-sup 9473  df-inf 9474  df-pnf 11288  df-mnf 11289  df-xr 11290  df-ltxr 11291  df-le 11292  df-sub 11484  df-neg 11485  df-div 11910  df-nn 12251  df-2 12313  df-3 12314  df-4 12315  df-5 12316  df-6 12317  df-7 12318  df-8 12319  df-9 12320  df-n0 12511  df-z 12597  df-dec 12716  df-uz 12861  df-q 12971  df-rp 13015  df-xneg 13132  df-xadd 13133  df-xmul 13134  df-ioo 13368  df-fz 13525  df-seq 14007  df-exp 14067  df-cj 15086  df-re 15087  df-im 15088  df-sqrt 15222  df-abs 15223  df-struct 17123  df-slot 17158  df-ndx 17170  df-base 17188  df-plusg 17253  df-mulr 17254  df-starv 17255  df-tset 17259  df-ple 17260  df-ds 17262  df-unif 17263  df-rest 17411  df-topn 17412  df-topgen 17432  df-psmet 21278  df-xmet 21279  df-met 21280  df-bl 21281  df-mopn 21282  df-cnfld 21287  df-top 22816  df-topon 22833  df-topsp 22855  df-bases 22869  df-cld 22943  df-ntr 22944  df-cls 22945  df-nei 23022  df-lp 23060  df-cnp 23152  df-xms 24246  df-ms 24247  df-limc 25815

This theorem is referenced by:  limclr  45072  jumpncnp  45315