limcleqr - Mathbox for Glauco Siliprandi

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

Theorem limcleqr 42653

Description: If the left and the right limits are equal, the limit of the function exits and the three limits coincide. (Contributed by Glauco Siliprandi, 11-Dec-2019.)

**Hypotheses**
Ref	Expression
limcleqr.k	⊢ 𝐾 = (TopOpen‘ℂ_fld)
limcleqr.a	⊢ (𝜑 → 𝐴 ⊆ ℝ)
limcleqr.j	⊢ 𝐽 = (topGen‘ran (,))
limcleqr.f	⊢ (𝜑 → 𝐹:𝐴⟶ℂ)
limcleqr.b	⊢ (𝜑 → 𝐵 ∈ ℝ)
limcleqr.l	⊢ (𝜑 → 𝐿 ∈ ((𝐹 ↾ (-∞(,)𝐵)) lim_ℂ 𝐵))
limcleqr.r	⊢ (𝜑 → 𝑅 ∈ ((𝐹 ↾ (𝐵(,)+∞)) lim_ℂ 𝐵))
limcleqr.leqr	⊢ (𝜑 → 𝐿 = 𝑅)

**Assertion**
Ref	Expression
limcleqr	⊢ (𝜑 → 𝐿 ∈ (𝐹 lim_ℂ 𝐵))

