dvcnp2

Description: A function is continuous at each point for which it is differentiable. (Contributed by Mario Carneiro, 9-Aug-2014) (Revised by Mario Carneiro, 28-Dec-2016) Avoid ax-mulf . (Revised by GG, 16-Mar-2025)

	Ref	Expression
Hypotheses	dvcnp.j	$⊢ J = K ↾_{𝑡} A$
	dvcnp.k	$⊢ K = TopOpen (ℂ_{fld})$
Assertion	dvcnp2	$⊢ ((S \subseteq ℂ \land F : A ⟶ ℂ \land A \subseteq S) \land B \in dom F_{S}^{'}) \to F \in (J CnP K) (B)$

Proof

Step	Hyp	Ref	Expression
1		dvcnp.j	$⊢ J = K ↾_{𝑡} A$
2		dvcnp.k	$⊢ K = TopOpen (ℂ_{fld})$
3		simpl2	$⊢ ((S \subseteq ℂ \land F : A ⟶ ℂ \land A \subseteq S) \land B F_{S}^{'} y) \to F : A ⟶ ℂ$
4	3	ffvelcdmda	$⊢ (((S \subseteq ℂ \land F : A ⟶ ℂ \land A \subseteq S) \land B F_{S}^{'} y) \land z \in A) \to F (z) \in ℂ$
5	2	cnfldtop	$⊢ K \in Top$
6		simpl1	$⊢ ((S \subseteq ℂ \land F : A ⟶ ℂ \land A \subseteq S) \land B F_{S}^{'} y) \to S \subseteq ℂ$
7		cnex	$⊢ ℂ \in V$
8		ssexg	$⊢ (S \subseteq ℂ \land ℂ \in V) \to S \in V$
9	6 7 8	sylancl	$⊢ ((S \subseteq ℂ \land F : A ⟶ ℂ \land A \subseteq S) \land B F_{S}^{'} y) \to S \in V$
10		resttop	$⊢ (K \in Top \land S \in V) \to K ↾_{𝑡} S \in Top$
11	5 9 10	sylancr	$⊢ ((S \subseteq ℂ \land F : A ⟶ ℂ \land A \subseteq S) \land B F_{S}^{'} y) \to K ↾_{𝑡} S \in Top$
12		simpl3	$⊢ ((S \subseteq ℂ \land F : A ⟶ ℂ \land A \subseteq S) \land B F_{S}^{'} y) \to A \subseteq S$
13	2	cnfldtopon	$⊢ K \in TopOn (ℂ)$
14		resttopon	$⊢ (K \in TopOn (ℂ) \land S \subseteq ℂ) \to K ↾_{𝑡} S \in TopOn (S)$
15	13 6 14	sylancr	$⊢ ((S \subseteq ℂ \land F : A ⟶ ℂ \land A \subseteq S) \land B F_{S}^{'} y) \to K ↾_{𝑡} S \in TopOn (S)$
16		toponuni	$⊢ K ↾_{𝑡} S \in TopOn (S) \to S = ⋃ (K ↾_{𝑡} S)$
17	15 16	syl	$⊢ ((S \subseteq ℂ \land F : A ⟶ ℂ \land A \subseteq S) \land B F_{S}^{'} y) \to S = ⋃ (K ↾_{𝑡} S)$
18	12 17	sseqtrd	$⊢ ((S \subseteq ℂ \land F : A ⟶ ℂ \land A \subseteq S) \land B F_{S}^{'} y) \to A \subseteq ⋃ (K ↾_{𝑡} S)$
19		eqid	$⊢ ⋃ (K ↾_{𝑡} S) = ⋃ (K ↾_{𝑡} S)$
20	19	ntrss2	$⊢ (K ↾_{𝑡} S \in Top \land A \subseteq ⋃ (K ↾_{𝑡} S)) \to int (K ↾_{𝑡} S) (A) \subseteq A$
21	11 18 20	syl2anc	$⊢ ((S \subseteq ℂ \land F : A ⟶ ℂ \land A \subseteq S) \land B F_{S}^{'} y) \to int (K ↾_{𝑡} S) (A) \subseteq A$
22		eqid	$⊢ K ↾_{𝑡} S = K ↾_{𝑡} S$
23		eqid	$⊢ (z \in (A ∖ \{B\}) ⟼ \frac{F (z) - F (B)}{z - B}) = (z \in (A ∖ \{B\}) ⟼ \frac{F (z) - F (B)}{z - B})$
24		simp1	$⊢ (S \subseteq ℂ \land F : A ⟶ ℂ \land A \subseteq S) \to S \subseteq ℂ$
25		simp2	$⊢ (S \subseteq ℂ \land F : A ⟶ ℂ \land A \subseteq S) \to F : A ⟶ ℂ$
26		simp3	$⊢ (S \subseteq ℂ \land F : A ⟶ ℂ \land A \subseteq S) \to A \subseteq S$
27	22 2 23 24 25 26	eldv	$⊢ (S \subseteq ℂ \land F : A ⟶ ℂ \land A \subseteq S) \to (B F_{S}^{'} y \leftrightarrow (B \in int (K ↾_{𝑡} S) (A) \land y \in ((z \in (A ∖ \{B\}) ⟼ \frac{F (z) - F (B)}{z - B}) {lim}_{ℂ} B)))$
28	27	simprbda	$⊢ ((S \subseteq ℂ \land F : A ⟶ ℂ \land A \subseteq S) \land B F_{S}^{'} y) \to B \in int (K ↾_{𝑡} S) (A)$
29	21 28	sseldd	$⊢ ((S \subseteq ℂ \land F : A ⟶ ℂ \land A \subseteq S) \land B F_{S}^{'} y) \to B \in A$
30	3 29	ffvelcdmd	$⊢ ((S \subseteq ℂ \land F : A ⟶ ℂ \land A \subseteq S) \land B F_{S}^{'} y) \to F (B) \in ℂ$
31	30	adantr	$⊢ (((S \subseteq ℂ \land F : A ⟶ ℂ \land A \subseteq S) \land B F_{S}^{'} y) \land z \in A) \to F (B) \in ℂ$
32	4 31	subcld	$⊢ (((S \subseteq ℂ \land F : A ⟶ ℂ \land A \subseteq S) \land B F_{S}^{'} y) \land z \in A) \to F (z) - F (B) \in ℂ$
33		ssidd	$⊢ ((S \subseteq ℂ \land F : A ⟶ ℂ \land A \subseteq S) \land B F_{S}^{'} y) \to ℂ \subseteq ℂ$
34		txtopon	$⊢ (K \in TopOn (ℂ) \land K \in TopOn (ℂ)) \to K \times_{t} K \in TopOn (ℂ \times ℂ)$
35	13 13 34	mp2an	$⊢ K \times_{t} K \in TopOn (ℂ \times ℂ)$
36	35	toponrestid	$⊢ K \times_{t} K = (K \times_{t} K) ↾_{𝑡} (ℂ \times ℂ)$
37	12 6	sstrd	$⊢ ((S \subseteq ℂ \land F : A ⟶ ℂ \land A \subseteq S) \land B F_{S}^{'} y) \to A \subseteq ℂ$
38		eqid	$⊢ (x \in (A ∖ \{B\}) ⟼ \frac{F (x) - F (B)}{x - B}) = (x \in (A ∖ \{B\}) ⟼ \frac{F (x) - F (B)}{x - B})$
39	22 2 38 24 25 26	eldv	$⊢ (S \subseteq ℂ \land F : A ⟶ ℂ \land A \subseteq S) \to (B F_{S}^{'} y \leftrightarrow (B \in int (K ↾_{𝑡} S) (A) \land y \in ((x \in (A ∖ \{B\}) ⟼ \frac{F (x) - F (B)}{x - B}) {lim}_{ℂ} B)))$
40	39	simprbda	$⊢ ((S \subseteq ℂ \land F : A ⟶ ℂ \land A \subseteq S) \land B F_{S}^{'} y) \to B \in int (K ↾_{𝑡} S) (A)$
41	21 40	sseldd	$⊢ ((S \subseteq ℂ \land F : A ⟶ ℂ \land A \subseteq S) \land B F_{S}^{'} y) \to B \in A$
42	3 37 41	dvlem	$⊢ (((S \subseteq ℂ \land F : A ⟶ ℂ \land A \subseteq S) \land B F_{S}^{'} y) \land z \in (A ∖ \{B\})) \to \frac{F (z) - F (B)}{z - B} \in ℂ$
43	37	ssdifssd	$⊢ ((S \subseteq ℂ \land F : A ⟶ ℂ \land A \subseteq S) \land B F_{S}^{'} y) \to A ∖ \{B\} \subseteq ℂ$
44	43	sselda	$⊢ (((S \subseteq ℂ \land F : A ⟶ ℂ \land A \subseteq S) \land B F_{S}^{'} y) \land z \in (A ∖ \{B\})) \to z \in ℂ$
45	37 41	sseldd	$⊢ ((S \subseteq ℂ \land F : A ⟶ ℂ \land A \subseteq S) \land B F_{S}^{'} y) \to B \in ℂ$
46	45	adantr	$⊢ (((S \subseteq ℂ \land F : A ⟶ ℂ \land A \subseteq S) \land B F_{S}^{'} y) \land z \in (A ∖ \{B\})) \to B \in ℂ$
47	44 46	subcld	$⊢ (((S \subseteq ℂ \land F : A ⟶ ℂ \land A \subseteq S) \land B F_{S}^{'} y) \land z \in (A ∖ \{B\})) \to z - B \in ℂ$
48	27	simplbda	$⊢ ((S \subseteq ℂ \land F : A ⟶ ℂ \land A \subseteq S) \land B F_{S}^{'} y) \to y \in ((z \in (A ∖ \{B\}) ⟼ \frac{F (z) - F (B)}{z - B}) {lim}_{ℂ} B)$
49		limcresi	$⊢ (z \in A ⟼ z - B) {lim}_{ℂ} B \subseteq ({(z \in A ⟼ z - B) ↾}_{(A ∖ \{B\})}) {lim}_{ℂ} B$
50		difss	$⊢ A ∖ \{B\} \subseteq A$
51		resmpt	$⊢ A ∖ \{B\} \subseteq A \to {(z \in A ⟼ z - B) ↾}_{(A ∖ \{B\})} = (z \in (A ∖ \{B\}) ⟼ z - B)$
52	50 51	ax-mp	$⊢ {(z \in A ⟼ z - B) ↾}_{(A ∖ \{B\})} = (z \in (A ∖ \{B\}) ⟼ z - B)$
53	52	oveq1i	$⊢ ({(z \in A ⟼ z - B) ↾}_{(A ∖ \{B\})}) {lim}_{ℂ} B = (z \in (A ∖ \{B\}) ⟼ z - B) {lim}_{ℂ} B$
54	49 53	sseqtri	$⊢ (z \in A ⟼ z - B) {lim}_{ℂ} B \subseteq (z \in (A ∖ \{B\}) ⟼ z - B) {lim}_{ℂ} B$
55	45	subidd	$⊢ ((S \subseteq ℂ \land F : A ⟶ ℂ \land A \subseteq S) \land B F_{S}^{'} y) \to B - B = 0$
56		ssid	$⊢ ℂ \subseteq ℂ$
57		cncfmptid	$⊢ (A \subseteq ℂ \land ℂ \subseteq ℂ) \to (z \in A ⟼ z) : A \underset{cn}{⟶} ℂ$
58	37 56 57	sylancl	$⊢ ((S \subseteq ℂ \land F : A ⟶ ℂ \land A \subseteq S) \land B F_{S}^{'} y) \to (z \in A ⟼ z) : A \underset{cn}{⟶} ℂ$
59		cncfmptc	$⊢ (B \in ℂ \land A \subseteq ℂ \land ℂ \subseteq ℂ) \to (z \in A ⟼ B) : A \underset{cn}{⟶} ℂ$
60	45 37 33 59	syl3anc	$⊢ ((S \subseteq ℂ \land F : A ⟶ ℂ \land A \subseteq S) \land B F_{S}^{'} y) \to (z \in A ⟼ B) : A \underset{cn}{⟶} ℂ$
61	58 60	subcncf	$⊢ ((S \subseteq ℂ \land F : A ⟶ ℂ \land A \subseteq S) \land B F_{S}^{'} y) \to (z \in A ⟼ z - B) : A \underset{cn}{⟶} ℂ$
62		oveq1	$⊢ z = B \to z - B = B - B$
63	61 41 62	cnmptlimc	$⊢ ((S \subseteq ℂ \land F : A ⟶ ℂ \land A \subseteq S) \land B F_{S}^{'} y) \to B - B \in ((z \in A ⟼ z - B) {lim}_{ℂ} B)$
64	55 63	eqeltrrd	$⊢ ((S \subseteq ℂ \land F : A ⟶ ℂ \land A \subseteq S) \land B F_{S}^{'} y) \to 0 \in ((z \in A ⟼ z - B) {lim}_{ℂ} B)$
65	54 64	sselid	$⊢ ((S \subseteq ℂ \land F : A ⟶ ℂ \land A \subseteq S) \land B F_{S}^{'} y) \to 0 \in ((z \in (A ∖ \{B\}) ⟼ z - B) {lim}_{ℂ} B)$
66	2	mpomulcn	$⊢ (u \in ℂ, v \in ℂ ⟼ u v) \in ((K \times_{t} K) Cn K)$
67	24 25 26	dvcl	$⊢ ((S \subseteq ℂ \land F : A ⟶ ℂ \land A \subseteq S) \land B F_{S}^{'} y) \to y \in ℂ$
68		0cn	$⊢ 0 \in ℂ$
69		opelxpi	$⊢ (y \in ℂ \land 0 \in ℂ) \to ⟨y, 0⟩ \in (ℂ \times ℂ)$
70	67 68 69	sylancl	$⊢ ((S \subseteq ℂ \land F : A ⟶ ℂ \land A \subseteq S) \land B F_{S}^{'} y) \to ⟨y, 0⟩ \in (ℂ \times ℂ)$
71	35	toponunii	$⊢ ℂ \times ℂ = ⋃ (K \times_{t} K)$
72	71	cncnpi	$⊢ ((u \in ℂ, v \in ℂ ⟼ u v) \in ((K \times_{t} K) Cn K) \land ⟨y, 0⟩ \in (ℂ \times ℂ)) \to (u \in ℂ, v \in ℂ ⟼ u v) \in ((K \times_{t} K) CnP K) (⟨y, 0⟩)$
73	66 70 72	sylancr	$⊢ ((S \subseteq ℂ \land F : A ⟶ ℂ \land A \subseteq S) \land B F_{S}^{'} y) \to (u \in ℂ, v \in ℂ ⟼ u v) \in ((K \times_{t} K) CnP K) (⟨y, 0⟩)$
74	42 47 33 33 2 36 48 65 73	limccnp2	$⊢ ((S \subseteq ℂ \land F : A ⟶ ℂ \land A \subseteq S) \land B F_{S}^{'} y) \to y (u \in ℂ, v \in ℂ ⟼ u v) 0 \in ((z \in (A ∖ \{B\}) ⟼ (\frac{F (z) - F (B)}{z - B}) (u \in ℂ, v \in ℂ ⟼ u v) (z - B)) {lim}_{ℂ} B)$
75		df-mpt	$⊢ (z \in (A ∖ \{B\}) ⟼ (\frac{F (z) - F (B)}{z - B}) (u \in ℂ, v \in ℂ ⟼ u v) (z - B)) = \{⟨z, w⟩ \| (z \in (A ∖ \{B\}) \land w = (\frac{F (z) - F (B)}{z - B}) (u \in ℂ, v \in ℂ ⟼ u v) (z - B))\}$
76	75	oveq1i	$⊢ (z \in (A ∖ \{B\}) ⟼ (\frac{F (z) - F (B)}{z - B}) (u \in ℂ, v \in ℂ ⟼ u v) (z - B)) {lim}_{ℂ} B = \{⟨z, w⟩ \| (z \in (A ∖ \{B\}) \land w = (\frac{F (z) - F (B)}{z - B}) (u \in ℂ, v \in ℂ ⟼ u v) (z - B))\} {lim}_{ℂ} B$
77	74 76	eleqtrdi	$⊢ ((S \subseteq ℂ \land F : A ⟶ ℂ \land A \subseteq S) \land B F_{S}^{'} y) \to y (u \in ℂ, v \in ℂ ⟼ u v) 0 \in (\{⟨z, w⟩ \| (z \in (A ∖ \{B\}) \land w = (\frac{F (z) - F (B)}{z - B}) (u \in ℂ, v \in ℂ ⟼ u v) (z - B))\} {lim}_{ℂ} B)$
78		0cnd	$⊢ ((S \subseteq ℂ \land F : A ⟶ ℂ \land A \subseteq S) \land B F_{S}^{'} y) \to 0 \in ℂ$
79		ovmpot	$⊢ (y \in ℂ \land 0 \in ℂ) \to y (u \in ℂ, v \in ℂ ⟼ u v) 0 = y \cdot 0$
80	67 78 79	syl2anc	$⊢ ((S \subseteq ℂ \land F : A ⟶ ℂ \land A \subseteq S) \land B F_{S}^{'} y) \to y (u \in ℂ, v \in ℂ ⟼ u v) 0 = y \cdot 0$
81	3 37 29	dvlem	$⊢ (((S \subseteq ℂ \land F : A ⟶ ℂ \land A \subseteq S) \land B F_{S}^{'} y) \land z \in (A ∖ \{B\})) \to \frac{F (z) - F (B)}{z - B} \in ℂ$
82	37 29	sseldd	$⊢ ((S \subseteq ℂ \land F : A ⟶ ℂ \land A \subseteq S) \land B F_{S}^{'} y) \to B \in ℂ$
83	82	adantr	$⊢ (((S \subseteq ℂ \land F : A ⟶ ℂ \land A \subseteq S) \land B F_{S}^{'} y) \land z \in (A ∖ \{B\})) \to B \in ℂ$
84	44 83	subcld	$⊢ (((S \subseteq ℂ \land F : A ⟶ ℂ \land A \subseteq S) \land B F_{S}^{'} y) \land z \in (A ∖ \{B\})) \to z - B \in ℂ$
85		ovmpot	$⊢ (\frac{F (z) - F (B)}{z - B} \in ℂ \land z - B \in ℂ) \to (\frac{F (z) - F (B)}{z - B}) (u \in ℂ, v \in ℂ ⟼ u v) (z - B) = (\frac{F (z) - F (B)}{z - B}) (z - B)$
86	81 84 85	syl2anc	$⊢ (((S \subseteq ℂ \land F : A ⟶ ℂ \land A \subseteq S) \land B F_{S}^{'} y) \land z \in (A ∖ \{B\})) \to (\frac{F (z) - F (B)}{z - B}) (u \in ℂ, v \in ℂ ⟼ u v) (z - B) = (\frac{F (z) - F (B)}{z - B}) (z - B)$
87	86	eqeq2d	$⊢ (((S \subseteq ℂ \land F : A ⟶ ℂ \land A \subseteq S) \land B F_{S}^{'} y) \land z \in (A ∖ \{B\})) \to (w = (\frac{F (z) - F (B)}{z - B}) (u \in ℂ, v \in ℂ ⟼ u v) (z - B) \leftrightarrow w = (\frac{F (z) - F (B)}{z - B}) (z - B))$
88	87	pm5.32da	$⊢ ((S \subseteq ℂ \land F : A ⟶ ℂ \land A \subseteq S) \land B F_{S}^{'} y) \to ((z \in (A ∖ \{B\}) \land w = (\frac{F (z) - F (B)}{z - B}) (u \in ℂ, v \in ℂ ⟼ u v) (z - B)) \leftrightarrow (z \in (A ∖ \{B\}) \land w = (\frac{F (z) - F (B)}{z - B}) (z - B)))$
89	88	opabbidv	$⊢ ((S \subseteq ℂ \land F : A ⟶ ℂ \land A \subseteq S) \land B F_{S}^{'} y) \to \{⟨z, w⟩ \| (z \in (A ∖ \{B\}) \land w = (\frac{F (z) - F (B)}{z - B}) (u \in ℂ, v \in ℂ ⟼ u v) (z - B))\} = \{⟨z, w⟩ \| (z \in (A ∖ \{B\}) \land w = (\frac{F (z) - F (B)}{z - B}) (z - B))\}$
90		df-mpt	$⊢ (z \in (A ∖ \{B\}) ⟼ (\frac{F (z) - F (B)}{z - B}) (z - B)) = \{⟨z, w⟩ \| (z \in (A ∖ \{B\}) \land w = (\frac{F (z) - F (B)}{z - B}) (z - B))\}$
91	89 90	eqtr4di	$⊢ ((S \subseteq ℂ \land F : A ⟶ ℂ \land A \subseteq S) \land B F_{S}^{'} y) \to \{⟨z, w⟩ \| (z \in (A ∖ \{B\}) \land w = (\frac{F (z) - F (B)}{z - B}) (u \in ℂ, v \in ℂ ⟼ u v) (z - B))\} = (z \in (A ∖ \{B\}) ⟼ (\frac{F (z) - F (B)}{z - B}) (z - B))$
92	91	oveq1d	$⊢ ((S \subseteq ℂ \land F : A ⟶ ℂ \land A \subseteq S) \land B F_{S}^{'} y) \to \{⟨z, w⟩ \| (z \in (A ∖ \{B\}) \land w = (\frac{F (z) - F (B)}{z - B}) (u \in ℂ, v \in ℂ ⟼ u v) (z - B))\} {lim}_{ℂ} B = (z \in (A ∖ \{B\}) ⟼ (\frac{F (z) - F (B)}{z - B}) (z - B)) {lim}_{ℂ} B$
93	77 80 92	3eltr3d	$⊢ ((S \subseteq ℂ \land F : A ⟶ ℂ \land A \subseteq S) \land B F_{S}^{'} y) \to y \cdot 0 \in ((z \in (A ∖ \{B\}) ⟼ (\frac{F (z) - F (B)}{z - B}) (z - B)) {lim}_{ℂ} B)$
94	67	mul01d	$⊢ ((S \subseteq ℂ \land F : A ⟶ ℂ \land A \subseteq S) \land B F_{S}^{'} y) \to y \cdot 0 = 0$
95	3	adantr	$⊢ (((S \subseteq ℂ \land F : A ⟶ ℂ \land A \subseteq S) \land B F_{S}^{'} y) \land z \in (A ∖ \{B\})) \to F : A ⟶ ℂ$
96		simpr	$⊢ (((S \subseteq ℂ \land F : A ⟶ ℂ \land A \subseteq S) \land B F_{S}^{'} y) \land z \in (A ∖ \{B\})) \to z \in (A ∖ \{B\})$
97	50 96	sselid	$⊢ (((S \subseteq ℂ \land F : A ⟶ ℂ \land A \subseteq S) \land B F_{S}^{'} y) \land z \in (A ∖ \{B\})) \to z \in A$
98	95 97	ffvelcdmd	$⊢ (((S \subseteq ℂ \land F : A ⟶ ℂ \land A \subseteq S) \land B F_{S}^{'} y) \land z \in (A ∖ \{B\})) \to F (z) \in ℂ$
99	30	adantr	$⊢ (((S \subseteq ℂ \land F : A ⟶ ℂ \land A \subseteq S) \land B F_{S}^{'} y) \land z \in (A ∖ \{B\})) \to F (B) \in ℂ$
100	98 99	subcld	$⊢ (((S \subseteq ℂ \land F : A ⟶ ℂ \land A \subseteq S) \land B F_{S}^{'} y) \land z \in (A ∖ \{B\})) \to F (z) - F (B) \in ℂ$
101		eldifsni	$⊢ z \in (A ∖ \{B\}) \to z \neq B$
102	101	adantl	$⊢ (((S \subseteq ℂ \land F : A ⟶ ℂ \land A \subseteq S) \land B F_{S}^{'} y) \land z \in (A ∖ \{B\})) \to z \neq B$
103	44 83 102	subne0d	$⊢ (((S \subseteq ℂ \land F : A ⟶ ℂ \land A \subseteq S) \land B F_{S}^{'} y) \land z \in (A ∖ \{B\})) \to z - B \neq 0$
104	100 84 103	divcan1d	$⊢ (((S \subseteq ℂ \land F : A ⟶ ℂ \land A \subseteq S) \land B F_{S}^{'} y) \land z \in (A ∖ \{B\})) \to (\frac{F (z) - F (B)}{z - B}) (z - B) = F (z) - F (B)$
105	104	mpteq2dva	$⊢ ((S \subseteq ℂ \land F : A ⟶ ℂ \land A \subseteq S) \land B F_{S}^{'} y) \to (z \in (A ∖ \{B\}) ⟼ (\frac{F (z) - F (B)}{z - B}) (z - B)) = (z \in (A ∖ \{B\}) ⟼ F (z) - F (B))$
106	105	oveq1d	$⊢ ((S \subseteq ℂ \land F : A ⟶ ℂ \land A \subseteq S) \land B F_{S}^{'} y) \to (z \in (A ∖ \{B\}) ⟼ (\frac{F (z) - F (B)}{z - B}) (z - B)) {lim}_{ℂ} B = (z \in (A ∖ \{B\}) ⟼ F (z) - F (B)) {lim}_{ℂ} B$
107	93 94 106	3eltr3d	$⊢ ((S \subseteq ℂ \land F : A ⟶ ℂ \land A \subseteq S) \land B F_{S}^{'} y) \to 0 \in ((z \in (A ∖ \{B\}) ⟼ F (z) - F (B)) {lim}_{ℂ} B)$
108	32	fmpttd	$⊢ ((S \subseteq ℂ \land F : A ⟶ ℂ \land A \subseteq S) \land B F_{S}^{'} y) \to (z \in A ⟼ F (z) - F (B)) : A ⟶ ℂ$
109	108	limcdif	$⊢ ((S \subseteq ℂ \land F : A ⟶ ℂ \land A \subseteq S) \land B F_{S}^{'} y) \to (z \in A ⟼ F (z) - F (B)) {lim}_{ℂ} B = ({(z \in A ⟼ F (z) - F (B)) ↾}_{(A ∖ \{B\})}) {lim}_{ℂ} B$
110		resmpt	$⊢ A ∖ \{B\} \subseteq A \to {(z \in A ⟼ F (z) - F (B)) ↾}_{(A ∖ \{B\})} = (z \in (A ∖ \{B\}) ⟼ F (z) - F (B))$
111	50 110	ax-mp	$⊢ {(z \in A ⟼ F (z) - F (B)) ↾}_{(A ∖ \{B\})} = (z \in (A ∖ \{B\}) ⟼ F (z) - F (B))$
112	111	oveq1i	$⊢ ({(z \in A ⟼ F (z) - F (B)) ↾}_{(A ∖ \{B\})}) {lim}_{ℂ} B = (z \in (A ∖ \{B\}) ⟼ F (z) - F (B)) {lim}_{ℂ} B$
113	109 112	eqtrdi	$⊢ ((S \subseteq ℂ \land F : A ⟶ ℂ \land A \subseteq S) \land B F_{S}^{'} y) \to (z \in A ⟼ F (z) - F (B)) {lim}_{ℂ} B = (z \in (A ∖ \{B\}) ⟼ F (z) - F (B)) {lim}_{ℂ} B$
114	107 113	eleqtrrd	$⊢ ((S \subseteq ℂ \land F : A ⟶ ℂ \land A \subseteq S) \land B F_{S}^{'} y) \to 0 \in ((z \in A ⟼ F (z) - F (B)) {lim}_{ℂ} B)$
115		cncfmptc	$⊢ (F (B) \in ℂ \land A \subseteq ℂ \land ℂ \subseteq ℂ) \to (z \in A ⟼ F (B)) : A \underset{cn}{⟶} ℂ$
116	30 37 33 115	syl3anc	$⊢ ((S \subseteq ℂ \land F : A ⟶ ℂ \land A \subseteq S) \land B F_{S}^{'} y) \to (z \in A ⟼ F (B)) : A \underset{cn}{⟶} ℂ$
117		eqidd	$⊢ z = B \to F (B) = F (B)$
118	116 29 117	cnmptlimc	$⊢ ((S \subseteq ℂ \land F : A ⟶ ℂ \land A \subseteq S) \land B F_{S}^{'} y) \to F (B) \in ((z \in A ⟼ F (B)) {lim}_{ℂ} B)$
119	2	addcn	$⊢ + \in ((K \times_{t} K) Cn K)$
120		opelxpi	$⊢ (0 \in ℂ \land F (B) \in ℂ) \to ⟨0, F (B)⟩ \in (ℂ \times ℂ)$
121	68 30 120	sylancr	$⊢ ((S \subseteq ℂ \land F : A ⟶ ℂ \land A \subseteq S) \land B F_{S}^{'} y) \to ⟨0, F (B)⟩ \in (ℂ \times ℂ)$
122	71	cncnpi	$⊢ (+ \in ((K \times_{t} K) Cn K) \land ⟨0, F (B)⟩ \in (ℂ \times ℂ)) \to + \in ((K \times_{t} K) CnP K) (⟨0, F (B)⟩)$
123	119 121 122	sylancr	$⊢ ((S \subseteq ℂ \land F : A ⟶ ℂ \land A \subseteq S) \land B F_{S}^{'} y) \to + \in ((K \times_{t} K) CnP K) (⟨0, F (B)⟩)$
124	32 31 33 33 2 36 114 118 123	limccnp2	$⊢ ((S \subseteq ℂ \land F : A ⟶ ℂ \land A \subseteq S) \land B F_{S}^{'} y) \to 0 + F (B) \in ((z \in A ⟼ F (z) - F (B) + F (B)) {lim}_{ℂ} B)$
125	30	addlidd	$⊢ ((S \subseteq ℂ \land F : A ⟶ ℂ \land A \subseteq S) \land B F_{S}^{'} y) \to 0 + F (B) = F (B)$
126	4 31	npcand	$⊢ (((S \subseteq ℂ \land F : A ⟶ ℂ \land A \subseteq S) \land B F_{S}^{'} y) \land z \in A) \to F (z) - F (B) + F (B) = F (z)$
127	126	mpteq2dva	$⊢ ((S \subseteq ℂ \land F : A ⟶ ℂ \land A \subseteq S) \land B F_{S}^{'} y) \to (z \in A ⟼ F (z) - F (B) + F (B)) = (z \in A ⟼ F (z))$
128	3	feqmptd	$⊢ ((S \subseteq ℂ \land F : A ⟶ ℂ \land A \subseteq S) \land B F_{S}^{'} y) \to F = (z \in A ⟼ F (z))$
129	127 128	eqtr4d	$⊢ ((S \subseteq ℂ \land F : A ⟶ ℂ \land A \subseteq S) \land B F_{S}^{'} y) \to (z \in A ⟼ F (z) - F (B) + F (B)) = F$
130	129	oveq1d	$⊢ ((S \subseteq ℂ \land F : A ⟶ ℂ \land A \subseteq S) \land B F_{S}^{'} y) \to (z \in A ⟼ F (z) - F (B) + F (B)) {lim}_{ℂ} B = F {lim}_{ℂ} B$
131	124 125 130	3eltr3d	$⊢ ((S \subseteq ℂ \land F : A ⟶ ℂ \land A \subseteq S) \land B F_{S}^{'} y) \to F (B) \in (F {lim}_{ℂ} B)$
132	2 1	cnplimc	$⊢ (A \subseteq ℂ \land B \in A) \to (F \in (J CnP K) (B) \leftrightarrow (F : A ⟶ ℂ \land F (B) \in (F {lim}_{ℂ} B)))$
133	37 29 132	syl2anc	$⊢ ((S \subseteq ℂ \land F : A ⟶ ℂ \land A \subseteq S) \land B F_{S}^{'} y) \to (F \in (J CnP K) (B) \leftrightarrow (F : A ⟶ ℂ \land F (B) \in (F {lim}_{ℂ} B)))$
134	3 131 133	mpbir2and	$⊢ ((S \subseteq ℂ \land F : A ⟶ ℂ \land A \subseteq S) \land B F_{S}^{'} y) \to F \in (J CnP K) (B)$
135	134	ex	$⊢ (S \subseteq ℂ \land F : A ⟶ ℂ \land A \subseteq S) \to (B F_{S}^{'} y \to F \in (J CnP K) (B))$
136	135	exlimdv	$⊢ (S \subseteq ℂ \land F : A ⟶ ℂ \land A \subseteq S) \to (\exists y B F_{S}^{'} y \to F \in (J CnP K) (B))$
137		eldmg	$⊢ B \in dom F_{S}^{'} \to (B \in dom F_{S}^{'} \leftrightarrow \exists y B F_{S}^{'} y)$
138	137	ibi	$⊢ B \in dom F_{S}^{'} \to \exists y B F_{S}^{'} y$
139	136 138	impel	$⊢ ((S \subseteq ℂ \land F : A ⟶ ℂ \land A \subseteq S) \land B \in dom F_{S}^{'}) \to F \in (J CnP K) (B)$

Metamath Proof Explorer

Theorem dvcnp2

Proof