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 25906

Description: The product rule for derivatives at a point. For the (simpler but more limited) function version, see dvmul 25908. (Contributed by Mario Carneiro, 9-Aug-2014.) (Revised by Mario Carneiro, 28-Dec-2016.) Avoid ax-mulf 11118 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 2736	. . . . . . 7 ⊢ (𝐽 ↾_t 𝑆) = (𝐽 ↾_t 𝑆)
3		dvadd.j	. . . . . . 7 ⊢ 𝐽 = (TopOpen‘ℂ_fld)
4		eqid 2736	. . . . . . 7 ⊢ (𝑧 ∈ (𝑋 ∖ {𝐶}) ↦ (((𝐹‘𝑧) − (𝐹‘𝐶)) / (𝑧 − 𝐶))) = (𝑧 ∈ (𝑋 ∖ {𝐶}) ↦ (((𝐹‘𝑧) − (𝐹‘𝐶)) / (𝑧 − 𝐶)))
5		dvaddbr.s	. . . . . . 7 ⊢ (𝜑 → 𝑆 ⊆ ℂ)
6		dvadd.f	. . . . . . 7 ⊢ (𝜑 → 𝐹:𝑋⟶ℂ)
7		dvadd.x	. . . . . . 7 ⊢ (𝜑 → 𝑋 ⊆ 𝑆)
8	2, 3, 4, 5, 6, 7	eldv 25865	. . . . . 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 2736	. . . . . . 7 ⊢ (𝑧 ∈ (𝑌 ∖ {𝐶}) ↦ (((𝐺‘𝑧) − (𝐺‘𝐶)) / (𝑧 − 𝐶))) = (𝑧 ∈ (𝑌 ∖ {𝐶}) ↦ (((𝐺‘𝑧) − (𝐺‘𝐶)) / (𝑧 − 𝐶)))
13		dvadd.g	. . . . . . 7 ⊢ (𝜑 → 𝐺:𝑌⟶ℂ)
14		dvadd.y	. . . . . . 7 ⊢ (𝜑 → 𝑌 ⊆ 𝑆)
15	2, 3, 12, 5, 13, 14	eldv 25865	. . . . . 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 4140	. . 3 ⊢ (𝜑 → 𝐶 ∈ (((int‘(𝐽 ↾_t 𝑆))‘𝑋) ∩ ((int‘(𝐽 ↾_t 𝑆))‘𝑌)))
19	3	cnfldtopon 24747	. . . . . 6 ⊢ 𝐽 ∈ (TopOn‘ℂ)
20		resttopon 23126	. . . . . 6 ⊢ ((𝐽 ∈ (TopOn‘ℂ) ∧ 𝑆 ⊆ ℂ) → (𝐽 ↾_t 𝑆) ∈ (TopOn‘𝑆))
21	19, 5, 20	sylancr 588	. . . . 5 ⊢ (𝜑 → (𝐽 ↾_t 𝑆) ∈ (TopOn‘𝑆))
22		topontop 22878	. . . . 5 ⊢ ((𝐽 ↾_t 𝑆) ∈ (TopOn‘𝑆) → (𝐽 ↾_t 𝑆) ∈ Top)
23	21, 22	syl 17	. . . 4 ⊢ (𝜑 → (𝐽 ↾_t 𝑆) ∈ Top)
24		toponuni 22879	. . . . . 6 ⊢ ((𝐽 ↾_t 𝑆) ∈ (TopOn‘𝑆) → 𝑆 = ∪ (𝐽 ↾_t 𝑆))
25	21, 24	syl 17	. . . . 5 ⊢ (𝜑 → 𝑆 = ∪ (𝐽 ↾_t 𝑆))
26	7, 25	sseqtrd 3958	. . . 4 ⊢ (𝜑 → 𝑋 ⊆ ∪ (𝐽 ↾_t 𝑆))
27	14, 25	sseqtrd 3958	. . . 4 ⊢ (𝜑 → 𝑌 ⊆ ∪ (𝐽 ↾_t 𝑆))
28		eqid 2736	. . . . 5 ⊢ ∪ (𝐽 ↾_t 𝑆) = ∪ (𝐽 ↾_t 𝑆)
29	28	ntrin 23026	. . . 4 ⊢ (((𝐽 ↾_t 𝑆) ∈ Top ∧ 𝑋 ⊆ ∪ (𝐽 ↾_t 𝑆) ∧ 𝑌 ⊆ ∪ (𝐽 ↾_t 𝑆)) → ((int‘(𝐽 ↾_t 𝑆))‘(𝑋 ∩ 𝑌)) = (((int‘(𝐽 ↾_t 𝑆))‘𝑋) ∩ ((int‘(𝐽 ↾_t 𝑆))‘𝑌)))
30	23, 26, 27, 29	syl3anc 1374	. . 3 ⊢ (𝜑 → ((int‘(𝐽 ↾_t 𝑆))‘(𝑋 ∩ 𝑌)) = (((int‘(𝐽 ↾_t 𝑆))‘𝑋) ∩ ((int‘(𝐽 ↾_t 𝑆))‘𝑌)))
31	18, 30	eleqtrrd 2839	. 2 ⊢ (𝜑 → 𝐶 ∈ ((int‘(𝐽 ↾_t 𝑆))‘(𝑋 ∩ 𝑌)))
32	6	adantr 480	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑧 ∈ ((𝑋 ∩ 𝑌) ∖ {𝐶})) → 𝐹:𝑋⟶ℂ)
33		inss1 4177	. . . . . . . . 9 ⊢ (𝑋 ∩ 𝑌) ⊆ 𝑋
34		eldifi 4071	. . . . . . . . . 10 ⊢ (𝑧 ∈ ((𝑋 ∩ 𝑌) ∖ {𝐶}) → 𝑧 ∈ (𝑋 ∩ 𝑌))
35	34	adantl 481	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑧 ∈ ((𝑋 ∩ 𝑌) ∖ {𝐶})) → 𝑧 ∈ (𝑋 ∩ 𝑌))
36	33, 35	sselid 3919	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑧 ∈ ((𝑋 ∩ 𝑌) ∖ {𝐶})) → 𝑧 ∈ 𝑋)
37	32, 36	ffvelcdmd 7037	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑧 ∈ ((𝑋 ∩ 𝑌) ∖ {𝐶})) → (𝐹‘𝑧) ∈ ℂ)
38	5, 6, 7	dvbss 25868	. . . . . . . . . 10 ⊢ (𝜑 → dom (𝑆 D 𝐹) ⊆ 𝑋)
39		reldv 25837	. . . . . . . . . . 11 ⊢ Rel (𝑆 D 𝐹)
40		releldm 5899	. . . . . . . . . . 11 ⊢ ((Rel (𝑆 D 𝐹) ∧ 𝐶(𝑆 D 𝐹)𝐾) → 𝐶 ∈ dom (𝑆 D 𝐹))
41	39, 1, 40	sylancr 588	. . . . . . . . . 10 ⊢ (𝜑 → 𝐶 ∈ dom (𝑆 D 𝐹))
42	38, 41	sseldd 3922	. . . . . . . . 9 ⊢ (𝜑 → 𝐶 ∈ 𝑋)
43	6, 42	ffvelcdmd 7037	. . . . . . . 8 ⊢ (𝜑 → (𝐹‘𝐶) ∈ ℂ)
44	43	adantr 480	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑧 ∈ ((𝑋 ∩ 𝑌) ∖ {𝐶})) → (𝐹‘𝐶) ∈ ℂ)
45	37, 44	subcld 11505	. . . . . 6 ⊢ ((𝜑 ∧ 𝑧 ∈ ((𝑋 ∩ 𝑌) ∖ {𝐶})) → ((𝐹‘𝑧) − (𝐹‘𝐶)) ∈ ℂ)
46	7, 5	sstrd 3932	. . . . . . . . 9 ⊢ (𝜑 → 𝑋 ⊆ ℂ)
47	46	adantr 480	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑧 ∈ ((𝑋 ∩ 𝑌) ∖ {𝐶})) → 𝑋 ⊆ ℂ)
48	47, 36	sseldd 3922	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑧 ∈ ((𝑋 ∩ 𝑌) ∖ {𝐶})) → 𝑧 ∈ ℂ)
49	46, 42	sseldd 3922	. . . . . . . 8 ⊢ (𝜑 → 𝐶 ∈ ℂ)
50	49	adantr 480	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑧 ∈ ((𝑋 ∩ 𝑌) ∖ {𝐶})) → 𝐶 ∈ ℂ)
51	48, 50	subcld 11505	. . . . . 6 ⊢ ((𝜑 ∧ 𝑧 ∈ ((𝑋 ∩ 𝑌) ∖ {𝐶})) → (𝑧 − 𝐶) ∈ ℂ)
52		eldifsni 4735	. . . . . . . 8 ⊢ (𝑧 ∈ ((𝑋 ∩ 𝑌) ∖ {𝐶}) → 𝑧 ≠ 𝐶)
53	52	adantl 481	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑧 ∈ ((𝑋 ∩ 𝑌) ∖ {𝐶})) → 𝑧 ≠ 𝐶)
54	48, 50, 53	subne0d 11514	. . . . . 6 ⊢ ((𝜑 ∧ 𝑧 ∈ ((𝑋 ∩ 𝑌) ∖ {𝐶})) → (𝑧 − 𝐶) ≠ 0)
55	45, 51, 54	divcld 11931	. . . . 5 ⊢ ((𝜑 ∧ 𝑧 ∈ ((𝑋 ∩ 𝑌) ∖ {𝐶})) → (((𝐹‘𝑧) − (𝐹‘𝐶)) / (𝑧 − 𝐶)) ∈ ℂ)
56	13	adantr 480	. . . . . 6 ⊢ ((𝜑 ∧ 𝑧 ∈ ((𝑋 ∩ 𝑌) ∖ {𝐶})) → 𝐺:𝑌⟶ℂ)
57		inss2 4178	. . . . . . 7 ⊢ (𝑋 ∩ 𝑌) ⊆ 𝑌
58	57, 35	sselid 3919	. . . . . 6 ⊢ ((𝜑 ∧ 𝑧 ∈ ((𝑋 ∩ 𝑌) ∖ {𝐶})) → 𝑧 ∈ 𝑌)
59	56, 58	ffvelcdmd 7037	. . . . 5 ⊢ ((𝜑 ∧ 𝑧 ∈ ((𝑋 ∩ 𝑌) ∖ {𝐶})) → (𝐺‘𝑧) ∈ ℂ)
60	55, 59	mulcld 11165	. . . 4 ⊢ ((𝜑 ∧ 𝑧 ∈ ((𝑋 ∩ 𝑌) ∖ {𝐶})) → ((((𝐹‘𝑧) − (𝐹‘𝐶)) / (𝑧 − 𝐶)) · (𝐺‘𝑧)) ∈ ℂ)
61		ssdif 4084	. . . . . . . 8 ⊢ ((𝑋 ∩ 𝑌) ⊆ 𝑌 → ((𝑋 ∩ 𝑌) ∖ {𝐶}) ⊆ (𝑌 ∖ {𝐶}))
62	57, 61	mp1i 13	. . . . . . 7 ⊢ (𝜑 → ((𝑋 ∩ 𝑌) ∖ {𝐶}) ⊆ (𝑌 ∖ {𝐶}))
63	62	sselda 3921	. . . . . 6 ⊢ ((𝜑 ∧ 𝑧 ∈ ((𝑋 ∩ 𝑌) ∖ {𝐶})) → 𝑧 ∈ (𝑌 ∖ {𝐶}))
64	14, 5	sstrd 3932	. . . . . . 7 ⊢ (𝜑 → 𝑌 ⊆ ℂ)
65	5, 13, 14	dvbss 25868	. . . . . . . 8 ⊢ (𝜑 → dom (𝑆 D 𝐺) ⊆ 𝑌)
66		reldv 25837	. . . . . . . . 9 ⊢ Rel (𝑆 D 𝐺)
67		releldm 5899	. . . . . . . . 9 ⊢ ((Rel (𝑆 D 𝐺) ∧ 𝐶(𝑆 D 𝐺)𝐿) → 𝐶 ∈ dom (𝑆 D 𝐺))
68	66, 11, 67	sylancr 588	. . . . . . . 8 ⊢ (𝜑 → 𝐶 ∈ dom (𝑆 D 𝐺))
69	65, 68	sseldd 3922	. . . . . . 7 ⊢ (𝜑 → 𝐶 ∈ 𝑌)
70	13, 64, 69	dvlem 25863	. . . . . 6 ⊢ ((𝜑 ∧ 𝑧 ∈ (𝑌 ∖ {𝐶})) → (((𝐺‘𝑧) − (𝐺‘𝐶)) / (𝑧 − 𝐶)) ∈ ℂ)
71	63, 70	syldan 592	. . . . 5 ⊢ ((𝜑 ∧ 𝑧 ∈ ((𝑋 ∩ 𝑌) ∖ {𝐶})) → (((𝐺‘𝑧) − (𝐺‘𝐶)) / (𝑧 − 𝐶)) ∈ ℂ)
72	71, 44	mulcld 11165	. . . 4 ⊢ ((𝜑 ∧ 𝑧 ∈ ((𝑋 ∩ 𝑌) ∖ {𝐶})) → ((((𝐺‘𝑧) − (𝐺‘𝐶)) / (𝑧 − 𝐶)) · (𝐹‘𝐶)) ∈ ℂ)
73		ssidd 3945	. . . 4 ⊢ (𝜑 → ℂ ⊆ ℂ)
74		txtopon 23556	. . . . . 6 ⊢ ((𝐽 ∈ (TopOn‘ℂ) ∧ 𝐽 ∈ (TopOn‘ℂ)) → (𝐽 ×_t 𝐽) ∈ (TopOn‘(ℂ × ℂ)))
75	19, 19, 74	mp2an 693	. . . . 5 ⊢ (𝐽 ×_t 𝐽) ∈ (TopOn‘(ℂ × ℂ))
76	75	toponrestid 22886	. . . 4 ⊢ (𝐽 ×_t 𝐽) = ((𝐽 ×_t 𝐽) ↾_t (ℂ × ℂ))
77	9	simprd 495	. . . . . . . 8 ⊢ (𝜑 → 𝐾 ∈ ((𝑧 ∈ (𝑋 ∖ {𝐶}) ↦ (((𝐹‘𝑧) − (𝐹‘𝐶)) / (𝑧 − 𝐶))) lim_ℂ 𝐶))
78	6, 46, 42	dvlem 25863	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑧 ∈ (𝑋 ∖ {𝐶})) → (((𝐹‘𝑧) − (𝐹‘𝐶)) / (𝑧 − 𝐶)) ∈ ℂ)
79	78	fmpttd 7067	. . . . . . . . . 10 ⊢ (𝜑 → (𝑧 ∈ (𝑋 ∖ {𝐶}) ↦ (((𝐹‘𝑧) − (𝐹‘𝐶)) / (𝑧 − 𝐶))):(𝑋 ∖ {𝐶})⟶ℂ)
80		ssdif 4084	. . . . . . . . . . 11 ⊢ ((𝑋 ∩ 𝑌) ⊆ 𝑋 → ((𝑋 ∩ 𝑌) ∖ {𝐶}) ⊆ (𝑋 ∖ {𝐶}))
81	33, 80	mp1i 13	. . . . . . . . . 10 ⊢ (𝜑 → ((𝑋 ∩ 𝑌) ∖ {𝐶}) ⊆ (𝑋 ∖ {𝐶}))
82	46	ssdifssd 4087	. . . . . . . . . 10 ⊢ (𝜑 → (𝑋 ∖ {𝐶}) ⊆ ℂ)
83		eqid 2736	. . . . . . . . . 10 ⊢ (𝐽 ↾_t ((𝑋 ∖ {𝐶}) ∪ {𝐶})) = (𝐽 ↾_t ((𝑋 ∖ {𝐶}) ∪ {𝐶}))
84	33, 7	sstrid 3933	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → (𝑋 ∩ 𝑌) ⊆ 𝑆)
85	84, 25	sseqtrd 3958	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (𝑋 ∩ 𝑌) ⊆ ∪ (𝐽 ↾_t 𝑆))
86		difssd 4077	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (∪ (𝐽 ↾_t 𝑆) ∖ 𝑋) ⊆ ∪ (𝐽 ↾_t 𝑆))
87	85, 86	unssd 4132	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → ((𝑋 ∩ 𝑌) ∪ (∪ (𝐽 ↾_t 𝑆) ∖ 𝑋)) ⊆ ∪ (𝐽 ↾_t 𝑆))
88		ssun1 4118	. . . . . . . . . . . . . . . 16 ⊢ (𝑋 ∩ 𝑌) ⊆ ((𝑋 ∩ 𝑌) ∪ (∪ (𝐽 ↾_t 𝑆) ∖ 𝑋))
89	88	a1i 11	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (𝑋 ∩ 𝑌) ⊆ ((𝑋 ∩ 𝑌) ∪ (∪ (𝐽 ↾_t 𝑆) ∖ 𝑋)))
90	28	ntrss 23020	. . . . . . . . . . . . . . 15 ⊢ (((𝐽 ↾_t 𝑆) ∈ Top ∧ ((𝑋 ∩ 𝑌) ∪ (∪ (𝐽 ↾_t 𝑆) ∖ 𝑋)) ⊆ ∪ (𝐽 ↾_t 𝑆) ∧ (𝑋 ∩ 𝑌) ⊆ ((𝑋 ∩ 𝑌) ∪ (∪ (𝐽 ↾_t 𝑆) ∖ 𝑋))) → ((int‘(𝐽 ↾_t 𝑆))‘(𝑋 ∩ 𝑌)) ⊆ ((int‘(𝐽 ↾_t 𝑆))‘((𝑋 ∩ 𝑌) ∪ (∪ (𝐽 ↾_t 𝑆) ∖ 𝑋))))
91	23, 87, 89, 90	syl3anc 1374	. . . . . . . . . . . . . 14 ⊢ (𝜑 → ((int‘(𝐽 ↾_t 𝑆))‘(𝑋 ∩ 𝑌)) ⊆ ((int‘(𝐽 ↾_t 𝑆))‘((𝑋 ∩ 𝑌) ∪ (∪ (𝐽 ↾_t 𝑆) ∖ 𝑋))))
92		eqid 2736	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑥 ∈ (𝑋 ∖ {𝐶}) ↦ (((𝐹‘𝑥) − (𝐹‘𝐶)) / (𝑥 − 𝐶))) = (𝑥 ∈ (𝑋 ∖ {𝐶}) ↦ (((𝐹‘𝑥) − (𝐹‘𝐶)) / (𝑥 − 𝐶)))
93	2, 3, 92, 5, 6, 7	eldv 25865	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → (𝐶(𝑆 D 𝐹)𝐾 ↔ (𝐶 ∈ ((int‘(𝐽 ↾_t 𝑆))‘𝑋) ∧ 𝐾 ∈ ((𝑥 ∈ (𝑋 ∖ {𝐶}) ↦ (((𝐹‘𝑥) − (𝐹‘𝐶)) / (𝑥 − 𝐶))) lim_ℂ 𝐶))))
94	1, 93	mpbid 232	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → (𝐶 ∈ ((int‘(𝐽 ↾_t 𝑆))‘𝑋) ∧ 𝐾 ∈ ((𝑥 ∈ (𝑋 ∖ {𝐶}) ↦ (((𝐹‘𝑥) − (𝐹‘𝐶)) / (𝑥 − 𝐶))) lim_ℂ 𝐶)))
95	94	simpld 494	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → 𝐶 ∈ ((int‘(𝐽 ↾_t 𝑆))‘𝑋))
96		eqid 2736	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑥 ∈ (𝑌 ∖ {𝐶}) ↦ (((𝐺‘𝑥) − (𝐺‘𝐶)) / (𝑥 − 𝐶))) = (𝑥 ∈ (𝑌 ∖ {𝐶}) ↦ (((𝐺‘𝑥) − (𝐺‘𝐶)) / (𝑥 − 𝐶)))
97	2, 3, 96, 5, 13, 14	eldv 25865	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → (𝐶(𝑆 D 𝐺)𝐿 ↔ (𝐶 ∈ ((int‘(𝐽 ↾_t 𝑆))‘𝑌) ∧ 𝐿 ∈ ((𝑥 ∈ (𝑌 ∖ {𝐶}) ↦ (((𝐺‘𝑥) − (𝐺‘𝐶)) / (𝑥 − 𝐶))) lim_ℂ 𝐶))))
98	11, 97	mpbid 232	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → (𝐶 ∈ ((int‘(𝐽 ↾_t 𝑆))‘𝑌) ∧ 𝐿 ∈ ((𝑥 ∈ (𝑌 ∖ {𝐶}) ↦ (((𝐺‘𝑥) − (𝐺‘𝐶)) / (𝑥 − 𝐶))) lim_ℂ 𝐶)))
99	98	simpld 494	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → 𝐶 ∈ ((int‘(𝐽 ↾_t 𝑆))‘𝑌))
100	95, 99	elind 4140	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → 𝐶 ∈ (((int‘(𝐽 ↾_t 𝑆))‘𝑋) ∩ ((int‘(𝐽 ↾_t 𝑆))‘𝑌)))
101	100, 30	eleqtrrd 2839	. . . . . . . . . . . . . 14 ⊢ (𝜑 → 𝐶 ∈ ((int‘(𝐽 ↾_t 𝑆))‘(𝑋 ∩ 𝑌)))
102	91, 101	sseldd 3922	. . . . . . . . . . . . 13 ⊢ (𝜑 → 𝐶 ∈ ((int‘(𝐽 ↾_t 𝑆))‘((𝑋 ∩ 𝑌) ∪ (∪ (𝐽 ↾_t 𝑆) ∖ 𝑋))))
103	102, 42	elind 4140	. . . . . . . . . . . 12 ⊢ (𝜑 → 𝐶 ∈ (((int‘(𝐽 ↾_t 𝑆))‘((𝑋 ∩ 𝑌) ∪ (∪ (𝐽 ↾_t 𝑆) ∖ 𝑋))) ∩ 𝑋))
104	33	a1i 11	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (𝑋 ∩ 𝑌) ⊆ 𝑋)
105		eqid 2736	. . . . . . . . . . . . . . 15 ⊢ ((𝐽 ↾_t 𝑆) ↾_t 𝑋) = ((𝐽 ↾_t 𝑆) ↾_t 𝑋)
106	28, 105	restntr 23147	. . . . . . . . . . . . . 14 ⊢ (((𝐽 ↾_t 𝑆) ∈ Top ∧ 𝑋 ⊆ ∪ (𝐽 ↾_t 𝑆) ∧ (𝑋 ∩ 𝑌) ⊆ 𝑋) → ((int‘((𝐽 ↾_t 𝑆) ↾_t 𝑋))‘(𝑋 ∩ 𝑌)) = (((int‘(𝐽 ↾_t 𝑆))‘((𝑋 ∩ 𝑌) ∪ (∪ (𝐽 ↾_t 𝑆) ∖ 𝑋))) ∩ 𝑋))
107	23, 26, 104, 106	syl3anc 1374	. . . . . . . . . . . . 13 ⊢ (𝜑 → ((int‘((𝐽 ↾_t 𝑆) ↾_t 𝑋))‘(𝑋 ∩ 𝑌)) = (((int‘(𝐽 ↾_t 𝑆))‘((𝑋 ∩ 𝑌) ∪ (∪ (𝐽 ↾_t 𝑆) ∖ 𝑋))) ∩ 𝑋))
108	3	cnfldtop 24748	. . . . . . . . . . . . . . . . 17 ⊢ 𝐽 ∈ Top
109	108	a1i 11	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → 𝐽 ∈ Top)
110		cnex 11119	. . . . . . . . . . . . . . . . 17 ⊢ ℂ ∈ V
111		ssexg 5264	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑆 ⊆ ℂ ∧ ℂ ∈ V) → 𝑆 ∈ V)
112	5, 110, 111	sylancl 587	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → 𝑆 ∈ V)
113		restabs 23130	. . . . . . . . . . . . . . . 16 ⊢ ((𝐽 ∈ Top ∧ 𝑋 ⊆ 𝑆 ∧ 𝑆 ∈ V) → ((𝐽 ↾_t 𝑆) ↾_t 𝑋) = (𝐽 ↾_t 𝑋))
114	109, 7, 112, 113	syl3anc 1374	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → ((𝐽 ↾_t 𝑆) ↾_t 𝑋) = (𝐽 ↾_t 𝑋))
115	114	fveq2d 6844	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (int‘((𝐽 ↾_t 𝑆) ↾_t 𝑋)) = (int‘(𝐽 ↾_t 𝑋)))
116	115	fveq1d 6842	. . . . . . . . . . . . 13 ⊢ (𝜑 → ((int‘((𝐽 ↾_t 𝑆) ↾_t 𝑋))‘(𝑋 ∩ 𝑌)) = ((int‘(𝐽 ↾_t 𝑋))‘(𝑋 ∩ 𝑌)))
117	107, 116	eqtr3d 2773	. . . . . . . . . . . 12 ⊢ (𝜑 → (((int‘(𝐽 ↾_t 𝑆))‘((𝑋 ∩ 𝑌) ∪ (∪ (𝐽 ↾_t 𝑆) ∖ 𝑋))) ∩ 𝑋) = ((int‘(𝐽 ↾_t 𝑋))‘(𝑋 ∩ 𝑌)))
118	103, 117	eleqtrd 2838	. . . . . . . . . . 11 ⊢ (𝜑 → 𝐶 ∈ ((int‘(𝐽 ↾_t 𝑋))‘(𝑋 ∩ 𝑌)))
119		undif1 4416	. . . . . . . . . . . . . . 15 ⊢ ((𝑋 ∖ {𝐶}) ∪ {𝐶}) = (𝑋 ∪ {𝐶})
120	42	snssd 4730	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → {𝐶} ⊆ 𝑋)
121		ssequn2 4129	. . . . . . . . . . . . . . . 16 ⊢ ({𝐶} ⊆ 𝑋 ↔ (𝑋 ∪ {𝐶}) = 𝑋)
122	120, 121	sylib 218	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (𝑋 ∪ {𝐶}) = 𝑋)
123	119, 122	eqtrid 2783	. . . . . . . . . . . . . 14 ⊢ (𝜑 → ((𝑋 ∖ {𝐶}) ∪ {𝐶}) = 𝑋)
124	123	oveq2d 7383	. . . . . . . . . . . . 13 ⊢ (𝜑 → (𝐽 ↾_t ((𝑋 ∖ {𝐶}) ∪ {𝐶})) = (𝐽 ↾_t 𝑋))
125	124	fveq2d 6844	. . . . . . . . . . . 12 ⊢ (𝜑 → (int‘(𝐽 ↾_t ((𝑋 ∖ {𝐶}) ∪ {𝐶}))) = (int‘(𝐽 ↾_t 𝑋)))
126		undif1 4416	. . . . . . . . . . . . 13 ⊢ (((𝑋 ∩ 𝑌) ∖ {𝐶}) ∪ {𝐶}) = ((𝑋 ∩ 𝑌) ∪ {𝐶})
127	42, 69	elind 4140	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → 𝐶 ∈ (𝑋 ∩ 𝑌))
128	127	snssd 4730	. . . . . . . . . . . . . 14 ⊢ (𝜑 → {𝐶} ⊆ (𝑋 ∩ 𝑌))
129		ssequn2 4129	. . . . . . . . . . . . . 14 ⊢ ({𝐶} ⊆ (𝑋 ∩ 𝑌) ↔ ((𝑋 ∩ 𝑌) ∪ {𝐶}) = (𝑋 ∩ 𝑌))
130	128, 129	sylib 218	. . . . . . . . . . . . 13 ⊢ (𝜑 → ((𝑋 ∩ 𝑌) ∪ {𝐶}) = (𝑋 ∩ 𝑌))
131	126, 130	eqtrid 2783	. . . . . . . . . . . 12 ⊢ (𝜑 → (((𝑋 ∩ 𝑌) ∖ {𝐶}) ∪ {𝐶}) = (𝑋 ∩ 𝑌))
132	125, 131	fveq12d 6847	. . . . . . . . . . 11 ⊢ (𝜑 → ((int‘(𝐽 ↾_t ((𝑋 ∖ {𝐶}) ∪ {𝐶})))‘(((𝑋 ∩ 𝑌) ∖ {𝐶}) ∪ {𝐶})) = ((int‘(𝐽 ↾_t 𝑋))‘(𝑋 ∩ 𝑌)))
133	118, 132	eleqtrrd 2839	. . . . . . . . . 10 ⊢ (𝜑 → 𝐶 ∈ ((int‘(𝐽 ↾_t ((𝑋 ∖ {𝐶}) ∪ {𝐶})))‘(((𝑋 ∩ 𝑌) ∖ {𝐶}) ∪ {𝐶})))
134	79, 81, 82, 3, 83, 133	limcres 25853	. . . . . . . . 9 ⊢ (𝜑 → (((𝑧 ∈ (𝑋 ∖ {𝐶}) ↦ (((𝐹‘𝑧) − (𝐹‘𝐶)) / (𝑧 − 𝐶))) ↾ ((𝑋 ∩ 𝑌) ∖ {𝐶})) lim_ℂ 𝐶) = ((𝑧 ∈ (𝑋 ∖ {𝐶}) ↦ (((𝐹‘𝑧) − (𝐹‘𝐶)) / (𝑧 − 𝐶))) lim_ℂ 𝐶))
135	81	resmptd 6005	. . . . . . . . . 10 ⊢ (𝜑 → ((𝑧 ∈ (𝑋 ∖ {𝐶}) ↦ (((𝐹‘𝑧) − (𝐹‘𝐶)) / (𝑧 − 𝐶))) ↾ ((𝑋 ∩ 𝑌) ∖ {𝐶})) = (𝑧 ∈ ((𝑋 ∩ 𝑌) ∖ {𝐶}) ↦ (((𝐹‘𝑧) − (𝐹‘𝐶)) / (𝑧 − 𝐶))))
136	135	oveq1d 7382	. . . . . . . . 9 ⊢ (𝜑 → (((𝑧 ∈ (𝑋 ∖ {𝐶}) ↦ (((𝐹‘𝑧) − (𝐹‘𝐶)) / (𝑧 − 𝐶))) ↾ ((𝑋 ∩ 𝑌) ∖ {𝐶})) lim_ℂ 𝐶) = ((𝑧 ∈ ((𝑋 ∩ 𝑌) ∖ {𝐶}) ↦ (((𝐹‘𝑧) − (𝐹‘𝐶)) / (𝑧 − 𝐶))) lim_ℂ 𝐶))
137	134, 136	eqtr3d 2773	. . . . . . . 8 ⊢ (𝜑 → ((𝑧 ∈ (𝑋 ∖ {𝐶}) ↦ (((𝐹‘𝑧) − (𝐹‘𝐶)) / (𝑧 − 𝐶))) lim_ℂ 𝐶) = ((𝑧 ∈ ((𝑋 ∩ 𝑌) ∖ {𝐶}) ↦ (((𝐹‘𝑧) − (𝐹‘𝐶)) / (𝑧 − 𝐶))) lim_ℂ 𝐶))
138	77, 137	eleqtrd 2838	. . . . . . 7 ⊢ (𝜑 → 𝐾 ∈ ((𝑧 ∈ ((𝑋 ∩ 𝑌) ∖ {𝐶}) ↦ (((𝐹‘𝑧) − (𝐹‘𝐶)) / (𝑧 − 𝐶))) lim_ℂ 𝐶))
139		eqid 2736	. . . . . . . . . . . 12 ⊢ (𝐽 ↾_t 𝑌) = (𝐽 ↾_t 𝑌)
140	139, 3	dvcnp2 25887	. . . . . . . . . . 11 ⊢ (((𝑆 ⊆ ℂ ∧ 𝐺:𝑌⟶ℂ ∧ 𝑌 ⊆ 𝑆) ∧ 𝐶 ∈ dom (𝑆 D 𝐺)) → 𝐺 ∈ (((𝐽 ↾_t 𝑌) CnP 𝐽)‘𝐶))
141	5, 13, 14, 68, 140	syl31anc 1376	. . . . . . . . . 10 ⊢ (𝜑 → 𝐺 ∈ (((𝐽 ↾_t 𝑌) CnP 𝐽)‘𝐶))
142	3, 139	cnplimc 25854	. . . . . . . . . . 11 ⊢ ((𝑌 ⊆ ℂ ∧ 𝐶 ∈ 𝑌) → (𝐺 ∈ (((𝐽 ↾_t 𝑌) CnP 𝐽)‘𝐶) ↔ (𝐺:𝑌⟶ℂ ∧ (𝐺‘𝐶) ∈ (𝐺 lim_ℂ 𝐶))))
143	64, 69, 142	syl2anc 585	. . . . . . . . . 10 ⊢ (𝜑 → (𝐺 ∈ (((𝐽 ↾_t 𝑌) CnP 𝐽)‘𝐶) ↔ (𝐺:𝑌⟶ℂ ∧ (𝐺‘𝐶) ∈ (𝐺 lim_ℂ 𝐶))))
144	141, 143	mpbid 232	. . . . . . . . 9 ⊢ (𝜑 → (𝐺:𝑌⟶ℂ ∧ (𝐺‘𝐶) ∈ (𝐺 lim_ℂ 𝐶)))
145	144	simprd 495	. . . . . . . 8 ⊢ (𝜑 → (𝐺‘𝐶) ∈ (𝐺 lim_ℂ 𝐶))
146		difss 4076	. . . . . . . . . . . 12 ⊢ ((𝑋 ∩ 𝑌) ∖ {𝐶}) ⊆ (𝑋 ∩ 𝑌)
147	146, 57	sstri 3931	. . . . . . . . . . 11 ⊢ ((𝑋 ∩ 𝑌) ∖ {𝐶}) ⊆ 𝑌
148	147	a1i 11	. . . . . . . . . 10 ⊢ (𝜑 → ((𝑋 ∩ 𝑌) ∖ {𝐶}) ⊆ 𝑌)
149		eqid 2736	. . . . . . . . . 10 ⊢ (𝐽 ↾_t (𝑌 ∪ {𝐶})) = (𝐽 ↾_t (𝑌 ∪ {𝐶}))
150		difssd 4077	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (∪ (𝐽 ↾_t 𝑆) ∖ 𝑌) ⊆ ∪ (𝐽 ↾_t 𝑆))
151	85, 150	unssd 4132	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → ((𝑋 ∩ 𝑌) ∪ (∪ (𝐽 ↾_t 𝑆) ∖ 𝑌)) ⊆ ∪ (𝐽 ↾_t 𝑆))
152		ssun1 4118	. . . . . . . . . . . . . . . 16 ⊢ (𝑋 ∩ 𝑌) ⊆ ((𝑋 ∩ 𝑌) ∪ (∪ (𝐽 ↾_t 𝑆) ∖ 𝑌))
153	152	a1i 11	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (𝑋 ∩ 𝑌) ⊆ ((𝑋 ∩ 𝑌) ∪ (∪ (𝐽 ↾_t 𝑆) ∖ 𝑌)))
154	28	ntrss 23020	. . . . . . . . . . . . . . 15 ⊢ (((𝐽 ↾_t 𝑆) ∈ Top ∧ ((𝑋 ∩ 𝑌) ∪ (∪ (𝐽 ↾_t 𝑆) ∖ 𝑌)) ⊆ ∪ (𝐽 ↾_t 𝑆) ∧ (𝑋 ∩ 𝑌) ⊆ ((𝑋 ∩ 𝑌) ∪ (∪ (𝐽 ↾_t 𝑆) ∖ 𝑌))) → ((int‘(𝐽 ↾_t 𝑆))‘(𝑋 ∩ 𝑌)) ⊆ ((int‘(𝐽 ↾_t 𝑆))‘((𝑋 ∩ 𝑌) ∪ (∪ (𝐽 ↾_t 𝑆) ∖ 𝑌))))
155	23, 151, 153, 154	syl3anc 1374	. . . . . . . . . . . . . 14 ⊢ (𝜑 → ((int‘(𝐽 ↾_t 𝑆))‘(𝑋 ∩ 𝑌)) ⊆ ((int‘(𝐽 ↾_t 𝑆))‘((𝑋 ∩ 𝑌) ∪ (∪ (𝐽 ↾_t 𝑆) ∖ 𝑌))))
156	155, 101	sseldd 3922	. . . . . . . . . . . . 13 ⊢ (𝜑 → 𝐶 ∈ ((int‘(𝐽 ↾_t 𝑆))‘((𝑋 ∩ 𝑌) ∪ (∪ (𝐽 ↾_t 𝑆) ∖ 𝑌))))
157	156, 69	elind 4140	. . . . . . . . . . . 12 ⊢ (𝜑 → 𝐶 ∈ (((int‘(𝐽 ↾_t 𝑆))‘((𝑋 ∩ 𝑌) ∪ (∪ (𝐽 ↾_t 𝑆) ∖ 𝑌))) ∩ 𝑌))
158	57	a1i 11	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (𝑋 ∩ 𝑌) ⊆ 𝑌)
159		eqid 2736	. . . . . . . . . . . . . . 15 ⊢ ((𝐽 ↾_t 𝑆) ↾_t 𝑌) = ((𝐽 ↾_t 𝑆) ↾_t 𝑌)
160	28, 159	restntr 23147	. . . . . . . . . . . . . 14 ⊢ (((𝐽 ↾_t 𝑆) ∈ Top ∧ 𝑌 ⊆ ∪ (𝐽 ↾_t 𝑆) ∧ (𝑋 ∩ 𝑌) ⊆ 𝑌) → ((int‘((𝐽 ↾_t 𝑆) ↾_t 𝑌))‘(𝑋 ∩ 𝑌)) = (((int‘(𝐽 ↾_t 𝑆))‘((𝑋 ∩ 𝑌) ∪ (∪ (𝐽 ↾_t 𝑆) ∖ 𝑌))) ∩ 𝑌))
161	23, 27, 158, 160	syl3anc 1374	. . . . . . . . . . . . 13 ⊢ (𝜑 → ((int‘((𝐽 ↾_t 𝑆) ↾_t 𝑌))‘(𝑋 ∩ 𝑌)) = (((int‘(𝐽 ↾_t 𝑆))‘((𝑋 ∩ 𝑌) ∪ (∪ (𝐽 ↾_t 𝑆) ∖ 𝑌))) ∩ 𝑌))
162		restabs 23130	. . . . . . . . . . . . . . . 16 ⊢ ((𝐽 ∈ Top ∧ 𝑌 ⊆ 𝑆 ∧ 𝑆 ∈ V) → ((𝐽 ↾_t 𝑆) ↾_t 𝑌) = (𝐽 ↾_t 𝑌))
163	109, 14, 112, 162	syl3anc 1374	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → ((𝐽 ↾_t 𝑆) ↾_t 𝑌) = (𝐽 ↾_t 𝑌))
164	163	fveq2d 6844	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (int‘((𝐽 ↾_t 𝑆) ↾_t 𝑌)) = (int‘(𝐽 ↾_t 𝑌)))
165	164	fveq1d 6842	. . . . . . . . . . . . 13 ⊢ (𝜑 → ((int‘((𝐽 ↾_t 𝑆) ↾_t 𝑌))‘(𝑋 ∩ 𝑌)) = ((int‘(𝐽 ↾_t 𝑌))‘(𝑋 ∩ 𝑌)))
166	161, 165	eqtr3d 2773	. . . . . . . . . . . 12 ⊢ (𝜑 → (((int‘(𝐽 ↾_t 𝑆))‘((𝑋 ∩ 𝑌) ∪ (∪ (𝐽 ↾_t 𝑆) ∖ 𝑌))) ∩ 𝑌) = ((int‘(𝐽 ↾_t 𝑌))‘(𝑋 ∩ 𝑌)))
167	157, 166	eleqtrd 2838	. . . . . . . . . . 11 ⊢ (𝜑 → 𝐶 ∈ ((int‘(𝐽 ↾_t 𝑌))‘(𝑋 ∩ 𝑌)))
168	69	snssd 4730	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → {𝐶} ⊆ 𝑌)
169		ssequn2 4129	. . . . . . . . . . . . . . 15 ⊢ ({𝐶} ⊆ 𝑌 ↔ (𝑌 ∪ {𝐶}) = 𝑌)
170	168, 169	sylib 218	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (𝑌 ∪ {𝐶}) = 𝑌)
171	170	oveq2d 7383	. . . . . . . . . . . . 13 ⊢ (𝜑 → (𝐽 ↾_t (𝑌 ∪ {𝐶})) = (𝐽 ↾_t 𝑌))
172	171	fveq2d 6844	. . . . . . . . . . . 12 ⊢ (𝜑 → (int‘(𝐽 ↾_t (𝑌 ∪ {𝐶}))) = (int‘(𝐽 ↾_t 𝑌)))
173	172, 131	fveq12d 6847	. . . . . . . . . . 11 ⊢ (𝜑 → ((int‘(𝐽 ↾_t (𝑌 ∪ {𝐶})))‘(((𝑋 ∩ 𝑌) ∖ {𝐶}) ∪ {𝐶})) = ((int‘(𝐽 ↾_t 𝑌))‘(𝑋 ∩ 𝑌)))
174	167, 173	eleqtrrd 2839	. . . . . . . . . 10 ⊢ (𝜑 → 𝐶 ∈ ((int‘(𝐽 ↾_t (𝑌 ∪ {𝐶})))‘(((𝑋 ∩ 𝑌) ∖ {𝐶}) ∪ {𝐶})))
175	13, 148, 64, 3, 149, 174	limcres 25853	. . . . . . . . 9 ⊢ (𝜑 → ((𝐺 ↾ ((𝑋 ∩ 𝑌) ∖ {𝐶})) lim_ℂ 𝐶) = (𝐺 lim_ℂ 𝐶))
176	13, 148	feqresmpt 6909	. . . . . . . . . 10 ⊢ (𝜑 → (𝐺 ↾ ((𝑋 ∩ 𝑌) ∖ {𝐶})) = (𝑧 ∈ ((𝑋 ∩ 𝑌) ∖ {𝐶}) ↦ (𝐺‘𝑧)))
177	176	oveq1d 7382	. . . . . . . . 9 ⊢ (𝜑 → ((𝐺 ↾ ((𝑋 ∩ 𝑌) ∖ {𝐶})) lim_ℂ 𝐶) = ((𝑧 ∈ ((𝑋 ∩ 𝑌) ∖ {𝐶}) ↦ (𝐺‘𝑧)) lim_ℂ 𝐶))
178	175, 177	eqtr3d 2773	. . . . . . . 8 ⊢ (𝜑 → (𝐺 lim_ℂ 𝐶) = ((𝑧 ∈ ((𝑋 ∩ 𝑌) ∖ {𝐶}) ↦ (𝐺‘𝑧)) lim_ℂ 𝐶))
179	145, 178	eleqtrd 2838	. . . . . . 7 ⊢ (𝜑 → (𝐺‘𝐶) ∈ ((𝑧 ∈ ((𝑋 ∩ 𝑌) ∖ {𝐶}) ↦ (𝐺‘𝑧)) lim_ℂ 𝐶))
180	3	mpomulcn 24834	. . . . . . . 8 ⊢ (𝑢 ∈ ℂ, 𝑣 ∈ ℂ ↦ (𝑢 · 𝑣)) ∈ ((𝐽 ×_t 𝐽) Cn 𝐽)
181	5, 6, 7	dvcl 25866	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝐶(𝑆 D 𝐹)𝐾) → 𝐾 ∈ ℂ)
182	1, 181	mpdan 688	. . . . . . . . 9 ⊢ (𝜑 → 𝐾 ∈ ℂ)
183	13, 69	ffvelcdmd 7037	. . . . . . . . 9 ⊢ (𝜑 → (𝐺‘𝐶) ∈ ℂ)
184	182, 183	opelxpd 5670	. . . . . . . 8 ⊢ (𝜑 → ⟨𝐾, (𝐺‘𝐶)⟩ ∈ (ℂ × ℂ))
185	75	toponunii 22881	. . . . . . . . 9 ⊢ (ℂ × ℂ) = ∪ (𝐽 ×_t 𝐽)
186	185	cncnpi 23243	. . . . . . . 8 ⊢ (((𝑢 ∈ ℂ, 𝑣 ∈ ℂ ↦ (𝑢 · 𝑣)) ∈ ((𝐽 ×_t 𝐽) Cn 𝐽) ∧ ⟨𝐾, (𝐺‘𝐶)⟩ ∈ (ℂ × ℂ)) → (𝑢 ∈ ℂ, 𝑣 ∈ ℂ ↦ (𝑢 · 𝑣)) ∈ (((𝐽 ×_t 𝐽) CnP 𝐽)‘⟨𝐾, (𝐺‘𝐶)⟩))
187	180, 184, 186	sylancr 588	. . . . . . 7 ⊢ (𝜑 → (𝑢 ∈ ℂ, 𝑣 ∈ ℂ ↦ (𝑢 · 𝑣)) ∈ (((𝐽 ×_t 𝐽) CnP 𝐽)‘⟨𝐾, (𝐺‘𝐶)⟩))
188	55, 59, 73, 73, 3, 76, 138, 179, 187	limccnp2 25859	. . . . . 6 ⊢ (𝜑 → (𝐾(𝑢 ∈ ℂ, 𝑣 ∈ ℂ ↦ (𝑢 · 𝑣))(𝐺‘𝐶)) ∈ ((𝑧 ∈ ((𝑋 ∩ 𝑌) ∖ {𝐶}) ↦ ((((𝐹‘𝑧) − (𝐹‘𝐶)) / (𝑧 − 𝐶))(𝑢 ∈ ℂ, 𝑣 ∈ ℂ ↦ (𝑢 · 𝑣))(𝐺‘𝑧))) lim_ℂ 𝐶))
189		df-mpt 5167	. . . . . . 7 ⊢ (𝑧 ∈ ((𝑋 ∩ 𝑌) ∖ {𝐶}) ↦ ((((𝐹‘𝑧) − (𝐹‘𝐶)) / (𝑧 − 𝐶))(𝑢 ∈ ℂ, 𝑣 ∈ ℂ ↦ (𝑢 · 𝑣))(𝐺‘𝑧))) = {⟨𝑧, 𝑤⟩ ∣ (𝑧 ∈ ((𝑋 ∩ 𝑌) ∖ {𝐶}) ∧ 𝑤 = ((((𝐹‘𝑧) − (𝐹‘𝐶)) / (𝑧 − 𝐶))(𝑢 ∈ ℂ, 𝑣 ∈ ℂ ↦ (𝑢 · 𝑣))(𝐺‘𝑧)))}
190	189	oveq1i 7377	. . . . . 6 ⊢ ((𝑧 ∈ ((𝑋 ∩ 𝑌) ∖ {𝐶}) ↦ ((((𝐹‘𝑧) − (𝐹‘𝐶)) / (𝑧 − 𝐶))(𝑢 ∈ ℂ, 𝑣 ∈ ℂ ↦ (𝑢 · 𝑣))(𝐺‘𝑧))) lim_ℂ 𝐶) = ({⟨𝑧, 𝑤⟩ ∣ (𝑧 ∈ ((𝑋 ∩ 𝑌) ∖ {𝐶}) ∧ 𝑤 = ((((𝐹‘𝑧) − (𝐹‘𝐶)) / (𝑧 − 𝐶))(𝑢 ∈ ℂ, 𝑣 ∈ ℂ ↦ (𝑢 · 𝑣))(𝐺‘𝑧)))} lim_ℂ 𝐶)
191	188, 190	eleqtrdi 2846	. . . . 5 ⊢ (𝜑 → (𝐾(𝑢 ∈ ℂ, 𝑣 ∈ ℂ ↦ (𝑢 · 𝑣))(𝐺‘𝐶)) ∈ ({⟨𝑧, 𝑤⟩ ∣ (𝑧 ∈ ((𝑋 ∩ 𝑌) ∖ {𝐶}) ∧ 𝑤 = ((((𝐹‘𝑧) − (𝐹‘𝐶)) / (𝑧 − 𝐶))(𝑢 ∈ ℂ, 𝑣 ∈ ℂ ↦ (𝑢 · 𝑣))(𝐺‘𝑧)))} lim_ℂ 𝐶))
192		ovmpot 7528	. . . . . 6 ⊢ ((𝐾 ∈ ℂ ∧ (𝐺‘𝐶) ∈ ℂ) → (𝐾(𝑢 ∈ ℂ, 𝑣 ∈ ℂ ↦ (𝑢 · 𝑣))(𝐺‘𝐶)) = (𝐾 · (𝐺‘𝐶)))
193	182, 183, 192	syl2anc 585	. . . . 5 ⊢ (𝜑 → (𝐾(𝑢 ∈ ℂ, 𝑣 ∈ ℂ ↦ (𝑢 · 𝑣))(𝐺‘𝐶)) = (𝐾 · (𝐺‘𝐶)))
194		ovmpot 7528	. . . . . . . . . . 11 ⊢ (((((𝐹‘𝑧) − (𝐹‘𝐶)) / (𝑧 − 𝐶)) ∈ ℂ ∧ (𝐺‘𝑧) ∈ ℂ) → ((((𝐹‘𝑧) − (𝐹‘𝐶)) / (𝑧 − 𝐶))(𝑢 ∈ ℂ, 𝑣 ∈ ℂ ↦ (𝑢 · 𝑣))(𝐺‘𝑧)) = ((((𝐹‘𝑧) − (𝐹‘𝐶)) / (𝑧 − 𝐶)) · (𝐺‘𝑧)))
195	55, 59, 194	syl2anc 585	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑧 ∈ ((𝑋 ∩ 𝑌) ∖ {𝐶})) → ((((𝐹‘𝑧) − (𝐹‘𝐶)) / (𝑧 − 𝐶))(𝑢 ∈ ℂ, 𝑣 ∈ ℂ ↦ (𝑢 · 𝑣))(𝐺‘𝑧)) = ((((𝐹‘𝑧) − (𝐹‘𝐶)) / (𝑧 − 𝐶)) · (𝐺‘𝑧)))
196	195	eqeq2d 2747	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑧 ∈ ((𝑋 ∩ 𝑌) ∖ {𝐶})) → (𝑤 = ((((𝐹‘𝑧) − (𝐹‘𝐶)) / (𝑧 − 𝐶))(𝑢 ∈ ℂ, 𝑣 ∈ ℂ ↦ (𝑢 · 𝑣))(𝐺‘𝑧)) ↔ 𝑤 = ((((𝐹‘𝑧) − (𝐹‘𝐶)) / (𝑧 − 𝐶)) · (𝐺‘𝑧))))
197	196	pm5.32da 579	. . . . . . . 8 ⊢ (𝜑 → ((𝑧 ∈ ((𝑋 ∩ 𝑌) ∖ {𝐶}) ∧ 𝑤 = ((((𝐹‘𝑧) − (𝐹‘𝐶)) / (𝑧 − 𝐶))(𝑢 ∈ ℂ, 𝑣 ∈ ℂ ↦ (𝑢 · 𝑣))(𝐺‘𝑧))) ↔ (𝑧 ∈ ((𝑋 ∩ 𝑌) ∖ {𝐶}) ∧ 𝑤 = ((((𝐹‘𝑧) − (𝐹‘𝐶)) / (𝑧 − 𝐶)) · (𝐺‘𝑧)))))
198	197	opabbidv 5151	. . . . . . 7 ⊢ (𝜑 → {⟨𝑧, 𝑤⟩ ∣ (𝑧 ∈ ((𝑋 ∩ 𝑌) ∖ {𝐶}) ∧ 𝑤 = ((((𝐹‘𝑧) − (𝐹‘𝐶)) / (𝑧 − 𝐶))(𝑢 ∈ ℂ, 𝑣 ∈ ℂ ↦ (𝑢 · 𝑣))(𝐺‘𝑧)))} = {⟨𝑧, 𝑤⟩ ∣ (𝑧 ∈ ((𝑋 ∩ 𝑌) ∖ {𝐶}) ∧ 𝑤 = ((((𝐹‘𝑧) − (𝐹‘𝐶)) / (𝑧 − 𝐶)) · (𝐺‘𝑧)))})
199		df-mpt 5167	. . . . . . 7 ⊢ (𝑧 ∈ ((𝑋 ∩ 𝑌) ∖ {𝐶}) ↦ ((((𝐹‘𝑧) − (𝐹‘𝐶)) / (𝑧 − 𝐶)) · (𝐺‘𝑧))) = {⟨𝑧, 𝑤⟩ ∣ (𝑧 ∈ ((𝑋 ∩ 𝑌) ∖ {𝐶}) ∧ 𝑤 = ((((𝐹‘𝑧) − (𝐹‘𝐶)) / (𝑧 − 𝐶)) · (𝐺‘𝑧)))}
200	198, 199	eqtr4di 2789	. . . . . 6 ⊢ (𝜑 → {⟨𝑧, 𝑤⟩ ∣ (𝑧 ∈ ((𝑋 ∩ 𝑌) ∖ {𝐶}) ∧ 𝑤 = ((((𝐹‘𝑧) − (𝐹‘𝐶)) / (𝑧 − 𝐶))(𝑢 ∈ ℂ, 𝑣 ∈ ℂ ↦ (𝑢 · 𝑣))(𝐺‘𝑧)))} = (𝑧 ∈ ((𝑋 ∩ 𝑌) ∖ {𝐶}) ↦ ((((𝐹‘𝑧) − (𝐹‘𝐶)) / (𝑧 − 𝐶)) · (𝐺‘𝑧))))
201	200	oveq1d 7382	. . . . 5 ⊢ (𝜑 → ({⟨𝑧, 𝑤⟩ ∣ (𝑧 ∈ ((𝑋 ∩ 𝑌) ∖ {𝐶}) ∧ 𝑤 = ((((𝐹‘𝑧) − (𝐹‘𝐶)) / (𝑧 − 𝐶))(𝑢 ∈ ℂ, 𝑣 ∈ ℂ ↦ (𝑢 · 𝑣))(𝐺‘𝑧)))} lim_ℂ 𝐶) = ((𝑧 ∈ ((𝑋 ∩ 𝑌) ∖ {𝐶}) ↦ ((((𝐹‘𝑧) − (𝐹‘𝐶)) / (𝑧 − 𝐶)) · (𝐺‘𝑧))) lim_ℂ 𝐶))
202	191, 193, 201	3eltr3d 2850	. . . 4 ⊢ (𝜑 → (𝐾 · (𝐺‘𝐶)) ∈ ((𝑧 ∈ ((𝑋 ∩ 𝑌) ∖ {𝐶}) ↦ ((((𝐹‘𝑧) − (𝐹‘𝐶)) / (𝑧 − 𝐶)) · (𝐺‘𝑧))) lim_ℂ 𝐶))
203	16	simprd 495	. . . . . . . 8 ⊢ (𝜑 → 𝐿 ∈ ((𝑧 ∈ (𝑌 ∖ {𝐶}) ↦ (((𝐺‘𝑧) − (𝐺‘𝐶)) / (𝑧 − 𝐶))) lim_ℂ 𝐶))
204	70	fmpttd 7067	. . . . . . . . . 10 ⊢ (𝜑 → (𝑧 ∈ (𝑌 ∖ {𝐶}) ↦ (((𝐺‘𝑧) − (𝐺‘𝐶)) / (𝑧 − 𝐶))):(𝑌 ∖ {𝐶})⟶ℂ)
205	64	ssdifssd 4087	. . . . . . . . . 10 ⊢ (𝜑 → (𝑌 ∖ {𝐶}) ⊆ ℂ)
206		eqid 2736	. . . . . . . . . 10 ⊢ (𝐽 ↾_t ((𝑌 ∖ {𝐶}) ∪ {𝐶})) = (𝐽 ↾_t ((𝑌 ∖ {𝐶}) ∪ {𝐶}))
207		undif1 4416	. . . . . . . . . . . . . . 15 ⊢ ((𝑌 ∖ {𝐶}) ∪ {𝐶}) = (𝑌 ∪ {𝐶})
208	207, 170	eqtrid 2783	. . . . . . . . . . . . . 14 ⊢ (𝜑 → ((𝑌 ∖ {𝐶}) ∪ {𝐶}) = 𝑌)
209	208	oveq2d 7383	. . . . . . . . . . . . 13 ⊢ (𝜑 → (𝐽 ↾_t ((𝑌 ∖ {𝐶}) ∪ {𝐶})) = (𝐽 ↾_t 𝑌))
210	209	fveq2d 6844	. . . . . . . . . . . 12 ⊢ (𝜑 → (int‘(𝐽 ↾_t ((𝑌 ∖ {𝐶}) ∪ {𝐶}))) = (int‘(𝐽 ↾_t 𝑌)))
211	210, 131	fveq12d 6847	. . . . . . . . . . 11 ⊢ (𝜑 → ((int‘(𝐽 ↾_t ((𝑌 ∖ {𝐶}) ∪ {𝐶})))‘(((𝑋 ∩ 𝑌) ∖ {𝐶}) ∪ {𝐶})) = ((int‘(𝐽 ↾_t 𝑌))‘(𝑋 ∩ 𝑌)))
212	167, 211	eleqtrrd 2839	. . . . . . . . . 10 ⊢ (𝜑 → 𝐶 ∈ ((int‘(𝐽 ↾_t ((𝑌 ∖ {𝐶}) ∪ {𝐶})))‘(((𝑋 ∩ 𝑌) ∖ {𝐶}) ∪ {𝐶})))
213	204, 62, 205, 3, 206, 212	limcres 25853	. . . . . . . . 9 ⊢ (𝜑 → (((𝑧 ∈ (𝑌 ∖ {𝐶}) ↦ (((𝐺‘𝑧) − (𝐺‘𝐶)) / (𝑧 − 𝐶))) ↾ ((𝑋 ∩ 𝑌) ∖ {𝐶})) lim_ℂ 𝐶) = ((𝑧 ∈ (𝑌 ∖ {𝐶}) ↦ (((𝐺‘𝑧) − (𝐺‘𝐶)) / (𝑧 − 𝐶))) lim_ℂ 𝐶))
214	62	resmptd 6005	. . . . . . . . . 10 ⊢ (𝜑 → ((𝑧 ∈ (𝑌 ∖ {𝐶}) ↦ (((𝐺‘𝑧) − (𝐺‘𝐶)) / (𝑧 − 𝐶))) ↾ ((𝑋 ∩ 𝑌) ∖ {𝐶})) = (𝑧 ∈ ((𝑋 ∩ 𝑌) ∖ {𝐶}) ↦ (((𝐺‘𝑧) − (𝐺‘𝐶)) / (𝑧 − 𝐶))))
215	214	oveq1d 7382	. . . . . . . . 9 ⊢ (𝜑 → (((𝑧 ∈ (𝑌 ∖ {𝐶}) ↦ (((𝐺‘𝑧) − (𝐺‘𝐶)) / (𝑧 − 𝐶))) ↾ ((𝑋 ∩ 𝑌) ∖ {𝐶})) lim_ℂ 𝐶) = ((𝑧 ∈ ((𝑋 ∩ 𝑌) ∖ {𝐶}) ↦ (((𝐺‘𝑧) − (𝐺‘𝐶)) / (𝑧 − 𝐶))) lim_ℂ 𝐶))
216	213, 215	eqtr3d 2773	. . . . . . . 8 ⊢ (𝜑 → ((𝑧 ∈ (𝑌 ∖ {𝐶}) ↦ (((𝐺‘𝑧) − (𝐺‘𝐶)) / (𝑧 − 𝐶))) lim_ℂ 𝐶) = ((𝑧 ∈ ((𝑋 ∩ 𝑌) ∖ {𝐶}) ↦ (((𝐺‘𝑧) − (𝐺‘𝐶)) / (𝑧 − 𝐶))) lim_ℂ 𝐶))
217	203, 216	eleqtrd 2838	. . . . . . 7 ⊢ (𝜑 → 𝐿 ∈ ((𝑧 ∈ ((𝑋 ∩ 𝑌) ∖ {𝐶}) ↦ (((𝐺‘𝑧) − (𝐺‘𝐶)) / (𝑧 − 𝐶))) lim_ℂ 𝐶))
218	84, 5	sstrd 3932	. . . . . . . . . 10 ⊢ (𝜑 → (𝑋 ∩ 𝑌) ⊆ ℂ)
219		cncfmptc 24879	. . . . . . . . . 10 ⊢ (((𝐹‘𝐶) ∈ ℂ ∧ (𝑋 ∩ 𝑌) ⊆ ℂ ∧ ℂ ⊆ ℂ) → (𝑧 ∈ (𝑋 ∩ 𝑌) ↦ (𝐹‘𝐶)) ∈ ((𝑋 ∩ 𝑌)–cn→ℂ))
220	43, 218, 73, 219	syl3anc 1374	. . . . . . . . 9 ⊢ (𝜑 → (𝑧 ∈ (𝑋 ∩ 𝑌) ↦ (𝐹‘𝐶)) ∈ ((𝑋 ∩ 𝑌)–cn→ℂ))
221		eqidd 2737	. . . . . . . . 9 ⊢ (𝑧 = 𝐶 → (𝐹‘𝐶) = (𝐹‘𝐶))
222	220, 127, 221	cnmptlimc 25857	. . . . . . . 8 ⊢ (𝜑 → (𝐹‘𝐶) ∈ ((𝑧 ∈ (𝑋 ∩ 𝑌) ↦ (𝐹‘𝐶)) lim_ℂ 𝐶))
223	43	adantr 480	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑧 ∈ (𝑋 ∩ 𝑌)) → (𝐹‘𝐶) ∈ ℂ)
224	223	fmpttd 7067	. . . . . . . . . 10 ⊢ (𝜑 → (𝑧 ∈ (𝑋 ∩ 𝑌) ↦ (𝐹‘𝐶)):(𝑋 ∩ 𝑌)⟶ℂ)
225	224	limcdif 25843	. . . . . . . . 9 ⊢ (𝜑 → ((𝑧 ∈ (𝑋 ∩ 𝑌) ↦ (𝐹‘𝐶)) lim_ℂ 𝐶) = (((𝑧 ∈ (𝑋 ∩ 𝑌) ↦ (𝐹‘𝐶)) ↾ ((𝑋 ∩ 𝑌) ∖ {𝐶})) lim_ℂ 𝐶))
226		resmpt 6002	. . . . . . . . . . 11 ⊢ (((𝑋 ∩ 𝑌) ∖ {𝐶}) ⊆ (𝑋 ∩ 𝑌) → ((𝑧 ∈ (𝑋 ∩ 𝑌) ↦ (𝐹‘𝐶)) ↾ ((𝑋 ∩ 𝑌) ∖ {𝐶})) = (𝑧 ∈ ((𝑋 ∩ 𝑌) ∖ {𝐶}) ↦ (𝐹‘𝐶)))
227	146, 226	mp1i 13	. . . . . . . . . 10 ⊢ (𝜑 → ((𝑧 ∈ (𝑋 ∩ 𝑌) ↦ (𝐹‘𝐶)) ↾ ((𝑋 ∩ 𝑌) ∖ {𝐶})) = (𝑧 ∈ ((𝑋 ∩ 𝑌) ∖ {𝐶}) ↦ (𝐹‘𝐶)))
228	227	oveq1d 7382	. . . . . . . . 9 ⊢ (𝜑 → (((𝑧 ∈ (𝑋 ∩ 𝑌) ↦ (𝐹‘𝐶)) ↾ ((𝑋 ∩ 𝑌) ∖ {𝐶})) lim_ℂ 𝐶) = ((𝑧 ∈ ((𝑋 ∩ 𝑌) ∖ {𝐶}) ↦ (𝐹‘𝐶)) lim_ℂ 𝐶))
229	225, 228	eqtrd 2771	. . . . . . . 8 ⊢ (𝜑 → ((𝑧 ∈ (𝑋 ∩ 𝑌) ↦ (𝐹‘𝐶)) lim_ℂ 𝐶) = ((𝑧 ∈ ((𝑋 ∩ 𝑌) ∖ {𝐶}) ↦ (𝐹‘𝐶)) lim_ℂ 𝐶))
230	222, 229	eleqtrd 2838	. . . . . . 7 ⊢ (𝜑 → (𝐹‘𝐶) ∈ ((𝑧 ∈ ((𝑋 ∩ 𝑌) ∖ {𝐶}) ↦ (𝐹‘𝐶)) lim_ℂ 𝐶))
231	5, 13, 14	dvcl 25866	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝐶(𝑆 D 𝐺)𝐿) → 𝐿 ∈ ℂ)
232	11, 231	mpdan 688	. . . . . . . . 9 ⊢ (𝜑 → 𝐿 ∈ ℂ)
233	232, 43	opelxpd 5670	. . . . . . . 8 ⊢ (𝜑 → ⟨𝐿, (𝐹‘𝐶)⟩ ∈ (ℂ × ℂ))
234	185	cncnpi 23243	. . . . . . . 8 ⊢ (((𝑢 ∈ ℂ, 𝑣 ∈ ℂ ↦ (𝑢 · 𝑣)) ∈ ((𝐽 ×_t 𝐽) Cn 𝐽) ∧ ⟨𝐿, (𝐹‘𝐶)⟩ ∈ (ℂ × ℂ)) → (𝑢 ∈ ℂ, 𝑣 ∈ ℂ ↦ (𝑢 · 𝑣)) ∈ (((𝐽 ×_t 𝐽) CnP 𝐽)‘⟨𝐿, (𝐹‘𝐶)⟩))
235	180, 233, 234	sylancr 588	. . . . . . 7 ⊢ (𝜑 → (𝑢 ∈ ℂ, 𝑣 ∈ ℂ ↦ (𝑢 · 𝑣)) ∈ (((𝐽 ×_t 𝐽) CnP 𝐽)‘⟨𝐿, (𝐹‘𝐶)⟩))
236	71, 44, 73, 73, 3, 76, 217, 230, 235	limccnp2 25859	. . . . . 6 ⊢ (𝜑 → (𝐿(𝑢 ∈ ℂ, 𝑣 ∈ ℂ ↦ (𝑢 · 𝑣))(𝐹‘𝐶)) ∈ ((𝑧 ∈ ((𝑋 ∩ 𝑌) ∖ {𝐶}) ↦ ((((𝐺‘𝑧) − (𝐺‘𝐶)) / (𝑧 − 𝐶))(𝑢 ∈ ℂ, 𝑣 ∈ ℂ ↦ (𝑢 · 𝑣))(𝐹‘𝐶))) lim_ℂ 𝐶))
237		df-mpt 5167	. . . . . . 7 ⊢ (𝑧 ∈ ((𝑋 ∩ 𝑌) ∖ {𝐶}) ↦ ((((𝐺‘𝑧) − (𝐺‘𝐶)) / (𝑧 − 𝐶))(𝑢 ∈ ℂ, 𝑣 ∈ ℂ ↦ (𝑢 · 𝑣))(𝐹‘𝐶))) = {⟨𝑧, 𝑤⟩ ∣ (𝑧 ∈ ((𝑋 ∩ 𝑌) ∖ {𝐶}) ∧ 𝑤 = ((((𝐺‘𝑧) − (𝐺‘𝐶)) / (𝑧 − 𝐶))(𝑢 ∈ ℂ, 𝑣 ∈ ℂ ↦ (𝑢 · 𝑣))(𝐹‘𝐶)))}
238	237	oveq1i 7377	. . . . . 6 ⊢ ((𝑧 ∈ ((𝑋 ∩ 𝑌) ∖ {𝐶}) ↦ ((((𝐺‘𝑧) − (𝐺‘𝐶)) / (𝑧 − 𝐶))(𝑢 ∈ ℂ, 𝑣 ∈ ℂ ↦ (𝑢 · 𝑣))(𝐹‘𝐶))) lim_ℂ 𝐶) = ({⟨𝑧, 𝑤⟩ ∣ (𝑧 ∈ ((𝑋 ∩ 𝑌) ∖ {𝐶}) ∧ 𝑤 = ((((𝐺‘𝑧) − (𝐺‘𝐶)) / (𝑧 − 𝐶))(𝑢 ∈ ℂ, 𝑣 ∈ ℂ ↦ (𝑢 · 𝑣))(𝐹‘𝐶)))} lim_ℂ 𝐶)
239	236, 238	eleqtrdi 2846	. . . . 5 ⊢ (𝜑 → (𝐿(𝑢 ∈ ℂ, 𝑣 ∈ ℂ ↦ (𝑢 · 𝑣))(𝐹‘𝐶)) ∈ ({⟨𝑧, 𝑤⟩ ∣ (𝑧 ∈ ((𝑋 ∩ 𝑌) ∖ {𝐶}) ∧ 𝑤 = ((((𝐺‘𝑧) − (𝐺‘𝐶)) / (𝑧 − 𝐶))(𝑢 ∈ ℂ, 𝑣 ∈ ℂ ↦ (𝑢 · 𝑣))(𝐹‘𝐶)))} lim_ℂ 𝐶))
240		ovmpot 7528	. . . . . 6 ⊢ ((𝐿 ∈ ℂ ∧ (𝐹‘𝐶) ∈ ℂ) → (𝐿(𝑢 ∈ ℂ, 𝑣 ∈ ℂ ↦ (𝑢 · 𝑣))(𝐹‘𝐶)) = (𝐿 · (𝐹‘𝐶)))
241	232, 43, 240	syl2anc 585	. . . . 5 ⊢ (𝜑 → (𝐿(𝑢 ∈ ℂ, 𝑣 ∈ ℂ ↦ (𝑢 · 𝑣))(𝐹‘𝐶)) = (𝐿 · (𝐹‘𝐶)))
242	42	adantr 480	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑧 ∈ ((𝑋 ∩ 𝑌) ∖ {𝐶})) → 𝐶 ∈ 𝑋)
243	32, 242	ffvelcdmd 7037	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑧 ∈ ((𝑋 ∩ 𝑌) ∖ {𝐶})) → (𝐹‘𝐶) ∈ ℂ)
244		ovmpot 7528	. . . . . . . . . . 11 ⊢ (((((𝐺‘𝑧) − (𝐺‘𝐶)) / (𝑧 − 𝐶)) ∈ ℂ ∧ (𝐹‘𝐶) ∈ ℂ) → ((((𝐺‘𝑧) − (𝐺‘𝐶)) / (𝑧 − 𝐶))(𝑢 ∈ ℂ, 𝑣 ∈ ℂ ↦ (𝑢 · 𝑣))(𝐹‘𝐶)) = ((((𝐺‘𝑧) − (𝐺‘𝐶)) / (𝑧 − 𝐶)) · (𝐹‘𝐶)))
245	71, 243, 244	syl2anc 585	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑧 ∈ ((𝑋 ∩ 𝑌) ∖ {𝐶})) → ((((𝐺‘𝑧) − (𝐺‘𝐶)) / (𝑧 − 𝐶))(𝑢 ∈ ℂ, 𝑣 ∈ ℂ ↦ (𝑢 · 𝑣))(𝐹‘𝐶)) = ((((𝐺‘𝑧) − (𝐺‘𝐶)) / (𝑧 − 𝐶)) · (𝐹‘𝐶)))
246	245	eqeq2d 2747	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑧 ∈ ((𝑋 ∩ 𝑌) ∖ {𝐶})) → (𝑤 = ((((𝐺‘𝑧) − (𝐺‘𝐶)) / (𝑧 − 𝐶))(𝑢 ∈ ℂ, 𝑣 ∈ ℂ ↦ (𝑢 · 𝑣))(𝐹‘𝐶)) ↔ 𝑤 = ((((𝐺‘𝑧) − (𝐺‘𝐶)) / (𝑧 − 𝐶)) · (𝐹‘𝐶))))
247	246	pm5.32da 579	. . . . . . . 8 ⊢ (𝜑 → ((𝑧 ∈ ((𝑋 ∩ 𝑌) ∖ {𝐶}) ∧ 𝑤 = ((((𝐺‘𝑧) − (𝐺‘𝐶)) / (𝑧 − 𝐶))(𝑢 ∈ ℂ, 𝑣 ∈ ℂ ↦ (𝑢 · 𝑣))(𝐹‘𝐶))) ↔ (𝑧 ∈ ((𝑋 ∩ 𝑌) ∖ {𝐶}) ∧ 𝑤 = ((((𝐺‘𝑧) − (𝐺‘𝐶)) / (𝑧 − 𝐶)) · (𝐹‘𝐶)))))
248	247	opabbidv 5151	. . . . . . 7 ⊢ (𝜑 → {⟨𝑧, 𝑤⟩ ∣ (𝑧 ∈ ((𝑋 ∩ 𝑌) ∖ {𝐶}) ∧ 𝑤 = ((((𝐺‘𝑧) − (𝐺‘𝐶)) / (𝑧 − 𝐶))(𝑢 ∈ ℂ, 𝑣 ∈ ℂ ↦ (𝑢 · 𝑣))(𝐹‘𝐶)))} = {⟨𝑧, 𝑤⟩ ∣ (𝑧 ∈ ((𝑋 ∩ 𝑌) ∖ {𝐶}) ∧ 𝑤 = ((((𝐺‘𝑧) − (𝐺‘𝐶)) / (𝑧 − 𝐶)) · (𝐹‘𝐶)))})
249		df-mpt 5167	. . . . . . 7 ⊢ (𝑧 ∈ ((𝑋 ∩ 𝑌) ∖ {𝐶}) ↦ ((((𝐺‘𝑧) − (𝐺‘𝐶)) / (𝑧 − 𝐶)) · (𝐹‘𝐶))) = {⟨𝑧, 𝑤⟩ ∣ (𝑧 ∈ ((𝑋 ∩ 𝑌) ∖ {𝐶}) ∧ 𝑤 = ((((𝐺‘𝑧) − (𝐺‘𝐶)) / (𝑧 − 𝐶)) · (𝐹‘𝐶)))}
250	248, 249	eqtr4di 2789	. . . . . 6 ⊢ (𝜑 → {⟨𝑧, 𝑤⟩ ∣ (𝑧 ∈ ((𝑋 ∩ 𝑌) ∖ {𝐶}) ∧ 𝑤 = ((((𝐺‘𝑧) − (𝐺‘𝐶)) / (𝑧 − 𝐶))(𝑢 ∈ ℂ, 𝑣 ∈ ℂ ↦ (𝑢 · 𝑣))(𝐹‘𝐶)))} = (𝑧 ∈ ((𝑋 ∩ 𝑌) ∖ {𝐶}) ↦ ((((𝐺‘𝑧) − (𝐺‘𝐶)) / (𝑧 − 𝐶)) · (𝐹‘𝐶))))
251	250	oveq1d 7382	. . . . 5 ⊢ (𝜑 → ({⟨𝑧, 𝑤⟩ ∣ (𝑧 ∈ ((𝑋 ∩ 𝑌) ∖ {𝐶}) ∧ 𝑤 = ((((𝐺‘𝑧) − (𝐺‘𝐶)) / (𝑧 − 𝐶))(𝑢 ∈ ℂ, 𝑣 ∈ ℂ ↦ (𝑢 · 𝑣))(𝐹‘𝐶)))} lim_ℂ 𝐶) = ((𝑧 ∈ ((𝑋 ∩ 𝑌) ∖ {𝐶}) ↦ ((((𝐺‘𝑧) − (𝐺‘𝐶)) / (𝑧 − 𝐶)) · (𝐹‘𝐶))) lim_ℂ 𝐶))
252	239, 241, 251	3eltr3d 2850	. . . 4 ⊢ (𝜑 → (𝐿 · (𝐹‘𝐶)) ∈ ((𝑧 ∈ ((𝑋 ∩ 𝑌) ∖ {𝐶}) ↦ ((((𝐺‘𝑧) − (𝐺‘𝐶)) / (𝑧 − 𝐶)) · (𝐹‘𝐶))) lim_ℂ 𝐶))
253	3	addcn 24831	. . . . 5 ⊢ + ∈ ((𝐽 ×_t 𝐽) Cn 𝐽)
254	182, 183	mulcld 11165	. . . . . 6 ⊢ (𝜑 → (𝐾 · (𝐺‘𝐶)) ∈ ℂ)
255	232, 43	mulcld 11165	. . . . . 6 ⊢ (𝜑 → (𝐿 · (𝐹‘𝐶)) ∈ ℂ)
256	254, 255	opelxpd 5670	. . . . 5 ⊢ (𝜑 → ⟨(𝐾 · (𝐺‘𝐶)), (𝐿 · (𝐹‘𝐶))⟩ ∈ (ℂ × ℂ))
257	185	cncnpi 23243	. . . . 5 ⊢ (( + ∈ ((𝐽 ×_t 𝐽) Cn 𝐽) ∧ ⟨(𝐾 · (𝐺‘𝐶)), (𝐿 · (𝐹‘𝐶))⟩ ∈ (ℂ × ℂ)) → + ∈ (((𝐽 ×_t 𝐽) CnP 𝐽)‘⟨(𝐾 · (𝐺‘𝐶)), (𝐿 · (𝐹‘𝐶))⟩))
258	253, 256, 257	sylancr 588	. . . 4 ⊢ (𝜑 → + ∈ (((𝐽 ×_t 𝐽) CnP 𝐽)‘⟨(𝐾 · (𝐺‘𝐶)), (𝐿 · (𝐹‘𝐶))⟩))
259	60, 72, 73, 73, 3, 76, 202, 252, 258	limccnp2 25859	. . 3 ⊢ (𝜑 → ((𝐾 · (𝐺‘𝐶)) + (𝐿 · (𝐹‘𝐶))) ∈ ((𝑧 ∈ ((𝑋 ∩ 𝑌) ∖ {𝐶}) ↦ (((((𝐹‘𝑧) − (𝐹‘𝐶)) / (𝑧 − 𝐶)) · (𝐺‘𝑧)) + ((((𝐺‘𝑧) − (𝐺‘𝐶)) / (𝑧 − 𝐶)) · (𝐹‘𝐶)))) lim_ℂ 𝐶))
260	37, 243	subcld 11505	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑧 ∈ ((𝑋 ∩ 𝑌) ∖ {𝐶})) → ((𝐹‘𝑧) − (𝐹‘𝐶)) ∈ ℂ)
261	260, 59	mulcld 11165	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑧 ∈ ((𝑋 ∩ 𝑌) ∖ {𝐶})) → (((𝐹‘𝑧) − (𝐹‘𝐶)) · (𝐺‘𝑧)) ∈ ℂ)
262	69	adantr 480	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑧 ∈ ((𝑋 ∩ 𝑌) ∖ {𝐶})) → 𝐶 ∈ 𝑌)
263	56, 262	ffvelcdmd 7037	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑧 ∈ ((𝑋 ∩ 𝑌) ∖ {𝐶})) → (𝐺‘𝐶) ∈ ℂ)
264	59, 263	subcld 11505	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑧 ∈ ((𝑋 ∩ 𝑌) ∖ {𝐶})) → ((𝐺‘𝑧) − (𝐺‘𝐶)) ∈ ℂ)
265	264, 243	mulcld 11165	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑧 ∈ ((𝑋 ∩ 𝑌) ∖ {𝐶})) → (((𝐺‘𝑧) − (𝐺‘𝐶)) · (𝐹‘𝐶)) ∈ ℂ)
266	47, 242	sseldd 3922	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑧 ∈ ((𝑋 ∩ 𝑌) ∖ {𝐶})) → 𝐶 ∈ ℂ)
267	48, 266	subcld 11505	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑧 ∈ ((𝑋 ∩ 𝑌) ∖ {𝐶})) → (𝑧 − 𝐶) ∈ ℂ)
268	261, 265, 267, 54	divdird 11969	. . . . . 6 ⊢ ((𝜑 ∧ 𝑧 ∈ ((𝑋 ∩ 𝑌) ∖ {𝐶})) → (((((𝐹‘𝑧) − (𝐹‘𝐶)) · (𝐺‘𝑧)) + (((𝐺‘𝑧) − (𝐺‘𝐶)) · (𝐹‘𝐶))) / (𝑧 − 𝐶)) = (((((𝐹‘𝑧) − (𝐹‘𝐶)) · (𝐺‘𝑧)) / (𝑧 − 𝐶)) + ((((𝐺‘𝑧) − (𝐺‘𝐶)) · (𝐹‘𝐶)) / (𝑧 − 𝐶))))
269	37, 59	mulcld 11165	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑧 ∈ ((𝑋 ∩ 𝑌) ∖ {𝐶})) → ((𝐹‘𝑧) · (𝐺‘𝑧)) ∈ ℂ)
270	243, 59	mulcld 11165	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑧 ∈ ((𝑋 ∩ 𝑌) ∖ {𝐶})) → ((𝐹‘𝐶) · (𝐺‘𝑧)) ∈ ℂ)
271	243, 263	mulcld 11165	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑧 ∈ ((𝑋 ∩ 𝑌) ∖ {𝐶})) → ((𝐹‘𝐶) · (𝐺‘𝐶)) ∈ ℂ)
272	269, 270, 271	npncand 11529	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑧 ∈ ((𝑋 ∩ 𝑌) ∖ {𝐶})) → ((((𝐹‘𝑧) · (𝐺‘𝑧)) − ((𝐹‘𝐶) · (𝐺‘𝑧))) + (((𝐹‘𝐶) · (𝐺‘𝑧)) − ((𝐹‘𝐶) · (𝐺‘𝐶)))) = (((𝐹‘𝑧) · (𝐺‘𝑧)) − ((𝐹‘𝐶) · (𝐺‘𝐶))))
273	37, 243, 59	subdird 11607	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑧 ∈ ((𝑋 ∩ 𝑌) ∖ {𝐶})) → (((𝐹‘𝑧) − (𝐹‘𝐶)) · (𝐺‘𝑧)) = (((𝐹‘𝑧) · (𝐺‘𝑧)) − ((𝐹‘𝐶) · (𝐺‘𝑧))))
274	264, 243	mulcomd 11166	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑧 ∈ ((𝑋 ∩ 𝑌) ∖ {𝐶})) → (((𝐺‘𝑧) − (𝐺‘𝐶)) · (𝐹‘𝐶)) = ((𝐹‘𝐶) · ((𝐺‘𝑧) − (𝐺‘𝐶))))
275	243, 59, 263	subdid 11606	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑧 ∈ ((𝑋 ∩ 𝑌) ∖ {𝐶})) → ((𝐹‘𝐶) · ((𝐺‘𝑧) − (𝐺‘𝐶))) = (((𝐹‘𝐶) · (𝐺‘𝑧)) − ((𝐹‘𝐶) · (𝐺‘𝐶))))
276	274, 275	eqtrd 2771	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑧 ∈ ((𝑋 ∩ 𝑌) ∖ {𝐶})) → (((𝐺‘𝑧) − (𝐺‘𝐶)) · (𝐹‘𝐶)) = (((𝐹‘𝐶) · (𝐺‘𝑧)) − ((𝐹‘𝐶) · (𝐺‘𝐶))))
277	273, 276	oveq12d 7385	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑧 ∈ ((𝑋 ∩ 𝑌) ∖ {𝐶})) → ((((𝐹‘𝑧) − (𝐹‘𝐶)) · (𝐺‘𝑧)) + (((𝐺‘𝑧) − (𝐺‘𝐶)) · (𝐹‘𝐶))) = ((((𝐹‘𝑧) · (𝐺‘𝑧)) − ((𝐹‘𝐶) · (𝐺‘𝑧))) + (((𝐹‘𝐶) · (𝐺‘𝑧)) − ((𝐹‘𝐶) · (𝐺‘𝐶)))))
278	6	ffnd 6669	. . . . . . . . . . . 12 ⊢ (𝜑 → 𝐹 Fn 𝑋)
279	278	adantr 480	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑧 ∈ ((𝑋 ∩ 𝑌) ∖ {𝐶})) → 𝐹 Fn 𝑋)
280	13	ffnd 6669	. . . . . . . . . . . 12 ⊢ (𝜑 → 𝐺 Fn 𝑌)
281	280	adantr 480	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑧 ∈ ((𝑋 ∩ 𝑌) ∖ {𝐶})) → 𝐺 Fn 𝑌)
282		ssexg 5264	. . . . . . . . . . . . 13 ⊢ ((𝑋 ⊆ ℂ ∧ ℂ ∈ V) → 𝑋 ∈ V)
283	46, 110, 282	sylancl 587	. . . . . . . . . . . 12 ⊢ (𝜑 → 𝑋 ∈ V)
284	283	adantr 480	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑧 ∈ ((𝑋 ∩ 𝑌) ∖ {𝐶})) → 𝑋 ∈ V)
285		ssexg 5264	. . . . . . . . . . . . 13 ⊢ ((𝑌 ⊆ ℂ ∧ ℂ ∈ V) → 𝑌 ∈ V)
286	64, 110, 285	sylancl 587	. . . . . . . . . . . 12 ⊢ (𝜑 → 𝑌 ∈ V)
287	286	adantr 480	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑧 ∈ ((𝑋 ∩ 𝑌) ∖ {𝐶})) → 𝑌 ∈ V)
288		eqid 2736	. . . . . . . . . . 11 ⊢ (𝑋 ∩ 𝑌) = (𝑋 ∩ 𝑌)
289		eqidd 2737	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑧 ∈ ((𝑋 ∩ 𝑌) ∖ {𝐶})) ∧ 𝑧 ∈ 𝑋) → (𝐹‘𝑧) = (𝐹‘𝑧))
290		eqidd 2737	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑧 ∈ ((𝑋 ∩ 𝑌) ∖ {𝐶})) ∧ 𝑧 ∈ 𝑌) → (𝐺‘𝑧) = (𝐺‘𝑧))
291	279, 281, 284, 287, 288, 289, 290	ofval 7642	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑧 ∈ ((𝑋 ∩ 𝑌) ∖ {𝐶})) ∧ 𝑧 ∈ (𝑋 ∩ 𝑌)) → ((𝐹 ∘_f · 𝐺)‘𝑧) = ((𝐹‘𝑧) · (𝐺‘𝑧)))
292	35, 291	mpdan 688	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑧 ∈ ((𝑋 ∩ 𝑌) ∖ {𝐶})) → ((𝐹 ∘_f · 𝐺)‘𝑧) = ((𝐹‘𝑧) · (𝐺‘𝑧)))
293		eqidd 2737	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑧 ∈ ((𝑋 ∩ 𝑌) ∖ {𝐶})) ∧ 𝐶 ∈ 𝑋) → (𝐹‘𝐶) = (𝐹‘𝐶))
294		eqidd 2737	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑧 ∈ ((𝑋 ∩ 𝑌) ∖ {𝐶})) ∧ 𝐶 ∈ 𝑌) → (𝐺‘𝐶) = (𝐺‘𝐶))
295	279, 281, 284, 287, 288, 293, 294	ofval 7642	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑧 ∈ ((𝑋 ∩ 𝑌) ∖ {𝐶})) ∧ 𝐶 ∈ (𝑋 ∩ 𝑌)) → ((𝐹 ∘_f · 𝐺)‘𝐶) = ((𝐹‘𝐶) · (𝐺‘𝐶)))
296	127, 295	mpidan 690	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑧 ∈ ((𝑋 ∩ 𝑌) ∖ {𝐶})) → ((𝐹 ∘_f · 𝐺)‘𝐶) = ((𝐹‘𝐶) · (𝐺‘𝐶)))
297	292, 296	oveq12d 7385	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑧 ∈ ((𝑋 ∩ 𝑌) ∖ {𝐶})) → (((𝐹 ∘_f · 𝐺)‘𝑧) − ((𝐹 ∘_f · 𝐺)‘𝐶)) = (((𝐹‘𝑧) · (𝐺‘𝑧)) − ((𝐹‘𝐶) · (𝐺‘𝐶))))
298	272, 277, 297	3eqtr4d 2781	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑧 ∈ ((𝑋 ∩ 𝑌) ∖ {𝐶})) → ((((𝐹‘𝑧) − (𝐹‘𝐶)) · (𝐺‘𝑧)) + (((𝐺‘𝑧) − (𝐺‘𝐶)) · (𝐹‘𝐶))) = (((𝐹 ∘_f · 𝐺)‘𝑧) − ((𝐹 ∘_f · 𝐺)‘𝐶)))
299	298	oveq1d 7382	. . . . . 6 ⊢ ((𝜑 ∧ 𝑧 ∈ ((𝑋 ∩ 𝑌) ∖ {𝐶})) → (((((𝐹‘𝑧) − (𝐹‘𝐶)) · (𝐺‘𝑧)) + (((𝐺‘𝑧) − (𝐺‘𝐶)) · (𝐹‘𝐶))) / (𝑧 − 𝐶)) = ((((𝐹 ∘_f · 𝐺)‘𝑧) − ((𝐹 ∘_f · 𝐺)‘𝐶)) / (𝑧 − 𝐶)))
300	260, 59, 267, 54	div23d 11968	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑧 ∈ ((𝑋 ∩ 𝑌) ∖ {𝐶})) → ((((𝐹‘𝑧) − (𝐹‘𝐶)) · (𝐺‘𝑧)) / (𝑧 − 𝐶)) = ((((𝐹‘𝑧) − (𝐹‘𝐶)) / (𝑧 − 𝐶)) · (𝐺‘𝑧)))
301	264, 243, 267, 54	div23d 11968	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑧 ∈ ((𝑋 ∩ 𝑌) ∖ {𝐶})) → ((((𝐺‘𝑧) − (𝐺‘𝐶)) · (𝐹‘𝐶)) / (𝑧 − 𝐶)) = ((((𝐺‘𝑧) − (𝐺‘𝐶)) / (𝑧 − 𝐶)) · (𝐹‘𝐶)))
302	300, 301	oveq12d 7385	. . . . . 6 ⊢ ((𝜑 ∧ 𝑧 ∈ ((𝑋 ∩ 𝑌) ∖ {𝐶})) → (((((𝐹‘𝑧) − (𝐹‘𝐶)) · (𝐺‘𝑧)) / (𝑧 − 𝐶)) + ((((𝐺‘𝑧) − (𝐺‘𝐶)) · (𝐹‘𝐶)) / (𝑧 − 𝐶))) = (((((𝐹‘𝑧) − (𝐹‘𝐶)) / (𝑧 − 𝐶)) · (𝐺‘𝑧)) + ((((𝐺‘𝑧) − (𝐺‘𝐶)) / (𝑧 − 𝐶)) · (𝐹‘𝐶))))
303	268, 299, 302	3eqtr3d 2779	. . . . 5 ⊢ ((𝜑 ∧ 𝑧 ∈ ((𝑋 ∩ 𝑌) ∖ {𝐶})) → ((((𝐹 ∘_f · 𝐺)‘𝑧) − ((𝐹 ∘_f · 𝐺)‘𝐶)) / (𝑧 − 𝐶)) = (((((𝐹‘𝑧) − (𝐹‘𝐶)) / (𝑧 − 𝐶)) · (𝐺‘𝑧)) + ((((𝐺‘𝑧) − (𝐺‘𝐶)) / (𝑧 − 𝐶)) · (𝐹‘𝐶))))
304	303	mpteq2dva 5178	. . . 4 ⊢ (𝜑 → (𝑧 ∈ ((𝑋 ∩ 𝑌) ∖ {𝐶}) ↦ ((((𝐹 ∘_f · 𝐺)‘𝑧) − ((𝐹 ∘_f · 𝐺)‘𝐶)) / (𝑧 − 𝐶))) = (𝑧 ∈ ((𝑋 ∩ 𝑌) ∖ {𝐶}) ↦ (((((𝐹‘𝑧) − (𝐹‘𝐶)) / (𝑧 − 𝐶)) · (𝐺‘𝑧)) + ((((𝐺‘𝑧) − (𝐺‘𝐶)) / (𝑧 − 𝐶)) · (𝐹‘𝐶)))))
305	304	oveq1d 7382	. . 3 ⊢ (𝜑 → ((𝑧 ∈ ((𝑋 ∩ 𝑌) ∖ {𝐶}) ↦ ((((𝐹 ∘_f · 𝐺)‘𝑧) − ((𝐹 ∘_f · 𝐺)‘𝐶)) / (𝑧 − 𝐶))) lim_ℂ 𝐶) = ((𝑧 ∈ ((𝑋 ∩ 𝑌) ∖ {𝐶}) ↦ (((((𝐹‘𝑧) − (𝐹‘𝐶)) / (𝑧 − 𝐶)) · (𝐺‘𝑧)) + ((((𝐺‘𝑧) − (𝐺‘𝐶)) / (𝑧 − 𝐶)) · (𝐹‘𝐶)))) lim_ℂ 𝐶))
306	259, 305	eleqtrrd 2839	. 2 ⊢ (𝜑 → ((𝐾 · (𝐺‘𝐶)) + (𝐿 · (𝐹‘𝐶))) ∈ ((𝑧 ∈ ((𝑋 ∩ 𝑌) ∖ {𝐶}) ↦ ((((𝐹 ∘_f · 𝐺)‘𝑧) − ((𝐹 ∘_f · 𝐺)‘𝐶)) / (𝑧 − 𝐶))) lim_ℂ 𝐶))
307		eqid 2736	. . 3 ⊢ (𝑧 ∈ ((𝑋 ∩ 𝑌) ∖ {𝐶}) ↦ ((((𝐹 ∘_f · 𝐺)‘𝑧) − ((𝐹 ∘_f · 𝐺)‘𝐶)) / (𝑧 − 𝐶))) = (𝑧 ∈ ((𝑋 ∩ 𝑌) ∖ {𝐶}) ↦ ((((𝐹 ∘_f · 𝐺)‘𝑧) − ((𝐹 ∘_f · 𝐺)‘𝐶)) / (𝑧 − 𝐶)))
308		mulcl 11122	. . . . 5 ⊢ ((𝑥 ∈ ℂ ∧ 𝑦 ∈ ℂ) → (𝑥 · 𝑦) ∈ ℂ)
309	308	adantl 481	. . . 4 ⊢ ((𝜑 ∧ (𝑥 ∈ ℂ ∧ 𝑦 ∈ ℂ)) → (𝑥 · 𝑦) ∈ ℂ)
310	309, 6, 13, 283, 286, 288	off 7649	. . 3 ⊢ (𝜑 → (𝐹 ∘_f · 𝐺):(𝑋 ∩ 𝑌)⟶ℂ)
311	2, 3, 307, 5, 310, 84	eldv 25865	. 2 ⊢ (𝜑 → (𝐶(𝑆 D (𝐹 ∘_f · 𝐺))((𝐾 · (𝐺‘𝐶)) + (𝐿 · (𝐹‘𝐶))) ↔ (𝐶 ∈ ((int‘(𝐽 ↾_t 𝑆))‘(𝑋 ∩ 𝑌)) ∧ ((𝐾 · (𝐺‘𝐶)) + (𝐿 · (𝐹‘𝐶))) ∈ ((𝑧 ∈ ((𝑋 ∩ 𝑌) ∖ {𝐶}) ↦ ((((𝐹 ∘_f · 𝐺)‘𝑧) − ((𝐹 ∘_f · 𝐺)‘𝐶)) / (𝑧 − 𝐶))) lim_ℂ 𝐶))))
312	31, 306, 311	mpbir2and 714	1 ⊢ (𝜑 → 𝐶(𝑆 D (𝐹 ∘_f · 𝐺))((𝐾 · (𝐺‘𝐶)) + (𝐿 · (𝐹‘𝐶))))

