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)

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

Metamath Proof Explorer

Theorem dvaddbr

Proof