Theorem dvmulbrOLD 25996

Description: Obsolete version of dvmulbr 25995 as of 10-Apr-2025. (Contributed by Mario Carneiro, 9-Aug-2014.) (Revised by Mario Carneiro, 28-Dec-2016.) (Proof modification is discouraged.) (New usage is discouraged.)

Hypotheses

Ref	Expression
dvadd.f	⊢ (𝜑 → 𝐹:𝑋⟶ℂ)
dvadd.x	⊢ (𝜑 → 𝑋 ⊆ 𝑆)
dvadd.g	⊢ (𝜑 → 𝐺:𝑌⟶ℂ)
dvadd.y	⊢ (𝜑 → 𝑌 ⊆ 𝑆)
dvaddbr.s	⊢ (𝜑 → 𝑆 ⊆ ℂ)
dvadd.bf	⊢ (𝜑 → 𝐶(𝑆 D 𝐹)𝐾)
dvadd.bg	⊢ (𝜑 → 𝐶(𝑆 D 𝐺)𝐿)
dvadd.j	⊢ 𝐽 = (TopOpen‘ℂfld)

Assertion

Ref	Expression
dvmulbrOLD	⊢ (𝜑 → 𝐶(𝑆 D (𝐹 ∘f · 𝐺))((𝐾 · (𝐺‘𝐶)) + (𝐿 · (𝐹‘𝐶))))

Proof of Theorem dvmulbrOLD

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

