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 39876

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 23639	. . 3 ⊢ ((𝐹 ↾ (-∞(,)𝐵)) lim_ℂ 𝐵) ⊆ ℂ
2		limcleqr.l	. . 3 ⊢ (𝜑 → 𝐿 ∈ ((𝐹 ↾ (-∞(,)𝐵)) lim_ℂ 𝐵))
3	1, 2	sseldi 3601	. 2 ⊢ (𝜑 → 𝐿 ∈ ℂ)
4		simp-4r 807	. . . . . . 7 ⊢ ((((((𝜑 ∧ 𝑥 ∈ ℝ⁺) ∧ 𝑎 ∈ ℝ⁺) ∧ ∀𝑧 ∈ (𝐴 ∩ (-∞(,)𝐵))((𝑧 ≠ 𝐵 ∧ (abs‘(𝑧 − 𝐵)) < 𝑎) → (abs‘(((𝐹 ↾ (-∞(,)𝐵))‘𝑧) − 𝐿)) < 𝑥)) ∧ 𝑏 ∈ ℝ⁺) ∧ ∀𝑧 ∈ (𝐴 ∩ (𝐵(,)+∞))((𝑧 ≠ 𝐵 ∧ (abs‘(𝑧 − 𝐵)) < 𝑏) → (abs‘(((𝐹 ↾ (𝐵(,)+∞))‘𝑧) − 𝐿)) < 𝑥)) → 𝑎 ∈ ℝ⁺)
5		simplr 792	. . . . . . 7 ⊢ ((((((𝜑 ∧ 𝑥 ∈ ℝ⁺) ∧ 𝑎 ∈ ℝ⁺) ∧ ∀𝑧 ∈ (𝐴 ∩ (-∞(,)𝐵))((𝑧 ≠ 𝐵 ∧ (abs‘(𝑧 − 𝐵)) < 𝑎) → (abs‘(((𝐹 ↾ (-∞(,)𝐵))‘𝑧) − 𝐿)) < 𝑥)) ∧ 𝑏 ∈ ℝ⁺) ∧ ∀𝑧 ∈ (𝐴 ∩ (𝐵(,)+∞))((𝑧 ≠ 𝐵 ∧ (abs‘(𝑧 − 𝐵)) < 𝑏) → (abs‘(((𝐹 ↾ (𝐵(,)+∞))‘𝑧) − 𝐿)) < 𝑥)) → 𝑏 ∈ ℝ⁺)
6	4, 5	ifcld 4131	. . . . . 6 ⊢ ((((((𝜑 ∧ 𝑥 ∈ ℝ⁺) ∧ 𝑎 ∈ ℝ⁺) ∧ ∀𝑧 ∈ (𝐴 ∩ (-∞(,)𝐵))((𝑧 ≠ 𝐵 ∧ (abs‘(𝑧 − 𝐵)) < 𝑎) → (abs‘(((𝐹 ↾ (-∞(,)𝐵))‘𝑧) − 𝐿)) < 𝑥)) ∧ 𝑏 ∈ ℝ⁺) ∧ ∀𝑧 ∈ (𝐴 ∩ (𝐵(,)+∞))((𝑧 ≠ 𝐵 ∧ (abs‘(𝑧 − 𝐵)) < 𝑏) → (abs‘(((𝐹 ↾ (𝐵(,)+∞))‘𝑧) − 𝐿)) < 𝑥)) → if(𝑎 ≤ 𝑏, 𝑎, 𝑏) ∈ ℝ⁺)
7		nfv 1843	. . . . . . . . . . 11 ⊢ Ⅎ𝑧(𝜑 ∧ 𝑥 ∈ ℝ⁺)
8		nfv 1843	. . . . . . . . . . 11 ⊢ Ⅎ𝑧 𝑎 ∈ ℝ⁺
9	7, 8	nfan 1828	. . . . . . . . . 10 ⊢ Ⅎ𝑧((𝜑 ∧ 𝑥 ∈ ℝ⁺) ∧ 𝑎 ∈ ℝ⁺)
10		nfra1 2941	. . . . . . . . . 10 ⊢ Ⅎ𝑧∀𝑧 ∈ (𝐴 ∩ (-∞(,)𝐵))((𝑧 ≠ 𝐵 ∧ (abs‘(𝑧 − 𝐵)) < 𝑎) → (abs‘(((𝐹 ↾ (-∞(,)𝐵))‘𝑧) − 𝐿)) < 𝑥)
11	9, 10	nfan 1828	. . . . . . . . 9 ⊢ Ⅎ𝑧(((𝜑 ∧ 𝑥 ∈ ℝ⁺) ∧ 𝑎 ∈ ℝ⁺) ∧ ∀𝑧 ∈ (𝐴 ∩ (-∞(,)𝐵))((𝑧 ≠ 𝐵 ∧ (abs‘(𝑧 − 𝐵)) < 𝑎) → (abs‘(((𝐹 ↾ (-∞(,)𝐵))‘𝑧) − 𝐿)) < 𝑥))
12		nfv 1843	. . . . . . . . 9 ⊢ Ⅎ𝑧 𝑏 ∈ ℝ⁺
13	11, 12	nfan 1828	. . . . . . . 8 ⊢ Ⅎ𝑧((((𝜑 ∧ 𝑥 ∈ ℝ⁺) ∧ 𝑎 ∈ ℝ⁺) ∧ ∀𝑧 ∈ (𝐴 ∩ (-∞(,)𝐵))((𝑧 ≠ 𝐵 ∧ (abs‘(𝑧 − 𝐵)) < 𝑎) → (abs‘(((𝐹 ↾ (-∞(,)𝐵))‘𝑧) − 𝐿)) < 𝑥)) ∧ 𝑏 ∈ ℝ⁺)
14		nfra1 2941	. . . . . . . 8 ⊢ Ⅎ𝑧∀𝑧 ∈ (𝐴 ∩ (𝐵(,)+∞))((𝑧 ≠ 𝐵 ∧ (abs‘(𝑧 − 𝐵)) < 𝑏) → (abs‘(((𝐹 ↾ (𝐵(,)+∞))‘𝑧) − 𝐿)) < 𝑥)
15	13, 14	nfan 1828	. . . . . . 7 ⊢ Ⅎ𝑧(((((𝜑 ∧ 𝑥 ∈ ℝ⁺) ∧ 𝑎 ∈ ℝ⁺) ∧ ∀𝑧 ∈ (𝐴 ∩ (-∞(,)𝐵))((𝑧 ≠ 𝐵 ∧ (abs‘(𝑧 − 𝐵)) < 𝑎) → (abs‘(((𝐹 ↾ (-∞(,)𝐵))‘𝑧) − 𝐿)) < 𝑥)) ∧ 𝑏 ∈ ℝ⁺) ∧ ∀𝑧 ∈ (𝐴 ∩ (𝐵(,)+∞))((𝑧 ≠ 𝐵 ∧ (abs‘(𝑧 − 𝐵)) < 𝑏) → (abs‘(((𝐹 ↾ (𝐵(,)+∞))‘𝑧) − 𝐿)) < 𝑥))
16		simp-6l 810	. . . . . . . . . . . . 13 ⊢ (((((((𝜑 ∧ 𝑥 ∈ ℝ⁺) ∧ 𝑎 ∈ ℝ⁺) ∧ ∀𝑧 ∈ (𝐴 ∩ (-∞(,)𝐵))((𝑧 ≠ 𝐵 ∧ (abs‘(𝑧 − 𝐵)) < 𝑎) → (abs‘(((𝐹 ↾ (-∞(,)𝐵))‘𝑧) − 𝐿)) < 𝑥)) ∧ 𝑏 ∈ ℝ⁺) ∧ ∀𝑧 ∈ (𝐴 ∩ (𝐵(,)+∞))((𝑧 ≠ 𝐵 ∧ (abs‘(𝑧 − 𝐵)) < 𝑏) → (abs‘(((𝐹 ↾ (𝐵(,)+∞))‘𝑧) − 𝐿)) < 𝑥)) ∧ 𝑧 < 𝐵) → 𝜑)
17	16	3ad2antl1 1223	. . . . . . . . . . . 12 ⊢ ((((((((𝜑 ∧ 𝑥 ∈ ℝ⁺) ∧ 𝑎 ∈ ℝ⁺) ∧ ∀𝑧 ∈ (𝐴 ∩ (-∞(,)𝐵))((𝑧 ≠ 𝐵 ∧ (abs‘(𝑧 − 𝐵)) < 𝑎) → (abs‘(((𝐹 ↾ (-∞(,)𝐵))‘𝑧) − 𝐿)) < 𝑥)) ∧ 𝑏 ∈ ℝ⁺) ∧ ∀𝑧 ∈ (𝐴 ∩ (𝐵(,)+∞))((𝑧 ≠ 𝐵 ∧ (abs‘(𝑧 − 𝐵)) < 𝑏) → (abs‘(((𝐹 ↾ (𝐵(,)+∞))‘𝑧) − 𝐿)) < 𝑥)) ∧ 𝑧 ∈ 𝐴 ∧ (𝑧 ≠ 𝐵 ∧ (abs‘(𝑧 − 𝐵)) < if(𝑎 ≤ 𝑏, 𝑎, 𝑏))) ∧ 𝑧 < 𝐵) → 𝜑)
18		simpl2 1065	. . . . . . . . . . . 12 ⊢ ((((((((𝜑 ∧ 𝑥 ∈ ℝ⁺) ∧ 𝑎 ∈ ℝ⁺) ∧ ∀𝑧 ∈ (𝐴 ∩ (-∞(,)𝐵))((𝑧 ≠ 𝐵 ∧ (abs‘(𝑧 − 𝐵)) < 𝑎) → (abs‘(((𝐹 ↾ (-∞(,)𝐵))‘𝑧) − 𝐿)) < 𝑥)) ∧ 𝑏 ∈ ℝ⁺) ∧ ∀𝑧 ∈ (𝐴 ∩ (𝐵(,)+∞))((𝑧 ≠ 𝐵 ∧ (abs‘(𝑧 − 𝐵)) < 𝑏) → (abs‘(((𝐹 ↾ (𝐵(,)+∞))‘𝑧) − 𝐿)) < 𝑥)) ∧ 𝑧 ∈ 𝐴 ∧ (𝑧 ≠ 𝐵 ∧ (abs‘(𝑧 − 𝐵)) < if(𝑎 ≤ 𝑏, 𝑎, 𝑏))) ∧ 𝑧 < 𝐵) → 𝑧 ∈ 𝐴)
19		simpr 477	. . . . . . . . . . . 12 ⊢ ((((((((𝜑 ∧ 𝑥 ∈ ℝ⁺) ∧ 𝑎 ∈ ℝ⁺) ∧ ∀𝑧 ∈ (𝐴 ∩ (-∞(,)𝐵))((𝑧 ≠ 𝐵 ∧ (abs‘(𝑧 − 𝐵)) < 𝑎) → (abs‘(((𝐹 ↾ (-∞(,)𝐵))‘𝑧) − 𝐿)) < 𝑥)) ∧ 𝑏 ∈ ℝ⁺) ∧ ∀𝑧 ∈ (𝐴 ∩ (𝐵(,)+∞))((𝑧 ≠ 𝐵 ∧ (abs‘(𝑧 − 𝐵)) < 𝑏) → (abs‘(((𝐹 ↾ (𝐵(,)+∞))‘𝑧) − 𝐿)) < 𝑥)) ∧ 𝑧 ∈ 𝐴 ∧ (𝑧 ≠ 𝐵 ∧ (abs‘(𝑧 − 𝐵)) < if(𝑎 ≤ 𝑏, 𝑎, 𝑏))) ∧ 𝑧 < 𝐵) → 𝑧 < 𝐵)
20		mnfxr 10096	. . . . . . . . . . . . . 14 ⊢ -∞ ∈ ℝ^*
21	20	a1i 11	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝐴 ∧ 𝑧 < 𝐵) → -∞ ∈ ℝ^*)
22		limcleqr.b	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → 𝐵 ∈ ℝ)
23	22	rexrd 10089	. . . . . . . . . . . . . 14 ⊢ (𝜑 → 𝐵 ∈ ℝ^*)
24	23	3ad2ant1 1082	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝐴 ∧ 𝑧 < 𝐵) → 𝐵 ∈ ℝ^*)
25		limcleqr.a	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → 𝐴 ⊆ ℝ)
26	25	sselda 3603	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝐴) → 𝑧 ∈ ℝ)
27	26	3adant3 1081	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝐴 ∧ 𝑧 < 𝐵) → 𝑧 ∈ ℝ)
28	27	mnfltd 11958	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝐴 ∧ 𝑧 < 𝐵) → -∞ < 𝑧)
29		simp3 1063	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝐴 ∧ 𝑧 < 𝐵) → 𝑧 < 𝐵)
30	21, 24, 27, 28, 29	eliood 39720	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝐴 ∧ 𝑧 < 𝐵) → 𝑧 ∈ (-∞(,)𝐵))
31	17, 18, 19, 30	syl3anc 1326	. . . . . . . . . . 11 ⊢ ((((((((𝜑 ∧ 𝑥 ∈ ℝ⁺) ∧ 𝑎 ∈ ℝ⁺) ∧ ∀𝑧 ∈ (𝐴 ∩ (-∞(,)𝐵))((𝑧 ≠ 𝐵 ∧ (abs‘(𝑧 − 𝐵)) < 𝑎) → (abs‘(((𝐹 ↾ (-∞(,)𝐵))‘𝑧) − 𝐿)) < 𝑥)) ∧ 𝑏 ∈ ℝ⁺) ∧ ∀𝑧 ∈ (𝐴 ∩ (𝐵(,)+∞))((𝑧 ≠ 𝐵 ∧ (abs‘(𝑧 − 𝐵)) < 𝑏) → (abs‘(((𝐹 ↾ (𝐵(,)+∞))‘𝑧) − 𝐿)) < 𝑥)) ∧ 𝑧 ∈ 𝐴 ∧ (𝑧 ≠ 𝐵 ∧ (abs‘(𝑧 − 𝐵)) < if(𝑎 ≤ 𝑏, 𝑎, 𝑏))) ∧ 𝑧 < 𝐵) → 𝑧 ∈ (-∞(,)𝐵))
32		fvres 6207	. . . . . . . . . . . . . 14 ⊢ (𝑧 ∈ (-∞(,)𝐵) → ((𝐹 ↾ (-∞(,)𝐵))‘𝑧) = (𝐹‘𝑧))
33	32	oveq1d 6665	. . . . . . . . . . . . 13 ⊢ (𝑧 ∈ (-∞(,)𝐵) → (((𝐹 ↾ (-∞(,)𝐵))‘𝑧) − 𝐿) = ((𝐹‘𝑧) − 𝐿))
34	33	eqcomd 2628	. . . . . . . . . . . 12 ⊢ (𝑧 ∈ (-∞(,)𝐵) → ((𝐹‘𝑧) − 𝐿) = (((𝐹 ↾ (-∞(,)𝐵))‘𝑧) − 𝐿))
35	34	fveq2d 6195	. . . . . . . . . . 11 ⊢ (𝑧 ∈ (-∞(,)𝐵) → (abs‘((𝐹‘𝑧) − 𝐿)) = (abs‘(((𝐹 ↾ (-∞(,)𝐵))‘𝑧) − 𝐿)))
36	31, 35	syl 17	. . . . . . . . . 10 ⊢ ((((((((𝜑 ∧ 𝑥 ∈ ℝ⁺) ∧ 𝑎 ∈ ℝ⁺) ∧ ∀𝑧 ∈ (𝐴 ∩ (-∞(,)𝐵))((𝑧 ≠ 𝐵 ∧ (abs‘(𝑧 − 𝐵)) < 𝑎) → (abs‘(((𝐹 ↾ (-∞(,)𝐵))‘𝑧) − 𝐿)) < 𝑥)) ∧ 𝑏 ∈ ℝ⁺) ∧ ∀𝑧 ∈ (𝐴 ∩ (𝐵(,)+∞))((𝑧 ≠ 𝐵 ∧ (abs‘(𝑧 − 𝐵)) < 𝑏) → (abs‘(((𝐹 ↾ (𝐵(,)+∞))‘𝑧) − 𝐿)) < 𝑥)) ∧ 𝑧 ∈ 𝐴 ∧ (𝑧 ≠ 𝐵 ∧ (abs‘(𝑧 − 𝐵)) < if(𝑎 ≤ 𝑏, 𝑎, 𝑏))) ∧ 𝑧 < 𝐵) → (abs‘((𝐹‘𝑧) − 𝐿)) = (abs‘(((𝐹 ↾ (-∞(,)𝐵))‘𝑧) − 𝐿)))
37		simp-4r 807	. . . . . . . . . . . . 13 ⊢ (((((((𝜑 ∧ 𝑥 ∈ ℝ⁺) ∧ 𝑎 ∈ ℝ⁺) ∧ ∀𝑧 ∈ (𝐴 ∩ (-∞(,)𝐵))((𝑧 ≠ 𝐵 ∧ (abs‘(𝑧 − 𝐵)) < 𝑎) → (abs‘(((𝐹 ↾ (-∞(,)𝐵))‘𝑧) − 𝐿)) < 𝑥)) ∧ 𝑏 ∈ ℝ⁺) ∧ ∀𝑧 ∈ (𝐴 ∩ (𝐵(,)+∞))((𝑧 ≠ 𝐵 ∧ (abs‘(𝑧 − 𝐵)) < 𝑏) → (abs‘(((𝐹 ↾ (𝐵(,)+∞))‘𝑧) − 𝐿)) < 𝑥)) ∧ 𝑧 < 𝐵) → ∀𝑧 ∈ (𝐴 ∩ (-∞(,)𝐵))((𝑧 ≠ 𝐵 ∧ (abs‘(𝑧 − 𝐵)) < 𝑎) → (abs‘(((𝐹 ↾ (-∞(,)𝐵))‘𝑧) − 𝐿)) < 𝑥))
38	37	3ad2antl1 1223	. . . . . . . . . . . 12 ⊢ ((((((((𝜑 ∧ 𝑥 ∈ ℝ⁺) ∧ 𝑎 ∈ ℝ⁺) ∧ ∀𝑧 ∈ (𝐴 ∩ (-∞(,)𝐵))((𝑧 ≠ 𝐵 ∧ (abs‘(𝑧 − 𝐵)) < 𝑎) → (abs‘(((𝐹 ↾ (-∞(,)𝐵))‘𝑧) − 𝐿)) < 𝑥)) ∧ 𝑏 ∈ ℝ⁺) ∧ ∀𝑧 ∈ (𝐴 ∩ (𝐵(,)+∞))((𝑧 ≠ 𝐵 ∧ (abs‘(𝑧 − 𝐵)) < 𝑏) → (abs‘(((𝐹 ↾ (𝐵(,)+∞))‘𝑧) − 𝐿)) < 𝑥)) ∧ 𝑧 ∈ 𝐴 ∧ (𝑧 ≠ 𝐵 ∧ (abs‘(𝑧 − 𝐵)) < if(𝑎 ≤ 𝑏, 𝑎, 𝑏))) ∧ 𝑧 < 𝐵) → ∀𝑧 ∈ (𝐴 ∩ (-∞(,)𝐵))((𝑧 ≠ 𝐵 ∧ (abs‘(𝑧 − 𝐵)) < 𝑎) → (abs‘(((𝐹 ↾ (-∞(,)𝐵))‘𝑧) − 𝐿)) < 𝑥))
39	18, 31	elind 3798	. . . . . . . . . . . 12 ⊢ ((((((((𝜑 ∧ 𝑥 ∈ ℝ⁺) ∧ 𝑎 ∈ ℝ⁺) ∧ ∀𝑧 ∈ (𝐴 ∩ (-∞(,)𝐵))((𝑧 ≠ 𝐵 ∧ (abs‘(𝑧 − 𝐵)) < 𝑎) → (abs‘(((𝐹 ↾ (-∞(,)𝐵))‘𝑧) − 𝐿)) < 𝑥)) ∧ 𝑏 ∈ ℝ⁺) ∧ ∀𝑧 ∈ (𝐴 ∩ (𝐵(,)+∞))((𝑧 ≠ 𝐵 ∧ (abs‘(𝑧 − 𝐵)) < 𝑏) → (abs‘(((𝐹 ↾ (𝐵(,)+∞))‘𝑧) − 𝐿)) < 𝑥)) ∧ 𝑧 ∈ 𝐴 ∧ (𝑧 ≠ 𝐵 ∧ (abs‘(𝑧 − 𝐵)) < if(𝑎 ≤ 𝑏, 𝑎, 𝑏))) ∧ 𝑧 < 𝐵) → 𝑧 ∈ (𝐴 ∩ (-∞(,)𝐵)))
40	38, 39	jca 554	. . . . . . . . . . 11 ⊢ ((((((((𝜑 ∧ 𝑥 ∈ ℝ⁺) ∧ 𝑎 ∈ ℝ⁺) ∧ ∀𝑧 ∈ (𝐴 ∩ (-∞(,)𝐵))((𝑧 ≠ 𝐵 ∧ (abs‘(𝑧 − 𝐵)) < 𝑎) → (abs‘(((𝐹 ↾ (-∞(,)𝐵))‘𝑧) − 𝐿)) < 𝑥)) ∧ 𝑏 ∈ ℝ⁺) ∧ ∀𝑧 ∈ (𝐴 ∩ (𝐵(,)+∞))((𝑧 ≠ 𝐵 ∧ (abs‘(𝑧 − 𝐵)) < 𝑏) → (abs‘(((𝐹 ↾ (𝐵(,)+∞))‘𝑧) − 𝐿)) < 𝑥)) ∧ 𝑧 ∈ 𝐴 ∧ (𝑧 ≠ 𝐵 ∧ (abs‘(𝑧 − 𝐵)) < if(𝑎 ≤ 𝑏, 𝑎, 𝑏))) ∧ 𝑧 < 𝐵) → (∀𝑧 ∈ (𝐴 ∩ (-∞(,)𝐵))((𝑧 ≠ 𝐵 ∧ (abs‘(𝑧 − 𝐵)) < 𝑎) → (abs‘(((𝐹 ↾ (-∞(,)𝐵))‘𝑧) − 𝐿)) < 𝑥) ∧ 𝑧 ∈ (𝐴 ∩ (-∞(,)𝐵))))
41		simpl3l 1116	. . . . . . . . . . . 12 ⊢ ((((((((𝜑 ∧ 𝑥 ∈ ℝ⁺) ∧ 𝑎 ∈ ℝ⁺) ∧ ∀𝑧 ∈ (𝐴 ∩ (-∞(,)𝐵))((𝑧 ≠ 𝐵 ∧ (abs‘(𝑧 − 𝐵)) < 𝑎) → (abs‘(((𝐹 ↾ (-∞(,)𝐵))‘𝑧) − 𝐿)) < 𝑥)) ∧ 𝑏 ∈ ℝ⁺) ∧ ∀𝑧 ∈ (𝐴 ∩ (𝐵(,)+∞))((𝑧 ≠ 𝐵 ∧ (abs‘(𝑧 − 𝐵)) < 𝑏) → (abs‘(((𝐹 ↾ (𝐵(,)+∞))‘𝑧) − 𝐿)) < 𝑥)) ∧ 𝑧 ∈ 𝐴 ∧ (𝑧 ≠ 𝐵 ∧ (abs‘(𝑧 − 𝐵)) < if(𝑎 ≤ 𝑏, 𝑎, 𝑏))) ∧ 𝑧 < 𝐵) → 𝑧 ≠ 𝐵)
42	4	adantr 481	. . . . . . . . . . . . . 14 ⊢ (((((((𝜑 ∧ 𝑥 ∈ ℝ⁺) ∧ 𝑎 ∈ ℝ⁺) ∧ ∀𝑧 ∈ (𝐴 ∩ (-∞(,)𝐵))((𝑧 ≠ 𝐵 ∧ (abs‘(𝑧 − 𝐵)) < 𝑎) → (abs‘(((𝐹 ↾ (-∞(,)𝐵))‘𝑧) − 𝐿)) < 𝑥)) ∧ 𝑏 ∈ ℝ⁺) ∧ ∀𝑧 ∈ (𝐴 ∩ (𝐵(,)+∞))((𝑧 ≠ 𝐵 ∧ (abs‘(𝑧 − 𝐵)) < 𝑏) → (abs‘(((𝐹 ↾ (𝐵(,)+∞))‘𝑧) − 𝐿)) < 𝑥)) ∧ 𝑧 < 𝐵) → 𝑎 ∈ ℝ⁺)
43	42	3ad2antl1 1223	. . . . . . . . . . . . 13 ⊢ ((((((((𝜑 ∧ 𝑥 ∈ ℝ⁺) ∧ 𝑎 ∈ ℝ⁺) ∧ ∀𝑧 ∈ (𝐴 ∩ (-∞(,)𝐵))((𝑧 ≠ 𝐵 ∧ (abs‘(𝑧 − 𝐵)) < 𝑎) → (abs‘(((𝐹 ↾ (-∞(,)𝐵))‘𝑧) − 𝐿)) < 𝑥)) ∧ 𝑏 ∈ ℝ⁺) ∧ ∀𝑧 ∈ (𝐴 ∩ (𝐵(,)+∞))((𝑧 ≠ 𝐵 ∧ (abs‘(𝑧 − 𝐵)) < 𝑏) → (abs‘(((𝐹 ↾ (𝐵(,)+∞))‘𝑧) − 𝐿)) < 𝑥)) ∧ 𝑧 ∈ 𝐴 ∧ (𝑧 ≠ 𝐵 ∧ (abs‘(𝑧 − 𝐵)) < if(𝑎 ≤ 𝑏, 𝑎, 𝑏))) ∧ 𝑧 < 𝐵) → 𝑎 ∈ ℝ⁺)
44	5	adantr 481	. . . . . . . . . . . . . 14 ⊢ (((((((𝜑 ∧ 𝑥 ∈ ℝ⁺) ∧ 𝑎 ∈ ℝ⁺) ∧ ∀𝑧 ∈ (𝐴 ∩ (-∞(,)𝐵))((𝑧 ≠ 𝐵 ∧ (abs‘(𝑧 − 𝐵)) < 𝑎) → (abs‘(((𝐹 ↾ (-∞(,)𝐵))‘𝑧) − 𝐿)) < 𝑥)) ∧ 𝑏 ∈ ℝ⁺) ∧ ∀𝑧 ∈ (𝐴 ∩ (𝐵(,)+∞))((𝑧 ≠ 𝐵 ∧ (abs‘(𝑧 − 𝐵)) < 𝑏) → (abs‘(((𝐹 ↾ (𝐵(,)+∞))‘𝑧) − 𝐿)) < 𝑥)) ∧ 𝑧 < 𝐵) → 𝑏 ∈ ℝ⁺)
45	44	3ad2antl1 1223	. . . . . . . . . . . . 13 ⊢ ((((((((𝜑 ∧ 𝑥 ∈ ℝ⁺) ∧ 𝑎 ∈ ℝ⁺) ∧ ∀𝑧 ∈ (𝐴 ∩ (-∞(,)𝐵))((𝑧 ≠ 𝐵 ∧ (abs‘(𝑧 − 𝐵)) < 𝑎) → (abs‘(((𝐹 ↾ (-∞(,)𝐵))‘𝑧) − 𝐿)) < 𝑥)) ∧ 𝑏 ∈ ℝ⁺) ∧ ∀𝑧 ∈ (𝐴 ∩ (𝐵(,)+∞))((𝑧 ≠ 𝐵 ∧ (abs‘(𝑧 − 𝐵)) < 𝑏) → (abs‘(((𝐹 ↾ (𝐵(,)+∞))‘𝑧) − 𝐿)) < 𝑥)) ∧ 𝑧 ∈ 𝐴 ∧ (𝑧 ≠ 𝐵 ∧ (abs‘(𝑧 − 𝐵)) < if(𝑎 ≤ 𝑏, 𝑎, 𝑏))) ∧ 𝑧 < 𝐵) → 𝑏 ∈ ℝ⁺)
46		simpl3r 1117	. . . . . . . . . . . . 13 ⊢ ((((((((𝜑 ∧ 𝑥 ∈ ℝ⁺) ∧ 𝑎 ∈ ℝ⁺) ∧ ∀𝑧 ∈ (𝐴 ∩ (-∞(,)𝐵))((𝑧 ≠ 𝐵 ∧ (abs‘(𝑧 − 𝐵)) < 𝑎) → (abs‘(((𝐹 ↾ (-∞(,)𝐵))‘𝑧) − 𝐿)) < 𝑥)) ∧ 𝑏 ∈ ℝ⁺) ∧ ∀𝑧 ∈ (𝐴 ∩ (𝐵(,)+∞))((𝑧 ≠ 𝐵 ∧ (abs‘(𝑧 − 𝐵)) < 𝑏) → (abs‘(((𝐹 ↾ (𝐵(,)+∞))‘𝑧) − 𝐿)) < 𝑥)) ∧ 𝑧 ∈ 𝐴 ∧ (𝑧 ≠ 𝐵 ∧ (abs‘(𝑧 − 𝐵)) < if(𝑎 ≤ 𝑏, 𝑎, 𝑏))) ∧ 𝑧 < 𝐵) → (abs‘(𝑧 − 𝐵)) < if(𝑎 ≤ 𝑏, 𝑎, 𝑏))
47		simpl1 1064	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑎 ∈ ℝ⁺ ∧ 𝑏 ∈ ℝ⁺) ∧ ((abs‘(𝑧 − 𝐵)) < if(𝑎 ≤ 𝑏, 𝑎, 𝑏) ∧ 𝑧 ∈ 𝐴)) → 𝜑)
48		simprr 796	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑎 ∈ ℝ⁺ ∧ 𝑏 ∈ ℝ⁺) ∧ ((abs‘(𝑧 − 𝐵)) < if(𝑎 ≤ 𝑏, 𝑎, 𝑏) ∧ 𝑧 ∈ 𝐴)) → 𝑧 ∈ 𝐴)
49	26	recnd 10068	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝐴) → 𝑧 ∈ ℂ)
50	22	recnd 10068	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → 𝐵 ∈ ℂ)
51	50	adantr 481	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝐴) → 𝐵 ∈ ℂ)
52	49, 51	subcld 10392	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝐴) → (𝑧 − 𝐵) ∈ ℂ)
53	52	abscld 14175	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝐴) → (abs‘(𝑧 − 𝐵)) ∈ ℝ)
54	47, 48, 53	syl2anc 693	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑎 ∈ ℝ⁺ ∧ 𝑏 ∈ ℝ⁺) ∧ ((abs‘(𝑧 − 𝐵)) < if(𝑎 ≤ 𝑏, 𝑎, 𝑏) ∧ 𝑧 ∈ 𝐴)) → (abs‘(𝑧 − 𝐵)) ∈ ℝ)
55		rpre 11839	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑎 ∈ ℝ⁺ → 𝑎 ∈ ℝ)
56	55	adantr 481	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑎 ∈ ℝ⁺ ∧ 𝑏 ∈ ℝ⁺) → 𝑎 ∈ ℝ)
57		rpre 11839	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑏 ∈ ℝ⁺ → 𝑏 ∈ ℝ)
58	57	adantl 482	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑎 ∈ ℝ⁺ ∧ 𝑏 ∈ ℝ⁺) → 𝑏 ∈ ℝ)
59	56, 58	ifcld 4131	. . . . . . . . . . . . . . . 16 ⊢ ((𝑎 ∈ ℝ⁺ ∧ 𝑏 ∈ ℝ⁺) → if(𝑎 ≤ 𝑏, 𝑎, 𝑏) ∈ ℝ)
60	59	3adant1 1079	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑎 ∈ ℝ⁺ ∧ 𝑏 ∈ ℝ⁺) → if(𝑎 ≤ 𝑏, 𝑎, 𝑏) ∈ ℝ)
61	60	adantr 481	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑎 ∈ ℝ⁺ ∧ 𝑏 ∈ ℝ⁺) ∧ ((abs‘(𝑧 − 𝐵)) < if(𝑎 ≤ 𝑏, 𝑎, 𝑏) ∧ 𝑧 ∈ 𝐴)) → if(𝑎 ≤ 𝑏, 𝑎, 𝑏) ∈ ℝ)
62	56	3adant1 1079	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑎 ∈ ℝ⁺ ∧ 𝑏 ∈ ℝ⁺) → 𝑎 ∈ ℝ)
63	62	adantr 481	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑎 ∈ ℝ⁺ ∧ 𝑏 ∈ ℝ⁺) ∧ ((abs‘(𝑧 − 𝐵)) < if(𝑎 ≤ 𝑏, 𝑎, 𝑏) ∧ 𝑧 ∈ 𝐴)) → 𝑎 ∈ ℝ)
64		simprl 794	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑎 ∈ ℝ⁺ ∧ 𝑏 ∈ ℝ⁺) ∧ ((abs‘(𝑧 − 𝐵)) < if(𝑎 ≤ 𝑏, 𝑎, 𝑏) ∧ 𝑧 ∈ 𝐴)) → (abs‘(𝑧 − 𝐵)) < if(𝑎 ≤ 𝑏, 𝑎, 𝑏))
65	58	3adant1 1079	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑎 ∈ ℝ⁺ ∧ 𝑏 ∈ ℝ⁺) → 𝑏 ∈ ℝ)
66		min1 12020	. . . . . . . . . . . . . . . 16 ⊢ ((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) → if(𝑎 ≤ 𝑏, 𝑎, 𝑏) ≤ 𝑎)
67	62, 65, 66	syl2anc 693	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑎 ∈ ℝ⁺ ∧ 𝑏 ∈ ℝ⁺) → if(𝑎 ≤ 𝑏, 𝑎, 𝑏) ≤ 𝑎)
68	67	adantr 481	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑎 ∈ ℝ⁺ ∧ 𝑏 ∈ ℝ⁺) ∧ ((abs‘(𝑧 − 𝐵)) < if(𝑎 ≤ 𝑏, 𝑎, 𝑏) ∧ 𝑧 ∈ 𝐴)) → if(𝑎 ≤ 𝑏, 𝑎, 𝑏) ≤ 𝑎)
69	54, 61, 63, 64, 68	ltletrd 10197	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑎 ∈ ℝ⁺ ∧ 𝑏 ∈ ℝ⁺) ∧ ((abs‘(𝑧 − 𝐵)) < if(𝑎 ≤ 𝑏, 𝑎, 𝑏) ∧ 𝑧 ∈ 𝐴)) → (abs‘(𝑧 − 𝐵)) < 𝑎)
70	17, 43, 45, 46, 18, 69	syl32anc 1334	. . . . . . . . . . . 12 ⊢ ((((((((𝜑 ∧ 𝑥 ∈ ℝ⁺) ∧ 𝑎 ∈ ℝ⁺) ∧ ∀𝑧 ∈ (𝐴 ∩ (-∞(,)𝐵))((𝑧 ≠ 𝐵 ∧ (abs‘(𝑧 − 𝐵)) < 𝑎) → (abs‘(((𝐹 ↾ (-∞(,)𝐵))‘𝑧) − 𝐿)) < 𝑥)) ∧ 𝑏 ∈ ℝ⁺) ∧ ∀𝑧 ∈ (𝐴 ∩ (𝐵(,)+∞))((𝑧 ≠ 𝐵 ∧ (abs‘(𝑧 − 𝐵)) < 𝑏) → (abs‘(((𝐹 ↾ (𝐵(,)+∞))‘𝑧) − 𝐿)) < 𝑥)) ∧ 𝑧 ∈ 𝐴 ∧ (𝑧 ≠ 𝐵 ∧ (abs‘(𝑧 − 𝐵)) < if(𝑎 ≤ 𝑏, 𝑎, 𝑏))) ∧ 𝑧 < 𝐵) → (abs‘(𝑧 − 𝐵)) < 𝑎)
71	41, 70	jca 554	. . . . . . . . . . 11 ⊢ ((((((((𝜑 ∧ 𝑥 ∈ ℝ⁺) ∧ 𝑎 ∈ ℝ⁺) ∧ ∀𝑧 ∈ (𝐴 ∩ (-∞(,)𝐵))((𝑧 ≠ 𝐵 ∧ (abs‘(𝑧 − 𝐵)) < 𝑎) → (abs‘(((𝐹 ↾ (-∞(,)𝐵))‘𝑧) − 𝐿)) < 𝑥)) ∧ 𝑏 ∈ ℝ⁺) ∧ ∀𝑧 ∈ (𝐴 ∩ (𝐵(,)+∞))((𝑧 ≠ 𝐵 ∧ (abs‘(𝑧 − 𝐵)) < 𝑏) → (abs‘(((𝐹 ↾ (𝐵(,)+∞))‘𝑧) − 𝐿)) < 𝑥)) ∧ 𝑧 ∈ 𝐴 ∧ (𝑧 ≠ 𝐵 ∧ (abs‘(𝑧 − 𝐵)) < if(𝑎 ≤ 𝑏, 𝑎, 𝑏))) ∧ 𝑧 < 𝐵) → (𝑧 ≠ 𝐵 ∧ (abs‘(𝑧 − 𝐵)) < 𝑎))
72		rspa 2930	. . . . . . . . . . 11 ⊢ ((∀𝑧 ∈ (𝐴 ∩ (-∞(,)𝐵))((𝑧 ≠ 𝐵 ∧ (abs‘(𝑧 − 𝐵)) < 𝑎) → (abs‘(((𝐹 ↾ (-∞(,)𝐵))‘𝑧) − 𝐿)) < 𝑥) ∧ 𝑧 ∈ (𝐴 ∩ (-∞(,)𝐵))) → ((𝑧 ≠ 𝐵 ∧ (abs‘(𝑧 − 𝐵)) < 𝑎) → (abs‘(((𝐹 ↾ (-∞(,)𝐵))‘𝑧) − 𝐿)) < 𝑥))
73	40, 71, 72	sylc 65	. . . . . . . . . 10 ⊢ ((((((((𝜑 ∧ 𝑥 ∈ ℝ⁺) ∧ 𝑎 ∈ ℝ⁺) ∧ ∀𝑧 ∈ (𝐴 ∩ (-∞(,)𝐵))((𝑧 ≠ 𝐵 ∧ (abs‘(𝑧 − 𝐵)) < 𝑎) → (abs‘(((𝐹 ↾ (-∞(,)𝐵))‘𝑧) − 𝐿)) < 𝑥)) ∧ 𝑏 ∈ ℝ⁺) ∧ ∀𝑧 ∈ (𝐴 ∩ (𝐵(,)+∞))((𝑧 ≠ 𝐵 ∧ (abs‘(𝑧 − 𝐵)) < 𝑏) → (abs‘(((𝐹 ↾ (𝐵(,)+∞))‘𝑧) − 𝐿)) < 𝑥)) ∧ 𝑧 ∈ 𝐴 ∧ (𝑧 ≠ 𝐵 ∧ (abs‘(𝑧 − 𝐵)) < if(𝑎 ≤ 𝑏, 𝑎, 𝑏))) ∧ 𝑧 < 𝐵) → (abs‘(((𝐹 ↾ (-∞(,)𝐵))‘𝑧) − 𝐿)) < 𝑥)
74	36, 73	eqbrtrd 4675	. . . . . . . . 9 ⊢ ((((((((𝜑 ∧ 𝑥 ∈ ℝ⁺) ∧ 𝑎 ∈ ℝ⁺) ∧ ∀𝑧 ∈ (𝐴 ∩ (-∞(,)𝐵))((𝑧 ≠ 𝐵 ∧ (abs‘(𝑧 − 𝐵)) < 𝑎) → (abs‘(((𝐹 ↾ (-∞(,)𝐵))‘𝑧) − 𝐿)) < 𝑥)) ∧ 𝑏 ∈ ℝ⁺) ∧ ∀𝑧 ∈ (𝐴 ∩ (𝐵(,)+∞))((𝑧 ≠ 𝐵 ∧ (abs‘(𝑧 − 𝐵)) < 𝑏) → (abs‘(((𝐹 ↾ (𝐵(,)+∞))‘𝑧) − 𝐿)) < 𝑥)) ∧ 𝑧 ∈ 𝐴 ∧ (𝑧 ≠ 𝐵 ∧ (abs‘(𝑧 − 𝐵)) < if(𝑎 ≤ 𝑏, 𝑎, 𝑏))) ∧ 𝑧 < 𝐵) → (abs‘((𝐹‘𝑧) − 𝐿)) < 𝑥)
75		simp-6l 810	. . . . . . . . . . . . 13 ⊢ (((((((𝜑 ∧ 𝑥 ∈ ℝ⁺) ∧ 𝑎 ∈ ℝ⁺) ∧ ∀𝑧 ∈ (𝐴 ∩ (-∞(,)𝐵))((𝑧 ≠ 𝐵 ∧ (abs‘(𝑧 − 𝐵)) < 𝑎) → (abs‘(((𝐹 ↾ (-∞(,)𝐵))‘𝑧) − 𝐿)) < 𝑥)) ∧ 𝑏 ∈ ℝ⁺) ∧ ∀𝑧 ∈ (𝐴 ∩ (𝐵(,)+∞))((𝑧 ≠ 𝐵 ∧ (abs‘(𝑧 − 𝐵)) < 𝑏) → (abs‘(((𝐹 ↾ (𝐵(,)+∞))‘𝑧) − 𝐿)) < 𝑥)) ∧ ¬ 𝑧 < 𝐵) → 𝜑)
76	75	3ad2antl1 1223	. . . . . . . . . . . 12 ⊢ ((((((((𝜑 ∧ 𝑥 ∈ ℝ⁺) ∧ 𝑎 ∈ ℝ⁺) ∧ ∀𝑧 ∈ (𝐴 ∩ (-∞(,)𝐵))((𝑧 ≠ 𝐵 ∧ (abs‘(𝑧 − 𝐵)) < 𝑎) → (abs‘(((𝐹 ↾ (-∞(,)𝐵))‘𝑧) − 𝐿)) < 𝑥)) ∧ 𝑏 ∈ ℝ⁺) ∧ ∀𝑧 ∈ (𝐴 ∩ (𝐵(,)+∞))((𝑧 ≠ 𝐵 ∧ (abs‘(𝑧 − 𝐵)) < 𝑏) → (abs‘(((𝐹 ↾ (𝐵(,)+∞))‘𝑧) − 𝐿)) < 𝑥)) ∧ 𝑧 ∈ 𝐴 ∧ (𝑧 ≠ 𝐵 ∧ (abs‘(𝑧 − 𝐵)) < if(𝑎 ≤ 𝑏, 𝑎, 𝑏))) ∧ ¬ 𝑧 < 𝐵) → 𝜑)
77	76, 22	syl 17	. . . . . . . . . . 11 ⊢ ((((((((𝜑 ∧ 𝑥 ∈ ℝ⁺) ∧ 𝑎 ∈ ℝ⁺) ∧ ∀𝑧 ∈ (𝐴 ∩ (-∞(,)𝐵))((𝑧 ≠ 𝐵 ∧ (abs‘(𝑧 − 𝐵)) < 𝑎) → (abs‘(((𝐹 ↾ (-∞(,)𝐵))‘𝑧) − 𝐿)) < 𝑥)) ∧ 𝑏 ∈ ℝ⁺) ∧ ∀𝑧 ∈ (𝐴 ∩ (𝐵(,)+∞))((𝑧 ≠ 𝐵 ∧ (abs‘(𝑧 − 𝐵)) < 𝑏) → (abs‘(((𝐹 ↾ (𝐵(,)+∞))‘𝑧) − 𝐿)) < 𝑥)) ∧ 𝑧 ∈ 𝐴 ∧ (𝑧 ≠ 𝐵 ∧ (abs‘(𝑧 − 𝐵)) < if(𝑎 ≤ 𝑏, 𝑎, 𝑏))) ∧ ¬ 𝑧 < 𝐵) → 𝐵 ∈ ℝ)
78		simpl2 1065	. . . . . . . . . . . 12 ⊢ ((((((((𝜑 ∧ 𝑥 ∈ ℝ⁺) ∧ 𝑎 ∈ ℝ⁺) ∧ ∀𝑧 ∈ (𝐴 ∩ (-∞(,)𝐵))((𝑧 ≠ 𝐵 ∧ (abs‘(𝑧 − 𝐵)) < 𝑎) → (abs‘(((𝐹 ↾ (-∞(,)𝐵))‘𝑧) − 𝐿)) < 𝑥)) ∧ 𝑏 ∈ ℝ⁺) ∧ ∀𝑧 ∈ (𝐴 ∩ (𝐵(,)+∞))((𝑧 ≠ 𝐵 ∧ (abs‘(𝑧 − 𝐵)) < 𝑏) → (abs‘(((𝐹 ↾ (𝐵(,)+∞))‘𝑧) − 𝐿)) < 𝑥)) ∧ 𝑧 ∈ 𝐴 ∧ (𝑧 ≠ 𝐵 ∧ (abs‘(𝑧 − 𝐵)) < if(𝑎 ≤ 𝑏, 𝑎, 𝑏))) ∧ ¬ 𝑧 < 𝐵) → 𝑧 ∈ 𝐴)
79	76, 78, 26	syl2anc 693	. . . . . . . . . . 11 ⊢ ((((((((𝜑 ∧ 𝑥 ∈ ℝ⁺) ∧ 𝑎 ∈ ℝ⁺) ∧ ∀𝑧 ∈ (𝐴 ∩ (-∞(,)𝐵))((𝑧 ≠ 𝐵 ∧ (abs‘(𝑧 − 𝐵)) < 𝑎) → (abs‘(((𝐹 ↾ (-∞(,)𝐵))‘𝑧) − 𝐿)) < 𝑥)) ∧ 𝑏 ∈ ℝ⁺) ∧ ∀𝑧 ∈ (𝐴 ∩ (𝐵(,)+∞))((𝑧 ≠ 𝐵 ∧ (abs‘(𝑧 − 𝐵)) < 𝑏) → (abs‘(((𝐹 ↾ (𝐵(,)+∞))‘𝑧) − 𝐿)) < 𝑥)) ∧ 𝑧 ∈ 𝐴 ∧ (𝑧 ≠ 𝐵 ∧ (abs‘(𝑧 − 𝐵)) < if(𝑎 ≤ 𝑏, 𝑎, 𝑏))) ∧ ¬ 𝑧 < 𝐵) → 𝑧 ∈ ℝ)
80		id 22	. . . . . . . . . . . . . 14 ⊢ (𝑧 ≠ 𝐵 → 𝑧 ≠ 𝐵)
81	80	necomd 2849	. . . . . . . . . . . . 13 ⊢ (𝑧 ≠ 𝐵 → 𝐵 ≠ 𝑧)
82	81	ad2antrr 762	. . . . . . . . . . . 12 ⊢ (((𝑧 ≠ 𝐵 ∧ (abs‘(𝑧 − 𝐵)) < if(𝑎 ≤ 𝑏, 𝑎, 𝑏)) ∧ ¬ 𝑧 < 𝐵) → 𝐵 ≠ 𝑧)
83	82	3ad2antl3 1225	. . . . . . . . . . 11 ⊢ ((((((((𝜑 ∧ 𝑥 ∈ ℝ⁺) ∧ 𝑎 ∈ ℝ⁺) ∧ ∀𝑧 ∈ (𝐴 ∩ (-∞(,)𝐵))((𝑧 ≠ 𝐵 ∧ (abs‘(𝑧 − 𝐵)) < 𝑎) → (abs‘(((𝐹 ↾ (-∞(,)𝐵))‘𝑧) − 𝐿)) < 𝑥)) ∧ 𝑏 ∈ ℝ⁺) ∧ ∀𝑧 ∈ (𝐴 ∩ (𝐵(,)+∞))((𝑧 ≠ 𝐵 ∧ (abs‘(𝑧 − 𝐵)) < 𝑏) → (abs‘(((𝐹 ↾ (𝐵(,)+∞))‘𝑧) − 𝐿)) < 𝑥)) ∧ 𝑧 ∈ 𝐴 ∧ (𝑧 ≠ 𝐵 ∧ (abs‘(𝑧 − 𝐵)) < if(𝑎 ≤ 𝑏, 𝑎, 𝑏))) ∧ ¬ 𝑧 < 𝐵) → 𝐵 ≠ 𝑧)
84		simpr 477	. . . . . . . . . . 11 ⊢ ((((((((𝜑 ∧ 𝑥 ∈ ℝ⁺) ∧ 𝑎 ∈ ℝ⁺) ∧ ∀𝑧 ∈ (𝐴 ∩ (-∞(,)𝐵))((𝑧 ≠ 𝐵 ∧ (abs‘(𝑧 − 𝐵)) < 𝑎) → (abs‘(((𝐹 ↾ (-∞(,)𝐵))‘𝑧) − 𝐿)) < 𝑥)) ∧ 𝑏 ∈ ℝ⁺) ∧ ∀𝑧 ∈ (𝐴 ∩ (𝐵(,)+∞))((𝑧 ≠ 𝐵 ∧ (abs‘(𝑧 − 𝐵)) < 𝑏) → (abs‘(((𝐹 ↾ (𝐵(,)+∞))‘𝑧) − 𝐿)) < 𝑥)) ∧ 𝑧 ∈ 𝐴 ∧ (𝑧 ≠ 𝐵 ∧ (abs‘(𝑧 − 𝐵)) < if(𝑎 ≤ 𝑏, 𝑎, 𝑏))) ∧ ¬ 𝑧 < 𝐵) → ¬ 𝑧 < 𝐵)
85	77, 79, 83, 84	lttri5d 39513	. . . . . . . . . 10 ⊢ ((((((((𝜑 ∧ 𝑥 ∈ ℝ⁺) ∧ 𝑎 ∈ ℝ⁺) ∧ ∀𝑧 ∈ (𝐴 ∩ (-∞(,)𝐵))((𝑧 ≠ 𝐵 ∧ (abs‘(𝑧 − 𝐵)) < 𝑎) → (abs‘(((𝐹 ↾ (-∞(,)𝐵))‘𝑧) − 𝐿)) < 𝑥)) ∧ 𝑏 ∈ ℝ⁺) ∧ ∀𝑧 ∈ (𝐴 ∩ (𝐵(,)+∞))((𝑧 ≠ 𝐵 ∧ (abs‘(𝑧 − 𝐵)) < 𝑏) → (abs‘(((𝐹 ↾ (𝐵(,)+∞))‘𝑧) − 𝐿)) < 𝑥)) ∧ 𝑧 ∈ 𝐴 ∧ (𝑧 ≠ 𝐵 ∧ (abs‘(𝑧 − 𝐵)) < if(𝑎 ≤ 𝑏, 𝑎, 𝑏))) ∧ ¬ 𝑧 < 𝐵) → 𝐵 < 𝑧)
86		simp-6l 810	. . . . . . . . . . . . . 14 ⊢ (((((((𝜑 ∧ 𝑥 ∈ ℝ⁺) ∧ 𝑎 ∈ ℝ⁺) ∧ ∀𝑧 ∈ (𝐴 ∩ (-∞(,)𝐵))((𝑧 ≠ 𝐵 ∧ (abs‘(𝑧 − 𝐵)) < 𝑎) → (abs‘(((𝐹 ↾ (-∞(,)𝐵))‘𝑧) − 𝐿)) < 𝑥)) ∧ 𝑏 ∈ ℝ⁺) ∧ ∀𝑧 ∈ (𝐴 ∩ (𝐵(,)+∞))((𝑧 ≠ 𝐵 ∧ (abs‘(𝑧 − 𝐵)) < 𝑏) → (abs‘(((𝐹 ↾ (𝐵(,)+∞))‘𝑧) − 𝐿)) < 𝑥)) ∧ 𝐵 < 𝑧) → 𝜑)
87	86	3ad2antl1 1223	. . . . . . . . . . . . 13 ⊢ ((((((((𝜑 ∧ 𝑥 ∈ ℝ⁺) ∧ 𝑎 ∈ ℝ⁺) ∧ ∀𝑧 ∈ (𝐴 ∩ (-∞(,)𝐵))((𝑧 ≠ 𝐵 ∧ (abs‘(𝑧 − 𝐵)) < 𝑎) → (abs‘(((𝐹 ↾ (-∞(,)𝐵))‘𝑧) − 𝐿)) < 𝑥)) ∧ 𝑏 ∈ ℝ⁺) ∧ ∀𝑧 ∈ (𝐴 ∩ (𝐵(,)+∞))((𝑧 ≠ 𝐵 ∧ (abs‘(𝑧 − 𝐵)) < 𝑏) → (abs‘(((𝐹 ↾ (𝐵(,)+∞))‘𝑧) − 𝐿)) < 𝑥)) ∧ 𝑧 ∈ 𝐴 ∧ (𝑧 ≠ 𝐵 ∧ (abs‘(𝑧 − 𝐵)) < if(𝑎 ≤ 𝑏, 𝑎, 𝑏))) ∧ 𝐵 < 𝑧) → 𝜑)
88		simpl2 1065	. . . . . . . . . . . . 13 ⊢ ((((((((𝜑 ∧ 𝑥 ∈ ℝ⁺) ∧ 𝑎 ∈ ℝ⁺) ∧ ∀𝑧 ∈ (𝐴 ∩ (-∞(,)𝐵))((𝑧 ≠ 𝐵 ∧ (abs‘(𝑧 − 𝐵)) < 𝑎) → (abs‘(((𝐹 ↾ (-∞(,)𝐵))‘𝑧) − 𝐿)) < 𝑥)) ∧ 𝑏 ∈ ℝ⁺) ∧ ∀𝑧 ∈ (𝐴 ∩ (𝐵(,)+∞))((𝑧 ≠ 𝐵 ∧ (abs‘(𝑧 − 𝐵)) < 𝑏) → (abs‘(((𝐹 ↾ (𝐵(,)+∞))‘𝑧) − 𝐿)) < 𝑥)) ∧ 𝑧 ∈ 𝐴 ∧ (𝑧 ≠ 𝐵 ∧ (abs‘(𝑧 − 𝐵)) < if(𝑎 ≤ 𝑏, 𝑎, 𝑏))) ∧ 𝐵 < 𝑧) → 𝑧 ∈ 𝐴)
89		simpr 477	. . . . . . . . . . . . 13 ⊢ ((((((((𝜑 ∧ 𝑥 ∈ ℝ⁺) ∧ 𝑎 ∈ ℝ⁺) ∧ ∀𝑧 ∈ (𝐴 ∩ (-∞(,)𝐵))((𝑧 ≠ 𝐵 ∧ (abs‘(𝑧 − 𝐵)) < 𝑎) → (abs‘(((𝐹 ↾ (-∞(,)𝐵))‘𝑧) − 𝐿)) < 𝑥)) ∧ 𝑏 ∈ ℝ⁺) ∧ ∀𝑧 ∈ (𝐴 ∩ (𝐵(,)+∞))((𝑧 ≠ 𝐵 ∧ (abs‘(𝑧 − 𝐵)) < 𝑏) → (abs‘(((𝐹 ↾ (𝐵(,)+∞))‘𝑧) − 𝐿)) < 𝑥)) ∧ 𝑧 ∈ 𝐴 ∧ (𝑧 ≠ 𝐵 ∧ (abs‘(𝑧 − 𝐵)) < if(𝑎 ≤ 𝑏, 𝑎, 𝑏))) ∧ 𝐵 < 𝑧) → 𝐵 < 𝑧)
90	23	3ad2ant1 1082	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝐴 ∧ 𝐵 < 𝑧) → 𝐵 ∈ ℝ^*)
91		pnfxr 10092	. . . . . . . . . . . . . . 15 ⊢ +∞ ∈ ℝ^*
92	91	a1i 11	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝐴 ∧ 𝐵 < 𝑧) → +∞ ∈ ℝ^*)
93	26	3adant3 1081	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝐴 ∧ 𝐵 < 𝑧) → 𝑧 ∈ ℝ)
94		simp3 1063	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝐴 ∧ 𝐵 < 𝑧) → 𝐵 < 𝑧)
95	93	ltpnfd 11955	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝐴 ∧ 𝐵 < 𝑧) → 𝑧 < +∞)
96	90, 92, 93, 94, 95	eliood 39720	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝐴 ∧ 𝐵 < 𝑧) → 𝑧 ∈ (𝐵(,)+∞))
97	87, 88, 89, 96	syl3anc 1326	. . . . . . . . . . . 12 ⊢ ((((((((𝜑 ∧ 𝑥 ∈ ℝ⁺) ∧ 𝑎 ∈ ℝ⁺) ∧ ∀𝑧 ∈ (𝐴 ∩ (-∞(,)𝐵))((𝑧 ≠ 𝐵 ∧ (abs‘(𝑧 − 𝐵)) < 𝑎) → (abs‘(((𝐹 ↾ (-∞(,)𝐵))‘𝑧) − 𝐿)) < 𝑥)) ∧ 𝑏 ∈ ℝ⁺) ∧ ∀𝑧 ∈ (𝐴 ∩ (𝐵(,)+∞))((𝑧 ≠ 𝐵 ∧ (abs‘(𝑧 − 𝐵)) < 𝑏) → (abs‘(((𝐹 ↾ (𝐵(,)+∞))‘𝑧) − 𝐿)) < 𝑥)) ∧ 𝑧 ∈ 𝐴 ∧ (𝑧 ≠ 𝐵 ∧ (abs‘(𝑧 − 𝐵)) < if(𝑎 ≤ 𝑏, 𝑎, 𝑏))) ∧ 𝐵 < 𝑧) → 𝑧 ∈ (𝐵(,)+∞))
98		fvres 6207	. . . . . . . . . . . . . . 15 ⊢ (𝑧 ∈ (𝐵(,)+∞) → ((𝐹 ↾ (𝐵(,)+∞))‘𝑧) = (𝐹‘𝑧))
99	98	eqcomd 2628	. . . . . . . . . . . . . 14 ⊢ (𝑧 ∈ (𝐵(,)+∞) → (𝐹‘𝑧) = ((𝐹 ↾ (𝐵(,)+∞))‘𝑧))
100	99	oveq1d 6665	. . . . . . . . . . . . 13 ⊢ (𝑧 ∈ (𝐵(,)+∞) → ((𝐹‘𝑧) − 𝐿) = (((𝐹 ↾ (𝐵(,)+∞))‘𝑧) − 𝐿))
101	100	fveq2d 6195	. . . . . . . . . . . 12 ⊢ (𝑧 ∈ (𝐵(,)+∞) → (abs‘((𝐹‘𝑧) − 𝐿)) = (abs‘(((𝐹 ↾ (𝐵(,)+∞))‘𝑧) − 𝐿)))
102	97, 101	syl 17	. . . . . . . . . . 11 ⊢ ((((((((𝜑 ∧ 𝑥 ∈ ℝ⁺) ∧ 𝑎 ∈ ℝ⁺) ∧ ∀𝑧 ∈ (𝐴 ∩ (-∞(,)𝐵))((𝑧 ≠ 𝐵 ∧ (abs‘(𝑧 − 𝐵)) < 𝑎) → (abs‘(((𝐹 ↾ (-∞(,)𝐵))‘𝑧) − 𝐿)) < 𝑥)) ∧ 𝑏 ∈ ℝ⁺) ∧ ∀𝑧 ∈ (𝐴 ∩ (𝐵(,)+∞))((𝑧 ≠ 𝐵 ∧ (abs‘(𝑧 − 𝐵)) < 𝑏) → (abs‘(((𝐹 ↾ (𝐵(,)+∞))‘𝑧) − 𝐿)) < 𝑥)) ∧ 𝑧 ∈ 𝐴 ∧ (𝑧 ≠ 𝐵 ∧ (abs‘(𝑧 − 𝐵)) < if(𝑎 ≤ 𝑏, 𝑎, 𝑏))) ∧ 𝐵 < 𝑧) → (abs‘((𝐹‘𝑧) − 𝐿)) = (abs‘(((𝐹 ↾ (𝐵(,)+∞))‘𝑧) − 𝐿)))
103		simpl1r 1113	. . . . . . . . . . . . 13 ⊢ ((((((((𝜑 ∧ 𝑥 ∈ ℝ⁺) ∧ 𝑎 ∈ ℝ⁺) ∧ ∀𝑧 ∈ (𝐴 ∩ (-∞(,)𝐵))((𝑧 ≠ 𝐵 ∧ (abs‘(𝑧 − 𝐵)) < 𝑎) → (abs‘(((𝐹 ↾ (-∞(,)𝐵))‘𝑧) − 𝐿)) < 𝑥)) ∧ 𝑏 ∈ ℝ⁺) ∧ ∀𝑧 ∈ (𝐴 ∩ (𝐵(,)+∞))((𝑧 ≠ 𝐵 ∧ (abs‘(𝑧 − 𝐵)) < 𝑏) → (abs‘(((𝐹 ↾ (𝐵(,)+∞))‘𝑧) − 𝐿)) < 𝑥)) ∧ 𝑧 ∈ 𝐴 ∧ (𝑧 ≠ 𝐵 ∧ (abs‘(𝑧 − 𝐵)) < if(𝑎 ≤ 𝑏, 𝑎, 𝑏))) ∧ 𝐵 < 𝑧) → ∀𝑧 ∈ (𝐴 ∩ (𝐵(,)+∞))((𝑧 ≠ 𝐵 ∧ (abs‘(𝑧 − 𝐵)) < 𝑏) → (abs‘(((𝐹 ↾ (𝐵(,)+∞))‘𝑧) − 𝐿)) < 𝑥))
104	88, 97	elind 3798	. . . . . . . . . . . . 13 ⊢ ((((((((𝜑 ∧ 𝑥 ∈ ℝ⁺) ∧ 𝑎 ∈ ℝ⁺) ∧ ∀𝑧 ∈ (𝐴 ∩ (-∞(,)𝐵))((𝑧 ≠ 𝐵 ∧ (abs‘(𝑧 − 𝐵)) < 𝑎) → (abs‘(((𝐹 ↾ (-∞(,)𝐵))‘𝑧) − 𝐿)) < 𝑥)) ∧ 𝑏 ∈ ℝ⁺) ∧ ∀𝑧 ∈ (𝐴 ∩ (𝐵(,)+∞))((𝑧 ≠ 𝐵 ∧ (abs‘(𝑧 − 𝐵)) < 𝑏) → (abs‘(((𝐹 ↾ (𝐵(,)+∞))‘𝑧) − 𝐿)) < 𝑥)) ∧ 𝑧 ∈ 𝐴 ∧ (𝑧 ≠ 𝐵 ∧ (abs‘(𝑧 − 𝐵)) < if(𝑎 ≤ 𝑏, 𝑎, 𝑏))) ∧ 𝐵 < 𝑧) → 𝑧 ∈ (𝐴 ∩ (𝐵(,)+∞)))
105	103, 104	jca 554	. . . . . . . . . . . 12 ⊢ ((((((((𝜑 ∧ 𝑥 ∈ ℝ⁺) ∧ 𝑎 ∈ ℝ⁺) ∧ ∀𝑧 ∈ (𝐴 ∩ (-∞(,)𝐵))((𝑧 ≠ 𝐵 ∧ (abs‘(𝑧 − 𝐵)) < 𝑎) → (abs‘(((𝐹 ↾ (-∞(,)𝐵))‘𝑧) − 𝐿)) < 𝑥)) ∧ 𝑏 ∈ ℝ⁺) ∧ ∀𝑧 ∈ (𝐴 ∩ (𝐵(,)+∞))((𝑧 ≠ 𝐵 ∧ (abs‘(𝑧 − 𝐵)) < 𝑏) → (abs‘(((𝐹 ↾ (𝐵(,)+∞))‘𝑧) − 𝐿)) < 𝑥)) ∧ 𝑧 ∈ 𝐴 ∧ (𝑧 ≠ 𝐵 ∧ (abs‘(𝑧 − 𝐵)) < if(𝑎 ≤ 𝑏, 𝑎, 𝑏))) ∧ 𝐵 < 𝑧) → (∀𝑧 ∈ (𝐴 ∩ (𝐵(,)+∞))((𝑧 ≠ 𝐵 ∧ (abs‘(𝑧 − 𝐵)) < 𝑏) → (abs‘(((𝐹 ↾ (𝐵(,)+∞))‘𝑧) − 𝐿)) < 𝑥) ∧ 𝑧 ∈ (𝐴 ∩ (𝐵(,)+∞))))
106		simpl3l 1116	. . . . . . . . . . . . 13 ⊢ ((((((((𝜑 ∧ 𝑥 ∈ ℝ⁺) ∧ 𝑎 ∈ ℝ⁺) ∧ ∀𝑧 ∈ (𝐴 ∩ (-∞(,)𝐵))((𝑧 ≠ 𝐵 ∧ (abs‘(𝑧 − 𝐵)) < 𝑎) → (abs‘(((𝐹 ↾ (-∞(,)𝐵))‘𝑧) − 𝐿)) < 𝑥)) ∧ 𝑏 ∈ ℝ⁺) ∧ ∀𝑧 ∈ (𝐴 ∩ (𝐵(,)+∞))((𝑧 ≠ 𝐵 ∧ (abs‘(𝑧 − 𝐵)) < 𝑏) → (abs‘(((𝐹 ↾ (𝐵(,)+∞))‘𝑧) − 𝐿)) < 𝑥)) ∧ 𝑧 ∈ 𝐴 ∧ (𝑧 ≠ 𝐵 ∧ (abs‘(𝑧 − 𝐵)) < if(𝑎 ≤ 𝑏, 𝑎, 𝑏))) ∧ 𝐵 < 𝑧) → 𝑧 ≠ 𝐵)
107	4	adantr 481	. . . . . . . . . . . . . . 15 ⊢ (((((((𝜑 ∧ 𝑥 ∈ ℝ⁺) ∧ 𝑎 ∈ ℝ⁺) ∧ ∀𝑧 ∈ (𝐴 ∩ (-∞(,)𝐵))((𝑧 ≠ 𝐵 ∧ (abs‘(𝑧 − 𝐵)) < 𝑎) → (abs‘(((𝐹 ↾ (-∞(,)𝐵))‘𝑧) − 𝐿)) < 𝑥)) ∧ 𝑏 ∈ ℝ⁺) ∧ ∀𝑧 ∈ (𝐴 ∩ (𝐵(,)+∞))((𝑧 ≠ 𝐵 ∧ (abs‘(𝑧 − 𝐵)) < 𝑏) → (abs‘(((𝐹 ↾ (𝐵(,)+∞))‘𝑧) − 𝐿)) < 𝑥)) ∧ 𝐵 < 𝑧) → 𝑎 ∈ ℝ⁺)
108	107	3ad2antl1 1223	. . . . . . . . . . . . . 14 ⊢ ((((((((𝜑 ∧ 𝑥 ∈ ℝ⁺) ∧ 𝑎 ∈ ℝ⁺) ∧ ∀𝑧 ∈ (𝐴 ∩ (-∞(,)𝐵))((𝑧 ≠ 𝐵 ∧ (abs‘(𝑧 − 𝐵)) < 𝑎) → (abs‘(((𝐹 ↾ (-∞(,)𝐵))‘𝑧) − 𝐿)) < 𝑥)) ∧ 𝑏 ∈ ℝ⁺) ∧ ∀𝑧 ∈ (𝐴 ∩ (𝐵(,)+∞))((𝑧 ≠ 𝐵 ∧ (abs‘(𝑧 − 𝐵)) < 𝑏) → (abs‘(((𝐹 ↾ (𝐵(,)+∞))‘𝑧) − 𝐿)) < 𝑥)) ∧ 𝑧 ∈ 𝐴 ∧ (𝑧 ≠ 𝐵 ∧ (abs‘(𝑧 − 𝐵)) < if(𝑎 ≤ 𝑏, 𝑎, 𝑏))) ∧ 𝐵 < 𝑧) → 𝑎 ∈ ℝ⁺)
109	5	adantr 481	. . . . . . . . . . . . . . 15 ⊢ (((((((𝜑 ∧ 𝑥 ∈ ℝ⁺) ∧ 𝑎 ∈ ℝ⁺) ∧ ∀𝑧 ∈ (𝐴 ∩ (-∞(,)𝐵))((𝑧 ≠ 𝐵 ∧ (abs‘(𝑧 − 𝐵)) < 𝑎) → (abs‘(((𝐹 ↾ (-∞(,)𝐵))‘𝑧) − 𝐿)) < 𝑥)) ∧ 𝑏 ∈ ℝ⁺) ∧ ∀𝑧 ∈ (𝐴 ∩ (𝐵(,)+∞))((𝑧 ≠ 𝐵 ∧ (abs‘(𝑧 − 𝐵)) < 𝑏) → (abs‘(((𝐹 ↾ (𝐵(,)+∞))‘𝑧) − 𝐿)) < 𝑥)) ∧ 𝐵 < 𝑧) → 𝑏 ∈ ℝ⁺)
110	109	3ad2antl1 1223	. . . . . . . . . . . . . 14 ⊢ ((((((((𝜑 ∧ 𝑥 ∈ ℝ⁺) ∧ 𝑎 ∈ ℝ⁺) ∧ ∀𝑧 ∈ (𝐴 ∩ (-∞(,)𝐵))((𝑧 ≠ 𝐵 ∧ (abs‘(𝑧 − 𝐵)) < 𝑎) → (abs‘(((𝐹 ↾ (-∞(,)𝐵))‘𝑧) − 𝐿)) < 𝑥)) ∧ 𝑏 ∈ ℝ⁺) ∧ ∀𝑧 ∈ (𝐴 ∩ (𝐵(,)+∞))((𝑧 ≠ 𝐵 ∧ (abs‘(𝑧 − 𝐵)) < 𝑏) → (abs‘(((𝐹 ↾ (𝐵(,)+∞))‘𝑧) − 𝐿)) < 𝑥)) ∧ 𝑧 ∈ 𝐴 ∧ (𝑧 ≠ 𝐵 ∧ (abs‘(𝑧 − 𝐵)) < if(𝑎 ≤ 𝑏, 𝑎, 𝑏))) ∧ 𝐵 < 𝑧) → 𝑏 ∈ ℝ⁺)
111		simpl3r 1117	. . . . . . . . . . . . . 14 ⊢ ((((((((𝜑 ∧ 𝑥 ∈ ℝ⁺) ∧ 𝑎 ∈ ℝ⁺) ∧ ∀𝑧 ∈ (𝐴 ∩ (-∞(,)𝐵))((𝑧 ≠ 𝐵 ∧ (abs‘(𝑧 − 𝐵)) < 𝑎) → (abs‘(((𝐹 ↾ (-∞(,)𝐵))‘𝑧) − 𝐿)) < 𝑥)) ∧ 𝑏 ∈ ℝ⁺) ∧ ∀𝑧 ∈ (𝐴 ∩ (𝐵(,)+∞))((𝑧 ≠ 𝐵 ∧ (abs‘(𝑧 − 𝐵)) < 𝑏) → (abs‘(((𝐹 ↾ (𝐵(,)+∞))‘𝑧) − 𝐿)) < 𝑥)) ∧ 𝑧 ∈ 𝐴 ∧ (𝑧 ≠ 𝐵 ∧ (abs‘(𝑧 − 𝐵)) < if(𝑎 ≤ 𝑏, 𝑎, 𝑏))) ∧ 𝐵 < 𝑧) → (abs‘(𝑧 − 𝐵)) < if(𝑎 ≤ 𝑏, 𝑎, 𝑏))
112	65	adantr 481	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑎 ∈ ℝ⁺ ∧ 𝑏 ∈ ℝ⁺) ∧ ((abs‘(𝑧 − 𝐵)) < if(𝑎 ≤ 𝑏, 𝑎, 𝑏) ∧ 𝑧 ∈ 𝐴)) → 𝑏 ∈ ℝ)
113		min2 12021	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) → if(𝑎 ≤ 𝑏, 𝑎, 𝑏) ≤ 𝑏)
114	62, 65, 113	syl2anc 693	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑎 ∈ ℝ⁺ ∧ 𝑏 ∈ ℝ⁺) → if(𝑎 ≤ 𝑏, 𝑎, 𝑏) ≤ 𝑏)
115	114	adantr 481	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑎 ∈ ℝ⁺ ∧ 𝑏 ∈ ℝ⁺) ∧ ((abs‘(𝑧 − 𝐵)) < if(𝑎 ≤ 𝑏, 𝑎, 𝑏) ∧ 𝑧 ∈ 𝐴)) → if(𝑎 ≤ 𝑏, 𝑎, 𝑏) ≤ 𝑏)
116	54, 61, 112, 64, 115	ltletrd 10197	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑎 ∈ ℝ⁺ ∧ 𝑏 ∈ ℝ⁺) ∧ ((abs‘(𝑧 − 𝐵)) < if(𝑎 ≤ 𝑏, 𝑎, 𝑏) ∧ 𝑧 ∈ 𝐴)) → (abs‘(𝑧 − 𝐵)) < 𝑏)
117	87, 108, 110, 111, 88, 116	syl32anc 1334	. . . . . . . . . . . . 13 ⊢ ((((((((𝜑 ∧ 𝑥 ∈ ℝ⁺) ∧ 𝑎 ∈ ℝ⁺) ∧ ∀𝑧 ∈ (𝐴 ∩ (-∞(,)𝐵))((𝑧 ≠ 𝐵 ∧ (abs‘(𝑧 − 𝐵)) < 𝑎) → (abs‘(((𝐹 ↾ (-∞(,)𝐵))‘𝑧) − 𝐿)) < 𝑥)) ∧ 𝑏 ∈ ℝ⁺) ∧ ∀𝑧 ∈ (𝐴 ∩ (𝐵(,)+∞))((𝑧 ≠ 𝐵 ∧ (abs‘(𝑧 − 𝐵)) < 𝑏) → (abs‘(((𝐹 ↾ (𝐵(,)+∞))‘𝑧) − 𝐿)) < 𝑥)) ∧ 𝑧 ∈ 𝐴 ∧ (𝑧 ≠ 𝐵 ∧ (abs‘(𝑧 − 𝐵)) < if(𝑎 ≤ 𝑏, 𝑎, 𝑏))) ∧ 𝐵 < 𝑧) → (abs‘(𝑧 − 𝐵)) < 𝑏)
118	106, 117	jca 554	. . . . . . . . . . . 12 ⊢ ((((((((𝜑 ∧ 𝑥 ∈ ℝ⁺) ∧ 𝑎 ∈ ℝ⁺) ∧ ∀𝑧 ∈ (𝐴 ∩ (-∞(,)𝐵))((𝑧 ≠ 𝐵 ∧ (abs‘(𝑧 − 𝐵)) < 𝑎) → (abs‘(((𝐹 ↾ (-∞(,)𝐵))‘𝑧) − 𝐿)) < 𝑥)) ∧ 𝑏 ∈ ℝ⁺) ∧ ∀𝑧 ∈ (𝐴 ∩ (𝐵(,)+∞))((𝑧 ≠ 𝐵 ∧ (abs‘(𝑧 − 𝐵)) < 𝑏) → (abs‘(((𝐹 ↾ (𝐵(,)+∞))‘𝑧) − 𝐿)) < 𝑥)) ∧ 𝑧 ∈ 𝐴 ∧ (𝑧 ≠ 𝐵 ∧ (abs‘(𝑧 − 𝐵)) < if(𝑎 ≤ 𝑏, 𝑎, 𝑏))) ∧ 𝐵 < 𝑧) → (𝑧 ≠ 𝐵 ∧ (abs‘(𝑧 − 𝐵)) < 𝑏))
119		rspa 2930	. . . . . . . . . . . 12 ⊢ ((∀𝑧 ∈ (𝐴 ∩ (𝐵(,)+∞))((𝑧 ≠ 𝐵 ∧ (abs‘(𝑧 − 𝐵)) < 𝑏) → (abs‘(((𝐹 ↾ (𝐵(,)+∞))‘𝑧) − 𝐿)) < 𝑥) ∧ 𝑧 ∈ (𝐴 ∩ (𝐵(,)+∞))) → ((𝑧 ≠ 𝐵 ∧ (abs‘(𝑧 − 𝐵)) < 𝑏) → (abs‘(((𝐹 ↾ (𝐵(,)+∞))‘𝑧) − 𝐿)) < 𝑥))
120	105, 118, 119	sylc 65	. . . . . . . . . . 11 ⊢ ((((((((𝜑 ∧ 𝑥 ∈ ℝ⁺) ∧ 𝑎 ∈ ℝ⁺) ∧ ∀𝑧 ∈ (𝐴 ∩ (-∞(,)𝐵))((𝑧 ≠ 𝐵 ∧ (abs‘(𝑧 − 𝐵)) < 𝑎) → (abs‘(((𝐹 ↾ (-∞(,)𝐵))‘𝑧) − 𝐿)) < 𝑥)) ∧ 𝑏 ∈ ℝ⁺) ∧ ∀𝑧 ∈ (𝐴 ∩ (𝐵(,)+∞))((𝑧 ≠ 𝐵 ∧ (abs‘(𝑧 − 𝐵)) < 𝑏) → (abs‘(((𝐹 ↾ (𝐵(,)+∞))‘𝑧) − 𝐿)) < 𝑥)) ∧ 𝑧 ∈ 𝐴 ∧ (𝑧 ≠ 𝐵 ∧ (abs‘(𝑧 − 𝐵)) < if(𝑎 ≤ 𝑏, 𝑎, 𝑏))) ∧ 𝐵 < 𝑧) → (abs‘(((𝐹 ↾ (𝐵(,)+∞))‘𝑧) − 𝐿)) < 𝑥)
121	102, 120	eqbrtrd 4675	. . . . . . . . . 10 ⊢ ((((((((𝜑 ∧ 𝑥 ∈ ℝ⁺) ∧ 𝑎 ∈ ℝ⁺) ∧ ∀𝑧 ∈ (𝐴 ∩ (-∞(,)𝐵))((𝑧 ≠ 𝐵 ∧ (abs‘(𝑧 − 𝐵)) < 𝑎) → (abs‘(((𝐹 ↾ (-∞(,)𝐵))‘𝑧) − 𝐿)) < 𝑥)) ∧ 𝑏 ∈ ℝ⁺) ∧ ∀𝑧 ∈ (𝐴 ∩ (𝐵(,)+∞))((𝑧 ≠ 𝐵 ∧ (abs‘(𝑧 − 𝐵)) < 𝑏) → (abs‘(((𝐹 ↾ (𝐵(,)+∞))‘𝑧) − 𝐿)) < 𝑥)) ∧ 𝑧 ∈ 𝐴 ∧ (𝑧 ≠ 𝐵 ∧ (abs‘(𝑧 − 𝐵)) < if(𝑎 ≤ 𝑏, 𝑎, 𝑏))) ∧ 𝐵 < 𝑧) → (abs‘((𝐹‘𝑧) − 𝐿)) < 𝑥)
122	85, 121	syldan 487	. . . . . . . . 9 ⊢ ((((((((𝜑 ∧ 𝑥 ∈ ℝ⁺) ∧ 𝑎 ∈ ℝ⁺) ∧ ∀𝑧 ∈ (𝐴 ∩ (-∞(,)𝐵))((𝑧 ≠ 𝐵 ∧ (abs‘(𝑧 − 𝐵)) < 𝑎) → (abs‘(((𝐹 ↾ (-∞(,)𝐵))‘𝑧) − 𝐿)) < 𝑥)) ∧ 𝑏 ∈ ℝ⁺) ∧ ∀𝑧 ∈ (𝐴 ∩ (𝐵(,)+∞))((𝑧 ≠ 𝐵 ∧ (abs‘(𝑧 − 𝐵)) < 𝑏) → (abs‘(((𝐹 ↾ (𝐵(,)+∞))‘𝑧) − 𝐿)) < 𝑥)) ∧ 𝑧 ∈ 𝐴 ∧ (𝑧 ≠ 𝐵 ∧ (abs‘(𝑧 − 𝐵)) < if(𝑎 ≤ 𝑏, 𝑎, 𝑏))) ∧ ¬ 𝑧 < 𝐵) → (abs‘((𝐹‘𝑧) − 𝐿)) < 𝑥)
123	74, 122	pm2.61dan 832	. . . . . . . 8 ⊢ (((((((𝜑 ∧ 𝑥 ∈ ℝ⁺) ∧ 𝑎 ∈ ℝ⁺) ∧ ∀𝑧 ∈ (𝐴 ∩ (-∞(,)𝐵))((𝑧 ≠ 𝐵 ∧ (abs‘(𝑧 − 𝐵)) < 𝑎) → (abs‘(((𝐹 ↾ (-∞(,)𝐵))‘𝑧) − 𝐿)) < 𝑥)) ∧ 𝑏 ∈ ℝ⁺) ∧ ∀𝑧 ∈ (𝐴 ∩ (𝐵(,)+∞))((𝑧 ≠ 𝐵 ∧ (abs‘(𝑧 − 𝐵)) < 𝑏) → (abs‘(((𝐹 ↾ (𝐵(,)+∞))‘𝑧) − 𝐿)) < 𝑥)) ∧ 𝑧 ∈ 𝐴 ∧ (𝑧 ≠ 𝐵 ∧ (abs‘(𝑧 − 𝐵)) < if(𝑎 ≤ 𝑏, 𝑎, 𝑏))) → (abs‘((𝐹‘𝑧) − 𝐿)) < 𝑥)
124	123	3exp 1264	. . . . . . 7 ⊢ ((((((𝜑 ∧ 𝑥 ∈ ℝ⁺) ∧ 𝑎 ∈ ℝ⁺) ∧ ∀𝑧 ∈ (𝐴 ∩ (-∞(,)𝐵))((𝑧 ≠ 𝐵 ∧ (abs‘(𝑧 − 𝐵)) < 𝑎) → (abs‘(((𝐹 ↾ (-∞(,)𝐵))‘𝑧) − 𝐿)) < 𝑥)) ∧ 𝑏 ∈ ℝ⁺) ∧ ∀𝑧 ∈ (𝐴 ∩ (𝐵(,)+∞))((𝑧 ≠ 𝐵 ∧ (abs‘(𝑧 − 𝐵)) < 𝑏) → (abs‘(((𝐹 ↾ (𝐵(,)+∞))‘𝑧) − 𝐿)) < 𝑥)) → (𝑧 ∈ 𝐴 → ((𝑧 ≠ 𝐵 ∧ (abs‘(𝑧 − 𝐵)) < if(𝑎 ≤ 𝑏, 𝑎, 𝑏)) → (abs‘((𝐹‘𝑧) − 𝐿)) < 𝑥)))
125	15, 124	ralrimi 2957	. . . . . 6 ⊢ ((((((𝜑 ∧ 𝑥 ∈ ℝ⁺) ∧ 𝑎 ∈ ℝ⁺) ∧ ∀𝑧 ∈ (𝐴 ∩ (-∞(,)𝐵))((𝑧 ≠ 𝐵 ∧ (abs‘(𝑧 − 𝐵)) < 𝑎) → (abs‘(((𝐹 ↾ (-∞(,)𝐵))‘𝑧) − 𝐿)) < 𝑥)) ∧ 𝑏 ∈ ℝ⁺) ∧ ∀𝑧 ∈ (𝐴 ∩ (𝐵(,)+∞))((𝑧 ≠ 𝐵 ∧ (abs‘(𝑧 − 𝐵)) < 𝑏) → (abs‘(((𝐹 ↾ (𝐵(,)+∞))‘𝑧) − 𝐿)) < 𝑥)) → ∀𝑧 ∈ 𝐴 ((𝑧 ≠ 𝐵 ∧ (abs‘(𝑧 − 𝐵)) < if(𝑎 ≤ 𝑏, 𝑎, 𝑏)) → (abs‘((𝐹‘𝑧) − 𝐿)) < 𝑥))
126		breq2 4657	. . . . . . . . . 10 ⊢ (𝑦 = if(𝑎 ≤ 𝑏, 𝑎, 𝑏) → ((abs‘(𝑧 − 𝐵)) < 𝑦 ↔ (abs‘(𝑧 − 𝐵)) < if(𝑎 ≤ 𝑏, 𝑎, 𝑏)))
127	126	anbi2d 740	. . . . . . . . 9 ⊢ (𝑦 = if(𝑎 ≤ 𝑏, 𝑎, 𝑏) → ((𝑧 ≠ 𝐵 ∧ (abs‘(𝑧 − 𝐵)) < 𝑦) ↔ (𝑧 ≠ 𝐵 ∧ (abs‘(𝑧 − 𝐵)) < if(𝑎 ≤ 𝑏, 𝑎, 𝑏))))
128	127	imbi1d 331	. . . . . . . 8 ⊢ (𝑦 = if(𝑎 ≤ 𝑏, 𝑎, 𝑏) → (((𝑧 ≠ 𝐵 ∧ (abs‘(𝑧 − 𝐵)) < 𝑦) → (abs‘((𝐹‘𝑧) − 𝐿)) < 𝑥) ↔ ((𝑧 ≠ 𝐵 ∧ (abs‘(𝑧 − 𝐵)) < if(𝑎 ≤ 𝑏, 𝑎, 𝑏)) → (abs‘((𝐹‘𝑧) − 𝐿)) < 𝑥)))
129	128	ralbidv 2986	. . . . . . 7 ⊢ (𝑦 = if(𝑎 ≤ 𝑏, 𝑎, 𝑏) → (∀𝑧 ∈ 𝐴 ((𝑧 ≠ 𝐵 ∧ (abs‘(𝑧 − 𝐵)) < 𝑦) → (abs‘((𝐹‘𝑧) − 𝐿)) < 𝑥) ↔ ∀𝑧 ∈ 𝐴 ((𝑧 ≠ 𝐵 ∧ (abs‘(𝑧 − 𝐵)) < if(𝑎 ≤ 𝑏, 𝑎, 𝑏)) → (abs‘((𝐹‘𝑧) − 𝐿)) < 𝑥)))
130	129	rspcev 3309	. . . . . 6 ⊢ ((if(𝑎 ≤ 𝑏, 𝑎, 𝑏) ∈ ℝ⁺ ∧ ∀𝑧 ∈ 𝐴 ((𝑧 ≠ 𝐵 ∧ (abs‘(𝑧 − 𝐵)) < if(𝑎 ≤ 𝑏, 𝑎, 𝑏)) → (abs‘((𝐹‘𝑧) − 𝐿)) < 𝑥)) → ∃𝑦 ∈ ℝ⁺ ∀𝑧 ∈ 𝐴 ((𝑧 ≠ 𝐵 ∧ (abs‘(𝑧 − 𝐵)) < 𝑦) → (abs‘((𝐹‘𝑧) − 𝐿)) < 𝑥))
131	6, 125, 130	syl2anc 693	. . . . 5 ⊢ ((((((𝜑 ∧ 𝑥 ∈ ℝ⁺) ∧ 𝑎 ∈ ℝ⁺) ∧ ∀𝑧 ∈ (𝐴 ∩ (-∞(,)𝐵))((𝑧 ≠ 𝐵 ∧ (abs‘(𝑧 − 𝐵)) < 𝑎) → (abs‘(((𝐹 ↾ (-∞(,)𝐵))‘𝑧) − 𝐿)) < 𝑥)) ∧ 𝑏 ∈ ℝ⁺) ∧ ∀𝑧 ∈ (𝐴 ∩ (𝐵(,)+∞))((𝑧 ≠ 𝐵 ∧ (abs‘(𝑧 − 𝐵)) < 𝑏) → (abs‘(((𝐹 ↾ (𝐵(,)+∞))‘𝑧) − 𝐿)) < 𝑥)) → ∃𝑦 ∈ ℝ⁺ ∀𝑧 ∈ 𝐴 ((𝑧 ≠ 𝐵 ∧ (abs‘(𝑧 − 𝐵)) < 𝑦) → (abs‘((𝐹‘𝑧) − 𝐿)) < 𝑥))
132		limcleqr.r	. . . . . . . . . 10 ⊢ (𝜑 → 𝑅 ∈ ((𝐹 ↾ (𝐵(,)+∞)) lim_ℂ 𝐵))
133		limcleqr.f	. . . . . . . . . . . 12 ⊢ (𝜑 → 𝐹:𝐴⟶ℂ)
134		fresin 6073	. . . . . . . . . . . 12 ⊢ (𝐹:𝐴⟶ℂ → (𝐹 ↾ (𝐵(,)+∞)):(𝐴 ∩ (𝐵(,)+∞))⟶ℂ)
135	133, 134	syl 17	. . . . . . . . . . 11 ⊢ (𝜑 → (𝐹 ↾ (𝐵(,)+∞)):(𝐴 ∩ (𝐵(,)+∞))⟶ℂ)
136		inss2 3834	. . . . . . . . . . . . 13 ⊢ (𝐴 ∩ (𝐵(,)+∞)) ⊆ (𝐵(,)+∞)
137		ioosscn 39716	. . . . . . . . . . . . 13 ⊢ (𝐵(,)+∞) ⊆ ℂ
138	136, 137	sstri 3612	. . . . . . . . . . . 12 ⊢ (𝐴 ∩ (𝐵(,)+∞)) ⊆ ℂ
139	138	a1i 11	. . . . . . . . . . 11 ⊢ (𝜑 → (𝐴 ∩ (𝐵(,)+∞)) ⊆ ℂ)
140	135, 139, 50	ellimc3 23643	. . . . . . . . . 10 ⊢ (𝜑 → (𝑅 ∈ ((𝐹 ↾ (𝐵(,)+∞)) lim_ℂ 𝐵) ↔ (𝑅 ∈ ℂ ∧ ∀𝑥 ∈ ℝ⁺ ∃𝑏 ∈ ℝ⁺ ∀𝑧 ∈ (𝐴 ∩ (𝐵(,)+∞))((𝑧 ≠ 𝐵 ∧ (abs‘(𝑧 − 𝐵)) < 𝑏) → (abs‘(((𝐹 ↾ (𝐵(,)+∞))‘𝑧) − 𝑅)) < 𝑥))))
141	132, 140	mpbid 222	. . . . . . . . 9 ⊢ (𝜑 → (𝑅 ∈ ℂ ∧ ∀𝑥 ∈ ℝ⁺ ∃𝑏 ∈ ℝ⁺ ∀𝑧 ∈ (𝐴 ∩ (𝐵(,)+∞))((𝑧 ≠ 𝐵 ∧ (abs‘(𝑧 − 𝐵)) < 𝑏) → (abs‘(((𝐹 ↾ (𝐵(,)+∞))‘𝑧) − 𝑅)) < 𝑥)))
142	141	simprd 479	. . . . . . . 8 ⊢ (𝜑 → ∀𝑥 ∈ ℝ⁺ ∃𝑏 ∈ ℝ⁺ ∀𝑧 ∈ (𝐴 ∩ (𝐵(,)+∞))((𝑧 ≠ 𝐵 ∧ (abs‘(𝑧 − 𝐵)) < 𝑏) → (abs‘(((𝐹 ↾ (𝐵(,)+∞))‘𝑧) − 𝑅)) < 𝑥))
143	142	r19.21bi 2932	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ⁺) → ∃𝑏 ∈ ℝ⁺ ∀𝑧 ∈ (𝐴 ∩ (𝐵(,)+∞))((𝑧 ≠ 𝐵 ∧ (abs‘(𝑧 − 𝐵)) < 𝑏) → (abs‘(((𝐹 ↾ (𝐵(,)+∞))‘𝑧) − 𝑅)) < 𝑥))
144		limcleqr.leqr	. . . . . . . . . . . . 13 ⊢ (𝜑 → 𝐿 = 𝑅)
145	144	oveq2d 6666	. . . . . . . . . . . 12 ⊢ (𝜑 → (((𝐹 ↾ (𝐵(,)+∞))‘𝑧) − 𝐿) = (((𝐹 ↾ (𝐵(,)+∞))‘𝑧) − 𝑅))
146	145	fveq2d 6195	. . . . . . . . . . 11 ⊢ (𝜑 → (abs‘(((𝐹 ↾ (𝐵(,)+∞))‘𝑧) − 𝐿)) = (abs‘(((𝐹 ↾ (𝐵(,)+∞))‘𝑧) − 𝑅)))
147	146	breq1d 4663	. . . . . . . . . 10 ⊢ (𝜑 → ((abs‘(((𝐹 ↾ (𝐵(,)+∞))‘𝑧) − 𝐿)) < 𝑥 ↔ (abs‘(((𝐹 ↾ (𝐵(,)+∞))‘𝑧) − 𝑅)) < 𝑥))
148	147	imbi2d 330	. . . . . . . . 9 ⊢ (𝜑 → (((𝑧 ≠ 𝐵 ∧ (abs‘(𝑧 − 𝐵)) < 𝑏) → (abs‘(((𝐹 ↾ (𝐵(,)+∞))‘𝑧) − 𝐿)) < 𝑥) ↔ ((𝑧 ≠ 𝐵 ∧ (abs‘(𝑧 − 𝐵)) < 𝑏) → (abs‘(((𝐹 ↾ (𝐵(,)+∞))‘𝑧) − 𝑅)) < 𝑥)))
149	148	rexralbidv 3058	. . . . . . . 8 ⊢ (𝜑 → (∃𝑏 ∈ ℝ⁺ ∀𝑧 ∈ (𝐴 ∩ (𝐵(,)+∞))((𝑧 ≠ 𝐵 ∧ (abs‘(𝑧 − 𝐵)) < 𝑏) → (abs‘(((𝐹 ↾ (𝐵(,)+∞))‘𝑧) − 𝐿)) < 𝑥) ↔ ∃𝑏 ∈ ℝ⁺ ∀𝑧 ∈ (𝐴 ∩ (𝐵(,)+∞))((𝑧 ≠ 𝐵 ∧ (abs‘(𝑧 − 𝐵)) < 𝑏) → (abs‘(((𝐹 ↾ (𝐵(,)+∞))‘𝑧) − 𝑅)) < 𝑥)))
150	149	adantr 481	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ⁺) → (∃𝑏 ∈ ℝ⁺ ∀𝑧 ∈ (𝐴 ∩ (𝐵(,)+∞))((𝑧 ≠ 𝐵 ∧ (abs‘(𝑧 − 𝐵)) < 𝑏) → (abs‘(((𝐹 ↾ (𝐵(,)+∞))‘𝑧) − 𝐿)) < 𝑥) ↔ ∃𝑏 ∈ ℝ⁺ ∀𝑧 ∈ (𝐴 ∩ (𝐵(,)+∞))((𝑧 ≠ 𝐵 ∧ (abs‘(𝑧 − 𝐵)) < 𝑏) → (abs‘(((𝐹 ↾ (𝐵(,)+∞))‘𝑧) − 𝑅)) < 𝑥)))
151	143, 150	mpbird 247	. . . . . 6 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ⁺) → ∃𝑏 ∈ ℝ⁺ ∀𝑧 ∈ (𝐴 ∩ (𝐵(,)+∞))((𝑧 ≠ 𝐵 ∧ (abs‘(𝑧 − 𝐵)) < 𝑏) → (abs‘(((𝐹 ↾ (𝐵(,)+∞))‘𝑧) − 𝐿)) < 𝑥))
152	151	ad2antrr 762	. . . . 5 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ⁺) ∧ 𝑎 ∈ ℝ⁺) ∧ ∀𝑧 ∈ (𝐴 ∩ (-∞(,)𝐵))((𝑧 ≠ 𝐵 ∧ (abs‘(𝑧 − 𝐵)) < 𝑎) → (abs‘(((𝐹 ↾ (-∞(,)𝐵))‘𝑧) − 𝐿)) < 𝑥)) → ∃𝑏 ∈ ℝ⁺ ∀𝑧 ∈ (𝐴 ∩ (𝐵(,)+∞))((𝑧 ≠ 𝐵 ∧ (abs‘(𝑧 − 𝐵)) < 𝑏) → (abs‘(((𝐹 ↾ (𝐵(,)+∞))‘𝑧) − 𝐿)) < 𝑥))
153	131, 152	r19.29a 3078	. . . 4 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ⁺) ∧ 𝑎 ∈ ℝ⁺) ∧ ∀𝑧 ∈ (𝐴 ∩ (-∞(,)𝐵))((𝑧 ≠ 𝐵 ∧ (abs‘(𝑧 − 𝐵)) < 𝑎) → (abs‘(((𝐹 ↾ (-∞(,)𝐵))‘𝑧) − 𝐿)) < 𝑥)) → ∃𝑦 ∈ ℝ⁺ ∀𝑧 ∈ 𝐴 ((𝑧 ≠ 𝐵 ∧ (abs‘(𝑧 − 𝐵)) < 𝑦) → (abs‘((𝐹‘𝑧) − 𝐿)) < 𝑥))
154		fresin 6073	. . . . . . . . 9 ⊢ (𝐹:𝐴⟶ℂ → (𝐹 ↾ (-∞(,)𝐵)):(𝐴 ∩ (-∞(,)𝐵))⟶ℂ)
155	133, 154	syl 17	. . . . . . . 8 ⊢ (𝜑 → (𝐹 ↾ (-∞(,)𝐵)):(𝐴 ∩ (-∞(,)𝐵))⟶ℂ)
156		inss2 3834	. . . . . . . . . 10 ⊢ (𝐴 ∩ (-∞(,)𝐵)) ⊆ (-∞(,)𝐵)
157		ioossre 12235	. . . . . . . . . 10 ⊢ (-∞(,)𝐵) ⊆ ℝ
158	156, 157	sstri 3612	. . . . . . . . 9 ⊢ (𝐴 ∩ (-∞(,)𝐵)) ⊆ ℝ
159		ax-resscn 9993	. . . . . . . . . 10 ⊢ ℝ ⊆ ℂ
160	159	a1i 11	. . . . . . . . 9 ⊢ (𝜑 → ℝ ⊆ ℂ)
161	158, 160	syl5ss 3614	. . . . . . . 8 ⊢ (𝜑 → (𝐴 ∩ (-∞(,)𝐵)) ⊆ ℂ)
162	155, 161, 50	ellimc3 23643	. . . . . . 7 ⊢ (𝜑 → (𝐿 ∈ ((𝐹 ↾ (-∞(,)𝐵)) lim_ℂ 𝐵) ↔ (𝐿 ∈ ℂ ∧ ∀𝑥 ∈ ℝ⁺ ∃𝑎 ∈ ℝ⁺ ∀𝑧 ∈ (𝐴 ∩ (-∞(,)𝐵))((𝑧 ≠ 𝐵 ∧ (abs‘(𝑧 − 𝐵)) < 𝑎) → (abs‘(((𝐹 ↾ (-∞(,)𝐵))‘𝑧) − 𝐿)) < 𝑥))))
163	2, 162	mpbid 222	. . . . . 6 ⊢ (𝜑 → (𝐿 ∈ ℂ ∧ ∀𝑥 ∈ ℝ⁺ ∃𝑎 ∈ ℝ⁺ ∀𝑧 ∈ (𝐴 ∩ (-∞(,)𝐵))((𝑧 ≠ 𝐵 ∧ (abs‘(𝑧 − 𝐵)) < 𝑎) → (abs‘(((𝐹 ↾ (-∞(,)𝐵))‘𝑧) − 𝐿)) < 𝑥)))
164	163	simprd 479	. . . . 5 ⊢ (𝜑 → ∀𝑥 ∈ ℝ⁺ ∃𝑎 ∈ ℝ⁺ ∀𝑧 ∈ (𝐴 ∩ (-∞(,)𝐵))((𝑧 ≠ 𝐵 ∧ (abs‘(𝑧 − 𝐵)) < 𝑎) → (abs‘(((𝐹 ↾ (-∞(,)𝐵))‘𝑧) − 𝐿)) < 𝑥))
165	164	r19.21bi 2932	. . . 4 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ⁺) → ∃𝑎 ∈ ℝ⁺ ∀𝑧 ∈ (𝐴 ∩ (-∞(,)𝐵))((𝑧 ≠ 𝐵 ∧ (abs‘(𝑧 − 𝐵)) < 𝑎) → (abs‘(((𝐹 ↾ (-∞(,)𝐵))‘𝑧) − 𝐿)) < 𝑥))
166	153, 165	r19.29a 3078	. . 3 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ⁺) → ∃𝑦 ∈ ℝ⁺ ∀𝑧 ∈ 𝐴 ((𝑧 ≠ 𝐵 ∧ (abs‘(𝑧 − 𝐵)) < 𝑦) → (abs‘((𝐹‘𝑧) − 𝐿)) < 𝑥))
167	166	ralrimiva 2966	. 2 ⊢ (𝜑 → ∀𝑥 ∈ ℝ⁺ ∃𝑦 ∈ ℝ⁺ ∀𝑧 ∈ 𝐴 ((𝑧 ≠ 𝐵 ∧ (abs‘(𝑧 − 𝐵)) < 𝑦) → (abs‘((𝐹‘𝑧) − 𝐿)) < 𝑥))
168	25, 159	syl6ss 3615	. . 3 ⊢ (𝜑 → 𝐴 ⊆ ℂ)
169	133, 168, 50	ellimc3 23643	. 2 ⊢ (𝜑 → (𝐿 ∈ (𝐹 lim_ℂ 𝐵) ↔ (𝐿 ∈ ℂ ∧ ∀𝑥 ∈ ℝ⁺ ∃𝑦 ∈ ℝ⁺ ∀𝑧 ∈ 𝐴 ((𝑧 ≠ 𝐵 ∧ (abs‘(𝑧 − 𝐵)) < 𝑦) → (abs‘((𝐹‘𝑧) − 𝐿)) < 𝑥))))
170	3, 167, 169	mpbir2and 957	1 ⊢ (𝜑 → 𝐿 ∈ (𝐹 lim_ℂ 𝐵))