Colors of variables: wff setvar class

Syntax hints: → wi 4 ↔ wb 206 ∧ wa 395 = wceq 1542 ∈ wcel 2114 ≠ wne 2932 Vcvv 3429 ∖ cdif 3886 ∪ cun 3887 ∩ cin 3888 ⊆ wss 3889 {csn 4567 ⟨cop 4573 ∪ cuni 4850 class class class wbr 5085 {copab 5147 ↦ cmpt 5166 × cxp 5629 dom cdm 5631 ↾ cres 5633 Rel wrel 5636 Fn wfn 6493 ⟶wf 6494 ‘cfv 6498 (class class class)co 7367 ∈ cmpo 7369 ∘_f cof 7629 ℂcc 11036 + caddc 11041 · cmul 11043 − cmin 11377 / cdiv 11807 ↾_t crest 17383 TopOpenctopn 17384 ℂ_fldccnfld 21352 Topctop 22858 TopOnctopon 22875 intcnt 22982 Cn ccn 23189 CnP ccnp 23190 ×_t ctx 23525 –cn→ccncf 24843 lim_ℂ climc 25829 D cdv 25830

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1797 ax-4 1811 ax-5 1912 ax-6 1969 ax-7 2010 ax-8 2116 ax-9 2124 ax-10 2147 ax-11 2163 ax-12 2185 ax-ext 2708 ax-rep 5212 ax-sep 5231 ax-nul 5241 ax-pow 5307 ax-pr 5375 ax-un 7689 ax-cnex 11094 ax-resscn 11095 ax-1cn 11096 ax-icn 11097 ax-addcl 11098 ax-addrcl 11099 ax-mulcl 11100 ax-mulrcl 11101 ax-mulcom 11102 ax-addass 11103 ax-mulass 11104 ax-distr 11105 ax-i2m1 11106 ax-1ne0 11107 ax-1rid 11108 ax-rnegex 11109 ax-rrecex 11110 ax-cnre 11111 ax-pre-lttri 11112 ax-pre-lttrn 11113 ax-pre-ltadd 11114 ax-pre-mulgt0 11115 ax-pre-sup 11116 ax-addf 11117

This theorem depends on definitions: df-bi 207 df-an 396 df-or 849 df-3or 1088 df-3an 1089 df-tru 1545 df-fal 1555 df-ex 1782 df-nf 1786 df-sb 2069 df-mo 2539 df-eu 2569 df-clab 2715 df-cleq 2728 df-clel 2811 df-nfc 2885 df-ne 2933 df-nel 3037 df-ral 3052 df-rex 3062 df-rmo 3342 df-reu 3343 df-rab 3390 df-v 3431 df-sbc 3729 df-csb 3838 df-dif 3892 df-un 3894 df-in 3896 df-ss 3906 df-pss 3909 df-nul 4274 df-if 4467 df-pw 4543 df-sn 4568 df-pr 4570 df-tp 4572 df-op 4574 df-uni 4851 df-int 4890 df-iun 4935 df-iin 4936 df-br 5086 df-opab 5148 df-mpt 5167 df-tr 5193 df-id 5526 df-eprel 5531 df-po 5539 df-so 5540 df-fr 5584 df-se 5585 df-we 5586 df-xp 5637 df-rel 5638 df-cnv 5639 df-co 5640 df-dm 5641 df-rn 5642 df-res 5643 df-ima 5644 df-pred 6265 df-ord 6326 df-on 6327 df-lim 6328 df-suc 6329 df-iota 6454 df-fun 6500 df-fn 6501 df-f 6502 df-f1 6503 df-fo 6504 df-f1o 6505 df-fv 6506 df-isom 6507 df-riota 7324 df-ov 7370 df-oprab 7371 df-mpo 7372 df-of 7631 df-om 7818 df-1st 7942 df-2nd 7943 df-supp 8111 df-frecs 8231 df-wrecs 8262 df-recs 8311 df-rdg 8349 df-1o 8405 df-2o 8406 df-er 8643 df-map 8775 df-pm 8776 df-ixp 8846 df-en 8894 df-dom 8895 df-sdom 8896 df-fin 8897 df-fsupp 9275 df-fi 9324 df-sup 9355 df-inf 9356 df-oi 9425 df-card 9863 df-pnf 11181 df-mnf 11182 df-xr 11183 df-ltxr 11184 df-le 11185 df-sub 11379 df-neg 11380 df-div 11808 df-nn 12175 df-2 12244 df-3 12245 df-4 12246 df-5 12247 df-6 12248 df-7 12249 df-8 12250 df-9 12251 df-n0 12438 df-z 12525 df-dec 12645 df-uz 12789 df-q 12899 df-rp 12943 df-xneg 13063 df-xadd 13064 df-xmul 13065 df-icc 13305 df-fz 13462 df-fzo 13609 df-seq 13964 df-exp 14024 df-hash 14293 df-cj 15061 df-re 15062 df-im 15063 df-sqrt 15197 df-abs 15198 df-struct 17117 df-sets 17134 df-slot 17152 df-ndx 17164 df-base 17180 df-ress 17201 df-plusg 17233 df-mulr 17234 df-starv 17235 df-sca 17236 df-vsca 17237 df-ip 17238 df-tset 17239 df-ple 17240 df-ds 17242 df-unif 17243 df-hom 17244 df-cco 17245 df-rest 17385 df-topn 17386 df-0g 17404 df-gsum 17405 df-topgen 17406 df-pt 17407 df-prds 17410 df-xrs 17466 df-qtop 17471 df-imas 17472 df-xps 17474 df-mre 17548 df-mrc 17549 df-acs 17551 df-mgm 18608 df-sgrp 18687 df-mnd 18703 df-submnd 18752 df-mulg 19044 df-cntz 19292 df-cmn 19757 df-psmet 21344 df-xmet 21345 df-met 21346 df-bl 21347 df-mopn 21348 df-cnfld 21353 df-top 22859 df-topon 22876 df-topsp 22898 df-bases 22911 df-cld 22984 df-ntr 22985 df-cls 22986 df-cn 23192 df-cnp 23193 df-tx 23527 df-hmeo 23720 df-xms 24285 df-ms 24286 df-tms 24287 df-cncf 24845 df-limc 25833 df-dv 25834

This theorem is referenced by: dvmul 25908 dvmulf 25910 dvef 25947

W3C validator