dvmulbr

Description: The product rule for derivatives at a point. For the (simpler but more limited) function version, see dvmul . (Contributed by Mario Carneiro, 9-Aug-2014) (Revised by Mario Carneiro, 28-Dec-2016) Avoid ax-mulf and remove unnecessary hypotheses. (Revised by GG, 16-Mar-2025)

	Ref	Expression
Hypotheses	dvadd.f	$⊢ φ \to F : X ⟶ ℂ$
	dvadd.x	$⊢ φ \to X \subseteq S$
	dvadd.g	$⊢ φ \to G : Y ⟶ ℂ$
	dvadd.y	$⊢ φ \to Y \subseteq S$
	dvaddbr.s	$⊢ φ \to S \subseteq ℂ$
	dvadd.bf	$⊢ φ \to C F_{S}^{'} K$
	dvadd.bg	$⊢ φ \to C G_{S}^{'} L$
	dvadd.j	$⊢ J = TopOpen (ℂ_{fld})$
Assertion	dvmulbr	$⊢ φ \to C {(F \times_{f} G)}_{S}^{'} (K G (C) + L F (C))$

Proof

Step	Hyp	Ref	Expression
1		dvadd.f	$⊢ φ \to F : X ⟶ ℂ$
2		dvadd.x	$⊢ φ \to X \subseteq S$
3		dvadd.g	$⊢ φ \to G : Y ⟶ ℂ$
4		dvadd.y	$⊢ φ \to Y \subseteq S$
5		dvaddbr.s	$⊢ φ \to S \subseteq ℂ$
6		dvadd.bf	$⊢ φ \to C F_{S}^{'} K$
7		dvadd.bg	$⊢ φ \to C G_{S}^{'} L$
8		dvadd.j	$⊢ J = TopOpen (ℂ_{fld})$
9		eqid	$⊢ J ↾_{𝑡} S = J ↾_{𝑡} S$
10		eqid	$⊢ (z \in (X ∖ \{C\}) ⟼ \frac{F (z) - F (C)}{z - C}) = (z \in (X ∖ \{C\}) ⟼ \frac{F (z) - F (C)}{z - C})$
11	9 8 10 5 1 2	eldv	$⊢ φ \to (C F_{S}^{'} K \leftrightarrow (C \in int (J ↾_{𝑡} S) (X) \land K \in ((z \in (X ∖ \{C\}) ⟼ \frac{F (z) - F (C)}{z - C}) {lim}_{ℂ} C)))$
12	6 11	mpbid	$⊢ φ \to (C \in int (J ↾_{𝑡} S) (X) \land K \in ((z \in (X ∖ \{C\}) ⟼ \frac{F (z) - F (C)}{z - C}) {lim}_{ℂ} C))$
13	12	simpld	$⊢ φ \to C \in int (J ↾_{𝑡} S) (X)$
14		eqid	$⊢ (z \in (Y ∖ \{C\}) ⟼ \frac{G (z) - G (C)}{z - C}) = (z \in (Y ∖ \{C\}) ⟼ \frac{G (z) - G (C)}{z - C})$
15	9 8 14 5 3 4	eldv	$⊢ φ \to (C G_{S}^{'} L \leftrightarrow (C \in int (J ↾_{𝑡} S) (Y) \land L \in ((z \in (Y ∖ \{C\}) ⟼ \frac{G (z) - G (C)}{z - C}) {lim}_{ℂ} C)))$
16	7 15	mpbid	$⊢ φ \to (C \in int (J ↾_{𝑡} S) (Y) \land L \in ((z \in (Y ∖ \{C\}) ⟼ \frac{G (z) - G (C)}{z - C}) {lim}_{ℂ} C))$
17	16	simpld	$⊢ φ \to C \in int (J ↾_{𝑡} S) (Y)$
18	13 17	elind	$⊢ φ \to C \in (int (J ↾_{𝑡} S) (X) \cap int (J ↾_{𝑡} S) (Y))$
19	8	cnfldtopon	$⊢ J \in TopOn (ℂ)$
20		resttopon	$⊢ (J \in TopOn (ℂ) \land S \subseteq ℂ) \to J ↾_{𝑡} S \in TopOn (S)$
21	19 5 20	sylancr	$⊢ φ \to J ↾_{𝑡} S \in TopOn (S)$
22		topontop	$⊢ J ↾_{𝑡} S \in TopOn (S) \to J ↾_{𝑡} S \in Top$
23	21 22	syl	$⊢ φ \to J ↾_{𝑡} S \in Top$
24		toponuni	$⊢ J ↾_{𝑡} S \in TopOn (S) \to S = ⋃ (J ↾_{𝑡} S)$
25	21 24	syl	$⊢ φ \to S = ⋃ (J ↾_{𝑡} S)$
26	2 25	sseqtrd	$⊢ φ \to X \subseteq ⋃ (J ↾_{𝑡} S)$
27	4 25	sseqtrd	$⊢ φ \to Y \subseteq ⋃ (J ↾_{𝑡} S)$
28		eqid	$⊢ ⋃ (J ↾_{𝑡} S) = ⋃ (J ↾_{𝑡} S)$
29	28	ntrin	$⊢ (J ↾_{𝑡} S \in Top \land X \subseteq ⋃ (J ↾_{𝑡} S) \land Y \subseteq ⋃ (J ↾_{𝑡} S)) \to int (J ↾_{𝑡} S) (X \cap Y) = int (J ↾_{𝑡} S) (X) \cap int (J ↾_{𝑡} S) (Y)$
30	23 26 27 29	syl3anc	$⊢ φ \to int (J ↾_{𝑡} S) (X \cap Y) = int (J ↾_{𝑡} S) (X) \cap int (J ↾_{𝑡} S) (Y)$
31	18 30	eleqtrrd	$⊢ φ \to C \in int (J ↾_{𝑡} S) (X \cap Y)$
32	1	adantr	$⊢ (φ \land z \in ((X \cap Y) ∖ \{C\})) \to F : X ⟶ ℂ$
33		inss1	$⊢ X \cap Y \subseteq X$
34		eldifi	$⊢ z \in ((X \cap Y) ∖ \{C\}) \to z \in (X \cap Y)$
35	34	adantl	$⊢ (φ \land z \in ((X \cap Y) ∖ \{C\})) \to z \in (X \cap Y)$
36	33 35	sselid	$⊢ (φ \land z \in ((X \cap Y) ∖ \{C\})) \to z \in X$
37	32 36	ffvelcdmd	$⊢ (φ \land z \in ((X \cap Y) ∖ \{C\})) \to F (z) \in ℂ$
38	5 1 2	dvbss	$⊢ φ \to dom F_{S}^{'} \subseteq X$
39		reldv	$⊢ Rel F_{S}^{'}$
40		releldm	$⊢ (Rel F_{S}^{'} \land C F_{S}^{'} K) \to C \in dom F_{S}^{'}$
41	39 6 40	sylancr	$⊢ φ \to C \in dom F_{S}^{'}$
42	38 41	sseldd	$⊢ φ \to C \in X$
43	1 42	ffvelcdmd	$⊢ φ \to F (C) \in ℂ$
44	43	adantr	$⊢ (φ \land z \in ((X \cap Y) ∖ \{C\})) \to F (C) \in ℂ$
45	37 44	subcld	$⊢ (φ \land z \in ((X \cap Y) ∖ \{C\})) \to F (z) - F (C) \in ℂ$
46	2 5	sstrd	$⊢ φ \to X \subseteq ℂ$
47	46	adantr	$⊢ (φ \land z \in ((X \cap Y) ∖ \{C\})) \to X \subseteq ℂ$
48	47 36	sseldd	$⊢ (φ \land z \in ((X \cap Y) ∖ \{C\})) \to z \in ℂ$
49	46 42	sseldd	$⊢ φ \to C \in ℂ$
50	49	adantr	$⊢ (φ \land z \in ((X \cap Y) ∖ \{C\})) \to C \in ℂ$
51	48 50	subcld	$⊢ (φ \land z \in ((X \cap Y) ∖ \{C\})) \to z - C \in ℂ$
52		eldifsni	$⊢ z \in ((X \cap Y) ∖ \{C\}) \to z \neq C$
53	52	adantl	$⊢ (φ \land z \in ((X \cap Y) ∖ \{C\})) \to z \neq C$
54	48 50 53	subne0d	$⊢ (φ \land z \in ((X \cap Y) ∖ \{C\})) \to z - C \neq 0$
55	45 51 54	divcld	$⊢ (φ \land z \in ((X \cap Y) ∖ \{C\})) \to \frac{F (z) - F (C)}{z - C} \in ℂ$
56	3	adantr	$⊢ (φ \land z \in ((X \cap Y) ∖ \{C\})) \to G : Y ⟶ ℂ$
57		inss2	$⊢ X \cap Y \subseteq Y$
58	57 35	sselid	$⊢ (φ \land z \in ((X \cap Y) ∖ \{C\})) \to z \in Y$
59	56 58	ffvelcdmd	$⊢ (φ \land z \in ((X \cap Y) ∖ \{C\})) \to G (z) \in ℂ$
60	55 59	mulcld	$⊢ (φ \land z \in ((X \cap Y) ∖ \{C\})) \to (\frac{F (z) - F (C)}{z - C}) G (z) \in ℂ$
61		ssdif	$⊢ X \cap Y \subseteq Y \to (X \cap Y) ∖ \{C\} \subseteq Y ∖ \{C\}$
62	57 61	mp1i	$⊢ φ \to (X \cap Y) ∖ \{C\} \subseteq Y ∖ \{C\}$
63	62	sselda	$⊢ (φ \land z \in ((X \cap Y) ∖ \{C\})) \to z \in (Y ∖ \{C\})$
64	4 5	sstrd	$⊢ φ \to Y \subseteq ℂ$
65	5 3 4	dvbss	$⊢ φ \to dom G_{S}^{'} \subseteq Y$
66		reldv	$⊢ Rel G_{S}^{'}$
67		releldm	$⊢ (Rel G_{S}^{'} \land C G_{S}^{'} L) \to C \in dom G_{S}^{'}$
68	66 7 67	sylancr	$⊢ φ \to C \in dom G_{S}^{'}$
69	65 68	sseldd	$⊢ φ \to C \in Y$
70	3 64 69	dvlem	$⊢ (φ \land z \in (Y ∖ \{C\})) \to \frac{G (z) - G (C)}{z - C} \in ℂ$
71	63 70	syldan	$⊢ (φ \land z \in ((X \cap Y) ∖ \{C\})) \to \frac{G (z) - G (C)}{z - C} \in ℂ$
72	71 44	mulcld	$⊢ (φ \land z \in ((X \cap Y) ∖ \{C\})) \to (\frac{G (z) - G (C)}{z - C}) F (C) \in ℂ$
73		ssidd	$⊢ φ \to ℂ \subseteq ℂ$
74		txtopon	$⊢ (J \in TopOn (ℂ) \land J \in TopOn (ℂ)) \to J \times_{t} J \in TopOn (ℂ \times ℂ)$
75	19 19 74	mp2an	$⊢ J \times_{t} J \in TopOn (ℂ \times ℂ)$
76	75	toponrestid	$⊢ J \times_{t} J = (J \times_{t} J) ↾_{𝑡} (ℂ \times ℂ)$
77	12	simprd	$⊢ φ \to K \in ((z \in (X ∖ \{C\}) ⟼ \frac{F (z) - F (C)}{z - C}) {lim}_{ℂ} C)$
78	1 46 42	dvlem	$⊢ (φ \land z \in (X ∖ \{C\})) \to \frac{F (z) - F (C)}{z - C} \in ℂ$
79	78	fmpttd	$⊢ φ \to (z \in (X ∖ \{C\}) ⟼ \frac{F (z) - F (C)}{z - C}) : X ∖ \{C\} ⟶ ℂ$
80		ssdif	$⊢ X \cap Y \subseteq X \to (X \cap Y) ∖ \{C\} \subseteq X ∖ \{C\}$
81	33 80	mp1i	$⊢ φ \to (X \cap Y) ∖ \{C\} \subseteq X ∖ \{C\}$
82	46	ssdifssd	$⊢ φ \to X ∖ \{C\} \subseteq ℂ$
83		eqid	$⊢ J ↾_{𝑡} ((X ∖ \{C\}) \cup \{C\}) = J ↾_{𝑡} ((X ∖ \{C\}) \cup \{C\})$
84	33 2	sstrid	$⊢ φ \to X \cap Y \subseteq S$
85	84 25	sseqtrd	$⊢ φ \to X \cap Y \subseteq ⋃ (J ↾_{𝑡} S)$
86		difssd	$⊢ φ \to ⋃ (J ↾_{𝑡} S) ∖ X \subseteq ⋃ (J ↾_{𝑡} S)$
87	85 86	unssd	$⊢ φ \to (X \cap Y) \cup (⋃ (J ↾_{𝑡} S) ∖ X) \subseteq ⋃ (J ↾_{𝑡} S)$
88		ssun1	$⊢ X \cap Y \subseteq (X \cap Y) \cup (⋃ (J ↾_{𝑡} S) ∖ X)$
89	88	a1i	$⊢ φ \to X \cap Y \subseteq (X \cap Y) \cup (⋃ (J ↾_{𝑡} S) ∖ X)$
90	28	ntrss	$⊢ (J ↾_{𝑡} S \in Top \land (X \cap Y) \cup (⋃ (J ↾_{𝑡} S) ∖ X) \subseteq ⋃ (J ↾_{𝑡} S) \land X \cap Y \subseteq (X \cap Y) \cup (⋃ (J ↾_{𝑡} S) ∖ X)) \to int (J ↾_{𝑡} S) (X \cap Y) \subseteq int (J ↾_{𝑡} S) ((X \cap Y) \cup (⋃ (J ↾_{𝑡} S) ∖ X))$
91	23 87 89 90	syl3anc	$⊢ φ \to int (J ↾_{𝑡} S) (X \cap Y) \subseteq int (J ↾_{𝑡} S) ((X \cap Y) \cup (⋃ (J ↾_{𝑡} S) ∖ X))$
92		eqid	$⊢ (x \in (X ∖ \{C\}) ⟼ \frac{F (x) - F (C)}{x - C}) = (x \in (X ∖ \{C\}) ⟼ \frac{F (x) - F (C)}{x - C})$
93	9 8 92 5 1 2	eldv	$⊢ φ \to (C F_{S}^{'} K \leftrightarrow (C \in int (J ↾_{𝑡} S) (X) \land K \in ((x \in (X ∖ \{C\}) ⟼ \frac{F (x) - F (C)}{x - C}) {lim}_{ℂ} C)))$
94	6 93	mpbid	$⊢ φ \to (C \in int (J ↾_{𝑡} S) (X) \land K \in ((x \in (X ∖ \{C\}) ⟼ \frac{F (x) - F (C)}{x - C}) {lim}_{ℂ} C))$
95	94	simpld	$⊢ φ \to C \in int (J ↾_{𝑡} S) (X)$
96		eqid	$⊢ (x \in (Y ∖ \{C\}) ⟼ \frac{G (x) - G (C)}{x - C}) = (x \in (Y ∖ \{C\}) ⟼ \frac{G (x) - G (C)}{x - C})$
97	9 8 96 5 3 4	eldv	$⊢ φ \to (C G_{S}^{'} L \leftrightarrow (C \in int (J ↾_{𝑡} S) (Y) \land L \in ((x \in (Y ∖ \{C\}) ⟼ \frac{G (x) - G (C)}{x - C}) {lim}_{ℂ} C)))$
98	7 97	mpbid	$⊢ φ \to (C \in int (J ↾_{𝑡} S) (Y) \land L \in ((x \in (Y ∖ \{C\}) ⟼ \frac{G (x) - G (C)}{x - C}) {lim}_{ℂ} C))$
99	98	simpld	$⊢ φ \to C \in int (J ↾_{𝑡} S) (Y)$
100	95 99	elind	$⊢ φ \to C \in (int (J ↾_{𝑡} S) (X) \cap int (J ↾_{𝑡} S) (Y))$
101	100 30	eleqtrrd	$⊢ φ \to C \in int (J ↾_{𝑡} S) (X \cap Y)$
102	91 101	sseldd	$⊢ φ \to C \in int (J ↾_{𝑡} S) ((X \cap Y) \cup (⋃ (J ↾_{𝑡} S) ∖ X))$
103	102 42	elind	$⊢ φ \to C \in (int (J ↾_{𝑡} S) ((X \cap Y) \cup (⋃ (J ↾_{𝑡} S) ∖ X)) \cap X)$
104	33	a1i	$⊢ φ \to X \cap Y \subseteq X$
105		eqid	$⊢ (J ↾_{𝑡} S) ↾_{𝑡} X = (J ↾_{𝑡} S) ↾_{𝑡} X$
106	28 105	restntr	$⊢ (J ↾_{𝑡} S \in Top \land X \subseteq ⋃ (J ↾_{𝑡} S) \land X \cap Y \subseteq X) \to int ((J ↾_{𝑡} S) ↾_{𝑡} X) (X \cap Y) = int (J ↾_{𝑡} S) ((X \cap Y) \cup (⋃ (J ↾_{𝑡} S) ∖ X)) \cap X$
107	23 26 104 106	syl3anc	$⊢ φ \to int ((J ↾_{𝑡} S) ↾_{𝑡} X) (X \cap Y) = int (J ↾_{𝑡} S) ((X \cap Y) \cup (⋃ (J ↾_{𝑡} S) ∖ X)) \cap X$
108	8	cnfldtop	$⊢ J \in Top$
109	108	a1i	$⊢ φ \to J \in Top$
110		cnex	$⊢ ℂ \in V$
111		ssexg	$⊢ (S \subseteq ℂ \land ℂ \in V) \to S \in V$
112	5 110 111	sylancl	$⊢ φ \to S \in V$
113		restabs	$⊢ (J \in Top \land X \subseteq S \land S \in V) \to (J ↾_{𝑡} S) ↾_{𝑡} X = J ↾_{𝑡} X$
114	109 2 112 113	syl3anc	$⊢ φ \to (J ↾_{𝑡} S) ↾_{𝑡} X = J ↾_{𝑡} X$
115	114	fveq2d	$⊢ φ \to int ((J ↾_{𝑡} S) ↾_{𝑡} X) = int (J ↾_{𝑡} X)$
116	115	fveq1d	$⊢ φ \to int ((J ↾_{𝑡} S) ↾_{𝑡} X) (X \cap Y) = int (J ↾_{𝑡} X) (X \cap Y)$
117	107 116	eqtr3d	$⊢ φ \to int (J ↾_{𝑡} S) ((X \cap Y) \cup (⋃ (J ↾_{𝑡} S) ∖ X)) \cap X = int (J ↾_{𝑡} X) (X \cap Y)$
118	103 117	eleqtrd	$⊢ φ \to C \in int (J ↾_{𝑡} X) (X \cap Y)$
119		undif1	$⊢ (X ∖ \{C\}) \cup \{C\} = X \cup \{C\}$
120	42	snssd	$⊢ φ \to \{C\} \subseteq X$
121		ssequn2	$⊢ \{C\} \subseteq X \leftrightarrow X \cup \{C\} = X$
122	120 121	sylib	$⊢ φ \to X \cup \{C\} = X$
123	119 122	eqtrid	$⊢ φ \to (X ∖ \{C\}) \cup \{C\} = X$
124	123	oveq2d	$⊢ φ \to J ↾_{𝑡} ((X ∖ \{C\}) \cup \{C\}) = J ↾_{𝑡} X$
125	124	fveq2d	$⊢ φ \to int (J ↾_{𝑡} ((X ∖ \{C\}) \cup \{C\})) = int (J ↾_{𝑡} X)$
126		undif1	$⊢ ((X \cap Y) ∖ \{C\}) \cup \{C\} = (X \cap Y) \cup \{C\}$
127	42 69	elind	$⊢ φ \to C \in (X \cap Y)$
128	127	snssd	$⊢ φ \to \{C\} \subseteq X \cap Y$
129		ssequn2	$⊢ \{C\} \subseteq X \cap Y \leftrightarrow (X \cap Y) \cup \{C\} = X \cap Y$
130	128 129	sylib	$⊢ φ \to (X \cap Y) \cup \{C\} = X \cap Y$
131	126 130	eqtrid	$⊢ φ \to ((X \cap Y) ∖ \{C\}) \cup \{C\} = X \cap Y$
132	125 131	fveq12d	$⊢ φ \to int (J ↾_{𝑡} ((X ∖ \{C\}) \cup \{C\})) (((X \cap Y) ∖ \{C\}) \cup \{C\}) = int (J ↾_{𝑡} X) (X \cap Y)$
133	118 132	eleqtrrd	$⊢ φ \to C \in int (J ↾_{𝑡} ((X ∖ \{C\}) \cup \{C\})) (((X \cap Y) ∖ \{C\}) \cup \{C\})$
134	79 81 82 8 83 133	limcres	$⊢ φ \to ({(z \in (X ∖ \{C\}) ⟼ \frac{F (z) - F (C)}{z - C}) ↾}_{((X \cap Y) ∖ \{C\})}) {lim}_{ℂ} C = (z \in (X ∖ \{C\}) ⟼ \frac{F (z) - F (C)}{z - C}) {lim}_{ℂ} C$
135	81	resmptd	$⊢ φ \to {(z \in (X ∖ \{C\}) ⟼ \frac{F (z) - F (C)}{z - C}) ↾}_{((X \cap Y) ∖ \{C\})} = (z \in ((X \cap Y) ∖ \{C\}) ⟼ \frac{F (z) - F (C)}{z - C})$
136	135	oveq1d	$⊢ φ \to ({(z \in (X ∖ \{C\}) ⟼ \frac{F (z) - F (C)}{z - C}) ↾}_{((X \cap Y) ∖ \{C\})}) {lim}_{ℂ} C = (z \in ((X \cap Y) ∖ \{C\}) ⟼ \frac{F (z) - F (C)}{z - C}) {lim}_{ℂ} C$
137	134 136	eqtr3d	$⊢ φ \to (z \in (X ∖ \{C\}) ⟼ \frac{F (z) - F (C)}{z - C}) {lim}_{ℂ} C = (z \in ((X \cap Y) ∖ \{C\}) ⟼ \frac{F (z) - F (C)}{z - C}) {lim}_{ℂ} C$
138	77 137	eleqtrd	$⊢ φ \to K \in ((z \in ((X \cap Y) ∖ \{C\}) ⟼ \frac{F (z) - F (C)}{z - C}) {lim}_{ℂ} C)$
139		eqid	$⊢ J ↾_{𝑡} Y = J ↾_{𝑡} Y$
140	139 8	dvcnp2	$⊢ ((S \subseteq ℂ \land G : Y ⟶ ℂ \land Y \subseteq S) \land C \in dom G_{S}^{'}) \to G \in ((J ↾_{𝑡} Y) CnP J) (C)$
141	5 3 4 68 140	syl31anc	$⊢ φ \to G \in ((J ↾_{𝑡} Y) CnP J) (C)$
142	8 139	cnplimc	$⊢ (Y \subseteq ℂ \land C \in Y) \to (G \in ((J ↾_{𝑡} Y) CnP J) (C) \leftrightarrow (G : Y ⟶ ℂ \land G (C) \in (G {lim}_{ℂ} C)))$
143	64 69 142	syl2anc	$⊢ φ \to (G \in ((J ↾_{𝑡} Y) CnP J) (C) \leftrightarrow (G : Y ⟶ ℂ \land G (C) \in (G {lim}_{ℂ} C)))$
144	141 143	mpbid	$⊢ φ \to (G : Y ⟶ ℂ \land G (C) \in (G {lim}_{ℂ} C))$
145	144	simprd	$⊢ φ \to G (C) \in (G {lim}_{ℂ} C)$
146		difss	$⊢ (X \cap Y) ∖ \{C\} \subseteq X \cap Y$
147	146 57	sstri	$⊢ (X \cap Y) ∖ \{C\} \subseteq Y$
148	147	a1i	$⊢ φ \to (X \cap Y) ∖ \{C\} \subseteq Y$
149		eqid	$⊢ J ↾_{𝑡} (Y \cup \{C\}) = J ↾_{𝑡} (Y \cup \{C\})$
150		difssd	$⊢ φ \to ⋃ (J ↾_{𝑡} S) ∖ Y \subseteq ⋃ (J ↾_{𝑡} S)$
151	85 150	unssd	$⊢ φ \to (X \cap Y) \cup (⋃ (J ↾_{𝑡} S) ∖ Y) \subseteq ⋃ (J ↾_{𝑡} S)$
152		ssun1	$⊢ X \cap Y \subseteq (X \cap Y) \cup (⋃ (J ↾_{𝑡} S) ∖ Y)$
153	152	a1i	$⊢ φ \to X \cap Y \subseteq (X \cap Y) \cup (⋃ (J ↾_{𝑡} S) ∖ Y)$
154	28	ntrss	$⊢ (J ↾_{𝑡} S \in Top \land (X \cap Y) \cup (⋃ (J ↾_{𝑡} S) ∖ Y) \subseteq ⋃ (J ↾_{𝑡} S) \land X \cap Y \subseteq (X \cap Y) \cup (⋃ (J ↾_{𝑡} S) ∖ Y)) \to int (J ↾_{𝑡} S) (X \cap Y) \subseteq int (J ↾_{𝑡} S) ((X \cap Y) \cup (⋃ (J ↾_{𝑡} S) ∖ Y))$
155	23 151 153 154	syl3anc	$⊢ φ \to int (J ↾_{𝑡} S) (X \cap Y) \subseteq int (J ↾_{𝑡} S) ((X \cap Y) \cup (⋃ (J ↾_{𝑡} S) ∖ Y))$
156	155 101	sseldd	$⊢ φ \to C \in int (J ↾_{𝑡} S) ((X \cap Y) \cup (⋃ (J ↾_{𝑡} S) ∖ Y))$
157	156 69	elind	$⊢ φ \to C \in (int (J ↾_{𝑡} S) ((X \cap Y) \cup (⋃ (J ↾_{𝑡} S) ∖ Y)) \cap Y)$
158	57	a1i	$⊢ φ \to X \cap Y \subseteq Y$
159		eqid	$⊢ (J ↾_{𝑡} S) ↾_{𝑡} Y = (J ↾_{𝑡} S) ↾_{𝑡} Y$
160	28 159	restntr	$⊢ (J ↾_{𝑡} S \in Top \land Y \subseteq ⋃ (J ↾_{𝑡} S) \land X \cap Y \subseteq Y) \to int ((J ↾_{𝑡} S) ↾_{𝑡} Y) (X \cap Y) = int (J ↾_{𝑡} S) ((X \cap Y) \cup (⋃ (J ↾_{𝑡} S) ∖ Y)) \cap Y$
161	23 27 158 160	syl3anc	$⊢ φ \to int ((J ↾_{𝑡} S) ↾_{𝑡} Y) (X \cap Y) = int (J ↾_{𝑡} S) ((X \cap Y) \cup (⋃ (J ↾_{𝑡} S) ∖ Y)) \cap Y$
162		restabs	$⊢ (J \in Top \land Y \subseteq S \land S \in V) \to (J ↾_{𝑡} S) ↾_{𝑡} Y = J ↾_{𝑡} Y$
163	109 4 112 162	syl3anc	$⊢ φ \to (J ↾_{𝑡} S) ↾_{𝑡} Y = J ↾_{𝑡} Y$
164	163	fveq2d	$⊢ φ \to int ((J ↾_{𝑡} S) ↾_{𝑡} Y) = int (J ↾_{𝑡} Y)$
165	164	fveq1d	$⊢ φ \to int ((J ↾_{𝑡} S) ↾_{𝑡} Y) (X \cap Y) = int (J ↾_{𝑡} Y) (X \cap Y)$
166	161 165	eqtr3d	$⊢ φ \to int (J ↾_{𝑡} S) ((X \cap Y) \cup (⋃ (J ↾_{𝑡} S) ∖ Y)) \cap Y = int (J ↾_{𝑡} Y) (X \cap Y)$
167	157 166	eleqtrd	$⊢ φ \to C \in int (J ↾_{𝑡} Y) (X \cap Y)$
168	69	snssd	$⊢ φ \to \{C\} \subseteq Y$
169		ssequn2	$⊢ \{C\} \subseteq Y \leftrightarrow Y \cup \{C\} = Y$
170	168 169	sylib	$⊢ φ \to Y \cup \{C\} = Y$
171	170	oveq2d	$⊢ φ \to J ↾_{𝑡} (Y \cup \{C\}) = J ↾_{𝑡} Y$
172	171	fveq2d	$⊢ φ \to int (J ↾_{𝑡} (Y \cup \{C\})) = int (J ↾_{𝑡} Y)$
173	172 131	fveq12d	$⊢ φ \to int (J ↾_{𝑡} (Y \cup \{C\})) (((X \cap Y) ∖ \{C\}) \cup \{C\}) = int (J ↾_{𝑡} Y) (X \cap Y)$
174	167 173	eleqtrrd	$⊢ φ \to C \in int (J ↾_{𝑡} (Y \cup \{C\})) (((X \cap Y) ∖ \{C\}) \cup \{C\})$
175	3 148 64 8 149 174	limcres	$⊢ φ \to ({G ↾}_{((X \cap Y) ∖ \{C\})}) {lim}_{ℂ} C = G {lim}_{ℂ} C$
176	3 148	feqresmpt	$⊢ φ \to {G ↾}_{((X \cap Y) ∖ \{C\})} = (z \in ((X \cap Y) ∖ \{C\}) ⟼ G (z))$
177	176	oveq1d	$⊢ φ \to ({G ↾}_{((X \cap Y) ∖ \{C\})}) {lim}_{ℂ} C = (z \in ((X \cap Y) ∖ \{C\}) ⟼ G (z)) {lim}_{ℂ} C$
178	175 177	eqtr3d	$⊢ φ \to G {lim}_{ℂ} C = (z \in ((X \cap Y) ∖ \{C\}) ⟼ G (z)) {lim}_{ℂ} C$
179	145 178	eleqtrd	$⊢ φ \to G (C) \in ((z \in ((X \cap Y) ∖ \{C\}) ⟼ G (z)) {lim}_{ℂ} C)$
180	8	mpomulcn	$⊢ (u \in ℂ, v \in ℂ ⟼ u v) \in ((J \times_{t} J) Cn J)$
181	5 1 2	dvcl	$⊢ (φ \land C F_{S}^{'} K) \to K \in ℂ$
182	6 181	mpdan	$⊢ φ \to K \in ℂ$
183	3 69	ffvelcdmd	$⊢ φ \to G (C) \in ℂ$
184	182 183	opelxpd	$⊢ φ \to ⟨K, G (C)⟩ \in (ℂ \times ℂ)$
185	75	toponunii	$⊢ ℂ \times ℂ = ⋃ (J \times_{t} J)$
186	185	cncnpi	$⊢ ((u \in ℂ, v \in ℂ ⟼ u v) \in ((J \times_{t} J) Cn J) \land ⟨K, G (C)⟩ \in (ℂ \times ℂ)) \to (u \in ℂ, v \in ℂ ⟼ u v) \in ((J \times_{t} J) CnP J) (⟨K, G (C)⟩)$
187	180 184 186	sylancr	$⊢ φ \to (u \in ℂ, v \in ℂ ⟼ u v) \in ((J \times_{t} J) CnP J) (⟨K, G (C)⟩)$
188	55 59 73 73 8 76 138 179 187	limccnp2	$⊢ φ \to K (u \in ℂ, v \in ℂ ⟼ u v) G (C) \in ((z \in ((X \cap Y) ∖ \{C\}) ⟼ (\frac{F (z) - F (C)}{z - C}) (u \in ℂ, v \in ℂ ⟼ u v) G (z)) {lim}_{ℂ} C)$
189		df-mpt	$⊢ (z \in ((X \cap Y) ∖ \{C\}) ⟼ (\frac{F (z) - F (C)}{z - C}) (u \in ℂ, v \in ℂ ⟼ u v) G (z)) = \{⟨z, w⟩ \| (z \in ((X \cap Y) ∖ \{C\}) \land w = (\frac{F (z) - F (C)}{z - C}) (u \in ℂ, v \in ℂ ⟼ u v) G (z))\}$
190	189	oveq1i	$⊢ (z \in ((X \cap Y) ∖ \{C\}) ⟼ (\frac{F (z) - F (C)}{z - C}) (u \in ℂ, v \in ℂ ⟼ u v) G (z)) {lim}_{ℂ} C = \{⟨z, w⟩ \| (z \in ((X \cap Y) ∖ \{C\}) \land w = (\frac{F (z) - F (C)}{z - C}) (u \in ℂ, v \in ℂ ⟼ u v) G (z))\} {lim}_{ℂ} C$
191	188 190	eleqtrdi	$⊢ φ \to K (u \in ℂ, v \in ℂ ⟼ u v) G (C) \in (\{⟨z, w⟩ \| (z \in ((X \cap Y) ∖ \{C\}) \land w = (\frac{F (z) - F (C)}{z - C}) (u \in ℂ, v \in ℂ ⟼ u v) G (z))\} {lim}_{ℂ} C)$
192		ovmul	$⊢ (K \in ℂ \land G (C) \in ℂ) \to K (u \in ℂ, v \in ℂ ⟼ u v) G (C) = K G (C)$
193	182 183 192	syl2anc	$⊢ φ \to K (u \in ℂ, v \in ℂ ⟼ u v) G (C) = K G (C)$
194		ovmul	$⊢ (\frac{F (z) - F (C)}{z - C} \in ℂ \land G (z) \in ℂ) \to (\frac{F (z) - F (C)}{z - C}) (u \in ℂ, v \in ℂ ⟼ u v) G (z) = (\frac{F (z) - F (C)}{z - C}) G (z)$
195	55 59 194	syl2anc	$⊢ (φ \land z \in ((X \cap Y) ∖ \{C\})) \to (\frac{F (z) - F (C)}{z - C}) (u \in ℂ, v \in ℂ ⟼ u v) G (z) = (\frac{F (z) - F (C)}{z - C}) G (z)$
196	195	eqeq2d	$⊢ (φ \land z \in ((X \cap Y) ∖ \{C\})) \to (w = (\frac{F (z) - F (C)}{z - C}) (u \in ℂ, v \in ℂ ⟼ u v) G (z) \leftrightarrow w = (\frac{F (z) - F (C)}{z - C}) G (z))$
197	196	pm5.32da	$⊢ φ \to ((z \in ((X \cap Y) ∖ \{C\}) \land w = (\frac{F (z) - F (C)}{z - C}) (u \in ℂ, v \in ℂ ⟼ u v) G (z)) \leftrightarrow (z \in ((X \cap Y) ∖ \{C\}) \land w = (\frac{F (z) - F (C)}{z - C}) G (z)))$
198	197	opabbidv	$⊢ φ \to \{⟨z, w⟩ \| (z \in ((X \cap Y) ∖ \{C\}) \land w = (\frac{F (z) - F (C)}{z - C}) (u \in ℂ, v \in ℂ ⟼ u v) G (z))\} = \{⟨z, w⟩ \| (z \in ((X \cap Y) ∖ \{C\}) \land w = (\frac{F (z) - F (C)}{z - C}) G (z))\}$
199		df-mpt	$⊢ (z \in ((X \cap Y) ∖ \{C\}) ⟼ (\frac{F (z) - F (C)}{z - C}) G (z)) = \{⟨z, w⟩ \| (z \in ((X \cap Y) ∖ \{C\}) \land w = (\frac{F (z) - F (C)}{z - C}) G (z))\}$
200	198 199	eqtr4di	$⊢ φ \to \{⟨z, w⟩ \| (z \in ((X \cap Y) ∖ \{C\}) \land w = (\frac{F (z) - F (C)}{z - C}) (u \in ℂ, v \in ℂ ⟼ u v) G (z))\} = (z \in ((X \cap Y) ∖ \{C\}) ⟼ (\frac{F (z) - F (C)}{z - C}) G (z))$
201	200	oveq1d	$⊢ φ \to \{⟨z, w⟩ \| (z \in ((X \cap Y) ∖ \{C\}) \land w = (\frac{F (z) - F (C)}{z - C}) (u \in ℂ, v \in ℂ ⟼ u v) G (z))\} {lim}_{ℂ} C = (z \in ((X \cap Y) ∖ \{C\}) ⟼ (\frac{F (z) - F (C)}{z - C}) G (z)) {lim}_{ℂ} C$
202	191 193 201	3eltr3d	$⊢ φ \to K G (C) \in ((z \in ((X \cap Y) ∖ \{C\}) ⟼ (\frac{F (z) - F (C)}{z - C}) G (z)) {lim}_{ℂ} C)$
203	16	simprd	$⊢ φ \to L \in ((z \in (Y ∖ \{C\}) ⟼ \frac{G (z) - G (C)}{z - C}) {lim}_{ℂ} C)$
204	70	fmpttd	$⊢ φ \to (z \in (Y ∖ \{C\}) ⟼ \frac{G (z) - G (C)}{z - C}) : Y ∖ \{C\} ⟶ ℂ$
205	64	ssdifssd	$⊢ φ \to Y ∖ \{C\} \subseteq ℂ$
206		eqid	$⊢ J ↾_{𝑡} ((Y ∖ \{C\}) \cup \{C\}) = J ↾_{𝑡} ((Y ∖ \{C\}) \cup \{C\})$
207		undif1	$⊢ (Y ∖ \{C\}) \cup \{C\} = Y \cup \{C\}$
208	207 170	eqtrid	$⊢ φ \to (Y ∖ \{C\}) \cup \{C\} = Y$
209	208	oveq2d	$⊢ φ \to J ↾_{𝑡} ((Y ∖ \{C\}) \cup \{C\}) = J ↾_{𝑡} Y$
210	209	fveq2d	$⊢ φ \to int (J ↾_{𝑡} ((Y ∖ \{C\}) \cup \{C\})) = int (J ↾_{𝑡} Y)$
211	210 131	fveq12d	$⊢ φ \to int (J ↾_{𝑡} ((Y ∖ \{C\}) \cup \{C\})) (((X \cap Y) ∖ \{C\}) \cup \{C\}) = int (J ↾_{𝑡} Y) (X \cap Y)$
212	167 211	eleqtrrd	$⊢ φ \to C \in int (J ↾_{𝑡} ((Y ∖ \{C\}) \cup \{C\})) (((X \cap Y) ∖ \{C\}) \cup \{C\})$
213	204 62 205 8 206 212	limcres	$⊢ φ \to ({(z \in (Y ∖ \{C\}) ⟼ \frac{G (z) - G (C)}{z - C}) ↾}_{((X \cap Y) ∖ \{C\})}) {lim}_{ℂ} C = (z \in (Y ∖ \{C\}) ⟼ \frac{G (z) - G (C)}{z - C}) {lim}_{ℂ} C$
214	62	resmptd	$⊢ φ \to {(z \in (Y ∖ \{C\}) ⟼ \frac{G (z) - G (C)}{z - C}) ↾}_{((X \cap Y) ∖ \{C\})} = (z \in ((X \cap Y) ∖ \{C\}) ⟼ \frac{G (z) - G (C)}{z - C})$
215	214	oveq1d	$⊢ φ \to ({(z \in (Y ∖ \{C\}) ⟼ \frac{G (z) - G (C)}{z - C}) ↾}_{((X \cap Y) ∖ \{C\})}) {lim}_{ℂ} C = (z \in ((X \cap Y) ∖ \{C\}) ⟼ \frac{G (z) - G (C)}{z - C}) {lim}_{ℂ} C$
216	213 215	eqtr3d	$⊢ φ \to (z \in (Y ∖ \{C\}) ⟼ \frac{G (z) - G (C)}{z - C}) {lim}_{ℂ} C = (z \in ((X \cap Y) ∖ \{C\}) ⟼ \frac{G (z) - G (C)}{z - C}) {lim}_{ℂ} C$
217	203 216	eleqtrd	$⊢ φ \to L \in ((z \in ((X \cap Y) ∖ \{C\}) ⟼ \frac{G (z) - G (C)}{z - C}) {lim}_{ℂ} C)$
218	84 5	sstrd	$⊢ φ \to X \cap Y \subseteq ℂ$
219		cncfmptc	$⊢ (F (C) \in ℂ \land X \cap Y \subseteq ℂ \land ℂ \subseteq ℂ) \to (z \in (X \cap Y) ⟼ F (C)) : (X \cap Y) \underset{cn}{⟶} ℂ$
220	43 218 73 219	syl3anc	$⊢ φ \to (z \in (X \cap Y) ⟼ F (C)) : (X \cap Y) \underset{cn}{⟶} ℂ$
221		eqidd	$⊢ z = C \to F (C) = F (C)$
222	220 127 221	cnmptlimc	$⊢ φ \to F (C) \in ((z \in (X \cap Y) ⟼ F (C)) {lim}_{ℂ} C)$
223	43	adantr	$⊢ (φ \land z \in (X \cap Y)) \to F (C) \in ℂ$
224	223	fmpttd	$⊢ φ \to (z \in (X \cap Y) ⟼ F (C)) : X \cap Y ⟶ ℂ$
225	224	limcdif	$⊢ φ \to (z \in (X \cap Y) ⟼ F (C)) {lim}_{ℂ} C = ({(z \in (X \cap Y) ⟼ F (C)) ↾}_{((X \cap Y) ∖ \{C\})}) {lim}_{ℂ} C$
226		resmpt	$⊢ (X \cap Y) ∖ \{C\} \subseteq X \cap Y \to {(z \in (X \cap Y) ⟼ F (C)) ↾}_{((X \cap Y) ∖ \{C\})} = (z \in ((X \cap Y) ∖ \{C\}) ⟼ F (C))$
227	146 226	mp1i	$⊢ φ \to {(z \in (X \cap Y) ⟼ F (C)) ↾}_{((X \cap Y) ∖ \{C\})} = (z \in ((X \cap Y) ∖ \{C\}) ⟼ F (C))$
228	227	oveq1d	$⊢ φ \to ({(z \in (X \cap Y) ⟼ F (C)) ↾}_{((X \cap Y) ∖ \{C\})}) {lim}_{ℂ} C = (z \in ((X \cap Y) ∖ \{C\}) ⟼ F (C)) {lim}_{ℂ} C$
229	225 228	eqtrd	$⊢ φ \to (z \in (X \cap Y) ⟼ F (C)) {lim}_{ℂ} C = (z \in ((X \cap Y) ∖ \{C\}) ⟼ F (C)) {lim}_{ℂ} C$
230	222 229	eleqtrd	$⊢ φ \to F (C) \in ((z \in ((X \cap Y) ∖ \{C\}) ⟼ F (C)) {lim}_{ℂ} C)$
231	5 3 4	dvcl	$⊢ (φ \land C G_{S}^{'} L) \to L \in ℂ$
232	7 231	mpdan	$⊢ φ \to L \in ℂ$
233	232 43	opelxpd	$⊢ φ \to ⟨L, F (C)⟩ \in (ℂ \times ℂ)$
234	185	cncnpi	$⊢ ((u \in ℂ, v \in ℂ ⟼ u v) \in ((J \times_{t} J) Cn J) \land ⟨L, F (C)⟩ \in (ℂ \times ℂ)) \to (u \in ℂ, v \in ℂ ⟼ u v) \in ((J \times_{t} J) CnP J) (⟨L, F (C)⟩)$
235	180 233 234	sylancr	$⊢ φ \to (u \in ℂ, v \in ℂ ⟼ u v) \in ((J \times_{t} J) CnP J) (⟨L, F (C)⟩)$
236	71 44 73 73 8 76 217 230 235	limccnp2	$⊢ φ \to L (u \in ℂ, v \in ℂ ⟼ u v) F (C) \in ((z \in ((X \cap Y) ∖ \{C\}) ⟼ (\frac{G (z) - G (C)}{z - C}) (u \in ℂ, v \in ℂ ⟼ u v) F (C)) {lim}_{ℂ} C)$
237		df-mpt	$⊢ (z \in ((X \cap Y) ∖ \{C\}) ⟼ (\frac{G (z) - G (C)}{z - C}) (u \in ℂ, v \in ℂ ⟼ u v) F (C)) = \{⟨z, w⟩ \| (z \in ((X \cap Y) ∖ \{C\}) \land w = (\frac{G (z) - G (C)}{z - C}) (u \in ℂ, v \in ℂ ⟼ u v) F (C))\}$
238	237	oveq1i	$⊢ (z \in ((X \cap Y) ∖ \{C\}) ⟼ (\frac{G (z) - G (C)}{z - C}) (u \in ℂ, v \in ℂ ⟼ u v) F (C)) {lim}_{ℂ} C = \{⟨z, w⟩ \| (z \in ((X \cap Y) ∖ \{C\}) \land w = (\frac{G (z) - G (C)}{z - C}) (u \in ℂ, v \in ℂ ⟼ u v) F (C))\} {lim}_{ℂ} C$
239	236 238	eleqtrdi	$⊢ φ \to L (u \in ℂ, v \in ℂ ⟼ u v) F (C) \in (\{⟨z, w⟩ \| (z \in ((X \cap Y) ∖ \{C\}) \land w = (\frac{G (z) - G (C)}{z - C}) (u \in ℂ, v \in ℂ ⟼ u v) F (C))\} {lim}_{ℂ} C)$
240		ovmul	$⊢ (L \in ℂ \land F (C) \in ℂ) \to L (u \in ℂ, v \in ℂ ⟼ u v) F (C) = L F (C)$
241	232 43 240	syl2anc	$⊢ φ \to L (u \in ℂ, v \in ℂ ⟼ u v) F (C) = L F (C)$
242	42	adantr	$⊢ (φ \land z \in ((X \cap Y) ∖ \{C\})) \to C \in X$
243	32 242	ffvelcdmd	$⊢ (φ \land z \in ((X \cap Y) ∖ \{C\})) \to F (C) \in ℂ$
244		ovmul	$⊢ (\frac{G (z) - G (C)}{z - C} \in ℂ \land F (C) \in ℂ) \to (\frac{G (z) - G (C)}{z - C}) (u \in ℂ, v \in ℂ ⟼ u v) F (C) = (\frac{G (z) - G (C)}{z - C}) F (C)$
245	71 243 244	syl2anc	$⊢ (φ \land z \in ((X \cap Y) ∖ \{C\})) \to (\frac{G (z) - G (C)}{z - C}) (u \in ℂ, v \in ℂ ⟼ u v) F (C) = (\frac{G (z) - G (C)}{z - C}) F (C)$
246	245	eqeq2d	$⊢ (φ \land z \in ((X \cap Y) ∖ \{C\})) \to (w = (\frac{G (z) - G (C)}{z - C}) (u \in ℂ, v \in ℂ ⟼ u v) F (C) \leftrightarrow w = (\frac{G (z) - G (C)}{z - C}) F (C))$
247	246	pm5.32da	$⊢ φ \to ((z \in ((X \cap Y) ∖ \{C\}) \land w = (\frac{G (z) - G (C)}{z - C}) (u \in ℂ, v \in ℂ ⟼ u v) F (C)) \leftrightarrow (z \in ((X \cap Y) ∖ \{C\}) \land w = (\frac{G (z) - G (C)}{z - C}) F (C)))$
248	247	opabbidv	$⊢ φ \to \{⟨z, w⟩ \| (z \in ((X \cap Y) ∖ \{C\}) \land w = (\frac{G (z) - G (C)}{z - C}) (u \in ℂ, v \in ℂ ⟼ u v) F (C))\} = \{⟨z, w⟩ \| (z \in ((X \cap Y) ∖ \{C\}) \land w = (\frac{G (z) - G (C)}{z - C}) F (C))\}$
249		df-mpt	$⊢ (z \in ((X \cap Y) ∖ \{C\}) ⟼ (\frac{G (z) - G (C)}{z - C}) F (C)) = \{⟨z, w⟩ \| (z \in ((X \cap Y) ∖ \{C\}) \land w = (\frac{G (z) - G (C)}{z - C}) F (C))\}$
250	248 249	eqtr4di	$⊢ φ \to \{⟨z, w⟩ \| (z \in ((X \cap Y) ∖ \{C\}) \land w = (\frac{G (z) - G (C)}{z - C}) (u \in ℂ, v \in ℂ ⟼ u v) F (C))\} = (z \in ((X \cap Y) ∖ \{C\}) ⟼ (\frac{G (z) - G (C)}{z - C}) F (C))$
251	250	oveq1d	$⊢ φ \to \{⟨z, w⟩ \| (z \in ((X \cap Y) ∖ \{C\}) \land w = (\frac{G (z) - G (C)}{z - C}) (u \in ℂ, v \in ℂ ⟼ u v) F (C))\} {lim}_{ℂ} C = (z \in ((X \cap Y) ∖ \{C\}) ⟼ (\frac{G (z) - G (C)}{z - C}) F (C)) {lim}_{ℂ} C$
252	239 241 251	3eltr3d	$⊢ φ \to L F (C) \in ((z \in ((X \cap Y) ∖ \{C\}) ⟼ (\frac{G (z) - G (C)}{z - C}) F (C)) {lim}_{ℂ} C)$
253	8	addcn	$⊢ + \in ((J \times_{t} J) Cn J)$
254	182 183	mulcld	$⊢ φ \to K G (C) \in ℂ$
255	232 43	mulcld	$⊢ φ \to L F (C) \in ℂ$
256	254 255	opelxpd	$⊢ φ \to ⟨K G (C), L F (C)⟩ \in (ℂ \times ℂ)$
257	185	cncnpi	$⊢ (+ \in ((J \times_{t} J) Cn J) \land ⟨K G (C), L F (C)⟩ \in (ℂ \times ℂ)) \to + \in ((J \times_{t} J) CnP J) (⟨K G (C), L F (C)⟩)$
258	253 256 257	sylancr	$⊢ φ \to + \in ((J \times_{t} J) CnP J) (⟨K G (C), L F (C)⟩)$
259	60 72 73 73 8 76 202 252 258	limccnp2	$⊢ φ \to K G (C) + L F (C) \in ((z \in ((X \cap Y) ∖ \{C\}) ⟼ (\frac{F (z) - F (C)}{z - C}) G (z) + (\frac{G (z) - G (C)}{z - C}) F (C)) {lim}_{ℂ} C)$
260	37 243	subcld	$⊢ (φ \land z \in ((X \cap Y) ∖ \{C\})) \to F (z) - F (C) \in ℂ$
261	260 59	mulcld	$⊢ (φ \land z \in ((X \cap Y) ∖ \{C\})) \to (F (z) - F (C)) G (z) \in ℂ$
262	69	adantr	$⊢ (φ \land z \in ((X \cap Y) ∖ \{C\})) \to C \in Y$
263	56 262	ffvelcdmd	$⊢ (φ \land z \in ((X \cap Y) ∖ \{C\})) \to G (C) \in ℂ$
264	59 263	subcld	$⊢ (φ \land z \in ((X \cap Y) ∖ \{C\})) \to G (z) - G (C) \in ℂ$
265	264 243	mulcld	$⊢ (φ \land z \in ((X \cap Y) ∖ \{C\})) \to (G (z) - G (C)) F (C) \in ℂ$
266	47 242	sseldd	$⊢ (φ \land z \in ((X \cap Y) ∖ \{C\})) \to C \in ℂ$
267	48 266	subcld	$⊢ (φ \land z \in ((X \cap Y) ∖ \{C\})) \to z - C \in ℂ$
268	261 265 267 54	divdird	$⊢ (φ \land z \in ((X \cap Y) ∖ \{C\})) \to \frac{(F (z) - F (C)) G (z) + (G (z) - G (C)) F (C)}{z - C} = (\frac{(F (z) - F (C)) G (z)}{z - C}) + (\frac{(G (z) - G (C)) F (C)}{z - C})$
269	37 59	mulcld	$⊢ (φ \land z \in ((X \cap Y) ∖ \{C\})) \to F (z) G (z) \in ℂ$
270	243 59	mulcld	$⊢ (φ \land z \in ((X \cap Y) ∖ \{C\})) \to F (C) G (z) \in ℂ$
271	243 263	mulcld	$⊢ (φ \land z \in ((X \cap Y) ∖ \{C\})) \to F (C) G (C) \in ℂ$
272	269 270 271	npncand	$⊢ (φ \land z \in ((X \cap Y) ∖ \{C\})) \to (F (z) G (z) - F (C) G (z)) + F (C) G (z) - F (C) G (C) = F (z) G (z) - F (C) G (C)$
273	37 243 59	subdird	$⊢ (φ \land z \in ((X \cap Y) ∖ \{C\})) \to (F (z) - F (C)) G (z) = F (z) G (z) - F (C) G (z)$
274	264 243	mulcomd	$⊢ (φ \land z \in ((X \cap Y) ∖ \{C\})) \to (G (z) - G (C)) F (C) = F (C) (G (z) - G (C))$
275	243 59 263	subdid	$⊢ (φ \land z \in ((X \cap Y) ∖ \{C\})) \to F (C) (G (z) - G (C)) = F (C) G (z) - F (C) G (C)$
276	274 275	eqtrd	$⊢ (φ \land z \in ((X \cap Y) ∖ \{C\})) \to (G (z) - G (C)) F (C) = F (C) G (z) - F (C) G (C)$
277	273 276	oveq12d	$⊢ (φ \land z \in ((X \cap Y) ∖ \{C\})) \to (F (z) - F (C)) G (z) + (G (z) - G (C)) F (C) = (F (z) G (z) - F (C) G (z)) + F (C) G (z) - F (C) G (C)$
278	1	ffnd	$⊢ φ \to F Fn X$
279	278	adantr	$⊢ (φ \land z \in ((X \cap Y) ∖ \{C\})) \to F Fn X$
280	3	ffnd	$⊢ φ \to G Fn Y$
281	280	adantr	$⊢ (φ \land z \in ((X \cap Y) ∖ \{C\})) \to G Fn Y$
282		ssexg	$⊢ (X \subseteq ℂ \land ℂ \in V) \to X \in V$
283	46 110 282	sylancl	$⊢ φ \to X \in V$
284	283	adantr	$⊢ (φ \land z \in ((X \cap Y) ∖ \{C\})) \to X \in V$
285		ssexg	$⊢ (Y \subseteq ℂ \land ℂ \in V) \to Y \in V$
286	64 110 285	sylancl	$⊢ φ \to Y \in V$
287	286	adantr	$⊢ (φ \land z \in ((X \cap Y) ∖ \{C\})) \to Y \in V$
288		eqid	$⊢ X \cap Y = X \cap Y$
289		eqidd	$⊢ ((φ \land z \in ((X \cap Y) ∖ \{C\})) \land z \in X) \to F (z) = F (z)$
290		eqidd	$⊢ ((φ \land z \in ((X \cap Y) ∖ \{C\})) \land z \in Y) \to G (z) = G (z)$
291	279 281 284 287 288 289 290	ofval	$⊢ ((φ \land z \in ((X \cap Y) ∖ \{C\})) \land z \in (X \cap Y)) \to (F \times_{f} G) (z) = F (z) G (z)$
292	35 291	mpdan	$⊢ (φ \land z \in ((X \cap Y) ∖ \{C\})) \to (F \times_{f} G) (z) = F (z) G (z)$
293		eqidd	$⊢ ((φ \land z \in ((X \cap Y) ∖ \{C\})) \land C \in X) \to F (C) = F (C)$
294		eqidd	$⊢ ((φ \land z \in ((X \cap Y) ∖ \{C\})) \land C \in Y) \to G (C) = G (C)$
295	279 281 284 287 288 293 294	ofval	$⊢ ((φ \land z \in ((X \cap Y) ∖ \{C\})) \land C \in (X \cap Y)) \to (F \times_{f} G) (C) = F (C) G (C)$
296	127 295	mpidan	$⊢ (φ \land z \in ((X \cap Y) ∖ \{C\})) \to (F \times_{f} G) (C) = F (C) G (C)$
297	292 296	oveq12d	$⊢ (φ \land z \in ((X \cap Y) ∖ \{C\})) \to (F \times_{f} G) (z) - (F \times_{f} G) (C) = F (z) G (z) - F (C) G (C)$
298	272 277 297	3eqtr4d	$⊢ (φ \land z \in ((X \cap Y) ∖ \{C\})) \to (F (z) - F (C)) G (z) + (G (z) - G (C)) F (C) = (F \times_{f} G) (z) - (F \times_{f} G) (C)$
299	298	oveq1d	$⊢ (φ \land z \in ((X \cap Y) ∖ \{C\})) \to \frac{(F (z) - F (C)) G (z) + (G (z) - G (C)) F (C)}{z - C} = \frac{(F \times_{f} G) (z) - (F \times_{f} G) (C)}{z - C}$
300	260 59 267 54	div23d	$⊢ (φ \land z \in ((X \cap Y) ∖ \{C\})) \to \frac{(F (z) - F (C)) G (z)}{z - C} = (\frac{F (z) - F (C)}{z - C}) G (z)$
301	264 243 267 54	div23d	$⊢ (φ \land z \in ((X \cap Y) ∖ \{C\})) \to \frac{(G (z) - G (C)) F (C)}{z - C} = (\frac{G (z) - G (C)}{z - C}) F (C)$
302	300 301	oveq12d	$⊢ (φ \land z \in ((X \cap Y) ∖ \{C\})) \to (\frac{(F (z) - F (C)) G (z)}{z - C}) + (\frac{(G (z) - G (C)) F (C)}{z - C}) = (\frac{F (z) - F (C)}{z - C}) G (z) + (\frac{G (z) - G (C)}{z - C}) F (C)$
303	268 299 302	3eqtr3d	$⊢ (φ \land z \in ((X \cap Y) ∖ \{C\})) \to \frac{(F \times_{f} G) (z) - (F \times_{f} G) (C)}{z - C} = (\frac{F (z) - F (C)}{z - C}) G (z) + (\frac{G (z) - G (C)}{z - C}) F (C)$
304	303	mpteq2dva	$⊢ φ \to (z \in ((X \cap Y) ∖ \{C\}) ⟼ \frac{(F \times_{f} G) (z) - (F \times_{f} G) (C)}{z - C}) = (z \in ((X \cap Y) ∖ \{C\}) ⟼ (\frac{F (z) - F (C)}{z - C}) G (z) + (\frac{G (z) - G (C)}{z - C}) F (C))$
305	304	oveq1d	$⊢ φ \to (z \in ((X \cap Y) ∖ \{C\}) ⟼ \frac{(F \times_{f} G) (z) - (F \times_{f} G) (C)}{z - C}) {lim}_{ℂ} C = (z \in ((X \cap Y) ∖ \{C\}) ⟼ (\frac{F (z) - F (C)}{z - C}) G (z) + (\frac{G (z) - G (C)}{z - C}) F (C)) {lim}_{ℂ} C$
306	259 305	eleqtrrd	$⊢ φ \to K G (C) + L F (C) \in ((z \in ((X \cap Y) ∖ \{C\}) ⟼ \frac{(F \times_{f} G) (z) - (F \times_{f} G) (C)}{z - C}) {lim}_{ℂ} C)$
307		eqid	$⊢ (z \in ((X \cap Y) ∖ \{C\}) ⟼ \frac{(F \times_{f} G) (z) - (F \times_{f} G) (C)}{z - C}) = (z \in ((X \cap Y) ∖ \{C\}) ⟼ \frac{(F \times_{f} G) (z) - (F \times_{f} G) (C)}{z - C})$
308		mulcl	$⊢ (x \in ℂ \land y \in ℂ) \to x y \in ℂ$
309	308	adantl	$⊢ (φ \land (x \in ℂ \land y \in ℂ)) \to x y \in ℂ$
310	309 1 3 283 286 288	off	$⊢ φ \to (F \times_{f} G) : X \cap Y ⟶ ℂ$
311	9 8 307 5 310 84	eldv	$⊢ φ \to (C {(F \times_{f} G)}_{S}^{'} (K G (C) + L F (C)) \leftrightarrow (C \in int (J ↾_{𝑡} S) (X \cap Y) \land K G (C) + L F (C) \in ((z \in ((X \cap Y) ∖ \{C\}) ⟼ \frac{(F \times_{f} G) (z) - (F \times_{f} G) (C)}{z - C}) {lim}_{ℂ} C)))$
312	31 306 311	mpbir2and	$⊢ φ \to C {(F \times_{f} G)}_{S}^{'} (K G (C) + L F (C))$

Metamath Proof Explorer

Theorem dvmulbr

Proof