Step	Hyp	Ref	Expression
1		dvadd.bf	. . . . . 6 ⊢ (𝜑 → 𝐶(𝑆 D 𝐹)𝐾)
2		eqid 2740	. . . . . . 7 ⊢ (𝐽 ↾t 𝑆) = (𝐽 ↾t 𝑆)
3		dvadd.j	. . . . . . 7 ⊢ 𝐽 = (TopOpen‘ℂfld)
4		eqid 2740	. . . . . . 7 ⊢ (𝑧 ∈ (𝑋 ∖ {𝐶}) ↦ (((𝐹‘𝑧) − (𝐹‘𝐶)) / (𝑧 − 𝐶))) = (𝑧 ∈ (𝑋 ∖ {𝐶}) ↦ (((𝐹‘𝑧) − (𝐹‘𝐶)) / (𝑧 − 𝐶)))
5		dvaddbr.s	. . . . . . 7 ⊢ (𝜑 → 𝑆 ⊆ ℂ)
6		dvadd.f	. . . . . . 7 ⊢ (𝜑 → 𝐹:𝑋⟶ℂ)
7		dvadd.x	. . . . . . 7 ⊢ (𝜑 → 𝑋 ⊆ 𝑆)
8	2, 3, 4, 5, 6, 7	eldv 25953	. . . . . 6 ⊢ (𝜑 → (𝐶(𝑆 D 𝐹)𝐾 ↔ (𝐶 ∈ ((int‘(𝐽 ↾t 𝑆))‘𝑋) ∧ 𝐾 ∈ ((𝑧 ∈ (𝑋 ∖ {𝐶}) ↦ (((𝐹‘𝑧) − (𝐹‘𝐶)) / (𝑧 − 𝐶))) limℂ 𝐶))))
9	1, 8	mpbid 232	. . . . 5 ⊢ (𝜑 → (𝐶 ∈ ((int‘(𝐽 ↾t 𝑆))‘𝑋) ∧ 𝐾 ∈ ((𝑧 ∈ (𝑋 ∖ {𝐶}) ↦ (((𝐹‘𝑧) − (𝐹‘𝐶)) / (𝑧 − 𝐶))) limℂ 𝐶)))
10	9	simpld 494	. . . 4 ⊢ (𝜑 → 𝐶 ∈ ((int‘(𝐽 ↾t 𝑆))‘𝑋))
11		dvadd.bg	. . . . . 6 ⊢ (𝜑 → 𝐶(𝑆 D 𝐺)𝐿)
12		eqid 2740	. . . . . . 7 ⊢ (𝑧 ∈ (𝑌 ∖ {𝐶}) ↦ (((𝐺‘𝑧) − (𝐺‘𝐶)) / (𝑧 − 𝐶))) = (𝑧 ∈ (𝑌 ∖ {𝐶}) ↦ (((𝐺‘𝑧) − (𝐺‘𝐶)) / (𝑧 − 𝐶)))
13		dvadd.g	. . . . . . 7 ⊢ (𝜑 → 𝐺:𝑌⟶ℂ)
14		dvadd.y	. . . . . . 7 ⊢ (𝜑 → 𝑌 ⊆ 𝑆)
15	2, 3, 12, 5, 13, 14	eldv 25953	. . . . . 6 ⊢ (𝜑 → (𝐶(𝑆 D 𝐺)𝐿 ↔ (𝐶 ∈ ((int‘(𝐽 ↾t 𝑆))‘𝑌) ∧ 𝐿 ∈ ((𝑧 ∈ (𝑌 ∖ {𝐶}) ↦ (((𝐺‘𝑧) − (𝐺‘𝐶)) / (𝑧 − 𝐶))) limℂ 𝐶))))
16	11, 15	mpbid 232	. . . . 5 ⊢ (𝜑 → (𝐶 ∈ ((int‘(𝐽 ↾t 𝑆))‘𝑌) ∧ 𝐿 ∈ ((𝑧 ∈ (𝑌 ∖ {𝐶}) ↦ (((𝐺‘𝑧) − (𝐺‘𝐶)) / (𝑧 − 𝐶))) limℂ 𝐶)))
17	16	simpld 494	. . . 4 ⊢ (𝜑 → 𝐶 ∈ ((int‘(𝐽 ↾t 𝑆))‘𝑌))
18	10, 17	elind 4223	. . 3 ⊢ (𝜑 → 𝐶 ∈ (((int‘(𝐽 ↾t 𝑆))‘𝑋) ∩ ((int‘(𝐽 ↾t 𝑆))‘𝑌)))
19	3	cnfldtopon 24824	. . . . . 6 ⊢ 𝐽 ∈ (TopOn‘ℂ)
20		resttopon 23190	. . . . . 6 ⊢ ((𝐽 ∈ (TopOn‘ℂ) ∧ 𝑆 ⊆ ℂ) → (𝐽 ↾t 𝑆) ∈ (TopOn‘𝑆))
21	19, 5, 20	sylancr 586	. . . . 5 ⊢ (𝜑 → (𝐽 ↾t 𝑆) ∈ (TopOn‘𝑆))
22		topontop 22940	. . . . 5 ⊢ ((𝐽 ↾t 𝑆) ∈ (TopOn‘𝑆) → (𝐽 ↾t 𝑆) ∈ Top)
23	21, 22	syl 17	. . . 4 ⊢ (𝜑 → (𝐽 ↾t 𝑆) ∈ Top)
24		toponuni 22941	. . . . . 6 ⊢ ((𝐽 ↾t 𝑆) ∈ (TopOn‘𝑆) → 𝑆 = ∪ (𝐽 ↾t 𝑆))
25	21, 24	syl 17	. . . . 5 ⊢ (𝜑 → 𝑆 = ∪ (𝐽 ↾t 𝑆))
26	7, 25	sseqtrd 4049	. . . 4 ⊢ (𝜑 → 𝑋 ⊆ ∪ (𝐽 ↾t 𝑆))
27	14, 25	sseqtrd 4049	. . . 4 ⊢ (𝜑 → 𝑌 ⊆ ∪ (𝐽 ↾t 𝑆))
28		eqid 2740	. . . . 5 ⊢ ∪ (𝐽 ↾t 𝑆) = ∪ (𝐽 ↾t 𝑆)
29	28	ntrin 23090	. . . 4 ⊢ (((𝐽 ↾t 𝑆) ∈ Top ∧ 𝑋 ⊆ ∪ (𝐽 ↾t 𝑆) ∧ 𝑌 ⊆ ∪ (𝐽 ↾t 𝑆)) → ((int‘(𝐽 ↾t 𝑆))‘(𝑋 ∩ 𝑌)) = (((int‘(𝐽 ↾t 𝑆))‘𝑋) ∩ ((int‘(𝐽 ↾t 𝑆))‘𝑌)))
30	23, 26, 27, 29	syl3anc 1371	. . 3 ⊢ (𝜑 → ((int‘(𝐽 ↾t 𝑆))‘(𝑋 ∩ 𝑌)) = (((int‘(𝐽 ↾t 𝑆))‘𝑋) ∩ ((int‘(𝐽 ↾t 𝑆))‘𝑌)))
31	18, 30	eleqtrrd 2847	. 2 ⊢ (𝜑 → 𝐶 ∈ ((int‘(𝐽 ↾t 𝑆))‘(𝑋 ∩ 𝑌)))
32	6	adantr 480	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑧 ∈ ((𝑋 ∩ 𝑌) ∖ {𝐶})) → 𝐹:𝑋⟶ℂ)
33		inss1 4258	. . . . . . . . 9 ⊢ (𝑋 ∩ 𝑌) ⊆ 𝑋
34		eldifi 4154	. . . . . . . . . 10 ⊢ (𝑧 ∈ ((𝑋 ∩ 𝑌) ∖ {𝐶}) → 𝑧 ∈ (𝑋 ∩ 𝑌))
35	34	adantl 481	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑧 ∈ ((𝑋 ∩ 𝑌) ∖ {𝐶})) → 𝑧 ∈ (𝑋 ∩ 𝑌))
36	33, 35	sselid 4006	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑧 ∈ ((𝑋 ∩ 𝑌) ∖ {𝐶})) → 𝑧 ∈ 𝑋)
37	32, 36	ffvelcdmd 7119	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑧 ∈ ((𝑋 ∩ 𝑌) ∖ {𝐶})) → (𝐹‘𝑧) ∈ ℂ)
38	5, 6, 7	dvbss 25956	. . . . . . . . . 10 ⊢ (𝜑 → dom (𝑆 D 𝐹) ⊆ 𝑋)
39		reldv 25925	. . . . . . . . . . 11 ⊢ Rel (𝑆 D 𝐹)
40		releldm 5969	. . . . . . . . . . 11 ⊢ ((Rel (𝑆 D 𝐹) ∧ 𝐶(𝑆 D 𝐹)𝐾) → 𝐶 ∈ dom (𝑆 D 𝐹))
41	39, 1, 40	sylancr 586	. . . . . . . . . 10 ⊢ (𝜑 → 𝐶 ∈ dom (𝑆 D 𝐹))
42	38, 41	sseldd 4009	. . . . . . . . 9 ⊢ (𝜑 → 𝐶 ∈ 𝑋)
43	6, 42	ffvelcdmd 7119	. . . . . . . 8 ⊢ (𝜑 → (𝐹‘𝐶) ∈ ℂ)
44	43	adantr 480	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑧 ∈ ((𝑋 ∩ 𝑌) ∖ {𝐶})) → (𝐹‘𝐶) ∈ ℂ)
45	37, 44	subcld 11647	. . . . . 6 ⊢ ((𝜑 ∧ 𝑧 ∈ ((𝑋 ∩ 𝑌) ∖ {𝐶})) → ((𝐹‘𝑧) − (𝐹‘𝐶)) ∈ ℂ)
46	7, 5	sstrd 4019	. . . . . . . . 9 ⊢ (𝜑 → 𝑋 ⊆ ℂ)
47	46	adantr 480	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑧 ∈ ((𝑋 ∩ 𝑌) ∖ {𝐶})) → 𝑋 ⊆ ℂ)
48	47, 36	sseldd 4009	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑧 ∈ ((𝑋 ∩ 𝑌) ∖ {𝐶})) → 𝑧 ∈ ℂ)
49	46, 42	sseldd 4009	. . . . . . . 8 ⊢ (𝜑 → 𝐶 ∈ ℂ)
50	49	adantr 480	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑧 ∈ ((𝑋 ∩ 𝑌) ∖ {𝐶})) → 𝐶 ∈ ℂ)
51	48, 50	subcld 11647	. . . . . 6 ⊢ ((𝜑 ∧ 𝑧 ∈ ((𝑋 ∩ 𝑌) ∖ {𝐶})) → (𝑧 − 𝐶) ∈ ℂ)
52		eldifsni 4815	. . . . . . . 8 ⊢ (𝑧 ∈ ((𝑋 ∩ 𝑌) ∖ {𝐶}) → 𝑧 ≠ 𝐶)
53	52	adantl 481	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑧 ∈ ((𝑋 ∩ 𝑌) ∖ {𝐶})) → 𝑧 ≠ 𝐶)
54	48, 50, 53	subne0d 11656	. . . . . 6 ⊢ ((𝜑 ∧ 𝑧 ∈ ((𝑋 ∩ 𝑌) ∖ {𝐶})) → (𝑧 − 𝐶) ≠ 0)
55	45, 51, 54	divcld 12070	. . . . 5 ⊢ ((𝜑 ∧ 𝑧 ∈ ((𝑋 ∩ 𝑌) ∖ {𝐶})) → (((𝐹‘𝑧) − (𝐹‘𝐶)) / (𝑧 − 𝐶)) ∈ ℂ)
56	13	adantr 480	. . . . . 6 ⊢ ((𝜑 ∧ 𝑧 ∈ ((𝑋 ∩ 𝑌) ∖ {𝐶})) → 𝐺:𝑌⟶ℂ)
57		inss2 4259	. . . . . . 7 ⊢ (𝑋 ∩ 𝑌) ⊆ 𝑌
58	57, 35	sselid 4006	. . . . . 6 ⊢ ((𝜑 ∧ 𝑧 ∈ ((𝑋 ∩ 𝑌) ∖ {𝐶})) → 𝑧 ∈ 𝑌)
59	56, 58	ffvelcdmd 7119	. . . . 5 ⊢ ((𝜑 ∧ 𝑧 ∈ ((𝑋 ∩ 𝑌) ∖ {𝐶})) → (𝐺‘𝑧) ∈ ℂ)
60	55, 59	mulcld 11310	. . . 4 ⊢ ((𝜑 ∧ 𝑧 ∈ ((𝑋 ∩ 𝑌) ∖ {𝐶})) → ((((𝐹‘𝑧) − (𝐹‘𝐶)) / (𝑧 − 𝐶)) · (𝐺‘𝑧)) ∈ ℂ)
61		ssdif 4167	. . . . . . . 8 ⊢ ((𝑋 ∩ 𝑌) ⊆ 𝑌 → ((𝑋 ∩ 𝑌) ∖ {𝐶}) ⊆ (𝑌 ∖ {𝐶}))
62	57, 61	mp1i 13	. . . . . . 7 ⊢ (𝜑 → ((𝑋 ∩ 𝑌) ∖ {𝐶}) ⊆ (𝑌 ∖ {𝐶}))
63	62	sselda 4008	. . . . . 6 ⊢ ((𝜑 ∧ 𝑧 ∈ ((𝑋 ∩ 𝑌) ∖ {𝐶})) → 𝑧 ∈ (𝑌 ∖ {𝐶}))
64	14, 5	sstrd 4019	. . . . . . 7 ⊢ (𝜑 → 𝑌 ⊆ ℂ)
65	5, 13, 14	dvbss 25956	. . . . . . . 8 ⊢ (𝜑 → dom (𝑆 D 𝐺) ⊆ 𝑌)
66		reldv 25925	. . . . . . . . 9 ⊢ Rel (𝑆 D 𝐺)
67		releldm 5969	. . . . . . . . 9 ⊢ ((Rel (𝑆 D 𝐺) ∧ 𝐶(𝑆 D 𝐺)𝐿) → 𝐶 ∈ dom (𝑆 D 𝐺))
68	66, 11, 67	sylancr 586	. . . . . . . 8 ⊢ (𝜑 → 𝐶 ∈ dom (𝑆 D 𝐺))
69	65, 68	sseldd 4009	. . . . . . 7 ⊢ (𝜑 → 𝐶 ∈ 𝑌)
70	13, 64, 69	dvlem 25951	. . . . . 6 ⊢ ((𝜑 ∧ 𝑧 ∈ (𝑌 ∖ {𝐶})) → (((𝐺‘𝑧) − (𝐺‘𝐶)) / (𝑧 − 𝐶)) ∈ ℂ)
71	63, 70	syldan 590	. . . . 5 ⊢ ((𝜑 ∧ 𝑧 ∈ ((𝑋 ∩ 𝑌) ∖ {𝐶})) → (((𝐺‘𝑧) − (𝐺‘𝐶)) / (𝑧 − 𝐶)) ∈ ℂ)
72	71, 44	mulcld 11310	. . . 4 ⊢ ((𝜑 ∧ 𝑧 ∈ ((𝑋 ∩ 𝑌) ∖ {𝐶})) → ((((𝐺‘𝑧) − (𝐺‘𝐶)) / (𝑧 − 𝐶)) · (𝐹‘𝐶)) ∈ ℂ)
73		ssidd 4032	. . . 4 ⊢ (𝜑 → ℂ ⊆ ℂ)
74		txtopon 23620	. . . . . 6 ⊢ ((𝐽 ∈ (TopOn‘ℂ) ∧ 𝐽 ∈ (TopOn‘ℂ)) → (𝐽 ×t 𝐽) ∈ (TopOn‘(ℂ × ℂ)))
75	19, 19, 74	mp2an 691	. . . . 5 ⊢ (𝐽 ×t 𝐽) ∈ (TopOn‘(ℂ × ℂ))
76	75	toponrestid 22948	. . . 4 ⊢ (𝐽 ×t 𝐽) = ((𝐽 ×t 𝐽) ↾t (ℂ × ℂ))
77	9	simprd 495	. . . . . 6 ⊢ (𝜑 → 𝐾 ∈ ((𝑧 ∈ (𝑋 ∖ {𝐶}) ↦ (((𝐹‘𝑧) − (𝐹‘𝐶)) / (𝑧 − 𝐶))) limℂ 𝐶))
78	6, 46, 42	dvlem 25951	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑧 ∈ (𝑋 ∖ {𝐶})) → (((𝐹‘𝑧) − (𝐹‘𝐶)) / (𝑧 − 𝐶)) ∈ ℂ)
79	78	fmpttd 7149	. . . . . . . 8 ⊢ (𝜑 → (𝑧 ∈ (𝑋 ∖ {𝐶}) ↦ (((𝐹‘𝑧) − (𝐹‘𝐶)) / (𝑧 − 𝐶))):(𝑋 ∖ {𝐶})⟶ℂ)
80		ssdif 4167	. . . . . . . . 9 ⊢ ((𝑋 ∩ 𝑌) ⊆ 𝑋 → ((𝑋 ∩ 𝑌) ∖ {𝐶}) ⊆ (𝑋 ∖ {𝐶}))
81	33, 80	mp1i 13	. . . . . . . 8 ⊢ (𝜑 → ((𝑋 ∩ 𝑌) ∖ {𝐶}) ⊆ (𝑋 ∖ {𝐶}))
82	46	ssdifssd 4170	. . . . . . . 8 ⊢ (𝜑 → (𝑋 ∖ {𝐶}) ⊆ ℂ)
83		eqid 2740	. . . . . . . 8 ⊢ (𝐽 ↾t ((𝑋 ∖ {𝐶}) ∪ {𝐶})) = (𝐽 ↾t ((𝑋 ∖ {𝐶}) ∪ {𝐶}))
84	33, 7	sstrid 4020	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (𝑋 ∩ 𝑌) ⊆ 𝑆)
85	84, 25	sseqtrd 4049	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (𝑋 ∩ 𝑌) ⊆ ∪ (𝐽 ↾t 𝑆))
86		difssd 4160	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (∪ (𝐽 ↾t 𝑆) ∖ 𝑋) ⊆ ∪ (𝐽 ↾t 𝑆))
87	85, 86	unssd 4215	. . . . . . . . . . . . 13 ⊢ (𝜑 → ((𝑋 ∩ 𝑌) ∪ (∪ (𝐽 ↾t 𝑆) ∖ 𝑋)) ⊆ ∪ (𝐽 ↾t 𝑆))
88		ssun1 4201	. . . . . . . . . . . . . 14 ⊢ (𝑋 ∩ 𝑌) ⊆ ((𝑋 ∩ 𝑌) ∪ (∪ (𝐽 ↾t 𝑆) ∖ 𝑋))
89	88	a1i 11	. . . . . . . . . . . . 13 ⊢ (𝜑 → (𝑋 ∩ 𝑌) ⊆ ((𝑋 ∩ 𝑌) ∪ (∪ (𝐽 ↾t 𝑆) ∖ 𝑋)))
90	28	ntrss 23084	. . . . . . . . . . . . 13 ⊢ (((𝐽 ↾t 𝑆) ∈ Top ∧ ((𝑋 ∩ 𝑌) ∪ (∪ (𝐽 ↾t 𝑆) ∖ 𝑋)) ⊆ ∪ (𝐽 ↾t 𝑆) ∧ (𝑋 ∩ 𝑌) ⊆ ((𝑋 ∩ 𝑌) ∪ (∪ (𝐽 ↾t 𝑆) ∖ 𝑋))) → ((int‘(𝐽 ↾t 𝑆))‘(𝑋 ∩ 𝑌)) ⊆ ((int‘(𝐽 ↾t 𝑆))‘((𝑋 ∩ 𝑌) ∪ (∪ (𝐽 ↾t 𝑆) ∖ 𝑋))))
91	23, 87, 89, 90	syl3anc 1371	. . . . . . . . . . . 12 ⊢ (𝜑 → ((int‘(𝐽 ↾t 𝑆))‘(𝑋 ∩ 𝑌)) ⊆ ((int‘(𝐽 ↾t 𝑆))‘((𝑋 ∩ 𝑌) ∪ (∪ (𝐽 ↾t 𝑆) ∖ 𝑋))))
92	91, 31	sseldd 4009	. . . . . . . . . . 11 ⊢ (𝜑 → 𝐶 ∈ ((int‘(𝐽 ↾t 𝑆))‘((𝑋 ∩ 𝑌) ∪ (∪ (𝐽 ↾t 𝑆) ∖ 𝑋))))
93	92, 42	elind 4223	. . . . . . . . . 10 ⊢ (𝜑 → 𝐶 ∈ (((int‘(𝐽 ↾t 𝑆))‘((𝑋 ∩ 𝑌) ∪ (∪ (𝐽 ↾t 𝑆) ∖ 𝑋))) ∩ 𝑋))
94	33	a1i 11	. . . . . . . . . . . 12 ⊢ (𝜑 → (𝑋 ∩ 𝑌) ⊆ 𝑋)
95		eqid 2740	. . . . . . . . . . . . 13 ⊢ ((𝐽 ↾t 𝑆) ↾t 𝑋) = ((𝐽 ↾t 𝑆) ↾t 𝑋)
96	28, 95	restntr 23211	. . . . . . . . . . . 12 ⊢ (((𝐽 ↾t 𝑆) ∈ Top ∧ 𝑋 ⊆ ∪ (𝐽 ↾t 𝑆) ∧ (𝑋 ∩ 𝑌) ⊆ 𝑋) → ((int‘((𝐽 ↾t 𝑆) ↾t 𝑋))‘(𝑋 ∩ 𝑌)) = (((int‘(𝐽 ↾t 𝑆))‘((𝑋 ∩ 𝑌) ∪ (∪ (𝐽 ↾t 𝑆) ∖ 𝑋))) ∩ 𝑋))
97	23, 26, 94, 96	syl3anc 1371	. . . . . . . . . . 11 ⊢ (𝜑 → ((int‘((𝐽 ↾t 𝑆) ↾t 𝑋))‘(𝑋 ∩ 𝑌)) = (((int‘(𝐽 ↾t 𝑆))‘((𝑋 ∩ 𝑌) ∪ (∪ (𝐽 ↾t 𝑆) ∖ 𝑋))) ∩ 𝑋))
98	3	cnfldtop 24825	. . . . . . . . . . . . . . 15 ⊢ 𝐽 ∈ Top
99	98	a1i 11	. . . . . . . . . . . . . 14 ⊢ (𝜑 → 𝐽 ∈ Top)
100		cnex 11265	. . . . . . . . . . . . . . 15 ⊢ ℂ ∈ V
101		ssexg 5341	. . . . . . . . . . . . . . 15 ⊢ ((𝑆 ⊆ ℂ ∧ ℂ ∈ V) → 𝑆 ∈ V)
102	5, 100, 101	sylancl 585	. . . . . . . . . . . . . 14 ⊢ (𝜑 → 𝑆 ∈ V)
103		restabs 23194	. . . . . . . . . . . . . 14 ⊢ ((𝐽 ∈ Top ∧ 𝑋 ⊆ 𝑆 ∧ 𝑆 ∈ V) → ((𝐽 ↾t 𝑆) ↾t 𝑋) = (𝐽 ↾t 𝑋))
104	99, 7, 102, 103	syl3anc 1371	. . . . . . . . . . . . 13 ⊢ (𝜑 → ((𝐽 ↾t 𝑆) ↾t 𝑋) = (𝐽 ↾t 𝑋))
105	104	fveq2d 6924	. . . . . . . . . . . 12 ⊢ (𝜑 → (int‘((𝐽 ↾t 𝑆) ↾t 𝑋)) = (int‘(𝐽 ↾t 𝑋)))
106	105	fveq1d 6922	. . . . . . . . . . 11 ⊢ (𝜑 → ((int‘((𝐽 ↾t 𝑆) ↾t 𝑋))‘(𝑋 ∩ 𝑌)) = ((int‘(𝐽 ↾t 𝑋))‘(𝑋 ∩ 𝑌)))
107	97, 106	eqtr3d 2782	. . . . . . . . . 10 ⊢ (𝜑 → (((int‘(𝐽 ↾t 𝑆))‘((𝑋 ∩ 𝑌) ∪ (∪ (𝐽 ↾t 𝑆) ∖ 𝑋))) ∩ 𝑋) = ((int‘(𝐽 ↾t 𝑋))‘(𝑋 ∩ 𝑌)))
108	93, 107	eleqtrd 2846	. . . . . . . . 9 ⊢ (𝜑 → 𝐶 ∈ ((int‘(𝐽 ↾t 𝑋))‘(𝑋 ∩ 𝑌)))
109		undif1 4499	. . . . . . . . . . . . 13 ⊢ ((𝑋 ∖ {𝐶}) ∪ {𝐶}) = (𝑋 ∪ {𝐶})
110	42	snssd 4834	. . . . . . . . . . . . . 14 ⊢ (𝜑 → {𝐶} ⊆ 𝑋)
111		ssequn2 4212	. . . . . . . . . . . . . 14 ⊢ ({𝐶} ⊆ 𝑋 ↔ (𝑋 ∪ {𝐶}) = 𝑋)
112	110, 111	sylib 218	. . . . . . . . . . . . 13 ⊢ (𝜑 → (𝑋 ∪ {𝐶}) = 𝑋)
113	109, 112	eqtrid 2792	. . . . . . . . . . . 12 ⊢ (𝜑 → ((𝑋 ∖ {𝐶}) ∪ {𝐶}) = 𝑋)
114	113	oveq2d 7464	. . . . . . . . . . 11 ⊢ (𝜑 → (𝐽 ↾t ((𝑋 ∖ {𝐶}) ∪ {𝐶})) = (𝐽 ↾t 𝑋))
115	114	fveq2d 6924	. . . . . . . . . 10 ⊢ (𝜑 → (int‘(𝐽 ↾t ((𝑋 ∖ {𝐶}) ∪ {𝐶}))) = (int‘(𝐽 ↾t 𝑋)))
116		undif1 4499	. . . . . . . . . . 11 ⊢ (((𝑋 ∩ 𝑌) ∖ {𝐶}) ∪ {𝐶}) = ((𝑋 ∩ 𝑌) ∪ {𝐶})
117	42, 69	elind 4223	. . . . . . . . . . . . 13 ⊢ (𝜑 → 𝐶 ∈ (𝑋 ∩ 𝑌))
118	117	snssd 4834	. . . . . . . . . . . 12 ⊢ (𝜑 → {𝐶} ⊆ (𝑋 ∩ 𝑌))
119		ssequn2 4212	. . . . . . . . . . . 12 ⊢ ({𝐶} ⊆ (𝑋 ∩ 𝑌) ↔ ((𝑋 ∩ 𝑌) ∪ {𝐶}) = (𝑋 ∩ 𝑌))
120	118, 119	sylib 218	. . . . . . . . . . 11 ⊢ (𝜑 → ((𝑋 ∩ 𝑌) ∪ {𝐶}) = (𝑋 ∩ 𝑌))
121	116, 120	eqtrid 2792	. . . . . . . . . 10 ⊢ (𝜑 → (((𝑋 ∩ 𝑌) ∖ {𝐶}) ∪ {𝐶}) = (𝑋 ∩ 𝑌))
122	115, 121	fveq12d 6927	. . . . . . . . 9 ⊢ (𝜑 → ((int‘(𝐽 ↾t ((𝑋 ∖ {𝐶}) ∪ {𝐶})))‘(((𝑋 ∩ 𝑌) ∖ {𝐶}) ∪ {𝐶})) = ((int‘(𝐽 ↾t 𝑋))‘(𝑋 ∩ 𝑌)))
123	108, 122	eleqtrrd 2847	. . . . . . . 8 ⊢ (𝜑 → 𝐶 ∈ ((int‘(𝐽 ↾t ((𝑋 ∖ {𝐶}) ∪ {𝐶})))‘(((𝑋 ∩ 𝑌) ∖ {𝐶}) ∪ {𝐶})))
124	79, 81, 82, 3, 83, 123	limcres 25941	. . . . . . 7 ⊢ (𝜑 → (((𝑧 ∈ (𝑋 ∖ {𝐶}) ↦ (((𝐹‘𝑧) − (𝐹‘𝐶)) / (𝑧 − 𝐶))) ↾ ((𝑋 ∩ 𝑌) ∖ {𝐶})) limℂ 𝐶) = ((𝑧 ∈ (𝑋 ∖ {𝐶}) ↦ (((𝐹‘𝑧) − (𝐹‘𝐶)) / (𝑧 − 𝐶))) limℂ 𝐶))
125	81	resmptd 6069	. . . . . . . 8 ⊢ (𝜑 → ((𝑧 ∈ (𝑋 ∖ {𝐶}) ↦ (((𝐹‘𝑧) − (𝐹‘𝐶)) / (𝑧 − 𝐶))) ↾ ((𝑋 ∩ 𝑌) ∖ {𝐶})) = (𝑧 ∈ ((𝑋 ∩ 𝑌) ∖ {𝐶}) ↦ (((𝐹‘𝑧) − (𝐹‘𝐶)) / (𝑧 − 𝐶))))
126	125	oveq1d 7463	. . . . . . 7 ⊢ (𝜑 → (((𝑧 ∈ (𝑋 ∖ {𝐶}) ↦ (((𝐹‘𝑧) − (𝐹‘𝐶)) / (𝑧 − 𝐶))) ↾ ((𝑋 ∩ 𝑌) ∖ {𝐶})) limℂ 𝐶) = ((𝑧 ∈ ((𝑋 ∩ 𝑌) ∖ {𝐶}) ↦ (((𝐹‘𝑧) − (𝐹‘𝐶)) / (𝑧 − 𝐶))) limℂ 𝐶))
127	124, 126	eqtr3d 2782	. . . . . 6 ⊢ (𝜑 → ((𝑧 ∈ (𝑋 ∖ {𝐶}) ↦ (((𝐹‘𝑧) − (𝐹‘𝐶)) / (𝑧 − 𝐶))) limℂ 𝐶) = ((𝑧 ∈ ((𝑋 ∩ 𝑌) ∖ {𝐶}) ↦ (((𝐹‘𝑧) − (𝐹‘𝐶)) / (𝑧 − 𝐶))) limℂ 𝐶))
128	77, 127	eleqtrd 2846	. . . . 5 ⊢ (𝜑 → 𝐾 ∈ ((𝑧 ∈ ((𝑋 ∩ 𝑌) ∖ {𝐶}) ↦ (((𝐹‘𝑧) − (𝐹‘𝐶)) / (𝑧 − 𝐶))) limℂ 𝐶))
129		eqid 2740	. . . . . . . . . 10 ⊢ (𝐽 ↾t 𝑌) = (𝐽 ↾t 𝑌)
130	129, 3	dvcnp2 25975	. . . . . . . . 9 ⊢ (((𝑆 ⊆ ℂ ∧ 𝐺:𝑌⟶ℂ ∧ 𝑌 ⊆ 𝑆) ∧ 𝐶 ∈ dom (𝑆 D 𝐺)) → 𝐺 ∈ (((𝐽 ↾t 𝑌) CnP 𝐽)‘𝐶))
131	5, 13, 14, 68, 130	syl31anc 1373	. . . . . . . 8 ⊢ (𝜑 → 𝐺 ∈ (((𝐽 ↾t 𝑌) CnP 𝐽)‘𝐶))
132	3, 129	cnplimc 25942	. . . . . . . . 9 ⊢ ((𝑌 ⊆ ℂ ∧ 𝐶 ∈ 𝑌) → (𝐺 ∈ (((𝐽 ↾t 𝑌) CnP 𝐽)‘𝐶) ↔ (𝐺:𝑌⟶ℂ ∧ (𝐺‘𝐶) ∈ (𝐺 limℂ 𝐶))))
133	64, 69, 132	syl2anc 583	. . . . . . . 8 ⊢ (𝜑 → (𝐺 ∈ (((𝐽 ↾t 𝑌) CnP 𝐽)‘𝐶) ↔ (𝐺:𝑌⟶ℂ ∧ (𝐺‘𝐶) ∈ (𝐺 limℂ 𝐶))))
134	131, 133	mpbid 232	. . . . . . 7 ⊢ (𝜑 → (𝐺:𝑌⟶ℂ ∧ (𝐺‘𝐶) ∈ (𝐺 limℂ 𝐶)))
135	134	simprd 495	. . . . . 6 ⊢ (𝜑 → (𝐺‘𝐶) ∈ (𝐺 limℂ 𝐶))
136		difss 4159	. . . . . . . . . 10 ⊢ ((𝑋 ∩ 𝑌) ∖ {𝐶}) ⊆ (𝑋 ∩ 𝑌)
137	136, 57	sstri 4018	. . . . . . . . 9 ⊢ ((𝑋 ∩ 𝑌) ∖ {𝐶}) ⊆ 𝑌
138	137	a1i 11	. . . . . . . 8 ⊢ (𝜑 → ((𝑋 ∩ 𝑌) ∖ {𝐶}) ⊆ 𝑌)
139		eqid 2740	. . . . . . . 8 ⊢ (𝐽 ↾t (𝑌 ∪ {𝐶})) = (𝐽 ↾t (𝑌 ∪ {𝐶}))
140		difssd 4160	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (∪ (𝐽 ↾t 𝑆) ∖ 𝑌) ⊆ ∪ (𝐽 ↾t 𝑆))
141	85, 140	unssd 4215	. . . . . . . . . . . . 13 ⊢ (𝜑 → ((𝑋 ∩ 𝑌) ∪ (∪ (𝐽 ↾t 𝑆) ∖ 𝑌)) ⊆ ∪ (𝐽 ↾t 𝑆))
142		ssun1 4201	. . . . . . . . . . . . . 14 ⊢ (𝑋 ∩ 𝑌) ⊆ ((𝑋 ∩ 𝑌) ∪ (∪ (𝐽 ↾t 𝑆) ∖ 𝑌))
143	142	a1i 11	. . . . . . . . . . . . 13 ⊢ (𝜑 → (𝑋 ∩ 𝑌) ⊆ ((𝑋 ∩ 𝑌) ∪ (∪ (𝐽 ↾t 𝑆) ∖ 𝑌)))
144	28	ntrss 23084	. . . . . . . . . . . . 13 ⊢ (((𝐽 ↾t 𝑆) ∈ Top ∧ ((𝑋 ∩ 𝑌) ∪ (∪ (𝐽 ↾t 𝑆) ∖ 𝑌)) ⊆ ∪ (𝐽 ↾t 𝑆) ∧ (𝑋 ∩ 𝑌) ⊆ ((𝑋 ∩ 𝑌) ∪ (∪ (𝐽 ↾t 𝑆) ∖ 𝑌))) → ((int‘(𝐽 ↾t 𝑆))‘(𝑋 ∩ 𝑌)) ⊆ ((int‘(𝐽 ↾t 𝑆))‘((𝑋 ∩ 𝑌) ∪ (∪ (𝐽 ↾t 𝑆) ∖ 𝑌))))
145	23, 141, 143, 144	syl3anc 1371	. . . . . . . . . . . 12 ⊢ (𝜑 → ((int‘(𝐽 ↾t 𝑆))‘(𝑋 ∩ 𝑌)) ⊆ ((int‘(𝐽 ↾t 𝑆))‘((𝑋 ∩ 𝑌) ∪ (∪ (𝐽 ↾t 𝑆) ∖ 𝑌))))
146	145, 31	sseldd 4009	. . . . . . . . . . 11 ⊢ (𝜑 → 𝐶 ∈ ((int‘(𝐽 ↾t 𝑆))‘((𝑋 ∩ 𝑌) ∪ (∪ (𝐽 ↾t 𝑆) ∖ 𝑌))))
147	146, 69	elind 4223	. . . . . . . . . 10 ⊢ (𝜑 → 𝐶 ∈ (((int‘(𝐽 ↾t 𝑆))‘((𝑋 ∩ 𝑌) ∪ (∪ (𝐽 ↾t 𝑆) ∖ 𝑌))) ∩ 𝑌))
148	57	a1i 11	. . . . . . . . . . . 12 ⊢ (𝜑 → (𝑋 ∩ 𝑌) ⊆ 𝑌)
149		eqid 2740	. . . . . . . . . . . . 13 ⊢ ((𝐽 ↾t 𝑆) ↾t 𝑌) = ((𝐽 ↾t 𝑆) ↾t 𝑌)
150	28, 149	restntr 23211	. . . . . . . . . . . 12 ⊢ (((𝐽 ↾t 𝑆) ∈ Top ∧ 𝑌 ⊆ ∪ (𝐽 ↾t 𝑆) ∧ (𝑋 ∩ 𝑌) ⊆ 𝑌) → ((int‘((𝐽 ↾t 𝑆) ↾t 𝑌))‘(𝑋 ∩ 𝑌)) = (((int‘(𝐽 ↾t 𝑆))‘((𝑋 ∩ 𝑌) ∪ (∪ (𝐽 ↾t 𝑆) ∖ 𝑌))) ∩ 𝑌))
151	23, 27, 148, 150	syl3anc 1371	. . . . . . . . . . 11 ⊢ (𝜑 → ((int‘((𝐽 ↾t 𝑆) ↾t 𝑌))‘(𝑋 ∩ 𝑌)) = (((int‘(𝐽 ↾t 𝑆))‘((𝑋 ∩ 𝑌) ∪ (∪ (𝐽 ↾t 𝑆) ∖ 𝑌))) ∩ 𝑌))
152		restabs 23194	. . . . . . . . . . . . . 14 ⊢ ((𝐽 ∈ Top ∧ 𝑌 ⊆ 𝑆 ∧ 𝑆 ∈ V) → ((𝐽 ↾t 𝑆) ↾t 𝑌) = (𝐽 ↾t 𝑌))
153	99, 14, 102, 152	syl3anc 1371	. . . . . . . . . . . . 13 ⊢ (𝜑 → ((𝐽 ↾t 𝑆) ↾t 𝑌) = (𝐽 ↾t 𝑌))
154	153	fveq2d 6924	. . . . . . . . . . . 12 ⊢ (𝜑 → (int‘((𝐽 ↾t 𝑆) ↾t 𝑌)) = (int‘(𝐽 ↾t 𝑌)))
155	154	fveq1d 6922	. . . . . . . . . . 11 ⊢ (𝜑 → ((int‘((𝐽 ↾t 𝑆) ↾t 𝑌))‘(𝑋 ∩ 𝑌)) = ((int‘(𝐽 ↾t 𝑌))‘(𝑋 ∩ 𝑌)))
156	151, 155	eqtr3d 2782	. . . . . . . . . 10 ⊢ (𝜑 → (((int‘(𝐽 ↾t 𝑆))‘((𝑋 ∩ 𝑌) ∪ (∪ (𝐽 ↾t 𝑆) ∖ 𝑌))) ∩ 𝑌) = ((int‘(𝐽 ↾t 𝑌))‘(𝑋 ∩ 𝑌)))
157	147, 156	eleqtrd 2846	. . . . . . . . 9 ⊢ (𝜑 → 𝐶 ∈ ((int‘(𝐽 ↾t 𝑌))‘(𝑋 ∩ 𝑌)))
158	69	snssd 4834	. . . . . . . . . . . . 13 ⊢ (𝜑 → {𝐶} ⊆ 𝑌)
159		ssequn2 4212	. . . . . . . . . . . . 13 ⊢ ({𝐶} ⊆ 𝑌 ↔ (𝑌 ∪ {𝐶}) = 𝑌)
160	158, 159	sylib 218	. . . . . . . . . . . 12 ⊢ (𝜑 → (𝑌 ∪ {𝐶}) = 𝑌)
161	160	oveq2d 7464	. . . . . . . . . . 11 ⊢ (𝜑 → (𝐽 ↾t (𝑌 ∪ {𝐶})) = (𝐽 ↾t 𝑌))
162	161	fveq2d 6924	. . . . . . . . . 10 ⊢ (𝜑 → (int‘(𝐽 ↾t (𝑌 ∪ {𝐶}))) = (int‘(𝐽 ↾t 𝑌)))
163	162, 121	fveq12d 6927	. . . . . . . . 9 ⊢ (𝜑 → ((int‘(𝐽 ↾t (𝑌 ∪ {𝐶})))‘(((𝑋 ∩ 𝑌) ∖ {𝐶}) ∪ {𝐶})) = ((int‘(𝐽 ↾t 𝑌))‘(𝑋 ∩ 𝑌)))
164	157, 163	eleqtrrd 2847	. . . . . . . 8 ⊢ (𝜑 → 𝐶 ∈ ((int‘(𝐽 ↾t (𝑌 ∪ {𝐶})))‘(((𝑋 ∩ 𝑌) ∖ {𝐶}) ∪ {𝐶})))
165	13, 138, 64, 3, 139, 164	limcres 25941	. . . . . . 7 ⊢ (𝜑 → ((𝐺 ↾ ((𝑋 ∩ 𝑌) ∖ {𝐶})) limℂ 𝐶) = (𝐺 limℂ 𝐶))
166	13, 138	feqresmpt 6991	. . . . . . . 8 ⊢ (𝜑 → (𝐺 ↾ ((𝑋 ∩ 𝑌) ∖ {𝐶})) = (𝑧 ∈ ((𝑋 ∩ 𝑌) ∖ {𝐶}) ↦ (𝐺‘𝑧)))
167	166	oveq1d 7463	. . . . . . 7 ⊢ (𝜑 → ((𝐺 ↾ ((𝑋 ∩ 𝑌) ∖ {𝐶})) limℂ 𝐶) = ((𝑧 ∈ ((𝑋 ∩ 𝑌) ∖ {𝐶}) ↦ (𝐺‘𝑧)) limℂ 𝐶))
168	165, 167	eqtr3d 2782	. . . . . 6 ⊢ (𝜑 → (𝐺 limℂ 𝐶) = ((𝑧 ∈ ((𝑋 ∩ 𝑌) ∖ {𝐶}) ↦ (𝐺‘𝑧)) limℂ 𝐶))
169	135, 168	eleqtrd 2846	. . . . 5 ⊢ (𝜑 → (𝐺‘𝐶) ∈ ((𝑧 ∈ ((𝑋 ∩ 𝑌) ∖ {𝐶}) ↦ (𝐺‘𝑧)) limℂ 𝐶))
170	3	mulcn 24908	. . . . . 6 ⊢ · ∈ ((𝐽 ×t 𝐽) Cn 𝐽)
171	5, 6, 7	dvcl 25954	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝐶(𝑆 D 𝐹)𝐾) → 𝐾 ∈ ℂ)
172	1, 171	mpdan 686	. . . . . . 7 ⊢ (𝜑 → 𝐾 ∈ ℂ)
173	13, 69	ffvelcdmd 7119	. . . . . . 7 ⊢ (𝜑 → (𝐺‘𝐶) ∈ ℂ)
174	172, 173	opelxpd 5739	. . . . . 6 ⊢ (𝜑 → ⟨𝐾, (𝐺‘𝐶)⟩ ∈ (ℂ × ℂ))
175	75	toponunii 22943	. . . . . . 7 ⊢ (ℂ × ℂ) = ∪ (𝐽 ×t 𝐽)
176	175	cncnpi 23307	. . . . . 6 ⊢ (( · ∈ ((𝐽 ×t 𝐽) Cn 𝐽) ∧ ⟨𝐾, (𝐺‘𝐶)⟩ ∈ (ℂ × ℂ)) → · ∈ (((𝐽 ×t 𝐽) CnP 𝐽)‘⟨𝐾, (𝐺‘𝐶)⟩))
177	170, 174, 176	sylancr 586	. . . . 5 ⊢ (𝜑 → · ∈ (((𝐽 ×t 𝐽) CnP 𝐽)‘⟨𝐾, (𝐺‘𝐶)⟩))
178	55, 59, 73, 73, 3, 76, 128, 169, 177	limccnp2 25947	. . . 4 ⊢ (𝜑 → (𝐾 · (𝐺‘𝐶)) ∈ ((𝑧 ∈ ((𝑋 ∩ 𝑌) ∖ {𝐶}) ↦ ((((𝐹‘𝑧) − (𝐹‘𝐶)) / (𝑧 − 𝐶)) · (𝐺‘𝑧))) limℂ 𝐶))
179	16	simprd 495	. . . . . 6 ⊢ (𝜑 → 𝐿 ∈ ((𝑧 ∈ (𝑌 ∖ {𝐶}) ↦ (((𝐺‘𝑧) − (𝐺‘𝐶)) / (𝑧 − 𝐶))) limℂ 𝐶))
180	70	fmpttd 7149	. . . . . . . 8 ⊢ (𝜑 → (𝑧 ∈ (𝑌 ∖ {𝐶}) ↦ (((𝐺‘𝑧) − (𝐺‘𝐶)) / (𝑧 − 𝐶))):(𝑌 ∖ {𝐶})⟶ℂ)
181	64	ssdifssd 4170	. . . . . . . 8 ⊢ (𝜑 → (𝑌 ∖ {𝐶}) ⊆ ℂ)
182		eqid 2740	. . . . . . . 8 ⊢ (𝐽 ↾t ((𝑌 ∖ {𝐶}) ∪ {𝐶})) = (𝐽 ↾t ((𝑌 ∖ {𝐶}) ∪ {𝐶}))
183		undif1 4499	. . . . . . . . . . . . 13 ⊢ ((𝑌 ∖ {𝐶}) ∪ {𝐶}) = (𝑌 ∪ {𝐶})
184	183, 160	eqtrid 2792	. . . . . . . . . . . 12 ⊢ (𝜑 → ((𝑌 ∖ {𝐶}) ∪ {𝐶}) = 𝑌)
185	184	oveq2d 7464	. . . . . . . . . . 11 ⊢ (𝜑 → (𝐽 ↾t ((𝑌 ∖ {𝐶}) ∪ {𝐶})) = (𝐽 ↾t 𝑌))
186	185	fveq2d 6924	. . . . . . . . . 10 ⊢ (𝜑 → (int‘(𝐽 ↾t ((𝑌 ∖ {𝐶}) ∪ {𝐶}))) = (int‘(𝐽 ↾t 𝑌)))
187	186, 121	fveq12d 6927	. . . . . . . . 9 ⊢ (𝜑 → ((int‘(𝐽 ↾t ((𝑌 ∖ {𝐶}) ∪ {𝐶})))‘(((𝑋 ∩ 𝑌) ∖ {𝐶}) ∪ {𝐶})) = ((int‘(𝐽 ↾t 𝑌))‘(𝑋 ∩ 𝑌)))
188	157, 187	eleqtrrd 2847	. . . . . . . 8 ⊢ (𝜑 → 𝐶 ∈ ((int‘(𝐽 ↾t ((𝑌 ∖ {𝐶}) ∪ {𝐶})))‘(((𝑋 ∩ 𝑌) ∖ {𝐶}) ∪ {𝐶})))
189	180, 62, 181, 3, 182, 188	limcres 25941	. . . . . . 7 ⊢ (𝜑 → (((𝑧 ∈ (𝑌 ∖ {𝐶}) ↦ (((𝐺‘𝑧) − (𝐺‘𝐶)) / (𝑧 − 𝐶))) ↾ ((𝑋 ∩ 𝑌) ∖ {𝐶})) limℂ 𝐶) = ((𝑧 ∈ (𝑌 ∖ {𝐶}) ↦ (((𝐺‘𝑧) − (𝐺‘𝐶)) / (𝑧 − 𝐶))) limℂ 𝐶))
190	62	resmptd 6069	. . . . . . . 8 ⊢ (𝜑 → ((𝑧 ∈ (𝑌 ∖ {𝐶}) ↦ (((𝐺‘𝑧) − (𝐺‘𝐶)) / (𝑧 − 𝐶))) ↾ ((𝑋 ∩ 𝑌) ∖ {𝐶})) = (𝑧 ∈ ((𝑋 ∩ 𝑌) ∖ {𝐶}) ↦ (((𝐺‘𝑧) − (𝐺‘𝐶)) / (𝑧 − 𝐶))))
191	190	oveq1d 7463	. . . . . . 7 ⊢ (𝜑 → (((𝑧 ∈ (𝑌 ∖ {𝐶}) ↦ (((𝐺‘𝑧) − (𝐺‘𝐶)) / (𝑧 − 𝐶))) ↾ ((𝑋 ∩ 𝑌) ∖ {𝐶})) limℂ 𝐶) = ((𝑧 ∈ ((𝑋 ∩ 𝑌) ∖ {𝐶}) ↦ (((𝐺‘𝑧) − (𝐺‘𝐶)) / (𝑧 − 𝐶))) limℂ 𝐶))
192	189, 191	eqtr3d 2782	. . . . . 6 ⊢ (𝜑 → ((𝑧 ∈ (𝑌 ∖ {𝐶}) ↦ (((𝐺‘𝑧) − (𝐺‘𝐶)) / (𝑧 − 𝐶))) limℂ 𝐶) = ((𝑧 ∈ ((𝑋 ∩ 𝑌) ∖ {𝐶}) ↦ (((𝐺‘𝑧) − (𝐺‘𝐶)) / (𝑧 − 𝐶))) limℂ 𝐶))
193	179, 192	eleqtrd 2846	. . . . 5 ⊢ (𝜑 → 𝐿 ∈ ((𝑧 ∈ ((𝑋 ∩ 𝑌) ∖ {𝐶}) ↦ (((𝐺‘𝑧) − (𝐺‘𝐶)) / (𝑧 − 𝐶))) limℂ 𝐶))
194	84, 5	sstrd 4019	. . . . . . . 8 ⊢ (𝜑 → (𝑋 ∩ 𝑌) ⊆ ℂ)
195		cncfmptc 24957	. . . . . . . 8 ⊢ (((𝐹‘𝐶) ∈ ℂ ∧ (𝑋 ∩ 𝑌) ⊆ ℂ ∧ ℂ ⊆ ℂ) → (𝑧 ∈ (𝑋 ∩ 𝑌) ↦ (𝐹‘𝐶)) ∈ ((𝑋 ∩ 𝑌)–cn→ℂ))
196	43, 194, 73, 195	syl3anc 1371	. . . . . . 7 ⊢ (𝜑 → (𝑧 ∈ (𝑋 ∩ 𝑌) ↦ (𝐹‘𝐶)) ∈ ((𝑋 ∩ 𝑌)–cn→ℂ))
197		eqidd 2741	. . . . . . 7 ⊢ (𝑧 = 𝐶 → (𝐹‘𝐶) = (𝐹‘𝐶))
198	196, 117, 197	cnmptlimc 25945	. . . . . 6 ⊢ (𝜑 → (𝐹‘𝐶) ∈ ((𝑧 ∈ (𝑋 ∩ 𝑌) ↦ (𝐹‘𝐶)) limℂ 𝐶))
199	43	adantr 480	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑧 ∈ (𝑋 ∩ 𝑌)) → (𝐹‘𝐶) ∈ ℂ)
200	199	fmpttd 7149	. . . . . . . 8 ⊢ (𝜑 → (𝑧 ∈ (𝑋 ∩ 𝑌) ↦ (𝐹‘𝐶)):(𝑋 ∩ 𝑌)⟶ℂ)
201	200	limcdif 25931	. . . . . . 7 ⊢ (𝜑 → ((𝑧 ∈ (𝑋 ∩ 𝑌) ↦ (𝐹‘𝐶)) limℂ 𝐶) = (((𝑧 ∈ (𝑋 ∩ 𝑌) ↦ (𝐹‘𝐶)) ↾ ((𝑋 ∩ 𝑌) ∖ {𝐶})) limℂ 𝐶))
202		resmpt 6066	. . . . . . . . 9 ⊢ (((𝑋 ∩ 𝑌) ∖ {𝐶}) ⊆ (𝑋 ∩ 𝑌) → ((𝑧 ∈ (𝑋 ∩ 𝑌) ↦ (𝐹‘𝐶)) ↾ ((𝑋 ∩ 𝑌) ∖ {𝐶})) = (𝑧 ∈ ((𝑋 ∩ 𝑌) ∖ {𝐶}) ↦ (𝐹‘𝐶)))
203	136, 202	mp1i 13	. . . . . . . 8 ⊢ (𝜑 → ((𝑧 ∈ (𝑋 ∩ 𝑌) ↦ (𝐹‘𝐶)) ↾ ((𝑋 ∩ 𝑌) ∖ {𝐶})) = (𝑧 ∈ ((𝑋 ∩ 𝑌) ∖ {𝐶}) ↦ (𝐹‘𝐶)))
204	203	oveq1d 7463	. . . . . . 7 ⊢ (𝜑 → (((𝑧 ∈ (𝑋 ∩ 𝑌) ↦ (𝐹‘𝐶)) ↾ ((𝑋 ∩ 𝑌) ∖ {𝐶})) limℂ 𝐶) = ((𝑧 ∈ ((𝑋 ∩ 𝑌) ∖ {𝐶}) ↦ (𝐹‘𝐶)) limℂ 𝐶))
205	201, 204	eqtrd 2780	. . . . . 6 ⊢ (𝜑 → ((𝑧 ∈ (𝑋 ∩ 𝑌) ↦ (𝐹‘𝐶)) limℂ 𝐶) = ((𝑧 ∈ ((𝑋 ∩ 𝑌) ∖ {𝐶}) ↦ (𝐹‘𝐶)) limℂ 𝐶))
206	198, 205	eleqtrd 2846	. . . . 5 ⊢ (𝜑 → (𝐹‘𝐶) ∈ ((𝑧 ∈ ((𝑋 ∩ 𝑌) ∖ {𝐶}) ↦ (𝐹‘𝐶)) limℂ 𝐶))
207	5, 13, 14	dvcl 25954	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝐶(𝑆 D 𝐺)𝐿) → 𝐿 ∈ ℂ)
208	11, 207	mpdan 686	. . . . . . 7 ⊢ (𝜑 → 𝐿 ∈ ℂ)
209	208, 43	opelxpd 5739	. . . . . 6 ⊢ (𝜑 → ⟨𝐿, (𝐹‘𝐶)⟩ ∈ (ℂ × ℂ))
210	175	cncnpi 23307	. . . . . 6 ⊢ (( · ∈ ((𝐽 ×t 𝐽) Cn 𝐽) ∧ ⟨𝐿, (𝐹‘𝐶)⟩ ∈ (ℂ × ℂ)) → · ∈ (((𝐽 ×t 𝐽) CnP 𝐽)‘⟨𝐿, (𝐹‘𝐶)⟩))
211	170, 209, 210	sylancr 586	. . . . 5 ⊢ (𝜑 → · ∈ (((𝐽 ×t 𝐽) CnP 𝐽)‘⟨𝐿, (𝐹‘𝐶)⟩))
212	71, 44, 73, 73, 3, 76, 193, 206, 211	limccnp2 25947	. . . 4 ⊢ (𝜑 → (𝐿 · (𝐹‘𝐶)) ∈ ((𝑧 ∈ ((𝑋 ∩ 𝑌) ∖ {𝐶}) ↦ ((((𝐺‘𝑧) − (𝐺‘𝐶)) / (𝑧 − 𝐶)) · (𝐹‘𝐶))) limℂ 𝐶))
213	3	addcn 24906	. . . . 5 ⊢ + ∈ ((𝐽 ×t 𝐽) Cn 𝐽)
214	172, 173	mulcld 11310	. . . . . 6 ⊢ (𝜑 → (𝐾 · (𝐺‘𝐶)) ∈ ℂ)
215	208, 43	mulcld 11310	. . . . . 6 ⊢ (𝜑 → (𝐿 · (𝐹‘𝐶)) ∈ ℂ)
216	214, 215	opelxpd 5739	. . . . 5 ⊢ (𝜑 → ⟨(𝐾 · (𝐺‘𝐶)), (𝐿 · (𝐹‘𝐶))⟩ ∈ (ℂ × ℂ))
217	175	cncnpi 23307	. . . . 5 ⊢ (( + ∈ ((𝐽 ×t 𝐽) Cn 𝐽) ∧ ⟨(𝐾 · (𝐺‘𝐶)), (𝐿 · (𝐹‘𝐶))⟩ ∈ (ℂ × ℂ)) → + ∈ (((𝐽 ×t 𝐽) CnP 𝐽)‘⟨(𝐾 · (𝐺‘𝐶)), (𝐿 · (𝐹‘𝐶))⟩))
218	213, 216, 217	sylancr 586	. . . 4 ⊢ (𝜑 → + ∈ (((𝐽 ×t 𝐽) CnP 𝐽)‘⟨(𝐾 · (𝐺‘𝐶)), (𝐿 · (𝐹‘𝐶))⟩))
219	60, 72, 73, 73, 3, 76, 178, 212, 218	limccnp2 25947	. . 3 ⊢ (𝜑 → ((𝐾 · (𝐺‘𝐶)) + (𝐿 · (𝐹‘𝐶))) ∈ ((𝑧 ∈ ((𝑋 ∩ 𝑌) ∖ {𝐶}) ↦ (((((𝐹‘𝑧) − (𝐹‘𝐶)) / (𝑧 − 𝐶)) · (𝐺‘𝑧)) + ((((𝐺‘𝑧) − (𝐺‘𝐶)) / (𝑧 − 𝐶)) · (𝐹‘𝐶)))) limℂ 𝐶))
220	42	adantr 480	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑧 ∈ ((𝑋 ∩ 𝑌) ∖ {𝐶})) → 𝐶 ∈ 𝑋)
221	32, 220	ffvelcdmd 7119	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑧 ∈ ((𝑋 ∩ 𝑌) ∖ {𝐶})) → (𝐹‘𝐶) ∈ ℂ)
222	37, 221	subcld 11647	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑧 ∈ ((𝑋 ∩ 𝑌) ∖ {𝐶})) → ((𝐹‘𝑧) − (𝐹‘𝐶)) ∈ ℂ)
223	222, 59	mulcld 11310	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑧 ∈ ((𝑋 ∩ 𝑌) ∖ {𝐶})) → (((𝐹‘𝑧) − (𝐹‘𝐶)) · (𝐺‘𝑧)) ∈ ℂ)
224	69	adantr 480	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑧 ∈ ((𝑋 ∩ 𝑌) ∖ {𝐶})) → 𝐶 ∈ 𝑌)
225	56, 224	ffvelcdmd 7119	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑧 ∈ ((𝑋 ∩ 𝑌) ∖ {𝐶})) → (𝐺‘𝐶) ∈ ℂ)
226	59, 225	subcld 11647	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑧 ∈ ((𝑋 ∩ 𝑌) ∖ {𝐶})) → ((𝐺‘𝑧) − (𝐺‘𝐶)) ∈ ℂ)
227	226, 221	mulcld 11310	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑧 ∈ ((𝑋 ∩ 𝑌) ∖ {𝐶})) → (((𝐺‘𝑧) − (𝐺‘𝐶)) · (𝐹‘𝐶)) ∈ ℂ)
228	47, 220	sseldd 4009	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑧 ∈ ((𝑋 ∩ 𝑌) ∖ {𝐶})) → 𝐶 ∈ ℂ)
229	48, 228	subcld 11647	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑧 ∈ ((𝑋 ∩ 𝑌) ∖ {𝐶})) → (𝑧 − 𝐶) ∈ ℂ)
230	223, 227, 229, 54	divdird 12108	. . . . . 6 ⊢ ((𝜑 ∧ 𝑧 ∈ ((𝑋 ∩ 𝑌) ∖ {𝐶})) → (((((𝐹‘𝑧) − (𝐹‘𝐶)) · (𝐺‘𝑧)) + (((𝐺‘𝑧) − (𝐺‘𝐶)) · (𝐹‘𝐶))) / (𝑧 − 𝐶)) = (((((𝐹‘𝑧) − (𝐹‘𝐶)) · (𝐺‘𝑧)) / (𝑧 − 𝐶)) + ((((𝐺‘𝑧) − (𝐺‘𝐶)) · (𝐹‘𝐶)) / (𝑧 − 𝐶))))
231	37, 59	mulcld 11310	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑧 ∈ ((𝑋 ∩ 𝑌) ∖ {𝐶})) → ((𝐹‘𝑧) · (𝐺‘𝑧)) ∈ ℂ)
232	221, 59	mulcld 11310	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑧 ∈ ((𝑋 ∩ 𝑌) ∖ {𝐶})) → ((𝐹‘𝐶) · (𝐺‘𝑧)) ∈ ℂ)
233	221, 225	mulcld 11310	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑧 ∈ ((𝑋 ∩ 𝑌) ∖ {𝐶})) → ((𝐹‘𝐶) · (𝐺‘𝐶)) ∈ ℂ)
234	231, 232, 233	npncand 11671	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑧 ∈ ((𝑋 ∩ 𝑌) ∖ {𝐶})) → ((((𝐹‘𝑧) · (𝐺‘𝑧)) − ((𝐹‘𝐶) · (𝐺‘𝑧))) + (((𝐹‘𝐶) · (𝐺‘𝑧)) − ((𝐹‘𝐶) · (𝐺‘𝐶)))) = (((𝐹‘𝑧) · (𝐺‘𝑧)) − ((𝐹‘𝐶) · (𝐺‘𝐶))))
235	37, 221, 59	subdird 11747	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑧 ∈ ((𝑋 ∩ 𝑌) ∖ {𝐶})) → (((𝐹‘𝑧) − (𝐹‘𝐶)) · (𝐺‘𝑧)) = (((𝐹‘𝑧) · (𝐺‘𝑧)) − ((𝐹‘𝐶) · (𝐺‘𝑧))))
236	226, 221	mulcomd 11311	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑧 ∈ ((𝑋 ∩ 𝑌) ∖ {𝐶})) → (((𝐺‘𝑧) − (𝐺‘𝐶)) · (𝐹‘𝐶)) = ((𝐹‘𝐶) · ((𝐺‘𝑧) − (𝐺‘𝐶))))
237	221, 59, 225	subdid 11746	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑧 ∈ ((𝑋 ∩ 𝑌) ∖ {𝐶})) → ((𝐹‘𝐶) · ((𝐺‘𝑧) − (𝐺‘𝐶))) = (((𝐹‘𝐶) · (𝐺‘𝑧)) − ((𝐹‘𝐶) · (𝐺‘𝐶))))
238	236, 237	eqtrd 2780	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑧 ∈ ((𝑋 ∩ 𝑌) ∖ {𝐶})) → (((𝐺‘𝑧) − (𝐺‘𝐶)) · (𝐹‘𝐶)) = (((𝐹‘𝐶) · (𝐺‘𝑧)) − ((𝐹‘𝐶) · (𝐺‘𝐶))))
239	235, 238	oveq12d 7466	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑧 ∈ ((𝑋 ∩ 𝑌) ∖ {𝐶})) → ((((𝐹‘𝑧) − (𝐹‘𝐶)) · (𝐺‘𝑧)) + (((𝐺‘𝑧) − (𝐺‘𝐶)) · (𝐹‘𝐶))) = ((((𝐹‘𝑧) · (𝐺‘𝑧)) − ((𝐹‘𝐶) · (𝐺‘𝑧))) + (((𝐹‘𝐶) · (𝐺‘𝑧)) − ((𝐹‘𝐶) · (𝐺‘𝐶)))))
240	6	ffnd 6748	. . . . . . . . . . . 12 ⊢ (𝜑 → 𝐹 Fn 𝑋)
241	240	adantr 480	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑧 ∈ ((𝑋 ∩ 𝑌) ∖ {𝐶})) → 𝐹 Fn 𝑋)
242	13	ffnd 6748	. . . . . . . . . . . 12 ⊢ (𝜑 → 𝐺 Fn 𝑌)
243	242	adantr 480	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑧 ∈ ((𝑋 ∩ 𝑌) ∖ {𝐶})) → 𝐺 Fn 𝑌)
244		ssexg 5341	. . . . . . . . . . . . 13 ⊢ ((𝑋 ⊆ ℂ ∧ ℂ ∈ V) → 𝑋 ∈ V)
245	46, 100, 244	sylancl 585	. . . . . . . . . . . 12 ⊢ (𝜑 → 𝑋 ∈ V)
246	245	adantr 480	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑧 ∈ ((𝑋 ∩ 𝑌) ∖ {𝐶})) → 𝑋 ∈ V)
247		ssexg 5341	. . . . . . . . . . . . 13 ⊢ ((𝑌 ⊆ ℂ ∧ ℂ ∈ V) → 𝑌 ∈ V)
248	64, 100, 247	sylancl 585	. . . . . . . . . . . 12 ⊢ (𝜑 → 𝑌 ∈ V)
249	248	adantr 480	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑧 ∈ ((𝑋 ∩ 𝑌) ∖ {𝐶})) → 𝑌 ∈ V)
250		eqid 2740	. . . . . . . . . . 11 ⊢ (𝑋 ∩ 𝑌) = (𝑋 ∩ 𝑌)
251		eqidd 2741	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑧 ∈ ((𝑋 ∩ 𝑌) ∖ {𝐶})) ∧ 𝑧 ∈ 𝑋) → (𝐹‘𝑧) = (𝐹‘𝑧))
252		eqidd 2741	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑧 ∈ ((𝑋 ∩ 𝑌) ∖ {𝐶})) ∧ 𝑧 ∈ 𝑌) → (𝐺‘𝑧) = (𝐺‘𝑧))
253	241, 243, 246, 249, 250, 251, 252	ofval 7725	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑧 ∈ ((𝑋 ∩ 𝑌) ∖ {𝐶})) ∧ 𝑧 ∈ (𝑋 ∩ 𝑌)) → ((𝐹 ∘f · 𝐺)‘𝑧) = ((𝐹‘𝑧) · (𝐺‘𝑧)))
254	35, 253	mpdan 686	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑧 ∈ ((𝑋 ∩ 𝑌) ∖ {𝐶})) → ((𝐹 ∘f · 𝐺)‘𝑧) = ((𝐹‘𝑧) · (𝐺‘𝑧)))
255		eqidd 2741	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑧 ∈ ((𝑋 ∩ 𝑌) ∖ {𝐶})) ∧ 𝐶 ∈ 𝑋) → (𝐹‘𝐶) = (𝐹‘𝐶))
256		eqidd 2741	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑧 ∈ ((𝑋 ∩ 𝑌) ∖ {𝐶})) ∧ 𝐶 ∈ 𝑌) → (𝐺‘𝐶) = (𝐺‘𝐶))
257	241, 243, 246, 249, 250, 255, 256	ofval 7725	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑧 ∈ ((𝑋 ∩ 𝑌) ∖ {𝐶})) ∧ 𝐶 ∈ (𝑋 ∩ 𝑌)) → ((𝐹 ∘f · 𝐺)‘𝐶) = ((𝐹‘𝐶) · (𝐺‘𝐶)))
258	117, 257	mpidan 688	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑧 ∈ ((𝑋 ∩ 𝑌) ∖ {𝐶})) → ((𝐹 ∘f · 𝐺)‘𝐶) = ((𝐹‘𝐶) · (𝐺‘𝐶)))
259	254, 258	oveq12d 7466	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑧 ∈ ((𝑋 ∩ 𝑌) ∖ {𝐶})) → (((𝐹 ∘f · 𝐺)‘𝑧) − ((𝐹 ∘f · 𝐺)‘𝐶)) = (((𝐹‘𝑧) · (𝐺‘𝑧)) − ((𝐹‘𝐶) · (𝐺‘𝐶))))
260	234, 239, 259	3eqtr4d 2790	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑧 ∈ ((𝑋 ∩ 𝑌) ∖ {𝐶})) → ((((𝐹‘𝑧) − (𝐹‘𝐶)) · (𝐺‘𝑧)) + (((𝐺‘𝑧) − (𝐺‘𝐶)) · (𝐹‘𝐶))) = (((𝐹 ∘f · 𝐺)‘𝑧) − ((𝐹 ∘f · 𝐺)‘𝐶)))
261	260	oveq1d 7463	. . . . . 6 ⊢ ((𝜑 ∧ 𝑧 ∈ ((𝑋 ∩ 𝑌) ∖ {𝐶})) → (((((𝐹‘𝑧) − (𝐹‘𝐶)) · (𝐺‘𝑧)) + (((𝐺‘𝑧) − (𝐺‘𝐶)) · (𝐹‘𝐶))) / (𝑧 − 𝐶)) = ((((𝐹 ∘f · 𝐺)‘𝑧) − ((𝐹 ∘f · 𝐺)‘𝐶)) / (𝑧 − 𝐶)))
262	222, 59, 229, 54	div23d 12107	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑧 ∈ ((𝑋 ∩ 𝑌) ∖ {𝐶})) → ((((𝐹‘𝑧) − (𝐹‘𝐶)) · (𝐺‘𝑧)) / (𝑧 − 𝐶)) = ((((𝐹‘𝑧) − (𝐹‘𝐶)) / (𝑧 − 𝐶)) · (𝐺‘𝑧)))
263	226, 221, 229, 54	div23d 12107	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑧 ∈ ((𝑋 ∩ 𝑌) ∖ {𝐶})) → ((((𝐺‘𝑧) − (𝐺‘𝐶)) · (𝐹‘𝐶)) / (𝑧 − 𝐶)) = ((((𝐺‘𝑧) − (𝐺‘𝐶)) / (𝑧 − 𝐶)) · (𝐹‘𝐶)))
264	262, 263	oveq12d 7466	. . . . . 6 ⊢ ((𝜑 ∧ 𝑧 ∈ ((𝑋 ∩ 𝑌) ∖ {𝐶})) → (((((𝐹‘𝑧) − (𝐹‘𝐶)) · (𝐺‘𝑧)) / (𝑧 − 𝐶)) + ((((𝐺‘𝑧) − (𝐺‘𝐶)) · (𝐹‘𝐶)) / (𝑧 − 𝐶))) = (((((𝐹‘𝑧) − (𝐹‘𝐶)) / (𝑧 − 𝐶)) · (𝐺‘𝑧)) + ((((𝐺‘𝑧) − (𝐺‘𝐶)) / (𝑧 − 𝐶)) · (𝐹‘𝐶))))
265	230, 261, 264	3eqtr3d 2788	. . . . 5 ⊢ ((𝜑 ∧ 𝑧 ∈ ((𝑋 ∩ 𝑌) ∖ {𝐶})) → ((((𝐹 ∘f · 𝐺)‘𝑧) − ((𝐹 ∘f · 𝐺)‘𝐶)) / (𝑧 − 𝐶)) = (((((𝐹‘𝑧) − (𝐹‘𝐶)) / (𝑧 − 𝐶)) · (𝐺‘𝑧)) + ((((𝐺‘𝑧) − (𝐺‘𝐶)) / (𝑧 − 𝐶)) · (𝐹‘𝐶))))
266	265	mpteq2dva 5266	. . . 4 ⊢ (𝜑 → (𝑧 ∈ ((𝑋 ∩ 𝑌) ∖ {𝐶}) ↦ ((((𝐹 ∘f · 𝐺)‘𝑧) − ((𝐹 ∘f · 𝐺)‘𝐶)) / (𝑧 − 𝐶))) = (𝑧 ∈ ((𝑋 ∩ 𝑌) ∖ {𝐶}) ↦ (((((𝐹‘𝑧) − (𝐹‘𝐶)) / (𝑧 − 𝐶)) · (𝐺‘𝑧)) + ((((𝐺‘𝑧) − (𝐺‘𝐶)) / (𝑧 − 𝐶)) · (𝐹‘𝐶)))))
267	266	oveq1d 7463	. . 3 ⊢ (𝜑 → ((𝑧 ∈ ((𝑋 ∩ 𝑌) ∖ {𝐶}) ↦ ((((𝐹 ∘f · 𝐺)‘𝑧) − ((𝐹 ∘f · 𝐺)‘𝐶)) / (𝑧 − 𝐶))) limℂ 𝐶) = ((𝑧 ∈ ((𝑋 ∩ 𝑌) ∖ {𝐶}) ↦ (((((𝐹‘𝑧) − (𝐹‘𝐶)) / (𝑧 − 𝐶)) · (𝐺‘𝑧)) + ((((𝐺‘𝑧) − (𝐺‘𝐶)) / (𝑧 − 𝐶)) · (𝐹‘𝐶)))) limℂ 𝐶))
268	219, 267	eleqtrrd 2847	. 2 ⊢ (𝜑 → ((𝐾 · (𝐺‘𝐶)) + (𝐿 · (𝐹‘𝐶))) ∈ ((𝑧 ∈ ((𝑋 ∩ 𝑌) ∖ {𝐶}) ↦ ((((𝐹 ∘f · 𝐺)‘𝑧) − ((𝐹 ∘f · 𝐺)‘𝐶)) / (𝑧 − 𝐶))) limℂ 𝐶))
269		eqid 2740	. . 3 ⊢ (𝑧 ∈ ((𝑋 ∩ 𝑌) ∖ {𝐶}) ↦ ((((𝐹 ∘f · 𝐺)‘𝑧) − ((𝐹 ∘f · 𝐺)‘𝐶)) / (𝑧 − 𝐶))) = (𝑧 ∈ ((𝑋 ∩ 𝑌) ∖ {𝐶}) ↦ ((((𝐹 ∘f · 𝐺)‘𝑧) − ((𝐹 ∘f · 𝐺)‘𝐶)) / (𝑧 − 𝐶)))
270		mulcl 11268	. . . . 5 ⊢ ((𝑥 ∈ ℂ ∧ 𝑦 ∈ ℂ) → (𝑥 · 𝑦) ∈ ℂ)
271	270	adantl 481	. . . 4 ⊢ ((𝜑 ∧ (𝑥 ∈ ℂ ∧ 𝑦 ∈ ℂ)) → (𝑥 · 𝑦) ∈ ℂ)
272	271, 6, 13, 245, 248, 250	off 7732	. . 3 ⊢ (𝜑 → (𝐹 ∘f · 𝐺):(𝑋 ∩ 𝑌)⟶ℂ)
273	2, 3, 269, 5, 272, 84	eldv 25953	. 2 ⊢ (𝜑 → (𝐶(𝑆 D (𝐹 ∘f · 𝐺))((𝐾 · (𝐺‘𝐶)) + (𝐿 · (𝐹‘𝐶))) ↔ (𝐶 ∈ ((int‘(𝐽 ↾t 𝑆))‘(𝑋 ∩ 𝑌)) ∧ ((𝐾 · (𝐺‘𝐶)) + (𝐿 · (𝐹‘𝐶))) ∈ ((𝑧 ∈ ((𝑋 ∩ 𝑌) ∖ {𝐶}) ↦ ((((𝐹 ∘f · 𝐺)‘𝑧) − ((𝐹 ∘f · 𝐺)‘𝐶)) / (𝑧 − 𝐶))) limℂ 𝐶))))
274	31, 268, 273	mpbir2and 712	1 ⊢ (𝜑 → 𝐶(𝑆 D (𝐹 ∘f · 𝐺))((𝐾 · (𝐺‘𝐶)) + (𝐿 · (𝐹‘𝐶))))