Proof of Theorem limcleqr Dummy variables 𝑎 𝑏 𝑥 𝑦 𝑧 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		limccl 24575	. . 3 ⊢ ((𝐹 ↾ (-∞(,)𝐵)) lim_ℂ 𝐵) ⊆ ℂ
2		limcleqr.l	. . 3 ⊢ (𝜑 → 𝐿 ∈ ((𝐹 ↾ (-∞(,)𝐵)) lim_ℂ 𝐵))
3	1, 2	sseldi 3891	. 2 ⊢ (𝜑 → 𝐿 ∈ ℂ)
4		simp-4r 784	. . . . . . 7 ⊢ ((((((𝜑 ∧ 𝑥 ∈ ℝ⁺) ∧ 𝑎 ∈ ℝ⁺) ∧ ∀𝑧 ∈ (𝐴 ∩ (-∞(,)𝐵))((𝑧 ≠ 𝐵 ∧ (abs‘(𝑧 − 𝐵)) < 𝑎) → (abs‘(((𝐹 ↾ (-∞(,)𝐵))‘𝑧) − 𝐿)) < 𝑥)) ∧ 𝑏 ∈ ℝ⁺) ∧ ∀𝑧 ∈ (𝐴 ∩ (𝐵(,)+∞))((𝑧 ≠ 𝐵 ∧ (abs‘(𝑧 − 𝐵)) < 𝑏) → (abs‘(((𝐹 ↾ (𝐵(,)+∞))‘𝑧) − 𝐿)) < 𝑥)) → 𝑎 ∈ ℝ⁺)
5		simplr 769	. . . . . . 7 ⊢ ((((((𝜑 ∧ 𝑥 ∈ ℝ⁺) ∧ 𝑎 ∈ ℝ⁺) ∧ ∀𝑧 ∈ (𝐴 ∩ (-∞(,)𝐵))((𝑧 ≠ 𝐵 ∧ (abs‘(𝑧 − 𝐵)) < 𝑎) → (abs‘(((𝐹 ↾ (-∞(,)𝐵))‘𝑧) − 𝐿)) < 𝑥)) ∧ 𝑏 ∈ ℝ⁺) ∧ ∀𝑧 ∈ (𝐴 ∩ (𝐵(,)+∞))((𝑧 ≠ 𝐵 ∧ (abs‘(𝑧 − 𝐵)) < 𝑏) → (abs‘(((𝐹 ↾ (𝐵(,)+∞))‘𝑧) − 𝐿)) < 𝑥)) → 𝑏 ∈ ℝ⁺)
6	4, 5	ifcld 4467	. . . . . 6 ⊢ ((((((𝜑 ∧ 𝑥 ∈ ℝ⁺) ∧ 𝑎 ∈ ℝ⁺) ∧ ∀𝑧 ∈ (𝐴 ∩ (-∞(,)𝐵))((𝑧 ≠ 𝐵 ∧ (abs‘(𝑧 − 𝐵)) < 𝑎) → (abs‘(((𝐹 ↾ (-∞(,)𝐵))‘𝑧) − 𝐿)) < 𝑥)) ∧ 𝑏 ∈ ℝ⁺) ∧ ∀𝑧 ∈ (𝐴 ∩ (𝐵(,)+∞))((𝑧 ≠ 𝐵 ∧ (abs‘(𝑧 − 𝐵)) < 𝑏) → (abs‘(((𝐹 ↾ (𝐵(,)+∞))‘𝑧) − 𝐿)) < 𝑥)) → if(𝑎 ≤ 𝑏, 𝑎, 𝑏) ∈ ℝ⁺)
7		nfv 1916	. . . . . . . . . . 11 ⊢ Ⅎ𝑧(𝜑 ∧ 𝑥 ∈ ℝ⁺)
8		nfv 1916	. . . . . . . . . . 11 ⊢ Ⅎ𝑧 𝑎 ∈ ℝ⁺
9	7, 8	nfan 1901	. . . . . . . . . 10 ⊢ Ⅎ𝑧((𝜑 ∧ 𝑥 ∈ ℝ⁺) ∧ 𝑎 ∈ ℝ⁺)
10		nfra1 3148	. . . . . . . . . 10 ⊢ Ⅎ𝑧∀𝑧 ∈ (𝐴 ∩ (-∞(,)𝐵))((𝑧 ≠ 𝐵 ∧ (abs‘(𝑧 − 𝐵)) < 𝑎) → (abs‘(((𝐹 ↾ (-∞(,)𝐵))‘𝑧) − 𝐿)) < 𝑥)
11	9, 10	nfan 1901	. . . . . . . . 9 ⊢ Ⅎ𝑧(((𝜑 ∧ 𝑥 ∈ ℝ⁺) ∧ 𝑎 ∈ ℝ⁺) ∧ ∀𝑧 ∈ (𝐴 ∩ (-∞(,)𝐵))((𝑧 ≠ 𝐵 ∧ (abs‘(𝑧 − 𝐵)) < 𝑎) → (abs‘(((𝐹 ↾ (-∞(,)𝐵))‘𝑧) − 𝐿)) < 𝑥))
12		nfv 1916	. . . . . . . . 9 ⊢ Ⅎ𝑧 𝑏 ∈ ℝ⁺
13	11, 12	nfan 1901	. . . . . . . 8 ⊢ Ⅎ𝑧((((𝜑 ∧ 𝑥 ∈ ℝ⁺) ∧ 𝑎 ∈ ℝ⁺) ∧ ∀𝑧 ∈ (𝐴 ∩ (-∞(,)𝐵))((𝑧 ≠ 𝐵 ∧ (abs‘(𝑧 − 𝐵)) < 𝑎) → (abs‘(((𝐹 ↾ (-∞(,)𝐵))‘𝑧) − 𝐿)) < 𝑥)) ∧ 𝑏 ∈ ℝ⁺)
14		nfra1 3148	. . . . . . . 8 ⊢ Ⅎ𝑧∀𝑧 ∈ (𝐴 ∩ (𝐵(,)+∞))((𝑧 ≠ 𝐵 ∧ (abs‘(𝑧 − 𝐵)) < 𝑏) → (abs‘(((𝐹 ↾ (𝐵(,)+∞))‘𝑧) − 𝐿)) < 𝑥)
15	13, 14	nfan 1901	. . . . . . 7 ⊢ Ⅎ𝑧(((((𝜑 ∧ 𝑥 ∈ ℝ⁺) ∧ 𝑎 ∈ ℝ⁺) ∧ ∀𝑧 ∈ (𝐴 ∩ (-∞(,)𝐵))((𝑧 ≠ 𝐵 ∧ (abs‘(𝑧 − 𝐵)) < 𝑎) → (abs‘(((𝐹 ↾ (-∞(,)𝐵))‘𝑧) − 𝐿)) < 𝑥)) ∧ 𝑏 ∈ ℝ⁺) ∧ ∀𝑧 ∈ (𝐴 ∩ (𝐵(,)+∞))((𝑧 ≠ 𝐵 ∧ (abs‘(𝑧 − 𝐵)) < 𝑏) → (abs‘(((𝐹 ↾ (𝐵(,)+∞))‘𝑧) − 𝐿)) < 𝑥))
16		simp-6l 787	. . . . . . . . . . . . 13 ⊢ (((((((𝜑 ∧ 𝑥 ∈ ℝ⁺) ∧ 𝑎 ∈ ℝ⁺) ∧ ∀𝑧 ∈ (𝐴 ∩ (-∞(,)𝐵))((𝑧 ≠ 𝐵 ∧ (abs‘(𝑧 − 𝐵)) < 𝑎) → (abs‘(((𝐹 ↾ (-∞(,)𝐵))‘𝑧) − 𝐿)) < 𝑥)) ∧ 𝑏 ∈ ℝ⁺) ∧ ∀𝑧 ∈ (𝐴 ∩ (𝐵(,)+∞))((𝑧 ≠ 𝐵 ∧ (abs‘(𝑧 − 𝐵)) < 𝑏) → (abs‘(((𝐹 ↾ (𝐵(,)+∞))‘𝑧) − 𝐿)) < 𝑥)) ∧ 𝑧 < 𝐵) → 𝜑)
17	16	3ad2antl1 1183	. . . . . . . . . . . 12 ⊢ ((((((((𝜑 ∧ 𝑥 ∈ ℝ⁺) ∧ 𝑎 ∈ ℝ⁺) ∧ ∀𝑧 ∈ (𝐴 ∩ (-∞(,)𝐵))((𝑧 ≠ 𝐵 ∧ (abs‘(𝑧 − 𝐵)) < 𝑎) → (abs‘(((𝐹 ↾ (-∞(,)𝐵))‘𝑧) − 𝐿)) < 𝑥)) ∧ 𝑏 ∈ ℝ⁺) ∧ ∀𝑧 ∈ (𝐴 ∩ (𝐵(,)+∞))((𝑧 ≠ 𝐵 ∧ (abs‘(𝑧 − 𝐵)) < 𝑏) → (abs‘(((𝐹 ↾ (𝐵(,)+∞))‘𝑧) − 𝐿)) < 𝑥)) ∧ 𝑧 ∈ 𝐴 ∧ (𝑧 ≠ 𝐵 ∧ (abs‘(𝑧 − 𝐵)) < if(𝑎 ≤ 𝑏, 𝑎, 𝑏))) ∧ 𝑧 < 𝐵) → 𝜑)
18		simpl2 1190	. . . . . . . . . . . 12 ⊢ ((((((((𝜑 ∧ 𝑥 ∈ ℝ⁺) ∧ 𝑎 ∈ ℝ⁺) ∧ ∀𝑧 ∈ (𝐴 ∩ (-∞(,)𝐵))((𝑧 ≠ 𝐵 ∧ (abs‘(𝑧 − 𝐵)) < 𝑎) → (abs‘(((𝐹 ↾ (-∞(,)𝐵))‘𝑧) − 𝐿)) < 𝑥)) ∧ 𝑏 ∈ ℝ⁺) ∧ ∀𝑧 ∈ (𝐴 ∩ (𝐵(,)+∞))((𝑧 ≠ 𝐵 ∧ (abs‘(𝑧 − 𝐵)) < 𝑏) → (abs‘(((𝐹 ↾ (𝐵(,)+∞))‘𝑧) − 𝐿)) < 𝑥)) ∧ 𝑧 ∈ 𝐴 ∧ (𝑧 ≠ 𝐵 ∧ (abs‘(𝑧 − 𝐵)) < if(𝑎 ≤ 𝑏, 𝑎, 𝑏))) ∧ 𝑧 < 𝐵) → 𝑧 ∈ 𝐴)
19		simpr 489	. . . . . . . . . . . 12 ⊢ ((((((((𝜑 ∧ 𝑥 ∈ ℝ⁺) ∧ 𝑎 ∈ ℝ⁺) ∧ ∀𝑧 ∈ (𝐴 ∩ (-∞(,)𝐵))((𝑧 ≠ 𝐵 ∧ (abs‘(𝑧 − 𝐵)) < 𝑎) → (abs‘(((𝐹 ↾ (-∞(,)𝐵))‘𝑧) − 𝐿)) < 𝑥)) ∧ 𝑏 ∈ ℝ⁺) ∧ ∀𝑧 ∈ (𝐴 ∩ (𝐵(,)+∞))((𝑧 ≠ 𝐵 ∧ (abs‘(𝑧 − 𝐵)) < 𝑏) → (abs‘(((𝐹 ↾ (𝐵(,)+∞))‘𝑧) − 𝐿)) < 𝑥)) ∧ 𝑧 ∈ 𝐴 ∧ (𝑧 ≠ 𝐵 ∧ (abs‘(𝑧 − 𝐵)) < if(𝑎 ≤ 𝑏, 𝑎, 𝑏))) ∧ 𝑧 < 𝐵) → 𝑧 < 𝐵)
20		mnfxr 10737	. . . . . . . . . . . . . 14 ⊢ -∞ ∈ ℝ^*
21	20	a1i 11	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝐴 ∧ 𝑧 < 𝐵) → -∞ ∈ ℝ^*)
22		limcleqr.b	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → 𝐵 ∈ ℝ)
23	22	rexrd 10730	. . . . . . . . . . . . . 14 ⊢ (𝜑 → 𝐵 ∈ ℝ^*)
24	23	3ad2ant1 1131	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝐴 ∧ 𝑧 < 𝐵) → 𝐵 ∈ ℝ^*)
25		limcleqr.a	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → 𝐴 ⊆ ℝ)
26	25	sselda 3893	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝐴) → 𝑧 ∈ ℝ)
27	26	3adant3 1130	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝐴 ∧ 𝑧 < 𝐵) → 𝑧 ∈ ℝ)
28	27	mnfltd 12561	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝐴 ∧ 𝑧 < 𝐵) → -∞ < 𝑧)
29		simp3 1136	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝐴 ∧ 𝑧 < 𝐵) → 𝑧 < 𝐵)
30	21, 24, 27, 28, 29	eliood 42502	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝐴 ∧ 𝑧 < 𝐵) → 𝑧 ∈ (-∞(,)𝐵))
31	17, 18, 19, 30	syl3anc 1369	. . . . . . . . . . 11 ⊢ ((((((((𝜑 ∧ 𝑥 ∈ ℝ⁺) ∧ 𝑎 ∈ ℝ⁺) ∧ ∀𝑧 ∈ (𝐴 ∩ (-∞(,)𝐵))((𝑧 ≠ 𝐵 ∧ (abs‘(𝑧 − 𝐵)) < 𝑎) → (abs‘(((𝐹 ↾ (-∞(,)𝐵))‘𝑧) − 𝐿)) < 𝑥)) ∧ 𝑏 ∈ ℝ⁺) ∧ ∀𝑧 ∈ (𝐴 ∩ (𝐵(,)+∞))((𝑧 ≠ 𝐵 ∧ (abs‘(𝑧 − 𝐵)) < 𝑏) → (abs‘(((𝐹 ↾ (𝐵(,)+∞))‘𝑧) − 𝐿)) < 𝑥)) ∧ 𝑧 ∈ 𝐴 ∧ (𝑧 ≠ 𝐵 ∧ (abs‘(𝑧 − 𝐵)) < if(𝑎 ≤ 𝑏, 𝑎, 𝑏))) ∧ 𝑧 < 𝐵) → 𝑧 ∈ (-∞(,)𝐵))
32		fvres 6678	. . . . . . . . . . . . . 14 ⊢ (𝑧 ∈ (-∞(,)𝐵) → ((𝐹 ↾ (-∞(,)𝐵))‘𝑧) = (𝐹‘𝑧))
33	32	oveq1d 7166	. . . . . . . . . . . . 13 ⊢ (𝑧 ∈ (-∞(,)𝐵) → (((𝐹 ↾ (-∞(,)𝐵))‘𝑧) − 𝐿) = ((𝐹‘𝑧) − 𝐿))
34	33	eqcomd 2765	. . . . . . . . . . . 12 ⊢ (𝑧 ∈ (-∞(,)𝐵) → ((𝐹‘𝑧) − 𝐿) = (((𝐹 ↾ (-∞(,)𝐵))‘𝑧) − 𝐿))
35	34	fveq2d 6663	. . . . . . . . . . 11 ⊢ (𝑧 ∈ (-∞(,)𝐵) → (abs‘((𝐹‘𝑧) − 𝐿)) = (abs‘(((𝐹 ↾ (-∞(,)𝐵))‘𝑧) − 𝐿)))
36	31, 35	syl 17	. . . . . . . . . 10 ⊢ ((((((((𝜑 ∧ 𝑥 ∈ ℝ⁺) ∧ 𝑎 ∈ ℝ⁺) ∧ ∀𝑧 ∈ (𝐴 ∩ (-∞(,)𝐵))((𝑧 ≠ 𝐵 ∧ (abs‘(𝑧 − 𝐵)) < 𝑎) → (abs‘(((𝐹 ↾ (-∞(,)𝐵))‘𝑧) − 𝐿)) < 𝑥)) ∧ 𝑏 ∈ ℝ⁺) ∧ ∀𝑧 ∈ (𝐴 ∩ (𝐵(,)+∞))((𝑧 ≠ 𝐵 ∧ (abs‘(𝑧 − 𝐵)) < 𝑏) → (abs‘(((𝐹 ↾ (𝐵(,)+∞))‘𝑧) − 𝐿)) < 𝑥)) ∧ 𝑧 ∈ 𝐴 ∧ (𝑧 ≠ 𝐵 ∧ (abs‘(𝑧 − 𝐵)) < if(𝑎 ≤ 𝑏, 𝑎, 𝑏))) ∧ 𝑧 < 𝐵) → (abs‘((𝐹‘𝑧) − 𝐿)) = (abs‘(((𝐹 ↾ (-∞(,)𝐵))‘𝑧) − 𝐿)))
37		simp-4r 784	. . . . . . . . . . . . 13 ⊢ (((((((𝜑 ∧ 𝑥 ∈ ℝ⁺) ∧ 𝑎 ∈ ℝ⁺) ∧ ∀𝑧 ∈ (𝐴 ∩ (-∞(,)𝐵))((𝑧 ≠ 𝐵 ∧ (abs‘(𝑧 − 𝐵)) < 𝑎) → (abs‘(((𝐹 ↾ (-∞(,)𝐵))‘𝑧) − 𝐿)) < 𝑥)) ∧ 𝑏 ∈ ℝ⁺) ∧ ∀𝑧 ∈ (𝐴 ∩ (𝐵(,)+∞))((𝑧 ≠ 𝐵 ∧ (abs‘(𝑧 − 𝐵)) < 𝑏) → (abs‘(((𝐹 ↾ (𝐵(,)+∞))‘𝑧) − 𝐿)) < 𝑥)) ∧ 𝑧 < 𝐵) → ∀𝑧 ∈ (𝐴 ∩ (-∞(,)𝐵))((𝑧 ≠ 𝐵 ∧ (abs‘(𝑧 − 𝐵)) < 𝑎) → (abs‘(((𝐹 ↾ (-∞(,)𝐵))‘𝑧) − 𝐿)) < 𝑥))
38	37	3ad2antl1 1183	. . . . . . . . . . . 12 ⊢ ((((((((𝜑 ∧ 𝑥 ∈ ℝ⁺) ∧ 𝑎 ∈ ℝ⁺) ∧ ∀𝑧 ∈ (𝐴 ∩ (-∞(,)𝐵))((𝑧 ≠ 𝐵 ∧ (abs‘(𝑧 − 𝐵)) < 𝑎) → (abs‘(((𝐹 ↾ (-∞(,)𝐵))‘𝑧) − 𝐿)) < 𝑥)) ∧ 𝑏 ∈ ℝ⁺) ∧ ∀𝑧 ∈ (𝐴 ∩ (𝐵(,)+∞))((𝑧 ≠ 𝐵 ∧ (abs‘(𝑧 − 𝐵)) < 𝑏) → (abs‘(((𝐹 ↾ (𝐵(,)+∞))‘𝑧) − 𝐿)) < 𝑥)) ∧ 𝑧 ∈ 𝐴 ∧ (𝑧 ≠ 𝐵 ∧ (abs‘(𝑧 − 𝐵)) < if(𝑎 ≤ 𝑏, 𝑎, 𝑏))) ∧ 𝑧 < 𝐵) → ∀𝑧 ∈ (𝐴 ∩ (-∞(,)𝐵))((𝑧 ≠ 𝐵 ∧ (abs‘(𝑧 − 𝐵)) < 𝑎) → (abs‘(((𝐹 ↾ (-∞(,)𝐵))‘𝑧) − 𝐿)) < 𝑥))
39	18, 31	elind 4100	. . . . . . . . . . . 12 ⊢ ((((((((𝜑 ∧ 𝑥 ∈ ℝ⁺) ∧ 𝑎 ∈ ℝ⁺) ∧ ∀𝑧 ∈ (𝐴 ∩ (-∞(,)𝐵))((𝑧 ≠ 𝐵 ∧ (abs‘(𝑧 − 𝐵)) < 𝑎) → (abs‘(((𝐹 ↾ (-∞(,)𝐵))‘𝑧) − 𝐿)) < 𝑥)) ∧ 𝑏 ∈ ℝ⁺) ∧ ∀𝑧 ∈ (𝐴 ∩ (𝐵(,)+∞))((𝑧 ≠ 𝐵 ∧ (abs‘(𝑧 − 𝐵)) < 𝑏) → (abs‘(((𝐹 ↾ (𝐵(,)+∞))‘𝑧) − 𝐿)) < 𝑥)) ∧ 𝑧 ∈ 𝐴 ∧ (𝑧 ≠ 𝐵 ∧ (abs‘(𝑧 − 𝐵)) < if(𝑎 ≤ 𝑏, 𝑎, 𝑏))) ∧ 𝑧 < 𝐵) → 𝑧 ∈ (𝐴 ∩ (-∞(,)𝐵)))
40	38, 39	jca 516	. . . . . . . . . . 11 ⊢ ((((((((𝜑 ∧ 𝑥 ∈ ℝ⁺) ∧ 𝑎 ∈ ℝ⁺) ∧ ∀𝑧 ∈ (𝐴 ∩ (-∞(,)𝐵))((𝑧 ≠ 𝐵 ∧ (abs‘(𝑧 − 𝐵)) < 𝑎) → (abs‘(((𝐹 ↾ (-∞(,)𝐵))‘𝑧) − 𝐿)) < 𝑥)) ∧ 𝑏 ∈ ℝ⁺) ∧ ∀𝑧 ∈ (𝐴 ∩ (𝐵(,)+∞))((𝑧 ≠ 𝐵 ∧ (abs‘(𝑧 − 𝐵)) < 𝑏) → (abs‘(((𝐹 ↾ (𝐵(,)+∞))‘𝑧) − 𝐿)) < 𝑥)) ∧ 𝑧 ∈ 𝐴 ∧ (𝑧 ≠ 𝐵 ∧ (abs‘(𝑧 − 𝐵)) < if(𝑎 ≤ 𝑏, 𝑎, 𝑏))) ∧ 𝑧 < 𝐵) → (∀𝑧 ∈ (𝐴 ∩ (-∞(,)𝐵))((𝑧 ≠ 𝐵 ∧ (abs‘(𝑧 − 𝐵)) < 𝑎) → (abs‘(((𝐹 ↾ (-∞(,)𝐵))‘𝑧) − 𝐿)) < 𝑥) ∧ 𝑧 ∈ (𝐴 ∩ (-∞(,)𝐵))))
41		simpl3l 1226	. . . . . . . . . . . 12 ⊢ ((((((((𝜑 ∧ 𝑥 ∈ ℝ⁺) ∧ 𝑎 ∈ ℝ⁺) ∧ ∀𝑧 ∈ (𝐴 ∩ (-∞(,)𝐵))((𝑧 ≠ 𝐵 ∧ (abs‘(𝑧 − 𝐵)) < 𝑎) → (abs‘(((𝐹 ↾ (-∞(,)𝐵))‘𝑧) − 𝐿)) < 𝑥)) ∧ 𝑏 ∈ ℝ⁺) ∧ ∀𝑧 ∈ (𝐴 ∩ (𝐵(,)+∞))((𝑧 ≠ 𝐵 ∧ (abs‘(𝑧 − 𝐵)) < 𝑏) → (abs‘(((𝐹 ↾ (𝐵(,)+∞))‘𝑧) − 𝐿)) < 𝑥)) ∧ 𝑧 ∈ 𝐴 ∧ (𝑧 ≠ 𝐵 ∧ (abs‘(𝑧 − 𝐵)) < if(𝑎 ≤ 𝑏, 𝑎, 𝑏))) ∧ 𝑧 < 𝐵) → 𝑧 ≠ 𝐵)
42	4	adantr 485	. . . . . . . . . . . . . 14 ⊢ (((((((𝜑 ∧ 𝑥 ∈ ℝ⁺) ∧ 𝑎 ∈ ℝ⁺) ∧ ∀𝑧 ∈ (𝐴 ∩ (-∞(,)𝐵))((𝑧 ≠ 𝐵 ∧ (abs‘(𝑧 − 𝐵)) < 𝑎) → (abs‘(((𝐹 ↾ (-∞(,)𝐵))‘𝑧) − 𝐿)) < 𝑥)) ∧ 𝑏 ∈ ℝ⁺) ∧ ∀𝑧 ∈ (𝐴 ∩ (𝐵(,)+∞))((𝑧 ≠ 𝐵 ∧ (abs‘(𝑧 − 𝐵)) < 𝑏) → (abs‘(((𝐹 ↾ (𝐵(,)+∞))‘𝑧) − 𝐿)) < 𝑥)) ∧ 𝑧 < 𝐵) → 𝑎 ∈ ℝ⁺)
43	42	3ad2antl1 1183	. . . . . . . . . . . . 13 ⊢ ((((((((𝜑 ∧ 𝑥 ∈ ℝ⁺) ∧ 𝑎 ∈ ℝ⁺) ∧ ∀𝑧 ∈ (𝐴 ∩ (-∞(,)𝐵))((𝑧 ≠ 𝐵 ∧ (abs‘(𝑧 − 𝐵)) < 𝑎) → (abs‘(((𝐹 ↾ (-∞(,)𝐵))‘𝑧) − 𝐿)) < 𝑥)) ∧ 𝑏 ∈ ℝ⁺) ∧ ∀𝑧 ∈ (𝐴 ∩ (𝐵(,)+∞))((𝑧 ≠ 𝐵 ∧ (abs‘(𝑧 − 𝐵)) < 𝑏) → (abs‘(((𝐹 ↾ (𝐵(,)+∞))‘𝑧) − 𝐿)) < 𝑥)) ∧ 𝑧 ∈ 𝐴 ∧ (𝑧 ≠ 𝐵 ∧ (abs‘(𝑧 − 𝐵)) < if(𝑎 ≤ 𝑏, 𝑎, 𝑏))) ∧ 𝑧 < 𝐵) → 𝑎 ∈ ℝ⁺)
44	5	adantr 485	. . . . . . . . . . . . . 14 ⊢ (((((((𝜑 ∧ 𝑥 ∈ ℝ⁺) ∧ 𝑎 ∈ ℝ⁺) ∧ ∀𝑧 ∈ (𝐴 ∩ (-∞(,)𝐵))((𝑧 ≠ 𝐵 ∧ (abs‘(𝑧 − 𝐵)) < 𝑎) → (abs‘(((𝐹 ↾ (-∞(,)𝐵))‘𝑧) − 𝐿)) < 𝑥)) ∧ 𝑏 ∈ ℝ⁺) ∧ ∀𝑧 ∈ (𝐴 ∩ (𝐵(,)+∞))((𝑧 ≠ 𝐵 ∧ (abs‘(𝑧 − 𝐵)) < 𝑏) → (abs‘(((𝐹 ↾ (𝐵(,)+∞))‘𝑧) − 𝐿)) < 𝑥)) ∧ 𝑧 < 𝐵) → 𝑏 ∈ ℝ⁺)
45	44	3ad2antl1 1183	. . . . . . . . . . . . 13 ⊢ ((((((((𝜑 ∧ 𝑥 ∈ ℝ⁺) ∧ 𝑎 ∈ ℝ⁺) ∧ ∀𝑧 ∈ (𝐴 ∩ (-∞(,)𝐵))((𝑧 ≠ 𝐵 ∧ (abs‘(𝑧 − 𝐵)) < 𝑎) → (abs‘(((𝐹 ↾ (-∞(,)𝐵))‘𝑧) − 𝐿)) < 𝑥)) ∧ 𝑏 ∈ ℝ⁺) ∧ ∀𝑧 ∈ (𝐴 ∩ (𝐵(,)+∞))((𝑧 ≠ 𝐵 ∧ (abs‘(𝑧 − 𝐵)) < 𝑏) → (abs‘(((𝐹 ↾ (𝐵(,)+∞))‘𝑧) − 𝐿)) < 𝑥)) ∧ 𝑧 ∈ 𝐴 ∧ (𝑧 ≠ 𝐵 ∧ (abs‘(𝑧 − 𝐵)) < if(𝑎 ≤ 𝑏, 𝑎, 𝑏))) ∧ 𝑧 < 𝐵) → 𝑏 ∈ ℝ⁺)
46		simpl3r 1227	. . . . . . . . . . . . 13 ⊢ ((((((((𝜑 ∧ 𝑥 ∈ ℝ⁺) ∧ 𝑎 ∈ ℝ⁺) ∧ ∀𝑧 ∈ (𝐴 ∩ (-∞(,)𝐵))((𝑧 ≠ 𝐵 ∧ (abs‘(𝑧 − 𝐵)) < 𝑎) → (abs‘(((𝐹 ↾ (-∞(,)𝐵))‘𝑧) − 𝐿)) < 𝑥)) ∧ 𝑏 ∈ ℝ⁺) ∧ ∀𝑧 ∈ (𝐴 ∩ (𝐵(,)+∞))((𝑧 ≠ 𝐵 ∧ (abs‘(𝑧 − 𝐵)) < 𝑏) → (abs‘(((𝐹 ↾ (𝐵(,)+∞))‘𝑧) − 𝐿)) < 𝑥)) ∧ 𝑧 ∈ 𝐴 ∧ (𝑧 ≠ 𝐵 ∧ (abs‘(𝑧 − 𝐵)) < if(𝑎 ≤ 𝑏, 𝑎, 𝑏))) ∧ 𝑧 < 𝐵) → (abs‘(𝑧 − 𝐵)) < if(𝑎 ≤ 𝑏, 𝑎, 𝑏))
47		simpl1 1189	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑎 ∈ ℝ⁺ ∧ 𝑏 ∈ ℝ⁺) ∧ ((abs‘(𝑧 − 𝐵)) < if(𝑎 ≤ 𝑏, 𝑎, 𝑏) ∧ 𝑧 ∈ 𝐴)) → 𝜑)
48		simprr 773	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑎 ∈ ℝ⁺ ∧ 𝑏 ∈ ℝ⁺) ∧ ((abs‘(𝑧 − 𝐵)) < if(𝑎 ≤ 𝑏, 𝑎, 𝑏) ∧ 𝑧 ∈ 𝐴)) → 𝑧 ∈ 𝐴)
49	26	recnd 10708	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝐴) → 𝑧 ∈ ℂ)
50	22	recnd 10708	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → 𝐵 ∈ ℂ)
51	50	adantr 485	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝐴) → 𝐵 ∈ ℂ)
52	49, 51	subcld 11036	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝐴) → (𝑧 − 𝐵) ∈ ℂ)
53	52	abscld 14845	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝐴) → (abs‘(𝑧 − 𝐵)) ∈ ℝ)
54	47, 48, 53	syl2anc 588	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑎 ∈ ℝ⁺ ∧ 𝑏 ∈ ℝ⁺) ∧ ((abs‘(𝑧 − 𝐵)) < if(𝑎 ≤ 𝑏, 𝑎, 𝑏) ∧ 𝑧 ∈ 𝐴)) → (abs‘(𝑧 − 𝐵)) ∈ ℝ)
55		rpre 12439	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑎 ∈ ℝ⁺ → 𝑎 ∈ ℝ)
56	55	adantr 485	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑎 ∈ ℝ⁺ ∧ 𝑏 ∈ ℝ⁺) → 𝑎 ∈ ℝ)
57		rpre 12439	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑏 ∈ ℝ⁺ → 𝑏 ∈ ℝ)
58	57	adantl 486	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑎 ∈ ℝ⁺ ∧ 𝑏 ∈ ℝ⁺) → 𝑏 ∈ ℝ)
59	56, 58	ifcld 4467	. . . . . . . . . . . . . . . 16 ⊢ ((𝑎 ∈ ℝ⁺ ∧ 𝑏 ∈ ℝ⁺) → if(𝑎 ≤ 𝑏, 𝑎, 𝑏) ∈ ℝ)
60	59	3adant1 1128	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑎 ∈ ℝ⁺ ∧ 𝑏 ∈ ℝ⁺) → if(𝑎 ≤ 𝑏, 𝑎, 𝑏) ∈ ℝ)
61	60	adantr 485	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑎 ∈ ℝ⁺ ∧ 𝑏 ∈ ℝ⁺) ∧ ((abs‘(𝑧 − 𝐵)) < if(𝑎 ≤ 𝑏, 𝑎, 𝑏) ∧ 𝑧 ∈ 𝐴)) → if(𝑎 ≤ 𝑏, 𝑎, 𝑏) ∈ ℝ)
62	56	3adant1 1128	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑎 ∈ ℝ⁺ ∧ 𝑏 ∈ ℝ⁺) → 𝑎 ∈ ℝ)
63	62	adantr 485	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑎 ∈ ℝ⁺ ∧ 𝑏 ∈ ℝ⁺) ∧ ((abs‘(𝑧 − 𝐵)) < if(𝑎 ≤ 𝑏, 𝑎, 𝑏) ∧ 𝑧 ∈ 𝐴)) → 𝑎 ∈ ℝ)
64		simprl 771	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑎 ∈ ℝ⁺ ∧ 𝑏 ∈ ℝ⁺) ∧ ((abs‘(𝑧 − 𝐵)) < if(𝑎 ≤ 𝑏, 𝑎, 𝑏) ∧ 𝑧 ∈ 𝐴)) → (abs‘(𝑧 − 𝐵)) < if(𝑎 ≤ 𝑏, 𝑎, 𝑏))
65	58	3adant1 1128	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑎 ∈ ℝ⁺ ∧ 𝑏 ∈ ℝ⁺) → 𝑏 ∈ ℝ)
66		min1 12624	. . . . . . . . . . . . . . . 16 ⊢ ((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) → if(𝑎 ≤ 𝑏, 𝑎, 𝑏) ≤ 𝑎)
67	62, 65, 66	syl2anc 588	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑎 ∈ ℝ⁺ ∧ 𝑏 ∈ ℝ⁺) → if(𝑎 ≤ 𝑏, 𝑎, 𝑏) ≤ 𝑎)
68	67	adantr 485	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑎 ∈ ℝ⁺ ∧ 𝑏 ∈ ℝ⁺) ∧ ((abs‘(𝑧 − 𝐵)) < if(𝑎 ≤ 𝑏, 𝑎, 𝑏) ∧ 𝑧 ∈ 𝐴)) → if(𝑎 ≤ 𝑏, 𝑎, 𝑏) ≤ 𝑎)
69	54, 61, 63, 64, 68	ltletrd 10839	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑎 ∈ ℝ⁺ ∧ 𝑏 ∈ ℝ⁺) ∧ ((abs‘(𝑧 − 𝐵)) < if(𝑎 ≤ 𝑏, 𝑎, 𝑏) ∧ 𝑧 ∈ 𝐴)) → (abs‘(𝑧 − 𝐵)) < 𝑎)
70	17, 43, 45, 46, 18, 69	syl32anc 1376	. . . . . . . . . . . 12 ⊢ ((((((((𝜑 ∧ 𝑥 ∈ ℝ⁺) ∧ 𝑎 ∈ ℝ⁺) ∧ ∀𝑧 ∈ (𝐴 ∩ (-∞(,)𝐵))((𝑧 ≠ 𝐵 ∧ (abs‘(𝑧 − 𝐵)) < 𝑎) → (abs‘(((𝐹 ↾ (-∞(,)𝐵))‘𝑧) − 𝐿)) < 𝑥)) ∧ 𝑏 ∈ ℝ⁺) ∧ ∀𝑧 ∈ (𝐴 ∩ (𝐵(,)+∞))((𝑧 ≠ 𝐵 ∧ (abs‘(𝑧 − 𝐵)) < 𝑏) → (abs‘(((𝐹 ↾ (𝐵(,)+∞))‘𝑧) − 𝐿)) < 𝑥)) ∧ 𝑧 ∈ 𝐴 ∧ (𝑧 ≠ 𝐵 ∧ (abs‘(𝑧 − 𝐵)) < if(𝑎 ≤ 𝑏, 𝑎, 𝑏))) ∧ 𝑧 < 𝐵) → (abs‘(𝑧 − 𝐵)) < 𝑎)
71	41, 70	jca 516	. . . . . . . . . . 11 ⊢ ((((((((𝜑 ∧ 𝑥 ∈ ℝ⁺) ∧ 𝑎 ∈ ℝ⁺) ∧ ∀𝑧 ∈ (𝐴 ∩ (-∞(,)𝐵))((𝑧 ≠ 𝐵 ∧ (abs‘(𝑧 − 𝐵)) < 𝑎) → (abs‘(((𝐹 ↾ (-∞(,)𝐵))‘𝑧) − 𝐿)) < 𝑥)) ∧ 𝑏 ∈ ℝ⁺) ∧ ∀𝑧 ∈ (𝐴 ∩ (𝐵(,)+∞))((𝑧 ≠ 𝐵 ∧ (abs‘(𝑧 − 𝐵)) < 𝑏) → (abs‘(((𝐹 ↾ (𝐵(,)+∞))‘𝑧) − 𝐿)) < 𝑥)) ∧ 𝑧 ∈ 𝐴 ∧ (𝑧 ≠ 𝐵 ∧ (abs‘(𝑧 − 𝐵)) < if(𝑎 ≤ 𝑏, 𝑎, 𝑏))) ∧ 𝑧 < 𝐵) → (𝑧 ≠ 𝐵 ∧ (abs‘(𝑧 − 𝐵)) < 𝑎))
72		rspa 3136	. . . . . . . . . . 11 ⊢ ((∀𝑧 ∈ (𝐴 ∩ (-∞(,)𝐵))((𝑧 ≠ 𝐵 ∧ (abs‘(𝑧 − 𝐵)) < 𝑎) → (abs‘(((𝐹 ↾ (-∞(,)𝐵))‘𝑧) − 𝐿)) < 𝑥) ∧ 𝑧 ∈ (𝐴 ∩ (-∞(,)𝐵))) → ((𝑧 ≠ 𝐵 ∧ (abs‘(𝑧 − 𝐵)) < 𝑎) → (abs‘(((𝐹 ↾ (-∞(,)𝐵))‘𝑧) − 𝐿)) < 𝑥))
73	40, 71, 72	sylc 65	. . . . . . . . . 10 ⊢ ((((((((𝜑 ∧ 𝑥 ∈ ℝ⁺) ∧ 𝑎 ∈ ℝ⁺) ∧ ∀𝑧 ∈ (𝐴 ∩ (-∞(,)𝐵))((𝑧 ≠ 𝐵 ∧ (abs‘(𝑧 − 𝐵)) < 𝑎) → (abs‘(((𝐹 ↾ (-∞(,)𝐵))‘𝑧) − 𝐿)) < 𝑥)) ∧ 𝑏 ∈ ℝ⁺) ∧ ∀𝑧 ∈ (𝐴 ∩ (𝐵(,)+∞))((𝑧 ≠ 𝐵 ∧ (abs‘(𝑧 − 𝐵)) < 𝑏) → (abs‘(((𝐹 ↾ (𝐵(,)+∞))‘𝑧) − 𝐿)) < 𝑥)) ∧ 𝑧 ∈ 𝐴 ∧ (𝑧 ≠ 𝐵 ∧ (abs‘(𝑧 − 𝐵)) < if(𝑎 ≤ 𝑏, 𝑎, 𝑏))) ∧ 𝑧 < 𝐵) → (abs‘(((𝐹 ↾ (-∞(,)𝐵))‘𝑧) − 𝐿)) < 𝑥)
74	36, 73	eqbrtrd 5055	. . . . . . . . 9 ⊢ ((((((((𝜑 ∧ 𝑥 ∈ ℝ⁺) ∧ 𝑎 ∈ ℝ⁺) ∧ ∀𝑧 ∈ (𝐴 ∩ (-∞(,)𝐵))((𝑧 ≠ 𝐵 ∧ (abs‘(𝑧 − 𝐵)) < 𝑎) → (abs‘(((𝐹 ↾ (-∞(,)𝐵))‘𝑧) − 𝐿)) < 𝑥)) ∧ 𝑏 ∈ ℝ⁺) ∧ ∀𝑧 ∈ (𝐴 ∩ (𝐵(,)+∞))((𝑧 ≠ 𝐵 ∧ (abs‘(𝑧 − 𝐵)) < 𝑏) → (abs‘(((𝐹 ↾ (𝐵(,)+∞))‘𝑧) − 𝐿)) < 𝑥)) ∧ 𝑧 ∈ 𝐴 ∧ (𝑧 ≠ 𝐵 ∧ (abs‘(𝑧 − 𝐵)) < if(𝑎 ≤ 𝑏, 𝑎, 𝑏))) ∧ 𝑧 < 𝐵) → (abs‘((𝐹‘𝑧) − 𝐿)) < 𝑥)
75		simp-6l 787	. . . . . . . . . . . . 13 ⊢ (((((((𝜑 ∧ 𝑥 ∈ ℝ⁺) ∧ 𝑎 ∈ ℝ⁺) ∧ ∀𝑧 ∈ (𝐴 ∩ (-∞(,)𝐵))((𝑧 ≠ 𝐵 ∧ (abs‘(𝑧 − 𝐵)) < 𝑎) → (abs‘(((𝐹 ↾ (-∞(,)𝐵))‘𝑧) − 𝐿)) < 𝑥)) ∧ 𝑏 ∈ ℝ⁺) ∧ ∀𝑧 ∈ (𝐴 ∩ (𝐵(,)+∞))((𝑧 ≠ 𝐵 ∧ (abs‘(𝑧 − 𝐵)) < 𝑏) → (abs‘(((𝐹 ↾ (𝐵(,)+∞))‘𝑧) − 𝐿)) < 𝑥)) ∧ ¬ 𝑧 < 𝐵) → 𝜑)
76	75	3ad2antl1 1183	. . . . . . . . . . . 12 ⊢ ((((((((𝜑 ∧ 𝑥 ∈ ℝ⁺) ∧ 𝑎 ∈ ℝ⁺) ∧ ∀𝑧 ∈ (𝐴 ∩ (-∞(,)𝐵))((𝑧 ≠ 𝐵 ∧ (abs‘(𝑧 − 𝐵)) < 𝑎) → (abs‘(((𝐹 ↾ (-∞(,)𝐵))‘𝑧) − 𝐿)) < 𝑥)) ∧ 𝑏 ∈ ℝ⁺) ∧ ∀𝑧 ∈ (𝐴 ∩ (𝐵(,)+∞))((𝑧 ≠ 𝐵 ∧ (abs‘(𝑧 − 𝐵)) < 𝑏) → (abs‘(((𝐹 ↾ (𝐵(,)+∞))‘𝑧) − 𝐿)) < 𝑥)) ∧ 𝑧 ∈ 𝐴 ∧ (𝑧 ≠ 𝐵 ∧ (abs‘(𝑧 − 𝐵)) < if(𝑎 ≤ 𝑏, 𝑎, 𝑏))) ∧ ¬ 𝑧 < 𝐵) → 𝜑)
77	76, 22	syl 17	. . . . . . . . . . 11 ⊢ ((((((((𝜑 ∧ 𝑥 ∈ ℝ⁺) ∧ 𝑎 ∈ ℝ⁺) ∧ ∀𝑧 ∈ (𝐴 ∩ (-∞(,)𝐵))((𝑧 ≠ 𝐵 ∧ (abs‘(𝑧 − 𝐵)) < 𝑎) → (abs‘(((𝐹 ↾ (-∞(,)𝐵))‘𝑧) − 𝐿)) < 𝑥)) ∧ 𝑏 ∈ ℝ⁺) ∧ ∀𝑧 ∈ (𝐴 ∩ (𝐵(,)+∞))((𝑧 ≠ 𝐵 ∧ (abs‘(𝑧 − 𝐵)) < 𝑏) → (abs‘(((𝐹 ↾ (𝐵(,)+∞))‘𝑧) − 𝐿)) < 𝑥)) ∧ 𝑧 ∈ 𝐴 ∧ (𝑧 ≠ 𝐵 ∧ (abs‘(𝑧 − 𝐵)) < if(𝑎 ≤ 𝑏, 𝑎, 𝑏))) ∧ ¬ 𝑧 < 𝐵) → 𝐵 ∈ ℝ)
78		simpl2 1190	. . . . . . . . . . . 12 ⊢ ((((((((𝜑 ∧ 𝑥 ∈ ℝ⁺) ∧ 𝑎 ∈ ℝ⁺) ∧ ∀𝑧 ∈ (𝐴 ∩ (-∞(,)𝐵))((𝑧 ≠ 𝐵 ∧ (abs‘(𝑧 − 𝐵)) < 𝑎) → (abs‘(((𝐹 ↾ (-∞(,)𝐵))‘𝑧) − 𝐿)) < 𝑥)) ∧ 𝑏 ∈ ℝ⁺) ∧ ∀𝑧 ∈ (𝐴 ∩ (𝐵(,)+∞))((𝑧 ≠ 𝐵 ∧ (abs‘(𝑧 − 𝐵)) < 𝑏) → (abs‘(((𝐹 ↾ (𝐵(,)+∞))‘𝑧) − 𝐿)) < 𝑥)) ∧ 𝑧 ∈ 𝐴 ∧ (𝑧 ≠ 𝐵 ∧ (abs‘(𝑧 − 𝐵)) < if(𝑎 ≤ 𝑏, 𝑎, 𝑏))) ∧ ¬ 𝑧 < 𝐵) → 𝑧 ∈ 𝐴)
79	76, 78, 26	syl2anc 588	. . . . . . . . . . 11 ⊢ ((((((((𝜑 ∧ 𝑥 ∈ ℝ⁺) ∧ 𝑎 ∈ ℝ⁺) ∧ ∀𝑧 ∈ (𝐴 ∩ (-∞(,)𝐵))((𝑧 ≠ 𝐵 ∧ (abs‘(𝑧 − 𝐵)) < 𝑎) → (abs‘(((𝐹 ↾ (-∞(,)𝐵))‘𝑧) − 𝐿)) < 𝑥)) ∧ 𝑏 ∈ ℝ⁺) ∧ ∀𝑧 ∈ (𝐴 ∩ (𝐵(,)+∞))((𝑧 ≠ 𝐵 ∧ (abs‘(𝑧 − 𝐵)) < 𝑏) → (abs‘(((𝐹 ↾ (𝐵(,)+∞))‘𝑧) − 𝐿)) < 𝑥)) ∧ 𝑧 ∈ 𝐴 ∧ (𝑧 ≠ 𝐵 ∧ (abs‘(𝑧 − 𝐵)) < if(𝑎 ≤ 𝑏, 𝑎, 𝑏))) ∧ ¬ 𝑧 < 𝐵) → 𝑧 ∈ ℝ)
80		id 22	. . . . . . . . . . . . . 14 ⊢ (𝑧 ≠ 𝐵 → 𝑧 ≠ 𝐵)
81	80	necomd 3007	. . . . . . . . . . . . 13 ⊢ (𝑧 ≠ 𝐵 → 𝐵 ≠ 𝑧)
82	81	ad2antrr 726	. . . . . . . . . . . 12 ⊢ (((𝑧 ≠ 𝐵 ∧ (abs‘(𝑧 − 𝐵)) < if(𝑎 ≤ 𝑏, 𝑎, 𝑏)) ∧ ¬ 𝑧 < 𝐵) → 𝐵 ≠ 𝑧)
83	82	3ad2antl3 1185	. . . . . . . . . . 11 ⊢ ((((((((𝜑 ∧ 𝑥 ∈ ℝ⁺) ∧ 𝑎 ∈ ℝ⁺) ∧ ∀𝑧 ∈ (𝐴 ∩ (-∞(,)𝐵))((𝑧 ≠ 𝐵 ∧ (abs‘(𝑧 − 𝐵)) < 𝑎) → (abs‘(((𝐹 ↾ (-∞(,)𝐵))‘𝑧) − 𝐿)) < 𝑥)) ∧ 𝑏 ∈ ℝ⁺) ∧ ∀𝑧 ∈ (𝐴 ∩ (𝐵(,)+∞))((𝑧 ≠ 𝐵 ∧ (abs‘(𝑧 − 𝐵)) < 𝑏) → (abs‘(((𝐹 ↾ (𝐵(,)+∞))‘𝑧) − 𝐿)) < 𝑥)) ∧ 𝑧 ∈ 𝐴 ∧ (𝑧 ≠ 𝐵 ∧ (abs‘(𝑧 − 𝐵)) < if(𝑎 ≤ 𝑏, 𝑎, 𝑏))) ∧ ¬ 𝑧 < 𝐵) → 𝐵 ≠ 𝑧)
84		simpr 489	. . . . . . . . . . 11 ⊢ ((((((((𝜑 ∧ 𝑥 ∈ ℝ⁺) ∧ 𝑎 ∈ ℝ⁺) ∧ ∀𝑧 ∈ (𝐴 ∩ (-∞(,)𝐵))((𝑧 ≠ 𝐵 ∧ (abs‘(𝑧 − 𝐵)) < 𝑎) → (abs‘(((𝐹 ↾ (-∞(,)𝐵))‘𝑧) − 𝐿)) < 𝑥)) ∧ 𝑏 ∈ ℝ⁺) ∧ ∀𝑧 ∈ (𝐴 ∩ (𝐵(,)+∞))((𝑧 ≠ 𝐵 ∧ (abs‘(𝑧 − 𝐵)) < 𝑏) → (abs‘(((𝐹 ↾ (𝐵(,)+∞))‘𝑧) − 𝐿)) < 𝑥)) ∧ 𝑧 ∈ 𝐴 ∧ (𝑧 ≠ 𝐵 ∧ (abs‘(𝑧 − 𝐵)) < if(𝑎 ≤ 𝑏, 𝑎, 𝑏))) ∧ ¬ 𝑧 < 𝐵) → ¬ 𝑧 < 𝐵)
85	77, 79, 83, 84	lttri5d 42300	. . . . . . . . . 10 ⊢ ((((((((𝜑 ∧ 𝑥 ∈ ℝ⁺) ∧ 𝑎 ∈ ℝ⁺) ∧ ∀𝑧 ∈ (𝐴 ∩ (-∞(,)𝐵))((𝑧 ≠ 𝐵 ∧ (abs‘(𝑧 − 𝐵)) < 𝑎) → (abs‘(((𝐹 ↾ (-∞(,)𝐵))‘𝑧) − 𝐿)) < 𝑥)) ∧ 𝑏 ∈ ℝ⁺) ∧ ∀𝑧 ∈ (𝐴 ∩ (𝐵(,)+∞))((𝑧 ≠ 𝐵 ∧ (abs‘(𝑧 − 𝐵)) < 𝑏) → (abs‘(((𝐹 ↾ (𝐵(,)+∞))‘𝑧) − 𝐿)) < 𝑥)) ∧ 𝑧 ∈ 𝐴 ∧ (𝑧 ≠ 𝐵 ∧ (abs‘(𝑧 − 𝐵)) < if(𝑎 ≤ 𝑏, 𝑎, 𝑏))) ∧ ¬ 𝑧 < 𝐵) → 𝐵 < 𝑧)
86		simp-6l 787	. . . . . . . . . . . . . 14 ⊢ (((((((𝜑 ∧ 𝑥 ∈ ℝ⁺) ∧ 𝑎 ∈ ℝ⁺) ∧ ∀𝑧 ∈ (𝐴 ∩ (-∞(,)𝐵))((𝑧 ≠ 𝐵 ∧ (abs‘(𝑧 − 𝐵)) < 𝑎) → (abs‘(((𝐹 ↾ (-∞(,)𝐵))‘𝑧) − 𝐿)) < 𝑥)) ∧ 𝑏 ∈ ℝ⁺) ∧ ∀𝑧 ∈ (𝐴 ∩ (𝐵(,)+∞))((𝑧 ≠ 𝐵 ∧ (abs‘(𝑧 − 𝐵)) < 𝑏) → (abs‘(((𝐹 ↾ (𝐵(,)+∞))‘𝑧) − 𝐿)) < 𝑥)) ∧ 𝐵 < 𝑧) → 𝜑)
87	86	3ad2antl1 1183	. . . . . . . . . . . . 13 ⊢ ((((((((𝜑 ∧ 𝑥 ∈ ℝ⁺) ∧ 𝑎 ∈ ℝ⁺) ∧ ∀𝑧 ∈ (𝐴 ∩ (-∞(,)𝐵))((𝑧 ≠ 𝐵 ∧ (abs‘(𝑧 − 𝐵)) < 𝑎) → (abs‘(((𝐹 ↾ (-∞(,)𝐵))‘𝑧) − 𝐿)) < 𝑥)) ∧ 𝑏 ∈ ℝ⁺) ∧ ∀𝑧 ∈ (𝐴 ∩ (𝐵(,)+∞))((𝑧 ≠ 𝐵 ∧ (abs‘(𝑧 − 𝐵)) < 𝑏) → (abs‘(((𝐹 ↾ (𝐵(,)+∞))‘𝑧) − 𝐿)) < 𝑥)) ∧ 𝑧 ∈ 𝐴 ∧ (𝑧 ≠ 𝐵 ∧ (abs‘(𝑧 − 𝐵)) < if(𝑎 ≤ 𝑏, 𝑎, 𝑏))) ∧ 𝐵 < 𝑧) → 𝜑)
88		simpl2 1190	. . . . . . . . . . . . 13 ⊢ ((((((((𝜑 ∧ 𝑥 ∈ ℝ⁺) ∧ 𝑎 ∈ ℝ⁺) ∧ ∀𝑧 ∈ (𝐴 ∩ (-∞(,)𝐵))((𝑧 ≠ 𝐵 ∧ (abs‘(𝑧 − 𝐵)) < 𝑎) → (abs‘(((𝐹 ↾ (-∞(,)𝐵))‘𝑧) − 𝐿)) < 𝑥)) ∧ 𝑏 ∈ ℝ⁺) ∧ ∀𝑧 ∈ (𝐴 ∩ (𝐵(,)+∞))((𝑧 ≠ 𝐵 ∧ (abs‘(𝑧 − 𝐵)) < 𝑏) → (abs‘(((𝐹 ↾ (𝐵(,)+∞))‘𝑧) − 𝐿)) < 𝑥)) ∧ 𝑧 ∈ 𝐴 ∧ (𝑧 ≠ 𝐵 ∧ (abs‘(𝑧 − 𝐵)) < if(𝑎 ≤ 𝑏, 𝑎, 𝑏))) ∧ 𝐵 < 𝑧) → 𝑧 ∈ 𝐴)
89		simpr 489	. . . . . . . . . . . . 13 ⊢ ((((((((𝜑 ∧ 𝑥 ∈ ℝ⁺) ∧ 𝑎 ∈ ℝ⁺) ∧ ∀𝑧 ∈ (𝐴 ∩ (-∞(,)𝐵))((𝑧 ≠ 𝐵 ∧ (abs‘(𝑧 − 𝐵)) < 𝑎) → (abs‘(((𝐹 ↾ (-∞(,)𝐵))‘𝑧) − 𝐿)) < 𝑥)) ∧ 𝑏 ∈ ℝ⁺) ∧ ∀𝑧 ∈ (𝐴 ∩ (𝐵(,)+∞))((𝑧 ≠ 𝐵 ∧ (abs‘(𝑧 − 𝐵)) < 𝑏) → (abs‘(((𝐹 ↾ (𝐵(,)+∞))‘𝑧) − 𝐿)) < 𝑥)) ∧ 𝑧 ∈ 𝐴 ∧ (𝑧 ≠ 𝐵 ∧ (abs‘(𝑧 − 𝐵)) < if(𝑎 ≤ 𝑏, 𝑎, 𝑏))) ∧ 𝐵 < 𝑧) → 𝐵 < 𝑧)
90	23	3ad2ant1 1131	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝐴 ∧ 𝐵 < 𝑧) → 𝐵 ∈ ℝ^*)
91		pnfxr 10734	. . . . . . . . . . . . . . 15 ⊢ +∞ ∈ ℝ^*
92	91	a1i 11	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝐴 ∧ 𝐵 < 𝑧) → +∞ ∈ ℝ^*)
93	26	3adant3 1130	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝐴 ∧ 𝐵 < 𝑧) → 𝑧 ∈ ℝ)
94		simp3 1136	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝐴 ∧ 𝐵 < 𝑧) → 𝐵 < 𝑧)
95	93	ltpnfd 12558	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝐴 ∧ 𝐵 < 𝑧) → 𝑧 < +∞)
96	90, 92, 93, 94, 95	eliood 42502	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝐴 ∧ 𝐵 < 𝑧) → 𝑧 ∈ (𝐵(,)+∞))
97	87, 88, 89, 96	syl3anc 1369	. . . . . . . . . . . 12 ⊢ ((((((((𝜑 ∧ 𝑥 ∈ ℝ⁺) ∧ 𝑎 ∈ ℝ⁺) ∧ ∀𝑧 ∈ (𝐴 ∩ (-∞(,)𝐵))((𝑧 ≠ 𝐵 ∧ (abs‘(𝑧 − 𝐵)) < 𝑎) → (abs‘(((𝐹 ↾ (-∞(,)𝐵))‘𝑧) − 𝐿)) < 𝑥)) ∧ 𝑏 ∈ ℝ⁺) ∧ ∀𝑧 ∈ (𝐴 ∩ (𝐵(,)+∞))((𝑧 ≠ 𝐵 ∧ (abs‘(𝑧 − 𝐵)) < 𝑏) → (abs‘(((𝐹 ↾ (𝐵(,)+∞))‘𝑧) − 𝐿)) < 𝑥)) ∧ 𝑧 ∈ 𝐴 ∧ (𝑧 ≠ 𝐵 ∧ (abs‘(𝑧 − 𝐵)) < if(𝑎 ≤ 𝑏, 𝑎, 𝑏))) ∧ 𝐵 < 𝑧) → 𝑧 ∈ (𝐵(,)+∞))
98		fvres 6678	. . . . . . . . . . . . . 14 ⊢ (𝑧 ∈ (𝐵(,)+∞) → ((𝐹 ↾ (𝐵(,)+∞))‘𝑧) = (𝐹‘𝑧))
99	98	eqcomd 2765	. . . . . . . . . . . . 13 ⊢ (𝑧 ∈ (𝐵(,)+∞) → (𝐹‘𝑧) = ((𝐹 ↾ (𝐵(,)+∞))‘𝑧))
100	99	fvoveq1d 7173	. . . . . . . . . . . 12 ⊢ (𝑧 ∈ (𝐵(,)+∞) → (abs‘((𝐹‘𝑧) − 𝐿)) = (abs‘(((𝐹 ↾ (𝐵(,)+∞))‘𝑧) − 𝐿)))
101	97, 100	syl 17	. . . . . . . . . . 11 ⊢ ((((((((𝜑 ∧ 𝑥 ∈ ℝ⁺) ∧ 𝑎 ∈ ℝ⁺) ∧ ∀𝑧 ∈ (𝐴 ∩ (-∞(,)𝐵))((𝑧 ≠ 𝐵 ∧ (abs‘(𝑧 − 𝐵)) < 𝑎) → (abs‘(((𝐹 ↾ (-∞(,)𝐵))‘𝑧) − 𝐿)) < 𝑥)) ∧ 𝑏 ∈ ℝ⁺) ∧ ∀𝑧 ∈ (𝐴 ∩ (𝐵(,)+∞))((𝑧 ≠ 𝐵 ∧ (abs‘(𝑧 − 𝐵)) < 𝑏) → (abs‘(((𝐹 ↾ (𝐵(,)+∞))‘𝑧) − 𝐿)) < 𝑥)) ∧ 𝑧 ∈ 𝐴 ∧ (𝑧 ≠ 𝐵 ∧ (abs‘(𝑧 − 𝐵)) < if(𝑎 ≤ 𝑏, 𝑎, 𝑏))) ∧ 𝐵 < 𝑧) → (abs‘((𝐹‘𝑧) − 𝐿)) = (abs‘(((𝐹 ↾ (𝐵(,)+∞))‘𝑧) − 𝐿)))
102		simpl1r 1223	. . . . . . . . . . . . 13 ⊢ ((((((((𝜑 ∧ 𝑥 ∈ ℝ⁺) ∧ 𝑎 ∈ ℝ⁺) ∧ ∀𝑧 ∈ (𝐴 ∩ (-∞(,)𝐵))((𝑧 ≠ 𝐵 ∧ (abs‘(𝑧 − 𝐵)) < 𝑎) → (abs‘(((𝐹 ↾ (-∞(,)𝐵))‘𝑧) − 𝐿)) < 𝑥)) ∧ 𝑏 ∈ ℝ⁺) ∧ ∀𝑧 ∈ (𝐴 ∩ (𝐵(,)+∞))((𝑧 ≠ 𝐵 ∧ (abs‘(𝑧 − 𝐵)) < 𝑏) → (abs‘(((𝐹 ↾ (𝐵(,)+∞))‘𝑧) − 𝐿)) < 𝑥)) ∧ 𝑧 ∈ 𝐴 ∧ (𝑧 ≠ 𝐵 ∧ (abs‘(𝑧 − 𝐵)) < if(𝑎 ≤ 𝑏, 𝑎, 𝑏))) ∧ 𝐵 < 𝑧) → ∀𝑧 ∈ (𝐴 ∩ (𝐵(,)+∞))((𝑧 ≠ 𝐵 ∧ (abs‘(𝑧 − 𝐵)) < 𝑏) → (abs‘(((𝐹 ↾ (𝐵(,)+∞))‘𝑧) − 𝐿)) < 𝑥))
103	88, 97	elind 4100	. . . . . . . . . . . . 13 ⊢ ((((((((𝜑 ∧ 𝑥 ∈ ℝ⁺) ∧ 𝑎 ∈ ℝ⁺) ∧ ∀𝑧 ∈ (𝐴 ∩ (-∞(,)𝐵))((𝑧 ≠ 𝐵 ∧ (abs‘(𝑧 − 𝐵)) < 𝑎) → (abs‘(((𝐹 ↾ (-∞(,)𝐵))‘𝑧) − 𝐿)) < 𝑥)) ∧ 𝑏 ∈ ℝ⁺) ∧ ∀𝑧 ∈ (𝐴 ∩ (𝐵(,)+∞))((𝑧 ≠ 𝐵 ∧ (abs‘(𝑧 − 𝐵)) < 𝑏) → (abs‘(((𝐹 ↾ (𝐵(,)+∞))‘𝑧) − 𝐿)) < 𝑥)) ∧ 𝑧 ∈ 𝐴 ∧ (𝑧 ≠ 𝐵 ∧ (abs‘(𝑧 − 𝐵)) < if(𝑎 ≤ 𝑏, 𝑎, 𝑏))) ∧ 𝐵 < 𝑧) → 𝑧 ∈ (𝐴 ∩ (𝐵(,)+∞)))
104	102, 103	jca 516	. . . . . . . . . . . 12 ⊢ ((((((((𝜑 ∧ 𝑥 ∈ ℝ⁺) ∧ 𝑎 ∈ ℝ⁺) ∧ ∀𝑧 ∈ (𝐴 ∩ (-∞(,)𝐵))((𝑧 ≠ 𝐵 ∧ (abs‘(𝑧 − 𝐵)) < 𝑎) → (abs‘(((𝐹 ↾ (-∞(,)𝐵))‘𝑧) − 𝐿)) < 𝑥)) ∧ 𝑏 ∈ ℝ⁺) ∧ ∀𝑧 ∈ (𝐴 ∩ (𝐵(,)+∞))((𝑧 ≠ 𝐵 ∧ (abs‘(𝑧 − 𝐵)) < 𝑏) → (abs‘(((𝐹 ↾ (𝐵(,)+∞))‘𝑧) − 𝐿)) < 𝑥)) ∧ 𝑧 ∈ 𝐴 ∧ (𝑧 ≠ 𝐵 ∧ (abs‘(𝑧 − 𝐵)) < if(𝑎 ≤ 𝑏, 𝑎, 𝑏))) ∧ 𝐵 < 𝑧) → (∀𝑧 ∈ (𝐴 ∩ (𝐵(,)+∞))((𝑧 ≠ 𝐵 ∧ (abs‘(𝑧 − 𝐵)) < 𝑏) → (abs‘(((𝐹 ↾ (𝐵(,)+∞))‘𝑧) − 𝐿)) < 𝑥) ∧ 𝑧 ∈ (𝐴 ∩ (𝐵(,)+∞))))
105		simpl3l 1226	. . . . . . . . . . . . 13 ⊢ ((((((((𝜑 ∧ 𝑥 ∈ ℝ⁺) ∧ 𝑎 ∈ ℝ⁺) ∧ ∀𝑧 ∈ (𝐴 ∩ (-∞(,)𝐵))((𝑧 ≠ 𝐵 ∧ (abs‘(𝑧 − 𝐵)) < 𝑎) → (abs‘(((𝐹 ↾ (-∞(,)𝐵))‘𝑧) − 𝐿)) < 𝑥)) ∧ 𝑏 ∈ ℝ⁺) ∧ ∀𝑧 ∈ (𝐴 ∩ (𝐵(,)+∞))((𝑧 ≠ 𝐵 ∧ (abs‘(𝑧 − 𝐵)) < 𝑏) → (abs‘(((𝐹 ↾ (𝐵(,)+∞))‘𝑧) − 𝐿)) < 𝑥)) ∧ 𝑧 ∈ 𝐴 ∧ (𝑧 ≠ 𝐵 ∧ (abs‘(𝑧 − 𝐵)) < if(𝑎 ≤ 𝑏, 𝑎, 𝑏))) ∧ 𝐵 < 𝑧) → 𝑧 ≠ 𝐵)
106	4	adantr 485	. . . . . . . . . . . . . . 15 ⊢ (((((((𝜑 ∧ 𝑥 ∈ ℝ⁺) ∧ 𝑎 ∈ ℝ⁺) ∧ ∀𝑧 ∈ (𝐴 ∩ (-∞(,)𝐵))((𝑧 ≠ 𝐵 ∧ (abs‘(𝑧 − 𝐵)) < 𝑎) → (abs‘(((𝐹 ↾ (-∞(,)𝐵))‘𝑧) − 𝐿)) < 𝑥)) ∧ 𝑏 ∈ ℝ⁺) ∧ ∀𝑧 ∈ (𝐴 ∩ (𝐵(,)+∞))((𝑧 ≠ 𝐵 ∧ (abs‘(𝑧 − 𝐵)) < 𝑏) → (abs‘(((𝐹 ↾ (𝐵(,)+∞))‘𝑧) − 𝐿)) < 𝑥)) ∧ 𝐵 < 𝑧) → 𝑎 ∈ ℝ⁺)
107	106	3ad2antl1 1183	. . . . . . . . . . . . . 14 ⊢ ((((((((𝜑 ∧ 𝑥 ∈ ℝ⁺) ∧ 𝑎 ∈ ℝ⁺) ∧ ∀𝑧 ∈ (𝐴 ∩ (-∞(,)𝐵))((𝑧 ≠ 𝐵 ∧ (abs‘(𝑧 − 𝐵)) < 𝑎) → (abs‘(((𝐹 ↾ (-∞(,)𝐵))‘𝑧) − 𝐿)) < 𝑥)) ∧ 𝑏 ∈ ℝ⁺) ∧ ∀𝑧 ∈ (𝐴 ∩ (𝐵(,)+∞))((𝑧 ≠ 𝐵 ∧ (abs‘(𝑧 − 𝐵)) < 𝑏) → (abs‘(((𝐹 ↾ (𝐵(,)+∞))‘𝑧) − 𝐿)) < 𝑥)) ∧ 𝑧 ∈ 𝐴 ∧ (𝑧 ≠ 𝐵 ∧ (abs‘(𝑧 − 𝐵)) < if(𝑎 ≤ 𝑏, 𝑎, 𝑏))) ∧ 𝐵 < 𝑧) → 𝑎 ∈ ℝ⁺)
108	5	adantr 485	. . . . . . . . . . . . . . 15 ⊢ (((((((𝜑 ∧ 𝑥 ∈ ℝ⁺) ∧ 𝑎 ∈ ℝ⁺) ∧ ∀𝑧 ∈ (𝐴 ∩ (-∞(,)𝐵))((𝑧 ≠ 𝐵 ∧ (abs‘(𝑧 − 𝐵)) < 𝑎) → (abs‘(((𝐹 ↾ (-∞(,)𝐵))‘𝑧) − 𝐿)) < 𝑥)) ∧ 𝑏 ∈ ℝ⁺) ∧ ∀𝑧 ∈ (𝐴 ∩ (𝐵(,)+∞))((𝑧 ≠ 𝐵 ∧ (abs‘(𝑧 − 𝐵)) < 𝑏) → (abs‘(((𝐹 ↾ (𝐵(,)+∞))‘𝑧) − 𝐿)) < 𝑥)) ∧ 𝐵 < 𝑧) → 𝑏 ∈ ℝ⁺)
109	108	3ad2antl1 1183	. . . . . . . . . . . . . 14 ⊢ ((((((((𝜑 ∧ 𝑥 ∈ ℝ⁺) ∧ 𝑎 ∈ ℝ⁺) ∧ ∀𝑧 ∈ (𝐴 ∩ (-∞(,)𝐵))((𝑧 ≠ 𝐵 ∧ (abs‘(𝑧 − 𝐵)) < 𝑎) → (abs‘(((𝐹 ↾ (-∞(,)𝐵))‘𝑧) − 𝐿)) < 𝑥)) ∧ 𝑏 ∈ ℝ⁺) ∧ ∀𝑧 ∈ (𝐴 ∩ (𝐵(,)+∞))((𝑧 ≠ 𝐵 ∧ (abs‘(𝑧 − 𝐵)) < 𝑏) → (abs‘(((𝐹 ↾ (𝐵(,)+∞))‘𝑧) − 𝐿)) < 𝑥)) ∧ 𝑧 ∈ 𝐴 ∧ (𝑧 ≠ 𝐵 ∧ (abs‘(𝑧 − 𝐵)) < if(𝑎 ≤ 𝑏, 𝑎, 𝑏))) ∧ 𝐵 < 𝑧) → 𝑏 ∈ ℝ⁺)
110		simpl3r 1227	. . . . . . . . . . . . . 14 ⊢ ((((((((𝜑 ∧ 𝑥 ∈ ℝ⁺) ∧ 𝑎 ∈ ℝ⁺) ∧ ∀𝑧 ∈ (𝐴 ∩ (-∞(,)𝐵))((𝑧 ≠ 𝐵 ∧ (abs‘(𝑧 − 𝐵)) < 𝑎) → (abs‘(((𝐹 ↾ (-∞(,)𝐵))‘𝑧) − 𝐿)) < 𝑥)) ∧ 𝑏 ∈ ℝ⁺) ∧ ∀𝑧 ∈ (𝐴 ∩ (𝐵(,)+∞))((𝑧 ≠ 𝐵 ∧ (abs‘(𝑧 − 𝐵)) < 𝑏) → (abs‘(((𝐹 ↾ (𝐵(,)+∞))‘𝑧) − 𝐿)) < 𝑥)) ∧ 𝑧 ∈ 𝐴 ∧ (𝑧 ≠ 𝐵 ∧ (abs‘(𝑧 − 𝐵)) < if(𝑎 ≤ 𝑏, 𝑎, 𝑏))) ∧ 𝐵 < 𝑧) → (abs‘(𝑧 − 𝐵)) < if(𝑎 ≤ 𝑏, 𝑎, 𝑏))
111	65	adantr 485	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑎 ∈ ℝ⁺ ∧ 𝑏 ∈ ℝ⁺) ∧ ((abs‘(𝑧 − 𝐵)) < if(𝑎 ≤ 𝑏, 𝑎, 𝑏) ∧ 𝑧 ∈ 𝐴)) → 𝑏 ∈ ℝ)
112		min2 12625	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) → if(𝑎 ≤ 𝑏, 𝑎, 𝑏) ≤ 𝑏)
113	62, 65, 112	syl2anc 588	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑎 ∈ ℝ⁺ ∧ 𝑏 ∈ ℝ⁺) → if(𝑎 ≤ 𝑏, 𝑎, 𝑏) ≤ 𝑏)
114	113	adantr 485	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑎 ∈ ℝ⁺ ∧ 𝑏 ∈ ℝ⁺) ∧ ((abs‘(𝑧 − 𝐵)) < if(𝑎 ≤ 𝑏, 𝑎, 𝑏) ∧ 𝑧 ∈ 𝐴)) → if(𝑎 ≤ 𝑏, 𝑎, 𝑏) ≤ 𝑏)
115	54, 61, 111, 64, 114	ltletrd 10839	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑎 ∈ ℝ⁺ ∧ 𝑏 ∈ ℝ⁺) ∧ ((abs‘(𝑧 − 𝐵)) < if(𝑎 ≤ 𝑏, 𝑎, 𝑏) ∧ 𝑧 ∈ 𝐴)) → (abs‘(𝑧 − 𝐵)) < 𝑏)
116	87, 107, 109, 110, 88, 115	syl32anc 1376	. . . . . . . . . . . . 13 ⊢ ((((((((𝜑 ∧ 𝑥 ∈ ℝ⁺) ∧ 𝑎 ∈ ℝ⁺) ∧ ∀𝑧 ∈ (𝐴 ∩ (-∞(,)𝐵))((𝑧 ≠ 𝐵 ∧ (abs‘(𝑧 − 𝐵)) < 𝑎) → (abs‘(((𝐹 ↾ (-∞(,)𝐵))‘𝑧) − 𝐿)) < 𝑥)) ∧ 𝑏 ∈ ℝ⁺) ∧ ∀𝑧 ∈ (𝐴 ∩ (𝐵(,)+∞))((𝑧 ≠ 𝐵 ∧ (abs‘(𝑧 − 𝐵)) < 𝑏) → (abs‘(((𝐹 ↾ (𝐵(,)+∞))‘𝑧) − 𝐿)) < 𝑥)) ∧ 𝑧 ∈ 𝐴 ∧ (𝑧 ≠ 𝐵 ∧ (abs‘(𝑧 − 𝐵)) < if(𝑎 ≤ 𝑏, 𝑎, 𝑏))) ∧ 𝐵 < 𝑧) → (abs‘(𝑧 − 𝐵)) < 𝑏)
117	105, 116	jca 516	. . . . . . . . . . . 12 ⊢ ((((((((𝜑 ∧ 𝑥 ∈ ℝ⁺) ∧ 𝑎 ∈ ℝ⁺) ∧ ∀𝑧 ∈ (𝐴 ∩ (-∞(,)𝐵))((𝑧 ≠ 𝐵 ∧ (abs‘(𝑧 − 𝐵)) < 𝑎) → (abs‘(((𝐹 ↾ (-∞(,)𝐵))‘𝑧) − 𝐿)) < 𝑥)) ∧ 𝑏 ∈ ℝ⁺) ∧ ∀𝑧 ∈ (𝐴 ∩ (𝐵(,)+∞))((𝑧 ≠ 𝐵 ∧ (abs‘(𝑧 − 𝐵)) < 𝑏) → (abs‘(((𝐹 ↾ (𝐵(,)+∞))‘𝑧) − 𝐿)) < 𝑥)) ∧ 𝑧 ∈ 𝐴 ∧ (𝑧 ≠ 𝐵 ∧ (abs‘(𝑧 − 𝐵)) < if(𝑎 ≤ 𝑏, 𝑎, 𝑏))) ∧ 𝐵 < 𝑧) → (𝑧 ≠ 𝐵 ∧ (abs‘(𝑧 − 𝐵)) < 𝑏))
118		rspa 3136	. . . . . . . . . . . 12 ⊢ ((∀𝑧 ∈ (𝐴 ∩ (𝐵(,)+∞))((𝑧 ≠ 𝐵 ∧ (abs‘(𝑧 − 𝐵)) < 𝑏) → (abs‘(((𝐹 ↾ (𝐵(,)+∞))‘𝑧) − 𝐿)) < 𝑥) ∧ 𝑧 ∈ (𝐴 ∩ (𝐵(,)+∞))) → ((𝑧 ≠ 𝐵 ∧ (abs‘(𝑧 − 𝐵)) < 𝑏) → (abs‘(((𝐹 ↾ (𝐵(,)+∞))‘𝑧) − 𝐿)) < 𝑥))
119	104, 117, 118	sylc 65	. . . . . . . . . . 11 ⊢ ((((((((𝜑 ∧ 𝑥 ∈ ℝ⁺) ∧ 𝑎 ∈ ℝ⁺) ∧ ∀𝑧 ∈ (𝐴 ∩ (-∞(,)𝐵))((𝑧 ≠ 𝐵 ∧ (abs‘(𝑧 − 𝐵)) < 𝑎) → (abs‘(((𝐹 ↾ (-∞(,)𝐵))‘𝑧) − 𝐿)) < 𝑥)) ∧ 𝑏 ∈ ℝ⁺) ∧ ∀𝑧 ∈ (𝐴 ∩ (𝐵(,)+∞))((𝑧 ≠ 𝐵 ∧ (abs‘(𝑧 − 𝐵)) < 𝑏) → (abs‘(((𝐹 ↾ (𝐵(,)+∞))‘𝑧) − 𝐿)) < 𝑥)) ∧ 𝑧 ∈ 𝐴 ∧ (𝑧 ≠ 𝐵 ∧ (abs‘(𝑧 − 𝐵)) < if(𝑎 ≤ 𝑏, 𝑎, 𝑏))) ∧ 𝐵 < 𝑧) → (abs‘(((𝐹 ↾ (𝐵(,)+∞))‘𝑧) − 𝐿)) < 𝑥)
120	101, 119	eqbrtrd 5055	. . . . . . . . . 10 ⊢ ((((((((𝜑 ∧ 𝑥 ∈ ℝ⁺) ∧ 𝑎 ∈ ℝ⁺) ∧ ∀𝑧 ∈ (𝐴 ∩ (-∞(,)𝐵))((𝑧 ≠ 𝐵 ∧ (abs‘(𝑧 − 𝐵)) < 𝑎) → (abs‘(((𝐹 ↾ (-∞(,)𝐵))‘𝑧) − 𝐿)) < 𝑥)) ∧ 𝑏 ∈ ℝ⁺) ∧ ∀𝑧 ∈ (𝐴 ∩ (𝐵(,)+∞))((𝑧 ≠ 𝐵 ∧ (abs‘(𝑧 − 𝐵)) < 𝑏) → (abs‘(((𝐹 ↾ (𝐵(,)+∞))‘𝑧) − 𝐿)) < 𝑥)) ∧ 𝑧 ∈ 𝐴 ∧ (𝑧 ≠ 𝐵 ∧ (abs‘(𝑧 − 𝐵)) < if(𝑎 ≤ 𝑏, 𝑎, 𝑏))) ∧ 𝐵 < 𝑧) → (abs‘((𝐹‘𝑧) − 𝐿)) < 𝑥)
121	85, 120	syldan 595	. . . . . . . . 9 ⊢ ((((((((𝜑 ∧ 𝑥 ∈ ℝ⁺) ∧ 𝑎 ∈ ℝ⁺) ∧ ∀𝑧 ∈ (𝐴 ∩ (-∞(,)𝐵))((𝑧 ≠ 𝐵 ∧ (abs‘(𝑧 − 𝐵)) < 𝑎) → (abs‘(((𝐹 ↾ (-∞(,)𝐵))‘𝑧) − 𝐿)) < 𝑥)) ∧ 𝑏 ∈ ℝ⁺) ∧ ∀𝑧 ∈ (𝐴 ∩ (𝐵(,)+∞))((𝑧 ≠ 𝐵 ∧ (abs‘(𝑧 − 𝐵)) < 𝑏) → (abs‘(((𝐹 ↾ (𝐵(,)+∞))‘𝑧) − 𝐿)) < 𝑥)) ∧ 𝑧 ∈ 𝐴 ∧ (𝑧 ≠ 𝐵 ∧ (abs‘(𝑧 − 𝐵)) < if(𝑎 ≤ 𝑏, 𝑎, 𝑏))) ∧ ¬ 𝑧 < 𝐵) → (abs‘((𝐹‘𝑧) − 𝐿)) < 𝑥)
122	74, 121	pm2.61dan 813	. . . . . . . 8 ⊢ (((((((𝜑 ∧ 𝑥 ∈ ℝ⁺) ∧ 𝑎 ∈ ℝ⁺) ∧ ∀𝑧 ∈ (𝐴 ∩ (-∞(,)𝐵))((𝑧 ≠ 𝐵 ∧ (abs‘(𝑧 − 𝐵)) < 𝑎) → (abs‘(((𝐹 ↾ (-∞(,)𝐵))‘𝑧) − 𝐿)) < 𝑥)) ∧ 𝑏 ∈ ℝ⁺) ∧ ∀𝑧 ∈ (𝐴 ∩ (𝐵(,)+∞))((𝑧 ≠ 𝐵 ∧ (abs‘(𝑧 − 𝐵)) < 𝑏) → (abs‘(((𝐹 ↾ (𝐵(,)+∞))‘𝑧) − 𝐿)) < 𝑥)) ∧ 𝑧 ∈ 𝐴 ∧ (𝑧 ≠ 𝐵 ∧ (abs‘(𝑧 − 𝐵)) < if(𝑎 ≤ 𝑏, 𝑎, 𝑏))) → (abs‘((𝐹‘𝑧) − 𝐿)) < 𝑥)
123	122	3exp 1117	. . . . . . 7 ⊢ ((((((𝜑 ∧ 𝑥 ∈ ℝ⁺) ∧ 𝑎 ∈ ℝ⁺) ∧ ∀𝑧 ∈ (𝐴 ∩ (-∞(,)𝐵))((𝑧 ≠ 𝐵 ∧ (abs‘(𝑧 − 𝐵)) < 𝑎) → (abs‘(((𝐹 ↾ (-∞(,)𝐵))‘𝑧) − 𝐿)) < 𝑥)) ∧ 𝑏 ∈ ℝ⁺) ∧ ∀𝑧 ∈ (𝐴 ∩ (𝐵(,)+∞))((𝑧 ≠ 𝐵 ∧ (abs‘(𝑧 − 𝐵)) < 𝑏) → (abs‘(((𝐹 ↾ (𝐵(,)+∞))‘𝑧) − 𝐿)) < 𝑥)) → (𝑧 ∈ 𝐴 → ((𝑧 ≠ 𝐵 ∧ (abs‘(𝑧 − 𝐵)) < if(𝑎 ≤ 𝑏, 𝑎, 𝑏)) → (abs‘((𝐹‘𝑧) − 𝐿)) < 𝑥)))
124	15, 123	ralrimi 3145	. . . . . 6 ⊢ ((((((𝜑 ∧ 𝑥 ∈ ℝ⁺) ∧ 𝑎 ∈ ℝ⁺) ∧ ∀𝑧 ∈ (𝐴 ∩ (-∞(,)𝐵))((𝑧 ≠ 𝐵 ∧ (abs‘(𝑧 − 𝐵)) < 𝑎) → (abs‘(((𝐹 ↾ (-∞(,)𝐵))‘𝑧) − 𝐿)) < 𝑥)) ∧ 𝑏 ∈ ℝ⁺) ∧ ∀𝑧 ∈ (𝐴 ∩ (𝐵(,)+∞))((𝑧 ≠ 𝐵 ∧ (abs‘(𝑧 − 𝐵)) < 𝑏) → (abs‘(((𝐹 ↾ (𝐵(,)+∞))‘𝑧) − 𝐿)) < 𝑥)) → ∀𝑧 ∈ 𝐴 ((𝑧 ≠ 𝐵 ∧ (abs‘(𝑧 − 𝐵)) < if(𝑎 ≤ 𝑏, 𝑎, 𝑏)) → (abs‘((𝐹‘𝑧) − 𝐿)) < 𝑥))
125		brimralrspcev 5094	. . . . . 6 ⊢ ((if(𝑎 ≤ 𝑏, 𝑎, 𝑏) ∈ ℝ⁺ ∧ ∀𝑧 ∈ 𝐴 ((𝑧 ≠ 𝐵 ∧ (abs‘(𝑧 − 𝐵)) < if(𝑎 ≤ 𝑏, 𝑎, 𝑏)) → (abs‘((𝐹‘𝑧) − 𝐿)) < 𝑥)) → ∃𝑦 ∈ ℝ⁺ ∀𝑧 ∈ 𝐴 ((𝑧 ≠ 𝐵 ∧ (abs‘(𝑧 − 𝐵)) < 𝑦) → (abs‘((𝐹‘𝑧) − 𝐿)) < 𝑥))
126	6, 124, 125	syl2anc 588	. . . . 5 ⊢ ((((((𝜑 ∧ 𝑥 ∈ ℝ⁺) ∧ 𝑎 ∈ ℝ⁺) ∧ ∀𝑧 ∈ (𝐴 ∩ (-∞(,)𝐵))((𝑧 ≠ 𝐵 ∧ (abs‘(𝑧 − 𝐵)) < 𝑎) → (abs‘(((𝐹 ↾ (-∞(,)𝐵))‘𝑧) − 𝐿)) < 𝑥)) ∧ 𝑏 ∈ ℝ⁺) ∧ ∀𝑧 ∈ (𝐴 ∩ (𝐵(,)+∞))((𝑧 ≠ 𝐵 ∧ (abs‘(𝑧 − 𝐵)) < 𝑏) → (abs‘(((𝐹 ↾ (𝐵(,)+∞))‘𝑧) − 𝐿)) < 𝑥)) → ∃𝑦 ∈ ℝ⁺ ∀𝑧 ∈ 𝐴 ((𝑧 ≠ 𝐵 ∧ (abs‘(𝑧 − 𝐵)) < 𝑦) → (abs‘((𝐹‘𝑧) − 𝐿)) < 𝑥))
127		limcleqr.r	. . . . . . . . . 10 ⊢ (𝜑 → 𝑅 ∈ ((𝐹 ↾ (𝐵(,)+∞)) lim_ℂ 𝐵))
128		limcleqr.f	. . . . . . . . . . . 12 ⊢ (𝜑 → 𝐹:𝐴⟶ℂ)
129		fresin 6533	. . . . . . . . . . . 12 ⊢ (𝐹:𝐴⟶ℂ → (𝐹 ↾ (𝐵(,)+∞)):(𝐴 ∩ (𝐵(,)+∞))⟶ℂ)
130	128, 129	syl 17	. . . . . . . . . . 11 ⊢ (𝜑 → (𝐹 ↾ (𝐵(,)+∞)):(𝐴 ∩ (𝐵(,)+∞))⟶ℂ)
131		inss2 4135	. . . . . . . . . . . . 13 ⊢ (𝐴 ∩ (𝐵(,)+∞)) ⊆ (𝐵(,)+∞)
132		ioosscn 12842	. . . . . . . . . . . . 13 ⊢ (𝐵(,)+∞) ⊆ ℂ
133	131, 132	sstri 3902	. . . . . . . . . . . 12 ⊢ (𝐴 ∩ (𝐵(,)+∞)) ⊆ ℂ
134	133	a1i 11	. . . . . . . . . . 11 ⊢ (𝜑 → (𝐴 ∩ (𝐵(,)+∞)) ⊆ ℂ)
135	130, 134, 50	ellimc3 24579	. . . . . . . . . 10 ⊢ (𝜑 → (𝑅 ∈ ((𝐹 ↾ (𝐵(,)+∞)) lim_ℂ 𝐵) ↔ (𝑅 ∈ ℂ ∧ ∀𝑥 ∈ ℝ⁺ ∃𝑏 ∈ ℝ⁺ ∀𝑧 ∈ (𝐴 ∩ (𝐵(,)+∞))((𝑧 ≠ 𝐵 ∧ (abs‘(𝑧 − 𝐵)) < 𝑏) → (abs‘(((𝐹 ↾ (𝐵(,)+∞))‘𝑧) − 𝑅)) < 𝑥))))
136	127, 135	mpbid 235	. . . . . . . . 9 ⊢ (𝜑 → (𝑅 ∈ ℂ ∧ ∀𝑥 ∈ ℝ⁺ ∃𝑏 ∈ ℝ⁺ ∀𝑧 ∈ (𝐴 ∩ (𝐵(,)+∞))((𝑧 ≠ 𝐵 ∧ (abs‘(𝑧 − 𝐵)) < 𝑏) → (abs‘(((𝐹 ↾ (𝐵(,)+∞))‘𝑧) − 𝑅)) < 𝑥)))
137	136	simprd 500	. . . . . . . 8 ⊢ (𝜑 → ∀𝑥 ∈ ℝ⁺ ∃𝑏 ∈ ℝ⁺ ∀𝑧 ∈ (𝐴 ∩ (𝐵(,)+∞))((𝑧 ≠ 𝐵 ∧ (abs‘(𝑧 − 𝐵)) < 𝑏) → (abs‘(((𝐹 ↾ (𝐵(,)+∞))‘𝑧) − 𝑅)) < 𝑥))
138	137	r19.21bi 3138	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ⁺) → ∃𝑏 ∈ ℝ⁺ ∀𝑧 ∈ (𝐴 ∩ (𝐵(,)+∞))((𝑧 ≠ 𝐵 ∧ (abs‘(𝑧 − 𝐵)) < 𝑏) → (abs‘(((𝐹 ↾ (𝐵(,)+∞))‘𝑧) − 𝑅)) < 𝑥))
139		limcleqr.leqr	. . . . . . . . . . . . 13 ⊢ (𝜑 → 𝐿 = 𝑅)
140	139	oveq2d 7167	. . . . . . . . . . . 12 ⊢ (𝜑 → (((𝐹 ↾ (𝐵(,)+∞))‘𝑧) − 𝐿) = (((𝐹 ↾ (𝐵(,)+∞))‘𝑧) − 𝑅))
141	140	fveq2d 6663	. . . . . . . . . . 11 ⊢ (𝜑 → (abs‘(((𝐹 ↾ (𝐵(,)+∞))‘𝑧) − 𝐿)) = (abs‘(((𝐹 ↾ (𝐵(,)+∞))‘𝑧) − 𝑅)))
142	141	breq1d 5043	. . . . . . . . . 10 ⊢ (𝜑 → ((abs‘(((𝐹 ↾ (𝐵(,)+∞))‘𝑧) − 𝐿)) < 𝑥 ↔ (abs‘(((𝐹 ↾ (𝐵(,)+∞))‘𝑧) − 𝑅)) < 𝑥))
143	142	imbi2d 345	. . . . . . . . 9 ⊢ (𝜑 → (((𝑧 ≠ 𝐵 ∧ (abs‘(𝑧 − 𝐵)) < 𝑏) → (abs‘(((𝐹 ↾ (𝐵(,)+∞))‘𝑧) − 𝐿)) < 𝑥) ↔ ((𝑧 ≠ 𝐵 ∧ (abs‘(𝑧 − 𝐵)) < 𝑏) → (abs‘(((𝐹 ↾ (𝐵(,)+∞))‘𝑧) − 𝑅)) < 𝑥)))
144	143	rexralbidv 3226	. . . . . . . 8 ⊢ (𝜑 → (∃𝑏 ∈ ℝ⁺ ∀𝑧 ∈ (𝐴 ∩ (𝐵(,)+∞))((𝑧 ≠ 𝐵 ∧ (abs‘(𝑧 − 𝐵)) < 𝑏) → (abs‘(((𝐹 ↾ (𝐵(,)+∞))‘𝑧) − 𝐿)) < 𝑥) ↔ ∃𝑏 ∈ ℝ⁺ ∀𝑧 ∈ (𝐴 ∩ (𝐵(,)+∞))((𝑧 ≠ 𝐵 ∧ (abs‘(𝑧 − 𝐵)) < 𝑏) → (abs‘(((𝐹 ↾ (𝐵(,)+∞))‘𝑧) − 𝑅)) < 𝑥)))
145	144	adantr 485	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ⁺) → (∃𝑏 ∈ ℝ⁺ ∀𝑧 ∈ (𝐴 ∩ (𝐵(,)+∞))((𝑧 ≠ 𝐵 ∧ (abs‘(𝑧 − 𝐵)) < 𝑏) → (abs‘(((𝐹 ↾ (𝐵(,)+∞))‘𝑧) − 𝐿)) < 𝑥) ↔ ∃𝑏 ∈ ℝ⁺ ∀𝑧 ∈ (𝐴 ∩ (𝐵(,)+∞))((𝑧 ≠ 𝐵 ∧ (abs‘(𝑧 − 𝐵)) < 𝑏) → (abs‘(((𝐹 ↾ (𝐵(,)+∞))‘𝑧) − 𝑅)) < 𝑥)))
146	138, 145	mpbird 260	. . . . . 6 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ⁺) → ∃𝑏 ∈ ℝ⁺ ∀𝑧 ∈ (𝐴 ∩ (𝐵(,)+∞))((𝑧 ≠ 𝐵 ∧ (abs‘(𝑧 − 𝐵)) < 𝑏) → (abs‘(((𝐹 ↾ (𝐵(,)+∞))‘𝑧) − 𝐿)) < 𝑥))
147	146	ad2antrr 726	. . . . 5 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ⁺) ∧ 𝑎 ∈ ℝ⁺) ∧ ∀𝑧 ∈ (𝐴 ∩ (-∞(,)𝐵))((𝑧 ≠ 𝐵 ∧ (abs‘(𝑧 − 𝐵)) < 𝑎) → (abs‘(((𝐹 ↾ (-∞(,)𝐵))‘𝑧) − 𝐿)) < 𝑥)) → ∃𝑏 ∈ ℝ⁺ ∀𝑧 ∈ (𝐴 ∩ (𝐵(,)+∞))((𝑧 ≠ 𝐵 ∧ (abs‘(𝑧 − 𝐵)) < 𝑏) → (abs‘(((𝐹 ↾ (𝐵(,)+∞))‘𝑧) − 𝐿)) < 𝑥))
148	126, 147	r19.29a 3214	. . . 4 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ⁺) ∧ 𝑎 ∈ ℝ⁺) ∧ ∀𝑧 ∈ (𝐴 ∩ (-∞(,)𝐵))((𝑧 ≠ 𝐵 ∧ (abs‘(𝑧 − 𝐵)) < 𝑎) → (abs‘(((𝐹 ↾ (-∞(,)𝐵))‘𝑧) − 𝐿)) < 𝑥)) → ∃𝑦 ∈ ℝ⁺ ∀𝑧 ∈ 𝐴 ((𝑧 ≠ 𝐵 ∧ (abs‘(𝑧 − 𝐵)) < 𝑦) → (abs‘((𝐹‘𝑧) − 𝐿)) < 𝑥))
149		fresin 6533	. . . . . . . . 9 ⊢ (𝐹:𝐴⟶ℂ → (𝐹 ↾ (-∞(,)𝐵)):(𝐴 ∩ (-∞(,)𝐵))⟶ℂ)
150	128, 149	syl 17	. . . . . . . 8 ⊢ (𝜑 → (𝐹 ↾ (-∞(,)𝐵)):(𝐴 ∩ (-∞(,)𝐵))⟶ℂ)
151		inss2 4135	. . . . . . . . . 10 ⊢ (𝐴 ∩ (-∞(,)𝐵)) ⊆ (-∞(,)𝐵)
152		ioossre 12841	. . . . . . . . . 10 ⊢ (-∞(,)𝐵) ⊆ ℝ
153	151, 152	sstri 3902	. . . . . . . . 9 ⊢ (𝐴 ∩ (-∞(,)𝐵)) ⊆ ℝ
154		ax-resscn 10633	. . . . . . . . . 10 ⊢ ℝ ⊆ ℂ
155	154	a1i 11	. . . . . . . . 9 ⊢ (𝜑 → ℝ ⊆ ℂ)
156	153, 155	sstrid 3904	. . . . . . . 8 ⊢ (𝜑 → (𝐴 ∩ (-∞(,)𝐵)) ⊆ ℂ)
157	150, 156, 50	ellimc3 24579	. . . . . . 7 ⊢ (𝜑 → (𝐿 ∈ ((𝐹 ↾ (-∞(,)𝐵)) lim_ℂ 𝐵) ↔ (𝐿 ∈ ℂ ∧ ∀𝑥 ∈ ℝ⁺ ∃𝑎 ∈ ℝ⁺ ∀𝑧 ∈ (𝐴 ∩ (-∞(,)𝐵))((𝑧 ≠ 𝐵 ∧ (abs‘(𝑧 − 𝐵)) < 𝑎) → (abs‘(((𝐹 ↾ (-∞(,)𝐵))‘𝑧) − 𝐿)) < 𝑥))))
158	2, 157	mpbid 235	. . . . . 6 ⊢ (𝜑 → (𝐿 ∈ ℂ ∧ ∀𝑥 ∈ ℝ⁺ ∃𝑎 ∈ ℝ⁺ ∀𝑧 ∈ (𝐴 ∩ (-∞(,)𝐵))((𝑧 ≠ 𝐵 ∧ (abs‘(𝑧 − 𝐵)) < 𝑎) → (abs‘(((𝐹 ↾ (-∞(,)𝐵))‘𝑧) − 𝐿)) < 𝑥)))
159	158	simprd 500	. . . . 5 ⊢ (𝜑 → ∀𝑥 ∈ ℝ⁺ ∃𝑎 ∈ ℝ⁺ ∀𝑧 ∈ (𝐴 ∩ (-∞(,)𝐵))((𝑧 ≠ 𝐵 ∧ (abs‘(𝑧 − 𝐵)) < 𝑎) → (abs‘(((𝐹 ↾ (-∞(,)𝐵))‘𝑧) − 𝐿)) < 𝑥))
160	159	r19.21bi 3138	. . . 4 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ⁺) → ∃𝑎 ∈ ℝ⁺ ∀𝑧 ∈ (𝐴 ∩ (-∞(,)𝐵))((𝑧 ≠ 𝐵 ∧ (abs‘(𝑧 − 𝐵)) < 𝑎) → (abs‘(((𝐹 ↾ (-∞(,)𝐵))‘𝑧) − 𝐿)) < 𝑥))
161	148, 160	r19.29a 3214	. . 3 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ⁺) → ∃𝑦 ∈ ℝ⁺ ∀𝑧 ∈ 𝐴 ((𝑧 ≠ 𝐵 ∧ (abs‘(𝑧 − 𝐵)) < 𝑦) → (abs‘((𝐹‘𝑧) − 𝐿)) < 𝑥))
162	161	ralrimiva 3114	. 2 ⊢ (𝜑 → ∀𝑥 ∈ ℝ⁺ ∃𝑦 ∈ ℝ⁺ ∀𝑧 ∈ 𝐴 ((𝑧 ≠ 𝐵 ∧ (abs‘(𝑧 − 𝐵)) < 𝑦) → (abs‘((𝐹‘𝑧) − 𝐿)) < 𝑥))
163	25, 154	sstrdi 3905	. . 3 ⊢ (𝜑 → 𝐴 ⊆ ℂ)
164	128, 163, 50	ellimc3 24579	. 2 ⊢ (𝜑 → (𝐿 ∈ (𝐹 lim_ℂ 𝐵) ↔ (𝐿 ∈ ℂ ∧ ∀𝑥 ∈ ℝ⁺ ∃𝑦 ∈ ℝ⁺ ∀𝑧 ∈ 𝐴 ((𝑧 ≠ 𝐵 ∧ (abs‘(𝑧 − 𝐵)) < 𝑦) → (abs‘((𝐹‘𝑧) − 𝐿)) < 𝑥))))
165	3, 162, 164	mpbir2and 713	1 ⊢ (𝜑 → 𝐿 ∈ (𝐹 lim_ℂ 𝐵))

