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 46250

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 26003	. . 3 ⊢ ((𝐹 ↾ (-∞(,)𝐵)) lim_ℂ 𝐵) ⊆ ℂ
2		limcleqr.l	. . 3 ⊢ (𝜑 → 𝐿 ∈ ((𝐹 ↾ (-∞(,)𝐵)) lim_ℂ 𝐵))
3	1, 2	sselid 3943	. 2 ⊢ (𝜑 → 𝐿 ∈ ℂ)
4		simp-4r 795	. . . . . . 7 ⊢ ((((((𝜑 ∧ 𝑥 ∈ ℝ⁺) ∧ 𝑎 ∈ ℝ⁺) ∧ ∀𝑧 ∈ (𝐴 ∩ (-∞(,)𝐵))((𝑧 ≠ 𝐵 ∧ (abs‘(𝑧 − 𝐵)) < 𝑎) → (abs‘(((𝐹 ↾ (-∞(,)𝐵))‘𝑧) − 𝐿)) < 𝑥)) ∧ 𝑏 ∈ ℝ⁺) ∧ ∀𝑧 ∈ (𝐴 ∩ (𝐵(,)+∞))((𝑧 ≠ 𝐵 ∧ (abs‘(𝑧 − 𝐵)) < 𝑏) → (abs‘(((𝐹 ↾ (𝐵(,)+∞))‘𝑧) − 𝐿)) < 𝑥)) → 𝑎 ∈ ℝ⁺)
5		simplr 780	. . . . . . 7 ⊢ ((((((𝜑 ∧ 𝑥 ∈ ℝ⁺) ∧ 𝑎 ∈ ℝ⁺) ∧ ∀𝑧 ∈ (𝐴 ∩ (-∞(,)𝐵))((𝑧 ≠ 𝐵 ∧ (abs‘(𝑧 − 𝐵)) < 𝑎) → (abs‘(((𝐹 ↾ (-∞(,)𝐵))‘𝑧) − 𝐿)) < 𝑥)) ∧ 𝑏 ∈ ℝ⁺) ∧ ∀𝑧 ∈ (𝐴 ∩ (𝐵(,)+∞))((𝑧 ≠ 𝐵 ∧ (abs‘(𝑧 − 𝐵)) < 𝑏) → (abs‘(((𝐹 ↾ (𝐵(,)+∞))‘𝑧) − 𝐿)) < 𝑥)) → 𝑏 ∈ ℝ⁺)
6	4, 5	ifcld 4539	. . . . . 6 ⊢ ((((((𝜑 ∧ 𝑥 ∈ ℝ⁺) ∧ 𝑎 ∈ ℝ⁺) ∧ ∀𝑧 ∈ (𝐴 ∩ (-∞(,)𝐵))((𝑧 ≠ 𝐵 ∧ (abs‘(𝑧 − 𝐵)) < 𝑎) → (abs‘(((𝐹 ↾ (-∞(,)𝐵))‘𝑧) − 𝐿)) < 𝑥)) ∧ 𝑏 ∈ ℝ⁺) ∧ ∀𝑧 ∈ (𝐴 ∩ (𝐵(,)+∞))((𝑧 ≠ 𝐵 ∧ (abs‘(𝑧 − 𝐵)) < 𝑏) → (abs‘(((𝐹 ↾ (𝐵(,)+∞))‘𝑧) − 𝐿)) < 𝑥)) → if(𝑎 ≤ 𝑏, 𝑎, 𝑏) ∈ ℝ⁺)
7		nfv 1941	. . . . . . . . . . 11 ⊢ Ⅎ𝑧(𝜑 ∧ 𝑥 ∈ ℝ⁺)
8		nfv 1941	. . . . . . . . . . 11 ⊢ Ⅎ𝑧 𝑎 ∈ ℝ⁺
9	7, 8	nfan 1926	. . . . . . . . . 10 ⊢ Ⅎ𝑧((𝜑 ∧ 𝑥 ∈ ℝ⁺) ∧ 𝑎 ∈ ℝ⁺)
10		nfra1 3295	. . . . . . . . . 10 ⊢ Ⅎ𝑧∀𝑧 ∈ (𝐴 ∩ (-∞(,)𝐵))((𝑧 ≠ 𝐵 ∧ (abs‘(𝑧 − 𝐵)) < 𝑎) → (abs‘(((𝐹 ↾ (-∞(,)𝐵))‘𝑧) − 𝐿)) < 𝑥)
11	9, 10	nfan 1926	. . . . . . . . 9 ⊢ Ⅎ𝑧(((𝜑 ∧ 𝑥 ∈ ℝ⁺) ∧ 𝑎 ∈ ℝ⁺) ∧ ∀𝑧 ∈ (𝐴 ∩ (-∞(,)𝐵))((𝑧 ≠ 𝐵 ∧ (abs‘(𝑧 − 𝐵)) < 𝑎) → (abs‘(((𝐹 ↾ (-∞(,)𝐵))‘𝑧) − 𝐿)) < 𝑥))
12		nfv 1941	. . . . . . . . 9 ⊢ Ⅎ𝑧 𝑏 ∈ ℝ⁺
13	11, 12	nfan 1926	. . . . . . . 8 ⊢ Ⅎ𝑧((((𝜑 ∧ 𝑥 ∈ ℝ⁺) ∧ 𝑎 ∈ ℝ⁺) ∧ ∀𝑧 ∈ (𝐴 ∩ (-∞(,)𝐵))((𝑧 ≠ 𝐵 ∧ (abs‘(𝑧 − 𝐵)) < 𝑎) → (abs‘(((𝐹 ↾ (-∞(,)𝐵))‘𝑧) − 𝐿)) < 𝑥)) ∧ 𝑏 ∈ ℝ⁺)
14		nfra1 3295	. . . . . . . 8 ⊢ Ⅎ𝑧∀𝑧 ∈ (𝐴 ∩ (𝐵(,)+∞))((𝑧 ≠ 𝐵 ∧ (abs‘(𝑧 − 𝐵)) < 𝑏) → (abs‘(((𝐹 ↾ (𝐵(,)+∞))‘𝑧) − 𝐿)) < 𝑥)
15	13, 14	nfan 1926	. . . . . . 7 ⊢ Ⅎ𝑧(((((𝜑 ∧ 𝑥 ∈ ℝ⁺) ∧ 𝑎 ∈ ℝ⁺) ∧ ∀𝑧 ∈ (𝐴 ∩ (-∞(,)𝐵))((𝑧 ≠ 𝐵 ∧ (abs‘(𝑧 − 𝐵)) < 𝑎) → (abs‘(((𝐹 ↾ (-∞(,)𝐵))‘𝑧) − 𝐿)) < 𝑥)) ∧ 𝑏 ∈ ℝ⁺) ∧ ∀𝑧 ∈ (𝐴 ∩ (𝐵(,)+∞))((𝑧 ≠ 𝐵 ∧ (abs‘(𝑧 − 𝐵)) < 𝑏) → (abs‘(((𝐹 ↾ (𝐵(,)+∞))‘𝑧) − 𝐿)) < 𝑥))
16		simp-6l 798	. . . . . . . . . . . . 13 ⊢ (((((((𝜑 ∧ 𝑥 ∈ ℝ⁺) ∧ 𝑎 ∈ ℝ⁺) ∧ ∀𝑧 ∈ (𝐴 ∩ (-∞(,)𝐵))((𝑧 ≠ 𝐵 ∧ (abs‘(𝑧 − 𝐵)) < 𝑎) → (abs‘(((𝐹 ↾ (-∞(,)𝐵))‘𝑧) − 𝐿)) < 𝑥)) ∧ 𝑏 ∈ ℝ⁺) ∧ ∀𝑧 ∈ (𝐴 ∩ (𝐵(,)+∞))((𝑧 ≠ 𝐵 ∧ (abs‘(𝑧 − 𝐵)) < 𝑏) → (abs‘(((𝐹 ↾ (𝐵(,)+∞))‘𝑧) − 𝐿)) < 𝑥)) ∧ 𝑧 < 𝐵) → 𝜑)
17	16	3ad2antl1 1202	. . . . . . . . . . . 12 ⊢ ((((((((𝜑 ∧ 𝑥 ∈ ℝ⁺) ∧ 𝑎 ∈ ℝ⁺) ∧ ∀𝑧 ∈ (𝐴 ∩ (-∞(,)𝐵))((𝑧 ≠ 𝐵 ∧ (abs‘(𝑧 − 𝐵)) < 𝑎) → (abs‘(((𝐹 ↾ (-∞(,)𝐵))‘𝑧) − 𝐿)) < 𝑥)) ∧ 𝑏 ∈ ℝ⁺) ∧ ∀𝑧 ∈ (𝐴 ∩ (𝐵(,)+∞))((𝑧 ≠ 𝐵 ∧ (abs‘(𝑧 − 𝐵)) < 𝑏) → (abs‘(((𝐹 ↾ (𝐵(,)+∞))‘𝑧) − 𝐿)) < 𝑥)) ∧ 𝑧 ∈ 𝐴 ∧ (𝑧 ≠ 𝐵 ∧ (abs‘(𝑧 − 𝐵)) < if(𝑎 ≤ 𝑏, 𝑎, 𝑏))) ∧ 𝑧 < 𝐵) → 𝜑)
18		simpl2 1209	. . . . . . . . . . . 12 ⊢ ((((((((𝜑 ∧ 𝑥 ∈ ℝ⁺) ∧ 𝑎 ∈ ℝ⁺) ∧ ∀𝑧 ∈ (𝐴 ∩ (-∞(,)𝐵))((𝑧 ≠ 𝐵 ∧ (abs‘(𝑧 − 𝐵)) < 𝑎) → (abs‘(((𝐹 ↾ (-∞(,)𝐵))‘𝑧) − 𝐿)) < 𝑥)) ∧ 𝑏 ∈ ℝ⁺) ∧ ∀𝑧 ∈ (𝐴 ∩ (𝐵(,)+∞))((𝑧 ≠ 𝐵 ∧ (abs‘(𝑧 − 𝐵)) < 𝑏) → (abs‘(((𝐹 ↾ (𝐵(,)+∞))‘𝑧) − 𝐿)) < 𝑥)) ∧ 𝑧 ∈ 𝐴 ∧ (𝑧 ≠ 𝐵 ∧ (abs‘(𝑧 − 𝐵)) < if(𝑎 ≤ 𝑏, 𝑎, 𝑏))) ∧ 𝑧 < 𝐵) → 𝑧 ∈ 𝐴)
19		simpr 489	. . . . . . . . . . . 12 ⊢ ((((((((𝜑 ∧ 𝑥 ∈ ℝ⁺) ∧ 𝑎 ∈ ℝ⁺) ∧ ∀𝑧 ∈ (𝐴 ∩ (-∞(,)𝐵))((𝑧 ≠ 𝐵 ∧ (abs‘(𝑧 − 𝐵)) < 𝑎) → (abs‘(((𝐹 ↾ (-∞(,)𝐵))‘𝑧) − 𝐿)) < 𝑥)) ∧ 𝑏 ∈ ℝ⁺) ∧ ∀𝑧 ∈ (𝐴 ∩ (𝐵(,)+∞))((𝑧 ≠ 𝐵 ∧ (abs‘(𝑧 − 𝐵)) < 𝑏) → (abs‘(((𝐹 ↾ (𝐵(,)+∞))‘𝑧) − 𝐿)) < 𝑥)) ∧ 𝑧 ∈ 𝐴 ∧ (𝑧 ≠ 𝐵 ∧ (abs‘(𝑧 − 𝐵)) < if(𝑎 ≤ 𝑏, 𝑎, 𝑏))) ∧ 𝑧 < 𝐵) → 𝑧 < 𝐵)
20		mnfxr 11266	. . . . . . . . . . . . . 14 ⊢ -∞ ∈ ℝ^*
21	20	a1i 11	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝐴 ∧ 𝑧 < 𝐵) → -∞ ∈ ℝ^*)
22		limcleqr.b	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → 𝐵 ∈ ℝ)
23	22	rexrd 11259	. . . . . . . . . . . . . 14 ⊢ (𝜑 → 𝐵 ∈ ℝ^*)
24	23	3ad2ant1 1149	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝐴 ∧ 𝑧 < 𝐵) → 𝐵 ∈ ℝ^*)
25		limcleqr.a	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → 𝐴 ⊆ ℝ)
26	25	sselda 3945	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝐴) → 𝑧 ∈ ℝ)
27	26	3adant3 1148	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝐴 ∧ 𝑧 < 𝐵) → 𝑧 ∈ ℝ)
28	27	mnfltd 13149	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝐴 ∧ 𝑧 < 𝐵) → -∞ < 𝑧)
29		simp3 1154	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝐴 ∧ 𝑧 < 𝐵) → 𝑧 < 𝐵)
30	21, 24, 27, 28, 29	eliood 46106	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝐴 ∧ 𝑧 < 𝐵) → 𝑧 ∈ (-∞(,)𝐵))
31	17, 18, 19, 30	syl3anc 1396	. . . . . . . . . . 11 ⊢ ((((((((𝜑 ∧ 𝑥 ∈ ℝ⁺) ∧ 𝑎 ∈ ℝ⁺) ∧ ∀𝑧 ∈ (𝐴 ∩ (-∞(,)𝐵))((𝑧 ≠ 𝐵 ∧ (abs‘(𝑧 − 𝐵)) < 𝑎) → (abs‘(((𝐹 ↾ (-∞(,)𝐵))‘𝑧) − 𝐿)) < 𝑥)) ∧ 𝑏 ∈ ℝ⁺) ∧ ∀𝑧 ∈ (𝐴 ∩ (𝐵(,)+∞))((𝑧 ≠ 𝐵 ∧ (abs‘(𝑧 − 𝐵)) < 𝑏) → (abs‘(((𝐹 ↾ (𝐵(,)+∞))‘𝑧) − 𝐿)) < 𝑥)) ∧ 𝑧 ∈ 𝐴 ∧ (𝑧 ≠ 𝐵 ∧ (abs‘(𝑧 − 𝐵)) < if(𝑎 ≤ 𝑏, 𝑎, 𝑏))) ∧ 𝑧 < 𝐵) → 𝑧 ∈ (-∞(,)𝐵))
32		fvres 6901	. . . . . . . . . . . . . 14 ⊢ (𝑧 ∈ (-∞(,)𝐵) → ((𝐹 ↾ (-∞(,)𝐵))‘𝑧) = (𝐹‘𝑧))
33	32	oveq1d 7426	. . . . . . . . . . . . 13 ⊢ (𝑧 ∈ (-∞(,)𝐵) → (((𝐹 ↾ (-∞(,)𝐵))‘𝑧) − 𝐿) = ((𝐹‘𝑧) − 𝐿))
34	33	eqcomd 2775	. . . . . . . . . . . 12 ⊢ (𝑧 ∈ (-∞(,)𝐵) → ((𝐹‘𝑧) − 𝐿) = (((𝐹 ↾ (-∞(,)𝐵))‘𝑧) − 𝐿))
35	34	fveq2d 6886	. . . . . . . . . . 11 ⊢ (𝑧 ∈ (-∞(,)𝐵) → (abs‘((𝐹‘𝑧) − 𝐿)) = (abs‘(((𝐹 ↾ (-∞(,)𝐵))‘𝑧) − 𝐿)))
36	31, 35	syl 18	. . . . . . . . . 10 ⊢ ((((((((𝜑 ∧ 𝑥 ∈ ℝ⁺) ∧ 𝑎 ∈ ℝ⁺) ∧ ∀𝑧 ∈ (𝐴 ∩ (-∞(,)𝐵))((𝑧 ≠ 𝐵 ∧ (abs‘(𝑧 − 𝐵)) < 𝑎) → (abs‘(((𝐹 ↾ (-∞(,)𝐵))‘𝑧) − 𝐿)) < 𝑥)) ∧ 𝑏 ∈ ℝ⁺) ∧ ∀𝑧 ∈ (𝐴 ∩ (𝐵(,)+∞))((𝑧 ≠ 𝐵 ∧ (abs‘(𝑧 − 𝐵)) < 𝑏) → (abs‘(((𝐹 ↾ (𝐵(,)+∞))‘𝑧) − 𝐿)) < 𝑥)) ∧ 𝑧 ∈ 𝐴 ∧ (𝑧 ≠ 𝐵 ∧ (abs‘(𝑧 − 𝐵)) < if(𝑎 ≤ 𝑏, 𝑎, 𝑏))) ∧ 𝑧 < 𝐵) → (abs‘((𝐹‘𝑧) − 𝐿)) = (abs‘(((𝐹 ↾ (-∞(,)𝐵))‘𝑧) − 𝐿)))
37		simp-4r 795	. . . . . . . . . . . . 13 ⊢ (((((((𝜑 ∧ 𝑥 ∈ ℝ⁺) ∧ 𝑎 ∈ ℝ⁺) ∧ ∀𝑧 ∈ (𝐴 ∩ (-∞(,)𝐵))((𝑧 ≠ 𝐵 ∧ (abs‘(𝑧 − 𝐵)) < 𝑎) → (abs‘(((𝐹 ↾ (-∞(,)𝐵))‘𝑧) − 𝐿)) < 𝑥)) ∧ 𝑏 ∈ ℝ⁺) ∧ ∀𝑧 ∈ (𝐴 ∩ (𝐵(,)+∞))((𝑧 ≠ 𝐵 ∧ (abs‘(𝑧 − 𝐵)) < 𝑏) → (abs‘(((𝐹 ↾ (𝐵(,)+∞))‘𝑧) − 𝐿)) < 𝑥)) ∧ 𝑧 < 𝐵) → ∀𝑧 ∈ (𝐴 ∩ (-∞(,)𝐵))((𝑧 ≠ 𝐵 ∧ (abs‘(𝑧 − 𝐵)) < 𝑎) → (abs‘(((𝐹 ↾ (-∞(,)𝐵))‘𝑧) − 𝐿)) < 𝑥))
38	37	3ad2antl1 1202	. . . . . . . . . . . 12 ⊢ ((((((((𝜑 ∧ 𝑥 ∈ ℝ⁺) ∧ 𝑎 ∈ ℝ⁺) ∧ ∀𝑧 ∈ (𝐴 ∩ (-∞(,)𝐵))((𝑧 ≠ 𝐵 ∧ (abs‘(𝑧 − 𝐵)) < 𝑎) → (abs‘(((𝐹 ↾ (-∞(,)𝐵))‘𝑧) − 𝐿)) < 𝑥)) ∧ 𝑏 ∈ ℝ⁺) ∧ ∀𝑧 ∈ (𝐴 ∩ (𝐵(,)+∞))((𝑧 ≠ 𝐵 ∧ (abs‘(𝑧 − 𝐵)) < 𝑏) → (abs‘(((𝐹 ↾ (𝐵(,)+∞))‘𝑧) − 𝐿)) < 𝑥)) ∧ 𝑧 ∈ 𝐴 ∧ (𝑧 ≠ 𝐵 ∧ (abs‘(𝑧 − 𝐵)) < if(𝑎 ≤ 𝑏, 𝑎, 𝑏))) ∧ 𝑧 < 𝐵) → ∀𝑧 ∈ (𝐴 ∩ (-∞(,)𝐵))((𝑧 ≠ 𝐵 ∧ (abs‘(𝑧 − 𝐵)) < 𝑎) → (abs‘(((𝐹 ↾ (-∞(,)𝐵))‘𝑧) − 𝐿)) < 𝑥))
39	18, 31	elind 4161	. . . . . . . . . . . 12 ⊢ ((((((((𝜑 ∧ 𝑥 ∈ ℝ⁺) ∧ 𝑎 ∈ ℝ⁺) ∧ ∀𝑧 ∈ (𝐴 ∩ (-∞(,)𝐵))((𝑧 ≠ 𝐵 ∧ (abs‘(𝑧 − 𝐵)) < 𝑎) → (abs‘(((𝐹 ↾ (-∞(,)𝐵))‘𝑧) − 𝐿)) < 𝑥)) ∧ 𝑏 ∈ ℝ⁺) ∧ ∀𝑧 ∈ (𝐴 ∩ (𝐵(,)+∞))((𝑧 ≠ 𝐵 ∧ (abs‘(𝑧 − 𝐵)) < 𝑏) → (abs‘(((𝐹 ↾ (𝐵(,)+∞))‘𝑧) − 𝐿)) < 𝑥)) ∧ 𝑧 ∈ 𝐴 ∧ (𝑧 ≠ 𝐵 ∧ (abs‘(𝑧 − 𝐵)) < if(𝑎 ≤ 𝑏, 𝑎, 𝑏))) ∧ 𝑧 < 𝐵) → 𝑧 ∈ (𝐴 ∩ (-∞(,)𝐵)))
40	38, 39	jca 520	. . . . . . . . . . 11 ⊢ ((((((((𝜑 ∧ 𝑥 ∈ ℝ⁺) ∧ 𝑎 ∈ ℝ⁺) ∧ ∀𝑧 ∈ (𝐴 ∩ (-∞(,)𝐵))((𝑧 ≠ 𝐵 ∧ (abs‘(𝑧 − 𝐵)) < 𝑎) → (abs‘(((𝐹 ↾ (-∞(,)𝐵))‘𝑧) − 𝐿)) < 𝑥)) ∧ 𝑏 ∈ ℝ⁺) ∧ ∀𝑧 ∈ (𝐴 ∩ (𝐵(,)+∞))((𝑧 ≠ 𝐵 ∧ (abs‘(𝑧 − 𝐵)) < 𝑏) → (abs‘(((𝐹 ↾ (𝐵(,)+∞))‘𝑧) − 𝐿)) < 𝑥)) ∧ 𝑧 ∈ 𝐴 ∧ (𝑧 ≠ 𝐵 ∧ (abs‘(𝑧 − 𝐵)) < if(𝑎 ≤ 𝑏, 𝑎, 𝑏))) ∧ 𝑧 < 𝐵) → (∀𝑧 ∈ (𝐴 ∩ (-∞(,)𝐵))((𝑧 ≠ 𝐵 ∧ (abs‘(𝑧 − 𝐵)) < 𝑎) → (abs‘(((𝐹 ↾ (-∞(,)𝐵))‘𝑧) − 𝐿)) < 𝑥) ∧ 𝑧 ∈ (𝐴 ∩ (-∞(,)𝐵))))
41		simpl3l 1245	. . . . . . . . . . . 12 ⊢ ((((((((𝜑 ∧ 𝑥 ∈ ℝ⁺) ∧ 𝑎 ∈ ℝ⁺) ∧ ∀𝑧 ∈ (𝐴 ∩ (-∞(,)𝐵))((𝑧 ≠ 𝐵 ∧ (abs‘(𝑧 − 𝐵)) < 𝑎) → (abs‘(((𝐹 ↾ (-∞(,)𝐵))‘𝑧) − 𝐿)) < 𝑥)) ∧ 𝑏 ∈ ℝ⁺) ∧ ∀𝑧 ∈ (𝐴 ∩ (𝐵(,)+∞))((𝑧 ≠ 𝐵 ∧ (abs‘(𝑧 − 𝐵)) < 𝑏) → (abs‘(((𝐹 ↾ (𝐵(,)+∞))‘𝑧) − 𝐿)) < 𝑥)) ∧ 𝑧 ∈ 𝐴 ∧ (𝑧 ≠ 𝐵 ∧ (abs‘(𝑧 − 𝐵)) < if(𝑎 ≤ 𝑏, 𝑎, 𝑏))) ∧ 𝑧 < 𝐵) → 𝑧 ≠ 𝐵)
42	4	adantr 485	. . . . . . . . . . . . . 14 ⊢ (((((((𝜑 ∧ 𝑥 ∈ ℝ⁺) ∧ 𝑎 ∈ ℝ⁺) ∧ ∀𝑧 ∈ (𝐴 ∩ (-∞(,)𝐵))((𝑧 ≠ 𝐵 ∧ (abs‘(𝑧 − 𝐵)) < 𝑎) → (abs‘(((𝐹 ↾ (-∞(,)𝐵))‘𝑧) − 𝐿)) < 𝑥)) ∧ 𝑏 ∈ ℝ⁺) ∧ ∀𝑧 ∈ (𝐴 ∩ (𝐵(,)+∞))((𝑧 ≠ 𝐵 ∧ (abs‘(𝑧 − 𝐵)) < 𝑏) → (abs‘(((𝐹 ↾ (𝐵(,)+∞))‘𝑧) − 𝐿)) < 𝑥)) ∧ 𝑧 < 𝐵) → 𝑎 ∈ ℝ⁺)
43	42	3ad2antl1 1202	. . . . . . . . . . . . 13 ⊢ ((((((((𝜑 ∧ 𝑥 ∈ ℝ⁺) ∧ 𝑎 ∈ ℝ⁺) ∧ ∀𝑧 ∈ (𝐴 ∩ (-∞(,)𝐵))((𝑧 ≠ 𝐵 ∧ (abs‘(𝑧 − 𝐵)) < 𝑎) → (abs‘(((𝐹 ↾ (-∞(,)𝐵))‘𝑧) − 𝐿)) < 𝑥)) ∧ 𝑏 ∈ ℝ⁺) ∧ ∀𝑧 ∈ (𝐴 ∩ (𝐵(,)+∞))((𝑧 ≠ 𝐵 ∧ (abs‘(𝑧 − 𝐵)) < 𝑏) → (abs‘(((𝐹 ↾ (𝐵(,)+∞))‘𝑧) − 𝐿)) < 𝑥)) ∧ 𝑧 ∈ 𝐴 ∧ (𝑧 ≠ 𝐵 ∧ (abs‘(𝑧 − 𝐵)) < if(𝑎 ≤ 𝑏, 𝑎, 𝑏))) ∧ 𝑧 < 𝐵) → 𝑎 ∈ ℝ⁺)
44	5	adantr 485	. . . . . . . . . . . . . 14 ⊢ (((((((𝜑 ∧ 𝑥 ∈ ℝ⁺) ∧ 𝑎 ∈ ℝ⁺) ∧ ∀𝑧 ∈ (𝐴 ∩ (-∞(,)𝐵))((𝑧 ≠ 𝐵 ∧ (abs‘(𝑧 − 𝐵)) < 𝑎) → (abs‘(((𝐹 ↾ (-∞(,)𝐵))‘𝑧) − 𝐿)) < 𝑥)) ∧ 𝑏 ∈ ℝ⁺) ∧ ∀𝑧 ∈ (𝐴 ∩ (𝐵(,)+∞))((𝑧 ≠ 𝐵 ∧ (abs‘(𝑧 − 𝐵)) < 𝑏) → (abs‘(((𝐹 ↾ (𝐵(,)+∞))‘𝑧) − 𝐿)) < 𝑥)) ∧ 𝑧 < 𝐵) → 𝑏 ∈ ℝ⁺)
45	44	3ad2antl1 1202	. . . . . . . . . . . . 13 ⊢ ((((((((𝜑 ∧ 𝑥 ∈ ℝ⁺) ∧ 𝑎 ∈ ℝ⁺) ∧ ∀𝑧 ∈ (𝐴 ∩ (-∞(,)𝐵))((𝑧 ≠ 𝐵 ∧ (abs‘(𝑧 − 𝐵)) < 𝑎) → (abs‘(((𝐹 ↾ (-∞(,)𝐵))‘𝑧) − 𝐿)) < 𝑥)) ∧ 𝑏 ∈ ℝ⁺) ∧ ∀𝑧 ∈ (𝐴 ∩ (𝐵(,)+∞))((𝑧 ≠ 𝐵 ∧ (abs‘(𝑧 − 𝐵)) < 𝑏) → (abs‘(((𝐹 ↾ (𝐵(,)+∞))‘𝑧) − 𝐿)) < 𝑥)) ∧ 𝑧 ∈ 𝐴 ∧ (𝑧 ≠ 𝐵 ∧ (abs‘(𝑧 − 𝐵)) < if(𝑎 ≤ 𝑏, 𝑎, 𝑏))) ∧ 𝑧 < 𝐵) → 𝑏 ∈ ℝ⁺)
46		simpl3r 1246	. . . . . . . . . . . . 13 ⊢ ((((((((𝜑 ∧ 𝑥 ∈ ℝ⁺) ∧ 𝑎 ∈ ℝ⁺) ∧ ∀𝑧 ∈ (𝐴 ∩ (-∞(,)𝐵))((𝑧 ≠ 𝐵 ∧ (abs‘(𝑧 − 𝐵)) < 𝑎) → (abs‘(((𝐹 ↾ (-∞(,)𝐵))‘𝑧) − 𝐿)) < 𝑥)) ∧ 𝑏 ∈ ℝ⁺) ∧ ∀𝑧 ∈ (𝐴 ∩ (𝐵(,)+∞))((𝑧 ≠ 𝐵 ∧ (abs‘(𝑧 − 𝐵)) < 𝑏) → (abs‘(((𝐹 ↾ (𝐵(,)+∞))‘𝑧) − 𝐿)) < 𝑥)) ∧ 𝑧 ∈ 𝐴 ∧ (𝑧 ≠ 𝐵 ∧ (abs‘(𝑧 − 𝐵)) < if(𝑎 ≤ 𝑏, 𝑎, 𝑏))) ∧ 𝑧 < 𝐵) → (abs‘(𝑧 − 𝐵)) < if(𝑎 ≤ 𝑏, 𝑎, 𝑏))
47		simpl1 1208	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑎 ∈ ℝ⁺ ∧ 𝑏 ∈ ℝ⁺) ∧ ((abs‘(𝑧 − 𝐵)) < if(𝑎 ≤ 𝑏, 𝑎, 𝑏) ∧ 𝑧 ∈ 𝐴)) → 𝜑)
48		simprr 784	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑎 ∈ ℝ⁺ ∧ 𝑏 ∈ ℝ⁺) ∧ ((abs‘(𝑧 − 𝐵)) < if(𝑎 ≤ 𝑏, 𝑎, 𝑏) ∧ 𝑧 ∈ 𝐴)) → 𝑧 ∈ 𝐴)
49	26	recnd 11237	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝐴) → 𝑧 ∈ ℂ)
50	22	recnd 11237	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → 𝐵 ∈ ℂ)
51	50	adantr 485	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝐴) → 𝐵 ∈ ℂ)
52	49, 51	subcld 11569	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝐴) → (𝑧 − 𝐵) ∈ ℂ)
53	52	abscld 15490	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝐴) → (abs‘(𝑧 − 𝐵)) ∈ ℝ)
54	47, 48, 53	syl2anc 595	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑎 ∈ ℝ⁺ ∧ 𝑏 ∈ ℝ⁺) ∧ ((abs‘(𝑧 − 𝐵)) < if(𝑎 ≤ 𝑏, 𝑎, 𝑏) ∧ 𝑧 ∈ 𝐴)) → (abs‘(𝑧 − 𝐵)) ∈ ℝ)
55		rpre 13025	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑎 ∈ ℝ⁺ → 𝑎 ∈ ℝ)
56	55	adantr 485	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑎 ∈ ℝ⁺ ∧ 𝑏 ∈ ℝ⁺) → 𝑎 ∈ ℝ)
57		rpre 13025	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑏 ∈ ℝ⁺ → 𝑏 ∈ ℝ)
58	57	adantl 486	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑎 ∈ ℝ⁺ ∧ 𝑏 ∈ ℝ⁺) → 𝑏 ∈ ℝ)
59	56, 58	ifcld 4539	. . . . . . . . . . . . . . . 16 ⊢ ((𝑎 ∈ ℝ⁺ ∧ 𝑏 ∈ ℝ⁺) → if(𝑎 ≤ 𝑏, 𝑎, 𝑏) ∈ ℝ)
60	59	3adant1 1146	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑎 ∈ ℝ⁺ ∧ 𝑏 ∈ ℝ⁺) → if(𝑎 ≤ 𝑏, 𝑎, 𝑏) ∈ ℝ)
61	60	adantr 485	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑎 ∈ ℝ⁺ ∧ 𝑏 ∈ ℝ⁺) ∧ ((abs‘(𝑧 − 𝐵)) < if(𝑎 ≤ 𝑏, 𝑎, 𝑏) ∧ 𝑧 ∈ 𝐴)) → if(𝑎 ≤ 𝑏, 𝑎, 𝑏) ∈ ℝ)
62	56	3adant1 1146	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑎 ∈ ℝ⁺ ∧ 𝑏 ∈ ℝ⁺) → 𝑎 ∈ ℝ)
63	62	adantr 485	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑎 ∈ ℝ⁺ ∧ 𝑏 ∈ ℝ⁺) ∧ ((abs‘(𝑧 − 𝐵)) < if(𝑎 ≤ 𝑏, 𝑎, 𝑏) ∧ 𝑧 ∈ 𝐴)) → 𝑎 ∈ ℝ)
64		simprl 782	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑎 ∈ ℝ⁺ ∧ 𝑏 ∈ ℝ⁺) ∧ ((abs‘(𝑧 − 𝐵)) < if(𝑎 ≤ 𝑏, 𝑎, 𝑏) ∧ 𝑧 ∈ 𝐴)) → (abs‘(𝑧 − 𝐵)) < if(𝑎 ≤ 𝑏, 𝑎, 𝑏))
65	58	3adant1 1146	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑎 ∈ ℝ⁺ ∧ 𝑏 ∈ ℝ⁺) → 𝑏 ∈ ℝ)
66		min1 13215	. . . . . . . . . . . . . . . 16 ⊢ ((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) → if(𝑎 ≤ 𝑏, 𝑎, 𝑏) ≤ 𝑎)
67	62, 65, 66	syl2anc 595	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑎 ∈ ℝ⁺ ∧ 𝑏 ∈ ℝ⁺) → if(𝑎 ≤ 𝑏, 𝑎, 𝑏) ≤ 𝑎)
68	67	adantr 485	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑎 ∈ ℝ⁺ ∧ 𝑏 ∈ ℝ⁺) ∧ ((abs‘(𝑧 − 𝐵)) < if(𝑎 ≤ 𝑏, 𝑎, 𝑏) ∧ 𝑧 ∈ 𝐴)) → if(𝑎 ≤ 𝑏, 𝑎, 𝑏) ≤ 𝑎)
69	54, 61, 63, 64, 68	ltletrd 11370	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑎 ∈ ℝ⁺ ∧ 𝑏 ∈ ℝ⁺) ∧ ((abs‘(𝑧 − 𝐵)) < if(𝑎 ≤ 𝑏, 𝑎, 𝑏) ∧ 𝑧 ∈ 𝐴)) → (abs‘(𝑧 − 𝐵)) < 𝑎)
70	17, 43, 45, 46, 18, 69	syl32anc 1403	. . . . . . . . . . . 12 ⊢ ((((((((𝜑 ∧ 𝑥 ∈ ℝ⁺) ∧ 𝑎 ∈ ℝ⁺) ∧ ∀𝑧 ∈ (𝐴 ∩ (-∞(,)𝐵))((𝑧 ≠ 𝐵 ∧ (abs‘(𝑧 − 𝐵)) < 𝑎) → (abs‘(((𝐹 ↾ (-∞(,)𝐵))‘𝑧) − 𝐿)) < 𝑥)) ∧ 𝑏 ∈ ℝ⁺) ∧ ∀𝑧 ∈ (𝐴 ∩ (𝐵(,)+∞))((𝑧 ≠ 𝐵 ∧ (abs‘(𝑧 − 𝐵)) < 𝑏) → (abs‘(((𝐹 ↾ (𝐵(,)+∞))‘𝑧) − 𝐿)) < 𝑥)) ∧ 𝑧 ∈ 𝐴 ∧ (𝑧 ≠ 𝐵 ∧ (abs‘(𝑧 − 𝐵)) < if(𝑎 ≤ 𝑏, 𝑎, 𝑏))) ∧ 𝑧 < 𝐵) → (abs‘(𝑧 − 𝐵)) < 𝑎)
71	41, 70	jca 520	. . . . . . . . . . 11 ⊢ ((((((((𝜑 ∧ 𝑥 ∈ ℝ⁺) ∧ 𝑎 ∈ ℝ⁺) ∧ ∀𝑧 ∈ (𝐴 ∩ (-∞(,)𝐵))((𝑧 ≠ 𝐵 ∧ (abs‘(𝑧 − 𝐵)) < 𝑎) → (abs‘(((𝐹 ↾ (-∞(,)𝐵))‘𝑧) − 𝐿)) < 𝑥)) ∧ 𝑏 ∈ ℝ⁺) ∧ ∀𝑧 ∈ (𝐴 ∩ (𝐵(,)+∞))((𝑧 ≠ 𝐵 ∧ (abs‘(𝑧 − 𝐵)) < 𝑏) → (abs‘(((𝐹 ↾ (𝐵(,)+∞))‘𝑧) − 𝐿)) < 𝑥)) ∧ 𝑧 ∈ 𝐴 ∧ (𝑧 ≠ 𝐵 ∧ (abs‘(𝑧 − 𝐵)) < if(𝑎 ≤ 𝑏, 𝑎, 𝑏))) ∧ 𝑧 < 𝐵) → (𝑧 ≠ 𝐵 ∧ (abs‘(𝑧 − 𝐵)) < 𝑎))
72		rspa 3260	. . . . . . . . . . 11 ⊢ ((∀𝑧 ∈ (𝐴 ∩ (-∞(,)𝐵))((𝑧 ≠ 𝐵 ∧ (abs‘(𝑧 − 𝐵)) < 𝑎) → (abs‘(((𝐹 ↾ (-∞(,)𝐵))‘𝑧) − 𝐿)) < 𝑥) ∧ 𝑧 ∈ (𝐴 ∩ (-∞(,)𝐵))) → ((𝑧 ≠ 𝐵 ∧ (abs‘(𝑧 − 𝐵)) < 𝑎) → (abs‘(((𝐹 ↾ (-∞(,)𝐵))‘𝑧) − 𝐿)) < 𝑥))
73	40, 71, 72	sylc 66	. . . . . . . . . 10 ⊢ ((((((((𝜑 ∧ 𝑥 ∈ ℝ⁺) ∧ 𝑎 ∈ ℝ⁺) ∧ ∀𝑧 ∈ (𝐴 ∩ (-∞(,)𝐵))((𝑧 ≠ 𝐵 ∧ (abs‘(𝑧 − 𝐵)) < 𝑎) → (abs‘(((𝐹 ↾ (-∞(,)𝐵))‘𝑧) − 𝐿)) < 𝑥)) ∧ 𝑏 ∈ ℝ⁺) ∧ ∀𝑧 ∈ (𝐴 ∩ (𝐵(,)+∞))((𝑧 ≠ 𝐵 ∧ (abs‘(𝑧 − 𝐵)) < 𝑏) → (abs‘(((𝐹 ↾ (𝐵(,)+∞))‘𝑧) − 𝐿)) < 𝑥)) ∧ 𝑧 ∈ 𝐴 ∧ (𝑧 ≠ 𝐵 ∧ (abs‘(𝑧 − 𝐵)) < if(𝑎 ≤ 𝑏, 𝑎, 𝑏))) ∧ 𝑧 < 𝐵) → (abs‘(((𝐹 ↾ (-∞(,)𝐵))‘𝑧) − 𝐿)) < 𝑥)
74	36, 73	eqbrtrd 5137	. . . . . . . . 9 ⊢ ((((((((𝜑 ∧ 𝑥 ∈ ℝ⁺) ∧ 𝑎 ∈ ℝ⁺) ∧ ∀𝑧 ∈ (𝐴 ∩ (-∞(,)𝐵))((𝑧 ≠ 𝐵 ∧ (abs‘(𝑧 − 𝐵)) < 𝑎) → (abs‘(((𝐹 ↾ (-∞(,)𝐵))‘𝑧) − 𝐿)) < 𝑥)) ∧ 𝑏 ∈ ℝ⁺) ∧ ∀𝑧 ∈ (𝐴 ∩ (𝐵(,)+∞))((𝑧 ≠ 𝐵 ∧ (abs‘(𝑧 − 𝐵)) < 𝑏) → (abs‘(((𝐹 ↾ (𝐵(,)+∞))‘𝑧) − 𝐿)) < 𝑥)) ∧ 𝑧 ∈ 𝐴 ∧ (𝑧 ≠ 𝐵 ∧ (abs‘(𝑧 − 𝐵)) < if(𝑎 ≤ 𝑏, 𝑎, 𝑏))) ∧ 𝑧 < 𝐵) → (abs‘((𝐹‘𝑧) − 𝐿)) < 𝑥)
75		simp-6l 798	. . . . . . . . . . . . 13 ⊢ (((((((𝜑 ∧ 𝑥 ∈ ℝ⁺) ∧ 𝑎 ∈ ℝ⁺) ∧ ∀𝑧 ∈ (𝐴 ∩ (-∞(,)𝐵))((𝑧 ≠ 𝐵 ∧ (abs‘(𝑧 − 𝐵)) < 𝑎) → (abs‘(((𝐹 ↾ (-∞(,)𝐵))‘𝑧) − 𝐿)) < 𝑥)) ∧ 𝑏 ∈ ℝ⁺) ∧ ∀𝑧 ∈ (𝐴 ∩ (𝐵(,)+∞))((𝑧 ≠ 𝐵 ∧ (abs‘(𝑧 − 𝐵)) < 𝑏) → (abs‘(((𝐹 ↾ (𝐵(,)+∞))‘𝑧) − 𝐿)) < 𝑥)) ∧ ¬ 𝑧 < 𝐵) → 𝜑)
76	75	3ad2antl1 1202	. . . . . . . . . . . 12 ⊢ ((((((((𝜑 ∧ 𝑥 ∈ ℝ⁺) ∧ 𝑎 ∈ ℝ⁺) ∧ ∀𝑧 ∈ (𝐴 ∩ (-∞(,)𝐵))((𝑧 ≠ 𝐵 ∧ (abs‘(𝑧 − 𝐵)) < 𝑎) → (abs‘(((𝐹 ↾ (-∞(,)𝐵))‘𝑧) − 𝐿)) < 𝑥)) ∧ 𝑏 ∈ ℝ⁺) ∧ ∀𝑧 ∈ (𝐴 ∩ (𝐵(,)+∞))((𝑧 ≠ 𝐵 ∧ (abs‘(𝑧 − 𝐵)) < 𝑏) → (abs‘(((𝐹 ↾ (𝐵(,)+∞))‘𝑧) − 𝐿)) < 𝑥)) ∧ 𝑧 ∈ 𝐴 ∧ (𝑧 ≠ 𝐵 ∧ (abs‘(𝑧 − 𝐵)) < if(𝑎 ≤ 𝑏, 𝑎, 𝑏))) ∧ ¬ 𝑧 < 𝐵) → 𝜑)
77	76, 22	syl 18	. . . . . . . . . . 11 ⊢ ((((((((𝜑 ∧ 𝑥 ∈ ℝ⁺) ∧ 𝑎 ∈ ℝ⁺) ∧ ∀𝑧 ∈ (𝐴 ∩ (-∞(,)𝐵))((𝑧 ≠ 𝐵 ∧ (abs‘(𝑧 − 𝐵)) < 𝑎) → (abs‘(((𝐹 ↾ (-∞(,)𝐵))‘𝑧) − 𝐿)) < 𝑥)) ∧ 𝑏 ∈ ℝ⁺) ∧ ∀𝑧 ∈ (𝐴 ∩ (𝐵(,)+∞))((𝑧 ≠ 𝐵 ∧ (abs‘(𝑧 − 𝐵)) < 𝑏) → (abs‘(((𝐹 ↾ (𝐵(,)+∞))‘𝑧) − 𝐿)) < 𝑥)) ∧ 𝑧 ∈ 𝐴 ∧ (𝑧 ≠ 𝐵 ∧ (abs‘(𝑧 − 𝐵)) < if(𝑎 ≤ 𝑏, 𝑎, 𝑏))) ∧ ¬ 𝑧 < 𝐵) → 𝐵 ∈ ℝ)
78		simpl2 1209	. . . . . . . . . . . 12 ⊢ ((((((((𝜑 ∧ 𝑥 ∈ ℝ⁺) ∧ 𝑎 ∈ ℝ⁺) ∧ ∀𝑧 ∈ (𝐴 ∩ (-∞(,)𝐵))((𝑧 ≠ 𝐵 ∧ (abs‘(𝑧 − 𝐵)) < 𝑎) → (abs‘(((𝐹 ↾ (-∞(,)𝐵))‘𝑧) − 𝐿)) < 𝑥)) ∧ 𝑏 ∈ ℝ⁺) ∧ ∀𝑧 ∈ (𝐴 ∩ (𝐵(,)+∞))((𝑧 ≠ 𝐵 ∧ (abs‘(𝑧 − 𝐵)) < 𝑏) → (abs‘(((𝐹 ↾ (𝐵(,)+∞))‘𝑧) − 𝐿)) < 𝑥)) ∧ 𝑧 ∈ 𝐴 ∧ (𝑧 ≠ 𝐵 ∧ (abs‘(𝑧 − 𝐵)) < if(𝑎 ≤ 𝑏, 𝑎, 𝑏))) ∧ ¬ 𝑧 < 𝐵) → 𝑧 ∈ 𝐴)
79	76, 78, 26	syl2anc 595	. . . . . . . . . . 11 ⊢ ((((((((𝜑 ∧ 𝑥 ∈ ℝ⁺) ∧ 𝑎 ∈ ℝ⁺) ∧ ∀𝑧 ∈ (𝐴 ∩ (-∞(,)𝐵))((𝑧 ≠ 𝐵 ∧ (abs‘(𝑧 − 𝐵)) < 𝑎) → (abs‘(((𝐹 ↾ (-∞(,)𝐵))‘𝑧) − 𝐿)) < 𝑥)) ∧ 𝑏 ∈ ℝ⁺) ∧ ∀𝑧 ∈ (𝐴 ∩ (𝐵(,)+∞))((𝑧 ≠ 𝐵 ∧ (abs‘(𝑧 − 𝐵)) < 𝑏) → (abs‘(((𝐹 ↾ (𝐵(,)+∞))‘𝑧) − 𝐿)) < 𝑥)) ∧ 𝑧 ∈ 𝐴 ∧ (𝑧 ≠ 𝐵 ∧ (abs‘(𝑧 − 𝐵)) < if(𝑎 ≤ 𝑏, 𝑎, 𝑏))) ∧ ¬ 𝑧 < 𝐵) → 𝑧 ∈ ℝ)
80		id 23	. . . . . . . . . . . . . 14 ⊢ (𝑧 ≠ 𝐵 → 𝑧 ≠ 𝐵)
81	80	necomd 3019	. . . . . . . . . . . . 13 ⊢ (𝑧 ≠ 𝐵 → 𝐵 ≠ 𝑧)
82	81	ad2antrr 738	. . . . . . . . . . . 12 ⊢ (((𝑧 ≠ 𝐵 ∧ (abs‘(𝑧 − 𝐵)) < if(𝑎 ≤ 𝑏, 𝑎, 𝑏)) ∧ ¬ 𝑧 < 𝐵) → 𝐵 ≠ 𝑧)
83	82	3ad2antl3 1204	. . . . . . . . . . 11 ⊢ ((((((((𝜑 ∧ 𝑥 ∈ ℝ⁺) ∧ 𝑎 ∈ ℝ⁺) ∧ ∀𝑧 ∈ (𝐴 ∩ (-∞(,)𝐵))((𝑧 ≠ 𝐵 ∧ (abs‘(𝑧 − 𝐵)) < 𝑎) → (abs‘(((𝐹 ↾ (-∞(,)𝐵))‘𝑧) − 𝐿)) < 𝑥)) ∧ 𝑏 ∈ ℝ⁺) ∧ ∀𝑧 ∈ (𝐴 ∩ (𝐵(,)+∞))((𝑧 ≠ 𝐵 ∧ (abs‘(𝑧 − 𝐵)) < 𝑏) → (abs‘(((𝐹 ↾ (𝐵(,)+∞))‘𝑧) − 𝐿)) < 𝑥)) ∧ 𝑧 ∈ 𝐴 ∧ (𝑧 ≠ 𝐵 ∧ (abs‘(𝑧 − 𝐵)) < if(𝑎 ≤ 𝑏, 𝑎, 𝑏))) ∧ ¬ 𝑧 < 𝐵) → 𝐵 ≠ 𝑧)
84		simpr 489	. . . . . . . . . . 11 ⊢ ((((((((𝜑 ∧ 𝑥 ∈ ℝ⁺) ∧ 𝑎 ∈ ℝ⁺) ∧ ∀𝑧 ∈ (𝐴 ∩ (-∞(,)𝐵))((𝑧 ≠ 𝐵 ∧ (abs‘(𝑧 − 𝐵)) < 𝑎) → (abs‘(((𝐹 ↾ (-∞(,)𝐵))‘𝑧) − 𝐿)) < 𝑥)) ∧ 𝑏 ∈ ℝ⁺) ∧ ∀𝑧 ∈ (𝐴 ∩ (𝐵(,)+∞))((𝑧 ≠ 𝐵 ∧ (abs‘(𝑧 − 𝐵)) < 𝑏) → (abs‘(((𝐹 ↾ (𝐵(,)+∞))‘𝑧) − 𝐿)) < 𝑥)) ∧ 𝑧 ∈ 𝐴 ∧ (𝑧 ≠ 𝐵 ∧ (abs‘(𝑧 − 𝐵)) < if(𝑎 ≤ 𝑏, 𝑎, 𝑏))) ∧ ¬ 𝑧 < 𝐵) → ¬ 𝑧 < 𝐵)
85	77, 79, 83, 84	lttri5d 45910	. . . . . . . . . 10 ⊢ ((((((((𝜑 ∧ 𝑥 ∈ ℝ⁺) ∧ 𝑎 ∈ ℝ⁺) ∧ ∀𝑧 ∈ (𝐴 ∩ (-∞(,)𝐵))((𝑧 ≠ 𝐵 ∧ (abs‘(𝑧 − 𝐵)) < 𝑎) → (abs‘(((𝐹 ↾ (-∞(,)𝐵))‘𝑧) − 𝐿)) < 𝑥)) ∧ 𝑏 ∈ ℝ⁺) ∧ ∀𝑧 ∈ (𝐴 ∩ (𝐵(,)+∞))((𝑧 ≠ 𝐵 ∧ (abs‘(𝑧 − 𝐵)) < 𝑏) → (abs‘(((𝐹 ↾ (𝐵(,)+∞))‘𝑧) − 𝐿)) < 𝑥)) ∧ 𝑧 ∈ 𝐴 ∧ (𝑧 ≠ 𝐵 ∧ (abs‘(𝑧 − 𝐵)) < if(𝑎 ≤ 𝑏, 𝑎, 𝑏))) ∧ ¬ 𝑧 < 𝐵) → 𝐵 < 𝑧)
86		simp-6l 798	. . . . . . . . . . . . . 14 ⊢ (((((((𝜑 ∧ 𝑥 ∈ ℝ⁺) ∧ 𝑎 ∈ ℝ⁺) ∧ ∀𝑧 ∈ (𝐴 ∩ (-∞(,)𝐵))((𝑧 ≠ 𝐵 ∧ (abs‘(𝑧 − 𝐵)) < 𝑎) → (abs‘(((𝐹 ↾ (-∞(,)𝐵))‘𝑧) − 𝐿)) < 𝑥)) ∧ 𝑏 ∈ ℝ⁺) ∧ ∀𝑧 ∈ (𝐴 ∩ (𝐵(,)+∞))((𝑧 ≠ 𝐵 ∧ (abs‘(𝑧 − 𝐵)) < 𝑏) → (abs‘(((𝐹 ↾ (𝐵(,)+∞))‘𝑧) − 𝐿)) < 𝑥)) ∧ 𝐵 < 𝑧) → 𝜑)
87	86	3ad2antl1 1202	. . . . . . . . . . . . 13 ⊢ ((((((((𝜑 ∧ 𝑥 ∈ ℝ⁺) ∧ 𝑎 ∈ ℝ⁺) ∧ ∀𝑧 ∈ (𝐴 ∩ (-∞(,)𝐵))((𝑧 ≠ 𝐵 ∧ (abs‘(𝑧 − 𝐵)) < 𝑎) → (abs‘(((𝐹 ↾ (-∞(,)𝐵))‘𝑧) − 𝐿)) < 𝑥)) ∧ 𝑏 ∈ ℝ⁺) ∧ ∀𝑧 ∈ (𝐴 ∩ (𝐵(,)+∞))((𝑧 ≠ 𝐵 ∧ (abs‘(𝑧 − 𝐵)) < 𝑏) → (abs‘(((𝐹 ↾ (𝐵(,)+∞))‘𝑧) − 𝐿)) < 𝑥)) ∧ 𝑧 ∈ 𝐴 ∧ (𝑧 ≠ 𝐵 ∧ (abs‘(𝑧 − 𝐵)) < if(𝑎 ≤ 𝑏, 𝑎, 𝑏))) ∧ 𝐵 < 𝑧) → 𝜑)
88		simpl2 1209	. . . . . . . . . . . . 13 ⊢ ((((((((𝜑 ∧ 𝑥 ∈ ℝ⁺) ∧ 𝑎 ∈ ℝ⁺) ∧ ∀𝑧 ∈ (𝐴 ∩ (-∞(,)𝐵))((𝑧 ≠ 𝐵 ∧ (abs‘(𝑧 − 𝐵)) < 𝑎) → (abs‘(((𝐹 ↾ (-∞(,)𝐵))‘𝑧) − 𝐿)) < 𝑥)) ∧ 𝑏 ∈ ℝ⁺) ∧ ∀𝑧 ∈ (𝐴 ∩ (𝐵(,)+∞))((𝑧 ≠ 𝐵 ∧ (abs‘(𝑧 − 𝐵)) < 𝑏) → (abs‘(((𝐹 ↾ (𝐵(,)+∞))‘𝑧) − 𝐿)) < 𝑥)) ∧ 𝑧 ∈ 𝐴 ∧ (𝑧 ≠ 𝐵 ∧ (abs‘(𝑧 − 𝐵)) < if(𝑎 ≤ 𝑏, 𝑎, 𝑏))) ∧ 𝐵 < 𝑧) → 𝑧 ∈ 𝐴)
89		simpr 489	. . . . . . . . . . . . 13 ⊢ ((((((((𝜑 ∧ 𝑥 ∈ ℝ⁺) ∧ 𝑎 ∈ ℝ⁺) ∧ ∀𝑧 ∈ (𝐴 ∩ (-∞(,)𝐵))((𝑧 ≠ 𝐵 ∧ (abs‘(𝑧 − 𝐵)) < 𝑎) → (abs‘(((𝐹 ↾ (-∞(,)𝐵))‘𝑧) − 𝐿)) < 𝑥)) ∧ 𝑏 ∈ ℝ⁺) ∧ ∀𝑧 ∈ (𝐴 ∩ (𝐵(,)+∞))((𝑧 ≠ 𝐵 ∧ (abs‘(𝑧 − 𝐵)) < 𝑏) → (abs‘(((𝐹 ↾ (𝐵(,)+∞))‘𝑧) − 𝐿)) < 𝑥)) ∧ 𝑧 ∈ 𝐴 ∧ (𝑧 ≠ 𝐵 ∧ (abs‘(𝑧 − 𝐵)) < if(𝑎 ≤ 𝑏, 𝑎, 𝑏))) ∧ 𝐵 < 𝑧) → 𝐵 < 𝑧)
90	23	3ad2ant1 1149	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝐴 ∧ 𝐵 < 𝑧) → 𝐵 ∈ ℝ^*)
91		pnfxr 11263	. . . . . . . . . . . . . . 15 ⊢ +∞ ∈ ℝ^*
92	91	a1i 11	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝐴 ∧ 𝐵 < 𝑧) → +∞ ∈ ℝ^*)
93	26	3adant3 1148	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝐴 ∧ 𝐵 < 𝑧) → 𝑧 ∈ ℝ)
94		simp3 1154	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝐴 ∧ 𝐵 < 𝑧) → 𝐵 < 𝑧)
95	93	ltpnfd 13146	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝐴 ∧ 𝐵 < 𝑧) → 𝑧 < +∞)
96	90, 92, 93, 94, 95	eliood 46106	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝐴 ∧ 𝐵 < 𝑧) → 𝑧 ∈ (𝐵(,)+∞))
97	87, 88, 89, 96	syl3anc 1396	. . . . . . . . . . . 12 ⊢ ((((((((𝜑 ∧ 𝑥 ∈ ℝ⁺) ∧ 𝑎 ∈ ℝ⁺) ∧ ∀𝑧 ∈ (𝐴 ∩ (-∞(,)𝐵))((𝑧 ≠ 𝐵 ∧ (abs‘(𝑧 − 𝐵)) < 𝑎) → (abs‘(((𝐹 ↾ (-∞(,)𝐵))‘𝑧) − 𝐿)) < 𝑥)) ∧ 𝑏 ∈ ℝ⁺) ∧ ∀𝑧 ∈ (𝐴 ∩ (𝐵(,)+∞))((𝑧 ≠ 𝐵 ∧ (abs‘(𝑧 − 𝐵)) < 𝑏) → (abs‘(((𝐹 ↾ (𝐵(,)+∞))‘𝑧) − 𝐿)) < 𝑥)) ∧ 𝑧 ∈ 𝐴 ∧ (𝑧 ≠ 𝐵 ∧ (abs‘(𝑧 − 𝐵)) < if(𝑎 ≤ 𝑏, 𝑎, 𝑏))) ∧ 𝐵 < 𝑧) → 𝑧 ∈ (𝐵(,)+∞))
98		fvres 6901	. . . . . . . . . . . . . 14 ⊢ (𝑧 ∈ (𝐵(,)+∞) → ((𝐹 ↾ (𝐵(,)+∞))‘𝑧) = (𝐹‘𝑧))
99	98	eqcomd 2775	. . . . . . . . . . . . 13 ⊢ (𝑧 ∈ (𝐵(,)+∞) → (𝐹‘𝑧) = ((𝐹 ↾ (𝐵(,)+∞))‘𝑧))
100	99	fvoveq1d 7433	. . . . . . . . . . . 12 ⊢ (𝑧 ∈ (𝐵(,)+∞) → (abs‘((𝐹‘𝑧) − 𝐿)) = (abs‘(((𝐹 ↾ (𝐵(,)+∞))‘𝑧) − 𝐿)))
101	97, 100	syl 18	. . . . . . . . . . 11 ⊢ ((((((((𝜑 ∧ 𝑥 ∈ ℝ⁺) ∧ 𝑎 ∈ ℝ⁺) ∧ ∀𝑧 ∈ (𝐴 ∩ (-∞(,)𝐵))((𝑧 ≠ 𝐵 ∧ (abs‘(𝑧 − 𝐵)) < 𝑎) → (abs‘(((𝐹 ↾ (-∞(,)𝐵))‘𝑧) − 𝐿)) < 𝑥)) ∧ 𝑏 ∈ ℝ⁺) ∧ ∀𝑧 ∈ (𝐴 ∩ (𝐵(,)+∞))((𝑧 ≠ 𝐵 ∧ (abs‘(𝑧 − 𝐵)) < 𝑏) → (abs‘(((𝐹 ↾ (𝐵(,)+∞))‘𝑧) − 𝐿)) < 𝑥)) ∧ 𝑧 ∈ 𝐴 ∧ (𝑧 ≠ 𝐵 ∧ (abs‘(𝑧 − 𝐵)) < if(𝑎 ≤ 𝑏, 𝑎, 𝑏))) ∧ 𝐵 < 𝑧) → (abs‘((𝐹‘𝑧) − 𝐿)) = (abs‘(((𝐹 ↾ (𝐵(,)+∞))‘𝑧) − 𝐿)))
102		simpl1r 1242	. . . . . . . . . . . . 13 ⊢ ((((((((𝜑 ∧ 𝑥 ∈ ℝ⁺) ∧ 𝑎 ∈ ℝ⁺) ∧ ∀𝑧 ∈ (𝐴 ∩ (-∞(,)𝐵))((𝑧 ≠ 𝐵 ∧ (abs‘(𝑧 − 𝐵)) < 𝑎) → (abs‘(((𝐹 ↾ (-∞(,)𝐵))‘𝑧) − 𝐿)) < 𝑥)) ∧ 𝑏 ∈ ℝ⁺) ∧ ∀𝑧 ∈ (𝐴 ∩ (𝐵(,)+∞))((𝑧 ≠ 𝐵 ∧ (abs‘(𝑧 − 𝐵)) < 𝑏) → (abs‘(((𝐹 ↾ (𝐵(,)+∞))‘𝑧) − 𝐿)) < 𝑥)) ∧ 𝑧 ∈ 𝐴 ∧ (𝑧 ≠ 𝐵 ∧ (abs‘(𝑧 − 𝐵)) < if(𝑎 ≤ 𝑏, 𝑎, 𝑏))) ∧ 𝐵 < 𝑧) → ∀𝑧 ∈ (𝐴 ∩ (𝐵(,)+∞))((𝑧 ≠ 𝐵 ∧ (abs‘(𝑧 − 𝐵)) < 𝑏) → (abs‘(((𝐹 ↾ (𝐵(,)+∞))‘𝑧) − 𝐿)) < 𝑥))
103	88, 97	elind 4161	. . . . . . . . . . . . 13 ⊢ ((((((((𝜑 ∧ 𝑥 ∈ ℝ⁺) ∧ 𝑎 ∈ ℝ⁺) ∧ ∀𝑧 ∈ (𝐴 ∩ (-∞(,)𝐵))((𝑧 ≠ 𝐵 ∧ (abs‘(𝑧 − 𝐵)) < 𝑎) → (abs‘(((𝐹 ↾ (-∞(,)𝐵))‘𝑧) − 𝐿)) < 𝑥)) ∧ 𝑏 ∈ ℝ⁺) ∧ ∀𝑧 ∈ (𝐴 ∩ (𝐵(,)+∞))((𝑧 ≠ 𝐵 ∧ (abs‘(𝑧 − 𝐵)) < 𝑏) → (abs‘(((𝐹 ↾ (𝐵(,)+∞))‘𝑧) − 𝐿)) < 𝑥)) ∧ 𝑧 ∈ 𝐴 ∧ (𝑧 ≠ 𝐵 ∧ (abs‘(𝑧 − 𝐵)) < if(𝑎 ≤ 𝑏, 𝑎, 𝑏))) ∧ 𝐵 < 𝑧) → 𝑧 ∈ (𝐴 ∩ (𝐵(,)+∞)))
104	102, 103	jca 520	. . . . . . . . . . . 12 ⊢ ((((((((𝜑 ∧ 𝑥 ∈ ℝ⁺) ∧ 𝑎 ∈ ℝ⁺) ∧ ∀𝑧 ∈ (𝐴 ∩ (-∞(,)𝐵))((𝑧 ≠ 𝐵 ∧ (abs‘(𝑧 − 𝐵)) < 𝑎) → (abs‘(((𝐹 ↾ (-∞(,)𝐵))‘𝑧) − 𝐿)) < 𝑥)) ∧ 𝑏 ∈ ℝ⁺) ∧ ∀𝑧 ∈ (𝐴 ∩ (𝐵(,)+∞))((𝑧 ≠ 𝐵 ∧ (abs‘(𝑧 − 𝐵)) < 𝑏) → (abs‘(((𝐹 ↾ (𝐵(,)+∞))‘𝑧) − 𝐿)) < 𝑥)) ∧ 𝑧 ∈ 𝐴 ∧ (𝑧 ≠ 𝐵 ∧ (abs‘(𝑧 − 𝐵)) < if(𝑎 ≤ 𝑏, 𝑎, 𝑏))) ∧ 𝐵 < 𝑧) → (∀𝑧 ∈ (𝐴 ∩ (𝐵(,)+∞))((𝑧 ≠ 𝐵 ∧ (abs‘(𝑧 − 𝐵)) < 𝑏) → (abs‘(((𝐹 ↾ (𝐵(,)+∞))‘𝑧) − 𝐿)) < 𝑥) ∧ 𝑧 ∈ (𝐴 ∩ (𝐵(,)+∞))))
105		simpl3l 1245	. . . . . . . . . . . . 13 ⊢ ((((((((𝜑 ∧ 𝑥 ∈ ℝ⁺) ∧ 𝑎 ∈ ℝ⁺) ∧ ∀𝑧 ∈ (𝐴 ∩ (-∞(,)𝐵))((𝑧 ≠ 𝐵 ∧ (abs‘(𝑧 − 𝐵)) < 𝑎) → (abs‘(((𝐹 ↾ (-∞(,)𝐵))‘𝑧) − 𝐿)) < 𝑥)) ∧ 𝑏 ∈ ℝ⁺) ∧ ∀𝑧 ∈ (𝐴 ∩ (𝐵(,)+∞))((𝑧 ≠ 𝐵 ∧ (abs‘(𝑧 − 𝐵)) < 𝑏) → (abs‘(((𝐹 ↾ (𝐵(,)+∞))‘𝑧) − 𝐿)) < 𝑥)) ∧ 𝑧 ∈ 𝐴 ∧ (𝑧 ≠ 𝐵 ∧ (abs‘(𝑧 − 𝐵)) < if(𝑎 ≤ 𝑏, 𝑎, 𝑏))) ∧ 𝐵 < 𝑧) → 𝑧 ≠ 𝐵)
106	4	adantr 485	. . . . . . . . . . . . . . 15 ⊢ (((((((𝜑 ∧ 𝑥 ∈ ℝ⁺) ∧ 𝑎 ∈ ℝ⁺) ∧ ∀𝑧 ∈ (𝐴 ∩ (-∞(,)𝐵))((𝑧 ≠ 𝐵 ∧ (abs‘(𝑧 − 𝐵)) < 𝑎) → (abs‘(((𝐹 ↾ (-∞(,)𝐵))‘𝑧) − 𝐿)) < 𝑥)) ∧ 𝑏 ∈ ℝ⁺) ∧ ∀𝑧 ∈ (𝐴 ∩ (𝐵(,)+∞))((𝑧 ≠ 𝐵 ∧ (abs‘(𝑧 − 𝐵)) < 𝑏) → (abs‘(((𝐹 ↾ (𝐵(,)+∞))‘𝑧) − 𝐿)) < 𝑥)) ∧ 𝐵 < 𝑧) → 𝑎 ∈ ℝ⁺)
107	106	3ad2antl1 1202	. . . . . . . . . . . . . 14 ⊢ ((((((((𝜑 ∧ 𝑥 ∈ ℝ⁺) ∧ 𝑎 ∈ ℝ⁺) ∧ ∀𝑧 ∈ (𝐴 ∩ (-∞(,)𝐵))((𝑧 ≠ 𝐵 ∧ (abs‘(𝑧 − 𝐵)) < 𝑎) → (abs‘(((𝐹 ↾ (-∞(,)𝐵))‘𝑧) − 𝐿)) < 𝑥)) ∧ 𝑏 ∈ ℝ⁺) ∧ ∀𝑧 ∈ (𝐴 ∩ (𝐵(,)+∞))((𝑧 ≠ 𝐵 ∧ (abs‘(𝑧 − 𝐵)) < 𝑏) → (abs‘(((𝐹 ↾ (𝐵(,)+∞))‘𝑧) − 𝐿)) < 𝑥)) ∧ 𝑧 ∈ 𝐴 ∧ (𝑧 ≠ 𝐵 ∧ (abs‘(𝑧 − 𝐵)) < if(𝑎 ≤ 𝑏, 𝑎, 𝑏))) ∧ 𝐵 < 𝑧) → 𝑎 ∈ ℝ⁺)
108	5	adantr 485	. . . . . . . . . . . . . . 15 ⊢ (((((((𝜑 ∧ 𝑥 ∈ ℝ⁺) ∧ 𝑎 ∈ ℝ⁺) ∧ ∀𝑧 ∈ (𝐴 ∩ (-∞(,)𝐵))((𝑧 ≠ 𝐵 ∧ (abs‘(𝑧 − 𝐵)) < 𝑎) → (abs‘(((𝐹 ↾ (-∞(,)𝐵))‘𝑧) − 𝐿)) < 𝑥)) ∧ 𝑏 ∈ ℝ⁺) ∧ ∀𝑧 ∈ (𝐴 ∩ (𝐵(,)+∞))((𝑧 ≠ 𝐵 ∧ (abs‘(𝑧 − 𝐵)) < 𝑏) → (abs‘(((𝐹 ↾ (𝐵(,)+∞))‘𝑧) − 𝐿)) < 𝑥)) ∧ 𝐵 < 𝑧) → 𝑏 ∈ ℝ⁺)
109	108	3ad2antl1 1202	. . . . . . . . . . . . . 14 ⊢ ((((((((𝜑 ∧ 𝑥 ∈ ℝ⁺) ∧ 𝑎 ∈ ℝ⁺) ∧ ∀𝑧 ∈ (𝐴 ∩ (-∞(,)𝐵))((𝑧 ≠ 𝐵 ∧ (abs‘(𝑧 − 𝐵)) < 𝑎) → (abs‘(((𝐹 ↾ (-∞(,)𝐵))‘𝑧) − 𝐿)) < 𝑥)) ∧ 𝑏 ∈ ℝ⁺) ∧ ∀𝑧 ∈ (𝐴 ∩ (𝐵(,)+∞))((𝑧 ≠ 𝐵 ∧ (abs‘(𝑧 − 𝐵)) < 𝑏) → (abs‘(((𝐹 ↾ (𝐵(,)+∞))‘𝑧) − 𝐿)) < 𝑥)) ∧ 𝑧 ∈ 𝐴 ∧ (𝑧 ≠ 𝐵 ∧ (abs‘(𝑧 − 𝐵)) < if(𝑎 ≤ 𝑏, 𝑎, 𝑏))) ∧ 𝐵 < 𝑧) → 𝑏 ∈ ℝ⁺)
110		simpl3r 1246	. . . . . . . . . . . . . 14 ⊢ ((((((((𝜑 ∧ 𝑥 ∈ ℝ⁺) ∧ 𝑎 ∈ ℝ⁺) ∧ ∀𝑧 ∈ (𝐴 ∩ (-∞(,)𝐵))((𝑧 ≠ 𝐵 ∧ (abs‘(𝑧 − 𝐵)) < 𝑎) → (abs‘(((𝐹 ↾ (-∞(,)𝐵))‘𝑧) − 𝐿)) < 𝑥)) ∧ 𝑏 ∈ ℝ⁺) ∧ ∀𝑧 ∈ (𝐴 ∩ (𝐵(,)+∞))((𝑧 ≠ 𝐵 ∧ (abs‘(𝑧 − 𝐵)) < 𝑏) → (abs‘(((𝐹 ↾ (𝐵(,)+∞))‘𝑧) − 𝐿)) < 𝑥)) ∧ 𝑧 ∈ 𝐴 ∧ (𝑧 ≠ 𝐵 ∧ (abs‘(𝑧 − 𝐵)) < if(𝑎 ≤ 𝑏, 𝑎, 𝑏))) ∧ 𝐵 < 𝑧) → (abs‘(𝑧 − 𝐵)) < if(𝑎 ≤ 𝑏, 𝑎, 𝑏))
111	65	adantr 485	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑎 ∈ ℝ⁺ ∧ 𝑏 ∈ ℝ⁺) ∧ ((abs‘(𝑧 − 𝐵)) < if(𝑎 ≤ 𝑏, 𝑎, 𝑏) ∧ 𝑧 ∈ 𝐴)) → 𝑏 ∈ ℝ)
112		min2 13216	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) → if(𝑎 ≤ 𝑏, 𝑎, 𝑏) ≤ 𝑏)
113	62, 65, 112	syl2anc 595	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑎 ∈ ℝ⁺ ∧ 𝑏 ∈ ℝ⁺) → if(𝑎 ≤ 𝑏, 𝑎, 𝑏) ≤ 𝑏)
114	113	adantr 485	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑎 ∈ ℝ⁺ ∧ 𝑏 ∈ ℝ⁺) ∧ ((abs‘(𝑧 − 𝐵)) < if(𝑎 ≤ 𝑏, 𝑎, 𝑏) ∧ 𝑧 ∈ 𝐴)) → if(𝑎 ≤ 𝑏, 𝑎, 𝑏) ≤ 𝑏)
115	54, 61, 111, 64, 114	ltletrd 11370	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑎 ∈ ℝ⁺ ∧ 𝑏 ∈ ℝ⁺) ∧ ((abs‘(𝑧 − 𝐵)) < if(𝑎 ≤ 𝑏, 𝑎, 𝑏) ∧ 𝑧 ∈ 𝐴)) → (abs‘(𝑧 − 𝐵)) < 𝑏)
116	87, 107, 109, 110, 88, 115	syl32anc 1403	. . . . . . . . . . . . 13 ⊢ ((((((((𝜑 ∧ 𝑥 ∈ ℝ⁺) ∧ 𝑎 ∈ ℝ⁺) ∧ ∀𝑧 ∈ (𝐴 ∩ (-∞(,)𝐵))((𝑧 ≠ 𝐵 ∧ (abs‘(𝑧 − 𝐵)) < 𝑎) → (abs‘(((𝐹 ↾ (-∞(,)𝐵))‘𝑧) − 𝐿)) < 𝑥)) ∧ 𝑏 ∈ ℝ⁺) ∧ ∀𝑧 ∈ (𝐴 ∩ (𝐵(,)+∞))((𝑧 ≠ 𝐵 ∧ (abs‘(𝑧 − 𝐵)) < 𝑏) → (abs‘(((𝐹 ↾ (𝐵(,)+∞))‘𝑧) − 𝐿)) < 𝑥)) ∧ 𝑧 ∈ 𝐴 ∧ (𝑧 ≠ 𝐵 ∧ (abs‘(𝑧 − 𝐵)) < if(𝑎 ≤ 𝑏, 𝑎, 𝑏))) ∧ 𝐵 < 𝑧) → (abs‘(𝑧 − 𝐵)) < 𝑏)
117	105, 116	jca 520	. . . . . . . . . . . 12 ⊢ ((((((((𝜑 ∧ 𝑥 ∈ ℝ⁺) ∧ 𝑎 ∈ ℝ⁺) ∧ ∀𝑧 ∈ (𝐴 ∩ (-∞(,)𝐵))((𝑧 ≠ 𝐵 ∧ (abs‘(𝑧 − 𝐵)) < 𝑎) → (abs‘(((𝐹 ↾ (-∞(,)𝐵))‘𝑧) − 𝐿)) < 𝑥)) ∧ 𝑏 ∈ ℝ⁺) ∧ ∀𝑧 ∈ (𝐴 ∩ (𝐵(,)+∞))((𝑧 ≠ 𝐵 ∧ (abs‘(𝑧 − 𝐵)) < 𝑏) → (abs‘(((𝐹 ↾ (𝐵(,)+∞))‘𝑧) − 𝐿)) < 𝑥)) ∧ 𝑧 ∈ 𝐴 ∧ (𝑧 ≠ 𝐵 ∧ (abs‘(𝑧 − 𝐵)) < if(𝑎 ≤ 𝑏, 𝑎, 𝑏))) ∧ 𝐵 < 𝑧) → (𝑧 ≠ 𝐵 ∧ (abs‘(𝑧 − 𝐵)) < 𝑏))
118		rspa 3260	. . . . . . . . . . . 12 ⊢ ((∀𝑧 ∈ (𝐴 ∩ (𝐵(,)+∞))((𝑧 ≠ 𝐵 ∧ (abs‘(𝑧 − 𝐵)) < 𝑏) → (abs‘(((𝐹 ↾ (𝐵(,)+∞))‘𝑧) − 𝐿)) < 𝑥) ∧ 𝑧 ∈ (𝐴 ∩ (𝐵(,)+∞))) → ((𝑧 ≠ 𝐵 ∧ (abs‘(𝑧 − 𝐵)) < 𝑏) → (abs‘(((𝐹 ↾ (𝐵(,)+∞))‘𝑧) − 𝐿)) < 𝑥))
119	104, 117, 118	sylc 66	. . . . . . . . . . 11 ⊢ ((((((((𝜑 ∧ 𝑥 ∈ ℝ⁺) ∧ 𝑎 ∈ ℝ⁺) ∧ ∀𝑧 ∈ (𝐴 ∩ (-∞(,)𝐵))((𝑧 ≠ 𝐵 ∧ (abs‘(𝑧 − 𝐵)) < 𝑎) → (abs‘(((𝐹 ↾ (-∞(,)𝐵))‘𝑧) − 𝐿)) < 𝑥)) ∧ 𝑏 ∈ ℝ⁺) ∧ ∀𝑧 ∈ (𝐴 ∩ (𝐵(,)+∞))((𝑧 ≠ 𝐵 ∧ (abs‘(𝑧 − 𝐵)) < 𝑏) → (abs‘(((𝐹 ↾ (𝐵(,)+∞))‘𝑧) − 𝐿)) < 𝑥)) ∧ 𝑧 ∈ 𝐴 ∧ (𝑧 ≠ 𝐵 ∧ (abs‘(𝑧 − 𝐵)) < if(𝑎 ≤ 𝑏, 𝑎, 𝑏))) ∧ 𝐵 < 𝑧) → (abs‘(((𝐹 ↾ (𝐵(,)+∞))‘𝑧) − 𝐿)) < 𝑥)
120	101, 119	eqbrtrd 5137	. . . . . . . . . 10 ⊢ ((((((((𝜑 ∧ 𝑥 ∈ ℝ⁺) ∧ 𝑎 ∈ ℝ⁺) ∧ ∀𝑧 ∈ (𝐴 ∩ (-∞(,)𝐵))((𝑧 ≠ 𝐵 ∧ (abs‘(𝑧 − 𝐵)) < 𝑎) → (abs‘(((𝐹 ↾ (-∞(,)𝐵))‘𝑧) − 𝐿)) < 𝑥)) ∧ 𝑏 ∈ ℝ⁺) ∧ ∀𝑧 ∈ (𝐴 ∩ (𝐵(,)+∞))((𝑧 ≠ 𝐵 ∧ (abs‘(𝑧 − 𝐵)) < 𝑏) → (abs‘(((𝐹 ↾ (𝐵(,)+∞))‘𝑧) − 𝐿)) < 𝑥)) ∧ 𝑧 ∈ 𝐴 ∧ (𝑧 ≠ 𝐵 ∧ (abs‘(𝑧 − 𝐵)) < if(𝑎 ≤ 𝑏, 𝑎, 𝑏))) ∧ 𝐵 < 𝑧) → (abs‘((𝐹‘𝑧) − 𝐿)) < 𝑥)
121	85, 120	syldan 602	. . . . . . . . 9 ⊢ ((((((((𝜑 ∧ 𝑥 ∈ ℝ⁺) ∧ 𝑎 ∈ ℝ⁺) ∧ ∀𝑧 ∈ (𝐴 ∩ (-∞(,)𝐵))((𝑧 ≠ 𝐵 ∧ (abs‘(𝑧 − 𝐵)) < 𝑎) → (abs‘(((𝐹 ↾ (-∞(,)𝐵))‘𝑧) − 𝐿)) < 𝑥)) ∧ 𝑏 ∈ ℝ⁺) ∧ ∀𝑧 ∈ (𝐴 ∩ (𝐵(,)+∞))((𝑧 ≠ 𝐵 ∧ (abs‘(𝑧 − 𝐵)) < 𝑏) → (abs‘(((𝐹 ↾ (𝐵(,)+∞))‘𝑧) − 𝐿)) < 𝑥)) ∧ 𝑧 ∈ 𝐴 ∧ (𝑧 ≠ 𝐵 ∧ (abs‘(𝑧 − 𝐵)) < if(𝑎 ≤ 𝑏, 𝑎, 𝑏))) ∧ ¬ 𝑧 < 𝐵) → (abs‘((𝐹‘𝑧) − 𝐿)) < 𝑥)
122	74, 121	pm2.61dan 824	. . . . . . . 8 ⊢ (((((((𝜑 ∧ 𝑥 ∈ ℝ⁺) ∧ 𝑎 ∈ ℝ⁺) ∧ ∀𝑧 ∈ (𝐴 ∩ (-∞(,)𝐵))((𝑧 ≠ 𝐵 ∧ (abs‘(𝑧 − 𝐵)) < 𝑎) → (abs‘(((𝐹 ↾ (-∞(,)𝐵))‘𝑧) − 𝐿)) < 𝑥)) ∧ 𝑏 ∈ ℝ⁺) ∧ ∀𝑧 ∈ (𝐴 ∩ (𝐵(,)+∞))((𝑧 ≠ 𝐵 ∧ (abs‘(𝑧 − 𝐵)) < 𝑏) → (abs‘(((𝐹 ↾ (𝐵(,)+∞))‘𝑧) − 𝐿)) < 𝑥)) ∧ 𝑧 ∈ 𝐴 ∧ (𝑧 ≠ 𝐵 ∧ (abs‘(𝑧 − 𝐵)) < if(𝑎 ≤ 𝑏, 𝑎, 𝑏))) → (abs‘((𝐹‘𝑧) − 𝐿)) < 𝑥)
123	122	3exp 1135	. . . . . . 7 ⊢ ((((((𝜑 ∧ 𝑥 ∈ ℝ⁺) ∧ 𝑎 ∈ ℝ⁺) ∧ ∀𝑧 ∈ (𝐴 ∩ (-∞(,)𝐵))((𝑧 ≠ 𝐵 ∧ (abs‘(𝑧 − 𝐵)) < 𝑎) → (abs‘(((𝐹 ↾ (-∞(,)𝐵))‘𝑧) − 𝐿)) < 𝑥)) ∧ 𝑏 ∈ ℝ⁺) ∧ ∀𝑧 ∈ (𝐴 ∩ (𝐵(,)+∞))((𝑧 ≠ 𝐵 ∧ (abs‘(𝑧 − 𝐵)) < 𝑏) → (abs‘(((𝐹 ↾ (𝐵(,)+∞))‘𝑧) − 𝐿)) < 𝑥)) → (𝑧 ∈ 𝐴 → ((𝑧 ≠ 𝐵 ∧ (abs‘(𝑧 − 𝐵)) < if(𝑎 ≤ 𝑏, 𝑎, 𝑏)) → (abs‘((𝐹‘𝑧) − 𝐿)) < 𝑥)))
124	15, 123	ralrimi 3269	. . . . . 6 ⊢ ((((((𝜑 ∧ 𝑥 ∈ ℝ⁺) ∧ 𝑎 ∈ ℝ⁺) ∧ ∀𝑧 ∈ (𝐴 ∩ (-∞(,)𝐵))((𝑧 ≠ 𝐵 ∧ (abs‘(𝑧 − 𝐵)) < 𝑎) → (abs‘(((𝐹 ↾ (-∞(,)𝐵))‘𝑧) − 𝐿)) < 𝑥)) ∧ 𝑏 ∈ ℝ⁺) ∧ ∀𝑧 ∈ (𝐴 ∩ (𝐵(,)+∞))((𝑧 ≠ 𝐵 ∧ (abs‘(𝑧 − 𝐵)) < 𝑏) → (abs‘(((𝐹 ↾ (𝐵(,)+∞))‘𝑧) − 𝐿)) < 𝑥)) → ∀𝑧 ∈ 𝐴 ((𝑧 ≠ 𝐵 ∧ (abs‘(𝑧 − 𝐵)) < if(𝑎 ≤ 𝑏, 𝑎, 𝑏)) → (abs‘((𝐹‘𝑧) − 𝐿)) < 𝑥))
125		brimralrspcev 5176	. . . . . 6 ⊢ ((if(𝑎 ≤ 𝑏, 𝑎, 𝑏) ∈ ℝ⁺ ∧ ∀𝑧 ∈ 𝐴 ((𝑧 ≠ 𝐵 ∧ (abs‘(𝑧 − 𝐵)) < if(𝑎 ≤ 𝑏, 𝑎, 𝑏)) → (abs‘((𝐹‘𝑧) − 𝐿)) < 𝑥)) → ∃𝑦 ∈ ℝ⁺ ∀𝑧 ∈ 𝐴 ((𝑧 ≠ 𝐵 ∧ (abs‘(𝑧 − 𝐵)) < 𝑦) → (abs‘((𝐹‘𝑧) − 𝐿)) < 𝑥))
126	6, 124, 125	syl2anc 595	. . . . 5 ⊢ ((((((𝜑 ∧ 𝑥 ∈ ℝ⁺) ∧ 𝑎 ∈ ℝ⁺) ∧ ∀𝑧 ∈ (𝐴 ∩ (-∞(,)𝐵))((𝑧 ≠ 𝐵 ∧ (abs‘(𝑧 − 𝐵)) < 𝑎) → (abs‘(((𝐹 ↾ (-∞(,)𝐵))‘𝑧) − 𝐿)) < 𝑥)) ∧ 𝑏 ∈ ℝ⁺) ∧ ∀𝑧 ∈ (𝐴 ∩ (𝐵(,)+∞))((𝑧 ≠ 𝐵 ∧ (abs‘(𝑧 − 𝐵)) < 𝑏) → (abs‘(((𝐹 ↾ (𝐵(,)+∞))‘𝑧) − 𝐿)) < 𝑥)) → ∃𝑦 ∈ ℝ⁺ ∀𝑧 ∈ 𝐴 ((𝑧 ≠ 𝐵 ∧ (abs‘(𝑧 − 𝐵)) < 𝑦) → (abs‘((𝐹‘𝑧) − 𝐿)) < 𝑥))
127		limcleqr.r	. . . . . . . . . 10 ⊢ (𝜑 → 𝑅 ∈ ((𝐹 ↾ (𝐵(,)+∞)) lim_ℂ 𝐵))
128		limcleqr.f	. . . . . . . . . . . 12 ⊢ (𝜑 → 𝐹:𝐴⟶ℂ)
129		fresin 6748	. . . . . . . . . . . 12 ⊢ (𝐹:𝐴⟶ℂ → (𝐹 ↾ (𝐵(,)+∞)):(𝐴 ∩ (𝐵(,)+∞))⟶ℂ)
130	128, 129	syl 18	. . . . . . . . . . 11 ⊢ (𝜑 → (𝐹 ↾ (𝐵(,)+∞)):(𝐴 ∩ (𝐵(,)+∞))⟶ℂ)
131		inss2 4198	. . . . . . . . . . . . 13 ⊢ (𝐴 ∩ (𝐵(,)+∞)) ⊆ (𝐵(,)+∞)
132		ioosscn 13435	. . . . . . . . . . . . 13 ⊢ (𝐵(,)+∞) ⊆ ℂ
133	131, 132	sstri 3954	. . . . . . . . . . . 12 ⊢ (𝐴 ∩ (𝐵(,)+∞)) ⊆ ℂ
134	133	a1i 11	. . . . . . . . . . 11 ⊢ (𝜑 → (𝐴 ∩ (𝐵(,)+∞)) ⊆ ℂ)
135	130, 134, 50	ellimc3 26007	. . . . . . . . . 10 ⊢ (𝜑 → (𝑅 ∈ ((𝐹 ↾ (𝐵(,)+∞)) lim_ℂ 𝐵) ↔ (𝑅 ∈ ℂ ∧ ∀𝑥 ∈ ℝ⁺ ∃𝑏 ∈ ℝ⁺ ∀𝑧 ∈ (𝐴 ∩ (𝐵(,)+∞))((𝑧 ≠ 𝐵 ∧ (abs‘(𝑧 − 𝐵)) < 𝑏) → (abs‘(((𝐹 ↾ (𝐵(,)+∞))‘𝑧) − 𝑅)) < 𝑥))))
136	127, 135	mpbid 235	. . . . . . . . 9 ⊢ (𝜑 → (𝑅 ∈ ℂ ∧ ∀𝑥 ∈ ℝ⁺ ∃𝑏 ∈ ℝ⁺ ∀𝑧 ∈ (𝐴 ∩ (𝐵(,)+∞))((𝑧 ≠ 𝐵 ∧ (abs‘(𝑧 − 𝐵)) < 𝑏) → (abs‘(((𝐹 ↾ (𝐵(,)+∞))‘𝑧) − 𝑅)) < 𝑥)))
137	136	simprd 500	. . . . . . . 8 ⊢ (𝜑 → ∀𝑥 ∈ ℝ⁺ ∃𝑏 ∈ ℝ⁺ ∀𝑧 ∈ (𝐴 ∩ (𝐵(,)+∞))((𝑧 ≠ 𝐵 ∧ (abs‘(𝑧 − 𝐵)) < 𝑏) → (abs‘(((𝐹 ↾ (𝐵(,)+∞))‘𝑧) − 𝑅)) < 𝑥))
138	137	r19.21bi 3263	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ⁺) → ∃𝑏 ∈ ℝ⁺ ∀𝑧 ∈ (𝐴 ∩ (𝐵(,)+∞))((𝑧 ≠ 𝐵 ∧ (abs‘(𝑧 − 𝐵)) < 𝑏) → (abs‘(((𝐹 ↾ (𝐵(,)+∞))‘𝑧) − 𝑅)) < 𝑥))
139		limcleqr.leqr	. . . . . . . . . . . . 13 ⊢ (𝜑 → 𝐿 = 𝑅)
140	139	oveq2d 7427	. . . . . . . . . . . 12 ⊢ (𝜑 → (((𝐹 ↾ (𝐵(,)+∞))‘𝑧) − 𝐿) = (((𝐹 ↾ (𝐵(,)+∞))‘𝑧) − 𝑅))
141	140	fveq2d 6886	. . . . . . . . . . 11 ⊢ (𝜑 → (abs‘(((𝐹 ↾ (𝐵(,)+∞))‘𝑧) − 𝐿)) = (abs‘(((𝐹 ↾ (𝐵(,)+∞))‘𝑧) − 𝑅)))
142	141	breq1d 5123	. . . . . . . . . 10 ⊢ (𝜑 → ((abs‘(((𝐹 ↾ (𝐵(,)+∞))‘𝑧) − 𝐿)) < 𝑥 ↔ (abs‘(((𝐹 ↾ (𝐵(,)+∞))‘𝑧) − 𝑅)) < 𝑥))
143	142	imbi2d 343	. . . . . . . . 9 ⊢ (𝜑 → (((𝑧 ≠ 𝐵 ∧ (abs‘(𝑧 − 𝐵)) < 𝑏) → (abs‘(((𝐹 ↾ (𝐵(,)+∞))‘𝑧) − 𝐿)) < 𝑥) ↔ ((𝑧 ≠ 𝐵 ∧ (abs‘(𝑧 − 𝐵)) < 𝑏) → (abs‘(((𝐹 ↾ (𝐵(,)+∞))‘𝑧) − 𝑅)) < 𝑥)))
144	143	rexralbidv 3237	. . . . . . . 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 738	. . . . 5 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ⁺) ∧ 𝑎 ∈ ℝ⁺) ∧ ∀𝑧 ∈ (𝐴 ∩ (-∞(,)𝐵))((𝑧 ≠ 𝐵 ∧ (abs‘(𝑧 − 𝐵)) < 𝑎) → (abs‘(((𝐹 ↾ (-∞(,)𝐵))‘𝑧) − 𝐿)) < 𝑥)) → ∃𝑏 ∈ ℝ⁺ ∀𝑧 ∈ (𝐴 ∩ (𝐵(,)+∞))((𝑧 ≠ 𝐵 ∧ (abs‘(𝑧 − 𝐵)) < 𝑏) → (abs‘(((𝐹 ↾ (𝐵(,)+∞))‘𝑧) − 𝐿)) < 𝑥))
148	126, 147	r19.29a 3179	. . . 4 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ⁺) ∧ 𝑎 ∈ ℝ⁺) ∧ ∀𝑧 ∈ (𝐴 ∩ (-∞(,)𝐵))((𝑧 ≠ 𝐵 ∧ (abs‘(𝑧 − 𝐵)) < 𝑎) → (abs‘(((𝐹 ↾ (-∞(,)𝐵))‘𝑧) − 𝐿)) < 𝑥)) → ∃𝑦 ∈ ℝ⁺ ∀𝑧 ∈ 𝐴 ((𝑧 ≠ 𝐵 ∧ (abs‘(𝑧 − 𝐵)) < 𝑦) → (abs‘((𝐹‘𝑧) − 𝐿)) < 𝑥))
149		fresin 6748	. . . . . . . . 9 ⊢ (𝐹:𝐴⟶ℂ → (𝐹 ↾ (-∞(,)𝐵)):(𝐴 ∩ (-∞(,)𝐵))⟶ℂ)
150	128, 149	syl 18	. . . . . . . 8 ⊢ (𝜑 → (𝐹 ↾ (-∞(,)𝐵)):(𝐴 ∩ (-∞(,)𝐵))⟶ℂ)
151		inss2 4198	. . . . . . . . . 10 ⊢ (𝐴 ∩ (-∞(,)𝐵)) ⊆ (-∞(,)𝐵)
152		ioossre 13434	. . . . . . . . . 10 ⊢ (-∞(,)𝐵) ⊆ ℝ
153	151, 152	sstri 3954	. . . . . . . . 9 ⊢ (𝐴 ∩ (-∞(,)𝐵)) ⊆ ℝ
154		ax-resscn 11157	. . . . . . . . . 10 ⊢ ℝ ⊆ ℂ
155	154	a1i 11	. . . . . . . . 9 ⊢ (𝜑 → ℝ ⊆ ℂ)
156	153, 155	sstrid 3956	. . . . . . . 8 ⊢ (𝜑 → (𝐴 ∩ (-∞(,)𝐵)) ⊆ ℂ)
157	150, 156, 50	ellimc3 26007	. . . . . . 7 ⊢ (𝜑 → (𝐿 ∈ ((𝐹 ↾ (-∞(,)𝐵)) lim_ℂ 𝐵) ↔ (𝐿 ∈ ℂ ∧ ∀𝑥 ∈ ℝ⁺ ∃𝑎 ∈ ℝ⁺ ∀𝑧 ∈ (𝐴 ∩ (-∞(,)𝐵))((𝑧 ≠ 𝐵 ∧ (abs‘(𝑧 − 𝐵)) < 𝑎) → (abs‘(((𝐹 ↾ (-∞(,)𝐵))‘𝑧) − 𝐿)) < 𝑥))))
158	2, 157	mpbid 235	. . . . . 6 ⊢ (𝜑 → (𝐿 ∈ ℂ ∧ ∀𝑥 ∈ ℝ⁺ ∃𝑎 ∈ ℝ⁺ ∀𝑧 ∈ (𝐴 ∩ (-∞(,)𝐵))((𝑧 ≠ 𝐵 ∧ (abs‘(𝑧 − 𝐵)) < 𝑎) → (abs‘(((𝐹 ↾ (-∞(,)𝐵))‘𝑧) − 𝐿)) < 𝑥)))
159	158	simprd 500	. . . . 5 ⊢ (𝜑 → ∀𝑥 ∈ ℝ⁺ ∃𝑎 ∈ ℝ⁺ ∀𝑧 ∈ (𝐴 ∩ (-∞(,)𝐵))((𝑧 ≠ 𝐵 ∧ (abs‘(𝑧 − 𝐵)) < 𝑎) → (abs‘(((𝐹 ↾ (-∞(,)𝐵))‘𝑧) − 𝐿)) < 𝑥))
160	159	r19.21bi 3263	. . . 4 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ⁺) → ∃𝑎 ∈ ℝ⁺ ∀𝑧 ∈ (𝐴 ∩ (-∞(,)𝐵))((𝑧 ≠ 𝐵 ∧ (abs‘(𝑧 − 𝐵)) < 𝑎) → (abs‘(((𝐹 ↾ (-∞(,)𝐵))‘𝑧) − 𝐿)) < 𝑥))
161	148, 160	r19.29a 3179	. . 3 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ⁺) → ∃𝑦 ∈ ℝ⁺ ∀𝑧 ∈ 𝐴 ((𝑧 ≠ 𝐵 ∧ (abs‘(𝑧 − 𝐵)) < 𝑦) → (abs‘((𝐹‘𝑧) − 𝐿)) < 𝑥))
162	161	ralrimiva 3163	. 2 ⊢ (𝜑 → ∀𝑥 ∈ ℝ⁺ ∃𝑦 ∈ ℝ⁺ ∀𝑧 ∈ 𝐴 ((𝑧 ≠ 𝐵 ∧ (abs‘(𝑧 − 𝐵)) < 𝑦) → (abs‘((𝐹‘𝑧) − 𝐿)) < 𝑥))
163	25, 154	sstrdi 3957	. . 3 ⊢ (𝜑 → 𝐴 ⊆ ℂ)
164	128, 163, 50	ellimc3 26007	. 2 ⊢ (𝜑 → (𝐿 ∈ (𝐹 lim_ℂ 𝐵) ↔ (𝐿 ∈ ℂ ∧ ∀𝑥 ∈ ℝ⁺ ∃𝑦 ∈ ℝ⁺ ∀𝑧 ∈ 𝐴 ((𝑧 ≠ 𝐵 ∧ (abs‘(𝑧 − 𝐵)) < 𝑦) → (abs‘((𝐹‘𝑧) − 𝐿)) < 𝑥))))
165	3, 162, 164	mpbir2and 725	1 ⊢ (𝜑 → 𝐿 ∈ (𝐹 lim_ℂ 𝐵))

