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 26259

Description: The product rule for derivatives at a point. For the (simpler but more limited) function version, see dvmul 26261. (Contributed by Mario Carneiro, 9-Aug-2014.) (Revised by Mario Carneiro, 28-Dec-2016.) Avoid ax-mulf 11280 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 2761	. . . . . . 7 ⊢ (𝐽 ↾_t 𝑆) = (𝐽 ↾_t 𝑆)
3		dvadd.j	. . . . . . 7 ⊢ 𝐽 = (TopOpen‘ℂ_fld)
4		eqid 2761	. . . . . . 7 ⊢ (𝑧 ∈ (𝑋 ∖ {𝐶}) ↦ (((𝐹‘𝑧) − (𝐹‘𝐶)) / (𝑧 − 𝐶))) = (𝑧 ∈ (𝑋 ∖ {𝐶}) ↦ (((𝐹‘𝑧) − (𝐹‘𝐶)) / (𝑧 − 𝐶)))
5		dvaddbr.s	. . . . . . 7 ⊢ (𝜑 → 𝑆 ⊆ ℂ)
6		dvadd.f	. . . . . . 7 ⊢ (𝜑 → 𝐹:𝑋⟶ℂ)
7		dvadd.x	. . . . . . 7 ⊢ (𝜑 → 𝑋 ⊆ 𝑆)
8	2, 3, 4, 5, 6, 7	eldv 26218	. . . . . 6 ⊢ (𝜑 → (𝐶(𝑆 D 𝐹)𝐾 ↔ (𝐶 ∈ ((int‘(𝐽 ↾_t 𝑆))‘𝑋) ∧ 𝐾 ∈ ((𝑧 ∈ (𝑋 ∖ {𝐶}) ↦ (((𝐹‘𝑧) − (𝐹‘𝐶)) / (𝑧 − 𝐶))) lim_ℂ 𝐶))))
9	1, 8	mpbid 235	. . . . 5 ⊢ (𝜑 → (𝐶 ∈ ((int‘(𝐽 ↾_t 𝑆))‘𝑋) ∧ 𝐾 ∈ ((𝑧 ∈ (𝑋 ∖ {𝐶}) ↦ (((𝐹‘𝑧) − (𝐹‘𝐶)) / (𝑧 − 𝐶))) lim_ℂ 𝐶)))
10	9	simpld 500	. . . 4 ⊢ (𝜑 → 𝐶 ∈ ((int‘(𝐽 ↾_t 𝑆))‘𝑋))
11		dvadd.bg	. . . . . 6 ⊢ (𝜑 → 𝐶(𝑆 D 𝐺)𝐿)
12		eqid 2761	. . . . . . 7 ⊢ (𝑧 ∈ (𝑌 ∖ {𝐶}) ↦ (((𝐺‘𝑧) − (𝐺‘𝐶)) / (𝑧 − 𝐶))) = (𝑧 ∈ (𝑌 ∖ {𝐶}) ↦ (((𝐺‘𝑧) − (𝐺‘𝐶)) / (𝑧 − 𝐶)))
13		dvadd.g	. . . . . . 7 ⊢ (𝜑 → 𝐺:𝑌⟶ℂ)
14		dvadd.y	. . . . . . 7 ⊢ (𝜑 → 𝑌 ⊆ 𝑆)
15	2, 3, 12, 5, 13, 14	eldv 26218	. . . . . 6 ⊢ (𝜑 → (𝐶(𝑆 D 𝐺)𝐿 ↔ (𝐶 ∈ ((int‘(𝐽 ↾_t 𝑆))‘𝑌) ∧ 𝐿 ∈ ((𝑧 ∈ (𝑌 ∖ {𝐶}) ↦ (((𝐺‘𝑧) − (𝐺‘𝐶)) / (𝑧 − 𝐶))) lim_ℂ 𝐶))))
16	11, 15	mpbid 235	. . . . 5 ⊢ (𝜑 → (𝐶 ∈ ((int‘(𝐽 ↾_t 𝑆))‘𝑌) ∧ 𝐿 ∈ ((𝑧 ∈ (𝑌 ∖ {𝐶}) ↦ (((𝐺‘𝑧) − (𝐺‘𝐶)) / (𝑧 − 𝐶))) lim_ℂ 𝐶)))
17	16	simpld 500	. . . 4 ⊢ (𝜑 → 𝐶 ∈ ((int‘(𝐽 ↾_t 𝑆))‘𝑌))
18	10, 17	elind 4146	. . 3 ⊢ (𝜑 → 𝐶 ∈ (((int‘(𝐽 ↾_t 𝑆))‘𝑋) ∩ ((int‘(𝐽 ↾_t 𝑆))‘𝑌)))
19	3	cnfldtopon 25101	. . . . . 6 ⊢ 𝐽 ∈ (TopOn‘ℂ)
20		resttopon 23479	. . . . . 6 ⊢ ((𝐽 ∈ (TopOn‘ℂ) ∧ 𝑆 ⊆ ℂ) → (𝐽 ↾_t 𝑆) ∈ (TopOn‘𝑆))
21	19, 5, 20	sylancr 599	. . . . 5 ⊢ (𝜑 → (𝐽 ↾_t 𝑆) ∈ (TopOn‘𝑆))
22		topontop 23231	. . . . 5 ⊢ ((𝐽 ↾_t 𝑆) ∈ (TopOn‘𝑆) → (𝐽 ↾_t 𝑆) ∈ Top)
23	21, 22	syl 18	. . . 4 ⊢ (𝜑 → (𝐽 ↾_t 𝑆) ∈ Top)
24		toponuni 23232	. . . . . 6 ⊢ ((𝐽 ↾_t 𝑆) ∈ (TopOn‘𝑆) → 𝑆 = ∪ (𝐽 ↾_t 𝑆))
25	21, 24	syl 18	. . . . 5 ⊢ (𝜑 → 𝑆 = ∪ (𝐽 ↾_t 𝑆))
26	7, 25	sseqtrd 3967	. . . 4 ⊢ (𝜑 → 𝑋 ⊆ ∪ (𝐽 ↾_t 𝑆))
27	14, 25	sseqtrd 3967	. . . 4 ⊢ (𝜑 → 𝑌 ⊆ ∪ (𝐽 ↾_t 𝑆))
28		eqid 2761	. . . . 5 ⊢ ∪ (𝐽 ↾_t 𝑆) = ∪ (𝐽 ↾_t 𝑆)
29	28	ntrin 23379	. . . 4 ⊢ (((𝐽 ↾_t 𝑆) ∈ Top ∧ 𝑋 ⊆ ∪ (𝐽 ↾_t 𝑆) ∧ 𝑌 ⊆ ∪ (𝐽 ↾_t 𝑆)) → ((int‘(𝐽 ↾_t 𝑆))‘(𝑋 ∩ 𝑌)) = (((int‘(𝐽 ↾_t 𝑆))‘𝑋) ∩ ((int‘(𝐽 ↾_t 𝑆))‘𝑌)))
30	23, 26, 27, 29	syl3anc 1398	. . 3 ⊢ (𝜑 → ((int‘(𝐽 ↾_t 𝑆))‘(𝑋 ∩ 𝑌)) = (((int‘(𝐽 ↾_t 𝑆))‘𝑋) ∩ ((int‘(𝐽 ↾_t 𝑆))‘𝑌)))
31	18, 30	eleqtrrd 2864	. 2 ⊢ (𝜑 → 𝐶 ∈ ((int‘(𝐽 ↾_t 𝑆))‘(𝑋 ∩ 𝑌)))
32	6	adantr 486	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑧 ∈ ((𝑋 ∩ 𝑌) ∖ {𝐶})) → 𝐹:𝑋⟶ℂ)
33		inss1 4182	. . . . . . . . 9 ⊢ (𝑋 ∩ 𝑌) ⊆ 𝑋
34		eldifi 4078	. . . . . . . . . 10 ⊢ (𝑧 ∈ ((𝑋 ∩ 𝑌) ∖ {𝐶}) → 𝑧 ∈ (𝑋 ∩ 𝑌))
35	34	adantl 487	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑧 ∈ ((𝑋 ∩ 𝑌) ∖ {𝐶})) → 𝑧 ∈ (𝑋 ∩ 𝑌))
36	33, 35	sselid 3929	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑧 ∈ ((𝑋 ∩ 𝑌) ∖ {𝐶})) → 𝑧 ∈ 𝑋)
37	32, 36	ffvelcdmd 7085	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑧 ∈ ((𝑋 ∩ 𝑌) ∖ {𝐶})) → (𝐹‘𝑧) ∈ ℂ)
38	5, 6, 7	dvbss 26221	. . . . . . . . . 10 ⊢ (𝜑 → dom (𝑆 D 𝐹) ⊆ 𝑋)
39		reldv 26190	. . . . . . . . . . 11 ⊢ Rel (𝑆 D 𝐹)
40		releldm 5926	. . . . . . . . . . 11 ⊢ ((Rel (𝑆 D 𝐹) ∧ 𝐶(𝑆 D 𝐹)𝐾) → 𝐶 ∈ dom (𝑆 D 𝐹))
41	39, 1, 40	sylancr 599	. . . . . . . . . 10 ⊢ (𝜑 → 𝐶 ∈ dom (𝑆 D 𝐹))
42	38, 41	sseldd 3932	. . . . . . . . 9 ⊢ (𝜑 → 𝐶 ∈ 𝑋)
43	6, 42	ffvelcdmd 7085	. . . . . . . 8 ⊢ (𝜑 → (𝐹‘𝐶) ∈ ℂ)
44	43	adantr 486	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑧 ∈ ((𝑋 ∩ 𝑌) ∖ {𝐶})) → (𝐹‘𝐶) ∈ ℂ)
45	37, 44	subcld 11669	. . . . . 6 ⊢ ((𝜑 ∧ 𝑧 ∈ ((𝑋 ∩ 𝑌) ∖ {𝐶})) → ((𝐹‘𝑧) − (𝐹‘𝐶)) ∈ ℂ)
46	7, 5	sstrd 3941	. . . . . . . . 9 ⊢ (𝜑 → 𝑋 ⊆ ℂ)
47	46	adantr 486	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑧 ∈ ((𝑋 ∩ 𝑌) ∖ {𝐶})) → 𝑋 ⊆ ℂ)
48	47, 36	sseldd 3932	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑧 ∈ ((𝑋 ∩ 𝑌) ∖ {𝐶})) → 𝑧 ∈ ℂ)
49	46, 42	sseldd 3932	. . . . . . . 8 ⊢ (𝜑 → 𝐶 ∈ ℂ)
50	49	adantr 486	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑧 ∈ ((𝑋 ∩ 𝑌) ∖ {𝐶})) → 𝐶 ∈ ℂ)
51	48, 50	subcld 11669	. . . . . 6 ⊢ ((𝜑 ∧ 𝑧 ∈ ((𝑋 ∩ 𝑌) ∖ {𝐶})) → (𝑧 − 𝐶) ∈ ℂ)
52		eldifsni 4753	. . . . . . . 8 ⊢ (𝑧 ∈ ((𝑋 ∩ 𝑌) ∖ {𝐶}) → 𝑧 ≠ 𝐶)
53	52	adantl 487	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑧 ∈ ((𝑋 ∩ 𝑌) ∖ {𝐶})) → 𝑧 ≠ 𝐶)
54	48, 50, 53	subne0d 11679	. . . . . 6 ⊢ ((𝜑 ∧ 𝑧 ∈ ((𝑋 ∩ 𝑌) ∖ {𝐶})) → (𝑧 − 𝐶) ≠ 0)
55	45, 51, 54	divcld 12093	. . . . 5 ⊢ ((𝜑 ∧ 𝑧 ∈ ((𝑋 ∩ 𝑌) ∖ {𝐶})) → (((𝐹‘𝑧) − (𝐹‘𝐶)) / (𝑧 − 𝐶)) ∈ ℂ)
56	13	adantr 486	. . . . . 6 ⊢ ((𝜑 ∧ 𝑧 ∈ ((𝑋 ∩ 𝑌) ∖ {𝐶})) → 𝐺:𝑌⟶ℂ)
57		inss2 4183	. . . . . . 7 ⊢ (𝑋 ∩ 𝑌) ⊆ 𝑌
58	57, 35	sselid 3929	. . . . . 6 ⊢ ((𝜑 ∧ 𝑧 ∈ ((𝑋 ∩ 𝑌) ∖ {𝐶})) → 𝑧 ∈ 𝑌)
59	56, 58	ffvelcdmd 7085	. . . . 5 ⊢ ((𝜑 ∧ 𝑧 ∈ ((𝑋 ∩ 𝑌) ∖ {𝐶})) → (𝐺‘𝑧) ∈ ℂ)
60	55, 59	mulcld 11329	. . . 4 ⊢ ((𝜑 ∧ 𝑧 ∈ ((𝑋 ∩ 𝑌) ∖ {𝐶})) → ((((𝐹‘𝑧) − (𝐹‘𝐶)) / (𝑧 − 𝐶)) · (𝐺‘𝑧)) ∈ ℂ)
61		ssdif 4091	. . . . . . . 8 ⊢ ((𝑋 ∩ 𝑌) ⊆ 𝑌 → ((𝑋 ∩ 𝑌) ∖ {𝐶}) ⊆ (𝑌 ∖ {𝐶}))
62	57, 61	mp1i 14	. . . . . . 7 ⊢ (𝜑 → ((𝑋 ∩ 𝑌) ∖ {𝐶}) ⊆ (𝑌 ∖ {𝐶}))
63	62	sselda 3931	. . . . . 6 ⊢ ((𝜑 ∧ 𝑧 ∈ ((𝑋 ∩ 𝑌) ∖ {𝐶})) → 𝑧 ∈ (𝑌 ∖ {𝐶}))
64	14, 5	sstrd 3941	. . . . . . 7 ⊢ (𝜑 → 𝑌 ⊆ ℂ)
65	5, 13, 14	dvbss 26221	. . . . . . . 8 ⊢ (𝜑 → dom (𝑆 D 𝐺) ⊆ 𝑌)
66		reldv 26190	. . . . . . . . 9 ⊢ Rel (𝑆 D 𝐺)
67		releldm 5926	. . . . . . . . 9 ⊢ ((Rel (𝑆 D 𝐺) ∧ 𝐶(𝑆 D 𝐺)𝐿) → 𝐶 ∈ dom (𝑆 D 𝐺))
68	66, 11, 67	sylancr 599	. . . . . . . 8 ⊢ (𝜑 → 𝐶 ∈ dom (𝑆 D 𝐺))
69	65, 68	sseldd 3932	. . . . . . 7 ⊢ (𝜑 → 𝐶 ∈ 𝑌)
70	13, 64, 69	dvlem 26216	. . . . . 6 ⊢ ((𝜑 ∧ 𝑧 ∈ (𝑌 ∖ {𝐶})) → (((𝐺‘𝑧) − (𝐺‘𝐶)) / (𝑧 − 𝐶)) ∈ ℂ)
71	63, 70	syldan 603	. . . . 5 ⊢ ((𝜑 ∧ 𝑧 ∈ ((𝑋 ∩ 𝑌) ∖ {𝐶})) → (((𝐺‘𝑧) − (𝐺‘𝐶)) / (𝑧 − 𝐶)) ∈ ℂ)
72	71, 44	mulcld 11329	. . . 4 ⊢ ((𝜑 ∧ 𝑧 ∈ ((𝑋 ∩ 𝑌) ∖ {𝐶})) → ((((𝐺‘𝑧) − (𝐺‘𝐶)) / (𝑧 − 𝐶)) · (𝐹‘𝐶)) ∈ ℂ)
73		ssidd 3954	. . . 4 ⊢ (𝜑 → ℂ ⊆ ℂ)
74		txtopon 23910	. . . . . 6 ⊢ ((𝐽 ∈ (TopOn‘ℂ) ∧ 𝐽 ∈ (TopOn‘ℂ)) → (𝐽 ×_t 𝐽) ∈ (TopOn‘(ℂ × ℂ)))
75	19, 19, 74	mp2an 705	. . . . 5 ⊢ (𝐽 ×_t 𝐽) ∈ (TopOn‘(ℂ × ℂ))
76	75	toponrestid 23239	. . . 4 ⊢ (𝐽 ×_t 𝐽) = ((𝐽 ×_t 𝐽) ↾_t (ℂ × ℂ))
77	9	simprd 501	. . . . . . . 8 ⊢ (𝜑 → 𝐾 ∈ ((𝑧 ∈ (𝑋 ∖ {𝐶}) ↦ (((𝐹‘𝑧) − (𝐹‘𝐶)) / (𝑧 − 𝐶))) lim_ℂ 𝐶))
78	6, 46, 42	dvlem 26216	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑧 ∈ (𝑋 ∖ {𝐶})) → (((𝐹‘𝑧) − (𝐹‘𝐶)) / (𝑧 − 𝐶)) ∈ ℂ)
79	78	fmpttd 7115	. . . . . . . . . 10 ⊢ (𝜑 → (𝑧 ∈ (𝑋 ∖ {𝐶}) ↦ (((𝐹‘𝑧) − (𝐹‘𝐶)) / (𝑧 − 𝐶))):(𝑋 ∖ {𝐶})⟶ℂ)
80		ssdif 4091	. . . . . . . . . . 11 ⊢ ((𝑋 ∩ 𝑌) ⊆ 𝑋 → ((𝑋 ∩ 𝑌) ∖ {𝐶}) ⊆ (𝑋 ∖ {𝐶}))
81	33, 80	mp1i 14	. . . . . . . . . 10 ⊢ (𝜑 → ((𝑋 ∩ 𝑌) ∖ {𝐶}) ⊆ (𝑋 ∖ {𝐶}))
82	46	ssdifssd 4094	. . . . . . . . . 10 ⊢ (𝜑 → (𝑋 ∖ {𝐶}) ⊆ ℂ)
83		eqid 2761	. . . . . . . . . 10 ⊢ (𝐽 ↾_t ((𝑋 ∖ {𝐶}) ∪ {𝐶})) = (𝐽 ↾_t ((𝑋 ∖ {𝐶}) ∪ {𝐶}))
84	33, 7	sstrid 3942	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → (𝑋 ∩ 𝑌) ⊆ 𝑆)
85	84, 25	sseqtrd 3967	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (𝑋 ∩ 𝑌) ⊆ ∪ (𝐽 ↾_t 𝑆))
86		difssd 4084	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (∪ (𝐽 ↾_t 𝑆) ∖ 𝑋) ⊆ ∪ (𝐽 ↾_t 𝑆))
87	85, 86	unssd 4138	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → ((𝑋 ∩ 𝑌) ∪ (∪ (𝐽 ↾_t 𝑆) ∖ 𝑋)) ⊆ ∪ (𝐽 ↾_t 𝑆))
88		ssun1 4124	. . . . . . . . . . . . . . . 16 ⊢ (𝑋 ∩ 𝑌) ⊆ ((𝑋 ∩ 𝑌) ∪ (∪ (𝐽 ↾_t 𝑆) ∖ 𝑋))
89	88	a1i 11	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (𝑋 ∩ 𝑌) ⊆ ((𝑋 ∩ 𝑌) ∪ (∪ (𝐽 ↾_t 𝑆) ∖ 𝑋)))
90	28	ntrss 23373	. . . . . . . . . . . . . . 15 ⊢ (((𝐽 ↾_t 𝑆) ∈ Top ∧ ((𝑋 ∩ 𝑌) ∪ (∪ (𝐽 ↾_t 𝑆) ∖ 𝑋)) ⊆ ∪ (𝐽 ↾_t 𝑆) ∧ (𝑋 ∩ 𝑌) ⊆ ((𝑋 ∩ 𝑌) ∪ (∪ (𝐽 ↾_t 𝑆) ∖ 𝑋))) → ((int‘(𝐽 ↾_t 𝑆))‘(𝑋 ∩ 𝑌)) ⊆ ((int‘(𝐽 ↾_t 𝑆))‘((𝑋 ∩ 𝑌) ∪ (∪ (𝐽 ↾_t 𝑆) ∖ 𝑋))))
91	23, 87, 89, 90	syl3anc 1398	. . . . . . . . . . . . . 14 ⊢ (𝜑 → ((int‘(𝐽 ↾_t 𝑆))‘(𝑋 ∩ 𝑌)) ⊆ ((int‘(𝐽 ↾_t 𝑆))‘((𝑋 ∩ 𝑌) ∪ (∪ (𝐽 ↾_t 𝑆) ∖ 𝑋))))
92		eqid 2761	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑥 ∈ (𝑋 ∖ {𝐶}) ↦ (((𝐹‘𝑥) − (𝐹‘𝐶)) / (𝑥 − 𝐶))) = (𝑥 ∈ (𝑋 ∖ {𝐶}) ↦ (((𝐹‘𝑥) − (𝐹‘𝐶)) / (𝑥 − 𝐶)))
93	2, 3, 92, 5, 6, 7	eldv 26218	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → (𝐶(𝑆 D 𝐹)𝐾 ↔ (𝐶 ∈ ((int‘(𝐽 ↾_t 𝑆))‘𝑋) ∧ 𝐾 ∈ ((𝑥 ∈ (𝑋 ∖ {𝐶}) ↦ (((𝐹‘𝑥) − (𝐹‘𝐶)) / (𝑥 − 𝐶))) lim_ℂ 𝐶))))
94	1, 93	mpbid 235	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → (𝐶 ∈ ((int‘(𝐽 ↾_t 𝑆))‘𝑋) ∧ 𝐾 ∈ ((𝑥 ∈ (𝑋 ∖ {𝐶}) ↦ (((𝐹‘𝑥) − (𝐹‘𝐶)) / (𝑥 − 𝐶))) lim_ℂ 𝐶)))
95	94	simpld 500	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → 𝐶 ∈ ((int‘(𝐽 ↾_t 𝑆))‘𝑋))
96		eqid 2761	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑥 ∈ (𝑌 ∖ {𝐶}) ↦ (((𝐺‘𝑥) − (𝐺‘𝐶)) / (𝑥 − 𝐶))) = (𝑥 ∈ (𝑌 ∖ {𝐶}) ↦ (((𝐺‘𝑥) − (𝐺‘𝐶)) / (𝑥 − 𝐶)))
97	2, 3, 96, 5, 13, 14	eldv 26218	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → (𝐶(𝑆 D 𝐺)𝐿 ↔ (𝐶 ∈ ((int‘(𝐽 ↾_t 𝑆))‘𝑌) ∧ 𝐿 ∈ ((𝑥 ∈ (𝑌 ∖ {𝐶}) ↦ (((𝐺‘𝑥) − (𝐺‘𝐶)) / (𝑥 − 𝐶))) lim_ℂ 𝐶))))
98	11, 97	mpbid 235	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → (𝐶 ∈ ((int‘(𝐽 ↾_t 𝑆))‘𝑌) ∧ 𝐿 ∈ ((𝑥 ∈ (𝑌 ∖ {𝐶}) ↦ (((𝐺‘𝑥) − (𝐺‘𝐶)) / (𝑥 − 𝐶))) lim_ℂ 𝐶)))
99	98	simpld 500	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → 𝐶 ∈ ((int‘(𝐽 ↾_t 𝑆))‘𝑌))
100	95, 99	elind 4146	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → 𝐶 ∈ (((int‘(𝐽 ↾_t 𝑆))‘𝑋) ∩ ((int‘(𝐽 ↾_t 𝑆))‘𝑌)))
101	100, 30	eleqtrrd 2864	. . . . . . . . . . . . . 14 ⊢ (𝜑 → 𝐶 ∈ ((int‘(𝐽 ↾_t 𝑆))‘(𝑋 ∩ 𝑌)))
102	91, 101	sseldd 3932	. . . . . . . . . . . . 13 ⊢ (𝜑 → 𝐶 ∈ ((int‘(𝐽 ↾_t 𝑆))‘((𝑋 ∩ 𝑌) ∪ (∪ (𝐽 ↾_t 𝑆) ∖ 𝑋))))
103	102, 42	elind 4146	. . . . . . . . . . . 12 ⊢ (𝜑 → 𝐶 ∈ (((int‘(𝐽 ↾_t 𝑆))‘((𝑋 ∩ 𝑌) ∪ (∪ (𝐽 ↾_t 𝑆) ∖ 𝑋))) ∩ 𝑋))
104	33	a1i 11	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (𝑋 ∩ 𝑌) ⊆ 𝑋)
105		eqid 2761	. . . . . . . . . . . . . . 15 ⊢ ((𝐽 ↾_t 𝑆) ↾_t 𝑋) = ((𝐽 ↾_t 𝑆) ↾_t 𝑋)
106	28, 105	restntr 23500	. . . . . . . . . . . . . 14 ⊢ (((𝐽 ↾_t 𝑆) ∈ Top ∧ 𝑋 ⊆ ∪ (𝐽 ↾_t 𝑆) ∧ (𝑋 ∩ 𝑌) ⊆ 𝑋) → ((int‘((𝐽 ↾_t 𝑆) ↾_t 𝑋))‘(𝑋 ∩ 𝑌)) = (((int‘(𝐽 ↾_t 𝑆))‘((𝑋 ∩ 𝑌) ∪ (∪ (𝐽 ↾_t 𝑆) ∖ 𝑋))) ∩ 𝑋))
107	23, 26, 104, 106	syl3anc 1398	. . . . . . . . . . . . 13 ⊢ (𝜑 → ((int‘((𝐽 ↾_t 𝑆) ↾_t 𝑋))‘(𝑋 ∩ 𝑌)) = (((int‘(𝐽 ↾_t 𝑆))‘((𝑋 ∩ 𝑌) ∪ (∪ (𝐽 ↾_t 𝑆) ∖ 𝑋))) ∩ 𝑋))
108	3	cnfldtop 25102	. . . . . . . . . . . . . . . . 17 ⊢ 𝐽 ∈ Top
109	108	a1i 11	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → 𝐽 ∈ Top)
110		cnex 11281	. . . . . . . . . . . . . . . . 17 ⊢ ℂ ∈ V
111		ssexg 5281	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑆 ⊆ ℂ ∧ ℂ ∈ V) → 𝑆 ∈ V)
112	5, 110, 111	sylancl 598	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → 𝑆 ∈ V)
113		restabs 23483	. . . . . . . . . . . . . . . 16 ⊢ ((𝐽 ∈ Top ∧ 𝑋 ⊆ 𝑆 ∧ 𝑆 ∈ V) → ((𝐽 ↾_t 𝑆) ↾_t 𝑋) = (𝐽 ↾_t 𝑋))
114	109, 7, 112, 113	syl3anc 1398	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → ((𝐽 ↾_t 𝑆) ↾_t 𝑋) = (𝐽 ↾_t 𝑋))
115	114	fveq2d 6889	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (int‘((𝐽 ↾_t 𝑆) ↾_t 𝑋)) = (int‘(𝐽 ↾_t 𝑋)))
116	115	fveq1d 6887	. . . . . . . . . . . . 13 ⊢ (𝜑 → ((int‘((𝐽 ↾_t 𝑆) ↾_t 𝑋))‘(𝑋 ∩ 𝑌)) = ((int‘(𝐽 ↾_t 𝑋))‘(𝑋 ∩ 𝑌)))
117	107, 116	eqtr3d 2798	. . . . . . . . . . . 12 ⊢ (𝜑 → (((int‘(𝐽 ↾_t 𝑆))‘((𝑋 ∩ 𝑌) ∪ (∪ (𝐽 ↾_t 𝑆) ∖ 𝑋))) ∩ 𝑋) = ((int‘(𝐽 ↾_t 𝑋))‘(𝑋 ∩ 𝑌)))
118	103, 117	eleqtrd 2863	. . . . . . . . . . 11 ⊢ (𝜑 → 𝐶 ∈ ((int‘(𝐽 ↾_t 𝑋))‘(𝑋 ∩ 𝑌)))
119		undif1 4430	. . . . . . . . . . . . . . 15 ⊢ ((𝑋 ∖ {𝐶}) ∪ {𝐶}) = (𝑋 ∪ {𝐶})
120	42	snssd 4747	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → {𝐶} ⊆ 𝑋)
121		ssequn2 4135	. . . . . . . . . . . . . . . 16 ⊢ ({𝐶} ⊆ 𝑋 ↔ (𝑋 ∪ {𝐶}) = 𝑋)
122	120, 121	sylib 221	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (𝑋 ∪ {𝐶}) = 𝑋)
123	119, 122	eqtrid 2808	. . . . . . . . . . . . . 14 ⊢ (𝜑 → ((𝑋 ∖ {𝐶}) ∪ {𝐶}) = 𝑋)
124	123	oveq2d 7436	. . . . . . . . . . . . 13 ⊢ (𝜑 → (𝐽 ↾_t ((𝑋 ∖ {𝐶}) ∪ {𝐶})) = (𝐽 ↾_t 𝑋))
125	124	fveq2d 6889	. . . . . . . . . . . 12 ⊢ (𝜑 → (int‘(𝐽 ↾_t ((𝑋 ∖ {𝐶}) ∪ {𝐶}))) = (int‘(𝐽 ↾_t 𝑋)))
126		undif1 4430	. . . . . . . . . . . . 13 ⊢ (((𝑋 ∩ 𝑌) ∖ {𝐶}) ∪ {𝐶}) = ((𝑋 ∩ 𝑌) ∪ {𝐶})
127	42, 69	elind 4146	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → 𝐶 ∈ (𝑋 ∩ 𝑌))
128	127	snssd 4747	. . . . . . . . . . . . . 14 ⊢ (𝜑 → {𝐶} ⊆ (𝑋 ∩ 𝑌))
129		ssequn2 4135	. . . . . . . . . . . . . 14 ⊢ ({𝐶} ⊆ (𝑋 ∩ 𝑌) ↔ ((𝑋 ∩ 𝑌) ∪ {𝐶}) = (𝑋 ∩ 𝑌))
130	128, 129	sylib 221	. . . . . . . . . . . . 13 ⊢ (𝜑 → ((𝑋 ∩ 𝑌) ∪ {𝐶}) = (𝑋 ∩ 𝑌))
131	126, 130	eqtrid 2808	. . . . . . . . . . . 12 ⊢ (𝜑 → (((𝑋 ∩ 𝑌) ∖ {𝐶}) ∪ {𝐶}) = (𝑋 ∩ 𝑌))
132	125, 131	fveq12d 6892	. . . . . . . . . . 11 ⊢ (𝜑 → ((int‘(𝐽 ↾_t ((𝑋 ∖ {𝐶}) ∪ {𝐶})))‘(((𝑋 ∩ 𝑌) ∖ {𝐶}) ∪ {𝐶})) = ((int‘(𝐽 ↾_t 𝑋))‘(𝑋 ∩ 𝑌)))
133	118, 132	eleqtrrd 2864	. . . . . . . . . 10 ⊢ (𝜑 → 𝐶 ∈ ((int‘(𝐽 ↾_t ((𝑋 ∖ {𝐶}) ∪ {𝐶})))‘(((𝑋 ∩ 𝑌) ∖ {𝐶}) ∪ {𝐶})))
134	79, 81, 82, 3, 83, 133	limcres 26206	. . . . . . . . 9 ⊢ (𝜑 → (((𝑧 ∈ (𝑋 ∖ {𝐶}) ↦ (((𝐹‘𝑧) − (𝐹‘𝐶)) / (𝑧 − 𝐶))) ↾ ((𝑋 ∩ 𝑌) ∖ {𝐶})) lim_ℂ 𝐶) = ((𝑧 ∈ (𝑋 ∖ {𝐶}) ↦ (((𝐹‘𝑧) − (𝐹‘𝐶)) / (𝑧 − 𝐶))) lim_ℂ 𝐶))
135	81	resmptd 6032	. . . . . . . . . 10 ⊢ (𝜑 → ((𝑧 ∈ (𝑋 ∖ {𝐶}) ↦ (((𝐹‘𝑧) − (𝐹‘𝐶)) / (𝑧 − 𝐶))) ↾ ((𝑋 ∩ 𝑌) ∖ {𝐶})) = (𝑧 ∈ ((𝑋 ∩ 𝑌) ∖ {𝐶}) ↦ (((𝐹‘𝑧) − (𝐹‘𝐶)) / (𝑧 − 𝐶))))
136	135	oveq1d 7435	. . . . . . . . 9 ⊢ (𝜑 → (((𝑧 ∈ (𝑋 ∖ {𝐶}) ↦ (((𝐹‘𝑧) − (𝐹‘𝐶)) / (𝑧 − 𝐶))) ↾ ((𝑋 ∩ 𝑌) ∖ {𝐶})) lim_ℂ 𝐶) = ((𝑧 ∈ ((𝑋 ∩ 𝑌) ∖ {𝐶}) ↦ (((𝐹‘𝑧) − (𝐹‘𝐶)) / (𝑧 − 𝐶))) lim_ℂ 𝐶))
137	134, 136	eqtr3d 2798	. . . . . . . 8 ⊢ (𝜑 → ((𝑧 ∈ (𝑋 ∖ {𝐶}) ↦ (((𝐹‘𝑧) − (𝐹‘𝐶)) / (𝑧 − 𝐶))) lim_ℂ 𝐶) = ((𝑧 ∈ ((𝑋 ∩ 𝑌) ∖ {𝐶}) ↦ (((𝐹‘𝑧) − (𝐹‘𝐶)) / (𝑧 − 𝐶))) lim_ℂ 𝐶))
138	77, 137	eleqtrd 2863	. . . . . . 7 ⊢ (𝜑 → 𝐾 ∈ ((𝑧 ∈ ((𝑋 ∩ 𝑌) ∖ {𝐶}) ↦ (((𝐹‘𝑧) − (𝐹‘𝐶)) / (𝑧 − 𝐶))) lim_ℂ 𝐶))
139		eqid 2761	. . . . . . . . . . . 12 ⊢ (𝐽 ↾_t 𝑌) = (𝐽 ↾_t 𝑌)
140	139, 3	dvcnp2 26240	. . . . . . . . . . 11 ⊢ (((𝑆 ⊆ ℂ ∧ 𝐺:𝑌⟶ℂ ∧ 𝑌 ⊆ 𝑆) ∧ 𝐶 ∈ dom (𝑆 D 𝐺)) → 𝐺 ∈ (((𝐽 ↾_t 𝑌) CnP 𝐽)‘𝐶))
141	5, 13, 14, 68, 140	syl31anc 1400	. . . . . . . . . 10 ⊢ (𝜑 → 𝐺 ∈ (((𝐽 ↾_t 𝑌) CnP 𝐽)‘𝐶))
142	3, 139	cnplimc 26207	. . . . . . . . . . 11 ⊢ ((𝑌 ⊆ ℂ ∧ 𝐶 ∈ 𝑌) → (𝐺 ∈ (((𝐽 ↾_t 𝑌) CnP 𝐽)‘𝐶) ↔ (𝐺:𝑌⟶ℂ ∧ (𝐺‘𝐶) ∈ (𝐺 lim_ℂ 𝐶))))
143	64, 69, 142	syl2anc 596	. . . . . . . . . 10 ⊢ (𝜑 → (𝐺 ∈ (((𝐽 ↾_t 𝑌) CnP 𝐽)‘𝐶) ↔ (𝐺:𝑌⟶ℂ ∧ (𝐺‘𝐶) ∈ (𝐺 lim_ℂ 𝐶))))
144	141, 143	mpbid 235	. . . . . . . . 9 ⊢ (𝜑 → (𝐺:𝑌⟶ℂ ∧ (𝐺‘𝐶) ∈ (𝐺 lim_ℂ 𝐶)))
145	144	simprd 501	. . . . . . . 8 ⊢ (𝜑 → (𝐺‘𝐶) ∈ (𝐺 lim_ℂ 𝐶))
146		difss 4083	. . . . . . . . . . . 12 ⊢ ((𝑋 ∩ 𝑌) ∖ {𝐶}) ⊆ (𝑋 ∩ 𝑌)
147	146, 57	sstri 3940	. . . . . . . . . . 11 ⊢ ((𝑋 ∩ 𝑌) ∖ {𝐶}) ⊆ 𝑌
148	147	a1i 11	. . . . . . . . . 10 ⊢ (𝜑 → ((𝑋 ∩ 𝑌) ∖ {𝐶}) ⊆ 𝑌)
149		eqid 2761	. . . . . . . . . 10 ⊢ (𝐽 ↾_t (𝑌 ∪ {𝐶})) = (𝐽 ↾_t (𝑌 ∪ {𝐶}))
150		difssd 4084	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (∪ (𝐽 ↾_t 𝑆) ∖ 𝑌) ⊆ ∪ (𝐽 ↾_t 𝑆))
151	85, 150	unssd 4138	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → ((𝑋 ∩ 𝑌) ∪ (∪ (𝐽 ↾_t 𝑆) ∖ 𝑌)) ⊆ ∪ (𝐽 ↾_t 𝑆))
152		ssun1 4124	. . . . . . . . . . . . . . . 16 ⊢ (𝑋 ∩ 𝑌) ⊆ ((𝑋 ∩ 𝑌) ∪ (∪ (𝐽 ↾_t 𝑆) ∖ 𝑌))
153	152	a1i 11	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (𝑋 ∩ 𝑌) ⊆ ((𝑋 ∩ 𝑌) ∪ (∪ (𝐽 ↾_t 𝑆) ∖ 𝑌)))
154	28	ntrss 23373	. . . . . . . . . . . . . . 15 ⊢ (((𝐽 ↾_t 𝑆) ∈ Top ∧ ((𝑋 ∩ 𝑌) ∪ (∪ (𝐽 ↾_t 𝑆) ∖ 𝑌)) ⊆ ∪ (𝐽 ↾_t 𝑆) ∧ (𝑋 ∩ 𝑌) ⊆ ((𝑋 ∩ 𝑌) ∪ (∪ (𝐽 ↾_t 𝑆) ∖ 𝑌))) → ((int‘(𝐽 ↾_t 𝑆))‘(𝑋 ∩ 𝑌)) ⊆ ((int‘(𝐽 ↾_t 𝑆))‘((𝑋 ∩ 𝑌) ∪ (∪ (𝐽 ↾_t 𝑆) ∖ 𝑌))))
155	23, 151, 153, 154	syl3anc 1398	. . . . . . . . . . . . . 14 ⊢ (𝜑 → ((int‘(𝐽 ↾_t 𝑆))‘(𝑋 ∩ 𝑌)) ⊆ ((int‘(𝐽 ↾_t 𝑆))‘((𝑋 ∩ 𝑌) ∪ (∪ (𝐽 ↾_t 𝑆) ∖ 𝑌))))
156	155, 101	sseldd 3932	. . . . . . . . . . . . 13 ⊢ (𝜑 → 𝐶 ∈ ((int‘(𝐽 ↾_t 𝑆))‘((𝑋 ∩ 𝑌) ∪ (∪ (𝐽 ↾_t 𝑆) ∖ 𝑌))))
157	156, 69	elind 4146	. . . . . . . . . . . 12 ⊢ (𝜑 → 𝐶 ∈ (((int‘(𝐽 ↾_t 𝑆))‘((𝑋 ∩ 𝑌) ∪ (∪ (𝐽 ↾_t 𝑆) ∖ 𝑌))) ∩ 𝑌))
158	57	a1i 11	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (𝑋 ∩ 𝑌) ⊆ 𝑌)
159		eqid 2761	. . . . . . . . . . . . . . 15 ⊢ ((𝐽 ↾_t 𝑆) ↾_t 𝑌) = ((𝐽 ↾_t 𝑆) ↾_t 𝑌)
160	28, 159	restntr 23500	. . . . . . . . . . . . . 14 ⊢ (((𝐽 ↾_t 𝑆) ∈ Top ∧ 𝑌 ⊆ ∪ (𝐽 ↾_t 𝑆) ∧ (𝑋 ∩ 𝑌) ⊆ 𝑌) → ((int‘((𝐽 ↾_t 𝑆) ↾_t 𝑌))‘(𝑋 ∩ 𝑌)) = (((int‘(𝐽 ↾_t 𝑆))‘((𝑋 ∩ 𝑌) ∪ (∪ (𝐽 ↾_t 𝑆) ∖ 𝑌))) ∩ 𝑌))
161	23, 27, 158, 160	syl3anc 1398	. . . . . . . . . . . . 13 ⊢ (𝜑 → ((int‘((𝐽 ↾_t 𝑆) ↾_t 𝑌))‘(𝑋 ∩ 𝑌)) = (((int‘(𝐽 ↾_t 𝑆))‘((𝑋 ∩ 𝑌) ∪ (∪ (𝐽 ↾_t 𝑆) ∖ 𝑌))) ∩ 𝑌))
162		restabs 23483	. . . . . . . . . . . . . . . 16 ⊢ ((𝐽 ∈ Top ∧ 𝑌 ⊆ 𝑆 ∧ 𝑆 ∈ V) → ((𝐽 ↾_t 𝑆) ↾_t 𝑌) = (𝐽 ↾_t 𝑌))
163	109, 14, 112, 162	syl3anc 1398	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → ((𝐽 ↾_t 𝑆) ↾_t 𝑌) = (𝐽 ↾_t 𝑌))
164	163	fveq2d 6889	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (int‘((𝐽 ↾_t 𝑆) ↾_t 𝑌)) = (int‘(𝐽 ↾_t 𝑌)))
165	164	fveq1d 6887	. . . . . . . . . . . . 13 ⊢ (𝜑 → ((int‘((𝐽 ↾_t 𝑆) ↾_t 𝑌))‘(𝑋 ∩ 𝑌)) = ((int‘(𝐽 ↾_t 𝑌))‘(𝑋 ∩ 𝑌)))
166	161, 165	eqtr3d 2798	. . . . . . . . . . . 12 ⊢ (𝜑 → (((int‘(𝐽 ↾_t 𝑆))‘((𝑋 ∩ 𝑌) ∪ (∪ (𝐽 ↾_t 𝑆) ∖ 𝑌))) ∩ 𝑌) = ((int‘(𝐽 ↾_t 𝑌))‘(𝑋 ∩ 𝑌)))
167	157, 166	eleqtrd 2863	. . . . . . . . . . 11 ⊢ (𝜑 → 𝐶 ∈ ((int‘(𝐽 ↾_t 𝑌))‘(𝑋 ∩ 𝑌)))
168	69	snssd 4747	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → {𝐶} ⊆ 𝑌)
169		ssequn2 4135	. . . . . . . . . . . . . . 15 ⊢ ({𝐶} ⊆ 𝑌 ↔ (𝑌 ∪ {𝐶}) = 𝑌)
170	168, 169	sylib 221	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (𝑌 ∪ {𝐶}) = 𝑌)
171	170	oveq2d 7436	. . . . . . . . . . . . 13 ⊢ (𝜑 → (𝐽 ↾_t (𝑌 ∪ {𝐶})) = (𝐽 ↾_t 𝑌))
172	171	fveq2d 6889	. . . . . . . . . . . 12 ⊢ (𝜑 → (int‘(𝐽 ↾_t (𝑌 ∪ {𝐶}))) = (int‘(𝐽 ↾_t 𝑌)))
173	172, 131	fveq12d 6892	. . . . . . . . . . 11 ⊢ (𝜑 → ((int‘(𝐽 ↾_t (𝑌 ∪ {𝐶})))‘(((𝑋 ∩ 𝑌) ∖ {𝐶}) ∪ {𝐶})) = ((int‘(𝐽 ↾_t 𝑌))‘(𝑋 ∩ 𝑌)))
174	167, 173	eleqtrrd 2864	. . . . . . . . . 10 ⊢ (𝜑 → 𝐶 ∈ ((int‘(𝐽 ↾_t (𝑌 ∪ {𝐶})))‘(((𝑋 ∩ 𝑌) ∖ {𝐶}) ∪ {𝐶})))
175	13, 148, 64, 3, 149, 174	limcres 26206	. . . . . . . . 9 ⊢ (𝜑 → ((𝐺 ↾ ((𝑋 ∩ 𝑌) ∖ {𝐶})) lim_ℂ 𝐶) = (𝐺 lim_ℂ 𝐶))
176	13, 148	feqresmpt 6954	. . . . . . . . . 10 ⊢ (𝜑 → (𝐺 ↾ ((𝑋 ∩ 𝑌) ∖ {𝐶})) = (𝑧 ∈ ((𝑋 ∩ 𝑌) ∖ {𝐶}) ↦ (𝐺‘𝑧)))
177	176	oveq1d 7435	. . . . . . . . 9 ⊢ (𝜑 → ((𝐺 ↾ ((𝑋 ∩ 𝑌) ∖ {𝐶})) lim_ℂ 𝐶) = ((𝑧 ∈ ((𝑋 ∩ 𝑌) ∖ {𝐶}) ↦ (𝐺‘𝑧)) lim_ℂ 𝐶))
178	175, 177	eqtr3d 2798	. . . . . . . 8 ⊢ (𝜑 → (𝐺 lim_ℂ 𝐶) = ((𝑧 ∈ ((𝑋 ∩ 𝑌) ∖ {𝐶}) ↦ (𝐺‘𝑧)) lim_ℂ 𝐶))
179	145, 178	eleqtrd 2863	. . . . . . 7 ⊢ (𝜑 → (𝐺‘𝐶) ∈ ((𝑧 ∈ ((𝑋 ∩ 𝑌) ∖ {𝐶}) ↦ (𝐺‘𝑧)) lim_ℂ 𝐶))
180	3	mpomulcn 25188	. . . . . . . 8 ⊢ (𝑢 ∈ ℂ, 𝑣 ∈ ℂ ↦ (𝑢 · 𝑣)) ∈ ((𝐽 ×_t 𝐽) Cn 𝐽)
181	5, 6, 7	dvcl 26219	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝐶(𝑆 D 𝐹)𝐾) → 𝐾 ∈ ℂ)
182	1, 181	mpdan 700	. . . . . . . . 9 ⊢ (𝜑 → 𝐾 ∈ ℂ)
183	13, 69	ffvelcdmd 7085	. . . . . . . . 9 ⊢ (𝜑 → (𝐺‘𝐶) ∈ ℂ)
184	182, 183	opelxpd 5690	. . . . . . . 8 ⊢ (𝜑 → ⟨𝐾, (𝐺‘𝐶)⟩ ∈ (ℂ × ℂ))
185	75	toponunii 23234	. . . . . . . . 9 ⊢ (ℂ × ℂ) = ∪ (𝐽 ×_t 𝐽)
186	185	cncnpi 23596	. . . . . . . 8 ⊢ (((𝑢 ∈ ℂ, 𝑣 ∈ ℂ ↦ (𝑢 · 𝑣)) ∈ ((𝐽 ×_t 𝐽) Cn 𝐽) ∧ ⟨𝐾, (𝐺‘𝐶)⟩ ∈ (ℂ × ℂ)) → (𝑢 ∈ ℂ, 𝑣 ∈ ℂ ↦ (𝑢 · 𝑣)) ∈ (((𝐽 ×_t 𝐽) CnP 𝐽)‘⟨𝐾, (𝐺‘𝐶)⟩))
187	180, 184, 186	sylancr 599	. . . . . . 7 ⊢ (𝜑 → (𝑢 ∈ ℂ, 𝑣 ∈ ℂ ↦ (𝑢 · 𝑣)) ∈ (((𝐽 ×_t 𝐽) CnP 𝐽)‘⟨𝐾, (𝐺‘𝐶)⟩))
188	55, 59, 73, 73, 3, 76, 138, 179, 187	limccnp2 26212	. . . . . 6 ⊢ (𝜑 → (𝐾(𝑢 ∈ ℂ, 𝑣 ∈ ℂ ↦ (𝑢 · 𝑣))(𝐺‘𝐶)) ∈ ((𝑧 ∈ ((𝑋 ∩ 𝑌) ∖ {𝐶}) ↦ ((((𝐹‘𝑧) − (𝐹‘𝐶)) / (𝑧 − 𝐶))(𝑢 ∈ ℂ, 𝑣 ∈ ℂ ↦ (𝑢 · 𝑣))(𝐺‘𝑧))) lim_ℂ 𝐶))
189		df-mpt 5187	. . . . . . 7 ⊢ (𝑧 ∈ ((𝑋 ∩ 𝑌) ∖ {𝐶}) ↦ ((((𝐹‘𝑧) − (𝐹‘𝐶)) / (𝑧 − 𝐶))(𝑢 ∈ ℂ, 𝑣 ∈ ℂ ↦ (𝑢 · 𝑣))(𝐺‘𝑧))) = {⟨𝑧, 𝑤⟩ ∣ (𝑧 ∈ ((𝑋 ∩ 𝑌) ∖ {𝐶}) ∧ 𝑤 = ((((𝐹‘𝑧) − (𝐹‘𝐶)) / (𝑧 − 𝐶))(𝑢 ∈ ℂ, 𝑣 ∈ ℂ ↦ (𝑢 · 𝑣))(𝐺‘𝑧)))}
190	189	oveq1i 7430	. . . . . 6 ⊢ ((𝑧 ∈ ((𝑋 ∩ 𝑌) ∖ {𝐶}) ↦ ((((𝐹‘𝑧) − (𝐹‘𝐶)) / (𝑧 − 𝐶))(𝑢 ∈ ℂ, 𝑣 ∈ ℂ ↦ (𝑢 · 𝑣))(𝐺‘𝑧))) lim_ℂ 𝐶) = ({⟨𝑧, 𝑤⟩ ∣ (𝑧 ∈ ((𝑋 ∩ 𝑌) ∖ {𝐶}) ∧ 𝑤 = ((((𝐹‘𝑧) − (𝐹‘𝐶)) / (𝑧 − 𝐶))(𝑢 ∈ ℂ, 𝑣 ∈ ℂ ↦ (𝑢 · 𝑣))(𝐺‘𝑧)))} lim_ℂ 𝐶)
191	188, 190	eleqtrdi 2871	. . . . 5 ⊢ (𝜑 → (𝐾(𝑢 ∈ ℂ, 𝑣 ∈ ℂ ↦ (𝑢 · 𝑣))(𝐺‘𝐶)) ∈ ({⟨𝑧, 𝑤⟩ ∣ (𝑧 ∈ ((𝑋 ∩ 𝑌) ∖ {𝐶}) ∧ 𝑤 = ((((𝐹‘𝑧) − (𝐹‘𝐶)) / (𝑧 − 𝐶))(𝑢 ∈ ℂ, 𝑣 ∈ ℂ ↦ (𝑢 · 𝑣))(𝐺‘𝑧)))} lim_ℂ 𝐶))
192		ovmpot 7581	. . . . . 6 ⊢ ((𝐾 ∈ ℂ ∧ (𝐺‘𝐶) ∈ ℂ) → (𝐾(𝑢 ∈ ℂ, 𝑣 ∈ ℂ ↦ (𝑢 · 𝑣))(𝐺‘𝐶)) = (𝐾 · (𝐺‘𝐶)))
193	182, 183, 192	syl2anc 596	. . . . 5 ⊢ (𝜑 → (𝐾(𝑢 ∈ ℂ, 𝑣 ∈ ℂ ↦ (𝑢 · 𝑣))(𝐺‘𝐶)) = (𝐾 · (𝐺‘𝐶)))
194		ovmpot 7581	. . . . . . . . . . 11 ⊢ (((((𝐹‘𝑧) − (𝐹‘𝐶)) / (𝑧 − 𝐶)) ∈ ℂ ∧ (𝐺‘𝑧) ∈ ℂ) → ((((𝐹‘𝑧) − (𝐹‘𝐶)) / (𝑧 − 𝐶))(𝑢 ∈ ℂ, 𝑣 ∈ ℂ ↦ (𝑢 · 𝑣))(𝐺‘𝑧)) = ((((𝐹‘𝑧) − (𝐹‘𝐶)) / (𝑧 − 𝐶)) · (𝐺‘𝑧)))
195	55, 59, 194	syl2anc 596	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑧 ∈ ((𝑋 ∩ 𝑌) ∖ {𝐶})) → ((((𝐹‘𝑧) − (𝐹‘𝐶)) / (𝑧 − 𝐶))(𝑢 ∈ ℂ, 𝑣 ∈ ℂ ↦ (𝑢 · 𝑣))(𝐺‘𝑧)) = ((((𝐹‘𝑧) − (𝐹‘𝐶)) / (𝑧 − 𝐶)) · (𝐺‘𝑧)))
196	195	eqeq2d 2772	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑧 ∈ ((𝑋 ∩ 𝑌) ∖ {𝐶})) → (𝑤 = ((((𝐹‘𝑧) − (𝐹‘𝐶)) / (𝑧 − 𝐶))(𝑢 ∈ ℂ, 𝑣 ∈ ℂ ↦ (𝑢 · 𝑣))(𝐺‘𝑧)) ↔ 𝑤 = ((((𝐹‘𝑧) − (𝐹‘𝐶)) / (𝑧 − 𝐶)) · (𝐺‘𝑧))))
197	196	pm5.32da 590	. . . . . . . 8 ⊢ (𝜑 → ((𝑧 ∈ ((𝑋 ∩ 𝑌) ∖ {𝐶}) ∧ 𝑤 = ((((𝐹‘𝑧) − (𝐹‘𝐶)) / (𝑧 − 𝐶))(𝑢 ∈ ℂ, 𝑣 ∈ ℂ ↦ (𝑢 · 𝑣))(𝐺‘𝑧))) ↔ (𝑧 ∈ ((𝑋 ∩ 𝑌) ∖ {𝐶}) ∧ 𝑤 = ((((𝐹‘𝑧) − (𝐹‘𝐶)) / (𝑧 − 𝐶)) · (𝐺‘𝑧)))))
198	197	opabbidv 5171	. . . . . . 7 ⊢ (𝜑 → {⟨𝑧, 𝑤⟩ ∣ (𝑧 ∈ ((𝑋 ∩ 𝑌) ∖ {𝐶}) ∧ 𝑤 = ((((𝐹‘𝑧) − (𝐹‘𝐶)) / (𝑧 − 𝐶))(𝑢 ∈ ℂ, 𝑣 ∈ ℂ ↦ (𝑢 · 𝑣))(𝐺‘𝑧)))} = {⟨𝑧, 𝑤⟩ ∣ (𝑧 ∈ ((𝑋 ∩ 𝑌) ∖ {𝐶}) ∧ 𝑤 = ((((𝐹‘𝑧) − (𝐹‘𝐶)) / (𝑧 − 𝐶)) · (𝐺‘𝑧)))})
199		df-mpt 5187	. . . . . . 7 ⊢ (𝑧 ∈ ((𝑋 ∩ 𝑌) ∖ {𝐶}) ↦ ((((𝐹‘𝑧) − (𝐹‘𝐶)) / (𝑧 − 𝐶)) · (𝐺‘𝑧))) = {⟨𝑧, 𝑤⟩ ∣ (𝑧 ∈ ((𝑋 ∩ 𝑌) ∖ {𝐶}) ∧ 𝑤 = ((((𝐹‘𝑧) − (𝐹‘𝐶)) / (𝑧 − 𝐶)) · (𝐺‘𝑧)))}
200	198, 199	eqtr4di 2814	. . . . . 6 ⊢ (𝜑 → {⟨𝑧, 𝑤⟩ ∣ (𝑧 ∈ ((𝑋 ∩ 𝑌) ∖ {𝐶}) ∧ 𝑤 = ((((𝐹‘𝑧) − (𝐹‘𝐶)) / (𝑧 − 𝐶))(𝑢 ∈ ℂ, 𝑣 ∈ ℂ ↦ (𝑢 · 𝑣))(𝐺‘𝑧)))} = (𝑧 ∈ ((𝑋 ∩ 𝑌) ∖ {𝐶}) ↦ ((((𝐹‘𝑧) − (𝐹‘𝐶)) / (𝑧 − 𝐶)) · (𝐺‘𝑧))))
201	200	oveq1d 7435	. . . . 5 ⊢ (𝜑 → ({⟨𝑧, 𝑤⟩ ∣ (𝑧 ∈ ((𝑋 ∩ 𝑌) ∖ {𝐶}) ∧ 𝑤 = ((((𝐹‘𝑧) − (𝐹‘𝐶)) / (𝑧 − 𝐶))(𝑢 ∈ ℂ, 𝑣 ∈ ℂ ↦ (𝑢 · 𝑣))(𝐺‘𝑧)))} lim_ℂ 𝐶) = ((𝑧 ∈ ((𝑋 ∩ 𝑌) ∖ {𝐶}) ↦ ((((𝐹‘𝑧) − (𝐹‘𝐶)) / (𝑧 − 𝐶)) · (𝐺‘𝑧))) lim_ℂ 𝐶))
202	191, 193, 201	3eltr3d 2875	. . . 4 ⊢ (𝜑 → (𝐾 · (𝐺‘𝐶)) ∈ ((𝑧 ∈ ((𝑋 ∩ 𝑌) ∖ {𝐶}) ↦ ((((𝐹‘𝑧) − (𝐹‘𝐶)) / (𝑧 − 𝐶)) · (𝐺‘𝑧))) lim_ℂ 𝐶))
203	16	simprd 501	. . . . . . . 8 ⊢ (𝜑 → 𝐿 ∈ ((𝑧 ∈ (𝑌 ∖ {𝐶}) ↦ (((𝐺‘𝑧) − (𝐺‘𝐶)) / (𝑧 − 𝐶))) lim_ℂ 𝐶))
204	70	fmpttd 7115	. . . . . . . . . 10 ⊢ (𝜑 → (𝑧 ∈ (𝑌 ∖ {𝐶}) ↦ (((𝐺‘𝑧) − (𝐺‘𝐶)) / (𝑧 − 𝐶))):(𝑌 ∖ {𝐶})⟶ℂ)
205	64	ssdifssd 4094	. . . . . . . . . 10 ⊢ (𝜑 → (𝑌 ∖ {𝐶}) ⊆ ℂ)
206		eqid 2761	. . . . . . . . . 10 ⊢ (𝐽 ↾_t ((𝑌 ∖ {𝐶}) ∪ {𝐶})) = (𝐽 ↾_t ((𝑌 ∖ {𝐶}) ∪ {𝐶}))
207		undif1 4430	. . . . . . . . . . . . . . 15 ⊢ ((𝑌 ∖ {𝐶}) ∪ {𝐶}) = (𝑌 ∪ {𝐶})
208	207, 170	eqtrid 2808	. . . . . . . . . . . . . 14 ⊢ (𝜑 → ((𝑌 ∖ {𝐶}) ∪ {𝐶}) = 𝑌)
209	208	oveq2d 7436	. . . . . . . . . . . . 13 ⊢ (𝜑 → (𝐽 ↾_t ((𝑌 ∖ {𝐶}) ∪ {𝐶})) = (𝐽 ↾_t 𝑌))
210	209	fveq2d 6889	. . . . . . . . . . . 12 ⊢ (𝜑 → (int‘(𝐽 ↾_t ((𝑌 ∖ {𝐶}) ∪ {𝐶}))) = (int‘(𝐽 ↾_t 𝑌)))
211	210, 131	fveq12d 6892	. . . . . . . . . . 11 ⊢ (𝜑 → ((int‘(𝐽 ↾_t ((𝑌 ∖ {𝐶}) ∪ {𝐶})))‘(((𝑋 ∩ 𝑌) ∖ {𝐶}) ∪ {𝐶})) = ((int‘(𝐽 ↾_t 𝑌))‘(𝑋 ∩ 𝑌)))
212	167, 211	eleqtrrd 2864	. . . . . . . . . 10 ⊢ (𝜑 → 𝐶 ∈ ((int‘(𝐽 ↾_t ((𝑌 ∖ {𝐶}) ∪ {𝐶})))‘(((𝑋 ∩ 𝑌) ∖ {𝐶}) ∪ {𝐶})))
213	204, 62, 205, 3, 206, 212	limcres 26206	. . . . . . . . 9 ⊢ (𝜑 → (((𝑧 ∈ (𝑌 ∖ {𝐶}) ↦ (((𝐺‘𝑧) − (𝐺‘𝐶)) / (𝑧 − 𝐶))) ↾ ((𝑋 ∩ 𝑌) ∖ {𝐶})) lim_ℂ 𝐶) = ((𝑧 ∈ (𝑌 ∖ {𝐶}) ↦ (((𝐺‘𝑧) − (𝐺‘𝐶)) / (𝑧 − 𝐶))) lim_ℂ 𝐶))
214	62	resmptd 6032	. . . . . . . . . 10 ⊢ (𝜑 → ((𝑧 ∈ (𝑌 ∖ {𝐶}) ↦ (((𝐺‘𝑧) − (𝐺‘𝐶)) / (𝑧 − 𝐶))) ↾ ((𝑋 ∩ 𝑌) ∖ {𝐶})) = (𝑧 ∈ ((𝑋 ∩ 𝑌) ∖ {𝐶}) ↦ (((𝐺‘𝑧) − (𝐺‘𝐶)) / (𝑧 − 𝐶))))
215	214	oveq1d 7435	. . . . . . . . 9 ⊢ (𝜑 → (((𝑧 ∈ (𝑌 ∖ {𝐶}) ↦ (((𝐺‘𝑧) − (𝐺‘𝐶)) / (𝑧 − 𝐶))) ↾ ((𝑋 ∩ 𝑌) ∖ {𝐶})) lim_ℂ 𝐶) = ((𝑧 ∈ ((𝑋 ∩ 𝑌) ∖ {𝐶}) ↦ (((𝐺‘𝑧) − (𝐺‘𝐶)) / (𝑧 − 𝐶))) lim_ℂ 𝐶))
216	213, 215	eqtr3d 2798	. . . . . . . 8 ⊢ (𝜑 → ((𝑧 ∈ (𝑌 ∖ {𝐶}) ↦ (((𝐺‘𝑧) − (𝐺‘𝐶)) / (𝑧 − 𝐶))) lim_ℂ 𝐶) = ((𝑧 ∈ ((𝑋 ∩ 𝑌) ∖ {𝐶}) ↦ (((𝐺‘𝑧) − (𝐺‘𝐶)) / (𝑧 − 𝐶))) lim_ℂ 𝐶))
217	203, 216	eleqtrd 2863	. . . . . . 7 ⊢ (𝜑 → 𝐿 ∈ ((𝑧 ∈ ((𝑋 ∩ 𝑌) ∖ {𝐶}) ↦ (((𝐺‘𝑧) − (𝐺‘𝐶)) / (𝑧 − 𝐶))) lim_ℂ 𝐶))
218	84, 5	sstrd 3941	. . . . . . . . . 10 ⊢ (𝜑 → (𝑋 ∩ 𝑌) ⊆ ℂ)
219		cncfmptc 25233	. . . . . . . . . 10 ⊢ (((𝐹‘𝐶) ∈ ℂ ∧ (𝑋 ∩ 𝑌) ⊆ ℂ ∧ ℂ ⊆ ℂ) → (𝑧 ∈ (𝑋 ∩ 𝑌) ↦ (𝐹‘𝐶)) ∈ ((𝑋 ∩ 𝑌)–cn→ℂ))
220	43, 218, 73, 219	syl3anc 1398	. . . . . . . . 9 ⊢ (𝜑 → (𝑧 ∈ (𝑋 ∩ 𝑌) ↦ (𝐹‘𝐶)) ∈ ((𝑋 ∩ 𝑌)–cn→ℂ))
221		eqidd 2762	. . . . . . . . 9 ⊢ (𝑧 = 𝐶 → (𝐹‘𝐶) = (𝐹‘𝐶))
222	220, 127, 221	cnmptlimc 26210	. . . . . . . 8 ⊢ (𝜑 → (𝐹‘𝐶) ∈ ((𝑧 ∈ (𝑋 ∩ 𝑌) ↦ (𝐹‘𝐶)) lim_ℂ 𝐶))
223	43	adantr 486	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑧 ∈ (𝑋 ∩ 𝑌)) → (𝐹‘𝐶) ∈ ℂ)
224	223	fmpttd 7115	. . . . . . . . . 10 ⊢ (𝜑 → (𝑧 ∈ (𝑋 ∩ 𝑌) ↦ (𝐹‘𝐶)):(𝑋 ∩ 𝑌)⟶ℂ)
225	224	limcdif 26196	. . . . . . . . 9 ⊢ (𝜑 → ((𝑧 ∈ (𝑋 ∩ 𝑌) ↦ (𝐹‘𝐶)) lim_ℂ 𝐶) = (((𝑧 ∈ (𝑋 ∩ 𝑌) ↦ (𝐹‘𝐶)) ↾ ((𝑋 ∩ 𝑌) ∖ {𝐶})) lim_ℂ 𝐶))
226		resmpt 6029	. . . . . . . . . . 11 ⊢ (((𝑋 ∩ 𝑌) ∖ {𝐶}) ⊆ (𝑋 ∩ 𝑌) → ((𝑧 ∈ (𝑋 ∩ 𝑌) ↦ (𝐹‘𝐶)) ↾ ((𝑋 ∩ 𝑌) ∖ {𝐶})) = (𝑧 ∈ ((𝑋 ∩ 𝑌) ∖ {𝐶}) ↦ (𝐹‘𝐶)))
227	146, 226	mp1i 14	. . . . . . . . . 10 ⊢ (𝜑 → ((𝑧 ∈ (𝑋 ∩ 𝑌) ↦ (𝐹‘𝐶)) ↾ ((𝑋 ∩ 𝑌) ∖ {𝐶})) = (𝑧 ∈ ((𝑋 ∩ 𝑌) ∖ {𝐶}) ↦ (𝐹‘𝐶)))
228	227	oveq1d 7435	. . . . . . . . 9 ⊢ (𝜑 → (((𝑧 ∈ (𝑋 ∩ 𝑌) ↦ (𝐹‘𝐶)) ↾ ((𝑋 ∩ 𝑌) ∖ {𝐶})) lim_ℂ 𝐶) = ((𝑧 ∈ ((𝑋 ∩ 𝑌) ∖ {𝐶}) ↦ (𝐹‘𝐶)) lim_ℂ 𝐶))
229	225, 228	eqtrd 2796	. . . . . . . 8 ⊢ (𝜑 → ((𝑧 ∈ (𝑋 ∩ 𝑌) ↦ (𝐹‘𝐶)) lim_ℂ 𝐶) = ((𝑧 ∈ ((𝑋 ∩ 𝑌) ∖ {𝐶}) ↦ (𝐹‘𝐶)) lim_ℂ 𝐶))
230	222, 229	eleqtrd 2863	. . . . . . 7 ⊢ (𝜑 → (𝐹‘𝐶) ∈ ((𝑧 ∈ ((𝑋 ∩ 𝑌) ∖ {𝐶}) ↦ (𝐹‘𝐶)) lim_ℂ 𝐶))
231	5, 13, 14	dvcl 26219	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝐶(𝑆 D 𝐺)𝐿) → 𝐿 ∈ ℂ)
232	11, 231	mpdan 700	. . . . . . . . 9 ⊢ (𝜑 → 𝐿 ∈ ℂ)
233	232, 43	opelxpd 5690	. . . . . . . 8 ⊢ (𝜑 → ⟨𝐿, (𝐹‘𝐶)⟩ ∈ (ℂ × ℂ))
234	185	cncnpi 23596	. . . . . . . 8 ⊢ (((𝑢 ∈ ℂ, 𝑣 ∈ ℂ ↦ (𝑢 · 𝑣)) ∈ ((𝐽 ×_t 𝐽) Cn 𝐽) ∧ ⟨𝐿, (𝐹‘𝐶)⟩ ∈ (ℂ × ℂ)) → (𝑢 ∈ ℂ, 𝑣 ∈ ℂ ↦ (𝑢 · 𝑣)) ∈ (((𝐽 ×_t 𝐽) CnP 𝐽)‘⟨𝐿, (𝐹‘𝐶)⟩))
235	180, 233, 234	sylancr 599	. . . . . . 7 ⊢ (𝜑 → (𝑢 ∈ ℂ, 𝑣 ∈ ℂ ↦ (𝑢 · 𝑣)) ∈ (((𝐽 ×_t 𝐽) CnP 𝐽)‘⟨𝐿, (𝐹‘𝐶)⟩))
236	71, 44, 73, 73, 3, 76, 217, 230, 235	limccnp2 26212	. . . . . 6 ⊢ (𝜑 → (𝐿(𝑢 ∈ ℂ, 𝑣 ∈ ℂ ↦ (𝑢 · 𝑣))(𝐹‘𝐶)) ∈ ((𝑧 ∈ ((𝑋 ∩ 𝑌) ∖ {𝐶}) ↦ ((((𝐺‘𝑧) − (𝐺‘𝐶)) / (𝑧 − 𝐶))(𝑢 ∈ ℂ, 𝑣 ∈ ℂ ↦ (𝑢 · 𝑣))(𝐹‘𝐶))) lim_ℂ 𝐶))
237		df-mpt 5187	. . . . . . 7 ⊢ (𝑧 ∈ ((𝑋 ∩ 𝑌) ∖ {𝐶}) ↦ ((((𝐺‘𝑧) − (𝐺‘𝐶)) / (𝑧 − 𝐶))(𝑢 ∈ ℂ, 𝑣 ∈ ℂ ↦ (𝑢 · 𝑣))(𝐹‘𝐶))) = {⟨𝑧, 𝑤⟩ ∣ (𝑧 ∈ ((𝑋 ∩ 𝑌) ∖ {𝐶}) ∧ 𝑤 = ((((𝐺‘𝑧) − (𝐺‘𝐶)) / (𝑧 − 𝐶))(𝑢 ∈ ℂ, 𝑣 ∈ ℂ ↦ (𝑢 · 𝑣))(𝐹‘𝐶)))}
238	237	oveq1i 7430	. . . . . 6 ⊢ ((𝑧 ∈ ((𝑋 ∩ 𝑌) ∖ {𝐶}) ↦ ((((𝐺‘𝑧) − (𝐺‘𝐶)) / (𝑧 − 𝐶))(𝑢 ∈ ℂ, 𝑣 ∈ ℂ ↦ (𝑢 · 𝑣))(𝐹‘𝐶))) lim_ℂ 𝐶) = ({⟨𝑧, 𝑤⟩ ∣ (𝑧 ∈ ((𝑋 ∩ 𝑌) ∖ {𝐶}) ∧ 𝑤 = ((((𝐺‘𝑧) − (𝐺‘𝐶)) / (𝑧 − 𝐶))(𝑢 ∈ ℂ, 𝑣 ∈ ℂ ↦ (𝑢 · 𝑣))(𝐹‘𝐶)))} lim_ℂ 𝐶)
239	236, 238	eleqtrdi 2871	. . . . 5 ⊢ (𝜑 → (𝐿(𝑢 ∈ ℂ, 𝑣 ∈ ℂ ↦ (𝑢 · 𝑣))(𝐹‘𝐶)) ∈ ({⟨𝑧, 𝑤⟩ ∣ (𝑧 ∈ ((𝑋 ∩ 𝑌) ∖ {𝐶}) ∧ 𝑤 = ((((𝐺‘𝑧) − (𝐺‘𝐶)) / (𝑧 − 𝐶))(𝑢 ∈ ℂ, 𝑣 ∈ ℂ ↦ (𝑢 · 𝑣))(𝐹‘𝐶)))} lim_ℂ 𝐶))
240		ovmpot 7581	. . . . . 6 ⊢ ((𝐿 ∈ ℂ ∧ (𝐹‘𝐶) ∈ ℂ) → (𝐿(𝑢 ∈ ℂ, 𝑣 ∈ ℂ ↦ (𝑢 · 𝑣))(𝐹‘𝐶)) = (𝐿 · (𝐹‘𝐶)))
241	232, 43, 240	syl2anc 596	. . . . 5 ⊢ (𝜑 → (𝐿(𝑢 ∈ ℂ, 𝑣 ∈ ℂ ↦ (𝑢 · 𝑣))(𝐹‘𝐶)) = (𝐿 · (𝐹‘𝐶)))
242	42	adantr 486	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑧 ∈ ((𝑋 ∩ 𝑌) ∖ {𝐶})) → 𝐶 ∈ 𝑋)
243	32, 242	ffvelcdmd 7085	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑧 ∈ ((𝑋 ∩ 𝑌) ∖ {𝐶})) → (𝐹‘𝐶) ∈ ℂ)
244		ovmpot 7581	. . . . . . . . . . 11 ⊢ (((((𝐺‘𝑧) − (𝐺‘𝐶)) / (𝑧 − 𝐶)) ∈ ℂ ∧ (𝐹‘𝐶) ∈ ℂ) → ((((𝐺‘𝑧) − (𝐺‘𝐶)) / (𝑧 − 𝐶))(𝑢 ∈ ℂ, 𝑣 ∈ ℂ ↦ (𝑢 · 𝑣))(𝐹‘𝐶)) = ((((𝐺‘𝑧) − (𝐺‘𝐶)) / (𝑧 − 𝐶)) · (𝐹‘𝐶)))
245	71, 243, 244	syl2anc 596	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑧 ∈ ((𝑋 ∩ 𝑌) ∖ {𝐶})) → ((((𝐺‘𝑧) − (𝐺‘𝐶)) / (𝑧 − 𝐶))(𝑢 ∈ ℂ, 𝑣 ∈ ℂ ↦ (𝑢 · 𝑣))(𝐹‘𝐶)) = ((((𝐺‘𝑧) − (𝐺‘𝐶)) / (𝑧 − 𝐶)) · (𝐹‘𝐶)))
246	245	eqeq2d 2772	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑧 ∈ ((𝑋 ∩ 𝑌) ∖ {𝐶})) → (𝑤 = ((((𝐺‘𝑧) − (𝐺‘𝐶)) / (𝑧 − 𝐶))(𝑢 ∈ ℂ, 𝑣 ∈ ℂ ↦ (𝑢 · 𝑣))(𝐹‘𝐶)) ↔ 𝑤 = ((((𝐺‘𝑧) − (𝐺‘𝐶)) / (𝑧 − 𝐶)) · (𝐹‘𝐶))))
247	246	pm5.32da 590	. . . . . . . 8 ⊢ (𝜑 → ((𝑧 ∈ ((𝑋 ∩ 𝑌) ∖ {𝐶}) ∧ 𝑤 = ((((𝐺‘𝑧) − (𝐺‘𝐶)) / (𝑧 − 𝐶))(𝑢 ∈ ℂ, 𝑣 ∈ ℂ ↦ (𝑢 · 𝑣))(𝐹‘𝐶))) ↔ (𝑧 ∈ ((𝑋 ∩ 𝑌) ∖ {𝐶}) ∧ 𝑤 = ((((𝐺‘𝑧) − (𝐺‘𝐶)) / (𝑧 − 𝐶)) · (𝐹‘𝐶)))))
248	247	opabbidv 5171	. . . . . . 7 ⊢ (𝜑 → {⟨𝑧, 𝑤⟩ ∣ (𝑧 ∈ ((𝑋 ∩ 𝑌) ∖ {𝐶}) ∧ 𝑤 = ((((𝐺‘𝑧) − (𝐺‘𝐶)) / (𝑧 − 𝐶))(𝑢 ∈ ℂ, 𝑣 ∈ ℂ ↦ (𝑢 · 𝑣))(𝐹‘𝐶)))} = {⟨𝑧, 𝑤⟩ ∣ (𝑧 ∈ ((𝑋 ∩ 𝑌) ∖ {𝐶}) ∧ 𝑤 = ((((𝐺‘𝑧) − (𝐺‘𝐶)) / (𝑧 − 𝐶)) · (𝐹‘𝐶)))})
249		df-mpt 5187	. . . . . . 7 ⊢ (𝑧 ∈ ((𝑋 ∩ 𝑌) ∖ {𝐶}) ↦ ((((𝐺‘𝑧) − (𝐺‘𝐶)) / (𝑧 − 𝐶)) · (𝐹‘𝐶))) = {⟨𝑧, 𝑤⟩ ∣ (𝑧 ∈ ((𝑋 ∩ 𝑌) ∖ {𝐶}) ∧ 𝑤 = ((((𝐺‘𝑧) − (𝐺‘𝐶)) / (𝑧 − 𝐶)) · (𝐹‘𝐶)))}
250	248, 249	eqtr4di 2814	. . . . . 6 ⊢ (𝜑 → {⟨𝑧, 𝑤⟩ ∣ (𝑧 ∈ ((𝑋 ∩ 𝑌) ∖ {𝐶}) ∧ 𝑤 = ((((𝐺‘𝑧) − (𝐺‘𝐶)) / (𝑧 − 𝐶))(𝑢 ∈ ℂ, 𝑣 ∈ ℂ ↦ (𝑢 · 𝑣))(𝐹‘𝐶)))} = (𝑧 ∈ ((𝑋 ∩ 𝑌) ∖ {𝐶}) ↦ ((((𝐺‘𝑧) − (𝐺‘𝐶)) / (𝑧 − 𝐶)) · (𝐹‘𝐶))))
251	250	oveq1d 7435	. . . . 5 ⊢ (𝜑 → ({⟨𝑧, 𝑤⟩ ∣ (𝑧 ∈ ((𝑋 ∩ 𝑌) ∖ {𝐶}) ∧ 𝑤 = ((((𝐺‘𝑧) − (𝐺‘𝐶)) / (𝑧 − 𝐶))(𝑢 ∈ ℂ, 𝑣 ∈ ℂ ↦ (𝑢 · 𝑣))(𝐹‘𝐶)))} lim_ℂ 𝐶) = ((𝑧 ∈ ((𝑋 ∩ 𝑌) ∖ {𝐶}) ↦ ((((𝐺‘𝑧) − (𝐺‘𝐶)) / (𝑧 − 𝐶)) · (𝐹‘𝐶))) lim_ℂ 𝐶))
252	239, 241, 251	3eltr3d 2875	. . . 4 ⊢ (𝜑 → (𝐿 · (𝐹‘𝐶)) ∈ ((𝑧 ∈ ((𝑋 ∩ 𝑌) ∖ {𝐶}) ↦ ((((𝐺‘𝑧) − (𝐺‘𝐶)) / (𝑧 − 𝐶)) · (𝐹‘𝐶))) lim_ℂ 𝐶))
253	3	addcn 25185	. . . . 5 ⊢ + ∈ ((𝐽 ×_t 𝐽) Cn 𝐽)
254	182, 183	mulcld 11329	. . . . . 6 ⊢ (𝜑 → (𝐾 · (𝐺‘𝐶)) ∈ ℂ)
255	232, 43	mulcld 11329	. . . . . 6 ⊢ (𝜑 → (𝐿 · (𝐹‘𝐶)) ∈ ℂ)
256	254, 255	opelxpd 5690	. . . . 5 ⊢ (𝜑 → ⟨(𝐾 · (𝐺‘𝐶)), (𝐿 · (𝐹‘𝐶))⟩ ∈ (ℂ × ℂ))
257	185	cncnpi 23596	. . . . 5 ⊢ (( + ∈ ((𝐽 ×_t 𝐽) Cn 𝐽) ∧ ⟨(𝐾 · (𝐺‘𝐶)), (𝐿 · (𝐹‘𝐶))⟩ ∈ (ℂ × ℂ)) → + ∈ (((𝐽 ×_t 𝐽) CnP 𝐽)‘⟨(𝐾 · (𝐺‘𝐶)), (𝐿 · (𝐹‘𝐶))⟩))
258	253, 256, 257	sylancr 599	. . . 4 ⊢ (𝜑 → + ∈ (((𝐽 ×_t 𝐽) CnP 𝐽)‘⟨(𝐾 · (𝐺‘𝐶)), (𝐿 · (𝐹‘𝐶))⟩))
259	60, 72, 73, 73, 3, 76, 202, 252, 258	limccnp2 26212	. . 3 ⊢ (𝜑 → ((𝐾 · (𝐺‘𝐶)) + (𝐿 · (𝐹‘𝐶))) ∈ ((𝑧 ∈ ((𝑋 ∩ 𝑌) ∖ {𝐶}) ↦ (((((𝐹‘𝑧) − (𝐹‘𝐶)) / (𝑧 − 𝐶)) · (𝐺‘𝑧)) + ((((𝐺‘𝑧) − (𝐺‘𝐶)) / (𝑧 − 𝐶)) · (𝐹‘𝐶)))) lim_ℂ 𝐶))
260	37, 243	subcld 11669	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑧 ∈ ((𝑋 ∩ 𝑌) ∖ {𝐶})) → ((𝐹‘𝑧) − (𝐹‘𝐶)) ∈ ℂ)
261	260, 59	mulcld 11329	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑧 ∈ ((𝑋 ∩ 𝑌) ∖ {𝐶})) → (((𝐹‘𝑧) − (𝐹‘𝐶)) · (𝐺‘𝑧)) ∈ ℂ)
262	69	adantr 486	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑧 ∈ ((𝑋 ∩ 𝑌) ∖ {𝐶})) → 𝐶 ∈ 𝑌)
263	56, 262	ffvelcdmd 7085	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑧 ∈ ((𝑋 ∩ 𝑌) ∖ {𝐶})) → (𝐺‘𝐶) ∈ ℂ)
264	59, 263	subcld 11669	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑧 ∈ ((𝑋 ∩ 𝑌) ∖ {𝐶})) → ((𝐺‘𝑧) − (𝐺‘𝐶)) ∈ ℂ)
265	264, 243	mulcld 11329	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑧 ∈ ((𝑋 ∩ 𝑌) ∖ {𝐶})) → (((𝐺‘𝑧) − (𝐺‘𝐶)) · (𝐹‘𝐶)) ∈ ℂ)
266	47, 242	sseldd 3932	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑧 ∈ ((𝑋 ∩ 𝑌) ∖ {𝐶})) → 𝐶 ∈ ℂ)
267	48, 266	subcld 11669	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑧 ∈ ((𝑋 ∩ 𝑌) ∖ {𝐶})) → (𝑧 − 𝐶) ∈ ℂ)
268	261, 265, 267, 54	divdird 12131	. . . . . 6 ⊢ ((𝜑 ∧ 𝑧 ∈ ((𝑋 ∩ 𝑌) ∖ {𝐶})) → (((((𝐹‘𝑧) − (𝐹‘𝐶)) · (𝐺‘𝑧)) + (((𝐺‘𝑧) − (𝐺‘𝐶)) · (𝐹‘𝐶))) / (𝑧 − 𝐶)) = (((((𝐹‘𝑧) − (𝐹‘𝐶)) · (𝐺‘𝑧)) / (𝑧 − 𝐶)) + ((((𝐺‘𝑧) − (𝐺‘𝐶)) · (𝐹‘𝐶)) / (𝑧 − 𝐶))))
269	37, 59	mulcld 11329	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑧 ∈ ((𝑋 ∩ 𝑌) ∖ {𝐶})) → ((𝐹‘𝑧) · (𝐺‘𝑧)) ∈ ℂ)
270	243, 59	mulcld 11329	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑧 ∈ ((𝑋 ∩ 𝑌) ∖ {𝐶})) → ((𝐹‘𝐶) · (𝐺‘𝑧)) ∈ ℂ)
271	243, 263	mulcld 11329	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑧 ∈ ((𝑋 ∩ 𝑌) ∖ {𝐶})) → ((𝐹‘𝐶) · (𝐺‘𝐶)) ∈ ℂ)
272	269, 270, 271	npncand 11693	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑧 ∈ ((𝑋 ∩ 𝑌) ∖ {𝐶})) → ((((𝐹‘𝑧) · (𝐺‘𝑧)) − ((𝐹‘𝐶) · (𝐺‘𝑧))) + (((𝐹‘𝐶) · (𝐺‘𝑧)) − ((𝐹‘𝐶) · (𝐺‘𝐶)))) = (((𝐹‘𝑧) · (𝐺‘𝑧)) − ((𝐹‘𝐶) · (𝐺‘𝐶))))
273	37, 243, 59	subdird 11773	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑧 ∈ ((𝑋 ∩ 𝑌) ∖ {𝐶})) → (((𝐹‘𝑧) − (𝐹‘𝐶)) · (𝐺‘𝑧)) = (((𝐹‘𝑧) · (𝐺‘𝑧)) − ((𝐹‘𝐶) · (𝐺‘𝑧))))
274	264, 243	mulcomd 11330	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑧 ∈ ((𝑋 ∩ 𝑌) ∖ {𝐶})) → (((𝐺‘𝑧) − (𝐺‘𝐶)) · (𝐹‘𝐶)) = ((𝐹‘𝐶) · ((𝐺‘𝑧) − (𝐺‘𝐶))))
275	243, 59, 263	subdid 11772	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑧 ∈ ((𝑋 ∩ 𝑌) ∖ {𝐶})) → ((𝐹‘𝐶) · ((𝐺‘𝑧) − (𝐺‘𝐶))) = (((𝐹‘𝐶) · (𝐺‘𝑧)) − ((𝐹‘𝐶) · (𝐺‘𝐶))))
276	274, 275	eqtrd 2796	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑧 ∈ ((𝑋 ∩ 𝑌) ∖ {𝐶})) → (((𝐺‘𝑧) − (𝐺‘𝐶)) · (𝐹‘𝐶)) = (((𝐹‘𝐶) · (𝐺‘𝑧)) − ((𝐹‘𝐶) · (𝐺‘𝐶))))
277	273, 276	oveq12d 7438	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑧 ∈ ((𝑋 ∩ 𝑌) ∖ {𝐶})) → ((((𝐹‘𝑧) − (𝐹‘𝐶)) · (𝐺‘𝑧)) + (((𝐺‘𝑧) − (𝐺‘𝐶)) · (𝐹‘𝐶))) = ((((𝐹‘𝑧) · (𝐺‘𝑧)) − ((𝐹‘𝐶) · (𝐺‘𝑧))) + (((𝐹‘𝐶) · (𝐺‘𝑧)) − ((𝐹‘𝐶) · (𝐺‘𝐶)))))
278	6	ffnd 6710	. . . . . . . . . . . 12 ⊢ (𝜑 → 𝐹 Fn 𝑋)
279	278	adantr 486	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑧 ∈ ((𝑋 ∩ 𝑌) ∖ {𝐶})) → 𝐹 Fn 𝑋)
280	13	ffnd 6710	. . . . . . . . . . . 12 ⊢ (𝜑 → 𝐺 Fn 𝑌)
281	280	adantr 486	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑧 ∈ ((𝑋 ∩ 𝑌) ∖ {𝐶})) → 𝐺 Fn 𝑌)
282		ssexg 5281	. . . . . . . . . . . . 13 ⊢ ((𝑋 ⊆ ℂ ∧ ℂ ∈ V) → 𝑋 ∈ V)
283	46, 110, 282	sylancl 598	. . . . . . . . . . . 12 ⊢ (𝜑 → 𝑋 ∈ V)
284	283	adantr 486	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑧 ∈ ((𝑋 ∩ 𝑌) ∖ {𝐶})) → 𝑋 ∈ V)
285		ssexg 5281	. . . . . . . . . . . . 13 ⊢ ((𝑌 ⊆ ℂ ∧ ℂ ∈ V) → 𝑌 ∈ V)
286	64, 110, 285	sylancl 598	. . . . . . . . . . . 12 ⊢ (𝜑 → 𝑌 ∈ V)
287	286	adantr 486	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑧 ∈ ((𝑋 ∩ 𝑌) ∖ {𝐶})) → 𝑌 ∈ V)
288		eqid 2761	. . . . . . . . . . 11 ⊢ (𝑋 ∩ 𝑌) = (𝑋 ∩ 𝑌)
289		eqidd 2762	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑧 ∈ ((𝑋 ∩ 𝑌) ∖ {𝐶})) ∧ 𝑧 ∈ 𝑋) → (𝐹‘𝑧) = (𝐹‘𝑧))
290		eqidd 2762	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑧 ∈ ((𝑋 ∩ 𝑌) ∖ {𝐶})) ∧ 𝑧 ∈ 𝑌) → (𝐺‘𝑧) = (𝐺‘𝑧))
291	279, 281, 284, 287, 288, 289, 290	ofval 7704	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑧 ∈ ((𝑋 ∩ 𝑌) ∖ {𝐶})) ∧ 𝑧 ∈ (𝑋 ∩ 𝑌)) → ((𝐹 ∘_f · 𝐺)‘𝑧) = ((𝐹‘𝑧) · (𝐺‘𝑧)))
292	35, 291	mpdan 700	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑧 ∈ ((𝑋 ∩ 𝑌) ∖ {𝐶})) → ((𝐹 ∘_f · 𝐺)‘𝑧) = ((𝐹‘𝑧) · (𝐺‘𝑧)))
293		eqidd 2762	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑧 ∈ ((𝑋 ∩ 𝑌) ∖ {𝐶})) ∧ 𝐶 ∈ 𝑋) → (𝐹‘𝐶) = (𝐹‘𝐶))
294		eqidd 2762	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑧 ∈ ((𝑋 ∩ 𝑌) ∖ {𝐶})) ∧ 𝐶 ∈ 𝑌) → (𝐺‘𝐶) = (𝐺‘𝐶))
295	279, 281, 284, 287, 288, 293, 294	ofval 7704	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑧 ∈ ((𝑋 ∩ 𝑌) ∖ {𝐶})) ∧ 𝐶 ∈ (𝑋 ∩ 𝑌)) → ((𝐹 ∘_f · 𝐺)‘𝐶) = ((𝐹‘𝐶) · (𝐺‘𝐶)))
296	127, 295	mpidan 702	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑧 ∈ ((𝑋 ∩ 𝑌) ∖ {𝐶})) → ((𝐹 ∘_f · 𝐺)‘𝐶) = ((𝐹‘𝐶) · (𝐺‘𝐶)))
297	292, 296	oveq12d 7438	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑧 ∈ ((𝑋 ∩ 𝑌) ∖ {𝐶})) → (((𝐹 ∘_f · 𝐺)‘𝑧) − ((𝐹 ∘_f · 𝐺)‘𝐶)) = (((𝐹‘𝑧) · (𝐺‘𝑧)) − ((𝐹‘𝐶) · (𝐺‘𝐶))))
298	272, 277, 297	3eqtr4d 2806	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑧 ∈ ((𝑋 ∩ 𝑌) ∖ {𝐶})) → ((((𝐹‘𝑧) − (𝐹‘𝐶)) · (𝐺‘𝑧)) + (((𝐺‘𝑧) − (𝐺‘𝐶)) · (𝐹‘𝐶))) = (((𝐹 ∘_f · 𝐺)‘𝑧) − ((𝐹 ∘_f · 𝐺)‘𝐶)))
299	298	oveq1d 7435	. . . . . 6 ⊢ ((𝜑 ∧ 𝑧 ∈ ((𝑋 ∩ 𝑌) ∖ {𝐶})) → (((((𝐹‘𝑧) − (𝐹‘𝐶)) · (𝐺‘𝑧)) + (((𝐺‘𝑧) − (𝐺‘𝐶)) · (𝐹‘𝐶))) / (𝑧 − 𝐶)) = ((((𝐹 ∘_f · 𝐺)‘𝑧) − ((𝐹 ∘_f · 𝐺)‘𝐶)) / (𝑧 − 𝐶)))
300	260, 59, 267, 54	div23d 12130	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑧 ∈ ((𝑋 ∩ 𝑌) ∖ {𝐶})) → ((((𝐹‘𝑧) − (𝐹‘𝐶)) · (𝐺‘𝑧)) / (𝑧 − 𝐶)) = ((((𝐹‘𝑧) − (𝐹‘𝐶)) / (𝑧 − 𝐶)) · (𝐺‘𝑧)))
301	264, 243, 267, 54	div23d 12130	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑧 ∈ ((𝑋 ∩ 𝑌) ∖ {𝐶})) → ((((𝐺‘𝑧) − (𝐺‘𝐶)) · (𝐹‘𝐶)) / (𝑧 − 𝐶)) = ((((𝐺‘𝑧) − (𝐺‘𝐶)) / (𝑧 − 𝐶)) · (𝐹‘𝐶)))
302	300, 301	oveq12d 7438	. . . . . 6 ⊢ ((𝜑 ∧ 𝑧 ∈ ((𝑋 ∩ 𝑌) ∖ {𝐶})) → (((((𝐹‘𝑧) − (𝐹‘𝐶)) · (𝐺‘𝑧)) / (𝑧 − 𝐶)) + ((((𝐺‘𝑧) − (𝐺‘𝐶)) · (𝐹‘𝐶)) / (𝑧 − 𝐶))) = (((((𝐹‘𝑧) − (𝐹‘𝐶)) / (𝑧 − 𝐶)) · (𝐺‘𝑧)) + ((((𝐺‘𝑧) − (𝐺‘𝐶)) / (𝑧 − 𝐶)) · (𝐹‘𝐶))))
303	268, 299, 302	3eqtr3d 2804	. . . . 5 ⊢ ((𝜑 ∧ 𝑧 ∈ ((𝑋 ∩ 𝑌) ∖ {𝐶})) → ((((𝐹 ∘_f · 𝐺)‘𝑧) − ((𝐹 ∘_f · 𝐺)‘𝐶)) / (𝑧 − 𝐶)) = (((((𝐹‘𝑧) − (𝐹‘𝐶)) / (𝑧 − 𝐶)) · (𝐺‘𝑧)) + ((((𝐺‘𝑧) − (𝐺‘𝐶)) / (𝑧 − 𝐶)) · (𝐹‘𝐶))))
304	303	mpteq2dva 5198	. . . 4 ⊢ (𝜑 → (𝑧 ∈ ((𝑋 ∩ 𝑌) ∖ {𝐶}) ↦ ((((𝐹 ∘_f · 𝐺)‘𝑧) − ((𝐹 ∘_f · 𝐺)‘𝐶)) / (𝑧 − 𝐶))) = (𝑧 ∈ ((𝑋 ∩ 𝑌) ∖ {𝐶}) ↦ (((((𝐹‘𝑧) − (𝐹‘𝐶)) / (𝑧 − 𝐶)) · (𝐺‘𝑧)) + ((((𝐺‘𝑧) − (𝐺‘𝐶)) / (𝑧 − 𝐶)) · (𝐹‘𝐶)))))
305	304	oveq1d 7435	. . 3 ⊢ (𝜑 → ((𝑧 ∈ ((𝑋 ∩ 𝑌) ∖ {𝐶}) ↦ ((((𝐹 ∘_f · 𝐺)‘𝑧) − ((𝐹 ∘_f · 𝐺)‘𝐶)) / (𝑧 − 𝐶))) lim_ℂ 𝐶) = ((𝑧 ∈ ((𝑋 ∩ 𝑌) ∖ {𝐶}) ↦ (((((𝐹‘𝑧) − (𝐹‘𝐶)) / (𝑧 − 𝐶)) · (𝐺‘𝑧)) + ((((𝐺‘𝑧) − (𝐺‘𝐶)) / (𝑧 − 𝐶)) · (𝐹‘𝐶)))) lim_ℂ 𝐶))
306	259, 305	eleqtrrd 2864	. 2 ⊢ (𝜑 → ((𝐾 · (𝐺‘𝐶)) + (𝐿 · (𝐹‘𝐶))) ∈ ((𝑧 ∈ ((𝑋 ∩ 𝑌) ∖ {𝐶}) ↦ ((((𝐹 ∘_f · 𝐺)‘𝑧) − ((𝐹 ∘_f · 𝐺)‘𝐶)) / (𝑧 − 𝐶))) lim_ℂ 𝐶))
307		eqid 2761	. . 3 ⊢ (𝑧 ∈ ((𝑋 ∩ 𝑌) ∖ {𝐶}) ↦ ((((𝐹 ∘_f · 𝐺)‘𝑧) − ((𝐹 ∘_f · 𝐺)‘𝐶)) / (𝑧 − 𝐶))) = (𝑧 ∈ ((𝑋 ∩ 𝑌) ∖ {𝐶}) ↦ ((((𝐹 ∘_f · 𝐺)‘𝑧) − ((𝐹 ∘_f · 𝐺)‘𝐶)) / (𝑧 − 𝐶)))
308		mulcl 11284	. . . . 5 ⊢ ((𝑥 ∈ ℂ ∧ 𝑦 ∈ ℂ) → (𝑥 · 𝑦) ∈ ℂ)
309	308	adantl 487	. . . 4 ⊢ ((𝜑 ∧ (𝑥 ∈ ℂ ∧ 𝑦 ∈ ℂ)) → (𝑥 · 𝑦) ∈ ℂ)
310	309, 6, 13, 283, 286, 288	off 7711	. . 3 ⊢ (𝜑 → (𝐹 ∘_f · 𝐺):(𝑋 ∩ 𝑌)⟶ℂ)
311	2, 3, 307, 5, 310, 84	eldv 26218	. 2 ⊢ (𝜑 → (𝐶(𝑆 D (𝐹 ∘_f · 𝐺))((𝐾 · (𝐺‘𝐶)) + (𝐿 · (𝐹‘𝐶))) ↔ (𝐶 ∈ ((int‘(𝐽 ↾_t 𝑆))‘(𝑋 ∩ 𝑌)) ∧ ((𝐾 · (𝐺‘𝐶)) + (𝐿 · (𝐹‘𝐶))) ∈ ((𝑧 ∈ ((𝑋 ∩ 𝑌) ∖ {𝐶}) ↦ ((((𝐹 ∘_f · 𝐺)‘𝑧) − ((𝐹 ∘_f · 𝐺)‘𝐶)) / (𝑧 − 𝐶))) lim_ℂ 𝐶))))
312	31, 306, 311	mpbir2and 726	1 ⊢ (𝜑 → 𝐶(𝑆 D (𝐹 ∘_f · 𝐺))((𝐾 · (𝐺‘𝐶)) + (𝐿 · (𝐹‘𝐶))))

