dvaddbr

Description: The sum rule for derivatives at a point. For the (simpler but more limited) function version, see dvadd . (Contributed by Mario Carneiro, 9-Aug-2014) (Revised by Mario Carneiro, 28-Dec-2016) Remove unnecessary hypotheses. (Revised by GG, 10-Apr-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	dvaddbr	$⊢ φ \to C {(F +_{f} G)}_{S}^{'} (K + L)$

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		inss1	$⊢ X \cap Y \subseteq X$
33		ssdif	$⊢ X \cap Y \subseteq X \to (X \cap Y) ∖ \{C\} \subseteq X ∖ \{C\}$
34	32 33	mp1i	$⊢ φ \to (X \cap Y) ∖ \{C\} \subseteq X ∖ \{C\}$
35	34	sselda	$⊢ (φ \land z \in ((X \cap Y) ∖ \{C\})) \to z \in (X ∖ \{C\})$
36	2 5	sstrd	$⊢ φ \to X \subseteq ℂ$
37	28	ntrss2	$⊢ (J ↾_{𝑡} S \in Top \land X \subseteq ⋃ (J ↾_{𝑡} S)) \to int (J ↾_{𝑡} S) (X) \subseteq X$
38	23 26 37	syl2anc	$⊢ φ \to int (J ↾_{𝑡} S) (X) \subseteq X$
39	38 13	sseldd	$⊢ φ \to C \in X$
40	1 36 39	dvlem	$⊢ (φ \land z \in (X ∖ \{C\})) \to \frac{F (z) - F (C)}{z - C} \in ℂ$
41	35 40	syldan	$⊢ (φ \land z \in ((X \cap Y) ∖ \{C\})) \to \frac{F (z) - F (C)}{z - C} \in ℂ$
42		inss2	$⊢ X \cap Y \subseteq Y$
43		ssdif	$⊢ X \cap Y \subseteq Y \to (X \cap Y) ∖ \{C\} \subseteq Y ∖ \{C\}$
44	42 43	mp1i	$⊢ φ \to (X \cap Y) ∖ \{C\} \subseteq Y ∖ \{C\}$
45	44	sselda	$⊢ (φ \land z \in ((X \cap Y) ∖ \{C\})) \to z \in (Y ∖ \{C\})$
46	4 5	sstrd	$⊢ φ \to Y \subseteq ℂ$
47	28	ntrss2	$⊢ (J ↾_{𝑡} S \in Top \land Y \subseteq ⋃ (J ↾_{𝑡} S)) \to int (J ↾_{𝑡} S) (Y) \subseteq Y$
48	23 27 47	syl2anc	$⊢ φ \to int (J ↾_{𝑡} S) (Y) \subseteq Y$
49	48 17	sseldd	$⊢ φ \to C \in Y$
50	3 46 49	dvlem	$⊢ (φ \land z \in (Y ∖ \{C\})) \to \frac{G (z) - G (C)}{z - C} \in ℂ$
51	45 50	syldan	$⊢ (φ \land z \in ((X \cap Y) ∖ \{C\})) \to \frac{G (z) - G (C)}{z - C} \in ℂ$
52		ssidd	$⊢ φ \to ℂ \subseteq ℂ$
53		txtopon	$⊢ (J \in TopOn (ℂ) \land J \in TopOn (ℂ)) \to J \times_{t} J \in TopOn (ℂ \times ℂ)$
54	19 19 53	mp2an	$⊢ J \times_{t} J \in TopOn (ℂ \times ℂ)$
55	54	toponrestid	$⊢ J \times_{t} J = (J \times_{t} J) ↾_{𝑡} (ℂ \times ℂ)$
56	12	simprd	$⊢ φ \to K \in ((z \in (X ∖ \{C\}) ⟼ \frac{F (z) - F (C)}{z - C}) {lim}_{ℂ} C)$
57	40	fmpttd	$⊢ φ \to (z \in (X ∖ \{C\}) ⟼ \frac{F (z) - F (C)}{z - C}) : X ∖ \{C\} ⟶ ℂ$
58	36	ssdifssd	$⊢ φ \to X ∖ \{C\} \subseteq ℂ$
59		eqid	$⊢ J ↾_{𝑡} ((X ∖ \{C\}) \cup \{C\}) = J ↾_{𝑡} ((X ∖ \{C\}) \cup \{C\})$
60	32 2	sstrid	$⊢ φ \to X \cap Y \subseteq S$
61	60 25	sseqtrd	$⊢ φ \to X \cap Y \subseteq ⋃ (J ↾_{𝑡} S)$
62		difssd	$⊢ φ \to ⋃ (J ↾_{𝑡} S) ∖ X \subseteq ⋃ (J ↾_{𝑡} S)$
63	61 62	unssd	$⊢ φ \to (X \cap Y) \cup (⋃ (J ↾_{𝑡} S) ∖ X) \subseteq ⋃ (J ↾_{𝑡} S)$
64		ssun1	$⊢ X \cap Y \subseteq (X \cap Y) \cup (⋃ (J ↾_{𝑡} S) ∖ X)$
65	64	a1i	$⊢ φ \to X \cap Y \subseteq (X \cap Y) \cup (⋃ (J ↾_{𝑡} S) ∖ X)$
66	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))$
67	23 63 65 66	syl3anc	$⊢ φ \to int (J ↾_{𝑡} S) (X \cap Y) \subseteq int (J ↾_{𝑡} S) ((X \cap Y) \cup (⋃ (J ↾_{𝑡} S) ∖ X))$
68	67 31	sseldd	$⊢ φ \to C \in int (J ↾_{𝑡} S) ((X \cap Y) \cup (⋃ (J ↾_{𝑡} S) ∖ X))$
69	68 39	elind	$⊢ φ \to C \in (int (J ↾_{𝑡} S) ((X \cap Y) \cup (⋃ (J ↾_{𝑡} S) ∖ X)) \cap X)$
70	32	a1i	$⊢ φ \to X \cap Y \subseteq X$
71		eqid	$⊢ (J ↾_{𝑡} S) ↾_{𝑡} X = (J ↾_{𝑡} S) ↾_{𝑡} X$
72	28 71	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$
73	23 26 70 72	syl3anc	$⊢ φ \to int ((J ↾_{𝑡} S) ↾_{𝑡} X) (X \cap Y) = int (J ↾_{𝑡} S) ((X \cap Y) \cup (⋃ (J ↾_{𝑡} S) ∖ X)) \cap X$
74	8	cnfldtop	$⊢ J \in Top$
75	74	a1i	$⊢ φ \to J \in Top$
76		cnex	$⊢ ℂ \in V$
77		ssexg	$⊢ (S \subseteq ℂ \land ℂ \in V) \to S \in V$
78	5 76 77	sylancl	$⊢ φ \to S \in V$
79		restabs	$⊢ (J \in Top \land X \subseteq S \land S \in V) \to (J ↾_{𝑡} S) ↾_{𝑡} X = J ↾_{𝑡} X$
80	75 2 78 79	syl3anc	$⊢ φ \to (J ↾_{𝑡} S) ↾_{𝑡} X = J ↾_{𝑡} X$
81	80	fveq2d	$⊢ φ \to int ((J ↾_{𝑡} S) ↾_{𝑡} X) = int (J ↾_{𝑡} X)$
82	81	fveq1d	$⊢ φ \to int ((J ↾_{𝑡} S) ↾_{𝑡} X) (X \cap Y) = int (J ↾_{𝑡} X) (X \cap Y)$
83	73 82	eqtr3d	$⊢ φ \to int (J ↾_{𝑡} S) ((X \cap Y) \cup (⋃ (J ↾_{𝑡} S) ∖ X)) \cap X = int (J ↾_{𝑡} X) (X \cap Y)$
84	69 83	eleqtrd	$⊢ φ \to C \in int (J ↾_{𝑡} X) (X \cap Y)$
85		undif1	$⊢ (X ∖ \{C\}) \cup \{C\} = X \cup \{C\}$
86	39	snssd	$⊢ φ \to \{C\} \subseteq X$
87		ssequn2	$⊢ \{C\} \subseteq X \leftrightarrow X \cup \{C\} = X$
88	86 87	sylib	$⊢ φ \to X \cup \{C\} = X$
89	85 88	eqtrid	$⊢ φ \to (X ∖ \{C\}) \cup \{C\} = X$
90	89	oveq2d	$⊢ φ \to J ↾_{𝑡} ((X ∖ \{C\}) \cup \{C\}) = J ↾_{𝑡} X$
91	90	fveq2d	$⊢ φ \to int (J ↾_{𝑡} ((X ∖ \{C\}) \cup \{C\})) = int (J ↾_{𝑡} X)$
92		undif1	$⊢ ((X \cap Y) ∖ \{C\}) \cup \{C\} = (X \cap Y) \cup \{C\}$
93	39 49	elind	$⊢ φ \to C \in (X \cap Y)$
94	93	snssd	$⊢ φ \to \{C\} \subseteq X \cap Y$
95		ssequn2	$⊢ \{C\} \subseteq X \cap Y \leftrightarrow (X \cap Y) \cup \{C\} = X \cap Y$
96	94 95	sylib	$⊢ φ \to (X \cap Y) \cup \{C\} = X \cap Y$
97	92 96	eqtrid	$⊢ φ \to ((X \cap Y) ∖ \{C\}) \cup \{C\} = X \cap Y$
98	91 97	fveq12d	$⊢ φ \to int (J ↾_{𝑡} ((X ∖ \{C\}) \cup \{C\})) (((X \cap Y) ∖ \{C\}) \cup \{C\}) = int (J ↾_{𝑡} X) (X \cap Y)$
99	84 98	eleqtrrd	$⊢ φ \to C \in int (J ↾_{𝑡} ((X ∖ \{C\}) \cup \{C\})) (((X \cap Y) ∖ \{C\}) \cup \{C\})$
100	57 34 58 8 59 99	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$
101	34	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})$
102	101	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$
103	100 102	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$
104	56 103	eleqtrd	$⊢ φ \to K \in ((z \in ((X \cap Y) ∖ \{C\}) ⟼ \frac{F (z) - F (C)}{z - C}) {lim}_{ℂ} C)$
105	16	simprd	$⊢ φ \to L \in ((z \in (Y ∖ \{C\}) ⟼ \frac{G (z) - G (C)}{z - C}) {lim}_{ℂ} C)$
106	50	fmpttd	$⊢ φ \to (z \in (Y ∖ \{C\}) ⟼ \frac{G (z) - G (C)}{z - C}) : Y ∖ \{C\} ⟶ ℂ$
107	46	ssdifssd	$⊢ φ \to Y ∖ \{C\} \subseteq ℂ$
108		eqid	$⊢ J ↾_{𝑡} ((Y ∖ \{C\}) \cup \{C\}) = J ↾_{𝑡} ((Y ∖ \{C\}) \cup \{C\})$
109		difssd	$⊢ φ \to ⋃ (J ↾_{𝑡} S) ∖ Y \subseteq ⋃ (J ↾_{𝑡} S)$
110	61 109	unssd	$⊢ φ \to (X \cap Y) \cup (⋃ (J ↾_{𝑡} S) ∖ Y) \subseteq ⋃ (J ↾_{𝑡} S)$
111		ssun1	$⊢ X \cap Y \subseteq (X \cap Y) \cup (⋃ (J ↾_{𝑡} S) ∖ Y)$
112	111	a1i	$⊢ φ \to X \cap Y \subseteq (X \cap Y) \cup (⋃ (J ↾_{𝑡} S) ∖ Y)$
113	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))$
114	23 110 112 113	syl3anc	$⊢ φ \to int (J ↾_{𝑡} S) (X \cap Y) \subseteq int (J ↾_{𝑡} S) ((X \cap Y) \cup (⋃ (J ↾_{𝑡} S) ∖ Y))$
115	114 31	sseldd	$⊢ φ \to C \in int (J ↾_{𝑡} S) ((X \cap Y) \cup (⋃ (J ↾_{𝑡} S) ∖ Y))$
116	115 49	elind	$⊢ φ \to C \in (int (J ↾_{𝑡} S) ((X \cap Y) \cup (⋃ (J ↾_{𝑡} S) ∖ Y)) \cap Y)$
117	42	a1i	$⊢ φ \to X \cap Y \subseteq Y$
118		eqid	$⊢ (J ↾_{𝑡} S) ↾_{𝑡} Y = (J ↾_{𝑡} S) ↾_{𝑡} Y$
119	28 118	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$
120	23 27 117 119	syl3anc	$⊢ φ \to int ((J ↾_{𝑡} S) ↾_{𝑡} Y) (X \cap Y) = int (J ↾_{𝑡} S) ((X \cap Y) \cup (⋃ (J ↾_{𝑡} S) ∖ Y)) \cap Y$
121		restabs	$⊢ (J \in Top \land Y \subseteq S \land S \in V) \to (J ↾_{𝑡} S) ↾_{𝑡} Y = J ↾_{𝑡} Y$
122	75 4 78 121	syl3anc	$⊢ φ \to (J ↾_{𝑡} S) ↾_{𝑡} Y = J ↾_{𝑡} Y$
123	122	fveq2d	$⊢ φ \to int ((J ↾_{𝑡} S) ↾_{𝑡} Y) = int (J ↾_{𝑡} Y)$
124	123	fveq1d	$⊢ φ \to int ((J ↾_{𝑡} S) ↾_{𝑡} Y) (X \cap Y) = int (J ↾_{𝑡} Y) (X \cap Y)$
125	120 124	eqtr3d	$⊢ φ \to int (J ↾_{𝑡} S) ((X \cap Y) \cup (⋃ (J ↾_{𝑡} S) ∖ Y)) \cap Y = int (J ↾_{𝑡} Y) (X \cap Y)$
126	116 125	eleqtrd	$⊢ φ \to C \in int (J ↾_{𝑡} Y) (X \cap Y)$
127		undif1	$⊢ (Y ∖ \{C\}) \cup \{C\} = Y \cup \{C\}$
128	49	snssd	$⊢ φ \to \{C\} \subseteq Y$
129		ssequn2	$⊢ \{C\} \subseteq Y \leftrightarrow Y \cup \{C\} = Y$
130	128 129	sylib	$⊢ φ \to Y \cup \{C\} = Y$
131	127 130	eqtrid	$⊢ φ \to (Y ∖ \{C\}) \cup \{C\} = Y$
132	131	oveq2d	$⊢ φ \to J ↾_{𝑡} ((Y ∖ \{C\}) \cup \{C\}) = J ↾_{𝑡} Y$
133	132	fveq2d	$⊢ φ \to int (J ↾_{𝑡} ((Y ∖ \{C\}) \cup \{C\})) = int (J ↾_{𝑡} Y)$
134	133 97	fveq12d	$⊢ φ \to int (J ↾_{𝑡} ((Y ∖ \{C\}) \cup \{C\})) (((X \cap Y) ∖ \{C\}) \cup \{C\}) = int (J ↾_{𝑡} Y) (X \cap Y)$
135	126 134	eleqtrrd	$⊢ φ \to C \in int (J ↾_{𝑡} ((Y ∖ \{C\}) \cup \{C\})) (((X \cap Y) ∖ \{C\}) \cup \{C\})$
136	106 44 107 8 108 135	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$
137	44	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})$
138	137	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$
139	136 138	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$
140	105 139	eleqtrd	$⊢ φ \to L \in ((z \in ((X \cap Y) ∖ \{C\}) ⟼ \frac{G (z) - G (C)}{z - C}) {lim}_{ℂ} C)$
141	8	addcn	$⊢ + \in ((J \times_{t} J) Cn J)$
142	5 1 2	dvcl	$⊢ (φ \land C F_{S}^{'} K) \to K \in ℂ$
143	6 142	mpdan	$⊢ φ \to K \in ℂ$
144	5 3 4	dvcl	$⊢ (φ \land C G_{S}^{'} L) \to L \in ℂ$
145	7 144	mpdan	$⊢ φ \to L \in ℂ$
146	143 145	opelxpd	$⊢ φ \to ⟨K, L⟩ \in (ℂ \times ℂ)$
147	54	toponunii	$⊢ ℂ \times ℂ = ⋃ (J \times_{t} J)$
148	147	cncnpi	$⊢ (+ \in ((J \times_{t} J) Cn J) \land ⟨K, L⟩ \in (ℂ \times ℂ)) \to + \in ((J \times_{t} J) CnP J) (⟨K, L⟩)$
149	141 146 148	sylancr	$⊢ φ \to + \in ((J \times_{t} J) CnP J) (⟨K, L⟩)$
150	41 51 52 52 8 55 104 140 149	limccnp2	$⊢ φ \to K + L \in ((z \in ((X \cap Y) ∖ \{C\}) ⟼ (\frac{F (z) - F (C)}{z - C}) + (\frac{G (z) - G (C)}{z - C})) {lim}_{ℂ} C)$
151		eldifi	$⊢ z \in ((X \cap Y) ∖ \{C\}) \to z \in (X \cap Y)$
152	151	adantl	$⊢ (φ \land z \in ((X \cap Y) ∖ \{C\})) \to z \in (X \cap Y)$
153	1	ffnd	$⊢ φ \to F Fn X$
154	153	adantr	$⊢ (φ \land z \in ((X \cap Y) ∖ \{C\})) \to F Fn X$
155	3	ffnd	$⊢ φ \to G Fn Y$
156	155	adantr	$⊢ (φ \land z \in ((X \cap Y) ∖ \{C\})) \to G Fn Y$
157		ssexg	$⊢ (X \subseteq ℂ \land ℂ \in V) \to X \in V$
158	36 76 157	sylancl	$⊢ φ \to X \in V$
159	158	adantr	$⊢ (φ \land z \in ((X \cap Y) ∖ \{C\})) \to X \in V$
160		ssexg	$⊢ (Y \subseteq ℂ \land ℂ \in V) \to Y \in V$
161	46 76 160	sylancl	$⊢ φ \to Y \in V$
162	161	adantr	$⊢ (φ \land z \in ((X \cap Y) ∖ \{C\})) \to Y \in V$
163		eqid	$⊢ X \cap Y = X \cap Y$
164		eqidd	$⊢ ((φ \land z \in ((X \cap Y) ∖ \{C\})) \land z \in X) \to F (z) = F (z)$
165		eqidd	$⊢ ((φ \land z \in ((X \cap Y) ∖ \{C\})) \land z \in Y) \to G (z) = G (z)$
166	154 156 159 162 163 164 165	ofval	$⊢ ((φ \land z \in ((X \cap Y) ∖ \{C\})) \land z \in (X \cap Y)) \to (F +_{f} G) (z) = F (z) + G (z)$
167	152 166	mpdan	$⊢ (φ \land z \in ((X \cap Y) ∖ \{C\})) \to (F +_{f} G) (z) = F (z) + G (z)$
168		eqidd	$⊢ ((φ \land z \in ((X \cap Y) ∖ \{C\})) \land C \in X) \to F (C) = F (C)$
169		eqidd	$⊢ ((φ \land z \in ((X \cap Y) ∖ \{C\})) \land C \in Y) \to G (C) = G (C)$
170	154 156 159 162 163 168 169	ofval	$⊢ ((φ \land z \in ((X \cap Y) ∖ \{C\})) \land C \in (X \cap Y)) \to (F +_{f} G) (C) = F (C) + G (C)$
171	93 170	mpidan	$⊢ (φ \land z \in ((X \cap Y) ∖ \{C\})) \to (F +_{f} G) (C) = F (C) + G (C)$
172	167 171	oveq12d	$⊢ (φ \land z \in ((X \cap Y) ∖ \{C\})) \to (F +_{f} G) (z) - (F +_{f} G) (C) = F (z) + G (z) - (F (C) + G (C))$
173		difss	$⊢ (X \cap Y) ∖ \{C\} \subseteq X \cap Y$
174	173 32	sstri	$⊢ (X \cap Y) ∖ \{C\} \subseteq X$
175	174	sseli	$⊢ z \in ((X \cap Y) ∖ \{C\}) \to z \in X$
176		ffvelcdm	$⊢ (F : X ⟶ ℂ \land z \in X) \to F (z) \in ℂ$
177	1 175 176	syl2an	$⊢ (φ \land z \in ((X \cap Y) ∖ \{C\})) \to F (z) \in ℂ$
178	173 42	sstri	$⊢ (X \cap Y) ∖ \{C\} \subseteq Y$
179	178	sseli	$⊢ z \in ((X \cap Y) ∖ \{C\}) \to z \in Y$
180		ffvelcdm	$⊢ (G : Y ⟶ ℂ \land z \in Y) \to G (z) \in ℂ$
181	3 179 180	syl2an	$⊢ (φ \land z \in ((X \cap Y) ∖ \{C\})) \to G (z) \in ℂ$
182	1 39	ffvelcdmd	$⊢ φ \to F (C) \in ℂ$
183	182	adantr	$⊢ (φ \land z \in ((X \cap Y) ∖ \{C\})) \to F (C) \in ℂ$
184	3 49	ffvelcdmd	$⊢ φ \to G (C) \in ℂ$
185	184	adantr	$⊢ (φ \land z \in ((X \cap Y) ∖ \{C\})) \to G (C) \in ℂ$
186	177 181 183 185	addsub4d	$⊢ (φ \land z \in ((X \cap Y) ∖ \{C\})) \to F (z) + G (z) - (F (C) + G (C)) = (F (z) - F (C)) + G (z) - G (C)$
187	172 186	eqtrd	$⊢ (φ \land z \in ((X \cap Y) ∖ \{C\})) \to (F +_{f} G) (z) - (F +_{f} G) (C) = (F (z) - F (C)) + G (z) - G (C)$
188	187	oveq1d	$⊢ (φ \land z \in ((X \cap Y) ∖ \{C\})) \to \frac{(F +_{f} G) (z) - (F +_{f} G) (C)}{z - C} = \frac{(F (z) - F (C)) + G (z) - G (C)}{z - C}$
189	177 183	subcld	$⊢ (φ \land z \in ((X \cap Y) ∖ \{C\})) \to F (z) - F (C) \in ℂ$
190	181 185	subcld	$⊢ (φ \land z \in ((X \cap Y) ∖ \{C\})) \to G (z) - G (C) \in ℂ$
191	174 36	sstrid	$⊢ φ \to (X \cap Y) ∖ \{C\} \subseteq ℂ$
192	191	sselda	$⊢ (φ \land z \in ((X \cap Y) ∖ \{C\})) \to z \in ℂ$
193	36 39	sseldd	$⊢ φ \to C \in ℂ$
194	193	adantr	$⊢ (φ \land z \in ((X \cap Y) ∖ \{C\})) \to C \in ℂ$
195	192 194	subcld	$⊢ (φ \land z \in ((X \cap Y) ∖ \{C\})) \to z - C \in ℂ$
196		eldifsni	$⊢ z \in ((X \cap Y) ∖ \{C\}) \to z \neq C$
197	196	adantl	$⊢ (φ \land z \in ((X \cap Y) ∖ \{C\})) \to z \neq C$
198	192 194 197	subne0d	$⊢ (φ \land z \in ((X \cap Y) ∖ \{C\})) \to z - C \neq 0$
199	189 190 195 198	divdird	$⊢ (φ \land z \in ((X \cap Y) ∖ \{C\})) \to \frac{(F (z) - F (C)) + G (z) - G (C)}{z - C} = (\frac{F (z) - F (C)}{z - C}) + (\frac{G (z) - G (C)}{z - C})$
200	188 199	eqtrd	$⊢ (φ \land z \in ((X \cap Y) ∖ \{C\})) \to \frac{(F +_{f} G) (z) - (F +_{f} G) (C)}{z - C} = (\frac{F (z) - F (C)}{z - C}) + (\frac{G (z) - G (C)}{z - C})$
201	200	mpteq2dva	$⊢ φ \to (z \in ((X \cap Y) ∖ \{C\}) ⟼ \frac{(F +_{f} G) (z) - (F +_{f} G) (C)}{z - C}) = (z \in ((X \cap Y) ∖ \{C\}) ⟼ (\frac{F (z) - F (C)}{z - C}) + (\frac{G (z) - G (C)}{z - C}))$
202	201	oveq1d	$⊢ φ \to (z \in ((X \cap Y) ∖ \{C\}) ⟼ \frac{(F +_{f} G) (z) - (F +_{f} G) (C)}{z - C}) {lim}_{ℂ} C = (z \in ((X \cap Y) ∖ \{C\}) ⟼ (\frac{F (z) - F (C)}{z - C}) + (\frac{G (z) - G (C)}{z - C})) {lim}_{ℂ} C$
203	150 202	eleqtrrd	$⊢ φ \to K + L \in ((z \in ((X \cap Y) ∖ \{C\}) ⟼ \frac{(F +_{f} G) (z) - (F +_{f} G) (C)}{z - C}) {lim}_{ℂ} C)$
204		eqid	$⊢ (z \in ((X \cap Y) ∖ \{C\}) ⟼ \frac{(F +_{f} G) (z) - (F +_{f} G) (C)}{z - C}) = (z \in ((X \cap Y) ∖ \{C\}) ⟼ \frac{(F +_{f} G) (z) - (F +_{f} G) (C)}{z - C})$
205		addcl	$⊢ (x \in ℂ \land y \in ℂ) \to x + y \in ℂ$
206	205	adantl	$⊢ (φ \land (x \in ℂ \land y \in ℂ)) \to x + y \in ℂ$
207	206 1 3 158 161 163	off	$⊢ φ \to (F +_{f} G) : X \cap Y ⟶ ℂ$
208	9 8 204 5 207 60	eldv	$⊢ φ \to (C {(F +_{f} G)}_{S}^{'} (K + L) \leftrightarrow (C \in int (J ↾_{𝑡} S) (X \cap Y) \land K + L \in ((z \in ((X \cap Y) ∖ \{C\}) ⟼ \frac{(F +_{f} G) (z) - (F +_{f} G) (C)}{z - C}) {lim}_{ℂ} C)))$
209	31 203 208	mpbir2and	$⊢ φ \to C {(F +_{f} G)}_{S}^{'} (K + L)$

Metamath Proof Explorer

Theorem dvaddbr

Proof