Colors of variables: wff setvar class

Syntax hints: ¬ wn 3 → wi 4 ↔ wb 209 ∧ wa 400 ∧ w3a 1101 = wceq 1567 ∈ wcel 2149 ≠ wne 2964 ∀wral 3085 ∃wrex 3095 ∩ cin 3912 ⊆ wss 3913 ifcif 4492 class class class wbr 5113 ran crn 5663 ↾ cres 5664 ⟶wf 6533 ‘cfv 6537 (class class class)co 7411 ℂcc 11098 ℝcr 11099 +∞cpnf 11240 -∞cmnf 11241 ℝ^*cxr 11242 < clt 11243 ≤ cle 11244 − cmin 11441 ℝ⁺crp 13016 (,)cioo 13372 abscabs 15285 TopOpenctopn 17474 topGenctg 17490 ℂ_fldccnfld 21491 lim_ℂ climc 25990

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1822 ax-4 1836 ax-5 1937 ax-6 1994 ax-7 2035 ax-8 2151 ax-9 2159 ax-10 2182 ax-11 2198 ax-12 2219 ax-ext 2741 ax-rep 5242 ax-sep 5261 ax-nul 5271 ax-pow 5337 ax-pr 5405 ax-un 7733 ax-cnex 11156 ax-resscn 11157 ax-1cn 11158 ax-icn 11159 ax-addcl 11160 ax-addrcl 11161 ax-mulcl 11162 ax-mulrcl 11163 ax-mulcom 11164 ax-addass 11165 ax-mulass 11166 ax-distr 11167 ax-i2m1 11168 ax-1ne0 11169 ax-1rid 11170 ax-rnegex 11171 ax-rrecex 11172 ax-cnre 11173 ax-pre-lttri 11174 ax-pre-lttrn 11175 ax-pre-ltadd 11176 ax-pre-mulgt0 11177 ax-pre-sup 11178

