dvmulbr - Metamath Proof Explorer

	Metamath Proof Explorer		< Previous Next > Nearby theorems
Mirrors > Home > MPE Home > Th. List > dvmulbr		Structured version Visualization version GIF version

Theorem dvmulbr 25791

Description: The product rule for derivatives at a point. For the (simpler but more limited) function version, see dvmul 25794. (Contributed by Mario Carneiro, 9-Aug-2014.) (Revised by Mario Carneiro, 28-Dec-2016.) Avoid ax-mulf 11186 and remove unnecessary hypotheses. (Revised by GG, 16-Mar-2025.)

**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
dvmulbr	⊢ (𝜑 → 𝐶(𝑆 D (𝐹 ∘_f · 𝐺))((𝐾 · (𝐺‘𝐶)) + (𝐿 · (𝐹‘𝐶))))

Proof of Theorem dvmulbr Dummy variables 𝑦 𝑧 𝑥 𝑢 𝑣 𝑤 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		dvadd.bf	. . . . . 6 ⊢ (𝜑 → 𝐶(𝑆 D 𝐹)𝐾)
2		eqid 2724	. . . . . . 7 ⊢ (𝐽 ↾_t 𝑆) = (𝐽 ↾_t 𝑆)
3		dvadd.j	. . . . . . 7 ⊢ 𝐽 = (TopOpen‘ℂ_fld)
4		eqid 2724	. . . . . . 7 ⊢ (𝑧 ∈ (𝑋 ∖ {𝐶}) ↦ (((𝐹‘𝑧) − (𝐹‘𝐶)) / (𝑧 − 𝐶))) = (𝑧 ∈ (𝑋 ∖ {𝐶}) ↦ (((𝐹‘𝑧) − (𝐹‘𝐶)) / (𝑧 − 𝐶)))
5		dvaddbr.s	. . . . . . 7 ⊢ (𝜑 → 𝑆 ⊆ ℂ)
6		dvadd.f	. . . . . . 7 ⊢ (𝜑 → 𝐹:𝑋⟶ℂ)
7		dvadd.x	. . . . . . 7 ⊢ (𝜑 → 𝑋 ⊆ 𝑆)
8	2, 3, 4, 5, 6, 7	eldv 25749	. . . . . 6 ⊢ (𝜑 → (𝐶(𝑆 D 𝐹)𝐾 ↔ (𝐶 ∈ ((int‘(𝐽 ↾_t 𝑆))‘𝑋) ∧ 𝐾 ∈ ((𝑧 ∈ (𝑋 ∖ {𝐶}) ↦ (((𝐹‘𝑧) − (𝐹‘𝐶)) / (𝑧 − 𝐶))) lim_ℂ 𝐶))))
9	1, 8	mpbid 231	. . . . 5 ⊢ (𝜑 → (𝐶 ∈ ((int‘(𝐽 ↾_t 𝑆))‘𝑋) ∧ 𝐾 ∈ ((𝑧 ∈ (𝑋 ∖ {𝐶}) ↦ (((𝐹‘𝑧) − (𝐹‘𝐶)) / (𝑧 − 𝐶))) lim_ℂ 𝐶)))
10	9	simpld 494	. . . 4 ⊢ (𝜑 → 𝐶 ∈ ((int‘(𝐽 ↾_t 𝑆))‘𝑋))
11		dvadd.bg	. . . . . 6 ⊢ (𝜑 → 𝐶(𝑆 D 𝐺)𝐿)
12		eqid 2724	. . . . . . 7 ⊢ (𝑧 ∈ (𝑌 ∖ {𝐶}) ↦ (((𝐺‘𝑧) − (𝐺‘𝐶)) / (𝑧 − 𝐶))) = (𝑧 ∈ (𝑌 ∖ {𝐶}) ↦ (((𝐺‘𝑧) − (𝐺‘𝐶)) / (𝑧 − 𝐶)))
13		dvadd.g	. . . . . . 7 ⊢ (𝜑 → 𝐺:𝑌⟶ℂ)
14		dvadd.y	. . . . . . 7 ⊢ (𝜑 → 𝑌 ⊆ 𝑆)
15	2, 3, 12, 5, 13, 14	eldv 25749	. . . . . 6 ⊢ (𝜑 → (𝐶(𝑆 D 𝐺)𝐿 ↔ (𝐶 ∈ ((int‘(𝐽 ↾_t 𝑆))‘𝑌) ∧ 𝐿 ∈ ((𝑧 ∈ (𝑌 ∖ {𝐶}) ↦ (((𝐺‘𝑧) − (𝐺‘𝐶)) / (𝑧 − 𝐶))) lim_ℂ 𝐶))))
16	11, 15	mpbid 231	. . . . 5 ⊢ (𝜑 → (𝐶 ∈ ((int‘(𝐽 ↾_t 𝑆))‘𝑌) ∧ 𝐿 ∈ ((𝑧 ∈ (𝑌 ∖ {𝐶}) ↦ (((𝐺‘𝑧) − (𝐺‘𝐶)) / (𝑧 − 𝐶))) lim_ℂ 𝐶)))
17	16	simpld 494	. . . 4 ⊢ (𝜑 → 𝐶 ∈ ((int‘(𝐽 ↾_t 𝑆))‘𝑌))
18	10, 17	elind 4186	. . 3 ⊢ (𝜑 → 𝐶 ∈ (((int‘(𝐽 ↾_t 𝑆))‘𝑋) ∩ ((int‘(𝐽 ↾_t 𝑆))‘𝑌)))
19	3	cnfldtopon 24621	. . . . . 6 ⊢ 𝐽 ∈ (TopOn‘ℂ)
20		resttopon 22987	. . . . . 6 ⊢ ((𝐽 ∈ (TopOn‘ℂ) ∧ 𝑆 ⊆ ℂ) → (𝐽 ↾_t 𝑆) ∈ (TopOn‘𝑆))
21	19, 5, 20	sylancr 586	. . . . 5 ⊢ (𝜑 → (𝐽 ↾_t 𝑆) ∈ (TopOn‘𝑆))
22		topontop 22737	. . . . 5 ⊢ ((𝐽 ↾_t 𝑆) ∈ (TopOn‘𝑆) → (𝐽 ↾_t 𝑆) ∈ Top)
23	21, 22	syl 17	. . . 4 ⊢ (𝜑 → (𝐽 ↾_t 𝑆) ∈ Top)
24		toponuni 22738	. . . . . 6 ⊢ ((𝐽 ↾_t 𝑆) ∈ (TopOn‘𝑆) → 𝑆 = ∪ (𝐽 ↾_t 𝑆))
25	21, 24	syl 17	. . . . 5 ⊢ (𝜑 → 𝑆 = ∪ (𝐽 ↾_t 𝑆))
26	7, 25	sseqtrd 4014	. . . 4 ⊢ (𝜑 → 𝑋 ⊆ ∪ (𝐽 ↾_t 𝑆))
27	14, 25	sseqtrd 4014	. . . 4 ⊢ (𝜑 → 𝑌 ⊆ ∪ (𝐽 ↾_t 𝑆))
28		eqid 2724	. . . . 5 ⊢ ∪ (𝐽 ↾_t 𝑆) = ∪ (𝐽 ↾_t 𝑆)
29	28	ntrin 22887	. . . 4 ⊢ (((𝐽 ↾_t 𝑆) ∈ Top ∧ 𝑋 ⊆ ∪ (𝐽 ↾_t 𝑆) ∧ 𝑌 ⊆ ∪ (𝐽 ↾_t 𝑆)) → ((int‘(𝐽 ↾_t 𝑆))‘(𝑋 ∩ 𝑌)) = (((int‘(𝐽 ↾_t 𝑆))‘𝑋) ∩ ((int‘(𝐽 ↾_t 𝑆))‘𝑌)))
30	23, 26, 27, 29	syl3anc 1368	. . 3 ⊢ (𝜑 → ((int‘(𝐽 ↾_t 𝑆))‘(𝑋 ∩ 𝑌)) = (((int‘(𝐽 ↾_t 𝑆))‘𝑋) ∩ ((int‘(𝐽 ↾_t 𝑆))‘𝑌)))
31	18, 30	eleqtrrd 2828	. 2 ⊢ (𝜑 → 𝐶 ∈ ((int‘(𝐽 ↾_t 𝑆))‘(𝑋 ∩ 𝑌)))
32	6	adantr 480	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑧 ∈ ((𝑋 ∩ 𝑌) ∖ {𝐶})) → 𝐹:𝑋⟶ℂ)
33		inss1 4220	. . . . . . . . 9 ⊢ (𝑋 ∩ 𝑌) ⊆ 𝑋
34		eldifi 4118	. . . . . . . . . 10 ⊢ (𝑧 ∈ ((𝑋 ∩ 𝑌) ∖ {𝐶}) → 𝑧 ∈ (𝑋 ∩ 𝑌))
35	34	adantl 481	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑧 ∈ ((𝑋 ∩ 𝑌) ∖ {𝐶})) → 𝑧 ∈ (𝑋 ∩ 𝑌))
36	33, 35	sselid 3972	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑧 ∈ ((𝑋 ∩ 𝑌) ∖ {𝐶})) → 𝑧 ∈ 𝑋)
37	32, 36	ffvelcdmd 7077	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑧 ∈ ((𝑋 ∩ 𝑌) ∖ {𝐶})) → (𝐹‘𝑧) ∈ ℂ)
38	5, 6, 7	dvbss 25752	. . . . . . . . . 10 ⊢ (𝜑 → dom (𝑆 D 𝐹) ⊆ 𝑋)
39		reldv 25721	. . . . . . . . . . 11 ⊢ Rel (𝑆 D 𝐹)
40		releldm 5933	. . . . . . . . . . 11 ⊢ ((Rel (𝑆 D 𝐹) ∧ 𝐶(𝑆 D 𝐹)𝐾) → 𝐶 ∈ dom (𝑆 D 𝐹))
41	39, 1, 40	sylancr 586	. . . . . . . . . 10 ⊢ (𝜑 → 𝐶 ∈ dom (𝑆 D 𝐹))
42	38, 41	sseldd 3975	. . . . . . . . 9 ⊢ (𝜑 → 𝐶 ∈ 𝑋)
43	6, 42	ffvelcdmd 7077	. . . . . . . 8 ⊢ (𝜑 → (𝐹‘𝐶) ∈ ℂ)
44	43	adantr 480	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑧 ∈ ((𝑋 ∩ 𝑌) ∖ {𝐶})) → (𝐹‘𝐶) ∈ ℂ)
45	37, 44	subcld 11568	. . . . . 6 ⊢ ((𝜑 ∧ 𝑧 ∈ ((𝑋 ∩ 𝑌) ∖ {𝐶})) → ((𝐹‘𝑧) − (𝐹‘𝐶)) ∈ ℂ)
46	7, 5	sstrd 3984	. . . . . . . . 9 ⊢ (𝜑 → 𝑋 ⊆ ℂ)
47	46	adantr 480	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑧 ∈ ((𝑋 ∩ 𝑌) ∖ {𝐶})) → 𝑋 ⊆ ℂ)
48	47, 36	sseldd 3975	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑧 ∈ ((𝑋 ∩ 𝑌) ∖ {𝐶})) → 𝑧 ∈ ℂ)
49	46, 42	sseldd 3975	. . . . . . . 8 ⊢ (𝜑 → 𝐶 ∈ ℂ)
50	49	adantr 480	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑧 ∈ ((𝑋 ∩ 𝑌) ∖ {𝐶})) → 𝐶 ∈ ℂ)
51	48, 50	subcld 11568	. . . . . 6 ⊢ ((𝜑 ∧ 𝑧 ∈ ((𝑋 ∩ 𝑌) ∖ {𝐶})) → (𝑧 − 𝐶) ∈ ℂ)
52		eldifsni 4785	. . . . . . . 8 ⊢ (𝑧 ∈ ((𝑋 ∩ 𝑌) ∖ {𝐶}) → 𝑧 ≠ 𝐶)
53	52	adantl 481	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑧 ∈ ((𝑋 ∩ 𝑌) ∖ {𝐶})) → 𝑧 ≠ 𝐶)
54	48, 50, 53	subne0d 11577	. . . . . 6 ⊢ ((𝜑 ∧ 𝑧 ∈ ((𝑋 ∩ 𝑌) ∖ {𝐶})) → (𝑧 − 𝐶) ≠ 0)
55	45, 51, 54	divcld 11987	. . . . 5 ⊢ ((𝜑 ∧ 𝑧 ∈ ((𝑋 ∩ 𝑌) ∖ {𝐶})) → (((𝐹‘𝑧) − (𝐹‘𝐶)) / (𝑧 − 𝐶)) ∈ ℂ)
56	13	adantr 480	. . . . . 6 ⊢ ((𝜑 ∧ 𝑧 ∈ ((𝑋 ∩ 𝑌) ∖ {𝐶})) → 𝐺:𝑌⟶ℂ)
57		inss2 4221	. . . . . . 7 ⊢ (𝑋 ∩ 𝑌) ⊆ 𝑌
58	57, 35	sselid 3972	. . . . . 6 ⊢ ((𝜑 ∧ 𝑧 ∈ ((𝑋 ∩ 𝑌) ∖ {𝐶})) → 𝑧 ∈ 𝑌)
59	56, 58	ffvelcdmd 7077	. . . . 5 ⊢ ((𝜑 ∧ 𝑧 ∈ ((𝑋 ∩ 𝑌) ∖ {𝐶})) → (𝐺‘𝑧) ∈ ℂ)
60	55, 59	mulcld 11231	. . . 4 ⊢ ((𝜑 ∧ 𝑧 ∈ ((𝑋 ∩ 𝑌) ∖ {𝐶})) → ((((𝐹‘𝑧) − (𝐹‘𝐶)) / (𝑧 − 𝐶)) · (𝐺‘𝑧)) ∈ ℂ)
61		ssdif 4131	. . . . . . . 8 ⊢ ((𝑋 ∩ 𝑌) ⊆ 𝑌 → ((𝑋 ∩ 𝑌) ∖ {𝐶}) ⊆ (𝑌 ∖ {𝐶}))
62	57, 61	mp1i 13	. . . . . . 7 ⊢ (𝜑 → ((𝑋 ∩ 𝑌) ∖ {𝐶}) ⊆ (𝑌 ∖ {𝐶}))
63	62	sselda 3974	. . . . . 6 ⊢ ((𝜑 ∧ 𝑧 ∈ ((𝑋 ∩ 𝑌) ∖ {𝐶})) → 𝑧 ∈ (𝑌 ∖ {𝐶}))
64	14, 5	sstrd 3984	. . . . . . 7 ⊢ (𝜑 → 𝑌 ⊆ ℂ)
65	5, 13, 14	dvbss 25752	. . . . . . . 8 ⊢ (𝜑 → dom (𝑆 D 𝐺) ⊆ 𝑌)
66		reldv 25721	. . . . . . . . 9 ⊢ Rel (𝑆 D 𝐺)
67		releldm 5933	. . . . . . . . 9 ⊢ ((Rel (𝑆 D 𝐺) ∧ 𝐶(𝑆 D 𝐺)𝐿) → 𝐶 ∈ dom (𝑆 D 𝐺))
68	66, 11, 67	sylancr 586	. . . . . . . 8 ⊢ (𝜑 → 𝐶 ∈ dom (𝑆 D 𝐺))
69	65, 68	sseldd 3975	. . . . . . 7 ⊢ (𝜑 → 𝐶 ∈ 𝑌)
70	13, 64, 69	dvlem 25747	. . . . . 6 ⊢ ((𝜑 ∧ 𝑧 ∈ (𝑌 ∖ {𝐶})) → (((𝐺‘𝑧) − (𝐺‘𝐶)) / (𝑧 − 𝐶)) ∈ ℂ)
71	63, 70	syldan 590	. . . . 5 ⊢ ((𝜑 ∧ 𝑧 ∈ ((𝑋 ∩ 𝑌) ∖ {𝐶})) → (((𝐺‘𝑧) − (𝐺‘𝐶)) / (𝑧 − 𝐶)) ∈ ℂ)
72	71, 44	mulcld 11231	. . . 4 ⊢ ((𝜑 ∧ 𝑧 ∈ ((𝑋 ∩ 𝑌) ∖ {𝐶})) → ((((𝐺‘𝑧) − (𝐺‘𝐶)) / (𝑧 − 𝐶)) · (𝐹‘𝐶)) ∈ ℂ)
73		ssidd 3997	. . . 4 ⊢ (𝜑 → ℂ ⊆ ℂ)
74		txtopon 23417	. . . . . 6 ⊢ ((𝐽 ∈ (TopOn‘ℂ) ∧ 𝐽 ∈ (TopOn‘ℂ)) → (𝐽 ×_t 𝐽) ∈ (TopOn‘(ℂ × ℂ)))
75	19, 19, 74	mp2an 689	. . . . 5 ⊢ (𝐽 ×_t 𝐽) ∈ (TopOn‘(ℂ × ℂ))
76	75	toponrestid 22745	. . . 4 ⊢ (𝐽 ×_t 𝐽) = ((𝐽 ×_t 𝐽) ↾_t (ℂ × ℂ))
77	9	simprd 495	. . . . . . . 8 ⊢ (𝜑 → 𝐾 ∈ ((𝑧 ∈ (𝑋 ∖ {𝐶}) ↦ (((𝐹‘𝑧) − (𝐹‘𝐶)) / (𝑧 − 𝐶))) lim_ℂ 𝐶))
78	6, 46, 42	dvlem 25747	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑧 ∈ (𝑋 ∖ {𝐶})) → (((𝐹‘𝑧) − (𝐹‘𝐶)) / (𝑧 − 𝐶)) ∈ ℂ)
79	78	fmpttd 7106	. . . . . . . . . 10 ⊢ (𝜑 → (𝑧 ∈ (𝑋 ∖ {𝐶}) ↦ (((𝐹‘𝑧) − (𝐹‘𝐶)) / (𝑧 − 𝐶))):(𝑋 ∖ {𝐶})⟶ℂ)
80		ssdif 4131	. . . . . . . . . . 11 ⊢ ((𝑋 ∩ 𝑌) ⊆ 𝑋 → ((𝑋 ∩ 𝑌) ∖ {𝐶}) ⊆ (𝑋 ∖ {𝐶}))
81	33, 80	mp1i 13	. . . . . . . . . 10 ⊢ (𝜑 → ((𝑋 ∩ 𝑌) ∖ {𝐶}) ⊆ (𝑋 ∖ {𝐶}))
82	46	ssdifssd 4134	. . . . . . . . . 10 ⊢ (𝜑 → (𝑋 ∖ {𝐶}) ⊆ ℂ)
83		eqid 2724	. . . . . . . . . 10 ⊢ (𝐽 ↾_t ((𝑋 ∖ {𝐶}) ∪ {𝐶})) = (𝐽 ↾_t ((𝑋 ∖ {𝐶}) ∪ {𝐶}))
84	33, 7	sstrid 3985	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → (𝑋 ∩ 𝑌) ⊆ 𝑆)
85	84, 25	sseqtrd 4014	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (𝑋 ∩ 𝑌) ⊆ ∪ (𝐽 ↾_t 𝑆))
86		difssd 4124	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (∪ (𝐽 ↾_t 𝑆) ∖ 𝑋) ⊆ ∪ (𝐽 ↾_t 𝑆))
87	85, 86	unssd 4178	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → ((𝑋 ∩ 𝑌) ∪ (∪ (𝐽 ↾_t 𝑆) ∖ 𝑋)) ⊆ ∪ (𝐽 ↾_t 𝑆))
88		ssun1 4164	. . . . . . . . . . . . . . . 16 ⊢ (𝑋 ∩ 𝑌) ⊆ ((𝑋 ∩ 𝑌) ∪ (∪ (𝐽 ↾_t 𝑆) ∖ 𝑋))
89	88	a1i 11	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (𝑋 ∩ 𝑌) ⊆ ((𝑋 ∩ 𝑌) ∪ (∪ (𝐽 ↾_t 𝑆) ∖ 𝑋)))
90	28	ntrss 22881	. . . . . . . . . . . . . . 15 ⊢ (((𝐽 ↾_t 𝑆) ∈ Top ∧ ((𝑋 ∩ 𝑌) ∪ (∪ (𝐽 ↾_t 𝑆) ∖ 𝑋)) ⊆ ∪ (𝐽 ↾_t 𝑆) ∧ (𝑋 ∩ 𝑌) ⊆ ((𝑋 ∩ 𝑌) ∪ (∪ (𝐽 ↾_t 𝑆) ∖ 𝑋))) → ((int‘(𝐽 ↾_t 𝑆))‘(𝑋 ∩ 𝑌)) ⊆ ((int‘(𝐽 ↾_t 𝑆))‘((𝑋 ∩ 𝑌) ∪ (∪ (𝐽 ↾_t 𝑆) ∖ 𝑋))))
91	23, 87, 89, 90	syl3anc 1368	. . . . . . . . . . . . . 14 ⊢ (𝜑 → ((int‘(𝐽 ↾_t 𝑆))‘(𝑋 ∩ 𝑌)) ⊆ ((int‘(𝐽 ↾_t 𝑆))‘((𝑋 ∩ 𝑌) ∪ (∪ (𝐽 ↾_t 𝑆) ∖ 𝑋))))
92		eqid 2724	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑥 ∈ (𝑋 ∖ {𝐶}) ↦ (((𝐹‘𝑥) − (𝐹‘𝐶)) / (𝑥 − 𝐶))) = (𝑥 ∈ (𝑋 ∖ {𝐶}) ↦ (((𝐹‘𝑥) − (𝐹‘𝐶)) / (𝑥 − 𝐶)))
93	2, 3, 92, 5, 6, 7	eldv 25749	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → (𝐶(𝑆 D 𝐹)𝐾 ↔ (𝐶 ∈ ((int‘(𝐽 ↾_t 𝑆))‘𝑋) ∧ 𝐾 ∈ ((𝑥 ∈ (𝑋 ∖ {𝐶}) ↦ (((𝐹‘𝑥) − (𝐹‘𝐶)) / (𝑥 − 𝐶))) lim_ℂ 𝐶))))
94	1, 93	mpbid 231	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → (𝐶 ∈ ((int‘(𝐽 ↾_t 𝑆))‘𝑋) ∧ 𝐾 ∈ ((𝑥 ∈ (𝑋 ∖ {𝐶}) ↦ (((𝐹‘𝑥) − (𝐹‘𝐶)) / (𝑥 − 𝐶))) lim_ℂ 𝐶)))
95	94	simpld 494	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → 𝐶 ∈ ((int‘(𝐽 ↾_t 𝑆))‘𝑋))
96		eqid 2724	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑥 ∈ (𝑌 ∖ {𝐶}) ↦ (((𝐺‘𝑥) − (𝐺‘𝐶)) / (𝑥 − 𝐶))) = (𝑥 ∈ (𝑌 ∖ {𝐶}) ↦ (((𝐺‘𝑥) − (𝐺‘𝐶)) / (𝑥 − 𝐶)))
97	2, 3, 96, 5, 13, 14	eldv 25749	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → (𝐶(𝑆 D 𝐺)𝐿 ↔ (𝐶 ∈ ((int‘(𝐽 ↾_t 𝑆))‘𝑌) ∧ 𝐿 ∈ ((𝑥 ∈ (𝑌 ∖ {𝐶}) ↦ (((𝐺‘𝑥) − (𝐺‘𝐶)) / (𝑥 − 𝐶))) lim_ℂ 𝐶))))
98	11, 97	mpbid 231	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → (𝐶 ∈ ((int‘(𝐽 ↾_t 𝑆))‘𝑌) ∧ 𝐿 ∈ ((𝑥 ∈ (𝑌 ∖ {𝐶}) ↦ (((𝐺‘𝑥) − (𝐺‘𝐶)) / (𝑥 − 𝐶))) lim_ℂ 𝐶)))
99	98	simpld 494	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → 𝐶 ∈ ((int‘(𝐽 ↾_t 𝑆))‘𝑌))
100	95, 99	elind 4186	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → 𝐶 ∈ (((int‘(𝐽 ↾_t 𝑆))‘𝑋) ∩ ((int‘(𝐽 ↾_t 𝑆))‘𝑌)))
101	100, 30	eleqtrrd 2828	. . . . . . . . . . . . . 14 ⊢ (𝜑 → 𝐶 ∈ ((int‘(𝐽 ↾_t 𝑆))‘(𝑋 ∩ 𝑌)))
102	91, 101	sseldd 3975	. . . . . . . . . . . . 13 ⊢ (𝜑 → 𝐶 ∈ ((int‘(𝐽 ↾_t 𝑆))‘((𝑋 ∩ 𝑌) ∪ (∪ (𝐽 ↾_t 𝑆) ∖ 𝑋))))
103	102, 42	elind 4186	. . . . . . . . . . . 12 ⊢ (𝜑 → 𝐶 ∈ (((int‘(𝐽 ↾_t 𝑆))‘((𝑋 ∩ 𝑌) ∪ (∪ (𝐽 ↾_t 𝑆) ∖ 𝑋))) ∩ 𝑋))
104	33	a1i 11	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (𝑋 ∩ 𝑌) ⊆ 𝑋)
105		eqid 2724	. . . . . . . . . . . . . . 15 ⊢ ((𝐽 ↾_t 𝑆) ↾_t 𝑋) = ((𝐽 ↾_t 𝑆) ↾_t 𝑋)
106	28, 105	restntr 23008	. . . . . . . . . . . . . 14 ⊢ (((𝐽 ↾_t 𝑆) ∈ Top ∧ 𝑋 ⊆ ∪ (𝐽 ↾_t 𝑆) ∧ (𝑋 ∩ 𝑌) ⊆ 𝑋) → ((int‘((𝐽 ↾_t 𝑆) ↾_t 𝑋))‘(𝑋 ∩ 𝑌)) = (((int‘(𝐽 ↾_t 𝑆))‘((𝑋 ∩ 𝑌) ∪ (∪ (𝐽 ↾_t 𝑆) ∖ 𝑋))) ∩ 𝑋))
107	23, 26, 104, 106	syl3anc 1368	. . . . . . . . . . . . 13 ⊢ (𝜑 → ((int‘((𝐽 ↾_t 𝑆) ↾_t 𝑋))‘(𝑋 ∩ 𝑌)) = (((int‘(𝐽 ↾_t 𝑆))‘((𝑋 ∩ 𝑌) ∪ (∪ (𝐽 ↾_t 𝑆) ∖ 𝑋))) ∩ 𝑋))
108	3	cnfldtop 24622	. . . . . . . . . . . . . . . . 17 ⊢ 𝐽 ∈ Top
109	108	a1i 11	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → 𝐽 ∈ Top)
110		cnex 11187	. . . . . . . . . . . . . . . . 17 ⊢ ℂ ∈ V
111		ssexg 5313	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑆 ⊆ ℂ ∧ ℂ ∈ V) → 𝑆 ∈ V)
112	5, 110, 111	sylancl 585	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → 𝑆 ∈ V)
113		restabs 22991	. . . . . . . . . . . . . . . 16 ⊢ ((𝐽 ∈ Top ∧ 𝑋 ⊆ 𝑆 ∧ 𝑆 ∈ V) → ((𝐽 ↾_t 𝑆) ↾_t 𝑋) = (𝐽 ↾_t 𝑋))
114	109, 7, 112, 113	syl3anc 1368	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → ((𝐽 ↾_t 𝑆) ↾_t 𝑋) = (𝐽 ↾_t 𝑋))
115	114	fveq2d 6885	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (int‘((𝐽 ↾_t 𝑆) ↾_t 𝑋)) = (int‘(𝐽 ↾_t 𝑋)))
116	115	fveq1d 6883	. . . . . . . . . . . . 13 ⊢ (𝜑 → ((int‘((𝐽 ↾_t 𝑆) ↾_t 𝑋))‘(𝑋 ∩ 𝑌)) = ((int‘(𝐽 ↾_t 𝑋))‘(𝑋 ∩ 𝑌)))
117	107, 116	eqtr3d 2766	. . . . . . . . . . . 12 ⊢ (𝜑 → (((int‘(𝐽 ↾_t 𝑆))‘((𝑋 ∩ 𝑌) ∪ (∪ (𝐽 ↾_t 𝑆) ∖ 𝑋))) ∩ 𝑋) = ((int‘(𝐽 ↾_t 𝑋))‘(𝑋 ∩ 𝑌)))
118	103, 117	eleqtrd 2827	. . . . . . . . . . 11 ⊢ (𝜑 → 𝐶 ∈ ((int‘(𝐽 ↾_t 𝑋))‘(𝑋 ∩ 𝑌)))
119		undif1 4467	. . . . . . . . . . . . . . 15 ⊢ ((𝑋 ∖ {𝐶}) ∪ {𝐶}) = (𝑋 ∪ {𝐶})
120	42	snssd 4804	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → {𝐶} ⊆ 𝑋)
121		ssequn2 4175	. . . . . . . . . . . . . . . 16 ⊢ ({𝐶} ⊆ 𝑋 ↔ (𝑋 ∪ {𝐶}) = 𝑋)
122	120, 121	sylib 217	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (𝑋 ∪ {𝐶}) = 𝑋)
123	119, 122	eqtrid 2776	. . . . . . . . . . . . . 14 ⊢ (𝜑 → ((𝑋 ∖ {𝐶}) ∪ {𝐶}) = 𝑋)
124	123	oveq2d 7417	. . . . . . . . . . . . 13 ⊢ (𝜑 → (𝐽 ↾_t ((𝑋 ∖ {𝐶}) ∪ {𝐶})) = (𝐽 ↾_t 𝑋))
125	124	fveq2d 6885	. . . . . . . . . . . 12 ⊢ (𝜑 → (int‘(𝐽 ↾_t ((𝑋 ∖ {𝐶}) ∪ {𝐶}))) = (int‘(𝐽 ↾_t 𝑋)))
126		undif1 4467	. . . . . . . . . . . . 13 ⊢ (((𝑋 ∩ 𝑌) ∖ {𝐶}) ∪ {𝐶}) = ((𝑋 ∩ 𝑌) ∪ {𝐶})
127	42, 69	elind 4186	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → 𝐶 ∈ (𝑋 ∩ 𝑌))
128	127	snssd 4804	. . . . . . . . . . . . . 14 ⊢ (𝜑 → {𝐶} ⊆ (𝑋 ∩ 𝑌))
129		ssequn2 4175	. . . . . . . . . . . . . 14 ⊢ ({𝐶} ⊆ (𝑋 ∩ 𝑌) ↔ ((𝑋 ∩ 𝑌) ∪ {𝐶}) = (𝑋 ∩ 𝑌))
130	128, 129	sylib 217	. . . . . . . . . . . . 13 ⊢ (𝜑 → ((𝑋 ∩ 𝑌) ∪ {𝐶}) = (𝑋 ∩ 𝑌))
131	126, 130	eqtrid 2776	. . . . . . . . . . . 12 ⊢ (𝜑 → (((𝑋 ∩ 𝑌) ∖ {𝐶}) ∪ {𝐶}) = (𝑋 ∩ 𝑌))
132	125, 131	fveq12d 6888	. . . . . . . . . . 11 ⊢ (𝜑 → ((int‘(𝐽 ↾_t ((𝑋 ∖ {𝐶}) ∪ {𝐶})))‘(((𝑋 ∩ 𝑌) ∖ {𝐶}) ∪ {𝐶})) = ((int‘(𝐽 ↾_t 𝑋))‘(𝑋 ∩ 𝑌)))
133	118, 132	eleqtrrd 2828	. . . . . . . . . 10 ⊢ (𝜑 → 𝐶 ∈ ((int‘(𝐽 ↾_t ((𝑋 ∖ {𝐶}) ∪ {𝐶})))‘(((𝑋 ∩ 𝑌) ∖ {𝐶}) ∪ {𝐶})))
134	79, 81, 82, 3, 83, 133	limcres 25737	. . . . . . . . 9 ⊢ (𝜑 → (((𝑧 ∈ (𝑋 ∖ {𝐶}) ↦ (((𝐹‘𝑧) − (𝐹‘𝐶)) / (𝑧 − 𝐶))) ↾ ((𝑋 ∩ 𝑌) ∖ {𝐶})) lim_ℂ 𝐶) = ((𝑧 ∈ (𝑋 ∖ {𝐶}) ↦ (((𝐹‘𝑧) − (𝐹‘𝐶)) / (𝑧 − 𝐶))) lim_ℂ 𝐶))
135	81	resmptd 6030	. . . . . . . . . 10 ⊢ (𝜑 → ((𝑧 ∈ (𝑋 ∖ {𝐶}) ↦ (((𝐹‘𝑧) − (𝐹‘𝐶)) / (𝑧 − 𝐶))) ↾ ((𝑋 ∩ 𝑌) ∖ {𝐶})) = (𝑧 ∈ ((𝑋 ∩ 𝑌) ∖ {𝐶}) ↦ (((𝐹‘𝑧) − (𝐹‘𝐶)) / (𝑧 − 𝐶))))
136	135	oveq1d 7416	. . . . . . . . 9 ⊢ (𝜑 → (((𝑧 ∈ (𝑋 ∖ {𝐶}) ↦ (((𝐹‘𝑧) − (𝐹‘𝐶)) / (𝑧 − 𝐶))) ↾ ((𝑋 ∩ 𝑌) ∖ {𝐶})) lim_ℂ 𝐶) = ((𝑧 ∈ ((𝑋 ∩ 𝑌) ∖ {𝐶}) ↦ (((𝐹‘𝑧) − (𝐹‘𝐶)) / (𝑧 − 𝐶))) lim_ℂ 𝐶))
137	134, 136	eqtr3d 2766	. . . . . . . 8 ⊢ (𝜑 → ((𝑧 ∈ (𝑋 ∖ {𝐶}) ↦ (((𝐹‘𝑧) − (𝐹‘𝐶)) / (𝑧 − 𝐶))) lim_ℂ 𝐶) = ((𝑧 ∈ ((𝑋 ∩ 𝑌) ∖ {𝐶}) ↦ (((𝐹‘𝑧) − (𝐹‘𝐶)) / (𝑧 − 𝐶))) lim_ℂ 𝐶))
138	77, 137	eleqtrd 2827	. . . . . . 7 ⊢ (𝜑 → 𝐾 ∈ ((𝑧 ∈ ((𝑋 ∩ 𝑌) ∖ {𝐶}) ↦ (((𝐹‘𝑧) − (𝐹‘𝐶)) / (𝑧 − 𝐶))) lim_ℂ 𝐶))
139		eqid 2724	. . . . . . . . . . . 12 ⊢ (𝐽 ↾_t 𝑌) = (𝐽 ↾_t 𝑌)
140	139, 3	dvcnp2 25771	. . . . . . . . . . 11 ⊢ (((𝑆 ⊆ ℂ ∧ 𝐺:𝑌⟶ℂ ∧ 𝑌 ⊆ 𝑆) ∧ 𝐶 ∈ dom (𝑆 D 𝐺)) → 𝐺 ∈ (((𝐽 ↾_t 𝑌) CnP 𝐽)‘𝐶))
141	5, 13, 14, 68, 140	syl31anc 1370	. . . . . . . . . 10 ⊢ (𝜑 → 𝐺 ∈ (((𝐽 ↾_t 𝑌) CnP 𝐽)‘𝐶))
142	3, 139	cnplimc 25738	. . . . . . . . . . 11 ⊢ ((𝑌 ⊆ ℂ ∧ 𝐶 ∈ 𝑌) → (𝐺 ∈ (((𝐽 ↾_t 𝑌) CnP 𝐽)‘𝐶) ↔ (𝐺:𝑌⟶ℂ ∧ (𝐺‘𝐶) ∈ (𝐺 lim_ℂ 𝐶))))
143	64, 69, 142	syl2anc 583	. . . . . . . . . 10 ⊢ (𝜑 → (𝐺 ∈ (((𝐽 ↾_t 𝑌) CnP 𝐽)‘𝐶) ↔ (𝐺:𝑌⟶ℂ ∧ (𝐺‘𝐶) ∈ (𝐺 lim_ℂ 𝐶))))
144	141, 143	mpbid 231	. . . . . . . . 9 ⊢ (𝜑 → (𝐺:𝑌⟶ℂ ∧ (𝐺‘𝐶) ∈ (𝐺 lim_ℂ 𝐶)))
145	144	simprd 495	. . . . . . . 8 ⊢ (𝜑 → (𝐺‘𝐶) ∈ (𝐺 lim_ℂ 𝐶))
146		difss 4123	. . . . . . . . . . . 12 ⊢ ((𝑋 ∩ 𝑌) ∖ {𝐶}) ⊆ (𝑋 ∩ 𝑌)
147	146, 57	sstri 3983	. . . . . . . . . . 11 ⊢ ((𝑋 ∩ 𝑌) ∖ {𝐶}) ⊆ 𝑌
148	147	a1i 11	. . . . . . . . . 10 ⊢ (𝜑 → ((𝑋 ∩ 𝑌) ∖ {𝐶}) ⊆ 𝑌)
149		eqid 2724	. . . . . . . . . 10 ⊢ (𝐽 ↾_t (𝑌 ∪ {𝐶})) = (𝐽 ↾_t (𝑌 ∪ {𝐶}))
150		difssd 4124	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (∪ (𝐽 ↾_t 𝑆) ∖ 𝑌) ⊆ ∪ (𝐽 ↾_t 𝑆))
151	85, 150	unssd 4178	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → ((𝑋 ∩ 𝑌) ∪ (∪ (𝐽 ↾_t 𝑆) ∖ 𝑌)) ⊆ ∪ (𝐽 ↾_t 𝑆))
152		ssun1 4164	. . . . . . . . . . . . . . . 16 ⊢ (𝑋 ∩ 𝑌) ⊆ ((𝑋 ∩ 𝑌) ∪ (∪ (𝐽 ↾_t 𝑆) ∖ 𝑌))
153	152	a1i 11	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (𝑋 ∩ 𝑌) ⊆ ((𝑋 ∩ 𝑌) ∪ (∪ (𝐽 ↾_t 𝑆) ∖ 𝑌)))
154	28	ntrss 22881	. . . . . . . . . . . . . . 15 ⊢ (((𝐽 ↾_t 𝑆) ∈ Top ∧ ((𝑋 ∩ 𝑌) ∪ (∪ (𝐽 ↾_t 𝑆) ∖ 𝑌)) ⊆ ∪ (𝐽 ↾_t 𝑆) ∧ (𝑋 ∩ 𝑌) ⊆ ((𝑋 ∩ 𝑌) ∪ (∪ (𝐽 ↾_t 𝑆) ∖ 𝑌))) → ((int‘(𝐽 ↾_t 𝑆))‘(𝑋 ∩ 𝑌)) ⊆ ((int‘(𝐽 ↾_t 𝑆))‘((𝑋 ∩ 𝑌) ∪ (∪ (𝐽 ↾_t 𝑆) ∖ 𝑌))))
155	23, 151, 153, 154	syl3anc 1368	. . . . . . . . . . . . . 14 ⊢ (𝜑 → ((int‘(𝐽 ↾_t 𝑆))‘(𝑋 ∩ 𝑌)) ⊆ ((int‘(𝐽 ↾_t 𝑆))‘((𝑋 ∩ 𝑌) ∪ (∪ (𝐽 ↾_t 𝑆) ∖ 𝑌))))
156	155, 101	sseldd 3975	. . . . . . . . . . . . 13 ⊢ (𝜑 → 𝐶 ∈ ((int‘(𝐽 ↾_t 𝑆))‘((𝑋 ∩ 𝑌) ∪ (∪ (𝐽 ↾_t 𝑆) ∖ 𝑌))))
157	156, 69	elind 4186	. . . . . . . . . . . 12 ⊢ (𝜑 → 𝐶 ∈ (((int‘(𝐽 ↾_t 𝑆))‘((𝑋 ∩ 𝑌) ∪ (∪ (𝐽 ↾_t 𝑆) ∖ 𝑌))) ∩ 𝑌))
158	57	a1i 11	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (𝑋 ∩ 𝑌) ⊆ 𝑌)
159		eqid 2724	. . . . . . . . . . . . . . 15 ⊢ ((𝐽 ↾_t 𝑆) ↾_t 𝑌) = ((𝐽 ↾_t 𝑆) ↾_t 𝑌)
160	28, 159	restntr 23008	. . . . . . . . . . . . . 14 ⊢ (((𝐽 ↾_t 𝑆) ∈ Top ∧ 𝑌 ⊆ ∪ (𝐽 ↾_t 𝑆) ∧ (𝑋 ∩ 𝑌) ⊆ 𝑌) → ((int‘((𝐽 ↾_t 𝑆) ↾_t 𝑌))‘(𝑋 ∩ 𝑌)) = (((int‘(𝐽 ↾_t 𝑆))‘((𝑋 ∩ 𝑌) ∪ (∪ (𝐽 ↾_t 𝑆) ∖ 𝑌))) ∩ 𝑌))
161	23, 27, 158, 160	syl3anc 1368	. . . . . . . . . . . . 13 ⊢ (𝜑 → ((int‘((𝐽 ↾_t 𝑆) ↾_t 𝑌))‘(𝑋 ∩ 𝑌)) = (((int‘(𝐽 ↾_t 𝑆))‘((𝑋 ∩ 𝑌) ∪ (∪ (𝐽 ↾_t 𝑆) ∖ 𝑌))) ∩ 𝑌))
162		restabs 22991	. . . . . . . . . . . . . . . 16 ⊢ ((𝐽 ∈ Top ∧ 𝑌 ⊆ 𝑆 ∧ 𝑆 ∈ V) → ((𝐽 ↾_t 𝑆) ↾_t 𝑌) = (𝐽 ↾_t 𝑌))
163	109, 14, 112, 162	syl3anc 1368	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → ((𝐽 ↾_t 𝑆) ↾_t 𝑌) = (𝐽 ↾_t 𝑌))
164	163	fveq2d 6885	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (int‘((𝐽 ↾_t 𝑆) ↾_t 𝑌)) = (int‘(𝐽 ↾_t 𝑌)))
165	164	fveq1d 6883	. . . . . . . . . . . . 13 ⊢ (𝜑 → ((int‘((𝐽 ↾_t 𝑆) ↾_t 𝑌))‘(𝑋 ∩ 𝑌)) = ((int‘(𝐽 ↾_t 𝑌))‘(𝑋 ∩ 𝑌)))
166	161, 165	eqtr3d 2766	. . . . . . . . . . . 12 ⊢ (𝜑 → (((int‘(𝐽 ↾_t 𝑆))‘((𝑋 ∩ 𝑌) ∪ (∪ (𝐽 ↾_t 𝑆) ∖ 𝑌))) ∩ 𝑌) = ((int‘(𝐽 ↾_t 𝑌))‘(𝑋 ∩ 𝑌)))
167	157, 166	eleqtrd 2827	. . . . . . . . . . 11 ⊢ (𝜑 → 𝐶 ∈ ((int‘(𝐽 ↾_t 𝑌))‘(𝑋 ∩ 𝑌)))
168	69	snssd 4804	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → {𝐶} ⊆ 𝑌)
169		ssequn2 4175	. . . . . . . . . . . . . . 15 ⊢ ({𝐶} ⊆ 𝑌 ↔ (𝑌 ∪ {𝐶}) = 𝑌)
170	168, 169	sylib 217	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (𝑌 ∪ {𝐶}) = 𝑌)
171	170	oveq2d 7417	. . . . . . . . . . . . 13 ⊢ (𝜑 → (𝐽 ↾_t (𝑌 ∪ {𝐶})) = (𝐽 ↾_t 𝑌))
172	171	fveq2d 6885	. . . . . . . . . . . 12 ⊢ (𝜑 → (int‘(𝐽 ↾_t (𝑌 ∪ {𝐶}))) = (int‘(𝐽 ↾_t 𝑌)))
173	172, 131	fveq12d 6888	. . . . . . . . . . 11 ⊢ (𝜑 → ((int‘(𝐽 ↾_t (𝑌 ∪ {𝐶})))‘(((𝑋 ∩ 𝑌) ∖ {𝐶}) ∪ {𝐶})) = ((int‘(𝐽 ↾_t 𝑌))‘(𝑋 ∩ 𝑌)))
174	167, 173	eleqtrrd 2828	. . . . . . . . . 10 ⊢ (𝜑 → 𝐶 ∈ ((int‘(𝐽 ↾_t (𝑌 ∪ {𝐶})))‘(((𝑋 ∩ 𝑌) ∖ {𝐶}) ∪ {𝐶})))
175	13, 148, 64, 3, 149, 174	limcres 25737	. . . . . . . . 9 ⊢ (𝜑 → ((𝐺 ↾ ((𝑋 ∩ 𝑌) ∖ {𝐶})) lim_ℂ 𝐶) = (𝐺 lim_ℂ 𝐶))
176	13, 148	feqresmpt 6951	. . . . . . . . . 10 ⊢ (𝜑 → (𝐺 ↾ ((𝑋 ∩ 𝑌) ∖ {𝐶})) = (𝑧 ∈ ((𝑋 ∩ 𝑌) ∖ {𝐶}) ↦ (𝐺‘𝑧)))
177	176	oveq1d 7416	. . . . . . . . 9 ⊢ (𝜑 → ((𝐺 ↾ ((𝑋 ∩ 𝑌) ∖ {𝐶})) lim_ℂ 𝐶) = ((𝑧 ∈ ((𝑋 ∩ 𝑌) ∖ {𝐶}) ↦ (𝐺‘𝑧)) lim_ℂ 𝐶))
178	175, 177	eqtr3d 2766	. . . . . . . 8 ⊢ (𝜑 → (𝐺 lim_ℂ 𝐶) = ((𝑧 ∈ ((𝑋 ∩ 𝑌) ∖ {𝐶}) ↦ (𝐺‘𝑧)) lim_ℂ 𝐶))
179	145, 178	eleqtrd 2827	. . . . . . 7 ⊢ (𝜑 → (𝐺‘𝐶) ∈ ((𝑧 ∈ ((𝑋 ∩ 𝑌) ∖ {𝐶}) ↦ (𝐺‘𝑧)) lim_ℂ 𝐶))
180	3	mpomulcn 24707	. . . . . . . 8 ⊢ (𝑢 ∈ ℂ, 𝑣 ∈ ℂ ↦ (𝑢 · 𝑣)) ∈ ((𝐽 ×_t 𝐽) Cn 𝐽)
181	5, 6, 7	dvcl 25750	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝐶(𝑆 D 𝐹)𝐾) → 𝐾 ∈ ℂ)
182	1, 181	mpdan 684	. . . . . . . . 9 ⊢ (𝜑 → 𝐾 ∈ ℂ)
183	13, 69	ffvelcdmd 7077	. . . . . . . . 9 ⊢ (𝜑 → (𝐺‘𝐶) ∈ ℂ)
184	182, 183	opelxpd 5705	. . . . . . . 8 ⊢ (𝜑 → ⟨𝐾, (𝐺‘𝐶)⟩ ∈ (ℂ × ℂ))
185	75	toponunii 22740	. . . . . . . . 9 ⊢ (ℂ × ℂ) = ∪ (𝐽 ×_t 𝐽)
186	185	cncnpi 23104	. . . . . . . 8 ⊢ (((𝑢 ∈ ℂ, 𝑣 ∈ ℂ ↦ (𝑢 · 𝑣)) ∈ ((𝐽 ×_t 𝐽) Cn 𝐽) ∧ ⟨𝐾, (𝐺‘𝐶)⟩ ∈ (ℂ × ℂ)) → (𝑢 ∈ ℂ, 𝑣 ∈ ℂ ↦ (𝑢 · 𝑣)) ∈ (((𝐽 ×_t 𝐽) CnP 𝐽)‘⟨𝐾, (𝐺‘𝐶)⟩))
187	180, 184, 186	sylancr 586	. . . . . . 7 ⊢ (𝜑 → (𝑢 ∈ ℂ, 𝑣 ∈ ℂ ↦ (𝑢 · 𝑣)) ∈ (((𝐽 ×_t 𝐽) CnP 𝐽)‘⟨𝐾, (𝐺‘𝐶)⟩))
188	55, 59, 73, 73, 3, 76, 138, 179, 187	limccnp2 25743	. . . . . 6 ⊢ (𝜑 → (𝐾(𝑢 ∈ ℂ, 𝑣 ∈ ℂ ↦ (𝑢 · 𝑣))(𝐺‘𝐶)) ∈ ((𝑧 ∈ ((𝑋 ∩ 𝑌) ∖ {𝐶}) ↦ ((((𝐹‘𝑧) − (𝐹‘𝐶)) / (𝑧 − 𝐶))(𝑢 ∈ ℂ, 𝑣 ∈ ℂ ↦ (𝑢 · 𝑣))(𝐺‘𝑧))) lim_ℂ 𝐶))
189		df-mpt 5222	. . . . . . 7 ⊢ (𝑧 ∈ ((𝑋 ∩ 𝑌) ∖ {𝐶}) ↦ ((((𝐹‘𝑧) − (𝐹‘𝐶)) / (𝑧 − 𝐶))(𝑢 ∈ ℂ, 𝑣 ∈ ℂ ↦ (𝑢 · 𝑣))(𝐺‘𝑧))) = {⟨𝑧, 𝑤⟩ ∣ (𝑧 ∈ ((𝑋 ∩ 𝑌) ∖ {𝐶}) ∧ 𝑤 = ((((𝐹‘𝑧) − (𝐹‘𝐶)) / (𝑧 − 𝐶))(𝑢 ∈ ℂ, 𝑣 ∈ ℂ ↦ (𝑢 · 𝑣))(𝐺‘𝑧)))}
190	189	oveq1i 7411	. . . . . 6 ⊢ ((𝑧 ∈ ((𝑋 ∩ 𝑌) ∖ {𝐶}) ↦ ((((𝐹‘𝑧) − (𝐹‘𝐶)) / (𝑧 − 𝐶))(𝑢 ∈ ℂ, 𝑣 ∈ ℂ ↦ (𝑢 · 𝑣))(𝐺‘𝑧))) lim_ℂ 𝐶) = ({⟨𝑧, 𝑤⟩ ∣ (𝑧 ∈ ((𝑋 ∩ 𝑌) ∖ {𝐶}) ∧ 𝑤 = ((((𝐹‘𝑧) − (𝐹‘𝐶)) / (𝑧 − 𝐶))(𝑢 ∈ ℂ, 𝑣 ∈ ℂ ↦ (𝑢 · 𝑣))(𝐺‘𝑧)))} lim_ℂ 𝐶)
191	188, 190	eleqtrdi 2835	. . . . 5 ⊢ (𝜑 → (𝐾(𝑢 ∈ ℂ, 𝑣 ∈ ℂ ↦ (𝑢 · 𝑣))(𝐺‘𝐶)) ∈ ({⟨𝑧, 𝑤⟩ ∣ (𝑧 ∈ ((𝑋 ∩ 𝑌) ∖ {𝐶}) ∧ 𝑤 = ((((𝐹‘𝑧) − (𝐹‘𝐶)) / (𝑧 − 𝐶))(𝑢 ∈ ℂ, 𝑣 ∈ ℂ ↦ (𝑢 · 𝑣))(𝐺‘𝑧)))} lim_ℂ 𝐶))
192		ovmpot 7561	. . . . . 6 ⊢ ((𝐾 ∈ ℂ ∧ (𝐺‘𝐶) ∈ ℂ) → (𝐾(𝑢 ∈ ℂ, 𝑣 ∈ ℂ ↦ (𝑢 · 𝑣))(𝐺‘𝐶)) = (𝐾 · (𝐺‘𝐶)))
193	182, 183, 192	syl2anc 583	. . . . 5 ⊢ (𝜑 → (𝐾(𝑢 ∈ ℂ, 𝑣 ∈ ℂ ↦ (𝑢 · 𝑣))(𝐺‘𝐶)) = (𝐾 · (𝐺‘𝐶)))
194		ovmpot 7561	. . . . . . . . . . 11 ⊢ (((((𝐹‘𝑧) − (𝐹‘𝐶)) / (𝑧 − 𝐶)) ∈ ℂ ∧ (𝐺‘𝑧) ∈ ℂ) → ((((𝐹‘𝑧) − (𝐹‘𝐶)) / (𝑧 − 𝐶))(𝑢 ∈ ℂ, 𝑣 ∈ ℂ ↦ (𝑢 · 𝑣))(𝐺‘𝑧)) = ((((𝐹‘𝑧) − (𝐹‘𝐶)) / (𝑧 − 𝐶)) · (𝐺‘𝑧)))
195	55, 59, 194	syl2anc 583	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑧 ∈ ((𝑋 ∩ 𝑌) ∖ {𝐶})) → ((((𝐹‘𝑧) − (𝐹‘𝐶)) / (𝑧 − 𝐶))(𝑢 ∈ ℂ, 𝑣 ∈ ℂ ↦ (𝑢 · 𝑣))(𝐺‘𝑧)) = ((((𝐹‘𝑧) − (𝐹‘𝐶)) / (𝑧 − 𝐶)) · (𝐺‘𝑧)))
196	195	eqeq2d 2735	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑧 ∈ ((𝑋 ∩ 𝑌) ∖ {𝐶})) → (𝑤 = ((((𝐹‘𝑧) − (𝐹‘𝐶)) / (𝑧 − 𝐶))(𝑢 ∈ ℂ, 𝑣 ∈ ℂ ↦ (𝑢 · 𝑣))(𝐺‘𝑧)) ↔ 𝑤 = ((((𝐹‘𝑧) − (𝐹‘𝐶)) / (𝑧 − 𝐶)) · (𝐺‘𝑧))))
197	196	pm5.32da 578	. . . . . . . 8 ⊢ (𝜑 → ((𝑧 ∈ ((𝑋 ∩ 𝑌) ∖ {𝐶}) ∧ 𝑤 = ((((𝐹‘𝑧) − (𝐹‘𝐶)) / (𝑧 − 𝐶))(𝑢 ∈ ℂ, 𝑣 ∈ ℂ ↦ (𝑢 · 𝑣))(𝐺‘𝑧))) ↔ (𝑧 ∈ ((𝑋 ∩ 𝑌) ∖ {𝐶}) ∧ 𝑤 = ((((𝐹‘𝑧) − (𝐹‘𝐶)) / (𝑧 − 𝐶)) · (𝐺‘𝑧)))))
198	197	opabbidv 5204	. . . . . . 7 ⊢ (𝜑 → {⟨𝑧, 𝑤⟩ ∣ (𝑧 ∈ ((𝑋 ∩ 𝑌) ∖ {𝐶}) ∧ 𝑤 = ((((𝐹‘𝑧) − (𝐹‘𝐶)) / (𝑧 − 𝐶))(𝑢 ∈ ℂ, 𝑣 ∈ ℂ ↦ (𝑢 · 𝑣))(𝐺‘𝑧)))} = {⟨𝑧, 𝑤⟩ ∣ (𝑧 ∈ ((𝑋 ∩ 𝑌) ∖ {𝐶}) ∧ 𝑤 = ((((𝐹‘𝑧) − (𝐹‘𝐶)) / (𝑧 − 𝐶)) · (𝐺‘𝑧)))})
199		df-mpt 5222	. . . . . . 7 ⊢ (𝑧 ∈ ((𝑋 ∩ 𝑌) ∖ {𝐶}) ↦ ((((𝐹‘𝑧) − (𝐹‘𝐶)) / (𝑧 − 𝐶)) · (𝐺‘𝑧))) = {⟨𝑧, 𝑤⟩ ∣ (𝑧 ∈ ((𝑋 ∩ 𝑌) ∖ {𝐶}) ∧ 𝑤 = ((((𝐹‘𝑧) − (𝐹‘𝐶)) / (𝑧 − 𝐶)) · (𝐺‘𝑧)))}
200	198, 199	eqtr4di 2782	. . . . . 6 ⊢ (𝜑 → {⟨𝑧, 𝑤⟩ ∣ (𝑧 ∈ ((𝑋 ∩ 𝑌) ∖ {𝐶}) ∧ 𝑤 = ((((𝐹‘𝑧) − (𝐹‘𝐶)) / (𝑧 − 𝐶))(𝑢 ∈ ℂ, 𝑣 ∈ ℂ ↦ (𝑢 · 𝑣))(𝐺‘𝑧)))} = (𝑧 ∈ ((𝑋 ∩ 𝑌) ∖ {𝐶}) ↦ ((((𝐹‘𝑧) − (𝐹‘𝐶)) / (𝑧 − 𝐶)) · (𝐺‘𝑧))))
201	200	oveq1d 7416	. . . . 5 ⊢ (𝜑 → ({⟨𝑧, 𝑤⟩ ∣ (𝑧 ∈ ((𝑋 ∩ 𝑌) ∖ {𝐶}) ∧ 𝑤 = ((((𝐹‘𝑧) − (𝐹‘𝐶)) / (𝑧 − 𝐶))(𝑢 ∈ ℂ, 𝑣 ∈ ℂ ↦ (𝑢 · 𝑣))(𝐺‘𝑧)))} lim_ℂ 𝐶) = ((𝑧 ∈ ((𝑋 ∩ 𝑌) ∖ {𝐶}) ↦ ((((𝐹‘𝑧) − (𝐹‘𝐶)) / (𝑧 − 𝐶)) · (𝐺‘𝑧))) lim_ℂ 𝐶))
202	191, 193, 201	3eltr3d 2839	. . . 4 ⊢ (𝜑 → (𝐾 · (𝐺‘𝐶)) ∈ ((𝑧 ∈ ((𝑋 ∩ 𝑌) ∖ {𝐶}) ↦ ((((𝐹‘𝑧) − (𝐹‘𝐶)) / (𝑧 − 𝐶)) · (𝐺‘𝑧))) lim_ℂ 𝐶))
203	16	simprd 495	. . . . . . . 8 ⊢ (𝜑 → 𝐿 ∈ ((𝑧 ∈ (𝑌 ∖ {𝐶}) ↦ (((𝐺‘𝑧) − (𝐺‘𝐶)) / (𝑧 − 𝐶))) lim_ℂ 𝐶))
204	70	fmpttd 7106	. . . . . . . . . 10 ⊢ (𝜑 → (𝑧 ∈ (𝑌 ∖ {𝐶}) ↦ (((𝐺‘𝑧) − (𝐺‘𝐶)) / (𝑧 − 𝐶))):(𝑌 ∖ {𝐶})⟶ℂ)
205	64	ssdifssd 4134	. . . . . . . . . 10 ⊢ (𝜑 → (𝑌 ∖ {𝐶}) ⊆ ℂ)
206		eqid 2724	. . . . . . . . . 10 ⊢ (𝐽 ↾_t ((𝑌 ∖ {𝐶}) ∪ {𝐶})) = (𝐽 ↾_t ((𝑌 ∖ {𝐶}) ∪ {𝐶}))
207		undif1 4467	. . . . . . . . . . . . . . 15 ⊢ ((𝑌 ∖ {𝐶}) ∪ {𝐶}) = (𝑌 ∪ {𝐶})
208	207, 170	eqtrid 2776	. . . . . . . . . . . . . 14 ⊢ (𝜑 → ((𝑌 ∖ {𝐶}) ∪ {𝐶}) = 𝑌)
209	208	oveq2d 7417	. . . . . . . . . . . . 13 ⊢ (𝜑 → (𝐽 ↾_t ((𝑌 ∖ {𝐶}) ∪ {𝐶})) = (𝐽 ↾_t 𝑌))
210	209	fveq2d 6885	. . . . . . . . . . . 12 ⊢ (𝜑 → (int‘(𝐽 ↾_t ((𝑌 ∖ {𝐶}) ∪ {𝐶}))) = (int‘(𝐽 ↾_t 𝑌)))
211	210, 131	fveq12d 6888	. . . . . . . . . . 11 ⊢ (𝜑 → ((int‘(𝐽 ↾_t ((𝑌 ∖ {𝐶}) ∪ {𝐶})))‘(((𝑋 ∩ 𝑌) ∖ {𝐶}) ∪ {𝐶})) = ((int‘(𝐽 ↾_t 𝑌))‘(𝑋 ∩ 𝑌)))
212	167, 211	eleqtrrd 2828	. . . . . . . . . 10 ⊢ (𝜑 → 𝐶 ∈ ((int‘(𝐽 ↾_t ((𝑌 ∖ {𝐶}) ∪ {𝐶})))‘(((𝑋 ∩ 𝑌) ∖ {𝐶}) ∪ {𝐶})))
213	204, 62, 205, 3, 206, 212	limcres 25737	. . . . . . . . 9 ⊢ (𝜑 → (((𝑧 ∈ (𝑌 ∖ {𝐶}) ↦ (((𝐺‘𝑧) − (𝐺‘𝐶)) / (𝑧 − 𝐶))) ↾ ((𝑋 ∩ 𝑌) ∖ {𝐶})) lim_ℂ 𝐶) = ((𝑧 ∈ (𝑌 ∖ {𝐶}) ↦ (((𝐺‘𝑧) − (𝐺‘𝐶)) / (𝑧 − 𝐶))) lim_ℂ 𝐶))
214	62	resmptd 6030	. . . . . . . . . 10 ⊢ (𝜑 → ((𝑧 ∈ (𝑌 ∖ {𝐶}) ↦ (((𝐺‘𝑧) − (𝐺‘𝐶)) / (𝑧 − 𝐶))) ↾ ((𝑋 ∩ 𝑌) ∖ {𝐶})) = (𝑧 ∈ ((𝑋 ∩ 𝑌) ∖ {𝐶}) ↦ (((𝐺‘𝑧) − (𝐺‘𝐶)) / (𝑧 − 𝐶))))
215	214	oveq1d 7416	. . . . . . . . 9 ⊢ (𝜑 → (((𝑧 ∈ (𝑌 ∖ {𝐶}) ↦ (((𝐺‘𝑧) − (𝐺‘𝐶)) / (𝑧 − 𝐶))) ↾ ((𝑋 ∩ 𝑌) ∖ {𝐶})) lim_ℂ 𝐶) = ((𝑧 ∈ ((𝑋 ∩ 𝑌) ∖ {𝐶}) ↦ (((𝐺‘𝑧) − (𝐺‘𝐶)) / (𝑧 − 𝐶))) lim_ℂ 𝐶))
216	213, 215	eqtr3d 2766	. . . . . . . 8 ⊢ (𝜑 → ((𝑧 ∈ (𝑌 ∖ {𝐶}) ↦ (((𝐺‘𝑧) − (𝐺‘𝐶)) / (𝑧 − 𝐶))) lim_ℂ 𝐶) = ((𝑧 ∈ ((𝑋 ∩ 𝑌) ∖ {𝐶}) ↦ (((𝐺‘𝑧) − (𝐺‘𝐶)) / (𝑧 − 𝐶))) lim_ℂ 𝐶))
217	203, 216	eleqtrd 2827	. . . . . . 7 ⊢ (𝜑 → 𝐿 ∈ ((𝑧 ∈ ((𝑋 ∩ 𝑌) ∖ {𝐶}) ↦ (((𝐺‘𝑧) − (𝐺‘𝐶)) / (𝑧 − 𝐶))) lim_ℂ 𝐶))
218	84, 5	sstrd 3984	. . . . . . . . . 10 ⊢ (𝜑 → (𝑋 ∩ 𝑌) ⊆ ℂ)
219		cncfmptc 24754	. . . . . . . . . 10 ⊢ (((𝐹‘𝐶) ∈ ℂ ∧ (𝑋 ∩ 𝑌) ⊆ ℂ ∧ ℂ ⊆ ℂ) → (𝑧 ∈ (𝑋 ∩ 𝑌) ↦ (𝐹‘𝐶)) ∈ ((𝑋 ∩ 𝑌)–cn→ℂ))
220	43, 218, 73, 219	syl3anc 1368	. . . . . . . . 9 ⊢ (𝜑 → (𝑧 ∈ (𝑋 ∩ 𝑌) ↦ (𝐹‘𝐶)) ∈ ((𝑋 ∩ 𝑌)–cn→ℂ))
221		eqidd 2725	. . . . . . . . 9 ⊢ (𝑧 = 𝐶 → (𝐹‘𝐶) = (𝐹‘𝐶))
222	220, 127, 221	cnmptlimc 25741	. . . . . . . 8 ⊢ (𝜑 → (𝐹‘𝐶) ∈ ((𝑧 ∈ (𝑋 ∩ 𝑌) ↦ (𝐹‘𝐶)) lim_ℂ 𝐶))
223	43	adantr 480	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑧 ∈ (𝑋 ∩ 𝑌)) → (𝐹‘𝐶) ∈ ℂ)
224	223	fmpttd 7106	. . . . . . . . . 10 ⊢ (𝜑 → (𝑧 ∈ (𝑋 ∩ 𝑌) ↦ (𝐹‘𝐶)):(𝑋 ∩ 𝑌)⟶ℂ)
225	224	limcdif 25727	. . . . . . . . 9 ⊢ (𝜑 → ((𝑧 ∈ (𝑋 ∩ 𝑌) ↦ (𝐹‘𝐶)) lim_ℂ 𝐶) = (((𝑧 ∈ (𝑋 ∩ 𝑌) ↦ (𝐹‘𝐶)) ↾ ((𝑋 ∩ 𝑌) ∖ {𝐶})) lim_ℂ 𝐶))
226		resmpt 6027	. . . . . . . . . . 11 ⊢ (((𝑋 ∩ 𝑌) ∖ {𝐶}) ⊆ (𝑋 ∩ 𝑌) → ((𝑧 ∈ (𝑋 ∩ 𝑌) ↦ (𝐹‘𝐶)) ↾ ((𝑋 ∩ 𝑌) ∖ {𝐶})) = (𝑧 ∈ ((𝑋 ∩ 𝑌) ∖ {𝐶}) ↦ (𝐹‘𝐶)))
227	146, 226	mp1i 13	. . . . . . . . . 10 ⊢ (𝜑 → ((𝑧 ∈ (𝑋 ∩ 𝑌) ↦ (𝐹‘𝐶)) ↾ ((𝑋 ∩ 𝑌) ∖ {𝐶})) = (𝑧 ∈ ((𝑋 ∩ 𝑌) ∖ {𝐶}) ↦ (𝐹‘𝐶)))
228	227	oveq1d 7416	. . . . . . . . 9 ⊢ (𝜑 → (((𝑧 ∈ (𝑋 ∩ 𝑌) ↦ (𝐹‘𝐶)) ↾ ((𝑋 ∩ 𝑌) ∖ {𝐶})) lim_ℂ 𝐶) = ((𝑧 ∈ ((𝑋 ∩ 𝑌) ∖ {𝐶}) ↦ (𝐹‘𝐶)) lim_ℂ 𝐶))
229	225, 228	eqtrd 2764	. . . . . . . 8 ⊢ (𝜑 → ((𝑧 ∈ (𝑋 ∩ 𝑌) ↦ (𝐹‘𝐶)) lim_ℂ 𝐶) = ((𝑧 ∈ ((𝑋 ∩ 𝑌) ∖ {𝐶}) ↦ (𝐹‘𝐶)) lim_ℂ 𝐶))
230	222, 229	eleqtrd 2827	. . . . . . 7 ⊢ (𝜑 → (𝐹‘𝐶) ∈ ((𝑧 ∈ ((𝑋 ∩ 𝑌) ∖ {𝐶}) ↦ (𝐹‘𝐶)) lim_ℂ 𝐶))
231	5, 13, 14	dvcl 25750	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝐶(𝑆 D 𝐺)𝐿) → 𝐿 ∈ ℂ)
232	11, 231	mpdan 684	. . . . . . . . 9 ⊢ (𝜑 → 𝐿 ∈ ℂ)
233	232, 43	opelxpd 5705	. . . . . . . 8 ⊢ (𝜑 → ⟨𝐿, (𝐹‘𝐶)⟩ ∈ (ℂ × ℂ))
234	185	cncnpi 23104	. . . . . . . 8 ⊢ (((𝑢 ∈ ℂ, 𝑣 ∈ ℂ ↦ (𝑢 · 𝑣)) ∈ ((𝐽 ×_t 𝐽) Cn 𝐽) ∧ ⟨𝐿, (𝐹‘𝐶)⟩ ∈ (ℂ × ℂ)) → (𝑢 ∈ ℂ, 𝑣 ∈ ℂ ↦ (𝑢 · 𝑣)) ∈ (((𝐽 ×_t 𝐽) CnP 𝐽)‘⟨𝐿, (𝐹‘𝐶)⟩))
235	180, 233, 234	sylancr 586	. . . . . . 7 ⊢ (𝜑 → (𝑢 ∈ ℂ, 𝑣 ∈ ℂ ↦ (𝑢 · 𝑣)) ∈ (((𝐽 ×_t 𝐽) CnP 𝐽)‘⟨𝐿, (𝐹‘𝐶)⟩))
236	71, 44, 73, 73, 3, 76, 217, 230, 235	limccnp2 25743	. . . . . 6 ⊢ (𝜑 → (𝐿(𝑢 ∈ ℂ, 𝑣 ∈ ℂ ↦ (𝑢 · 𝑣))(𝐹‘𝐶)) ∈ ((𝑧 ∈ ((𝑋 ∩ 𝑌) ∖ {𝐶}) ↦ ((((𝐺‘𝑧) − (𝐺‘𝐶)) / (𝑧 − 𝐶))(𝑢 ∈ ℂ, 𝑣 ∈ ℂ ↦ (𝑢 · 𝑣))(𝐹‘𝐶))) lim_ℂ 𝐶))
237		df-mpt 5222	. . . . . . 7 ⊢ (𝑧 ∈ ((𝑋 ∩ 𝑌) ∖ {𝐶}) ↦ ((((𝐺‘𝑧) − (𝐺‘𝐶)) / (𝑧 − 𝐶))(𝑢 ∈ ℂ, 𝑣 ∈ ℂ ↦ (𝑢 · 𝑣))(𝐹‘𝐶))) = {⟨𝑧, 𝑤⟩ ∣ (𝑧 ∈ ((𝑋 ∩ 𝑌) ∖ {𝐶}) ∧ 𝑤 = ((((𝐺‘𝑧) − (𝐺‘𝐶)) / (𝑧 − 𝐶))(𝑢 ∈ ℂ, 𝑣 ∈ ℂ ↦ (𝑢 · 𝑣))(𝐹‘𝐶)))}
238	237	oveq1i 7411	. . . . . 6 ⊢ ((𝑧 ∈ ((𝑋 ∩ 𝑌) ∖ {𝐶}) ↦ ((((𝐺‘𝑧) − (𝐺‘𝐶)) / (𝑧 − 𝐶))(𝑢 ∈ ℂ, 𝑣 ∈ ℂ ↦ (𝑢 · 𝑣))(𝐹‘𝐶))) lim_ℂ 𝐶) = ({⟨𝑧, 𝑤⟩ ∣ (𝑧 ∈ ((𝑋 ∩ 𝑌) ∖ {𝐶}) ∧ 𝑤 = ((((𝐺‘𝑧) − (𝐺‘𝐶)) / (𝑧 − 𝐶))(𝑢 ∈ ℂ, 𝑣 ∈ ℂ ↦ (𝑢 · 𝑣))(𝐹‘𝐶)))} lim_ℂ 𝐶)
239	236, 238	eleqtrdi 2835	. . . . 5 ⊢ (𝜑 → (𝐿(𝑢 ∈ ℂ, 𝑣 ∈ ℂ ↦ (𝑢 · 𝑣))(𝐹‘𝐶)) ∈ ({⟨𝑧, 𝑤⟩ ∣ (𝑧 ∈ ((𝑋 ∩ 𝑌) ∖ {𝐶}) ∧ 𝑤 = ((((𝐺‘𝑧) − (𝐺‘𝐶)) / (𝑧 − 𝐶))(𝑢 ∈ ℂ, 𝑣 ∈ ℂ ↦ (𝑢 · 𝑣))(𝐹‘𝐶)))} lim_ℂ 𝐶))
240		ovmpot 7561	. . . . . 6 ⊢ ((𝐿 ∈ ℂ ∧ (𝐹‘𝐶) ∈ ℂ) → (𝐿(𝑢 ∈ ℂ, 𝑣 ∈ ℂ ↦ (𝑢 · 𝑣))(𝐹‘𝐶)) = (𝐿 · (𝐹‘𝐶)))
241	232, 43, 240	syl2anc 583	. . . . 5 ⊢ (𝜑 → (𝐿(𝑢 ∈ ℂ, 𝑣 ∈ ℂ ↦ (𝑢 · 𝑣))(𝐹‘𝐶)) = (𝐿 · (𝐹‘𝐶)))
242	42	adantr 480	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑧 ∈ ((𝑋 ∩ 𝑌) ∖ {𝐶})) → 𝐶 ∈ 𝑋)
243	32, 242	ffvelcdmd 7077	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑧 ∈ ((𝑋 ∩ 𝑌) ∖ {𝐶})) → (𝐹‘𝐶) ∈ ℂ)
244		ovmpot 7561	. . . . . . . . . . 11 ⊢ (((((𝐺‘𝑧) − (𝐺‘𝐶)) / (𝑧 − 𝐶)) ∈ ℂ ∧ (𝐹‘𝐶) ∈ ℂ) → ((((𝐺‘𝑧) − (𝐺‘𝐶)) / (𝑧 − 𝐶))(𝑢 ∈ ℂ, 𝑣 ∈ ℂ ↦ (𝑢 · 𝑣))(𝐹‘𝐶)) = ((((𝐺‘𝑧) − (𝐺‘𝐶)) / (𝑧 − 𝐶)) · (𝐹‘𝐶)))
245	71, 243, 244	syl2anc 583	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑧 ∈ ((𝑋 ∩ 𝑌) ∖ {𝐶})) → ((((𝐺‘𝑧) − (𝐺‘𝐶)) / (𝑧 − 𝐶))(𝑢 ∈ ℂ, 𝑣 ∈ ℂ ↦ (𝑢 · 𝑣))(𝐹‘𝐶)) = ((((𝐺‘𝑧) − (𝐺‘𝐶)) / (𝑧 − 𝐶)) · (𝐹‘𝐶)))
246	245	eqeq2d 2735	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑧 ∈ ((𝑋 ∩ 𝑌) ∖ {𝐶})) → (𝑤 = ((((𝐺‘𝑧) − (𝐺‘𝐶)) / (𝑧 − 𝐶))(𝑢 ∈ ℂ, 𝑣 ∈ ℂ ↦ (𝑢 · 𝑣))(𝐹‘𝐶)) ↔ 𝑤 = ((((𝐺‘𝑧) − (𝐺‘𝐶)) / (𝑧 − 𝐶)) · (𝐹‘𝐶))))
247	246	pm5.32da 578	. . . . . . . 8 ⊢ (𝜑 → ((𝑧 ∈ ((𝑋 ∩ 𝑌) ∖ {𝐶}) ∧ 𝑤 = ((((𝐺‘𝑧) − (𝐺‘𝐶)) / (𝑧 − 𝐶))(𝑢 ∈ ℂ, 𝑣 ∈ ℂ ↦ (𝑢 · 𝑣))(𝐹‘𝐶))) ↔ (𝑧 ∈ ((𝑋 ∩ 𝑌) ∖ {𝐶}) ∧ 𝑤 = ((((𝐺‘𝑧) − (𝐺‘𝐶)) / (𝑧 − 𝐶)) · (𝐹‘𝐶)))))
248	247	opabbidv 5204	. . . . . . 7 ⊢ (𝜑 → {⟨𝑧, 𝑤⟩ ∣ (𝑧 ∈ ((𝑋 ∩ 𝑌) ∖ {𝐶}) ∧ 𝑤 = ((((𝐺‘𝑧) − (𝐺‘𝐶)) / (𝑧 − 𝐶))(𝑢 ∈ ℂ, 𝑣 ∈ ℂ ↦ (𝑢 · 𝑣))(𝐹‘𝐶)))} = {⟨𝑧, 𝑤⟩ ∣ (𝑧 ∈ ((𝑋 ∩ 𝑌) ∖ {𝐶}) ∧ 𝑤 = ((((𝐺‘𝑧) − (𝐺‘𝐶)) / (𝑧 − 𝐶)) · (𝐹‘𝐶)))})
249		df-mpt 5222	. . . . . . 7 ⊢ (𝑧 ∈ ((𝑋 ∩ 𝑌) ∖ {𝐶}) ↦ ((((𝐺‘𝑧) − (𝐺‘𝐶)) / (𝑧 − 𝐶)) · (𝐹‘𝐶))) = {⟨𝑧, 𝑤⟩ ∣ (𝑧 ∈ ((𝑋 ∩ 𝑌) ∖ {𝐶}) ∧ 𝑤 = ((((𝐺‘𝑧) − (𝐺‘𝐶)) / (𝑧 − 𝐶)) · (𝐹‘𝐶)))}
250	248, 249	eqtr4di 2782	. . . . . 6 ⊢ (𝜑 → {⟨𝑧, 𝑤⟩ ∣ (𝑧 ∈ ((𝑋 ∩ 𝑌) ∖ {𝐶}) ∧ 𝑤 = ((((𝐺‘𝑧) − (𝐺‘𝐶)) / (𝑧 − 𝐶))(𝑢 ∈ ℂ, 𝑣 ∈ ℂ ↦ (𝑢 · 𝑣))(𝐹‘𝐶)))} = (𝑧 ∈ ((𝑋 ∩ 𝑌) ∖ {𝐶}) ↦ ((((𝐺‘𝑧) − (𝐺‘𝐶)) / (𝑧 − 𝐶)) · (𝐹‘𝐶))))
251	250	oveq1d 7416	. . . . 5 ⊢ (𝜑 → ({⟨𝑧, 𝑤⟩ ∣ (𝑧 ∈ ((𝑋 ∩ 𝑌) ∖ {𝐶}) ∧ 𝑤 = ((((𝐺‘𝑧) − (𝐺‘𝐶)) / (𝑧 − 𝐶))(𝑢 ∈ ℂ, 𝑣 ∈ ℂ ↦ (𝑢 · 𝑣))(𝐹‘𝐶)))} lim_ℂ 𝐶) = ((𝑧 ∈ ((𝑋 ∩ 𝑌) ∖ {𝐶}) ↦ ((((𝐺‘𝑧) − (𝐺‘𝐶)) / (𝑧 − 𝐶)) · (𝐹‘𝐶))) lim_ℂ 𝐶))
252	239, 241, 251	3eltr3d 2839	. . . 4 ⊢ (𝜑 → (𝐿 · (𝐹‘𝐶)) ∈ ((𝑧 ∈ ((𝑋 ∩ 𝑌) ∖ {𝐶}) ↦ ((((𝐺‘𝑧) − (𝐺‘𝐶)) / (𝑧 − 𝐶)) · (𝐹‘𝐶))) lim_ℂ 𝐶))
253	3	addcn 24703	. . . . 5 ⊢ + ∈ ((𝐽 ×_t 𝐽) Cn 𝐽)
254	182, 183	mulcld 11231	. . . . . 6 ⊢ (𝜑 → (𝐾 · (𝐺‘𝐶)) ∈ ℂ)
255	232, 43	mulcld 11231	. . . . . 6 ⊢ (𝜑 → (𝐿 · (𝐹‘𝐶)) ∈ ℂ)
256	254, 255	opelxpd 5705	. . . . 5 ⊢ (𝜑 → ⟨(𝐾 · (𝐺‘𝐶)), (𝐿 · (𝐹‘𝐶))⟩ ∈ (ℂ × ℂ))
257	185	cncnpi 23104	. . . . 5 ⊢ (( + ∈ ((𝐽 ×_t 𝐽) Cn 𝐽) ∧ ⟨(𝐾 · (𝐺‘𝐶)), (𝐿 · (𝐹‘𝐶))⟩ ∈ (ℂ × ℂ)) → + ∈ (((𝐽 ×_t 𝐽) CnP 𝐽)‘⟨(𝐾 · (𝐺‘𝐶)), (𝐿 · (𝐹‘𝐶))⟩))
258	253, 256, 257	sylancr 586	. . . 4 ⊢ (𝜑 → + ∈ (((𝐽 ×_t 𝐽) CnP 𝐽)‘⟨(𝐾 · (𝐺‘𝐶)), (𝐿 · (𝐹‘𝐶))⟩))
259	60, 72, 73, 73, 3, 76, 202, 252, 258	limccnp2 25743	. . 3 ⊢ (𝜑 → ((𝐾 · (𝐺‘𝐶)) + (𝐿 · (𝐹‘𝐶))) ∈ ((𝑧 ∈ ((𝑋 ∩ 𝑌) ∖ {𝐶}) ↦ (((((𝐹‘𝑧) − (𝐹‘𝐶)) / (𝑧 − 𝐶)) · (𝐺‘𝑧)) + ((((𝐺‘𝑧) − (𝐺‘𝐶)) / (𝑧 − 𝐶)) · (𝐹‘𝐶)))) lim_ℂ 𝐶))
260	37, 243	subcld 11568	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑧 ∈ ((𝑋 ∩ 𝑌) ∖ {𝐶})) → ((𝐹‘𝑧) − (𝐹‘𝐶)) ∈ ℂ)
261	260, 59	mulcld 11231	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑧 ∈ ((𝑋 ∩ 𝑌) ∖ {𝐶})) → (((𝐹‘𝑧) − (𝐹‘𝐶)) · (𝐺‘𝑧)) ∈ ℂ)
262	69	adantr 480	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑧 ∈ ((𝑋 ∩ 𝑌) ∖ {𝐶})) → 𝐶 ∈ 𝑌)
263	56, 262	ffvelcdmd 7077	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑧 ∈ ((𝑋 ∩ 𝑌) ∖ {𝐶})) → (𝐺‘𝐶) ∈ ℂ)
264	59, 263	subcld 11568	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑧 ∈ ((𝑋 ∩ 𝑌) ∖ {𝐶})) → ((𝐺‘𝑧) − (𝐺‘𝐶)) ∈ ℂ)
265	264, 243	mulcld 11231	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑧 ∈ ((𝑋 ∩ 𝑌) ∖ {𝐶})) → (((𝐺‘𝑧) − (𝐺‘𝐶)) · (𝐹‘𝐶)) ∈ ℂ)
266	47, 242	sseldd 3975	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑧 ∈ ((𝑋 ∩ 𝑌) ∖ {𝐶})) → 𝐶 ∈ ℂ)
267	48, 266	subcld 11568	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑧 ∈ ((𝑋 ∩ 𝑌) ∖ {𝐶})) → (𝑧 − 𝐶) ∈ ℂ)
268	261, 265, 267, 54	divdird 12025	. . . . . 6 ⊢ ((𝜑 ∧ 𝑧 ∈ ((𝑋 ∩ 𝑌) ∖ {𝐶})) → (((((𝐹‘𝑧) − (𝐹‘𝐶)) · (𝐺‘𝑧)) + (((𝐺‘𝑧) − (𝐺‘𝐶)) · (𝐹‘𝐶))) / (𝑧 − 𝐶)) = (((((𝐹‘𝑧) − (𝐹‘𝐶)) · (𝐺‘𝑧)) / (𝑧 − 𝐶)) + ((((𝐺‘𝑧) − (𝐺‘𝐶)) · (𝐹‘𝐶)) / (𝑧 − 𝐶))))
269	37, 59	mulcld 11231	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑧 ∈ ((𝑋 ∩ 𝑌) ∖ {𝐶})) → ((𝐹‘𝑧) · (𝐺‘𝑧)) ∈ ℂ)
270	243, 59	mulcld 11231	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑧 ∈ ((𝑋 ∩ 𝑌) ∖ {𝐶})) → ((𝐹‘𝐶) · (𝐺‘𝑧)) ∈ ℂ)
271	243, 263	mulcld 11231	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑧 ∈ ((𝑋 ∩ 𝑌) ∖ {𝐶})) → ((𝐹‘𝐶) · (𝐺‘𝐶)) ∈ ℂ)
272	269, 270, 271	npncand 11592	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑧 ∈ ((𝑋 ∩ 𝑌) ∖ {𝐶})) → ((((𝐹‘𝑧) · (𝐺‘𝑧)) − ((𝐹‘𝐶) · (𝐺‘𝑧))) + (((𝐹‘𝐶) · (𝐺‘𝑧)) − ((𝐹‘𝐶) · (𝐺‘𝐶)))) = (((𝐹‘𝑧) · (𝐺‘𝑧)) − ((𝐹‘𝐶) · (𝐺‘𝐶))))
273	37, 243, 59	subdird 11668	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑧 ∈ ((𝑋 ∩ 𝑌) ∖ {𝐶})) → (((𝐹‘𝑧) − (𝐹‘𝐶)) · (𝐺‘𝑧)) = (((𝐹‘𝑧) · (𝐺‘𝑧)) − ((𝐹‘𝐶) · (𝐺‘𝑧))))
274	264, 243	mulcomd 11232	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑧 ∈ ((𝑋 ∩ 𝑌) ∖ {𝐶})) → (((𝐺‘𝑧) − (𝐺‘𝐶)) · (𝐹‘𝐶)) = ((𝐹‘𝐶) · ((𝐺‘𝑧) − (𝐺‘𝐶))))
275	243, 59, 263	subdid 11667	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑧 ∈ ((𝑋 ∩ 𝑌) ∖ {𝐶})) → ((𝐹‘𝐶) · ((𝐺‘𝑧) − (𝐺‘𝐶))) = (((𝐹‘𝐶) · (𝐺‘𝑧)) − ((𝐹‘𝐶) · (𝐺‘𝐶))))
276	274, 275	eqtrd 2764	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑧 ∈ ((𝑋 ∩ 𝑌) ∖ {𝐶})) → (((𝐺‘𝑧) − (𝐺‘𝐶)) · (𝐹‘𝐶)) = (((𝐹‘𝐶) · (𝐺‘𝑧)) − ((𝐹‘𝐶) · (𝐺‘𝐶))))
277	273, 276	oveq12d 7419	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑧 ∈ ((𝑋 ∩ 𝑌) ∖ {𝐶})) → ((((𝐹‘𝑧) − (𝐹‘𝐶)) · (𝐺‘𝑧)) + (((𝐺‘𝑧) − (𝐺‘𝐶)) · (𝐹‘𝐶))) = ((((𝐹‘𝑧) · (𝐺‘𝑧)) − ((𝐹‘𝐶) · (𝐺‘𝑧))) + (((𝐹‘𝐶) · (𝐺‘𝑧)) − ((𝐹‘𝐶) · (𝐺‘𝐶)))))
278	6	ffnd 6708	. . . . . . . . . . . 12 ⊢ (𝜑 → 𝐹 Fn 𝑋)
279	278	adantr 480	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑧 ∈ ((𝑋 ∩ 𝑌) ∖ {𝐶})) → 𝐹 Fn 𝑋)
280	13	ffnd 6708	. . . . . . . . . . . 12 ⊢ (𝜑 → 𝐺 Fn 𝑌)
281	280	adantr 480	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑧 ∈ ((𝑋 ∩ 𝑌) ∖ {𝐶})) → 𝐺 Fn 𝑌)
282		ssexg 5313	. . . . . . . . . . . . 13 ⊢ ((𝑋 ⊆ ℂ ∧ ℂ ∈ V) → 𝑋 ∈ V)
283	46, 110, 282	sylancl 585	. . . . . . . . . . . 12 ⊢ (𝜑 → 𝑋 ∈ V)
284	283	adantr 480	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑧 ∈ ((𝑋 ∩ 𝑌) ∖ {𝐶})) → 𝑋 ∈ V)
285		ssexg 5313	. . . . . . . . . . . . 13 ⊢ ((𝑌 ⊆ ℂ ∧ ℂ ∈ V) → 𝑌 ∈ V)
286	64, 110, 285	sylancl 585	. . . . . . . . . . . 12 ⊢ (𝜑 → 𝑌 ∈ V)
287	286	adantr 480	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑧 ∈ ((𝑋 ∩ 𝑌) ∖ {𝐶})) → 𝑌 ∈ V)
288		eqid 2724	. . . . . . . . . . 11 ⊢ (𝑋 ∩ 𝑌) = (𝑋 ∩ 𝑌)
289		eqidd 2725	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑧 ∈ ((𝑋 ∩ 𝑌) ∖ {𝐶})) ∧ 𝑧 ∈ 𝑋) → (𝐹‘𝑧) = (𝐹‘𝑧))
290		eqidd 2725	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑧 ∈ ((𝑋 ∩ 𝑌) ∖ {𝐶})) ∧ 𝑧 ∈ 𝑌) → (𝐺‘𝑧) = (𝐺‘𝑧))
291	279, 281, 284, 287, 288, 289, 290	ofval 7674	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑧 ∈ ((𝑋 ∩ 𝑌) ∖ {𝐶})) ∧ 𝑧 ∈ (𝑋 ∩ 𝑌)) → ((𝐹 ∘_f · 𝐺)‘𝑧) = ((𝐹‘𝑧) · (𝐺‘𝑧)))
292	35, 291	mpdan 684	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑧 ∈ ((𝑋 ∩ 𝑌) ∖ {𝐶})) → ((𝐹 ∘_f · 𝐺)‘𝑧) = ((𝐹‘𝑧) · (𝐺‘𝑧)))
293		eqidd 2725	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑧 ∈ ((𝑋 ∩ 𝑌) ∖ {𝐶})) ∧ 𝐶 ∈ 𝑋) → (𝐹‘𝐶) = (𝐹‘𝐶))
294		eqidd 2725	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑧 ∈ ((𝑋 ∩ 𝑌) ∖ {𝐶})) ∧ 𝐶 ∈ 𝑌) → (𝐺‘𝐶) = (𝐺‘𝐶))
295	279, 281, 284, 287, 288, 293, 294	ofval 7674	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑧 ∈ ((𝑋 ∩ 𝑌) ∖ {𝐶})) ∧ 𝐶 ∈ (𝑋 ∩ 𝑌)) → ((𝐹 ∘_f · 𝐺)‘𝐶) = ((𝐹‘𝐶) · (𝐺‘𝐶)))
296	127, 295	mpidan 686	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑧 ∈ ((𝑋 ∩ 𝑌) ∖ {𝐶})) → ((𝐹 ∘_f · 𝐺)‘𝐶) = ((𝐹‘𝐶) · (𝐺‘𝐶)))
297	292, 296	oveq12d 7419	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑧 ∈ ((𝑋 ∩ 𝑌) ∖ {𝐶})) → (((𝐹 ∘_f · 𝐺)‘𝑧) − ((𝐹 ∘_f · 𝐺)‘𝐶)) = (((𝐹‘𝑧) · (𝐺‘𝑧)) − ((𝐹‘𝐶) · (𝐺‘𝐶))))
298	272, 277, 297	3eqtr4d 2774	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑧 ∈ ((𝑋 ∩ 𝑌) ∖ {𝐶})) → ((((𝐹‘𝑧) − (𝐹‘𝐶)) · (𝐺‘𝑧)) + (((𝐺‘𝑧) − (𝐺‘𝐶)) · (𝐹‘𝐶))) = (((𝐹 ∘_f · 𝐺)‘𝑧) − ((𝐹 ∘_f · 𝐺)‘𝐶)))
299	298	oveq1d 7416	. . . . . 6 ⊢ ((𝜑 ∧ 𝑧 ∈ ((𝑋 ∩ 𝑌) ∖ {𝐶})) → (((((𝐹‘𝑧) − (𝐹‘𝐶)) · (𝐺‘𝑧)) + (((𝐺‘𝑧) − (𝐺‘𝐶)) · (𝐹‘𝐶))) / (𝑧 − 𝐶)) = ((((𝐹 ∘_f · 𝐺)‘𝑧) − ((𝐹 ∘_f · 𝐺)‘𝐶)) / (𝑧 − 𝐶)))
300	260, 59, 267, 54	div23d 12024	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑧 ∈ ((𝑋 ∩ 𝑌) ∖ {𝐶})) → ((((𝐹‘𝑧) − (𝐹‘𝐶)) · (𝐺‘𝑧)) / (𝑧 − 𝐶)) = ((((𝐹‘𝑧) − (𝐹‘𝐶)) / (𝑧 − 𝐶)) · (𝐺‘𝑧)))
301	264, 243, 267, 54	div23d 12024	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑧 ∈ ((𝑋 ∩ 𝑌) ∖ {𝐶})) → ((((𝐺‘𝑧) − (𝐺‘𝐶)) · (𝐹‘𝐶)) / (𝑧 − 𝐶)) = ((((𝐺‘𝑧) − (𝐺‘𝐶)) / (𝑧 − 𝐶)) · (𝐹‘𝐶)))
302	300, 301	oveq12d 7419	. . . . . 6 ⊢ ((𝜑 ∧ 𝑧 ∈ ((𝑋 ∩ 𝑌) ∖ {𝐶})) → (((((𝐹‘𝑧) − (𝐹‘𝐶)) · (𝐺‘𝑧)) / (𝑧 − 𝐶)) + ((((𝐺‘𝑧) − (𝐺‘𝐶)) · (𝐹‘𝐶)) / (𝑧 − 𝐶))) = (((((𝐹‘𝑧) − (𝐹‘𝐶)) / (𝑧 − 𝐶)) · (𝐺‘𝑧)) + ((((𝐺‘𝑧) − (𝐺‘𝐶)) / (𝑧 − 𝐶)) · (𝐹‘𝐶))))
303	268, 299, 302	3eqtr3d 2772	. . . . 5 ⊢ ((𝜑 ∧ 𝑧 ∈ ((𝑋 ∩ 𝑌) ∖ {𝐶})) → ((((𝐹 ∘_f · 𝐺)‘𝑧) − ((𝐹 ∘_f · 𝐺)‘𝐶)) / (𝑧 − 𝐶)) = (((((𝐹‘𝑧) − (𝐹‘𝐶)) / (𝑧 − 𝐶)) · (𝐺‘𝑧)) + ((((𝐺‘𝑧) − (𝐺‘𝐶)) / (𝑧 − 𝐶)) · (𝐹‘𝐶))))
304	303	mpteq2dva 5238	. . . 4 ⊢ (𝜑 → (𝑧 ∈ ((𝑋 ∩ 𝑌) ∖ {𝐶}) ↦ ((((𝐹 ∘_f · 𝐺)‘𝑧) − ((𝐹 ∘_f · 𝐺)‘𝐶)) / (𝑧 − 𝐶))) = (𝑧 ∈ ((𝑋 ∩ 𝑌) ∖ {𝐶}) ↦ (((((𝐹‘𝑧) − (𝐹‘𝐶)) / (𝑧 − 𝐶)) · (𝐺‘𝑧)) + ((((𝐺‘𝑧) − (𝐺‘𝐶)) / (𝑧 − 𝐶)) · (𝐹‘𝐶)))))
305	304	oveq1d 7416	. . 3 ⊢ (𝜑 → ((𝑧 ∈ ((𝑋 ∩ 𝑌) ∖ {𝐶}) ↦ ((((𝐹 ∘_f · 𝐺)‘𝑧) − ((𝐹 ∘_f · 𝐺)‘𝐶)) / (𝑧 − 𝐶))) lim_ℂ 𝐶) = ((𝑧 ∈ ((𝑋 ∩ 𝑌) ∖ {𝐶}) ↦ (((((𝐹‘𝑧) − (𝐹‘𝐶)) / (𝑧 − 𝐶)) · (𝐺‘𝑧)) + ((((𝐺‘𝑧) − (𝐺‘𝐶)) / (𝑧 − 𝐶)) · (𝐹‘𝐶)))) lim_ℂ 𝐶))
306	259, 305	eleqtrrd 2828	. 2 ⊢ (𝜑 → ((𝐾 · (𝐺‘𝐶)) + (𝐿 · (𝐹‘𝐶))) ∈ ((𝑧 ∈ ((𝑋 ∩ 𝑌) ∖ {𝐶}) ↦ ((((𝐹 ∘_f · 𝐺)‘𝑧) − ((𝐹 ∘_f · 𝐺)‘𝐶)) / (𝑧 − 𝐶))) lim_ℂ 𝐶))
307		eqid 2724	. . 3 ⊢ (𝑧 ∈ ((𝑋 ∩ 𝑌) ∖ {𝐶}) ↦ ((((𝐹 ∘_f · 𝐺)‘𝑧) − ((𝐹 ∘_f · 𝐺)‘𝐶)) / (𝑧 − 𝐶))) = (𝑧 ∈ ((𝑋 ∩ 𝑌) ∖ {𝐶}) ↦ ((((𝐹 ∘_f · 𝐺)‘𝑧) − ((𝐹 ∘_f · 𝐺)‘𝐶)) / (𝑧 − 𝐶)))
308		mulcl 11190	. . . . 5 ⊢ ((𝑥 ∈ ℂ ∧ 𝑦 ∈ ℂ) → (𝑥 · 𝑦) ∈ ℂ)
309	308	adantl 481	. . . 4 ⊢ ((𝜑 ∧ (𝑥 ∈ ℂ ∧ 𝑦 ∈ ℂ)) → (𝑥 · 𝑦) ∈ ℂ)
310	309, 6, 13, 283, 286, 288	off 7681	. . 3 ⊢ (𝜑 → (𝐹 ∘_f · 𝐺):(𝑋 ∩ 𝑌)⟶ℂ)
311	2, 3, 307, 5, 310, 84	eldv 25749	. 2 ⊢ (𝜑 → (𝐶(𝑆 D (𝐹 ∘_f · 𝐺))((𝐾 · (𝐺‘𝐶)) + (𝐿 · (𝐹‘𝐶))) ↔ (𝐶 ∈ ((int‘(𝐽 ↾_t 𝑆))‘(𝑋 ∩ 𝑌)) ∧ ((𝐾 · (𝐺‘𝐶)) + (𝐿 · (𝐹‘𝐶))) ∈ ((𝑧 ∈ ((𝑋 ∩ 𝑌) ∖ {𝐶}) ↦ ((((𝐹 ∘_f · 𝐺)‘𝑧) − ((𝐹 ∘_f · 𝐺)‘𝐶)) / (𝑧 − 𝐶))) lim_ℂ 𝐶))))
312	31, 306, 311	mpbir2and 710	1 ⊢ (𝜑 → 𝐶(𝑆 D (𝐹 ∘_f · 𝐺))((𝐾 · (𝐺‘𝐶)) + (𝐿 · (𝐹‘𝐶))))

