gg-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 . (Revised by GG, 16-Mar-2025)

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

Proof

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

Metamath Proof Explorer

Theorem gg-dvmulbr

Proof