limclner

Description: For a limit point, both from the left and from the right, of the domain, the limit of the function exits only if the left and the right limits are equal. (Contributed by Glauco Siliprandi, 11-Dec-2019)

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

Proof

Step	Hyp	Ref	Expression
1		limclner.k	$⊢ K = TopOpen (ℂ_{fld})$
2		limclner.a	$⊢ φ \to A \subseteq ℝ$
3		limclner.j	$⊢ J = topGen (ran (.))$
4		limclner.f	$⊢ φ \to F : A ⟶ ℂ$
5		limclner.blp1	$⊢ φ \to B \in limPt (J) (A \cap (−∞, B))$
6		limclner.blp2	$⊢ φ \to B \in limPt (J) (A \cap (B, +∞))$
7		limclner.l	$⊢ φ \to L \in (({F ↾}_{(−∞, B)}) {lim}_{ℂ} B)$
8		limclner.r	$⊢ φ \to R \in (({F ↾}_{(B, +∞)}) {lim}_{ℂ} B)$
9		limclner.lner	$⊢ φ \to L \neq R$
10		limccl	$⊢ ({F ↾}_{(B, +∞)}) {lim}_{ℂ} B \subseteq ℂ$
11	10 8	sselid	$⊢ φ \to R \in ℂ$
12	11	ad2antrr	$⊢ ((φ \land x \in ℂ) \land \forall y \in ℝ^{+} \exists z \in ℝ^{+} \forall w \in A ((w \neq B \land \|w - B\| < z) \to \|F (w) - x\| < y)) \to R \in ℂ$
13		limccl	$⊢ ({F ↾}_{(−∞, B)}) {lim}_{ℂ} B \subseteq ℂ$
14	13 7	sselid	$⊢ φ \to L \in ℂ$
15	14	ad2antrr	$⊢ ((φ \land x \in ℂ) \land \forall y \in ℝ^{+} \exists z \in ℝ^{+} \forall w \in A ((w \neq B \land \|w - B\| < z) \to \|F (w) - x\| < y)) \to L \in ℂ$
16	12 15	subcld	$⊢ ((φ \land x \in ℂ) \land \forall y \in ℝ^{+} \exists z \in ℝ^{+} \forall w \in A ((w \neq B \land \|w - B\| < z) \to \|F (w) - x\| < y)) \to R - L \in ℂ$
17	9	necomd	$⊢ φ \to R \neq L$
18	17	ad2antrr	$⊢ ((φ \land x \in ℂ) \land \forall y \in ℝ^{+} \exists z \in ℝ^{+} \forall w \in A ((w \neq B \land \|w - B\| < z) \to \|F (w) - x\| < y)) \to R \neq L$
19	12 15 18	subne0d	$⊢ ((φ \land x \in ℂ) \land \forall y \in ℝ^{+} \exists z \in ℝ^{+} \forall w \in A ((w \neq B \land \|w - B\| < z) \to \|F (w) - x\| < y)) \to R - L \neq 0$
20	16 19	absrpcld	$⊢ ((φ \land x \in ℂ) \land \forall y \in ℝ^{+} \exists z \in ℝ^{+} \forall w \in A ((w \neq B \land \|w - B\| < z) \to \|F (w) - x\| < y)) \to \|R - L\| \in ℝ^{+}$
21		4re	$⊢ 4 \in ℝ$
22		4pos	$⊢ 0 < 4$
23	21 22	elrpii	$⊢ 4 \in ℝ^{+}$
24	23	a1i	$⊢ ((φ \land x \in ℂ) \land \forall y \in ℝ^{+} \exists z \in ℝ^{+} \forall w \in A ((w \neq B \land \|w - B\| < z) \to \|F (w) - x\| < y)) \to 4 \in ℝ^{+}$
25	20 24	rpdivcld	$⊢ ((φ \land x \in ℂ) \land \forall y \in ℝ^{+} \exists z \in ℝ^{+} \forall w \in A ((w \neq B \land \|w - B\| < z) \to \|F (w) - x\| < y)) \to \frac{\|R - L\|}{4} \in ℝ^{+}$
26		nfv	$⊢ Ⅎ y (φ \land x \in ℂ)$
27		nfra1	$⊢ Ⅎ y \forall y \in ℝ^{+} \exists z \in ℝ^{+} \forall w \in A ((w \neq B \land \|w - B\| < z) \to \|F (w) - x\| < y)$
28	26 27	nfan	$⊢ Ⅎ y ((φ \land x \in ℂ) \land \forall y \in ℝ^{+} \exists z \in ℝ^{+} \forall w \in A ((w \neq B \land \|w - B\| < z) \to \|F (w) - x\| < y))$
29		nfv	$⊢ Ⅎ y (\frac{\|R - L\|}{4} \in ℝ^{+} \to \exists a \in A \exists b \in A \|R - L\| < 4 (\frac{\|R - L\|}{4}))$
30	28 29	nfim	$⊢ Ⅎ y (((φ \land x \in ℂ) \land \forall y \in ℝ^{+} \exists z \in ℝ^{+} \forall w \in A ((w \neq B \land \|w - B\| < z) \to \|F (w) - x\| < y)) \to (\frac{\|R - L\|}{4} \in ℝ^{+} \to \exists a \in A \exists b \in A \|R - L\| < 4 (\frac{\|R - L\|}{4})))$
31		ovex	$⊢ \frac{\|R - L\|}{4} \in V$
32		eleq1	$⊢ y = \frac{\|R - L\|}{4} \to (y \in ℝ^{+} \leftrightarrow \frac{\|R - L\|}{4} \in ℝ^{+})$
33		oveq2	$⊢ y = \frac{\|R - L\|}{4} \to 4 y = 4 (\frac{\|R - L\|}{4})$
34	33	breq2d	$⊢ y = \frac{\|R - L\|}{4} \to (\|R - L\| < 4 y \leftrightarrow \|R - L\| < 4 (\frac{\|R - L\|}{4}))$
35	34	2rexbidv	$⊢ y = \frac{\|R - L\|}{4} \to (\exists a \in A \exists b \in A \|R - L\| < 4 y \leftrightarrow \exists a \in A \exists b \in A \|R - L\| < 4 (\frac{\|R - L\|}{4}))$
36	32 35	imbi12d	$⊢ y = \frac{\|R - L\|}{4} \to ((y \in ℝ^{+} \to \exists a \in A \exists b \in A \|R - L\| < 4 y) \leftrightarrow (\frac{\|R - L\|}{4} \in ℝ^{+} \to \exists a \in A \exists b \in A \|R - L\| < 4 (\frac{\|R - L\|}{4})))$
37	36	imbi2d	$⊢ y = \frac{\|R - L\|}{4} \to ((((φ \land x \in ℂ) \land \forall y \in ℝ^{+} \exists z \in ℝ^{+} \forall w \in A ((w \neq B \land \|w - B\| < z) \to \|F (w) - x\| < y)) \to (y \in ℝ^{+} \to \exists a \in A \exists b \in A \|R - L\| < 4 y)) \leftrightarrow (((φ \land x \in ℂ) \land \forall y \in ℝ^{+} \exists z \in ℝ^{+} \forall w \in A ((w \neq B \land \|w - B\| < z) \to \|F (w) - x\| < y)) \to (\frac{\|R - L\|}{4} \in ℝ^{+} \to \exists a \in A \exists b \in A \|R - L\| < 4 (\frac{\|R - L\|}{4}))))$
38		simpll	$⊢ (((φ \land x \in ℂ) \land \forall y \in ℝ^{+} \exists z \in ℝ^{+} \forall w \in A ((w \neq B \land \|w - B\| < z) \to \|F (w) - x\| < y)) \land y \in ℝ^{+}) \to (φ \land x \in ℂ)$
39		simpr	$⊢ (((φ \land x \in ℂ) \land \forall y \in ℝ^{+} \exists z \in ℝ^{+} \forall w \in A ((w \neq B \land \|w - B\| < z) \to \|F (w) - x\| < y)) \land y \in ℝ^{+}) \to y \in ℝ^{+}$
40		rspa	$⊢ (\forall y \in ℝ^{+} \exists z \in ℝ^{+} \forall w \in A ((w \neq B \land \|w - B\| < z) \to \|F (w) - x\| < y) \land y \in ℝ^{+}) \to \exists z \in ℝ^{+} \forall w \in A ((w \neq B \land \|w - B\| < z) \to \|F (w) - x\| < y)$
41	40	adantll	$⊢ (((φ \land x \in ℂ) \land \forall y \in ℝ^{+} \exists z \in ℝ^{+} \forall w \in A ((w \neq B \land \|w - B\| < z) \to \|F (w) - x\| < y)) \land y \in ℝ^{+}) \to \exists z \in ℝ^{+} \forall w \in A ((w \neq B \land \|w - B\| < z) \to \|F (w) - x\| < y)$
42		fresin	$⊢ F : A ⟶ ℂ \to ({F ↾}_{(B, +∞)}) : A \cap (B, +∞) ⟶ ℂ$
43	4 42	syl	$⊢ φ \to ({F ↾}_{(B, +∞)}) : A \cap (B, +∞) ⟶ ℂ$
44		inss2	$⊢ A \cap (B, +∞) \subseteq (B, +∞)$
45		ioosscn	$⊢ (B, +∞) \subseteq ℂ$
46	44 45	sstri	$⊢ A \cap (B, +∞) \subseteq ℂ$
47	46	a1i	$⊢ φ \to A \cap (B, +∞) \subseteq ℂ$
48		retop	$⊢ topGen (ran (.)) \in Top$
49	3 48	eqeltri	$⊢ J \in Top$
50		inss2	$⊢ A \cap (−∞, B) \subseteq (−∞, B)$
51		ioossre	$⊢ (−∞, B) \subseteq ℝ$
52	50 51	sstri	$⊢ A \cap (−∞, B) \subseteq ℝ$
53		uniretop	$⊢ ℝ = ⋃ topGen (ran (.))$
54	3	unieqi	$⊢ ⋃ J = ⋃ topGen (ran (.))$
55	53 54	eqtr4i	$⊢ ℝ = ⋃ J$
56	55	lpss	$⊢ (J \in Top \land A \cap (−∞, B) \subseteq ℝ) \to limPt (J) (A \cap (−∞, B)) \subseteq ℝ$
57	49 52 56	mp2an	$⊢ limPt (J) (A \cap (−∞, B)) \subseteq ℝ$
58	57 5	sselid	$⊢ φ \to B \in ℝ$
59	58	recnd	$⊢ φ \to B \in ℂ$
60	43 47 59	ellimc3	$⊢ φ \to (R \in (({F ↾}_{(B, +∞)}) {lim}_{ℂ} B) \leftrightarrow (R \in ℂ \land \forall y \in ℝ^{+} \exists v \in ℝ^{+} \forall w \in (A \cap (B, +∞)) ((w \neq B \land \|w - B\| < v) \to \|({F ↾}_{(B, +∞)}) (w) - R\| < y)))$
61	8 60	mpbid	$⊢ φ \to (R \in ℂ \land \forall y \in ℝ^{+} \exists v \in ℝ^{+} \forall w \in (A \cap (B, +∞)) ((w \neq B \land \|w - B\| < v) \to \|({F ↾}_{(B, +∞)}) (w) - R\| < y))$
62	61	simprd	$⊢ φ \to \forall y \in ℝ^{+} \exists v \in ℝ^{+} \forall w \in (A \cap (B, +∞)) ((w \neq B \land \|w - B\| < v) \to \|({F ↾}_{(B, +∞)}) (w) - R\| < y)$
63	62	r19.21bi	$⊢ (φ \land y \in ℝ^{+}) \to \exists v \in ℝ^{+} \forall w \in (A \cap (B, +∞)) ((w \neq B \land \|w - B\| < v) \to \|({F ↾}_{(B, +∞)}) (w) - R\| < y)$
64	63	3ad2ant1	$⊢ ((φ \land y \in ℝ^{+}) \land z \in ℝ^{+} \land \forall w \in A ((w \neq B \land \|w - B\| < z) \to \|F (w) - x\| < y)) \to \exists v \in ℝ^{+} \forall w \in (A \cap (B, +∞)) ((w \neq B \land \|w - B\| < v) \to \|({F ↾}_{(B, +∞)}) (w) - R\| < y)$
65		simp11l	$⊢ (((φ \land y \in ℝ^{+}) \land z \in ℝ^{+} \land \forall w \in A ((w \neq B \land \|w - B\| < z) \to \|F (w) - x\| < y)) \land v \in ℝ^{+} \land \forall w \in (A \cap (B, +∞)) ((w \neq B \land \|w - B\| < v) \to \|({F ↾}_{(B, +∞)}) (w) - R\| < y)) \to φ$
66		simp12	$⊢ (((φ \land y \in ℝ^{+}) \land z \in ℝ^{+} \land \forall w \in A ((w \neq B \land \|w - B\| < z) \to \|F (w) - x\| < y)) \land v \in ℝ^{+} \land \forall w \in (A \cap (B, +∞)) ((w \neq B \land \|w - B\| < v) \to \|({F ↾}_{(B, +∞)}) (w) - R\| < y)) \to z \in ℝ^{+}$
67		simp2	$⊢ (((φ \land y \in ℝ^{+}) \land z \in ℝ^{+} \land \forall w \in A ((w \neq B \land \|w - B\| < z) \to \|F (w) - x\| < y)) \land v \in ℝ^{+} \land \forall w \in (A \cap (B, +∞)) ((w \neq B \land \|w - B\| < v) \to \|({F ↾}_{(B, +∞)}) (w) - R\| < y)) \to v \in ℝ^{+}$
68		breq2	$⊢ u = if (z \leq v, z, v) \to (\|b - B\| < u \leftrightarrow \|b - B\| < if (z \leq v, z, v))$
69	68	rexbidv	$⊢ u = if (z \leq v, z, v) \to (\exists b \in ((A \cap (B, +∞)) ∖ \{B\}) \|b - B\| < u \leftrightarrow \exists b \in ((A \cap (B, +∞)) ∖ \{B\}) \|b - B\| < if (z \leq v, z, v))$
70		inss1	$⊢ limPt (K) (A \cap (B, +∞)) \cap ℝ \subseteq limPt (K) (A \cap (B, +∞))$
71	70	a1i	$⊢ φ \to limPt (K) (A \cap (B, +∞)) \cap ℝ \subseteq limPt (K) (A \cap (B, +∞))$
72	1	cnfldtop	$⊢ K \in Top$
73	72	a1i	$⊢ φ \to K \in Top$
74		ax-resscn	$⊢ ℝ \subseteq ℂ$
75	74	a1i	$⊢ φ \to ℝ \subseteq ℂ$
76		ioossre	$⊢ (B, +∞) \subseteq ℝ$
77	44 76	sstri	$⊢ A \cap (B, +∞) \subseteq ℝ$
78	77	a1i	$⊢ φ \to A \cap (B, +∞) \subseteq ℝ$
79		unicntop	$⊢ ℂ = ⋃ TopOpen (ℂ_{fld})$
80	1	unieqi	$⊢ ⋃ K = ⋃ TopOpen (ℂ_{fld})$
81	79 80	eqtr4i	$⊢ ℂ = ⋃ K$
82	1	tgioo2	$⊢ topGen (ran (.)) = K ↾_{𝑡} ℝ$
83	3 82	eqtri	$⊢ J = K ↾_{𝑡} ℝ$
84	81 83	restlp	$⊢ (K \in Top \land ℝ \subseteq ℂ \land A \cap (B, +∞) \subseteq ℝ) \to limPt (J) (A \cap (B, +∞)) = limPt (K) (A \cap (B, +∞)) \cap ℝ$
85	73 75 78 84	syl3anc	$⊢ φ \to limPt (J) (A \cap (B, +∞)) = limPt (K) (A \cap (B, +∞)) \cap ℝ$
86	1	eqcomi	$⊢ TopOpen (ℂ_{fld}) = K$
87	86	fveq2i	$⊢ limPt (TopOpen (ℂ_{fld})) = limPt (K)$
88	87	fveq1i	$⊢ limPt (TopOpen (ℂ_{fld})) (A \cap (B, +∞)) = limPt (K) (A \cap (B, +∞))$
89	88	a1i	$⊢ φ \to limPt (TopOpen (ℂ_{fld})) (A \cap (B, +∞)) = limPt (K) (A \cap (B, +∞))$
90	71 85 89	3sstr4d	$⊢ φ \to limPt (J) (A \cap (B, +∞)) \subseteq limPt (TopOpen (ℂ_{fld})) (A \cap (B, +∞))$
91	90 6	sseldd	$⊢ φ \to B \in limPt (TopOpen (ℂ_{fld})) (A \cap (B, +∞))$
92	47 59	islpcn	$⊢ φ \to (B \in limPt (TopOpen (ℂ_{fld})) (A \cap (B, +∞)) \leftrightarrow \forall u \in ℝ^{+} \exists b \in ((A \cap (B, +∞)) ∖ \{B\}) \|b - B\| < u)$
93	91 92	mpbid	$⊢ φ \to \forall u \in ℝ^{+} \exists b \in ((A \cap (B, +∞)) ∖ \{B\}) \|b - B\| < u$
94	93	3ad2ant1	$⊢ (φ \land z \in ℝ^{+} \land v \in ℝ^{+}) \to \forall u \in ℝ^{+} \exists b \in ((A \cap (B, +∞)) ∖ \{B\}) \|b - B\| < u$
95		ifcl	$⊢ (z \in ℝ^{+} \land v \in ℝ^{+}) \to if (z \leq v, z, v) \in ℝ^{+}$
96	95	3adant1	$⊢ (φ \land z \in ℝ^{+} \land v \in ℝ^{+}) \to if (z \leq v, z, v) \in ℝ^{+}$
97	69 94 96	rspcdva	$⊢ (φ \land z \in ℝ^{+} \land v \in ℝ^{+}) \to \exists b \in ((A \cap (B, +∞)) ∖ \{B\}) \|b - B\| < if (z \leq v, z, v)$
98		eldifi	$⊢ b \in ((A \cap (B, +∞)) ∖ \{B\}) \to b \in (A \cap (B, +∞))$
99	77 98	sselid	$⊢ b \in ((A \cap (B, +∞)) ∖ \{B\}) \to b \in ℝ$
100	75	sselda	$⊢ (φ \land b \in ℝ) \to b \in ℂ$
101	59	adantr	$⊢ (φ \land b \in ℝ) \to B \in ℂ$
102	100 101	subcld	$⊢ (φ \land b \in ℝ) \to b - B \in ℂ$
103	102	abscld	$⊢ (φ \land b \in ℝ) \to \|b - B\| \in ℝ$
104	103	3ad2antl1	$⊢ ((φ \land z \in ℝ^{+} \land v \in ℝ^{+}) \land b \in ℝ) \to \|b - B\| \in ℝ$
105	104	adantr	$⊢ (((φ \land z \in ℝ^{+} \land v \in ℝ^{+}) \land b \in ℝ) \land \|b - B\| < if (z \leq v, z, v)) \to \|b - B\| \in ℝ$
106	96	rpred	$⊢ (φ \land z \in ℝ^{+} \land v \in ℝ^{+}) \to if (z \leq v, z, v) \in ℝ$
107	106	ad2antrr	$⊢ (((φ \land z \in ℝ^{+} \land v \in ℝ^{+}) \land b \in ℝ) \land \|b - B\| < if (z \leq v, z, v)) \to if (z \leq v, z, v) \in ℝ$
108		rpre	$⊢ z \in ℝ^{+} \to z \in ℝ$
109	108	3ad2ant2	$⊢ (φ \land z \in ℝ^{+} \land v \in ℝ^{+}) \to z \in ℝ$
110	109	ad2antrr	$⊢ (((φ \land z \in ℝ^{+} \land v \in ℝ^{+}) \land b \in ℝ) \land \|b - B\| < if (z \leq v, z, v)) \to z \in ℝ$
111		simpr	$⊢ (((φ \land z \in ℝ^{+} \land v \in ℝ^{+}) \land b \in ℝ) \land \|b - B\| < if (z \leq v, z, v)) \to \|b - B\| < if (z \leq v, z, v)$
112		rpre	$⊢ v \in ℝ^{+} \to v \in ℝ$
113		min1	$⊢ (z \in ℝ \land v \in ℝ) \to if (z \leq v, z, v) \leq z$
114	108 112 113	syl2an	$⊢ (z \in ℝ^{+} \land v \in ℝ^{+}) \to if (z \leq v, z, v) \leq z$
115	114	3adant1	$⊢ (φ \land z \in ℝ^{+} \land v \in ℝ^{+}) \to if (z \leq v, z, v) \leq z$
116	115	ad2antrr	$⊢ (((φ \land z \in ℝ^{+} \land v \in ℝ^{+}) \land b \in ℝ) \land \|b - B\| < if (z \leq v, z, v)) \to if (z \leq v, z, v) \leq z$
117	105 107 110 111 116	ltletrd	$⊢ (((φ \land z \in ℝ^{+} \land v \in ℝ^{+}) \land b \in ℝ) \land \|b - B\| < if (z \leq v, z, v)) \to \|b - B\| < z$
118	112	3ad2ant3	$⊢ (φ \land z \in ℝ^{+} \land v \in ℝ^{+}) \to v \in ℝ$
119	118	ad2antrr	$⊢ (((φ \land z \in ℝ^{+} \land v \in ℝ^{+}) \land b \in ℝ) \land \|b - B\| < if (z \leq v, z, v)) \to v \in ℝ$
120	110 119	min2d	$⊢ (((φ \land z \in ℝ^{+} \land v \in ℝ^{+}) \land b \in ℝ) \land \|b - B\| < if (z \leq v, z, v)) \to if (z \leq v, z, v) \leq v$
121	105 107 119 111 120	ltletrd	$⊢ (((φ \land z \in ℝ^{+} \land v \in ℝ^{+}) \land b \in ℝ) \land \|b - B\| < if (z \leq v, z, v)) \to \|b - B\| < v$
122	117 121	jca	$⊢ (((φ \land z \in ℝ^{+} \land v \in ℝ^{+}) \land b \in ℝ) \land \|b - B\| < if (z \leq v, z, v)) \to (\|b - B\| < z \land \|b - B\| < v)$
123	122	ex	$⊢ ((φ \land z \in ℝ^{+} \land v \in ℝ^{+}) \land b \in ℝ) \to (\|b - B\| < if (z \leq v, z, v) \to (\|b - B\| < z \land \|b - B\| < v))$
124	99 123	sylan2	$⊢ ((φ \land z \in ℝ^{+} \land v \in ℝ^{+}) \land b \in ((A \cap (B, +∞)) ∖ \{B\})) \to (\|b - B\| < if (z \leq v, z, v) \to (\|b - B\| < z \land \|b - B\| < v))$
125	124	reximdva	$⊢ (φ \land z \in ℝ^{+} \land v \in ℝ^{+}) \to (\exists b \in ((A \cap (B, +∞)) ∖ \{B\}) \|b - B\| < if (z \leq v, z, v) \to \exists b \in ((A \cap (B, +∞)) ∖ \{B\}) (\|b - B\| < z \land \|b - B\| < v))$
126	97 125	mpd	$⊢ (φ \land z \in ℝ^{+} \land v \in ℝ^{+}) \to \exists b \in ((A \cap (B, +∞)) ∖ \{B\}) (\|b - B\| < z \land \|b - B\| < v)$
127	65 66 67 126	syl3anc	$⊢ (((φ \land y \in ℝ^{+}) \land z \in ℝ^{+} \land \forall w \in A ((w \neq B \land \|w - B\| < z) \to \|F (w) - x\| < y)) \land v \in ℝ^{+} \land \forall w \in (A \cap (B, +∞)) ((w \neq B \land \|w - B\| < v) \to \|({F ↾}_{(B, +∞)}) (w) - R\| < y)) \to \exists b \in ((A \cap (B, +∞)) ∖ \{B\}) (\|b - B\| < z \land \|b - B\| < v)$
128		nfv	$⊢ Ⅎ b (((φ \land y \in ℝ^{+}) \land z \in ℝ^{+} \land \forall w \in A ((w \neq B \land \|w - B\| < z) \to \|F (w) - x\| < y)) \land v \in ℝ^{+} \land \forall w \in (A \cap (B, +∞)) ((w \neq B \land \|w - B\| < v) \to \|({F ↾}_{(B, +∞)}) (w) - R\| < y))$
129		nfre1	$⊢ Ⅎ b \exists b \in A (\|F (b) - x\| < y \land \|F (b) - R\| < y)$
130	98	elin1d	$⊢ b \in ((A \cap (B, +∞)) ∖ \{B\}) \to b \in A$
131	130	3ad2ant2	$⊢ ((((φ \land y \in ℝ^{+}) \land z \in ℝ^{+} \land \forall w \in A ((w \neq B \land \|w - B\| < z) \to \|F (w) - x\| < y)) \land v \in ℝ^{+} \land \forall w \in (A \cap (B, +∞)) ((w \neq B \land \|w - B\| < v) \to \|({F ↾}_{(B, +∞)}) (w) - R\| < y)) \land b \in ((A \cap (B, +∞)) ∖ \{B\}) \land (\|b - B\| < z \land \|b - B\| < v)) \to b \in A$
132		simp113	$⊢ ((((φ \land y \in ℝ^{+}) \land z \in ℝ^{+} \land \forall w \in A ((w \neq B \land \|w - B\| < z) \to \|F (w) - x\| < y)) \land v \in ℝ^{+} \land \forall w \in (A \cap (B, +∞)) ((w \neq B \land \|w - B\| < v) \to \|({F ↾}_{(B, +∞)}) (w) - R\| < y)) \land b \in ((A \cap (B, +∞)) ∖ \{B\}) \land (\|b - B\| < z \land \|b - B\| < v)) \to \forall w \in A ((w \neq B \land \|w - B\| < z) \to \|F (w) - x\| < y)$
133		eldifsni	$⊢ b \in ((A \cap (B, +∞)) ∖ \{B\}) \to b \neq B$
134	133	adantr	$⊢ (b \in ((A \cap (B, +∞)) ∖ \{B\}) \land (\|b - B\| < z \land \|b - B\| < v)) \to b \neq B$
135		simprl	$⊢ (b \in ((A \cap (B, +∞)) ∖ \{B\}) \land (\|b - B\| < z \land \|b - B\| < v)) \to \|b - B\| < z$
136	134 135	jca	$⊢ (b \in ((A \cap (B, +∞)) ∖ \{B\}) \land (\|b - B\| < z \land \|b - B\| < v)) \to (b \neq B \land \|b - B\| < z)$
137	136	3adant1	$⊢ ((((φ \land y \in ℝ^{+}) \land z \in ℝ^{+} \land \forall w \in A ((w \neq B \land \|w - B\| < z) \to \|F (w) - x\| < y)) \land v \in ℝ^{+} \land \forall w \in (A \cap (B, +∞)) ((w \neq B \land \|w - B\| < v) \to \|({F ↾}_{(B, +∞)}) (w) - R\| < y)) \land b \in ((A \cap (B, +∞)) ∖ \{B\}) \land (\|b - B\| < z \land \|b - B\| < v)) \to (b \neq B \land \|b - B\| < z)$
138		neeq1	$⊢ w = b \to (w \neq B \leftrightarrow b \neq B)$
139		fvoveq1	$⊢ w = b \to \|w - B\| = \|b - B\|$
140	139	breq1d	$⊢ w = b \to (\|w - B\| < z \leftrightarrow \|b - B\| < z)$
141	138 140	anbi12d	$⊢ w = b \to ((w \neq B \land \|w - B\| < z) \leftrightarrow (b \neq B \land \|b - B\| < z))$
142	141	imbrov2fvoveq	$⊢ w = b \to (((w \neq B \land \|w - B\| < z) \to \|F (w) - x\| < y) \leftrightarrow ((b \neq B \land \|b - B\| < z) \to \|F (b) - x\| < y))$
143	142	rspcva	$⊢ (b \in A \land \forall w \in A ((w \neq B \land \|w - B\| < z) \to \|F (w) - x\| < y)) \to ((b \neq B \land \|b - B\| < z) \to \|F (b) - x\| < y)$
144	143	imp	$⊢ ((b \in A \land \forall w \in A ((w \neq B \land \|w - B\| < z) \to \|F (w) - x\| < y)) \land (b \neq B \land \|b - B\| < z)) \to \|F (b) - x\| < y$
145	131 132 137 144	syl21anc	$⊢ ((((φ \land y \in ℝ^{+}) \land z \in ℝ^{+} \land \forall w \in A ((w \neq B \land \|w - B\| < z) \to \|F (w) - x\| < y)) \land v \in ℝ^{+} \land \forall w \in (A \cap (B, +∞)) ((w \neq B \land \|w - B\| < v) \to \|({F ↾}_{(B, +∞)}) (w) - R\| < y)) \land b \in ((A \cap (B, +∞)) ∖ \{B\}) \land (\|b - B\| < z \land \|b - B\| < v)) \to \|F (b) - x\| < y$
146	98	3ad2ant2	$⊢ ((((φ \land y \in ℝ^{+}) \land z \in ℝ^{+} \land \forall w \in A ((w \neq B \land \|w - B\| < z) \to \|F (w) - x\| < y)) \land v \in ℝ^{+} \land \forall w \in (A \cap (B, +∞)) ((w \neq B \land \|w - B\| < v) \to \|({F ↾}_{(B, +∞)}) (w) - R\| < y)) \land b \in ((A \cap (B, +∞)) ∖ \{B\}) \land (\|b - B\| < z \land \|b - B\| < v)) \to b \in (A \cap (B, +∞))$
147	65	3ad2ant1	$⊢ ((((φ \land y \in ℝ^{+}) \land z \in ℝ^{+} \land \forall w \in A ((w \neq B \land \|w - B\| < z) \to \|F (w) - x\| < y)) \land v \in ℝ^{+} \land \forall w \in (A \cap (B, +∞)) ((w \neq B \land \|w - B\| < v) \to \|({F ↾}_{(B, +∞)}) (w) - R\| < y)) \land b \in ((A \cap (B, +∞)) ∖ \{B\}) \land (\|b - B\| < z \land \|b - B\| < v)) \to φ$
148		simp13	$⊢ ((((φ \land y \in ℝ^{+}) \land z \in ℝ^{+} \land \forall w \in A ((w \neq B \land \|w - B\| < z) \to \|F (w) - x\| < y)) \land v \in ℝ^{+} \land \forall w \in (A \cap (B, +∞)) ((w \neq B \land \|w - B\| < v) \to \|({F ↾}_{(B, +∞)}) (w) - R\| < y)) \land b \in ((A \cap (B, +∞)) ∖ \{B\}) \land (\|b - B\| < z \land \|b - B\| < v)) \to \forall w \in (A \cap (B, +∞)) ((w \neq B \land \|w - B\| < v) \to \|({F ↾}_{(B, +∞)}) (w) - R\| < y)$
149		nfv	$⊢ Ⅎ w φ$
150		nfra1	$⊢ Ⅎ w \forall w \in (A \cap (B, +∞)) ((w \neq B \land \|w - B\| < v) \to \|({F ↾}_{(B, +∞)}) (w) - R\| < y)$
151	149 150	nfan	$⊢ Ⅎ w (φ \land \forall w \in (A \cap (B, +∞)) ((w \neq B \land \|w - B\| < v) \to \|({F ↾}_{(B, +∞)}) (w) - R\| < y))$
152		elinel2	$⊢ w \in (A \cap (B, +∞)) \to w \in (B, +∞)$
153	152	fvresd	$⊢ w \in (A \cap (B, +∞)) \to ({F ↾}_{(B, +∞)}) (w) = F (w)$
154	153	eqcomd	$⊢ w \in (A \cap (B, +∞)) \to F (w) = ({F ↾}_{(B, +∞)}) (w)$
155	154	fvoveq1d	$⊢ w \in (A \cap (B, +∞)) \to \|F (w) - R\| = \|({F ↾}_{(B, +∞)}) (w) - R\|$
156	155	3ad2ant2	$⊢ ((φ \land \forall w \in (A \cap (B, +∞)) ((w \neq B \land \|w - B\| < v) \to \|({F ↾}_{(B, +∞)}) (w) - R\| < y)) \land w \in (A \cap (B, +∞)) \land (w \neq B \land \|w - B\| < v)) \to \|F (w) - R\| = \|({F ↾}_{(B, +∞)}) (w) - R\|$
157		rspa	$⊢ (\forall w \in (A \cap (B, +∞)) ((w \neq B \land \|w - B\| < v) \to \|({F ↾}_{(B, +∞)}) (w) - R\| < y) \land w \in (A \cap (B, +∞))) \to ((w \neq B \land \|w - B\| < v) \to \|({F ↾}_{(B, +∞)}) (w) - R\| < y)$
158	157	3impia	$⊢ (\forall w \in (A \cap (B, +∞)) ((w \neq B \land \|w - B\| < v) \to \|({F ↾}_{(B, +∞)}) (w) - R\| < y) \land w \in (A \cap (B, +∞)) \land (w \neq B \land \|w - B\| < v)) \to \|({F ↾}_{(B, +∞)}) (w) - R\| < y$
159	158	3adant1l	$⊢ ((φ \land \forall w \in (A \cap (B, +∞)) ((w \neq B \land \|w - B\| < v) \to \|({F ↾}_{(B, +∞)}) (w) - R\| < y)) \land w \in (A \cap (B, +∞)) \land (w \neq B \land \|w - B\| < v)) \to \|({F ↾}_{(B, +∞)}) (w) - R\| < y$
160	156 159	eqbrtrd	$⊢ ((φ \land \forall w \in (A \cap (B, +∞)) ((w \neq B \land \|w - B\| < v) \to \|({F ↾}_{(B, +∞)}) (w) - R\| < y)) \land w \in (A \cap (B, +∞)) \land (w \neq B \land \|w - B\| < v)) \to \|F (w) - R\| < y$
161	160	3exp	$⊢ (φ \land \forall w \in (A \cap (B, +∞)) ((w \neq B \land \|w - B\| < v) \to \|({F ↾}_{(B, +∞)}) (w) - R\| < y)) \to (w \in (A \cap (B, +∞)) \to ((w \neq B \land \|w - B\| < v) \to \|F (w) - R\| < y))$
162	151 161	ralrimi	$⊢ (φ \land \forall w \in (A \cap (B, +∞)) ((w \neq B \land \|w - B\| < v) \to \|({F ↾}_{(B, +∞)}) (w) - R\| < y)) \to \forall w \in (A \cap (B, +∞)) ((w \neq B \land \|w - B\| < v) \to \|F (w) - R\| < y)$
163	147 148 162	syl2anc	$⊢ ((((φ \land y \in ℝ^{+}) \land z \in ℝ^{+} \land \forall w \in A ((w \neq B \land \|w - B\| < z) \to \|F (w) - x\| < y)) \land v \in ℝ^{+} \land \forall w \in (A \cap (B, +∞)) ((w \neq B \land \|w - B\| < v) \to \|({F ↾}_{(B, +∞)}) (w) - R\| < y)) \land b \in ((A \cap (B, +∞)) ∖ \{B\}) \land (\|b - B\| < z \land \|b - B\| < v)) \to \forall w \in (A \cap (B, +∞)) ((w \neq B \land \|w - B\| < v) \to \|F (w) - R\| < y)$
164	133	anim1i	$⊢ (b \in ((A \cap (B, +∞)) ∖ \{B\}) \land \|b - B\| < v) \to (b \neq B \land \|b - B\| < v)$
165	164	adantrl	$⊢ (b \in ((A \cap (B, +∞)) ∖ \{B\}) \land (\|b - B\| < z \land \|b - B\| < v)) \to (b \neq B \land \|b - B\| < v)$
166	165	3adant1	$⊢ ((((φ \land y \in ℝ^{+}) \land z \in ℝ^{+} \land \forall w \in A ((w \neq B \land \|w - B\| < z) \to \|F (w) - x\| < y)) \land v \in ℝ^{+} \land \forall w \in (A \cap (B, +∞)) ((w \neq B \land \|w - B\| < v) \to \|({F ↾}_{(B, +∞)}) (w) - R\| < y)) \land b \in ((A \cap (B, +∞)) ∖ \{B\}) \land (\|b - B\| < z \land \|b - B\| < v)) \to (b \neq B \land \|b - B\| < v)$
167	139	breq1d	$⊢ w = b \to (\|w - B\| < v \leftrightarrow \|b - B\| < v)$
168	138 167	anbi12d	$⊢ w = b \to ((w \neq B \land \|w - B\| < v) \leftrightarrow (b \neq B \land \|b - B\| < v))$
169	168	imbrov2fvoveq	$⊢ w = b \to (((w \neq B \land \|w - B\| < v) \to \|F (w) - R\| < y) \leftrightarrow ((b \neq B \land \|b - B\| < v) \to \|F (b) - R\| < y))$
170	169	rspcva	$⊢ (b \in (A \cap (B, +∞)) \land \forall w \in (A \cap (B, +∞)) ((w \neq B \land \|w - B\| < v) \to \|F (w) - R\| < y)) \to ((b \neq B \land \|b - B\| < v) \to \|F (b) - R\| < y)$
171	170	imp	$⊢ ((b \in (A \cap (B, +∞)) \land \forall w \in (A \cap (B, +∞)) ((w \neq B \land \|w - B\| < v) \to \|F (w) - R\| < y)) \land (b \neq B \land \|b - B\| < v)) \to \|F (b) - R\| < y$
172	146 163 166 171	syl21anc	$⊢ ((((φ \land y \in ℝ^{+}) \land z \in ℝ^{+} \land \forall w \in A ((w \neq B \land \|w - B\| < z) \to \|F (w) - x\| < y)) \land v \in ℝ^{+} \land \forall w \in (A \cap (B, +∞)) ((w \neq B \land \|w - B\| < v) \to \|({F ↾}_{(B, +∞)}) (w) - R\| < y)) \land b \in ((A \cap (B, +∞)) ∖ \{B\}) \land (\|b - B\| < z \land \|b - B\| < v)) \to \|F (b) - R\| < y$
173		rspe	$⊢ (b \in A \land (\|F (b) - x\| < y \land \|F (b) - R\| < y)) \to \exists b \in A (\|F (b) - x\| < y \land \|F (b) - R\| < y)$
174	131 145 172 173	syl12anc	$⊢ ((((φ \land y \in ℝ^{+}) \land z \in ℝ^{+} \land \forall w \in A ((w \neq B \land \|w - B\| < z) \to \|F (w) - x\| < y)) \land v \in ℝ^{+} \land \forall w \in (A \cap (B, +∞)) ((w \neq B \land \|w - B\| < v) \to \|({F ↾}_{(B, +∞)}) (w) - R\| < y)) \land b \in ((A \cap (B, +∞)) ∖ \{B\}) \land (\|b - B\| < z \land \|b - B\| < v)) \to \exists b \in A (\|F (b) - x\| < y \land \|F (b) - R\| < y)$
175	174	3exp	$⊢ (((φ \land y \in ℝ^{+}) \land z \in ℝ^{+} \land \forall w \in A ((w \neq B \land \|w - B\| < z) \to \|F (w) - x\| < y)) \land v \in ℝ^{+} \land \forall w \in (A \cap (B, +∞)) ((w \neq B \land \|w - B\| < v) \to \|({F ↾}_{(B, +∞)}) (w) - R\| < y)) \to (b \in ((A \cap (B, +∞)) ∖ \{B\}) \to ((\|b - B\| < z \land \|b - B\| < v) \to \exists b \in A (\|F (b) - x\| < y \land \|F (b) - R\| < y)))$
176	128 129 175	rexlimd	$⊢ (((φ \land y \in ℝ^{+}) \land z \in ℝ^{+} \land \forall w \in A ((w \neq B \land \|w - B\| < z) \to \|F (w) - x\| < y)) \land v \in ℝ^{+} \land \forall w \in (A \cap (B, +∞)) ((w \neq B \land \|w - B\| < v) \to \|({F ↾}_{(B, +∞)}) (w) - R\| < y)) \to (\exists b \in ((A \cap (B, +∞)) ∖ \{B\}) (\|b - B\| < z \land \|b - B\| < v) \to \exists b \in A (\|F (b) - x\| < y \land \|F (b) - R\| < y))$
177	127 176	mpd	$⊢ (((φ \land y \in ℝ^{+}) \land z \in ℝ^{+} \land \forall w \in A ((w \neq B \land \|w - B\| < z) \to \|F (w) - x\| < y)) \land v \in ℝ^{+} \land \forall w \in (A \cap (B, +∞)) ((w \neq B \land \|w - B\| < v) \to \|({F ↾}_{(B, +∞)}) (w) - R\| < y)) \to \exists b \in A (\|F (b) - x\| < y \land \|F (b) - R\| < y)$
178	177	3exp	$⊢ ((φ \land y \in ℝ^{+}) \land z \in ℝ^{+} \land \forall w \in A ((w \neq B \land \|w - B\| < z) \to \|F (w) - x\| < y)) \to (v \in ℝ^{+} \to (\forall w \in (A \cap (B, +∞)) ((w \neq B \land \|w - B\| < v) \to \|({F ↾}_{(B, +∞)}) (w) - R\| < y) \to \exists b \in A (\|F (b) - x\| < y \land \|F (b) - R\| < y)))$
179	178	rexlimdv	$⊢ ((φ \land y \in ℝ^{+}) \land z \in ℝ^{+} \land \forall w \in A ((w \neq B \land \|w - B\| < z) \to \|F (w) - x\| < y)) \to (\exists v \in ℝ^{+} \forall w \in (A \cap (B, +∞)) ((w \neq B \land \|w - B\| < v) \to \|({F ↾}_{(B, +∞)}) (w) - R\| < y) \to \exists b \in A (\|F (b) - x\| < y \land \|F (b) - R\| < y))$
180	64 179	mpd	$⊢ ((φ \land y \in ℝ^{+}) \land z \in ℝ^{+} \land \forall w \in A ((w \neq B \land \|w - B\| < z) \to \|F (w) - x\| < y)) \to \exists b \in A (\|F (b) - x\| < y \land \|F (b) - R\| < y)$
181	180	3exp	$⊢ (φ \land y \in ℝ^{+}) \to (z \in ℝ^{+} \to (\forall w \in A ((w \neq B \land \|w - B\| < z) \to \|F (w) - x\| < y) \to \exists b \in A (\|F (b) - x\| < y \land \|F (b) - R\| < y)))$
182	181	rexlimdv	$⊢ (φ \land y \in ℝ^{+}) \to (\exists z \in ℝ^{+} \forall w \in A ((w \neq B \land \|w - B\| < z) \to \|F (w) - x\| < y) \to \exists b \in A (\|F (b) - x\| < y \land \|F (b) - R\| < y))$
183	182	imp	$⊢ ((φ \land y \in ℝ^{+}) \land \exists z \in ℝ^{+} \forall w \in A ((w \neq B \land \|w - B\| < z) \to \|F (w) - x\| < y)) \to \exists b \in A (\|F (b) - x\| < y \land \|F (b) - R\| < y)$
184	183	adantllr	$⊢ (((φ \land x \in ℂ) \land y \in ℝ^{+}) \land \exists z \in ℝ^{+} \forall w \in A ((w \neq B \land \|w - B\| < z) \to \|F (w) - x\| < y)) \to \exists b \in A (\|F (b) - x\| < y \land \|F (b) - R\| < y)$
185	184	ad2antrr	$⊢ (((((φ \land x \in ℂ) \land y \in ℝ^{+}) \land \exists z \in ℝ^{+} \forall w \in A ((w \neq B \land \|w - B\| < z) \to \|F (w) - x\| < y)) \land a \in A) \land (\|F (a) - x\| < y \land \|F (a) - L\| < y)) \to \exists b \in A (\|F (b) - x\| < y \land \|F (b) - R\| < y)$
186	11	ad6antr	$⊢ ((((((φ \land x \in ℂ) \land y \in ℝ^{+}) \land a \in A) \land (\|F (a) - x\| < y \land \|F (a) - L\| < y)) \land b \in A) \land (\|F (b) - x\| < y \land \|F (b) - R\| < y)) \to R \in ℂ$
187	14	ad6antr	$⊢ ((((((φ \land x \in ℂ) \land y \in ℝ^{+}) \land a \in A) \land (\|F (a) - x\| < y \land \|F (a) - L\| < y)) \land b \in A) \land (\|F (b) - x\| < y \land \|F (b) - R\| < y)) \to L \in ℂ$
188	186 187	subcld	$⊢ ((((((φ \land x \in ℂ) \land y \in ℝ^{+}) \land a \in A) \land (\|F (a) - x\| < y \land \|F (a) - L\| < y)) \land b \in A) \land (\|F (b) - x\| < y \land \|F (b) - R\| < y)) \to R - L \in ℂ$
189	188	abscld	$⊢ ((((((φ \land x \in ℂ) \land y \in ℝ^{+}) \land a \in A) \land (\|F (a) - x\| < y \land \|F (a) - L\| < y)) \land b \in A) \land (\|F (b) - x\| < y \land \|F (b) - R\| < y)) \to \|R - L\| \in ℝ$
190		simp-6l	$⊢ ((((((φ \land x \in ℂ) \land y \in ℝ^{+}) \land a \in A) \land (\|F (a) - x\| < y \land \|F (a) - L\| < y)) \land b \in A) \land (\|F (b) - x\| < y \land \|F (b) - R\| < y)) \to φ$
191		simplr	$⊢ ((((((φ \land x \in ℂ) \land y \in ℝ^{+}) \land a \in A) \land (\|F (a) - x\| < y \land \|F (a) - L\| < y)) \land b \in A) \land (\|F (b) - x\| < y \land \|F (b) - R\| < y)) \to b \in A$
192	4	ffvelcdmda	$⊢ (φ \land b \in A) \to F (b) \in ℂ$
193	190 191 192	syl2anc	$⊢ ((((((φ \land x \in ℂ) \land y \in ℝ^{+}) \land a \in A) \land (\|F (a) - x\| < y \land \|F (a) - L\| < y)) \land b \in A) \land (\|F (b) - x\| < y \land \|F (b) - R\| < y)) \to F (b) \in ℂ$
194	186 193	subcld	$⊢ ((((((φ \land x \in ℂ) \land y \in ℝ^{+}) \land a \in A) \land (\|F (a) - x\| < y \land \|F (a) - L\| < y)) \land b \in A) \land (\|F (b) - x\| < y \land \|F (b) - R\| < y)) \to R - F (b) \in ℂ$
195	194	abscld	$⊢ ((((((φ \land x \in ℂ) \land y \in ℝ^{+}) \land a \in A) \land (\|F (a) - x\| < y \land \|F (a) - L\| < y)) \land b \in A) \land (\|F (b) - x\| < y \land \|F (b) - R\| < y)) \to \|R - F (b)\| \in ℝ$
196		simp-6r	$⊢ ((((((φ \land x \in ℂ) \land y \in ℝ^{+}) \land a \in A) \land (\|F (a) - x\| < y \land \|F (a) - L\| < y)) \land b \in A) \land (\|F (b) - x\| < y \land \|F (b) - R\| < y)) \to x \in ℂ$
197	193 196	subcld	$⊢ ((((((φ \land x \in ℂ) \land y \in ℝ^{+}) \land a \in A) \land (\|F (a) - x\| < y \land \|F (a) - L\| < y)) \land b \in A) \land (\|F (b) - x\| < y \land \|F (b) - R\| < y)) \to F (b) - x \in ℂ$
198	197	abscld	$⊢ ((((((φ \land x \in ℂ) \land y \in ℝ^{+}) \land a \in A) \land (\|F (a) - x\| < y \land \|F (a) - L\| < y)) \land b \in A) \land (\|F (b) - x\| < y \land \|F (b) - R\| < y)) \to \|F (b) - x\| \in ℝ$
199	195 198	readdcld	$⊢ ((((((φ \land x \in ℂ) \land y \in ℝ^{+}) \land a \in A) \land (\|F (a) - x\| < y \land \|F (a) - L\| < y)) \land b \in A) \land (\|F (b) - x\| < y \land \|F (b) - R\| < y)) \to \|R - F (b)\| + \|F (b) - x\| \in ℝ$
200		simp-4r	$⊢ ((((((φ \land x \in ℂ) \land y \in ℝ^{+}) \land a \in A) \land (\|F (a) - x\| < y \land \|F (a) - L\| < y)) \land b \in A) \land (\|F (b) - x\| < y \land \|F (b) - R\| < y)) \to a \in A$
201	4	ffvelcdmda	$⊢ (φ \land a \in A) \to F (a) \in ℂ$
202	190 200 201	syl2anc	$⊢ ((((((φ \land x \in ℂ) \land y \in ℝ^{+}) \land a \in A) \land (\|F (a) - x\| < y \land \|F (a) - L\| < y)) \land b \in A) \land (\|F (b) - x\| < y \land \|F (b) - R\| < y)) \to F (a) \in ℂ$
203	196 202	subcld	$⊢ ((((((φ \land x \in ℂ) \land y \in ℝ^{+}) \land a \in A) \land (\|F (a) - x\| < y \land \|F (a) - L\| < y)) \land b \in A) \land (\|F (b) - x\| < y \land \|F (b) - R\| < y)) \to x - F (a) \in ℂ$
204	203	abscld	$⊢ ((((((φ \land x \in ℂ) \land y \in ℝ^{+}) \land a \in A) \land (\|F (a) - x\| < y \land \|F (a) - L\| < y)) \land b \in A) \land (\|F (b) - x\| < y \land \|F (b) - R\| < y)) \to \|x - F (a)\| \in ℝ$
205	199 204	readdcld	$⊢ ((((((φ \land x \in ℂ) \land y \in ℝ^{+}) \land a \in A) \land (\|F (a) - x\| < y \land \|F (a) - L\| < y)) \land b \in A) \land (\|F (b) - x\| < y \land \|F (b) - R\| < y)) \to \|R - F (b)\| + \|F (b) - x\| + \|x - F (a)\| \in ℝ$
206	202 187	subcld	$⊢ ((((((φ \land x \in ℂ) \land y \in ℝ^{+}) \land a \in A) \land (\|F (a) - x\| < y \land \|F (a) - L\| < y)) \land b \in A) \land (\|F (b) - x\| < y \land \|F (b) - R\| < y)) \to F (a) - L \in ℂ$
207	206	abscld	$⊢ ((((((φ \land x \in ℂ) \land y \in ℝ^{+}) \land a \in A) \land (\|F (a) - x\| < y \land \|F (a) - L\| < y)) \land b \in A) \land (\|F (b) - x\| < y \land \|F (b) - R\| < y)) \to \|F (a) - L\| \in ℝ$
208	205 207	readdcld	$⊢ ((((((φ \land x \in ℂ) \land y \in ℝ^{+}) \land a \in A) \land (\|F (a) - x\| < y \land \|F (a) - L\| < y)) \land b \in A) \land (\|F (b) - x\| < y \land \|F (b) - R\| < y)) \to (\|R - F (b)\| + \|F (b) - x\|) + \|x - F (a)\| + \|F (a) - L\| \in ℝ$
209	21	a1i	$⊢ ((((((φ \land x \in ℂ) \land y \in ℝ^{+}) \land a \in A) \land (\|F (a) - x\| < y \land \|F (a) - L\| < y)) \land b \in A) \land (\|F (b) - x\| < y \land \|F (b) - R\| < y)) \to 4 \in ℝ$
210		rpre	$⊢ y \in ℝ^{+} \to y \in ℝ$
211	210	ad5antlr	$⊢ ((((((φ \land x \in ℂ) \land y \in ℝ^{+}) \land a \in A) \land (\|F (a) - x\| < y \land \|F (a) - L\| < y)) \land b \in A) \land (\|F (b) - x\| < y \land \|F (b) - R\| < y)) \to y \in ℝ$
212	209 211	remulcld	$⊢ ((((((φ \land x \in ℂ) \land y \in ℝ^{+}) \land a \in A) \land (\|F (a) - x\| < y \land \|F (a) - L\| < y)) \land b \in A) \land (\|F (b) - x\| < y \land \|F (b) - R\| < y)) \to 4 y \in ℝ$
213	186 193 196 202 187	absnpncan3d	$⊢ ((((((φ \land x \in ℂ) \land y \in ℝ^{+}) \land a \in A) \land (\|F (a) - x\| < y \land \|F (a) - L\| < y)) \land b \in A) \land (\|F (b) - x\| < y \land \|F (b) - R\| < y)) \to \|R - L\| \leq (\|R - F (b)\| + \|F (b) - x\|) + \|x - F (a)\| + \|F (a) - L\|$
214	186 193	abssubd	$⊢ ((((((φ \land x \in ℂ) \land y \in ℝ^{+}) \land a \in A) \land (\|F (a) - x\| < y \land \|F (a) - L\| < y)) \land b \in A) \land (\|F (b) - x\| < y \land \|F (b) - R\| < y)) \to \|R - F (b)\| = \|F (b) - R\|$
215		simprr	$⊢ ((((((φ \land x \in ℂ) \land y \in ℝ^{+}) \land a \in A) \land (\|F (a) - x\| < y \land \|F (a) - L\| < y)) \land b \in A) \land (\|F (b) - x\| < y \land \|F (b) - R\| < y)) \to \|F (b) - R\| < y$
216	214 215	eqbrtrd	$⊢ ((((((φ \land x \in ℂ) \land y \in ℝ^{+}) \land a \in A) \land (\|F (a) - x\| < y \land \|F (a) - L\| < y)) \land b \in A) \land (\|F (b) - x\| < y \land \|F (b) - R\| < y)) \to \|R - F (b)\| < y$
217		simprl	$⊢ ((((((φ \land x \in ℂ) \land y \in ℝ^{+}) \land a \in A) \land (\|F (a) - x\| < y \land \|F (a) - L\| < y)) \land b \in A) \land (\|F (b) - x\| < y \land \|F (b) - R\| < y)) \to \|F (b) - x\| < y$
218		simp-5r	$⊢ (((((φ \land x \in ℂ) \land y \in ℝ^{+}) \land a \in A) \land (\|F (a) - x\| < y \land \|F (a) - L\| < y)) \land b \in A) \to x \in ℂ$
219	201	ad5ant14	$⊢ ((((φ \land x \in ℂ) \land y \in ℝ^{+}) \land a \in A) \land (\|F (a) - x\| < y \land \|F (a) - L\| < y)) \to F (a) \in ℂ$
220	219	adantr	$⊢ (((((φ \land x \in ℂ) \land y \in ℝ^{+}) \land a \in A) \land (\|F (a) - x\| < y \land \|F (a) - L\| < y)) \land b \in A) \to F (a) \in ℂ$
221	218 220	abssubd	$⊢ (((((φ \land x \in ℂ) \land y \in ℝ^{+}) \land a \in A) \land (\|F (a) - x\| < y \land \|F (a) - L\| < y)) \land b \in A) \to \|x - F (a)\| = \|F (a) - x\|$
222		simplrl	$⊢ (((((φ \land x \in ℂ) \land y \in ℝ^{+}) \land a \in A) \land (\|F (a) - x\| < y \land \|F (a) - L\| < y)) \land b \in A) \to \|F (a) - x\| < y$
223	221 222	eqbrtrd	$⊢ (((((φ \land x \in ℂ) \land y \in ℝ^{+}) \land a \in A) \land (\|F (a) - x\| < y \land \|F (a) - L\| < y)) \land b \in A) \to \|x - F (a)\| < y$
224	223	adantr	$⊢ ((((((φ \land x \in ℂ) \land y \in ℝ^{+}) \land a \in A) \land (\|F (a) - x\| < y \land \|F (a) - L\| < y)) \land b \in A) \land (\|F (b) - x\| < y \land \|F (b) - R\| < y)) \to \|x - F (a)\| < y$
225		simplrr	$⊢ (((((φ \land x \in ℂ) \land y \in ℝ^{+}) \land a \in A) \land (\|F (a) - x\| < y \land \|F (a) - L\| < y)) \land b \in A) \to \|F (a) - L\| < y$
226	225	adantr	$⊢ ((((((φ \land x \in ℂ) \land y \in ℝ^{+}) \land a \in A) \land (\|F (a) - x\| < y \land \|F (a) - L\| < y)) \land b \in A) \land (\|F (b) - x\| < y \land \|F (b) - R\| < y)) \to \|F (a) - L\| < y$
227	195 198 204 207 211 216 217 224 226	lt4addmuld	$⊢ ((((((φ \land x \in ℂ) \land y \in ℝ^{+}) \land a \in A) \land (\|F (a) - x\| < y \land \|F (a) - L\| < y)) \land b \in A) \land (\|F (b) - x\| < y \land \|F (b) - R\| < y)) \to (\|R - F (b)\| + \|F (b) - x\|) + \|x - F (a)\| + \|F (a) - L\| < 4 y$
228	189 208 212 213 227	lelttrd	$⊢ ((((((φ \land x \in ℂ) \land y \in ℝ^{+}) \land a \in A) \land (\|F (a) - x\| < y \land \|F (a) - L\| < y)) \land b \in A) \land (\|F (b) - x\| < y \land \|F (b) - R\| < y)) \to \|R - L\| < 4 y$
229	228	ex	$⊢ (((((φ \land x \in ℂ) \land y \in ℝ^{+}) \land a \in A) \land (\|F (a) - x\| < y \land \|F (a) - L\| < y)) \land b \in A) \to ((\|F (b) - x\| < y \land \|F (b) - R\| < y) \to \|R - L\| < 4 y)$
230	229	adantl3r	$⊢ ((((((φ \land x \in ℂ) \land y \in ℝ^{+}) \land \exists z \in ℝ^{+} \forall w \in A ((w \neq B \land \|w - B\| < z) \to \|F (w) - x\| < y)) \land a \in A) \land (\|F (a) - x\| < y \land \|F (a) - L\| < y)) \land b \in A) \to ((\|F (b) - x\| < y \land \|F (b) - R\| < y) \to \|R - L\| < 4 y)$
231	230	reximdva	$⊢ (((((φ \land x \in ℂ) \land y \in ℝ^{+}) \land \exists z \in ℝ^{+} \forall w \in A ((w \neq B \land \|w - B\| < z) \to \|F (w) - x\| < y)) \land a \in A) \land (\|F (a) - x\| < y \land \|F (a) - L\| < y)) \to (\exists b \in A (\|F (b) - x\| < y \land \|F (b) - R\| < y) \to \exists b \in A \|R - L\| < 4 y)$
232	185 231	mpd	$⊢ (((((φ \land x \in ℂ) \land y \in ℝ^{+}) \land \exists z \in ℝ^{+} \forall w \in A ((w \neq B \land \|w - B\| < z) \to \|F (w) - x\| < y)) \land a \in A) \land (\|F (a) - x\| < y \land \|F (a) - L\| < y)) \to \exists b \in A \|R - L\| < 4 y$
233		fresin	$⊢ F : A ⟶ ℂ \to ({F ↾}_{(−∞, B)}) : A \cap (−∞, B) ⟶ ℂ$
234	4 233	syl	$⊢ φ \to ({F ↾}_{(−∞, B)}) : A \cap (−∞, B) ⟶ ℂ$
235		ioosscn	$⊢ (−∞, B) \subseteq ℂ$
236	50 235	sstri	$⊢ A \cap (−∞, B) \subseteq ℂ$
237	236	a1i	$⊢ φ \to A \cap (−∞, B) \subseteq ℂ$
238	234 237 59	ellimc3	$⊢ φ \to (L \in (({F ↾}_{(−∞, B)}) {lim}_{ℂ} B) \leftrightarrow (L \in ℂ \land \forall y \in ℝ^{+} \exists v \in ℝ^{+} \forall w \in (A \cap (−∞, B)) ((w \neq B \land \|w - B\| < v) \to \|({F ↾}_{(−∞, B)}) (w) - L\| < y)))$
239	7 238	mpbid	$⊢ φ \to (L \in ℂ \land \forall y \in ℝ^{+} \exists v \in ℝ^{+} \forall w \in (A \cap (−∞, B)) ((w \neq B \land \|w - B\| < v) \to \|({F ↾}_{(−∞, B)}) (w) - L\| < y))$
240	239	simprd	$⊢ φ \to \forall y \in ℝ^{+} \exists v \in ℝ^{+} \forall w \in (A \cap (−∞, B)) ((w \neq B \land \|w - B\| < v) \to \|({F ↾}_{(−∞, B)}) (w) - L\| < y)$
241	240	r19.21bi	$⊢ (φ \land y \in ℝ^{+}) \to \exists v \in ℝ^{+} \forall w \in (A \cap (−∞, B)) ((w \neq B \land \|w - B\| < v) \to \|({F ↾}_{(−∞, B)}) (w) - L\| < y)$
242	241	3ad2ant1	$⊢ ((φ \land y \in ℝ^{+}) \land z \in ℝ^{+} \land \forall w \in A ((w \neq B \land \|w - B\| < z) \to \|F (w) - x\| < y)) \to \exists v \in ℝ^{+} \forall w \in (A \cap (−∞, B)) ((w \neq B \land \|w - B\| < v) \to \|({F ↾}_{(−∞, B)}) (w) - L\| < y)$
243		simp11l	$⊢ (((φ \land y \in ℝ^{+}) \land z \in ℝ^{+} \land \forall w \in A ((w \neq B \land \|w - B\| < z) \to \|F (w) - x\| < y)) \land v \in ℝ^{+} \land \forall w \in (A \cap (−∞, B)) ((w \neq B \land \|w - B\| < v) \to \|({F ↾}_{(−∞, B)}) (w) - L\| < y)) \to φ$
244		simp12	$⊢ (((φ \land y \in ℝ^{+}) \land z \in ℝ^{+} \land \forall w \in A ((w \neq B \land \|w - B\| < z) \to \|F (w) - x\| < y)) \land v \in ℝ^{+} \land \forall w \in (A \cap (−∞, B)) ((w \neq B \land \|w - B\| < v) \to \|({F ↾}_{(−∞, B)}) (w) - L\| < y)) \to z \in ℝ^{+}$
245		simp2	$⊢ (((φ \land y \in ℝ^{+}) \land z \in ℝ^{+} \land \forall w \in A ((w \neq B \land \|w - B\| < z) \to \|F (w) - x\| < y)) \land v \in ℝ^{+} \land \forall w \in (A \cap (−∞, B)) ((w \neq B \land \|w - B\| < v) \to \|({F ↾}_{(−∞, B)}) (w) - L\| < y)) \to v \in ℝ^{+}$
246		breq2	$⊢ u = if (z \leq v, z, v) \to (\|a - B\| < u \leftrightarrow \|a - B\| < if (z \leq v, z, v))$
247	246	rexbidv	$⊢ u = if (z \leq v, z, v) \to (\exists a \in ((A \cap (−∞, B)) ∖ \{B\}) \|a - B\| < u \leftrightarrow \exists a \in ((A \cap (−∞, B)) ∖ \{B\}) \|a - B\| < if (z \leq v, z, v))$
248		inss1	$⊢ limPt (K) (A \cap (−∞, B)) \cap ℝ \subseteq limPt (K) (A \cap (−∞, B))$
249	248	a1i	$⊢ φ \to limPt (K) (A \cap (−∞, B)) \cap ℝ \subseteq limPt (K) (A \cap (−∞, B))$
250	52	a1i	$⊢ φ \to A \cap (−∞, B) \subseteq ℝ$
251	81 83	restlp	$⊢ (K \in Top \land ℝ \subseteq ℂ \land A \cap (−∞, B) \subseteq ℝ) \to limPt (J) (A \cap (−∞, B)) = limPt (K) (A \cap (−∞, B)) \cap ℝ$
252	73 75 250 251	syl3anc	$⊢ φ \to limPt (J) (A \cap (−∞, B)) = limPt (K) (A \cap (−∞, B)) \cap ℝ$
253	87	fveq1i	$⊢ limPt (TopOpen (ℂ_{fld})) (A \cap (−∞, B)) = limPt (K) (A \cap (−∞, B))$
254	253	a1i	$⊢ φ \to limPt (TopOpen (ℂ_{fld})) (A \cap (−∞, B)) = limPt (K) (A \cap (−∞, B))$
255	249 252 254	3sstr4d	$⊢ φ \to limPt (J) (A \cap (−∞, B)) \subseteq limPt (TopOpen (ℂ_{fld})) (A \cap (−∞, B))$
256	255 5	sseldd	$⊢ φ \to B \in limPt (TopOpen (ℂ_{fld})) (A \cap (−∞, B))$
257	237 59	islpcn	$⊢ φ \to (B \in limPt (TopOpen (ℂ_{fld})) (A \cap (−∞, B)) \leftrightarrow \forall u \in ℝ^{+} \exists a \in ((A \cap (−∞, B)) ∖ \{B\}) \|a - B\| < u)$
258	256 257	mpbid	$⊢ φ \to \forall u \in ℝ^{+} \exists a \in ((A \cap (−∞, B)) ∖ \{B\}) \|a - B\| < u$
259	258	3ad2ant1	$⊢ (φ \land z \in ℝ^{+} \land v \in ℝ^{+}) \to \forall u \in ℝ^{+} \exists a \in ((A \cap (−∞, B)) ∖ \{B\}) \|a - B\| < u$
260	247 259 96	rspcdva	$⊢ (φ \land z \in ℝ^{+} \land v \in ℝ^{+}) \to \exists a \in ((A \cap (−∞, B)) ∖ \{B\}) \|a - B\| < if (z \leq v, z, v)$
261		eldifi	$⊢ a \in ((A \cap (−∞, B)) ∖ \{B\}) \to a \in (A \cap (−∞, B))$
262	52 261	sselid	$⊢ a \in ((A \cap (−∞, B)) ∖ \{B\}) \to a \in ℝ$
263	75	sselda	$⊢ (φ \land a \in ℝ) \to a \in ℂ$
264	59	adantr	$⊢ (φ \land a \in ℝ) \to B \in ℂ$
265	263 264	subcld	$⊢ (φ \land a \in ℝ) \to a - B \in ℂ$
266	265	abscld	$⊢ (φ \land a \in ℝ) \to \|a - B\| \in ℝ$
267	266	3ad2antl1	$⊢ ((φ \land z \in ℝ^{+} \land v \in ℝ^{+}) \land a \in ℝ) \to \|a - B\| \in ℝ$
268	267	adantr	$⊢ (((φ \land z \in ℝ^{+} \land v \in ℝ^{+}) \land a \in ℝ) \land \|a - B\| < if (z \leq v, z, v)) \to \|a - B\| \in ℝ$
269	106	ad2antrr	$⊢ (((φ \land z \in ℝ^{+} \land v \in ℝ^{+}) \land a \in ℝ) \land \|a - B\| < if (z \leq v, z, v)) \to if (z \leq v, z, v) \in ℝ$
270	109	ad2antrr	$⊢ (((φ \land z \in ℝ^{+} \land v \in ℝ^{+}) \land a \in ℝ) \land \|a - B\| < if (z \leq v, z, v)) \to z \in ℝ$
271		simpr	$⊢ (((φ \land z \in ℝ^{+} \land v \in ℝ^{+}) \land a \in ℝ) \land \|a - B\| < if (z \leq v, z, v)) \to \|a - B\| < if (z \leq v, z, v)$
272	115	ad2antrr	$⊢ (((φ \land z \in ℝ^{+} \land v \in ℝ^{+}) \land a \in ℝ) \land \|a - B\| < if (z \leq v, z, v)) \to if (z \leq v, z, v) \leq z$
273	268 269 270 271 272	ltletrd	$⊢ (((φ \land z \in ℝ^{+} \land v \in ℝ^{+}) \land a \in ℝ) \land \|a - B\| < if (z \leq v, z, v)) \to \|a - B\| < z$
274	118	ad2antrr	$⊢ (((φ \land z \in ℝ^{+} \land v \in ℝ^{+}) \land a \in ℝ) \land \|a - B\| < if (z \leq v, z, v)) \to v \in ℝ$
275		min2	$⊢ (z \in ℝ \land v \in ℝ) \to if (z \leq v, z, v) \leq v$
276	108 112 275	syl2an	$⊢ (z \in ℝ^{+} \land v \in ℝ^{+}) \to if (z \leq v, z, v) \leq v$
277	276	3adant1	$⊢ (φ \land z \in ℝ^{+} \land v \in ℝ^{+}) \to if (z \leq v, z, v) \leq v$
278	277	ad2antrr	$⊢ (((φ \land z \in ℝ^{+} \land v \in ℝ^{+}) \land a \in ℝ) \land \|a - B\| < if (z \leq v, z, v)) \to if (z \leq v, z, v) \leq v$
279	268 269 274 271 278	ltletrd	$⊢ (((φ \land z \in ℝ^{+} \land v \in ℝ^{+}) \land a \in ℝ) \land \|a - B\| < if (z \leq v, z, v)) \to \|a - B\| < v$
280	273 279	jca	$⊢ (((φ \land z \in ℝ^{+} \land v \in ℝ^{+}) \land a \in ℝ) \land \|a - B\| < if (z \leq v, z, v)) \to (\|a - B\| < z \land \|a - B\| < v)$
281	280	ex	$⊢ ((φ \land z \in ℝ^{+} \land v \in ℝ^{+}) \land a \in ℝ) \to (\|a - B\| < if (z \leq v, z, v) \to (\|a - B\| < z \land \|a - B\| < v))$
282	262 281	sylan2	$⊢ ((φ \land z \in ℝ^{+} \land v \in ℝ^{+}) \land a \in ((A \cap (−∞, B)) ∖ \{B\})) \to (\|a - B\| < if (z \leq v, z, v) \to (\|a - B\| < z \land \|a - B\| < v))$
283	282	reximdva	$⊢ (φ \land z \in ℝ^{+} \land v \in ℝ^{+}) \to (\exists a \in ((A \cap (−∞, B)) ∖ \{B\}) \|a - B\| < if (z \leq v, z, v) \to \exists a \in ((A \cap (−∞, B)) ∖ \{B\}) (\|a - B\| < z \land \|a - B\| < v))$
284	260 283	mpd	$⊢ (φ \land z \in ℝ^{+} \land v \in ℝ^{+}) \to \exists a \in ((A \cap (−∞, B)) ∖ \{B\}) (\|a - B\| < z \land \|a - B\| < v)$
285	243 244 245 284	syl3anc	$⊢ (((φ \land y \in ℝ^{+}) \land z \in ℝ^{+} \land \forall w \in A ((w \neq B \land \|w - B\| < z) \to \|F (w) - x\| < y)) \land v \in ℝ^{+} \land \forall w \in (A \cap (−∞, B)) ((w \neq B \land \|w - B\| < v) \to \|({F ↾}_{(−∞, B)}) (w) - L\| < y)) \to \exists a \in ((A \cap (−∞, B)) ∖ \{B\}) (\|a - B\| < z \land \|a - B\| < v)$
286		nfv	$⊢ Ⅎ a (((φ \land y \in ℝ^{+}) \land z \in ℝ^{+} \land \forall w \in A ((w \neq B \land \|w - B\| < z) \to \|F (w) - x\| < y)) \land v \in ℝ^{+} \land \forall w \in (A \cap (−∞, B)) ((w \neq B \land \|w - B\| < v) \to \|({F ↾}_{(−∞, B)}) (w) - L\| < y))$
287		nfre1	$⊢ Ⅎ a \exists a \in A (\|F (a) - x\| < y \land \|F (a) - L\| < y)$
288	261	elin1d	$⊢ a \in ((A \cap (−∞, B)) ∖ \{B\}) \to a \in A$
289	288	3ad2ant2	$⊢ ((((φ \land y \in ℝ^{+}) \land z \in ℝ^{+} \land \forall w \in A ((w \neq B \land \|w - B\| < z) \to \|F (w) - x\| < y)) \land v \in ℝ^{+} \land \forall w \in (A \cap (−∞, B)) ((w \neq B \land \|w - B\| < v) \to \|({F ↾}_{(−∞, B)}) (w) - L\| < y)) \land a \in ((A \cap (−∞, B)) ∖ \{B\}) \land (\|a - B\| < z \land \|a - B\| < v)) \to a \in A$
290		simp113	$⊢ ((((φ \land y \in ℝ^{+}) \land z \in ℝ^{+} \land \forall w \in A ((w \neq B \land \|w - B\| < z) \to \|F (w) - x\| < y)) \land v \in ℝ^{+} \land \forall w \in (A \cap (−∞, B)) ((w \neq B \land \|w - B\| < v) \to \|({F ↾}_{(−∞, B)}) (w) - L\| < y)) \land a \in ((A \cap (−∞, B)) ∖ \{B\}) \land (\|a - B\| < z \land \|a - B\| < v)) \to \forall w \in A ((w \neq B \land \|w - B\| < z) \to \|F (w) - x\| < y)$
291		eldifsni	$⊢ a \in ((A \cap (−∞, B)) ∖ \{B\}) \to a \neq B$
292	291	adantr	$⊢ (a \in ((A \cap (−∞, B)) ∖ \{B\}) \land (\|a - B\| < z \land \|a - B\| < v)) \to a \neq B$
293		simprl	$⊢ (a \in ((A \cap (−∞, B)) ∖ \{B\}) \land (\|a - B\| < z \land \|a - B\| < v)) \to \|a - B\| < z$
294	292 293	jca	$⊢ (a \in ((A \cap (−∞, B)) ∖ \{B\}) \land (\|a - B\| < z \land \|a - B\| < v)) \to (a \neq B \land \|a - B\| < z)$
295	294	3adant1	$⊢ ((((φ \land y \in ℝ^{+}) \land z \in ℝ^{+} \land \forall w \in A ((w \neq B \land \|w - B\| < z) \to \|F (w) - x\| < y)) \land v \in ℝ^{+} \land \forall w \in (A \cap (−∞, B)) ((w \neq B \land \|w - B\| < v) \to \|({F ↾}_{(−∞, B)}) (w) - L\| < y)) \land a \in ((A \cap (−∞, B)) ∖ \{B\}) \land (\|a - B\| < z \land \|a - B\| < v)) \to (a \neq B \land \|a - B\| < z)$
296		neeq1	$⊢ w = a \to (w \neq B \leftrightarrow a \neq B)$
297		fvoveq1	$⊢ w = a \to \|w - B\| = \|a - B\|$
298	297	breq1d	$⊢ w = a \to (\|w - B\| < z \leftrightarrow \|a - B\| < z)$
299	296 298	anbi12d	$⊢ w = a \to ((w \neq B \land \|w - B\| < z) \leftrightarrow (a \neq B \land \|a - B\| < z))$
300	299	imbrov2fvoveq	$⊢ w = a \to (((w \neq B \land \|w - B\| < z) \to \|F (w) - x\| < y) \leftrightarrow ((a \neq B \land \|a - B\| < z) \to \|F (a) - x\| < y))$
301	300	rspcva	$⊢ (a \in A \land \forall w \in A ((w \neq B \land \|w - B\| < z) \to \|F (w) - x\| < y)) \to ((a \neq B \land \|a - B\| < z) \to \|F (a) - x\| < y)$
302	301	imp	$⊢ ((a \in A \land \forall w \in A ((w \neq B \land \|w - B\| < z) \to \|F (w) - x\| < y)) \land (a \neq B \land \|a - B\| < z)) \to \|F (a) - x\| < y$
303	289 290 295 302	syl21anc	$⊢ ((((φ \land y \in ℝ^{+}) \land z \in ℝ^{+} \land \forall w \in A ((w \neq B \land \|w - B\| < z) \to \|F (w) - x\| < y)) \land v \in ℝ^{+} \land \forall w \in (A \cap (−∞, B)) ((w \neq B \land \|w - B\| < v) \to \|({F ↾}_{(−∞, B)}) (w) - L\| < y)) \land a \in ((A \cap (−∞, B)) ∖ \{B\}) \land (\|a - B\| < z \land \|a - B\| < v)) \to \|F (a) - x\| < y$
304	261	3ad2ant2	$⊢ ((((φ \land y \in ℝ^{+}) \land z \in ℝ^{+} \land \forall w \in A ((w \neq B \land \|w - B\| < z) \to \|F (w) - x\| < y)) \land v \in ℝ^{+} \land \forall w \in (A \cap (−∞, B)) ((w \neq B \land \|w - B\| < v) \to \|({F ↾}_{(−∞, B)}) (w) - L\| < y)) \land a \in ((A \cap (−∞, B)) ∖ \{B\}) \land (\|a - B\| < z \land \|a - B\| < v)) \to a \in (A \cap (−∞, B))$
305	243	3ad2ant1	$⊢ ((((φ \land y \in ℝ^{+}) \land z \in ℝ^{+} \land \forall w \in A ((w \neq B \land \|w - B\| < z) \to \|F (w) - x\| < y)) \land v \in ℝ^{+} \land \forall w \in (A \cap (−∞, B)) ((w \neq B \land \|w - B\| < v) \to \|({F ↾}_{(−∞, B)}) (w) - L\| < y)) \land a \in ((A \cap (−∞, B)) ∖ \{B\}) \land (\|a - B\| < z \land \|a - B\| < v)) \to φ$
306		simp13	$⊢ ((((φ \land y \in ℝ^{+}) \land z \in ℝ^{+} \land \forall w \in A ((w \neq B \land \|w - B\| < z) \to \|F (w) - x\| < y)) \land v \in ℝ^{+} \land \forall w \in (A \cap (−∞, B)) ((w \neq B \land \|w - B\| < v) \to \|({F ↾}_{(−∞, B)}) (w) - L\| < y)) \land a \in ((A \cap (−∞, B)) ∖ \{B\}) \land (\|a - B\| < z \land \|a - B\| < v)) \to \forall w \in (A \cap (−∞, B)) ((w \neq B \land \|w - B\| < v) \to \|({F ↾}_{(−∞, B)}) (w) - L\| < y)$
307		nfra1	$⊢ Ⅎ w \forall w \in (A \cap (−∞, B)) ((w \neq B \land \|w - B\| < v) \to \|({F ↾}_{(−∞, B)}) (w) - L\| < y)$
308	149 307	nfan	$⊢ Ⅎ w (φ \land \forall w \in (A \cap (−∞, B)) ((w \neq B \land \|w - B\| < v) \to \|({F ↾}_{(−∞, B)}) (w) - L\| < y))$
309		elinel2	$⊢ w \in (A \cap (−∞, B)) \to w \in (−∞, B)$
310	309	fvresd	$⊢ w \in (A \cap (−∞, B)) \to ({F ↾}_{(−∞, B)}) (w) = F (w)$
311	310	eqcomd	$⊢ w \in (A \cap (−∞, B)) \to F (w) = ({F ↾}_{(−∞, B)}) (w)$
312	311	fvoveq1d	$⊢ w \in (A \cap (−∞, B)) \to \|F (w) - L\| = \|({F ↾}_{(−∞, B)}) (w) - L\|$
313	312	3ad2ant2	$⊢ ((φ \land \forall w \in (A \cap (−∞, B)) ((w \neq B \land \|w - B\| < v) \to \|({F ↾}_{(−∞, B)}) (w) - L\| < y)) \land w \in (A \cap (−∞, B)) \land (w \neq B \land \|w - B\| < v)) \to \|F (w) - L\| = \|({F ↾}_{(−∞, B)}) (w) - L\|$
314		rspa	$⊢ (\forall w \in (A \cap (−∞, B)) ((w \neq B \land \|w - B\| < v) \to \|({F ↾}_{(−∞, B)}) (w) - L\| < y) \land w \in (A \cap (−∞, B))) \to ((w \neq B \land \|w - B\| < v) \to \|({F ↾}_{(−∞, B)}) (w) - L\| < y)$
315	314	3impia	$⊢ (\forall w \in (A \cap (−∞, B)) ((w \neq B \land \|w - B\| < v) \to \|({F ↾}_{(−∞, B)}) (w) - L\| < y) \land w \in (A \cap (−∞, B)) \land (w \neq B \land \|w - B\| < v)) \to \|({F ↾}_{(−∞, B)}) (w) - L\| < y$
316	315	3adant1l	$⊢ ((φ \land \forall w \in (A \cap (−∞, B)) ((w \neq B \land \|w - B\| < v) \to \|({F ↾}_{(−∞, B)}) (w) - L\| < y)) \land w \in (A \cap (−∞, B)) \land (w \neq B \land \|w - B\| < v)) \to \|({F ↾}_{(−∞, B)}) (w) - L\| < y$
317	313 316	eqbrtrd	$⊢ ((φ \land \forall w \in (A \cap (−∞, B)) ((w \neq B \land \|w - B\| < v) \to \|({F ↾}_{(−∞, B)}) (w) - L\| < y)) \land w \in (A \cap (−∞, B)) \land (w \neq B \land \|w - B\| < v)) \to \|F (w) - L\| < y$
318	317	3exp	$⊢ (φ \land \forall w \in (A \cap (−∞, B)) ((w \neq B \land \|w - B\| < v) \to \|({F ↾}_{(−∞, B)}) (w) - L\| < y)) \to (w \in (A \cap (−∞, B)) \to ((w \neq B \land \|w - B\| < v) \to \|F (w) - L\| < y))$
319	308 318	ralrimi	$⊢ (φ \land \forall w \in (A \cap (−∞, B)) ((w \neq B \land \|w - B\| < v) \to \|({F ↾}_{(−∞, B)}) (w) - L\| < y)) \to \forall w \in (A \cap (−∞, B)) ((w \neq B \land \|w - B\| < v) \to \|F (w) - L\| < y)$
320	305 306 319	syl2anc	$⊢ ((((φ \land y \in ℝ^{+}) \land z \in ℝ^{+} \land \forall w \in A ((w \neq B \land \|w - B\| < z) \to \|F (w) - x\| < y)) \land v \in ℝ^{+} \land \forall w \in (A \cap (−∞, B)) ((w \neq B \land \|w - B\| < v) \to \|({F ↾}_{(−∞, B)}) (w) - L\| < y)) \land a \in ((A \cap (−∞, B)) ∖ \{B\}) \land (\|a - B\| < z \land \|a - B\| < v)) \to \forall w \in (A \cap (−∞, B)) ((w \neq B \land \|w - B\| < v) \to \|F (w) - L\| < y)$
321	291	anim1i	$⊢ (a \in ((A \cap (−∞, B)) ∖ \{B\}) \land \|a - B\| < v) \to (a \neq B \land \|a - B\| < v)$
322	321	adantrl	$⊢ (a \in ((A \cap (−∞, B)) ∖ \{B\}) \land (\|a - B\| < z \land \|a - B\| < v)) \to (a \neq B \land \|a - B\| < v)$
323	322	3adant1	$⊢ ((((φ \land y \in ℝ^{+}) \land z \in ℝ^{+} \land \forall w \in A ((w \neq B \land \|w - B\| < z) \to \|F (w) - x\| < y)) \land v \in ℝ^{+} \land \forall w \in (A \cap (−∞, B)) ((w \neq B \land \|w - B\| < v) \to \|({F ↾}_{(−∞, B)}) (w) - L\| < y)) \land a \in ((A \cap (−∞, B)) ∖ \{B\}) \land (\|a - B\| < z \land \|a - B\| < v)) \to (a \neq B \land \|a - B\| < v)$
324	297	breq1d	$⊢ w = a \to (\|w - B\| < v \leftrightarrow \|a - B\| < v)$
325	296 324	anbi12d	$⊢ w = a \to ((w \neq B \land \|w - B\| < v) \leftrightarrow (a \neq B \land \|a - B\| < v))$
326	325	imbrov2fvoveq	$⊢ w = a \to (((w \neq B \land \|w - B\| < v) \to \|F (w) - L\| < y) \leftrightarrow ((a \neq B \land \|a - B\| < v) \to \|F (a) - L\| < y))$
327	326	rspcva	$⊢ (a \in (A \cap (−∞, B)) \land \forall w \in (A \cap (−∞, B)) ((w \neq B \land \|w - B\| < v) \to \|F (w) - L\| < y)) \to ((a \neq B \land \|a - B\| < v) \to \|F (a) - L\| < y)$
328	327	imp	$⊢ ((a \in (A \cap (−∞, B)) \land \forall w \in (A \cap (−∞, B)) ((w \neq B \land \|w - B\| < v) \to \|F (w) - L\| < y)) \land (a \neq B \land \|a - B\| < v)) \to \|F (a) - L\| < y$
329	304 320 323 328	syl21anc	$⊢ ((((φ \land y \in ℝ^{+}) \land z \in ℝ^{+} \land \forall w \in A ((w \neq B \land \|w - B\| < z) \to \|F (w) - x\| < y)) \land v \in ℝ^{+} \land \forall w \in (A \cap (−∞, B)) ((w \neq B \land \|w - B\| < v) \to \|({F ↾}_{(−∞, B)}) (w) - L\| < y)) \land a \in ((A \cap (−∞, B)) ∖ \{B\}) \land (\|a - B\| < z \land \|a - B\| < v)) \to \|F (a) - L\| < y$
330		rspe	$⊢ (a \in A \land (\|F (a) - x\| < y \land \|F (a) - L\| < y)) \to \exists a \in A (\|F (a) - x\| < y \land \|F (a) - L\| < y)$
331	289 303 329 330	syl12anc	$⊢ ((((φ \land y \in ℝ^{+}) \land z \in ℝ^{+} \land \forall w \in A ((w \neq B \land \|w - B\| < z) \to \|F (w) - x\| < y)) \land v \in ℝ^{+} \land \forall w \in (A \cap (−∞, B)) ((w \neq B \land \|w - B\| < v) \to \|({F ↾}_{(−∞, B)}) (w) - L\| < y)) \land a \in ((A \cap (−∞, B)) ∖ \{B\}) \land (\|a - B\| < z \land \|a - B\| < v)) \to \exists a \in A (\|F (a) - x\| < y \land \|F (a) - L\| < y)$
332	331	3exp	$⊢ (((φ \land y \in ℝ^{+}) \land z \in ℝ^{+} \land \forall w \in A ((w \neq B \land \|w - B\| < z) \to \|F (w) - x\| < y)) \land v \in ℝ^{+} \land \forall w \in (A \cap (−∞, B)) ((w \neq B \land \|w - B\| < v) \to \|({F ↾}_{(−∞, B)}) (w) - L\| < y)) \to (a \in ((A \cap (−∞, B)) ∖ \{B\}) \to ((\|a - B\| < z \land \|a - B\| < v) \to \exists a \in A (\|F (a) - x\| < y \land \|F (a) - L\| < y)))$
333	286 287 332	rexlimd	$⊢ (((φ \land y \in ℝ^{+}) \land z \in ℝ^{+} \land \forall w \in A ((w \neq B \land \|w - B\| < z) \to \|F (w) - x\| < y)) \land v \in ℝ^{+} \land \forall w \in (A \cap (−∞, B)) ((w \neq B \land \|w - B\| < v) \to \|({F ↾}_{(−∞, B)}) (w) - L\| < y)) \to (\exists a \in ((A \cap (−∞, B)) ∖ \{B\}) (\|a - B\| < z \land \|a - B\| < v) \to \exists a \in A (\|F (a) - x\| < y \land \|F (a) - L\| < y))$
334	285 333	mpd	$⊢ (((φ \land y \in ℝ^{+}) \land z \in ℝ^{+} \land \forall w \in A ((w \neq B \land \|w - B\| < z) \to \|F (w) - x\| < y)) \land v \in ℝ^{+} \land \forall w \in (A \cap (−∞, B)) ((w \neq B \land \|w - B\| < v) \to \|({F ↾}_{(−∞, B)}) (w) - L\| < y)) \to \exists a \in A (\|F (a) - x\| < y \land \|F (a) - L\| < y)$
335	334	3exp	$⊢ ((φ \land y \in ℝ^{+}) \land z \in ℝ^{+} \land \forall w \in A ((w \neq B \land \|w - B\| < z) \to \|F (w) - x\| < y)) \to (v \in ℝ^{+} \to (\forall w \in (A \cap (−∞, B)) ((w \neq B \land \|w - B\| < v) \to \|({F ↾}_{(−∞, B)}) (w) - L\| < y) \to \exists a \in A (\|F (a) - x\| < y \land \|F (a) - L\| < y)))$
336	335	rexlimdv	$⊢ ((φ \land y \in ℝ^{+}) \land z \in ℝ^{+} \land \forall w \in A ((w \neq B \land \|w - B\| < z) \to \|F (w) - x\| < y)) \to (\exists v \in ℝ^{+} \forall w \in (A \cap (−∞, B)) ((w \neq B \land \|w - B\| < v) \to \|({F ↾}_{(−∞, B)}) (w) - L\| < y) \to \exists a \in A (\|F (a) - x\| < y \land \|F (a) - L\| < y))$
337	242 336	mpd	$⊢ ((φ \land y \in ℝ^{+}) \land z \in ℝ^{+} \land \forall w \in A ((w \neq B \land \|w - B\| < z) \to \|F (w) - x\| < y)) \to \exists a \in A (\|F (a) - x\| < y \land \|F (a) - L\| < y)$
338	337	3exp	$⊢ (φ \land y \in ℝ^{+}) \to (z \in ℝ^{+} \to (\forall w \in A ((w \neq B \land \|w - B\| < z) \to \|F (w) - x\| < y) \to \exists a \in A (\|F (a) - x\| < y \land \|F (a) - L\| < y)))$
339	338	rexlimdv	$⊢ (φ \land y \in ℝ^{+}) \to (\exists z \in ℝ^{+} \forall w \in A ((w \neq B \land \|w - B\| < z) \to \|F (w) - x\| < y) \to \exists a \in A (\|F (a) - x\| < y \land \|F (a) - L\| < y))$
340	339	imp	$⊢ ((φ \land y \in ℝ^{+}) \land \exists z \in ℝ^{+} \forall w \in A ((w \neq B \land \|w - B\| < z) \to \|F (w) - x\| < y)) \to \exists a \in A (\|F (a) - x\| < y \land \|F (a) - L\| < y)$
341	340	adantllr	$⊢ (((φ \land x \in ℂ) \land y \in ℝ^{+}) \land \exists z \in ℝ^{+} \forall w \in A ((w \neq B \land \|w - B\| < z) \to \|F (w) - x\| < y)) \to \exists a \in A (\|F (a) - x\| < y \land \|F (a) - L\| < y)$
342	232 341	reximddv3	$⊢ (((φ \land x \in ℂ) \land y \in ℝ^{+}) \land \exists z \in ℝ^{+} \forall w \in A ((w \neq B \land \|w - B\| < z) \to \|F (w) - x\| < y)) \to \exists a \in A \exists b \in A \|R - L\| < 4 y$
343	38 39 41 342	syl21anc	$⊢ (((φ \land x \in ℂ) \land \forall y \in ℝ^{+} \exists z \in ℝ^{+} \forall w \in A ((w \neq B \land \|w - B\| < z) \to \|F (w) - x\| < y)) \land y \in ℝ^{+}) \to \exists a \in A \exists b \in A \|R - L\| < 4 y$
344	343	ex	$⊢ ((φ \land x \in ℂ) \land \forall y \in ℝ^{+} \exists z \in ℝ^{+} \forall w \in A ((w \neq B \land \|w - B\| < z) \to \|F (w) - x\| < y)) \to (y \in ℝ^{+} \to \exists a \in A \exists b \in A \|R - L\| < 4 y)$
345	30 31 37 344	vtoclf	$⊢ ((φ \land x \in ℂ) \land \forall y \in ℝ^{+} \exists z \in ℝ^{+} \forall w \in A ((w \neq B \land \|w - B\| < z) \to \|F (w) - x\| < y)) \to (\frac{\|R - L\|}{4} \in ℝ^{+} \to \exists a \in A \exists b \in A \|R - L\| < 4 (\frac{\|R - L\|}{4}))$
346	25 345	mpd	$⊢ ((φ \land x \in ℂ) \land \forall y \in ℝ^{+} \exists z \in ℝ^{+} \forall w \in A ((w \neq B \land \|w - B\| < z) \to \|F (w) - x\| < y)) \to \exists a \in A \exists b \in A \|R - L\| < 4 (\frac{\|R - L\|}{4})$
347		simpr	$⊢ (φ \land \|R - L\| < 4 (\frac{\|R - L\|}{4})) \to \|R - L\| < 4 (\frac{\|R - L\|}{4})$
348		abssubrp	$⊢ (R \in ℂ \land L \in ℂ \land R \neq L) \to \|R - L\| \in ℝ^{+}$
349	11 14 17 348	syl3anc	$⊢ φ \to \|R - L\| \in ℝ^{+}$
350	349	rpcnd	$⊢ φ \to \|R - L\| \in ℂ$
351	350	adantr	$⊢ (φ \land \|R - L\| < 4 (\frac{\|R - L\|}{4})) \to \|R - L\| \in ℂ$
352		4cn	$⊢ 4 \in ℂ$
353	352	a1i	$⊢ (φ \land \|R - L\| < 4 (\frac{\|R - L\|}{4})) \to 4 \in ℂ$
354		4ne0	$⊢ 4 \neq 0$
355	354	a1i	$⊢ (φ \land \|R - L\| < 4 (\frac{\|R - L\|}{4})) \to 4 \neq 0$
356	351 353 355	divcan2d	$⊢ (φ \land \|R - L\| < 4 (\frac{\|R - L\|}{4})) \to 4 (\frac{\|R - L\|}{4}) = \|R - L\|$
357	347 356	breqtrd	$⊢ (φ \land \|R - L\| < 4 (\frac{\|R - L\|}{4})) \to \|R - L\| < \|R - L\|$
358	357	ex	$⊢ φ \to (\|R - L\| < 4 (\frac{\|R - L\|}{4}) \to \|R - L\| < \|R - L\|)$
359	358	a1d	$⊢ φ \to ((a \in A \land b \in A) \to (\|R - L\| < 4 (\frac{\|R - L\|}{4}) \to \|R - L\| < \|R - L\|))$
360	359	ad2antrr	$⊢ ((φ \land x \in ℂ) \land \forall y \in ℝ^{+} \exists z \in ℝ^{+} \forall w \in A ((w \neq B \land \|w - B\| < z) \to \|F (w) - x\| < y)) \to ((a \in A \land b \in A) \to (\|R - L\| < 4 (\frac{\|R - L\|}{4}) \to \|R - L\| < \|R - L\|))$
361	360	rexlimdvv	$⊢ ((φ \land x \in ℂ) \land \forall y \in ℝ^{+} \exists z \in ℝ^{+} \forall w \in A ((w \neq B \land \|w - B\| < z) \to \|F (w) - x\| < y)) \to (\exists a \in A \exists b \in A \|R - L\| < 4 (\frac{\|R - L\|}{4}) \to \|R - L\| < \|R - L\|)$
362	346 361	mpd	$⊢ ((φ \land x \in ℂ) \land \forall y \in ℝ^{+} \exists z \in ℝ^{+} \forall w \in A ((w \neq B \land \|w - B\| < z) \to \|F (w) - x\| < y)) \to \|R - L\| < \|R - L\|$
363	16	abscld	$⊢ ((φ \land x \in ℂ) \land \forall y \in ℝ^{+} \exists z \in ℝ^{+} \forall w \in A ((w \neq B \land \|w - B\| < z) \to \|F (w) - x\| < y)) \to \|R - L\| \in ℝ$
364	363	ltnrd	$⊢ ((φ \land x \in ℂ) \land \forall y \in ℝ^{+} \exists z \in ℝ^{+} \forall w \in A ((w \neq B \land \|w - B\| < z) \to \|F (w) - x\| < y)) \to \neg \|R - L\| < \|R - L\|$
365	362 364	pm2.65da	$⊢ (φ \land x \in ℂ) \to \neg \forall y \in ℝ^{+} \exists z \in ℝ^{+} \forall w \in A ((w \neq B \land \|w - B\| < z) \to \|F (w) - x\| < y)$
366	365	ex	$⊢ φ \to (x \in ℂ \to \neg \forall y \in ℝ^{+} \exists z \in ℝ^{+} \forall w \in A ((w \neq B \land \|w - B\| < z) \to \|F (w) - x\| < y))$
367		imnan	$⊢ (x \in ℂ \to \neg \forall y \in ℝ^{+} \exists z \in ℝ^{+} \forall w \in A ((w \neq B \land \|w - B\| < z) \to \|F (w) - x\| < y)) \leftrightarrow \neg (x \in ℂ \land \forall y \in ℝ^{+} \exists z \in ℝ^{+} \forall w \in A ((w \neq B \land \|w - B\| < z) \to \|F (w) - x\| < y))$
368	366 367	sylib	$⊢ φ \to \neg (x \in ℂ \land \forall y \in ℝ^{+} \exists z \in ℝ^{+} \forall w \in A ((w \neq B \land \|w - B\| < z) \to \|F (w) - x\| < y))$
369	2 75	sstrd	$⊢ φ \to A \subseteq ℂ$
370	4 369 59	ellimc3	$⊢ φ \to (x \in (F {lim}_{ℂ} B) \leftrightarrow (x \in ℂ \land \forall y \in ℝ^{+} \exists z \in ℝ^{+} \forall w \in A ((w \neq B \land \|w - B\| < z) \to \|F (w) - x\| < y)))$
371	368 370	mtbird	$⊢ φ \to \neg x \in (F {lim}_{ℂ} B)$
372	371	eq0rdv	$⊢ φ \to F {lim}_{ℂ} B = \emptyset$

Metamath Proof Explorer

Theorem limclner

Proof