Theorem dvaddxxbr 15375

Description: The sum rule for derivatives at a point. That is, if the derivative of 𝐹 at 𝐶 is 𝐾 and the derivative of 𝐺 at 𝐶 is 𝐿, then the derivative of the pointwise sum of those two functions at 𝐶 is 𝐾 + 𝐿. (Contributed by Mario Carneiro, 9-Aug-2014.) (Revised by Jim Kingdon, 25-Nov-2023.)

Hypotheses

Ref	Expression
dvadd.f	⊢ (𝜑 → 𝐹:𝑋⟶ℂ)
dvadd.x	⊢ (𝜑 → 𝑋 ⊆ 𝑆)
dvaddxx.g	⊢ (𝜑 → 𝐺:𝑋⟶ℂ)
dvaddbr.s	⊢ (𝜑 → 𝑆 ⊆ ℂ)
dvadd.bf	⊢ (𝜑 → 𝐶(𝑆 D 𝐹)𝐾)
dvadd.bg	⊢ (𝜑 → 𝐶(𝑆 D 𝐺)𝐿)
dvaddcntop.j	⊢ 𝐽 = (MetOpen‘(abs ∘ − ))

Assertion

Ref	Expression
dvaddxxbr	⊢ (𝜑 → 𝐶(𝑆 D (𝐹 ∘𝑓 + 𝐺))(𝐾 + 𝐿))

Proof of Theorem dvaddxxbr