Colors of variables: wff setvar class

Syntax hints: ¬ wn 3 → wi 4 ↔ wb 209 ∧ wa 400 ∧ w3a 1085 = wceq 1539 ∈ wcel 2112 ≠ wne 2952 ∀wral 3071 ∃wrex 3072 ∩ cin 3858 ⊆ wss 3859 ifcif 4421 class class class wbr 5033 ran crn 5526 ↾ cres 5527 ⟶wf 6332 ‘cfv 6336 (class class class)co 7151 ℂcc 10574 ℝcr 10575 +∞cpnf 10711 -∞cmnf 10712 ℝ^*cxr 10713 < clt 10714 ≤ cle 10715 − cmin 10909 ℝ⁺crp 12431 (,)cioo 12780 abscabs 14642 TopOpenctopn 16754 topGenctg 16770 ℂ_fldccnfld 20167 lim_ℂ climc 24562

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1798 ax-4 1812 ax-5 1912 ax-6 1971 ax-7 2016 ax-8 2114 ax-9 2122 ax-10 2143 ax-11 2159 ax-12 2176 ax-ext 2730 ax-rep 5157 ax-sep 5170 ax-nul 5177 ax-pow 5235 ax-pr 5299 ax-un 7460 ax-cnex 10632 ax-resscn 10633 ax-1cn 10634 ax-icn 10635 ax-addcl 10636 ax-addrcl 10637 ax-mulcl 10638 ax-mulrcl 10639 ax-mulcom 10640 ax-addass 10641 ax-mulass 10642 ax-distr 10643 ax-i2m1 10644 ax-1ne0 10645 ax-1rid 10646 ax-rnegex 10647 ax-rrecex 10648 ax-cnre 10649 ax-pre-lttri 10650 ax-pre-lttrn 10651 ax-pre-ltadd 10652 ax-pre-mulgt0 10653 ax-pre-sup 10654