Syntax hints:   → wi 4   ↔ wb 206   ∧ wa 395   = wceq 1537   ∈ wcel 2108   ≠ wne 2946  Vcvv 3488   ∖ cdif 3973   ∪ cun 3974   ∩ cin 3975   ⊆ wss 3976  {csn 4648  ⟨cop 4654  ∪ cuni 4931   class class class wbr 5166   ↦ cmpt 5249   × cxp 5698  dom cdm 5700   ↾ cres 5702  Rel wrel 5705   Fn wfn 6568  ⟶wf 6569  ‘cfv 6573  (class class class)co 7448   ∘_f cof 7712  ℂcc 11182   + caddc 11187   · cmul 11189   − cmin 11520   / cdiv 11947   ↾_t crest 17480  TopOpenctopn 17481  ℂ_fldccnfld 21387  Topctop 22920  TopOnctopon 22937  intcnt 23046   Cn ccn 23253   CnP ccnp 23254   ×_t ctx 23589  –cn→ccncf 24921   lim_ℂ climc 25917   D cdv 25918

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-10 2141  ax-11 2158  ax-12 2178  ax-ext 2711  ax-rep 5303  ax-sep 5317  ax-nul 5324  ax-pow 5383  ax-pr 5447  ax-un 7770  ax-cnex 11240  ax-resscn 11241  ax-1cn 11242  ax-icn 11243  ax-addcl 11244  ax-addrcl 11245  ax-mulcl 11246  ax-mulrcl 11247  ax-mulcom 11248  ax-addass 11249  ax-mulass 11250  ax-distr 11251  ax-i2m1 11252  ax-1ne0 11253  ax-1rid 11254  ax-rnegex 11255  ax-rrecex 11256  ax-cnre 11257  ax-pre-lttri 11258  ax-pre-lttrn 11259  ax-pre-ltadd 11260  ax-pre-mulgt0 11261  ax-pre-sup 11262  ax-addf 11263  ax-mulf 11264

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 847  df-3or 1088  df-3an 1089  df-tru 1540  df-fal 1550  df-ex 1778  df-nf 1782  df-sb 2065  df-mo 2543  df-eu 2572  df-clab 2718  df-cleq 2732  df-clel 2819  df-nfc 2895  df-ne 2947  df-nel 3053  df-ral 3068  df-rex 3077  df-rmo 3388  df-reu 3389  df-rab 3444  df-v 3490  df-sbc 3805  df-csb 3922  df-dif 3979  df-un 3981  df-in 3983  df-ss 3993  df-pss 3996  df-nul 4353  df-if 4549  df-pw 4624  df-sn 4649  df-pr 4651  df-tp 4653  df-op 4655  df-uni 4932  df-int 4971  df-iun 5017  df-iin 5018  df-br 5167  df-opab 5229  df-mpt 5250  df-tr 5284  df-id 5593  df-eprel 5599  df-po 5607  df-so 5608  df-fr 5652  df-se 5653  df-we 5654  df-xp 5706  df-rel 5707  df-cnv 5708  df-co 5709  df-dm 5710  df-rn 5711  df-res 5712  df-ima 5713  df-pred 6332  df-ord 6398  df-on 6399  df-lim 6400  df-suc 6401  df-iota 6525  df-fun 6575  df-fn 6576  df-f 6577  df-f1 6578  df-fo 6579  df-f1o 6580  df-fv 6581  df-isom 6582  df-riota 7404  df-ov 7451  df-oprab 7452  df-mpo 7453  df-of 7714  df-om 7904  df-1st 8030  df-2nd 8031  df-supp 8202  df-frecs 8322  df-wrecs 8353  df-recs 8427  df-rdg 8466  df-1o 8522  df-2o 8523  df-er 8763  df-map 8886  df-pm 8887  df-ixp 8956  df-en 9004  df-dom 9005  df-sdom 9006  df-fin 9007  df-fsupp 9432  df-fi 9480  df-sup 9511  df-inf 9512  df-oi 9579  df-card 10008  df-pnf 11326  df-mnf 11327  df-xr 11328  df-ltxr 11329  df-le 11330  df-sub 11522  df-neg 11523  df-div 11948  df-nn 12294  df-2 12356  df-3 12357  df-4 12358  df-5 12359  df-6 12360  df-7 12361  df-8 12362  df-9 12363  df-n0 12554  df-z 12640  df-dec 12759  df-uz 12904  df-q 13014  df-rp 13058  df-xneg 13175  df-xadd 13176  df-xmul 13177  df-icc 13414  df-fz 13568  df-fzo 13712  df-seq 14053  df-exp 14113  df-hash 14380  df-cj 15148  df-re 15149  df-im 15150  df-sqrt 15284  df-abs 15285  df-struct 17194  df-sets 17211  df-slot 17229  df-ndx 17241  df-base 17259  df-ress 17288  df-plusg 17324  df-mulr 17325  df-starv 17326  df-sca 17327  df-vsca 17328  df-ip 17329  df-tset 17330  df-ple 17331  df-ds 17333  df-unif 17334  df-hom 17335  df-cco 17336  df-rest 17482  df-topn 17483  df-0g 17501  df-gsum 17502  df-topgen 17503  df-pt 17504  df-prds 17507  df-xrs 17562  df-qtop 17567  df-imas 17568  df-xps 17570  df-mre 17644  df-mrc 17645  df-acs 17647  df-mgm 18678  df-sgrp 18757  df-mnd 18773  df-submnd 18819  df-mulg 19108  df-cntz 19357  df-cmn 19824  df-psmet 21379  df-xmet 21380  df-met 21381  df-bl 21382  df-mopn 21383  df-cnfld 21388  df-top 22921  df-topon 22938  df-topsp 22960  df-bases 22974  df-cld 23048  df-ntr 23049  df-cls 23050  df-cn 23256  df-cnp 23257  df-tx 23591  df-hmeo 23784  df-xms 24351  df-ms 24352  df-tms 24353  df-cncf 24923  df-limc 25921  df-dv 25922

This theorem is referenced by: (None)