Dummy variables 𝑦 𝑧 𝑥 𝑤 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		dvadd.bg	. . . 4 ⊢ (𝜑 → 𝐶(𝑆 D 𝐺)𝐿)
2		eqid 2229	. . . . 5 ⊢ (𝐽 ↾t 𝑆) = (𝐽 ↾t 𝑆)
3		dvaddcntop.j	. . . . 5 ⊢ 𝐽 = (MetOpen‘(abs ∘ − ))
4		eqid 2229	. . . . 5 ⊢ (𝑧 ∈ {𝑤 ∈ 𝑋 ∣ 𝑤 # 𝐶} ↦ (((𝐺‘𝑧) − (𝐺‘𝐶)) / (𝑧 − 𝐶))) = (𝑧 ∈ {𝑤 ∈ 𝑋 ∣ 𝑤 # 𝐶} ↦ (((𝐺‘𝑧) − (𝐺‘𝐶)) / (𝑧 − 𝐶)))
5		dvaddbr.s	. . . . 5 ⊢ (𝜑 → 𝑆 ⊆ ℂ)
6		dvaddxx.g	. . . . 5 ⊢ (𝜑 → 𝐺:𝑋⟶ℂ)
7		dvadd.x	. . . . 5 ⊢ (𝜑 → 𝑋 ⊆ 𝑆)
8	2, 3, 4, 5, 6, 7	eldvap 15356	. . . 4 ⊢ (𝜑 → (𝐶(𝑆 D 𝐺)𝐿 ↔ (𝐶 ∈ ((int‘(𝐽 ↾t 𝑆))‘𝑋) ∧ 𝐿 ∈ ((𝑧 ∈ {𝑤 ∈ 𝑋 ∣ 𝑤 # 𝐶} ↦ (((𝐺‘𝑧) − (𝐺‘𝐶)) / (𝑧 − 𝐶))) limℂ 𝐶))))
9	1, 8	mpbid 147	. . 3 ⊢ (𝜑 → (𝐶 ∈ ((int‘(𝐽 ↾t 𝑆))‘𝑋) ∧ 𝐿 ∈ ((𝑧 ∈ {𝑤 ∈ 𝑋 ∣ 𝑤 # 𝐶} ↦ (((𝐺‘𝑧) − (𝐺‘𝐶)) / (𝑧 − 𝐶))) limℂ 𝐶)))
10	9	simpld 112	. 2 ⊢ (𝜑 → 𝐶 ∈ ((int‘(𝐽 ↾t 𝑆))‘𝑋))
11		dvadd.f	. . . . 5 ⊢ (𝜑 → 𝐹:𝑋⟶ℂ)
12	7, 5	sstrd 3234	. . . . 5 ⊢ (𝜑 → 𝑋 ⊆ ℂ)
13	3	cntoptopon 15206	. . . . . . . . 9 ⊢ 𝐽 ∈ (TopOn‘ℂ)
14		resttopon 14845	. . . . . . . . 9 ⊢ ((𝐽 ∈ (TopOn‘ℂ) ∧ 𝑆 ⊆ ℂ) → (𝐽 ↾t 𝑆) ∈ (TopOn‘𝑆))
15	13, 5, 14	sylancr 414	. . . . . . . 8 ⊢ (𝜑 → (𝐽 ↾t 𝑆) ∈ (TopOn‘𝑆))
16		topontop 14688	. . . . . . . 8 ⊢ ((𝐽 ↾t 𝑆) ∈ (TopOn‘𝑆) → (𝐽 ↾t 𝑆) ∈ Top)
17	15, 16	syl 14	. . . . . . 7 ⊢ (𝜑 → (𝐽 ↾t 𝑆) ∈ Top)
18		toponuni 14689	. . . . . . . . 9 ⊢ ((𝐽 ↾t 𝑆) ∈ (TopOn‘𝑆) → 𝑆 = ∪ (𝐽 ↾t 𝑆))
19	15, 18	syl 14	. . . . . . . 8 ⊢ (𝜑 → 𝑆 = ∪ (𝐽 ↾t 𝑆))
20	7, 19	sseqtrd 3262	. . . . . . 7 ⊢ (𝜑 → 𝑋 ⊆ ∪ (𝐽 ↾t 𝑆))
21		eqid 2229	. . . . . . . 8 ⊢ ∪ (𝐽 ↾t 𝑆) = ∪ (𝐽 ↾t 𝑆)
22	21	ntrss2 14795	. . . . . . 7 ⊢ (((𝐽 ↾t 𝑆) ∈ Top ∧ 𝑋 ⊆ ∪ (𝐽 ↾t 𝑆)) → ((int‘(𝐽 ↾t 𝑆))‘𝑋) ⊆ 𝑋)
23	17, 20, 22	syl2anc 411	. . . . . 6 ⊢ (𝜑 → ((int‘(𝐽 ↾t 𝑆))‘𝑋) ⊆ 𝑋)
24		dvadd.bf	. . . . . . . 8 ⊢ (𝜑 → 𝐶(𝑆 D 𝐹)𝐾)
25		eqid 2229	. . . . . . . . 9 ⊢ (𝑧 ∈ {𝑤 ∈ 𝑋 ∣ 𝑤 # 𝐶} ↦ (((𝐹‘𝑧) − (𝐹‘𝐶)) / (𝑧 − 𝐶))) = (𝑧 ∈ {𝑤 ∈ 𝑋 ∣ 𝑤 # 𝐶} ↦ (((𝐹‘𝑧) − (𝐹‘𝐶)) / (𝑧 − 𝐶)))
26	2, 3, 25, 5, 11, 7	eldvap 15356	. . . . . . . 8 ⊢ (𝜑 → (𝐶(𝑆 D 𝐹)𝐾 ↔ (𝐶 ∈ ((int‘(𝐽 ↾t 𝑆))‘𝑋) ∧ 𝐾 ∈ ((𝑧 ∈ {𝑤 ∈ 𝑋 ∣ 𝑤 # 𝐶} ↦ (((𝐹‘𝑧) − (𝐹‘𝐶)) / (𝑧 − 𝐶))) limℂ 𝐶))))
27	24, 26	mpbid 147	. . . . . . 7 ⊢ (𝜑 → (𝐶 ∈ ((int‘(𝐽 ↾t 𝑆))‘𝑋) ∧ 𝐾 ∈ ((𝑧 ∈ {𝑤 ∈ 𝑋 ∣ 𝑤 # 𝐶} ↦ (((𝐹‘𝑧) − (𝐹‘𝐶)) / (𝑧 − 𝐶))) limℂ 𝐶)))
28	27	simpld 112	. . . . . 6 ⊢ (𝜑 → 𝐶 ∈ ((int‘(𝐽 ↾t 𝑆))‘𝑋))
29	23, 28	sseldd 3225	. . . . 5 ⊢ (𝜑 → 𝐶 ∈ 𝑋)
30	11, 12, 29	dvlemap 15354	. . . 4 ⊢ ((𝜑 ∧ 𝑧 ∈ {𝑤 ∈ 𝑋 ∣ 𝑤 # 𝐶}) → (((𝐹‘𝑧) − (𝐹‘𝐶)) / (𝑧 − 𝐶)) ∈ ℂ)
31	6, 12, 29	dvlemap 15354	. . . 4 ⊢ ((𝜑 ∧ 𝑧 ∈ {𝑤 ∈ 𝑋 ∣ 𝑤 # 𝐶}) → (((𝐺‘𝑧) − (𝐺‘𝐶)) / (𝑧 − 𝐶)) ∈ ℂ)
32		ssidd 3245	. . . 4 ⊢ (𝜑 → ℂ ⊆ ℂ)
33		txtopon 14936	. . . . . 6 ⊢ ((𝐽 ∈ (TopOn‘ℂ) ∧ 𝐽 ∈ (TopOn‘ℂ)) → (𝐽 ×t 𝐽) ∈ (TopOn‘(ℂ × ℂ)))
34	13, 13, 33	mp2an 426	. . . . 5 ⊢ (𝐽 ×t 𝐽) ∈ (TopOn‘(ℂ × ℂ))
35	34	toponrestid 14695	. . . 4 ⊢ (𝐽 ×t 𝐽) = ((𝐽 ×t 𝐽) ↾t (ℂ × ℂ))
36	27	simprd 114	. . . 4 ⊢ (𝜑 → 𝐾 ∈ ((𝑧 ∈ {𝑤 ∈ 𝑋 ∣ 𝑤 # 𝐶} ↦ (((𝐹‘𝑧) − (𝐹‘𝐶)) / (𝑧 − 𝐶))) limℂ 𝐶))
37	9	simprd 114	. . . 4 ⊢ (𝜑 → 𝐿 ∈ ((𝑧 ∈ {𝑤 ∈ 𝑋 ∣ 𝑤 # 𝐶} ↦ (((𝐺‘𝑧) − (𝐺‘𝐶)) / (𝑧 − 𝐶))) limℂ 𝐶))
38	3	addcncntop 15236	. . . . 5 ⊢ + ∈ ((𝐽 ×t 𝐽) Cn 𝐽)
39	5, 11, 7	dvcl 15357	. . . . . . 7 ⊢ ((𝜑 ∧ 𝐶(𝑆 D 𝐹)𝐾) → 𝐾 ∈ ℂ)
40	24, 39	mpdan 421	. . . . . 6 ⊢ (𝜑 → 𝐾 ∈ ℂ)
41	5, 6, 7	dvcl 15357	. . . . . . 7 ⊢ ((𝜑 ∧ 𝐶(𝑆 D 𝐺)𝐿) → 𝐿 ∈ ℂ)
42	1, 41	mpdan 421	. . . . . 6 ⊢ (𝜑 → 𝐿 ∈ ℂ)
43	40, 42	opelxpd 4752	. . . . 5 ⊢ (𝜑 → ⟨𝐾, 𝐿⟩ ∈ (ℂ × ℂ))
44	34	toponunii 14691	. . . . . 6 ⊢ (ℂ × ℂ) = ∪ (𝐽 ×t 𝐽)
45	44	cncnpi 14902	. . . . 5 ⊢ (( + ∈ ((𝐽 ×t 𝐽) Cn 𝐽) ∧ ⟨𝐾, 𝐿⟩ ∈ (ℂ × ℂ)) → + ∈ (((𝐽 ×t 𝐽) CnP 𝐽)‘⟨𝐾, 𝐿⟩))
46	38, 43, 45	sylancr 414	. . . 4 ⊢ (𝜑 → + ∈ (((𝐽 ×t 𝐽) CnP 𝐽)‘⟨𝐾, 𝐿⟩))
47	30, 31, 32, 32, 3, 35, 36, 37, 46	limccnp2cntop 15351	. . 3 ⊢ (𝜑 → (𝐾 + 𝐿) ∈ ((𝑧 ∈ {𝑤 ∈ 𝑋 ∣ 𝑤 # 𝐶} ↦ ((((𝐹‘𝑧) − (𝐹‘𝐶)) / (𝑧 − 𝐶)) + (((𝐺‘𝑧) − (𝐺‘𝐶)) / (𝑧 − 𝐶)))) limℂ 𝐶))
48		elrabi 2956	. . . . . . . . . . 11 ⊢ (𝑧 ∈ {𝑤 ∈ 𝑋 ∣ 𝑤 # 𝐶} → 𝑧 ∈ 𝑋)
49	48	adantl 277	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑧 ∈ {𝑤 ∈ 𝑋 ∣ 𝑤 # 𝐶}) → 𝑧 ∈ 𝑋)
50	11	ffnd 5474	. . . . . . . . . . . 12 ⊢ (𝜑 → 𝐹 Fn 𝑋)
51	50	adantr 276	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑧 ∈ {𝑤 ∈ 𝑋 ∣ 𝑤 # 𝐶}) → 𝐹 Fn 𝑋)
52	6	ffnd 5474	. . . . . . . . . . . 12 ⊢ (𝜑 → 𝐺 Fn 𝑋)
53	52	adantr 276	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑧 ∈ {𝑤 ∈ 𝑋 ∣ 𝑤 # 𝐶}) → 𝐺 Fn 𝑋)
54		cnex 8123	. . . . . . . . . . . . 13 ⊢ ℂ ∈ V
55		ssexg 4223	. . . . . . . . . . . . 13 ⊢ ((𝑋 ⊆ ℂ ∧ ℂ ∈ V) → 𝑋 ∈ V)
56	12, 54, 55	sylancl 413	. . . . . . . . . . . 12 ⊢ (𝜑 → 𝑋 ∈ V)
57	56	adantr 276	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑧 ∈ {𝑤 ∈ 𝑋 ∣ 𝑤 # 𝐶}) → 𝑋 ∈ V)
58		inidm 3413	. . . . . . . . . . 11 ⊢ (𝑋 ∩ 𝑋) = 𝑋
59		eqidd 2230	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑧 ∈ {𝑤 ∈ 𝑋 ∣ 𝑤 # 𝐶}) ∧ 𝑧 ∈ 𝑋) → (𝐹‘𝑧) = (𝐹‘𝑧))
60		eqidd 2230	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑧 ∈ {𝑤 ∈ 𝑋 ∣ 𝑤 # 𝐶}) ∧ 𝑧 ∈ 𝑋) → (𝐺‘𝑧) = (𝐺‘𝑧))
61	11	adantr 276	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑧 ∈ {𝑤 ∈ 𝑋 ∣ 𝑤 # 𝐶}) → 𝐹:𝑋⟶ℂ)
62	61	ffvelcdmda 5770	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑧 ∈ {𝑤 ∈ 𝑋 ∣ 𝑤 # 𝐶}) ∧ 𝑧 ∈ 𝑋) → (𝐹‘𝑧) ∈ ℂ)
63	6	adantr 276	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑧 ∈ {𝑤 ∈ 𝑋 ∣ 𝑤 # 𝐶}) → 𝐺:𝑋⟶ℂ)
64	63	ffvelcdmda 5770	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑧 ∈ {𝑤 ∈ 𝑋 ∣ 𝑤 # 𝐶}) ∧ 𝑧 ∈ 𝑋) → (𝐺‘𝑧) ∈ ℂ)
65	62, 64	addcld 8166	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑧 ∈ {𝑤 ∈ 𝑋 ∣ 𝑤 # 𝐶}) ∧ 𝑧 ∈ 𝑋) → ((𝐹‘𝑧) + (𝐺‘𝑧)) ∈ ℂ)
66	51, 53, 57, 57, 58, 59, 60, 65	ofvalg 6228	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑧 ∈ {𝑤 ∈ 𝑋 ∣ 𝑤 # 𝐶}) ∧ 𝑧 ∈ 𝑋) → ((𝐹 ∘𝑓 + 𝐺)‘𝑧) = ((𝐹‘𝑧) + (𝐺‘𝑧)))
67	49, 66	mpdan 421	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑧 ∈ {𝑤 ∈ 𝑋 ∣ 𝑤 # 𝐶}) → ((𝐹 ∘𝑓 + 𝐺)‘𝑧) = ((𝐹‘𝑧) + (𝐺‘𝑧)))
68		eqidd 2230	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑧 ∈ {𝑤 ∈ 𝑋 ∣ 𝑤 # 𝐶}) ∧ 𝐶 ∈ 𝑋) → (𝐹‘𝐶) = (𝐹‘𝐶))
69		eqidd 2230	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑧 ∈ {𝑤 ∈ 𝑋 ∣ 𝑤 # 𝐶}) ∧ 𝐶 ∈ 𝑋) → (𝐺‘𝐶) = (𝐺‘𝐶))
70	61	ffvelcdmda 5770	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑧 ∈ {𝑤 ∈ 𝑋 ∣ 𝑤 # 𝐶}) ∧ 𝐶 ∈ 𝑋) → (𝐹‘𝐶) ∈ ℂ)
71	63	ffvelcdmda 5770	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑧 ∈ {𝑤 ∈ 𝑋 ∣ 𝑤 # 𝐶}) ∧ 𝐶 ∈ 𝑋) → (𝐺‘𝐶) ∈ ℂ)
72	70, 71	addcld 8166	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑧 ∈ {𝑤 ∈ 𝑋 ∣ 𝑤 # 𝐶}) ∧ 𝐶 ∈ 𝑋) → ((𝐹‘𝐶) + (𝐺‘𝐶)) ∈ ℂ)
73	51, 53, 57, 57, 58, 68, 69, 72	ofvalg 6228	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑧 ∈ {𝑤 ∈ 𝑋 ∣ 𝑤 # 𝐶}) ∧ 𝐶 ∈ 𝑋) → ((𝐹 ∘𝑓 + 𝐺)‘𝐶) = ((𝐹‘𝐶) + (𝐺‘𝐶)))
74	29, 73	mpidan 423	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑧 ∈ {𝑤 ∈ 𝑋 ∣ 𝑤 # 𝐶}) → ((𝐹 ∘𝑓 + 𝐺)‘𝐶) = ((𝐹‘𝐶) + (𝐺‘𝐶)))
75	67, 74	oveq12d 6019	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑧 ∈ {𝑤 ∈ 𝑋 ∣ 𝑤 # 𝐶}) → (((𝐹 ∘𝑓 + 𝐺)‘𝑧) − ((𝐹 ∘𝑓 + 𝐺)‘𝐶)) = (((𝐹‘𝑧) + (𝐺‘𝑧)) − ((𝐹‘𝐶) + (𝐺‘𝐶))))
76		ffvelcdm 5768	. . . . . . . . . 10 ⊢ ((𝐹:𝑋⟶ℂ ∧ 𝑧 ∈ 𝑋) → (𝐹‘𝑧) ∈ ℂ)
77	11, 48, 76	syl2an 289	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑧 ∈ {𝑤 ∈ 𝑋 ∣ 𝑤 # 𝐶}) → (𝐹‘𝑧) ∈ ℂ)
78	63, 49	ffvelcdmd 5771	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑧 ∈ {𝑤 ∈ 𝑋 ∣ 𝑤 # 𝐶}) → (𝐺‘𝑧) ∈ ℂ)
79	11, 29	ffvelcdmd 5771	. . . . . . . . . 10 ⊢ (𝜑 → (𝐹‘𝐶) ∈ ℂ)
80	79	adantr 276	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑧 ∈ {𝑤 ∈ 𝑋 ∣ 𝑤 # 𝐶}) → (𝐹‘𝐶) ∈ ℂ)
81	6, 29	ffvelcdmd 5771	. . . . . . . . . 10 ⊢ (𝜑 → (𝐺‘𝐶) ∈ ℂ)
82	81	adantr 276	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑧 ∈ {𝑤 ∈ 𝑋 ∣ 𝑤 # 𝐶}) → (𝐺‘𝐶) ∈ ℂ)
83	77, 78, 80, 82	addsub4d 8504	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑧 ∈ {𝑤 ∈ 𝑋 ∣ 𝑤 # 𝐶}) → (((𝐹‘𝑧) + (𝐺‘𝑧)) − ((𝐹‘𝐶) + (𝐺‘𝐶))) = (((𝐹‘𝑧) − (𝐹‘𝐶)) + ((𝐺‘𝑧) − (𝐺‘𝐶))))
84	75, 83	eqtrd 2262	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑧 ∈ {𝑤 ∈ 𝑋 ∣ 𝑤 # 𝐶}) → (((𝐹 ∘𝑓 + 𝐺)‘𝑧) − ((𝐹 ∘𝑓 + 𝐺)‘𝐶)) = (((𝐹‘𝑧) − (𝐹‘𝐶)) + ((𝐺‘𝑧) − (𝐺‘𝐶))))
85	84	oveq1d 6016	. . . . . 6 ⊢ ((𝜑 ∧ 𝑧 ∈ {𝑤 ∈ 𝑋 ∣ 𝑤 # 𝐶}) → ((((𝐹 ∘𝑓 + 𝐺)‘𝑧) − ((𝐹 ∘𝑓 + 𝐺)‘𝐶)) / (𝑧 − 𝐶)) = ((((𝐹‘𝑧) − (𝐹‘𝐶)) + ((𝐺‘𝑧) − (𝐺‘𝐶))) / (𝑧 − 𝐶)))
86	61, 49	ffvelcdmd 5771	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑧 ∈ {𝑤 ∈ 𝑋 ∣ 𝑤 # 𝐶}) → (𝐹‘𝑧) ∈ ℂ)
87	86, 80	subcld 8457	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑧 ∈ {𝑤 ∈ 𝑋 ∣ 𝑤 # 𝐶}) → ((𝐹‘𝑧) − (𝐹‘𝐶)) ∈ ℂ)
88	78, 82	subcld 8457	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑧 ∈ {𝑤 ∈ 𝑋 ∣ 𝑤 # 𝐶}) → ((𝐺‘𝑧) − (𝐺‘𝐶)) ∈ ℂ)
89		ssrab2 3309	. . . . . . . . . 10 ⊢ {𝑤 ∈ 𝑋 ∣ 𝑤 # 𝐶} ⊆ 𝑋
90	89, 12	sstrid 3235	. . . . . . . . 9 ⊢ (𝜑 → {𝑤 ∈ 𝑋 ∣ 𝑤 # 𝐶} ⊆ ℂ)
91	90	sselda 3224	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑧 ∈ {𝑤 ∈ 𝑋 ∣ 𝑤 # 𝐶}) → 𝑧 ∈ ℂ)
92	12, 29	sseldd 3225	. . . . . . . . 9 ⊢ (𝜑 → 𝐶 ∈ ℂ)
93	92	adantr 276	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑧 ∈ {𝑤 ∈ 𝑋 ∣ 𝑤 # 𝐶}) → 𝐶 ∈ ℂ)
94	91, 93	subcld 8457	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑧 ∈ {𝑤 ∈ 𝑋 ∣ 𝑤 # 𝐶}) → (𝑧 − 𝐶) ∈ ℂ)
95		breq1 4086	. . . . . . . . . . 11 ⊢ (𝑤 = 𝑧 → (𝑤 # 𝐶 ↔ 𝑧 # 𝐶))
96	95	elrab 2959	. . . . . . . . . 10 ⊢ (𝑧 ∈ {𝑤 ∈ 𝑋 ∣ 𝑤 # 𝐶} ↔ (𝑧 ∈ 𝑋 ∧ 𝑧 # 𝐶))
97	96	simprbi 275	. . . . . . . . 9 ⊢ (𝑧 ∈ {𝑤 ∈ 𝑋 ∣ 𝑤 # 𝐶} → 𝑧 # 𝐶)
98	97	adantl 277	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑧 ∈ {𝑤 ∈ 𝑋 ∣ 𝑤 # 𝐶}) → 𝑧 # 𝐶)
99	91, 93, 98	subap0d 8791	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑧 ∈ {𝑤 ∈ 𝑋 ∣ 𝑤 # 𝐶}) → (𝑧 − 𝐶) # 0)
100	87, 88, 94, 99	divdirapd 8976	. . . . . 6 ⊢ ((𝜑 ∧ 𝑧 ∈ {𝑤 ∈ 𝑋 ∣ 𝑤 # 𝐶}) → ((((𝐹‘𝑧) − (𝐹‘𝐶)) + ((𝐺‘𝑧) − (𝐺‘𝐶))) / (𝑧 − 𝐶)) = ((((𝐹‘𝑧) − (𝐹‘𝐶)) / (𝑧 − 𝐶)) + (((𝐺‘𝑧) − (𝐺‘𝐶)) / (𝑧 − 𝐶))))
101	85, 100	eqtrd 2262	. . . . 5 ⊢ ((𝜑 ∧ 𝑧 ∈ {𝑤 ∈ 𝑋 ∣ 𝑤 # 𝐶}) → ((((𝐹 ∘𝑓 + 𝐺)‘𝑧) − ((𝐹 ∘𝑓 + 𝐺)‘𝐶)) / (𝑧 − 𝐶)) = ((((𝐹‘𝑧) − (𝐹‘𝐶)) / (𝑧 − 𝐶)) + (((𝐺‘𝑧) − (𝐺‘𝐶)) / (𝑧 − 𝐶))))
102	101	mpteq2dva 4174	. . . 4 ⊢ (𝜑 → (𝑧 ∈ {𝑤 ∈ 𝑋 ∣ 𝑤 # 𝐶} ↦ ((((𝐹 ∘𝑓 + 𝐺)‘𝑧) − ((𝐹 ∘𝑓 + 𝐺)‘𝐶)) / (𝑧 − 𝐶))) = (𝑧 ∈ {𝑤 ∈ 𝑋 ∣ 𝑤 # 𝐶} ↦ ((((𝐹‘𝑧) − (𝐹‘𝐶)) / (𝑧 − 𝐶)) + (((𝐺‘𝑧) − (𝐺‘𝐶)) / (𝑧 − 𝐶)))))
103	102	oveq1d 6016	. . 3 ⊢ (𝜑 → ((𝑧 ∈ {𝑤 ∈ 𝑋 ∣ 𝑤 # 𝐶} ↦ ((((𝐹 ∘𝑓 + 𝐺)‘𝑧) − ((𝐹 ∘𝑓 + 𝐺)‘𝐶)) / (𝑧 − 𝐶))) limℂ 𝐶) = ((𝑧 ∈ {𝑤 ∈ 𝑋 ∣ 𝑤 # 𝐶} ↦ ((((𝐹‘𝑧) − (𝐹‘𝐶)) / (𝑧 − 𝐶)) + (((𝐺‘𝑧) − (𝐺‘𝐶)) / (𝑧 − 𝐶)))) limℂ 𝐶))
104	47, 103	eleqtrrd 2309	. 2 ⊢ (𝜑 → (𝐾 + 𝐿) ∈ ((𝑧 ∈ {𝑤 ∈ 𝑋 ∣ 𝑤 # 𝐶} ↦ ((((𝐹 ∘𝑓 + 𝐺)‘𝑧) − ((𝐹 ∘𝑓 + 𝐺)‘𝐶)) / (𝑧 − 𝐶))) limℂ 𝐶))
105		eqid 2229	. . 3 ⊢ (𝑧 ∈ {𝑤 ∈ 𝑋 ∣ 𝑤 # 𝐶} ↦ ((((𝐹 ∘𝑓 + 𝐺)‘𝑧) − ((𝐹 ∘𝑓 + 𝐺)‘𝐶)) / (𝑧 − 𝐶))) = (𝑧 ∈ {𝑤 ∈ 𝑋 ∣ 𝑤 # 𝐶} ↦ ((((𝐹 ∘𝑓 + 𝐺)‘𝑧) − ((𝐹 ∘𝑓 + 𝐺)‘𝐶)) / (𝑧 − 𝐶)))
106		addcl 8124	. . . . 5 ⊢ ((𝑥 ∈ ℂ ∧ 𝑦 ∈ ℂ) → (𝑥 + 𝑦) ∈ ℂ)
107	106	adantl 277	. . . 4 ⊢ ((𝜑 ∧ (𝑥 ∈ ℂ ∧ 𝑦 ∈ ℂ)) → (𝑥 + 𝑦) ∈ ℂ)
108	107, 11, 6, 56, 56, 58	off 6231	. . 3 ⊢ (𝜑 → (𝐹 ∘𝑓 + 𝐺):𝑋⟶ℂ)
109	2, 3, 105, 5, 108, 7	eldvap 15356	. 2 ⊢ (𝜑 → (𝐶(𝑆 D (𝐹 ∘𝑓 + 𝐺))(𝐾 + 𝐿) ↔ (𝐶 ∈ ((int‘(𝐽 ↾t 𝑆))‘𝑋) ∧ (𝐾 + 𝐿) ∈ ((𝑧 ∈ {𝑤 ∈ 𝑋 ∣ 𝑤 # 𝐶} ↦ ((((𝐹 ∘𝑓 + 𝐺)‘𝑧) − ((𝐹 ∘𝑓 + 𝐺)‘𝐶)) / (𝑧 − 𝐶))) limℂ 𝐶))))
110	10, 104, 109	mpbir2and 950	1 ⊢ (𝜑 → 𝐶(𝑆 D (𝐹 ∘𝑓 + 𝐺))(𝐾 + 𝐿))

Syntax hints:   → wi 4   ∧ wa 104   = wceq 1395   ∈ wcel 2200  {crab 2512  Vcvv 2799   ⊆ wss 3197  ⟨cop 3669  ∪ cuni 3888   class class class wbr 4083   ↦ cmpt 4145   × cxp 4717   ∘ ccom 4723   Fn wfn 5313  ⟶wf 5314  ‘cfv 5318  (class class class)co 6001   ∘_𝑓 cof 6216  ℂcc 7997   + caddc 8002   − cmin 8317   # cap 8728   / cdiv 8819  abscabs 11508   ↾_t crest 13272  MetOpencmopn 14505  Topctop 14671  TopOnctopon 14684  intcnt 14767   Cn ccn 14859   CnP ccnp 14860   ×_t ctx 14926   lim_ℂ climc 15328   D cdv 15329

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-in1 617  ax-in2 618  ax-io 714  ax-5 1493  ax-7 1494  ax-gen 1495  ax-ie1 1539  ax-ie2 1540  ax-8 1550  ax-10 1551  ax-11 1552  ax-i12 1553  ax-bndl 1555  ax-4 1556  ax-17 1572  ax-i9 1576  ax-ial 1580  ax-i5r 1581  ax-13 2202  ax-14 2203  ax-ext 2211  ax-coll 4199  ax-sep 4202  ax-nul 4210  ax-pow 4258  ax-pr 4293  ax-un 4524  ax-setind 4629  ax-iinf 4680  ax-cnex 8090  ax-resscn 8091  ax-1cn 8092  ax-1re 8093  ax-icn 8094  ax-addcl 8095  ax-addrcl 8096  ax-mulcl 8097  ax-mulrcl 8098  ax-addcom 8099  ax-mulcom 8100  ax-addass 8101  ax-mulass 8102  ax-distr 8103  ax-i2m1 8104  ax-0lt1 8105  ax-1rid 8106  ax-0id 8107  ax-rnegex 8108  ax-precex 8109  ax-cnre 8110  ax-pre-ltirr 8111  ax-pre-ltwlin 8112  ax-pre-lttrn 8113  ax-pre-apti 8114  ax-pre-ltadd 8115  ax-pre-mulgt0 8116  ax-pre-mulext 8117  ax-arch 8118  ax-caucvg 8119  ax-addf 8121

This theorem depends on definitions:  df-bi 117  df-stab 836  df-dc 840  df-3or 1003  df-3an 1004  df-tru 1398  df-fal 1401  df-nf 1507  df-sb 1809  df-eu 2080  df-mo 2081  df-clab 2216  df-cleq 2222  df-clel 2225  df-nfc 2361  df-ne 2401  df-nel 2496  df-ral 2513  df-rex 2514  df-reu 2515  df-rmo 2516  df-rab 2517  df-v 2801  df-sbc 3029  df-csb 3125  df-dif 3199  df-un 3201  df-in 3203  df-ss 3210  df-nul 3492  df-if 3603  df-pw 3651  df-sn 3672  df-pr 3673  df-op 3675  df-uni 3889  df-int 3924  df-iun 3967  df-br 4084  df-opab 4146  df-mpt 4147  df-tr 4183  df-id 4384  df-po 4387  df-iso 4388  df-iord 4457  df-on 4459  df-ilim 4460  df-suc 4462  df-iom 4683  df-xp 4725  df-rel 4726  df-cnv 4727  df-co 4728  df-dm 4729  df-rn 4730  df-res 4731  df-ima 4732  df-iota 5278  df-fun 5320  df-fn 5321  df-f 5322  df-f1 5323  df-fo 5324  df-f1o 5325  df-fv 5326  df-isom 5327  df-riota 5954  df-ov 6004  df-oprab 6005  df-mpo 6006  df-of 6218  df-1st 6286  df-2nd 6287  df-recs 6451  df-frec 6537  df-map 6797  df-pm 6798  df-sup 7151  df-inf 7152  df-pnf 8183  df-mnf 8184  df-xr 8185  df-ltxr 8186  df-le 8187  df-sub 8319  df-neg 8320  df-reap 8722  df-ap 8729  df-div 8820  df-inn 9111  df-2 9169  df-3 9170  df-4 9171  df-n0 9370  df-z 9447  df-uz 9723  df-q 9815  df-rp 9850  df-xneg 9968  df-xadd 9969  df-seqfrec 10670  df-exp 10761  df-cj 11353  df-re 11354  df-im 11355  df-rsqrt 11509  df-abs 11510  df-rest 13274  df-topgen 13293  df-psmet 14507  df-xmet 14508  df-met 14509  df-bl 14510  df-mopn 14511  df-top 14672  df-topon 14685  df-bases 14717  df-ntr 14770  df-cn 14862  df-cnp 14863  df-tx 14927  df-limced 15330  df-dvap 15331

This theorem is referenced by:  dvaddxx  15377  dviaddf  15379