This theorem depends on definitions: df-bi 210 df-an 401 df-or 846 df-3or 1086 df-3an 1087 df-tru 1542 df-fal 1552 df-ex 1783 df-nf 1787 df-sb 2071 df-mo 2558 df-eu 2589 df-clab 2737 df-cleq 2751 df-clel 2831 df-nfc 2902 df-ne 2953 df-nel 3057 df-ral 3076 df-rex 3077 df-reu 3078 df-rmo 3079 df-rab 3080 df-v 3412 df-sbc 3698 df-csb 3807 df-dif 3862 df-un 3864 df-in 3866 df-ss 3876 df-pss 3878 df-nul 4227 df-if 4422 df-pw 4497 df-sn 4524 df-pr 4526 df-tp 4528 df-op 4530 df-uni 4800 df-int 4840 df-iun 4886 df-br 5034 df-opab 5096 df-mpt 5114 df-tr 5140 df-id 5431 df-eprel 5436 df-po 5444 df-so 5445 df-fr 5484 df-we 5486 df-xp 5531 df-rel 5532 df-cnv 5533 df-co 5534 df-dm 5535 df-rn 5536 df-res 5537 df-ima 5538 df-pred 6127 df-ord 6173 df-on 6174 df-lim 6175 df-suc 6176 df-iota 6295 df-fun 6338 df-fn 6339 df-f 6340 df-f1 6341 df-fo 6342 df-f1o 6343 df-fv 6344 df-riota 7109 df-ov 7154 df-oprab 7155 df-mpo 7156 df-om 7581 df-1st 7694 df-2nd 7695 df-wrecs 7958 df-recs 8019 df-rdg 8057 df-1o 8113 df-er 8300 df-map 8419 df-pm 8420 df-en 8529 df-dom 8530 df-sdom 8531 df-fin 8532 df-fi 8909 df-sup 8940 df-inf 8941 df-pnf 10716 df-mnf 10717 df-xr 10718 df-ltxr 10719 df-le 10720 df-sub 10911 df-neg 10912 df-div 11337 df-nn 11676 df-2 11738 df-3 11739 df-4 11740 df-5 11741 df-6 11742 df-7 11743 df-8 11744 df-9 11745 df-n0 11936 df-z 12022 df-dec 12139 df-uz 12284 df-q 12390 df-rp 12432 df-xneg 12549 df-xadd 12550 df-xmul 12551 df-ioo 12784 df-fz 12941 df-seq 13420 df-exp 13481 df-cj 14507 df-re 14508 df-im 14509 df-sqrt 14643 df-abs 14644 df-struct 16544 df-ndx 16545 df-slot 16546 df-base 16548 df-plusg 16637 df-mulr 16638 df-starv 16639 df-tset 16643 df-ple 16644 df-ds 16646 df-unif 16647 df-rest 16755 df-topn 16756 df-topgen 16776 df-psmet 20159 df-xmet 20160 df-met 20161 df-bl 20162 df-mopn 20163 df-cnfld 20168 df-top 21595 df-topon 21612 df-topsp 21634 df-bases 21647 df-cnp 21929 df-xms 23023 df-ms 23024 df-limc 24566

This theorem is referenced by: limclr 42664

W3C validator