This theorem depends on definitions: df-bi 210 df-an 401 df-or 861 df-3or 1102 df-3an 1103 df-tru 1570 df-fal 1580 df-ex 1807 df-nf 1811 df-sb 2098 df-mo 2573 df-eu 2603 df-clab 2748 df-cleq 2761 df-clel 2844 df-nfc 2918 df-ne 2965 df-nel 3071 df-ral 3086 df-rex 3096 df-rmo 3376 df-reu 3377 df-rab 3424 df-v 3465 df-sbc 3754 df-csb 3862 df-dif 3916 df-un 3918 df-in 3920 df-ss 3930 df-pss 3933 df-nul 4295 df-if 4493 df-pw 4569 df-sn 4595 df-pr 4597 df-tp 4599 df-op 4601 df-uni 4877 df-int 4917 df-iun 4962 df-br 5114 df-opab 5178 df-mpt 5197 df-tr 5223 df-id 5557 df-eprel 5562 df-po 5570 df-so 5571 df-fr 5615 df-we 5617 df-xp 5668 df-rel 5669 df-cnv 5670 df-co 5671 df-dm 5672 df-rn 5673 df-res 5674 df-ima 5675 df-pred 6303 df-ord 6364 df-on 6365 df-lim 6366 df-suc 6367 df-iota 6493 df-fun 6539 df-fn 6540 df-f 6541 df-f1 6542 df-fo 6543 df-f1o 6544 df-fv 6545 df-riota 7368 df-ov 7414 df-oprab 7415 df-mpo 7416 df-om 7863 df-1st 7986 df-2nd 7987 df-frecs 8278 df-wrecs 8309 df-recs 8358 df-rdg 8397 df-1o 8453 df-er 8694 df-map 8826 df-pm 8827 df-en 8944 df-dom 8945 df-sdom 8946 df-fin 8947 df-fi 9371 df-sup 9402 df-inf 9403 df-pnf 11245 df-mnf 11246 df-xr 11247 df-ltxr 11248 df-le 11249 df-sub 11443 df-neg 11444 df-div 11872 df-nn 12234 df-2 12303 df-3 12304 df-4 12305 df-5 12306 df-6 12307 df-7 12308 df-8 12309 df-9 12310 df-n0 12505 df-z 12592 df-dec 12712 df-uz 12863 df-q 12973 df-rp 13017 df-xneg 13137 df-xadd 13138 df-xmul 13139 df-ioo 13376 df-fz 13536 df-seq 14038 df-exp 14098 df-cj 15150 df-re 15151 df-im 15152 df-sqrt 15286 df-abs 15287 df-struct 17207 df-slot 17242 df-ndx 17254 df-base 17270 df-plusg 17323 df-mulr 17324 df-starv 17325 df-tset 17329 df-ple 17330 df-ds 17332 df-unif 17333 df-rest 17475 df-topn 17476 df-topgen 17496 df-psmet 21483 df-xmet 21484 df-met 21485 df-bl 21486 df-mopn 21487 df-cnfld 21492 df-top 23020 df-topon 23037 df-topsp 23059 df-bases 23072 df-cnp 23354 df-xms 24446 df-ms 24447 df-limc 25994

This theorem is referenced by: limclr 46261

W3C validator