Colors of variables: wff setvar class

Syntax hints: → wi 4 ↔ wb 205 ∧ wa 395 = wceq 1533 ∈ wcel 2098 ≠ wne 2932 Vcvv 3466 ∖ cdif 3937 ∪ cun 3938 ∩ cin 3939 ⊆ wss 3940 {csn 4620 ⟨cop 4626 ∪ cuni 4899 class class class wbr 5138 {copab 5200 ↦ cmpt 5221 × cxp 5664 dom cdm 5666 ↾ cres 5668 Rel wrel 5671 Fn wfn 6528 ⟶wf 6529 ‘cfv 6533 (class class class)co 7401 ∈ cmpo 7403 ∘_f cof 7661 ℂcc 11104 + caddc 11109 · cmul 11111 − cmin 11441 / cdiv 11868 ↾_t crest 17365 TopOpenctopn 17366 ℂ_fldccnfld 21228 Topctop 22717 TopOnctopon 22734 intcnt 22843 Cn ccn 23050 CnP ccnp 23051 ×_t ctx 23386 –cn→ccncf 24718 lim_ℂ climc 25713 D cdv 25714

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1789 ax-4 1803 ax-5 1905 ax-6 1963 ax-7 2003 ax-8 2100 ax-9 2108 ax-10 2129 ax-11 2146 ax-12 2163 ax-ext 2695 ax-rep 5275 ax-sep 5289 ax-nul 5296 ax-pow 5353 ax-pr 5417 ax-un 7718 ax-cnex 11162 ax-resscn 11163 ax-1cn 11164 ax-icn 11165 ax-addcl 11166 ax-addrcl 11167 ax-mulcl 11168 ax-mulrcl 11169 ax-mulcom 11170 ax-addass 11171 ax-mulass 11172 ax-distr 11173 ax-i2m1 11174 ax-1ne0 11175 ax-1rid 11176 ax-rnegex 11177 ax-rrecex 11178 ax-cnre 11179 ax-pre-lttri 11180 ax-pre-lttrn 11181 ax-pre-ltadd 11182 ax-pre-mulgt0 11183 ax-pre-sup 11184 ax-addf 11185

This theorem depends on definitions: df-bi 206 df-an 396 df-or 845 df-3or 1085 df-3an 1086 df-tru 1536 df-fal 1546 df-ex 1774 df-nf 1778 df-sb 2060 df-mo 2526 df-eu 2555 df-clab 2702 df-cleq 2716 df-clel 2802 df-nfc 2877 df-ne 2933 df-nel 3039 df-ral 3054 df-rex 3063 df-rmo 3368 df-reu 3369 df-rab 3425 df-v 3468 df-sbc 3770 df-csb 3886 df-dif 3943 df-un 3945 df-in 3947 df-ss 3957 df-pss 3959 df-nul 4315 df-if 4521 df-pw 4596 df-sn 4621 df-pr 4623 df-tp 4625 df-op 4627 df-uni 4900 df-int 4941 df-iun 4989 df-iin 4990 df-br 5139 df-opab 5201 df-mpt 5222 df-tr 5256 df-id 5564 df-eprel 5570 df-po 5578 df-so 5579 df-fr 5621 df-se 5622 df-we 5623 df-xp 5672 df-rel 5673 df-cnv 5674 df-co 5675 df-dm 5676 df-rn 5677 df-res 5678 df-ima 5679 df-pred 6290 df-ord 6357 df-on 6358 df-lim 6359 df-suc 6360 df-iota 6485 df-fun 6535 df-fn 6536 df-f 6537 df-f1 6538 df-fo 6539 df-f1o 6540 df-fv 6541 df-isom 6542 df-riota 7357 df-ov 7404 df-oprab 7405 df-mpo 7406 df-of 7663 df-om 7849 df-1st 7968 df-2nd 7969 df-supp 8141 df-frecs 8261 df-wrecs 8292 df-recs 8366 df-rdg 8405 df-1o 8461 df-2o 8462 df-er 8699 df-map 8818 df-pm 8819 df-ixp 8888 df-en 8936 df-dom 8937 df-sdom 8938 df-fin 8939 df-fsupp 9358 df-fi 9402 df-sup 9433 df-inf 9434 df-oi 9501 df-card 9930 df-pnf 11247 df-mnf 11248 df-xr 11249 df-ltxr 11250 df-le 11251 df-sub 11443 df-neg 11444 df-div 11869 df-nn 12210 df-2 12272 df-3 12273 df-4 12274 df-5 12275 df-6 12276 df-7 12277 df-8 12278 df-9 12279 df-n0 12470 df-z 12556 df-dec 12675 df-uz 12820 df-q 12930 df-rp 12972 df-xneg 13089 df-xadd 13090 df-xmul 13091 df-icc 13328 df-fz 13482 df-fzo 13625 df-seq 13964 df-exp 14025 df-hash 14288 df-cj 15043 df-re 15044 df-im 15045 df-sqrt 15179 df-abs 15180 df-struct 17079 df-sets 17096 df-slot 17114 df-ndx 17126 df-base 17144 df-ress 17173 df-plusg 17209 df-mulr 17210 df-starv 17211 df-sca 17212 df-vsca 17213 df-ip 17214 df-tset 17215 df-ple 17216 df-ds 17218 df-unif 17219 df-hom 17220 df-cco 17221 df-rest 17367 df-topn 17368 df-0g 17386 df-gsum 17387 df-topgen 17388 df-pt 17389 df-prds 17392 df-xrs 17447 df-qtop 17452 df-imas 17453 df-xps 17455 df-mre 17529 df-mrc 17530 df-acs 17532 df-mgm 18563 df-sgrp 18642 df-mnd 18658 df-submnd 18704 df-mulg 18986 df-cntz 19223 df-cmn 19692 df-psmet 21220 df-xmet 21221 df-met 21222 df-bl 21223 df-mopn 21224 df-cnfld 21229 df-top 22718 df-topon 22735 df-topsp 22757 df-bases 22771 df-cld 22845 df-ntr 22846 df-cls 22847 df-cn 23053 df-cnp 23054 df-tx 23388 df-hmeo 23581 df-xms 24148 df-ms 24149 df-tms 24150 df-cncf 24720 df-limc 25717 df-dv 25718

This theorem is referenced by: dvmul 25794 dvmulf 25796 dvef 25834

W3C validator