limcleqr

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)

	Ref	Expression
Hypotheses	limcleqr.k	$⊢ K = TopOpen (ℂ_{fld})$
	limcleqr.a	$⊢ φ \to A \subseteq ℝ$
	limcleqr.j	$⊢ J = topGen (ran (.))$
	limcleqr.f	$⊢ φ \to F : A ⟶ ℂ$
	limcleqr.b	$⊢ φ \to B \in ℝ$
	limcleqr.l	$⊢ φ \to L \in (({F ↾}_{(−∞, B)}) {lim}_{ℂ} B)$
	limcleqr.r	$⊢ φ \to R \in (({F ↾}_{(B, +∞)}) {lim}_{ℂ} B)$
	limcleqr.leqr	$⊢ φ \to L = R$
Assertion	limcleqr	$⊢ φ \to L \in (F {lim}_{ℂ} B)$

Proof

Step	Hyp	Ref	Expression
1		limcleqr.k	$⊢ K = TopOpen (ℂ_{fld})$
2		limcleqr.a	$⊢ φ \to A \subseteq ℝ$
3		limcleqr.j	$⊢ J = topGen (ran (.))$
4		limcleqr.f	$⊢ φ \to F : A ⟶ ℂ$
5		limcleqr.b	$⊢ φ \to B \in ℝ$
6		limcleqr.l	$⊢ φ \to L \in (({F ↾}_{(−∞, B)}) {lim}_{ℂ} B)$
7		limcleqr.r	$⊢ φ \to R \in (({F ↾}_{(B, +∞)}) {lim}_{ℂ} B)$
8		limcleqr.leqr	$⊢ φ \to L = R$
9		limccl	$⊢ ({F ↾}_{(−∞, B)}) {lim}_{ℂ} B \subseteq ℂ$
10	9 6	sselid	$⊢ φ \to L \in ℂ$
11		simp-4r	$⊢ (((((φ \land x \in ℝ^{+}) \land a \in ℝ^{+}) \land \forall z \in (A \cap (−∞, B)) ((z \neq B \land \|z - B\| < a) \to \|({F ↾}_{(−∞, B)}) (z) - L\| < x)) \land b \in ℝ^{+}) \land \forall z \in (A \cap (B, +∞)) ((z \neq B \land \|z - B\| < b) \to \|({F ↾}_{(B, +∞)}) (z) - L\| < x)) \to a \in ℝ^{+}$
12		simplr	$⊢ (((((φ \land x \in ℝ^{+}) \land a \in ℝ^{+}) \land \forall z \in (A \cap (−∞, B)) ((z \neq B \land \|z - B\| < a) \to \|({F ↾}_{(−∞, B)}) (z) - L\| < x)) \land b \in ℝ^{+}) \land \forall z \in (A \cap (B, +∞)) ((z \neq B \land \|z - B\| < b) \to \|({F ↾}_{(B, +∞)}) (z) - L\| < x)) \to b \in ℝ^{+}$
13	11 12	ifcld	$⊢ (((((φ \land x \in ℝ^{+}) \land a \in ℝ^{+}) \land \forall z \in (A \cap (−∞, B)) ((z \neq B \land \|z - B\| < a) \to \|({F ↾}_{(−∞, B)}) (z) - L\| < x)) \land b \in ℝ^{+}) \land \forall z \in (A \cap (B, +∞)) ((z \neq B \land \|z - B\| < b) \to \|({F ↾}_{(B, +∞)}) (z) - L\| < x)) \to if (a \leq b, a, b) \in ℝ^{+}$
14		nfv	$⊢ Ⅎ z (φ \land x \in ℝ^{+})$
15		nfv	$⊢ Ⅎ z a \in ℝ^{+}$
16	14 15	nfan	$⊢ Ⅎ z ((φ \land x \in ℝ^{+}) \land a \in ℝ^{+})$
17		nfra1	$⊢ Ⅎ z \forall z \in (A \cap (−∞, B)) ((z \neq B \land \|z - B\| < a) \to \|({F ↾}_{(−∞, B)}) (z) - L\| < x)$
18	16 17	nfan	$⊢ Ⅎ z (((φ \land x \in ℝ^{+}) \land a \in ℝ^{+}) \land \forall z \in (A \cap (−∞, B)) ((z \neq B \land \|z - B\| < a) \to \|({F ↾}_{(−∞, B)}) (z) - L\| < x))$
19		nfv	$⊢ Ⅎ z b \in ℝ^{+}$
20	18 19	nfan	$⊢ Ⅎ z ((((φ \land x \in ℝ^{+}) \land a \in ℝ^{+}) \land \forall z \in (A \cap (−∞, B)) ((z \neq B \land \|z - B\| < a) \to \|({F ↾}_{(−∞, B)}) (z) - L\| < x)) \land b \in ℝ^{+})$
21		nfra1	$⊢ Ⅎ z \forall z \in (A \cap (B, +∞)) ((z \neq B \land \|z - B\| < b) \to \|({F ↾}_{(B, +∞)}) (z) - L\| < x)$
22	20 21	nfan	$⊢ Ⅎ z (((((φ \land x \in ℝ^{+}) \land a \in ℝ^{+}) \land \forall z \in (A \cap (−∞, B)) ((z \neq B \land \|z - B\| < a) \to \|({F ↾}_{(−∞, B)}) (z) - L\| < x)) \land b \in ℝ^{+}) \land \forall z \in (A \cap (B, +∞)) ((z \neq B \land \|z - B\| < b) \to \|({F ↾}_{(B, +∞)}) (z) - L\| < x))$
23		simp-6l	$⊢ ((((((φ \land x \in ℝ^{+}) \land a \in ℝ^{+}) \land \forall z \in (A \cap (−∞, B)) ((z \neq B \land \|z - B\| < a) \to \|({F ↾}_{(−∞, B)}) (z) - L\| < x)) \land b \in ℝ^{+}) \land \forall z \in (A \cap (B, +∞)) ((z \neq B \land \|z - B\| < b) \to \|({F ↾}_{(B, +∞)}) (z) - L\| < x)) \land z < B) \to φ$
24	23	3ad2antl1	$⊢ (((((((φ \land x \in ℝ^{+}) \land a \in ℝ^{+}) \land \forall z \in (A \cap (−∞, B)) ((z \neq B \land \|z - B\| < a) \to \|({F ↾}_{(−∞, B)}) (z) - L\| < x)) \land b \in ℝ^{+}) \land \forall z \in (A \cap (B, +∞)) ((z \neq B \land \|z - B\| < b) \to \|({F ↾}_{(B, +∞)}) (z) - L\| < x)) \land z \in A \land (z \neq B \land \|z - B\| < if (a \leq b, a, b))) \land z < B) \to φ$
25		simpl2	$⊢ (((((((φ \land x \in ℝ^{+}) \land a \in ℝ^{+}) \land \forall z \in (A \cap (−∞, B)) ((z \neq B \land \|z - B\| < a) \to \|({F ↾}_{(−∞, B)}) (z) - L\| < x)) \land b \in ℝ^{+}) \land \forall z \in (A \cap (B, +∞)) ((z \neq B \land \|z - B\| < b) \to \|({F ↾}_{(B, +∞)}) (z) - L\| < x)) \land z \in A \land (z \neq B \land \|z - B\| < if (a \leq b, a, b))) \land z < B) \to z \in A$
26		simpr	$⊢ (((((((φ \land x \in ℝ^{+}) \land a \in ℝ^{+}) \land \forall z \in (A \cap (−∞, B)) ((z \neq B \land \|z - B\| < a) \to \|({F ↾}_{(−∞, B)}) (z) - L\| < x)) \land b \in ℝ^{+}) \land \forall z \in (A \cap (B, +∞)) ((z \neq B \land \|z - B\| < b) \to \|({F ↾}_{(B, +∞)}) (z) - L\| < x)) \land z \in A \land (z \neq B \land \|z - B\| < if (a \leq b, a, b))) \land z < B) \to z < B$
27		mnfxr	$⊢ −∞ \in ℝ^{*}$
28	27	a1i	$⊢ (φ \land z \in A \land z < B) \to −∞ \in ℝ^{*}$
29	5	rexrd	$⊢ φ \to B \in ℝ^{*}$
30	29	3ad2ant1	$⊢ (φ \land z \in A \land z < B) \to B \in ℝ^{*}$
31	2	sselda	$⊢ (φ \land z \in A) \to z \in ℝ$
32	31	3adant3	$⊢ (φ \land z \in A \land z < B) \to z \in ℝ$
33	32	mnfltd	$⊢ (φ \land z \in A \land z < B) \to −∞ < z$
34		simp3	$⊢ (φ \land z \in A \land z < B) \to z < B$
35	28 30 32 33 34	eliood	$⊢ (φ \land z \in A \land z < B) \to z \in (−∞, B)$
36	24 25 26 35	syl3anc	$⊢ (((((((φ \land x \in ℝ^{+}) \land a \in ℝ^{+}) \land \forall z \in (A \cap (−∞, B)) ((z \neq B \land \|z - B\| < a) \to \|({F ↾}_{(−∞, B)}) (z) - L\| < x)) \land b \in ℝ^{+}) \land \forall z \in (A \cap (B, +∞)) ((z \neq B \land \|z - B\| < b) \to \|({F ↾}_{(B, +∞)}) (z) - L\| < x)) \land z \in A \land (z \neq B \land \|z - B\| < if (a \leq b, a, b))) \land z < B) \to z \in (−∞, B)$
37		fvres	$⊢ z \in (−∞, B) \to ({F ↾}_{(−∞, B)}) (z) = F (z)$
38	37	oveq1d	$⊢ z \in (−∞, B) \to ({F ↾}_{(−∞, B)}) (z) - L = F (z) - L$
39	38	eqcomd	$⊢ z \in (−∞, B) \to F (z) - L = ({F ↾}_{(−∞, B)}) (z) - L$
40	39	fveq2d	$⊢ z \in (−∞, B) \to \|F (z) - L\| = \|({F ↾}_{(−∞, B)}) (z) - L\|$
41	36 40	syl	$⊢ (((((((φ \land x \in ℝ^{+}) \land a \in ℝ^{+}) \land \forall z \in (A \cap (−∞, B)) ((z \neq B \land \|z - B\| < a) \to \|({F ↾}_{(−∞, B)}) (z) - L\| < x)) \land b \in ℝ^{+}) \land \forall z \in (A \cap (B, +∞)) ((z \neq B \land \|z - B\| < b) \to \|({F ↾}_{(B, +∞)}) (z) - L\| < x)) \land z \in A \land (z \neq B \land \|z - B\| < if (a \leq b, a, b))) \land z < B) \to \|F (z) - L\| = \|({F ↾}_{(−∞, B)}) (z) - L\|$
42		simp-4r	$⊢ ((((((φ \land x \in ℝ^{+}) \land a \in ℝ^{+}) \land \forall z \in (A \cap (−∞, B)) ((z \neq B \land \|z - B\| < a) \to \|({F ↾}_{(−∞, B)}) (z) - L\| < x)) \land b \in ℝ^{+}) \land \forall z \in (A \cap (B, +∞)) ((z \neq B \land \|z - B\| < b) \to \|({F ↾}_{(B, +∞)}) (z) - L\| < x)) \land z < B) \to \forall z \in (A \cap (−∞, B)) ((z \neq B \land \|z - B\| < a) \to \|({F ↾}_{(−∞, B)}) (z) - L\| < x)$
43	42	3ad2antl1	$⊢ (((((((φ \land x \in ℝ^{+}) \land a \in ℝ^{+}) \land \forall z \in (A \cap (−∞, B)) ((z \neq B \land \|z - B\| < a) \to \|({F ↾}_{(−∞, B)}) (z) - L\| < x)) \land b \in ℝ^{+}) \land \forall z \in (A \cap (B, +∞)) ((z \neq B \land \|z - B\| < b) \to \|({F ↾}_{(B, +∞)}) (z) - L\| < x)) \land z \in A \land (z \neq B \land \|z - B\| < if (a \leq b, a, b))) \land z < B) \to \forall z \in (A \cap (−∞, B)) ((z \neq B \land \|z - B\| < a) \to \|({F ↾}_{(−∞, B)}) (z) - L\| < x)$
44	25 36	elind	$⊢ (((((((φ \land x \in ℝ^{+}) \land a \in ℝ^{+}) \land \forall z \in (A \cap (−∞, B)) ((z \neq B \land \|z - B\| < a) \to \|({F ↾}_{(−∞, B)}) (z) - L\| < x)) \land b \in ℝ^{+}) \land \forall z \in (A \cap (B, +∞)) ((z \neq B \land \|z - B\| < b) \to \|({F ↾}_{(B, +∞)}) (z) - L\| < x)) \land z \in A \land (z \neq B \land \|z - B\| < if (a \leq b, a, b))) \land z < B) \to z \in (A \cap (−∞, B))$
45	43 44	jca	$⊢ (((((((φ \land x \in ℝ^{+}) \land a \in ℝ^{+}) \land \forall z \in (A \cap (−∞, B)) ((z \neq B \land \|z - B\| < a) \to \|({F ↾}_{(−∞, B)}) (z) - L\| < x)) \land b \in ℝ^{+}) \land \forall z \in (A \cap (B, +∞)) ((z \neq B \land \|z - B\| < b) \to \|({F ↾}_{(B, +∞)}) (z) - L\| < x)) \land z \in A \land (z \neq B \land \|z - B\| < if (a \leq b, a, b))) \land z < B) \to (\forall z \in (A \cap (−∞, B)) ((z \neq B \land \|z - B\| < a) \to \|({F ↾}_{(−∞, B)}) (z) - L\| < x) \land z \in (A \cap (−∞, B)))$
46		simpl3l	$⊢ (((((((φ \land x \in ℝ^{+}) \land a \in ℝ^{+}) \land \forall z \in (A \cap (−∞, B)) ((z \neq B \land \|z - B\| < a) \to \|({F ↾}_{(−∞, B)}) (z) - L\| < x)) \land b \in ℝ^{+}) \land \forall z \in (A \cap (B, +∞)) ((z \neq B \land \|z - B\| < b) \to \|({F ↾}_{(B, +∞)}) (z) - L\| < x)) \land z \in A \land (z \neq B \land \|z - B\| < if (a \leq b, a, b))) \land z < B) \to z \neq B$
47	11	adantr	$⊢ ((((((φ \land x \in ℝ^{+}) \land a \in ℝ^{+}) \land \forall z \in (A \cap (−∞, B)) ((z \neq B \land \|z - B\| < a) \to \|({F ↾}_{(−∞, B)}) (z) - L\| < x)) \land b \in ℝ^{+}) \land \forall z \in (A \cap (B, +∞)) ((z \neq B \land \|z - B\| < b) \to \|({F ↾}_{(B, +∞)}) (z) - L\| < x)) \land z < B) \to a \in ℝ^{+}$
48	47	3ad2antl1	$⊢ (((((((φ \land x \in ℝ^{+}) \land a \in ℝ^{+}) \land \forall z \in (A \cap (−∞, B)) ((z \neq B \land \|z - B\| < a) \to \|({F ↾}_{(−∞, B)}) (z) - L\| < x)) \land b \in ℝ^{+}) \land \forall z \in (A \cap (B, +∞)) ((z \neq B \land \|z - B\| < b) \to \|({F ↾}_{(B, +∞)}) (z) - L\| < x)) \land z \in A \land (z \neq B \land \|z - B\| < if (a \leq b, a, b))) \land z < B) \to a \in ℝ^{+}$
49	12	adantr	$⊢ ((((((φ \land x \in ℝ^{+}) \land a \in ℝ^{+}) \land \forall z \in (A \cap (−∞, B)) ((z \neq B \land \|z - B\| < a) \to \|({F ↾}_{(−∞, B)}) (z) - L\| < x)) \land b \in ℝ^{+}) \land \forall z \in (A \cap (B, +∞)) ((z \neq B \land \|z - B\| < b) \to \|({F ↾}_{(B, +∞)}) (z) - L\| < x)) \land z < B) \to b \in ℝ^{+}$
50	49	3ad2antl1	$⊢ (((((((φ \land x \in ℝ^{+}) \land a \in ℝ^{+}) \land \forall z \in (A \cap (−∞, B)) ((z \neq B \land \|z - B\| < a) \to \|({F ↾}_{(−∞, B)}) (z) - L\| < x)) \land b \in ℝ^{+}) \land \forall z \in (A \cap (B, +∞)) ((z \neq B \land \|z - B\| < b) \to \|({F ↾}_{(B, +∞)}) (z) - L\| < x)) \land z \in A \land (z \neq B \land \|z - B\| < if (a \leq b, a, b))) \land z < B) \to b \in ℝ^{+}$
51		simpl3r	$⊢ (((((((φ \land x \in ℝ^{+}) \land a \in ℝ^{+}) \land \forall z \in (A \cap (−∞, B)) ((z \neq B \land \|z - B\| < a) \to \|({F ↾}_{(−∞, B)}) (z) - L\| < x)) \land b \in ℝ^{+}) \land \forall z \in (A \cap (B, +∞)) ((z \neq B \land \|z - B\| < b) \to \|({F ↾}_{(B, +∞)}) (z) - L\| < x)) \land z \in A \land (z \neq B \land \|z - B\| < if (a \leq b, a, b))) \land z < B) \to \|z - B\| < if (a \leq b, a, b)$
52		simpl1	$⊢ ((φ \land a \in ℝ^{+} \land b \in ℝ^{+}) \land (\|z - B\| < if (a \leq b, a, b) \land z \in A)) \to φ$
53		simprr	$⊢ ((φ \land a \in ℝ^{+} \land b \in ℝ^{+}) \land (\|z - B\| < if (a \leq b, a, b) \land z \in A)) \to z \in A$
54	31	recnd	$⊢ (φ \land z \in A) \to z \in ℂ$
55	5	recnd	$⊢ φ \to B \in ℂ$
56	55	adantr	$⊢ (φ \land z \in A) \to B \in ℂ$
57	54 56	subcld	$⊢ (φ \land z \in A) \to z - B \in ℂ$
58	57	abscld	$⊢ (φ \land z \in A) \to \|z - B\| \in ℝ$
59	52 53 58	syl2anc	$⊢ ((φ \land a \in ℝ^{+} \land b \in ℝ^{+}) \land (\|z - B\| < if (a \leq b, a, b) \land z \in A)) \to \|z - B\| \in ℝ$
60		rpre	$⊢ a \in ℝ^{+} \to a \in ℝ$
61	60	adantr	$⊢ (a \in ℝ^{+} \land b \in ℝ^{+}) \to a \in ℝ$
62		rpre	$⊢ b \in ℝ^{+} \to b \in ℝ$
63	62	adantl	$⊢ (a \in ℝ^{+} \land b \in ℝ^{+}) \to b \in ℝ$
64	61 63	ifcld	$⊢ (a \in ℝ^{+} \land b \in ℝ^{+}) \to if (a \leq b, a, b) \in ℝ$
65	64	3adant1	$⊢ (φ \land a \in ℝ^{+} \land b \in ℝ^{+}) \to if (a \leq b, a, b) \in ℝ$
66	65	adantr	$⊢ ((φ \land a \in ℝ^{+} \land b \in ℝ^{+}) \land (\|z - B\| < if (a \leq b, a, b) \land z \in A)) \to if (a \leq b, a, b) \in ℝ$
67	61	3adant1	$⊢ (φ \land a \in ℝ^{+} \land b \in ℝ^{+}) \to a \in ℝ$
68	67	adantr	$⊢ ((φ \land a \in ℝ^{+} \land b \in ℝ^{+}) \land (\|z - B\| < if (a \leq b, a, b) \land z \in A)) \to a \in ℝ$
69		simprl	$⊢ ((φ \land a \in ℝ^{+} \land b \in ℝ^{+}) \land (\|z - B\| < if (a \leq b, a, b) \land z \in A)) \to \|z - B\| < if (a \leq b, a, b)$
70	63	3adant1	$⊢ (φ \land a \in ℝ^{+} \land b \in ℝ^{+}) \to b \in ℝ$
71		min1	$⊢ (a \in ℝ \land b \in ℝ) \to if (a \leq b, a, b) \leq a$
72	67 70 71	syl2anc	$⊢ (φ \land a \in ℝ^{+} \land b \in ℝ^{+}) \to if (a \leq b, a, b) \leq a$
73	72	adantr	$⊢ ((φ \land a \in ℝ^{+} \land b \in ℝ^{+}) \land (\|z - B\| < if (a \leq b, a, b) \land z \in A)) \to if (a \leq b, a, b) \leq a$
74	59 66 68 69 73	ltletrd	$⊢ ((φ \land a \in ℝ^{+} \land b \in ℝ^{+}) \land (\|z - B\| < if (a \leq b, a, b) \land z \in A)) \to \|z - B\| < a$
75	24 48 50 51 25 74	syl32anc	$⊢ (((((((φ \land x \in ℝ^{+}) \land a \in ℝ^{+}) \land \forall z \in (A \cap (−∞, B)) ((z \neq B \land \|z - B\| < a) \to \|({F ↾}_{(−∞, B)}) (z) - L\| < x)) \land b \in ℝ^{+}) \land \forall z \in (A \cap (B, +∞)) ((z \neq B \land \|z - B\| < b) \to \|({F ↾}_{(B, +∞)}) (z) - L\| < x)) \land z \in A \land (z \neq B \land \|z - B\| < if (a \leq b, a, b))) \land z < B) \to \|z - B\| < a$
76	46 75	jca	$⊢ (((((((φ \land x \in ℝ^{+}) \land a \in ℝ^{+}) \land \forall z \in (A \cap (−∞, B)) ((z \neq B \land \|z - B\| < a) \to \|({F ↾}_{(−∞, B)}) (z) - L\| < x)) \land b \in ℝ^{+}) \land \forall z \in (A \cap (B, +∞)) ((z \neq B \land \|z - B\| < b) \to \|({F ↾}_{(B, +∞)}) (z) - L\| < x)) \land z \in A \land (z \neq B \land \|z - B\| < if (a \leq b, a, b))) \land z < B) \to (z \neq B \land \|z - B\| < a)$
77		rspa	$⊢ (\forall z \in (A \cap (−∞, B)) ((z \neq B \land \|z - B\| < a) \to \|({F ↾}_{(−∞, B)}) (z) - L\| < x) \land z \in (A \cap (−∞, B))) \to ((z \neq B \land \|z - B\| < a) \to \|({F ↾}_{(−∞, B)}) (z) - L\| < x)$
78	45 76 77	sylc	$⊢ (((((((φ \land x \in ℝ^{+}) \land a \in ℝ^{+}) \land \forall z \in (A \cap (−∞, B)) ((z \neq B \land \|z - B\| < a) \to \|({F ↾}_{(−∞, B)}) (z) - L\| < x)) \land b \in ℝ^{+}) \land \forall z \in (A \cap (B, +∞)) ((z \neq B \land \|z - B\| < b) \to \|({F ↾}_{(B, +∞)}) (z) - L\| < x)) \land z \in A \land (z \neq B \land \|z - B\| < if (a \leq b, a, b))) \land z < B) \to \|({F ↾}_{(−∞, B)}) (z) - L\| < x$
79	41 78	eqbrtrd	$⊢ (((((((φ \land x \in ℝ^{+}) \land a \in ℝ^{+}) \land \forall z \in (A \cap (−∞, B)) ((z \neq B \land \|z - B\| < a) \to \|({F ↾}_{(−∞, B)}) (z) - L\| < x)) \land b \in ℝ^{+}) \land \forall z \in (A \cap (B, +∞)) ((z \neq B \land \|z - B\| < b) \to \|({F ↾}_{(B, +∞)}) (z) - L\| < x)) \land z \in A \land (z \neq B \land \|z - B\| < if (a \leq b, a, b))) \land z < B) \to \|F (z) - L\| < x$
80		simp-6l	$⊢ ((((((φ \land x \in ℝ^{+}) \land a \in ℝ^{+}) \land \forall z \in (A \cap (−∞, B)) ((z \neq B \land \|z - B\| < a) \to \|({F ↾}_{(−∞, B)}) (z) - L\| < x)) \land b \in ℝ^{+}) \land \forall z \in (A \cap (B, +∞)) ((z \neq B \land \|z - B\| < b) \to \|({F ↾}_{(B, +∞)}) (z) - L\| < x)) \land \neg z < B) \to φ$
81	80	3ad2antl1	$⊢ (((((((φ \land x \in ℝ^{+}) \land a \in ℝ^{+}) \land \forall z \in (A \cap (−∞, B)) ((z \neq B \land \|z - B\| < a) \to \|({F ↾}_{(−∞, B)}) (z) - L\| < x)) \land b \in ℝ^{+}) \land \forall z \in (A \cap (B, +∞)) ((z \neq B \land \|z - B\| < b) \to \|({F ↾}_{(B, +∞)}) (z) - L\| < x)) \land z \in A \land (z \neq B \land \|z - B\| < if (a \leq b, a, b))) \land \neg z < B) \to φ$
82	81 5	syl	$⊢ (((((((φ \land x \in ℝ^{+}) \land a \in ℝ^{+}) \land \forall z \in (A \cap (−∞, B)) ((z \neq B \land \|z - B\| < a) \to \|({F ↾}_{(−∞, B)}) (z) - L\| < x)) \land b \in ℝ^{+}) \land \forall z \in (A \cap (B, +∞)) ((z \neq B \land \|z - B\| < b) \to \|({F ↾}_{(B, +∞)}) (z) - L\| < x)) \land z \in A \land (z \neq B \land \|z - B\| < if (a \leq b, a, b))) \land \neg z < B) \to B \in ℝ$
83		simpl2	$⊢ (((((((φ \land x \in ℝ^{+}) \land a \in ℝ^{+}) \land \forall z \in (A \cap (−∞, B)) ((z \neq B \land \|z - B\| < a) \to \|({F ↾}_{(−∞, B)}) (z) - L\| < x)) \land b \in ℝ^{+}) \land \forall z \in (A \cap (B, +∞)) ((z \neq B \land \|z - B\| < b) \to \|({F ↾}_{(B, +∞)}) (z) - L\| < x)) \land z \in A \land (z \neq B \land \|z - B\| < if (a \leq b, a, b))) \land \neg z < B) \to z \in A$
84	81 83 31	syl2anc	$⊢ (((((((φ \land x \in ℝ^{+}) \land a \in ℝ^{+}) \land \forall z \in (A \cap (−∞, B)) ((z \neq B \land \|z - B\| < a) \to \|({F ↾}_{(−∞, B)}) (z) - L\| < x)) \land b \in ℝ^{+}) \land \forall z \in (A \cap (B, +∞)) ((z \neq B \land \|z - B\| < b) \to \|({F ↾}_{(B, +∞)}) (z) - L\| < x)) \land z \in A \land (z \neq B \land \|z - B\| < if (a \leq b, a, b))) \land \neg z < B) \to z \in ℝ$
85		id	$⊢ z \neq B \to z \neq B$
86	85	necomd	$⊢ z \neq B \to B \neq z$
87	86	ad2antrr	$⊢ ((z \neq B \land \|z - B\| < if (a \leq b, a, b)) \land \neg z < B) \to B \neq z$
88	87	3ad2antl3	$⊢ (((((((φ \land x \in ℝ^{+}) \land a \in ℝ^{+}) \land \forall z \in (A \cap (−∞, B)) ((z \neq B \land \|z - B\| < a) \to \|({F ↾}_{(−∞, B)}) (z) - L\| < x)) \land b \in ℝ^{+}) \land \forall z \in (A \cap (B, +∞)) ((z \neq B \land \|z - B\| < b) \to \|({F ↾}_{(B, +∞)}) (z) - L\| < x)) \land z \in A \land (z \neq B \land \|z - B\| < if (a \leq b, a, b))) \land \neg z < B) \to B \neq z$
89		simpr	$⊢ (((((((φ \land x \in ℝ^{+}) \land a \in ℝ^{+}) \land \forall z \in (A \cap (−∞, B)) ((z \neq B \land \|z - B\| < a) \to \|({F ↾}_{(−∞, B)}) (z) - L\| < x)) \land b \in ℝ^{+}) \land \forall z \in (A \cap (B, +∞)) ((z \neq B \land \|z - B\| < b) \to \|({F ↾}_{(B, +∞)}) (z) - L\| < x)) \land z \in A \land (z \neq B \land \|z - B\| < if (a \leq b, a, b))) \land \neg z < B) \to \neg z < B$
90	82 84 88 89	lttri5d	$⊢ (((((((φ \land x \in ℝ^{+}) \land a \in ℝ^{+}) \land \forall z \in (A \cap (−∞, B)) ((z \neq B \land \|z - B\| < a) \to \|({F ↾}_{(−∞, B)}) (z) - L\| < x)) \land b \in ℝ^{+}) \land \forall z \in (A \cap (B, +∞)) ((z \neq B \land \|z - B\| < b) \to \|({F ↾}_{(B, +∞)}) (z) - L\| < x)) \land z \in A \land (z \neq B \land \|z - B\| < if (a \leq b, a, b))) \land \neg z < B) \to B < z$
91		simp-6l	$⊢ ((((((φ \land x \in ℝ^{+}) \land a \in ℝ^{+}) \land \forall z \in (A \cap (−∞, B)) ((z \neq B \land \|z - B\| < a) \to \|({F ↾}_{(−∞, B)}) (z) - L\| < x)) \land b \in ℝ^{+}) \land \forall z \in (A \cap (B, +∞)) ((z \neq B \land \|z - B\| < b) \to \|({F ↾}_{(B, +∞)}) (z) - L\| < x)) \land B < z) \to φ$
92	91	3ad2antl1	$⊢ (((((((φ \land x \in ℝ^{+}) \land a \in ℝ^{+}) \land \forall z \in (A \cap (−∞, B)) ((z \neq B \land \|z - B\| < a) \to \|({F ↾}_{(−∞, B)}) (z) - L\| < x)) \land b \in ℝ^{+}) \land \forall z \in (A \cap (B, +∞)) ((z \neq B \land \|z - B\| < b) \to \|({F ↾}_{(B, +∞)}) (z) - L\| < x)) \land z \in A \land (z \neq B \land \|z - B\| < if (a \leq b, a, b))) \land B < z) \to φ$
93		simpl2	$⊢ (((((((φ \land x \in ℝ^{+}) \land a \in ℝ^{+}) \land \forall z \in (A \cap (−∞, B)) ((z \neq B \land \|z - B\| < a) \to \|({F ↾}_{(−∞, B)}) (z) - L\| < x)) \land b \in ℝ^{+}) \land \forall z \in (A \cap (B, +∞)) ((z \neq B \land \|z - B\| < b) \to \|({F ↾}_{(B, +∞)}) (z) - L\| < x)) \land z \in A \land (z \neq B \land \|z - B\| < if (a \leq b, a, b))) \land B < z) \to z \in A$
94		simpr	$⊢ (((((((φ \land x \in ℝ^{+}) \land a \in ℝ^{+}) \land \forall z \in (A \cap (−∞, B)) ((z \neq B \land \|z - B\| < a) \to \|({F ↾}_{(−∞, B)}) (z) - L\| < x)) \land b \in ℝ^{+}) \land \forall z \in (A \cap (B, +∞)) ((z \neq B \land \|z - B\| < b) \to \|({F ↾}_{(B, +∞)}) (z) - L\| < x)) \land z \in A \land (z \neq B \land \|z - B\| < if (a \leq b, a, b))) \land B < z) \to B < z$
95	29	3ad2ant1	$⊢ (φ \land z \in A \land B < z) \to B \in ℝ^{*}$
96		pnfxr	$⊢ +∞ \in ℝ^{*}$
97	96	a1i	$⊢ (φ \land z \in A \land B < z) \to +∞ \in ℝ^{*}$
98	31	3adant3	$⊢ (φ \land z \in A \land B < z) \to z \in ℝ$
99		simp3	$⊢ (φ \land z \in A \land B < z) \to B < z$
100	98	ltpnfd	$⊢ (φ \land z \in A \land B < z) \to z < +∞$
101	95 97 98 99 100	eliood	$⊢ (φ \land z \in A \land B < z) \to z \in (B, +∞)$
102	92 93 94 101	syl3anc	$⊢ (((((((φ \land x \in ℝ^{+}) \land a \in ℝ^{+}) \land \forall z \in (A \cap (−∞, B)) ((z \neq B \land \|z - B\| < a) \to \|({F ↾}_{(−∞, B)}) (z) - L\| < x)) \land b \in ℝ^{+}) \land \forall z \in (A \cap (B, +∞)) ((z \neq B \land \|z - B\| < b) \to \|({F ↾}_{(B, +∞)}) (z) - L\| < x)) \land z \in A \land (z \neq B \land \|z - B\| < if (a \leq b, a, b))) \land B < z) \to z \in (B, +∞)$
103		fvres	$⊢ z \in (B, +∞) \to ({F ↾}_{(B, +∞)}) (z) = F (z)$
104	103	eqcomd	$⊢ z \in (B, +∞) \to F (z) = ({F ↾}_{(B, +∞)}) (z)$
105	104	fvoveq1d	$⊢ z \in (B, +∞) \to \|F (z) - L\| = \|({F ↾}_{(B, +∞)}) (z) - L\|$
106	102 105	syl	$⊢ (((((((φ \land x \in ℝ^{+}) \land a \in ℝ^{+}) \land \forall z \in (A \cap (−∞, B)) ((z \neq B \land \|z - B\| < a) \to \|({F ↾}_{(−∞, B)}) (z) - L\| < x)) \land b \in ℝ^{+}) \land \forall z \in (A \cap (B, +∞)) ((z \neq B \land \|z - B\| < b) \to \|({F ↾}_{(B, +∞)}) (z) - L\| < x)) \land z \in A \land (z \neq B \land \|z - B\| < if (a \leq b, a, b))) \land B < z) \to \|F (z) - L\| = \|({F ↾}_{(B, +∞)}) (z) - L\|$
107		simpl1r	$⊢ (((((((φ \land x \in ℝ^{+}) \land a \in ℝ^{+}) \land \forall z \in (A \cap (−∞, B)) ((z \neq B \land \|z - B\| < a) \to \|({F ↾}_{(−∞, B)}) (z) - L\| < x)) \land b \in ℝ^{+}) \land \forall z \in (A \cap (B, +∞)) ((z \neq B \land \|z - B\| < b) \to \|({F ↾}_{(B, +∞)}) (z) - L\| < x)) \land z \in A \land (z \neq B \land \|z - B\| < if (a \leq b, a, b))) \land B < z) \to \forall z \in (A \cap (B, +∞)) ((z \neq B \land \|z - B\| < b) \to \|({F ↾}_{(B, +∞)}) (z) - L\| < x)$
108	93 102	elind	$⊢ (((((((φ \land x \in ℝ^{+}) \land a \in ℝ^{+}) \land \forall z \in (A \cap (−∞, B)) ((z \neq B \land \|z - B\| < a) \to \|({F ↾}_{(−∞, B)}) (z) - L\| < x)) \land b \in ℝ^{+}) \land \forall z \in (A \cap (B, +∞)) ((z \neq B \land \|z - B\| < b) \to \|({F ↾}_{(B, +∞)}) (z) - L\| < x)) \land z \in A \land (z \neq B \land \|z - B\| < if (a \leq b, a, b))) \land B < z) \to z \in (A \cap (B, +∞))$
109	107 108	jca	$⊢ (((((((φ \land x \in ℝ^{+}) \land a \in ℝ^{+}) \land \forall z \in (A \cap (−∞, B)) ((z \neq B \land \|z - B\| < a) \to \|({F ↾}_{(−∞, B)}) (z) - L\| < x)) \land b \in ℝ^{+}) \land \forall z \in (A \cap (B, +∞)) ((z \neq B \land \|z - B\| < b) \to \|({F ↾}_{(B, +∞)}) (z) - L\| < x)) \land z \in A \land (z \neq B \land \|z - B\| < if (a \leq b, a, b))) \land B < z) \to (\forall z \in (A \cap (B, +∞)) ((z \neq B \land \|z - B\| < b) \to \|({F ↾}_{(B, +∞)}) (z) - L\| < x) \land z \in (A \cap (B, +∞)))$
110		simpl3l	$⊢ (((((((φ \land x \in ℝ^{+}) \land a \in ℝ^{+}) \land \forall z \in (A \cap (−∞, B)) ((z \neq B \land \|z - B\| < a) \to \|({F ↾}_{(−∞, B)}) (z) - L\| < x)) \land b \in ℝ^{+}) \land \forall z \in (A \cap (B, +∞)) ((z \neq B \land \|z - B\| < b) \to \|({F ↾}_{(B, +∞)}) (z) - L\| < x)) \land z \in A \land (z \neq B \land \|z - B\| < if (a \leq b, a, b))) \land B < z) \to z \neq B$
111	11	adantr	$⊢ ((((((φ \land x \in ℝ^{+}) \land a \in ℝ^{+}) \land \forall z \in (A \cap (−∞, B)) ((z \neq B \land \|z - B\| < a) \to \|({F ↾}_{(−∞, B)}) (z) - L\| < x)) \land b \in ℝ^{+}) \land \forall z \in (A \cap (B, +∞)) ((z \neq B \land \|z - B\| < b) \to \|({F ↾}_{(B, +∞)}) (z) - L\| < x)) \land B < z) \to a \in ℝ^{+}$
112	111	3ad2antl1	$⊢ (((((((φ \land x \in ℝ^{+}) \land a \in ℝ^{+}) \land \forall z \in (A \cap (−∞, B)) ((z \neq B \land \|z - B\| < a) \to \|({F ↾}_{(−∞, B)}) (z) - L\| < x)) \land b \in ℝ^{+}) \land \forall z \in (A \cap (B, +∞)) ((z \neq B \land \|z - B\| < b) \to \|({F ↾}_{(B, +∞)}) (z) - L\| < x)) \land z \in A \land (z \neq B \land \|z - B\| < if (a \leq b, a, b))) \land B < z) \to a \in ℝ^{+}$
113	12	adantr	$⊢ ((((((φ \land x \in ℝ^{+}) \land a \in ℝ^{+}) \land \forall z \in (A \cap (−∞, B)) ((z \neq B \land \|z - B\| < a) \to \|({F ↾}_{(−∞, B)}) (z) - L\| < x)) \land b \in ℝ^{+}) \land \forall z \in (A \cap (B, +∞)) ((z \neq B \land \|z - B\| < b) \to \|({F ↾}_{(B, +∞)}) (z) - L\| < x)) \land B < z) \to b \in ℝ^{+}$
114	113	3ad2antl1	$⊢ (((((((φ \land x \in ℝ^{+}) \land a \in ℝ^{+}) \land \forall z \in (A \cap (−∞, B)) ((z \neq B \land \|z - B\| < a) \to \|({F ↾}_{(−∞, B)}) (z) - L\| < x)) \land b \in ℝ^{+}) \land \forall z \in (A \cap (B, +∞)) ((z \neq B \land \|z - B\| < b) \to \|({F ↾}_{(B, +∞)}) (z) - L\| < x)) \land z \in A \land (z \neq B \land \|z - B\| < if (a \leq b, a, b))) \land B < z) \to b \in ℝ^{+}$
115		simpl3r	$⊢ (((((((φ \land x \in ℝ^{+}) \land a \in ℝ^{+}) \land \forall z \in (A \cap (−∞, B)) ((z \neq B \land \|z - B\| < a) \to \|({F ↾}_{(−∞, B)}) (z) - L\| < x)) \land b \in ℝ^{+}) \land \forall z \in (A \cap (B, +∞)) ((z \neq B \land \|z - B\| < b) \to \|({F ↾}_{(B, +∞)}) (z) - L\| < x)) \land z \in A \land (z \neq B \land \|z - B\| < if (a \leq b, a, b))) \land B < z) \to \|z - B\| < if (a \leq b, a, b)$
116	70	adantr	$⊢ ((φ \land a \in ℝ^{+} \land b \in ℝ^{+}) \land (\|z - B\| < if (a \leq b, a, b) \land z \in A)) \to b \in ℝ$
117		min2	$⊢ (a \in ℝ \land b \in ℝ) \to if (a \leq b, a, b) \leq b$
118	67 70 117	syl2anc	$⊢ (φ \land a \in ℝ^{+} \land b \in ℝ^{+}) \to if (a \leq b, a, b) \leq b$
119	118	adantr	$⊢ ((φ \land a \in ℝ^{+} \land b \in ℝ^{+}) \land (\|z - B\| < if (a \leq b, a, b) \land z \in A)) \to if (a \leq b, a, b) \leq b$
120	59 66 116 69 119	ltletrd	$⊢ ((φ \land a \in ℝ^{+} \land b \in ℝ^{+}) \land (\|z - B\| < if (a \leq b, a, b) \land z \in A)) \to \|z - B\| < b$
121	92 112 114 115 93 120	syl32anc	$⊢ (((((((φ \land x \in ℝ^{+}) \land a \in ℝ^{+}) \land \forall z \in (A \cap (−∞, B)) ((z \neq B \land \|z - B\| < a) \to \|({F ↾}_{(−∞, B)}) (z) - L\| < x)) \land b \in ℝ^{+}) \land \forall z \in (A \cap (B, +∞)) ((z \neq B \land \|z - B\| < b) \to \|({F ↾}_{(B, +∞)}) (z) - L\| < x)) \land z \in A \land (z \neq B \land \|z - B\| < if (a \leq b, a, b))) \land B < z) \to \|z - B\| < b$
122	110 121	jca	$⊢ (((((((φ \land x \in ℝ^{+}) \land a \in ℝ^{+}) \land \forall z \in (A \cap (−∞, B)) ((z \neq B \land \|z - B\| < a) \to \|({F ↾}_{(−∞, B)}) (z) - L\| < x)) \land b \in ℝ^{+}) \land \forall z \in (A \cap (B, +∞)) ((z \neq B \land \|z - B\| < b) \to \|({F ↾}_{(B, +∞)}) (z) - L\| < x)) \land z \in A \land (z \neq B \land \|z - B\| < if (a \leq b, a, b))) \land B < z) \to (z \neq B \land \|z - B\| < b)$
123		rspa	$⊢ (\forall z \in (A \cap (B, +∞)) ((z \neq B \land \|z - B\| < b) \to \|({F ↾}_{(B, +∞)}) (z) - L\| < x) \land z \in (A \cap (B, +∞))) \to ((z \neq B \land \|z - B\| < b) \to \|({F ↾}_{(B, +∞)}) (z) - L\| < x)$
124	109 122 123	sylc	$⊢ (((((((φ \land x \in ℝ^{+}) \land a \in ℝ^{+}) \land \forall z \in (A \cap (−∞, B)) ((z \neq B \land \|z - B\| < a) \to \|({F ↾}_{(−∞, B)}) (z) - L\| < x)) \land b \in ℝ^{+}) \land \forall z \in (A \cap (B, +∞)) ((z \neq B \land \|z - B\| < b) \to \|({F ↾}_{(B, +∞)}) (z) - L\| < x)) \land z \in A \land (z \neq B \land \|z - B\| < if (a \leq b, a, b))) \land B < z) \to \|({F ↾}_{(B, +∞)}) (z) - L\| < x$
125	106 124	eqbrtrd	$⊢ (((((((φ \land x \in ℝ^{+}) \land a \in ℝ^{+}) \land \forall z \in (A \cap (−∞, B)) ((z \neq B \land \|z - B\| < a) \to \|({F ↾}_{(−∞, B)}) (z) - L\| < x)) \land b \in ℝ^{+}) \land \forall z \in (A \cap (B, +∞)) ((z \neq B \land \|z - B\| < b) \to \|({F ↾}_{(B, +∞)}) (z) - L\| < x)) \land z \in A \land (z \neq B \land \|z - B\| < if (a \leq b, a, b))) \land B < z) \to \|F (z) - L\| < x$
126	90 125	syldan	$⊢ (((((((φ \land x \in ℝ^{+}) \land a \in ℝ^{+}) \land \forall z \in (A \cap (−∞, B)) ((z \neq B \land \|z - B\| < a) \to \|({F ↾}_{(−∞, B)}) (z) - L\| < x)) \land b \in ℝ^{+}) \land \forall z \in (A \cap (B, +∞)) ((z \neq B \land \|z - B\| < b) \to \|({F ↾}_{(B, +∞)}) (z) - L\| < x)) \land z \in A \land (z \neq B \land \|z - B\| < if (a \leq b, a, b))) \land \neg z < B) \to \|F (z) - L\| < x$
127	79 126	pm2.61dan	$⊢ ((((((φ \land x \in ℝ^{+}) \land a \in ℝ^{+}) \land \forall z \in (A \cap (−∞, B)) ((z \neq B \land \|z - B\| < a) \to \|({F ↾}_{(−∞, B)}) (z) - L\| < x)) \land b \in ℝ^{+}) \land \forall z \in (A \cap (B, +∞)) ((z \neq B \land \|z - B\| < b) \to \|({F ↾}_{(B, +∞)}) (z) - L\| < x)) \land z \in A \land (z \neq B \land \|z - B\| < if (a \leq b, a, b))) \to \|F (z) - L\| < x$
128	127	3exp	$⊢ (((((φ \land x \in ℝ^{+}) \land a \in ℝ^{+}) \land \forall z \in (A \cap (−∞, B)) ((z \neq B \land \|z - B\| < a) \to \|({F ↾}_{(−∞, B)}) (z) - L\| < x)) \land b \in ℝ^{+}) \land \forall z \in (A \cap (B, +∞)) ((z \neq B \land \|z - B\| < b) \to \|({F ↾}_{(B, +∞)}) (z) - L\| < x)) \to (z \in A \to ((z \neq B \land \|z - B\| < if (a \leq b, a, b)) \to \|F (z) - L\| < x))$
129	22 128	ralrimi	$⊢ (((((φ \land x \in ℝ^{+}) \land a \in ℝ^{+}) \land \forall z \in (A \cap (−∞, B)) ((z \neq B \land \|z - B\| < a) \to \|({F ↾}_{(−∞, B)}) (z) - L\| < x)) \land b \in ℝ^{+}) \land \forall z \in (A \cap (B, +∞)) ((z \neq B \land \|z - B\| < b) \to \|({F ↾}_{(B, +∞)}) (z) - L\| < x)) \to \forall z \in A ((z \neq B \land \|z - B\| < if (a \leq b, a, b)) \to \|F (z) - L\| < x)$
130		brimralrspcev	$⊢ (if (a \leq b, a, b) \in ℝ^{+} \land \forall z \in A ((z \neq B \land \|z - B\| < if (a \leq b, a, b)) \to \|F (z) - L\| < x)) \to \exists y \in ℝ^{+} \forall z \in A ((z \neq B \land \|z - B\| < y) \to \|F (z) - L\| < x)$
131	13 129 130	syl2anc	$⊢ (((((φ \land x \in ℝ^{+}) \land a \in ℝ^{+}) \land \forall z \in (A \cap (−∞, B)) ((z \neq B \land \|z - B\| < a) \to \|({F ↾}_{(−∞, B)}) (z) - L\| < x)) \land b \in ℝ^{+}) \land \forall z \in (A \cap (B, +∞)) ((z \neq B \land \|z - B\| < b) \to \|({F ↾}_{(B, +∞)}) (z) - L\| < x)) \to \exists y \in ℝ^{+} \forall z \in A ((z \neq B \land \|z - B\| < y) \to \|F (z) - L\| < x)$
132		fresin	$⊢ F : A ⟶ ℂ \to ({F ↾}_{(B, +∞)}) : A \cap (B, +∞) ⟶ ℂ$
133	4 132	syl	$⊢ φ \to ({F ↾}_{(B, +∞)}) : A \cap (B, +∞) ⟶ ℂ$
134		inss2	$⊢ A \cap (B, +∞) \subseteq (B, +∞)$
135		ioosscn	$⊢ (B, +∞) \subseteq ℂ$
136	134 135	sstri	$⊢ A \cap (B, +∞) \subseteq ℂ$
137	136	a1i	$⊢ φ \to A \cap (B, +∞) \subseteq ℂ$
138	133 137 55	ellimc3	$⊢ φ \to (R \in (({F ↾}_{(B, +∞)}) {lim}_{ℂ} B) \leftrightarrow (R \in ℂ \land \forall x \in ℝ^{+} \exists b \in ℝ^{+} \forall z \in (A \cap (B, +∞)) ((z \neq B \land \|z - B\| < b) \to \|({F ↾}_{(B, +∞)}) (z) - R\| < x)))$
139	7 138	mpbid	$⊢ φ \to (R \in ℂ \land \forall x \in ℝ^{+} \exists b \in ℝ^{+} \forall z \in (A \cap (B, +∞)) ((z \neq B \land \|z - B\| < b) \to \|({F ↾}_{(B, +∞)}) (z) - R\| < x))$
140	139	simprd	$⊢ φ \to \forall x \in ℝ^{+} \exists b \in ℝ^{+} \forall z \in (A \cap (B, +∞)) ((z \neq B \land \|z - B\| < b) \to \|({F ↾}_{(B, +∞)}) (z) - R\| < x)$
141	140	r19.21bi	$⊢ (φ \land x \in ℝ^{+}) \to \exists b \in ℝ^{+} \forall z \in (A \cap (B, +∞)) ((z \neq B \land \|z - B\| < b) \to \|({F ↾}_{(B, +∞)}) (z) - R\| < x)$
142	8	oveq2d	$⊢ φ \to ({F ↾}_{(B, +∞)}) (z) - L = ({F ↾}_{(B, +∞)}) (z) - R$
143	142	fveq2d	$⊢ φ \to \|({F ↾}_{(B, +∞)}) (z) - L\| = \|({F ↾}_{(B, +∞)}) (z) - R\|$
144	143	breq1d	$⊢ φ \to (\|({F ↾}_{(B, +∞)}) (z) - L\| < x \leftrightarrow \|({F ↾}_{(B, +∞)}) (z) - R\| < x)$
145	144	imbi2d	$⊢ φ \to (((z \neq B \land \|z - B\| < b) \to \|({F ↾}_{(B, +∞)}) (z) - L\| < x) \leftrightarrow ((z \neq B \land \|z - B\| < b) \to \|({F ↾}_{(B, +∞)}) (z) - R\| < x))$
146	145	rexralbidv	$⊢ φ \to (\exists b \in ℝ^{+} \forall z \in (A \cap (B, +∞)) ((z \neq B \land \|z - B\| < b) \to \|({F ↾}_{(B, +∞)}) (z) - L\| < x) \leftrightarrow \exists b \in ℝ^{+} \forall z \in (A \cap (B, +∞)) ((z \neq B \land \|z - B\| < b) \to \|({F ↾}_{(B, +∞)}) (z) - R\| < x))$
147	146	adantr	$⊢ (φ \land x \in ℝ^{+}) \to (\exists b \in ℝ^{+} \forall z \in (A \cap (B, +∞)) ((z \neq B \land \|z - B\| < b) \to \|({F ↾}_{(B, +∞)}) (z) - L\| < x) \leftrightarrow \exists b \in ℝ^{+} \forall z \in (A \cap (B, +∞)) ((z \neq B \land \|z - B\| < b) \to \|({F ↾}_{(B, +∞)}) (z) - R\| < x))$
148	141 147	mpbird	$⊢ (φ \land x \in ℝ^{+}) \to \exists b \in ℝ^{+} \forall z \in (A \cap (B, +∞)) ((z \neq B \land \|z - B\| < b) \to \|({F ↾}_{(B, +∞)}) (z) - L\| < x)$
149	148	ad2antrr	$⊢ (((φ \land x \in ℝ^{+}) \land a \in ℝ^{+}) \land \forall z \in (A \cap (−∞, B)) ((z \neq B \land \|z - B\| < a) \to \|({F ↾}_{(−∞, B)}) (z) - L\| < x)) \to \exists b \in ℝ^{+} \forall z \in (A \cap (B, +∞)) ((z \neq B \land \|z - B\| < b) \to \|({F ↾}_{(B, +∞)}) (z) - L\| < x)$
150	131 149	r19.29a	$⊢ (((φ \land x \in ℝ^{+}) \land a \in ℝ^{+}) \land \forall z \in (A \cap (−∞, B)) ((z \neq B \land \|z - B\| < a) \to \|({F ↾}_{(−∞, B)}) (z) - L\| < x)) \to \exists y \in ℝ^{+} \forall z \in A ((z \neq B \land \|z - B\| < y) \to \|F (z) - L\| < x)$
151		fresin	$⊢ F : A ⟶ ℂ \to ({F ↾}_{(−∞, B)}) : A \cap (−∞, B) ⟶ ℂ$
152	4 151	syl	$⊢ φ \to ({F ↾}_{(−∞, B)}) : A \cap (−∞, B) ⟶ ℂ$
153		inss2	$⊢ A \cap (−∞, B) \subseteq (−∞, B)$
154		ioossre	$⊢ (−∞, B) \subseteq ℝ$
155	153 154	sstri	$⊢ A \cap (−∞, B) \subseteq ℝ$
156		ax-resscn	$⊢ ℝ \subseteq ℂ$
157	156	a1i	$⊢ φ \to ℝ \subseteq ℂ$
158	155 157	sstrid	$⊢ φ \to A \cap (−∞, B) \subseteq ℂ$
159	152 158 55	ellimc3	$⊢ φ \to (L \in (({F ↾}_{(−∞, B)}) {lim}_{ℂ} B) \leftrightarrow (L \in ℂ \land \forall x \in ℝ^{+} \exists a \in ℝ^{+} \forall z \in (A \cap (−∞, B)) ((z \neq B \land \|z - B\| < a) \to \|({F ↾}_{(−∞, B)}) (z) - L\| < x)))$
160	6 159	mpbid	$⊢ φ \to (L \in ℂ \land \forall x \in ℝ^{+} \exists a \in ℝ^{+} \forall z \in (A \cap (−∞, B)) ((z \neq B \land \|z - B\| < a) \to \|({F ↾}_{(−∞, B)}) (z) - L\| < x))$
161	160	simprd	$⊢ φ \to \forall x \in ℝ^{+} \exists a \in ℝ^{+} \forall z \in (A \cap (−∞, B)) ((z \neq B \land \|z - B\| < a) \to \|({F ↾}_{(−∞, B)}) (z) - L\| < x)$
162	161	r19.21bi	$⊢ (φ \land x \in ℝ^{+}) \to \exists a \in ℝ^{+} \forall z \in (A \cap (−∞, B)) ((z \neq B \land \|z - B\| < a) \to \|({F ↾}_{(−∞, B)}) (z) - L\| < x)$
163	150 162	r19.29a	$⊢ (φ \land x \in ℝ^{+}) \to \exists y \in ℝ^{+} \forall z \in A ((z \neq B \land \|z - B\| < y) \to \|F (z) - L\| < x)$
164	163	ralrimiva	$⊢ φ \to \forall x \in ℝ^{+} \exists y \in ℝ^{+} \forall z \in A ((z \neq B \land \|z - B\| < y) \to \|F (z) - L\| < x)$
165	2 156	sstrdi	$⊢ φ \to A \subseteq ℂ$
166	4 165 55	ellimc3	$⊢ φ \to (L \in (F {lim}_{ℂ} B) \leftrightarrow (L \in ℂ \land \forall x \in ℝ^{+} \exists y \in ℝ^{+} \forall z \in A ((z \neq B \land \|z - B\| < y) \to \|F (z) - L\| < x)))$
167	10 164 166	mpbir2and	$⊢ φ \to L \in (F {lim}_{ℂ} B)$

Metamath Proof Explorer

Theorem limcleqr

Proof