Colors of variables: wff setvar class

This proof depends on syntax axioms: → wi 4 ↔ wb 209 ∧ wa 401 = wceq 1570 ∈ wcel 2145 ≠ wne 2956 Vcvv 3451 ∖ cdif 3896 ∪ cun 3897 ∩ cin 3898 ⊆ wss 3899 {csn 4584 ⟨cop 4590 ∪ cuni 4867 class class class wbr 5103 {copab 5167 ↦ cmpt 5186 × cxp 5649 dom cdm 5651 ↾ cres 5653 Rel wrel 5656 Fn wfn 6533 ⟶wf 6534 ‘cfv 6538 (class class class)co 7420 ∈ cmpo 7422 ∘_f cof 7691 ℂcc 11198 + caddc 11203 · cmul 11205 − cmin 11541 / cdiv 11973 ↾_t crest 17591 TopOpenctopn 17592 ℂ_fldccnfld 21678 Topctop 23211 TopOnctopon 23228 intcnt 23335 Cn ccn 23542 CnP ccnp 23543 ×_t ctx 23879 –cn→ccncf 25197 lim_ℂ climc 26182 D cdv 26183

This proof depends on axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1828 ax-4 1842 ax-5 1943 ax-6 2000 ax-7 2041 ax-8 2147 ax-9 2155 ax-10 2178 ax-11 2194 ax-12 2213 ax-ext 2733 ax-rep 5232 ax-sep 5249 ax-nul 5260 ax-pow 5327 ax-pr 5391 ax-un 7751 ax-cnex 11256 ax-resscn 11257 ax-1cn 11258 ax-icn 11259 ax-addcl 11260 ax-addrcl 11261 ax-mulcl 11262 ax-mulrcl 11263 ax-mulcom 11264 ax-addass 11265 ax-mulass 11266 ax-distr 11267 ax-i2m1 11268 ax-1ne0 11269 ax-1rid 11270 ax-rnegex 11271 ax-rrecex 11272 ax-cnre 11273 ax-pre-lttri 11274 ax-pre-lttrn 11275 ax-pre-ltadd 11276 ax-pre-mulgt0 11277 ax-pre-sup 11278 ax-addf 11279

This proof depends on definitions: df-bi 210 df-an 402 df-or 862 df-3or 1104 df-3an 1105 df-tru 1573 df-fal 1583 df-ex 1813 df-nf 1817 df-sb 2100 df-mo 2565 df-eu 2595 df-clab 2740 df-cleq 2753 df-clel 2836 df-nfc 2910 df-ne 2957 df-nel 3063 df-ral 3078 df-rex 3088 df-rmo 3366 df-reu 3367 df-rab 3414 df-v 3453 df-sbc 3740 df-csb 3848 df-dif 3902 df-un 3904 df-in 3906 df-ss 3916 df-pss 3919 df-nul 4280 df-if 4483 df-pw 4559 df-sn 4585 df-pr 4587 df-tp 4589 df-op 4591 df-uni 4868 df-int 4908 df-iun 4953 df-iin 4954 df-br 5104 df-opab 5168 df-mpt 5187 df-tr 5213 df-id 5546 df-eprel 5551 df-po 5559 df-so 5560 df-fr 5604 df-se 5605 df-we 5606 df-xp 5657 df-rel 5658 df-cnv 5659 df-co 5660 df-dm 5661 df-rn 5662 df-res 5663 df-ima 5664 df-pred 6304 df-ord 6365 df-on 6366 df-lim 6367 df-suc 6368 df-iota 6494 df-fun 6540 df-fn 6541 df-f 6542 df-f1 6543 df-fo 6544 df-f1o 6545 df-fv 6546 df-isom 6547 df-riota 7377 df-ov 7423 df-oprab 7424 df-mpo 7425 df-of 7693 df-om 7878 df-1st 8001 df-2nd 8002 df-supp 8178 df-frecs 8299 df-wrecs 8330 df-recs 8379 df-rdg 8418 df-1o 8476 df-2o 8477 df-er 8717 df-map 8849 df-pm 8850 df-ixp 8926 df-en 8974 df-dom 8975 df-sdom 8976 df-fin 8977 df-fsupp 9354 df-fi 9403 df-sup 9434 df-inf 9435 df-oi 9504 df-card 10020 df-pnf 11345 df-mnf 11346 df-xr 11347 df-ltxr 11348 df-le 11349 df-sub 11543 df-neg 11544 df-div 11974 df-nn 12336 df-2 12405 df-3 12406 df-4 12407 df-5 12408 df-6 12409 df-7 12410 df-8 12411 df-9 12412 df-n0 12607 df-z 12694 df-dec 12815 df-uz 12966 df-q 13076 df-rp 13121 df-xneg 13241 df-xadd 13242 df-xmul 13243 df-icc 13483 df-fz 13640 df-fzo 13789 df-seq 14145 df-exp 14205 df-hash 14475 df-cj 15266 df-re 15267 df-im 15268 df-sqrt 15402 df-abs 15403 df-struct 17325 df-sets 17342 df-slot 17360 df-ndx 17372 df-base 17388 df-ress 17409 df-plusg 17441 df-mulr 17442 df-starv 17443 df-sca 17444 df-vsca 17445 df-ip 17446 df-tset 17447 df-ple 17448 df-ds 17450 df-unif 17451 df-hom 17452 df-cco 17453 df-rest 17593 df-topn 17594 df-0g 17612 df-gsum 17613 df-topgen 17614 df-pt 17615 df-prds 17618 df-xrs 17674 df-qtop 17679 df-imas 17680 df-xps 17682 df-mre 17756 df-mrc 17757 df-acs 17759 df-mgm 18816 df-sgrp 18908 df-mnd 18924 df-submnd 18979 df-mulg 19278 df-cntz 19531 df-cmn 19996 df-psmet 21670 df-xmet 21671 df-met 21672 df-bl 21673 df-mopn 21674 df-cnfld 21679 df-top 23212 df-topon 23229 df-topsp 23251 df-bases 23264 df-cld 23337 df-ntr 23338 df-cls 23339 df-cn 23545 df-cnp 23546 df-tx 23881 df-hmeo 24074 df-xms 24639 df-ms 24640 df-tms 24641 df-cncf 25199 df-limc 26186 df-dv 26187

This theorem is used by: dvmul 26261 dvmulf 26263 dvef 26300

W3C validator