Colors of variables: wff setvar class

Syntax hints: ¬ wn 3 → wi 4 ↔ wb 196 ∧ wa 384 ∧ w3a 1037 = wceq 1483 ∈ wcel 1990 ≠ wne 2794 ∀wral 2912 ∃wrex 2913 ∩ cin 3573 ⊆ wss 3574 ifcif 4086 class class class wbr 4653 ran crn 5115 ↾ cres 5116 ⟶wf 5884 ‘cfv 5888 (class class class)co 6650 ℂcc 9934 ℝcr 9935 +∞cpnf 10071 -∞cmnf 10072 ℝ^*cxr 10073 < clt 10074 ≤ cle 10075 − cmin 10266 ℝ⁺crp 11832 (,)cioo 12175 abscabs 13974 TopOpenctopn 16082 topGenctg 16098 ℂ_fldccnfld 19746 lim_ℂ climc 23626

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1722 ax-4 1737 ax-5 1839 ax-6 1888 ax-7 1935 ax-8 1992 ax-9 1999 ax-10 2019 ax-11 2034 ax-12 2047 ax-13 2246 ax-ext 2602 ax-rep 4771 ax-sep 4781 ax-nul 4789 ax-pow 4843 ax-pr 4906 ax-un 6949 ax-cnex 9992 ax-resscn 9993 ax-1cn 9994 ax-icn 9995 ax-addcl 9996 ax-addrcl 9997 ax-mulcl 9998 ax-mulrcl 9999 ax-mulcom 10000 ax-addass 10001 ax-mulass 10002 ax-distr 10003 ax-i2m1 10004 ax-1ne0 10005 ax-1rid 10006 ax-rnegex 10007 ax-rrecex 10008 ax-cnre 10009 ax-pre-lttri 10010 ax-pre-lttrn 10011 ax-pre-ltadd 10012 ax-pre-mulgt0 10013 ax-pre-sup 10014

This theorem depends on definitions: df-bi 197 df-or 385 df-an 386 df-3or 1038 df-3an 1039 df-tru 1486 df-ex 1705 df-nf 1710 df-sb 1881 df-eu 2474 df-mo 2475 df-clab 2609 df-cleq 2615 df-clel 2618 df-nfc 2753 df-ne 2795 df-nel 2898 df-ral 2917 df-rex 2918 df-reu 2919 df-rmo 2920 df-rab 2921 df-v 3202 df-sbc 3436 df-csb 3534 df-dif 3577 df-un 3579 df-in 3581 df-ss 3588 df-pss 3590 df-nul 3916 df-if 4087 df-pw 4160 df-sn 4178 df-pr 4180 df-tp 4182 df-op 4184 df-uni 4437 df-int 4476 df-iun 4522 df-br 4654 df-opab 4713 df-mpt 4730 df-tr 4753 df-id 5024 df-eprel 5029 df-po 5035 df-so 5036 df-fr 5073 df-we 5075 df-xp 5120 df-rel 5121 df-cnv 5122 df-co 5123 df-dm 5124 df-rn 5125 df-res 5126 df-ima 5127 df-pred 5680 df-ord 5726 df-on 5727 df-lim 5728 df-suc 5729 df-iota 5851 df-fun 5890 df-fn 5891 df-f 5892 df-f1 5893 df-fo 5894 df-f1o 5895 df-fv 5896 df-riota 6611 df-ov 6653 df-oprab 6654 df-mpt2 6655 df-om 7066 df-1st 7168 df-2nd 7169 df-wrecs 7407 df-recs 7468 df-rdg 7506 df-1o 7560 df-oadd 7564 df-er 7742 df-map 7859 df-pm 7860 df-en 7956 df-dom 7957 df-sdom 7958 df-fin 7959 df-fi 8317 df-sup 8348 df-inf 8349 df-pnf 10076 df-mnf 10077 df-xr 10078 df-ltxr 10079 df-le 10080 df-sub 10268 df-neg 10269 df-div 10685 df-nn 11021 df-2 11079 df-3 11080 df-4 11081 df-5 11082 df-6 11083 df-7 11084 df-8 11085 df-9 11086 df-n0 11293 df-z 11378 df-dec 11494 df-uz 11688 df-q 11789 df-rp 11833 df-xneg 11946 df-xadd 11947 df-xmul 11948 df-ioo 12179 df-fz 12327 df-seq 12802 df-exp 12861 df-cj 13839 df-re 13840 df-im 13841 df-sqrt 13975 df-abs 13976 df-struct 15859 df-ndx 15860 df-slot 15861 df-base 15863 df-plusg 15954 df-mulr 15955 df-starv 15956 df-tset 15960 df-ple 15961 df-ds 15964 df-unif 15965 df-rest 16083 df-topn 16084 df-topgen 16104 df-psmet 19738 df-xmet 19739 df-met 19740 df-bl 19741 df-mopn 19742 df-cnfld 19747 df-top 20699 df-topon 20716 df-topsp 20737 df-bases 20750 df-cnp 21032 df-xms 22125 df-ms 22126 df-limc 23630

This theorem is referenced by: limclr 39887

W3C validator