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 25975

Description: The product rule for derivatives at a point. For the (simpler but more limited) function version, see dvmul 25978. (Contributed by Mario Carneiro, 9-Aug-2014.) (Revised by Mario Carneiro, 28-Dec-2016.) Avoid ax-mulf 11235 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 2737	. . . . . . 7 ⊢ (𝐽 ↾_t 𝑆) = (𝐽 ↾_t 𝑆)
3		dvadd.j	. . . . . . 7 ⊢ 𝐽 = (TopOpen‘ℂ_fld)
4		eqid 2737	. . . . . . 7 ⊢ (𝑧 ∈ (𝑋 ∖ {𝐶}) ↦ (((𝐹‘𝑧) − (𝐹‘𝐶)) / (𝑧 − 𝐶))) = (𝑧 ∈ (𝑋 ∖ {𝐶}) ↦ (((𝐹‘𝑧) − (𝐹‘𝐶)) / (𝑧 − 𝐶)))
5		dvaddbr.s	. . . . . . 7 ⊢ (𝜑 → 𝑆 ⊆ ℂ)
6		dvadd.f	. . . . . . 7 ⊢ (𝜑 → 𝐹:𝑋⟶ℂ)
7		dvadd.x	. . . . . . 7 ⊢ (𝜑 → 𝑋 ⊆ 𝑆)
8	2, 3, 4, 5, 6, 7	eldv 25933	. . . . . 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 2737	. . . . . . 7 ⊢ (𝑧 ∈ (𝑌 ∖ {𝐶}) ↦ (((𝐺‘𝑧) − (𝐺‘𝐶)) / (𝑧 − 𝐶))) = (𝑧 ∈ (𝑌 ∖ {𝐶}) ↦ (((𝐺‘𝑧) − (𝐺‘𝐶)) / (𝑧 − 𝐶)))
13		dvadd.g	. . . . . . 7 ⊢ (𝜑 → 𝐺:𝑌⟶ℂ)
14		dvadd.y	. . . . . . 7 ⊢ (𝜑 → 𝑌 ⊆ 𝑆)
15	2, 3, 12, 5, 13, 14	eldv 25933	. . . . . 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 4200	. . 3 ⊢ (𝜑 → 𝐶 ∈ (((int‘(𝐽 ↾_t 𝑆))‘𝑋) ∩ ((int‘(𝐽 ↾_t 𝑆))‘𝑌)))
19	3	cnfldtopon 24803	. . . . . 6 ⊢ 𝐽 ∈ (TopOn‘ℂ)
20		resttopon 23169	. . . . . 6 ⊢ ((𝐽 ∈ (TopOn‘ℂ) ∧ 𝑆 ⊆ ℂ) → (𝐽 ↾_t 𝑆) ∈ (TopOn‘𝑆))
21	19, 5, 20	sylancr 587	. . . . 5 ⊢ (𝜑 → (𝐽 ↾_t 𝑆) ∈ (TopOn‘𝑆))
22		topontop 22919	. . . . 5 ⊢ ((𝐽 ↾_t 𝑆) ∈ (TopOn‘𝑆) → (𝐽 ↾_t 𝑆) ∈ Top)
23	21, 22	syl 17	. . . 4 ⊢ (𝜑 → (𝐽 ↾_t 𝑆) ∈ Top)
24		toponuni 22920	. . . . . 6 ⊢ ((𝐽 ↾_t 𝑆) ∈ (TopOn‘𝑆) → 𝑆 = ∪ (𝐽 ↾_t 𝑆))
25	21, 24	syl 17	. . . . 5 ⊢ (𝜑 → 𝑆 = ∪ (𝐽 ↾_t 𝑆))
26	7, 25	sseqtrd 4020	. . . 4 ⊢ (𝜑 → 𝑋 ⊆ ∪ (𝐽 ↾_t 𝑆))
27	14, 25	sseqtrd 4020	. . . 4 ⊢ (𝜑 → 𝑌 ⊆ ∪ (𝐽 ↾_t 𝑆))
28		eqid 2737	. . . . 5 ⊢ ∪ (𝐽 ↾_t 𝑆) = ∪ (𝐽 ↾_t 𝑆)
29	28	ntrin 23069	. . . 4 ⊢ (((𝐽 ↾_t 𝑆) ∈ Top ∧ 𝑋 ⊆ ∪ (𝐽 ↾_t 𝑆) ∧ 𝑌 ⊆ ∪ (𝐽 ↾_t 𝑆)) → ((int‘(𝐽 ↾_t 𝑆))‘(𝑋 ∩ 𝑌)) = (((int‘(𝐽 ↾_t 𝑆))‘𝑋) ∩ ((int‘(𝐽 ↾_t 𝑆))‘𝑌)))
30	23, 26, 27, 29	syl3anc 1373	. . 3 ⊢ (𝜑 → ((int‘(𝐽 ↾_t 𝑆))‘(𝑋 ∩ 𝑌)) = (((int‘(𝐽 ↾_t 𝑆))‘𝑋) ∩ ((int‘(𝐽 ↾_t 𝑆))‘𝑌)))
31	18, 30	eleqtrrd 2844	. 2 ⊢ (𝜑 → 𝐶 ∈ ((int‘(𝐽 ↾_t 𝑆))‘(𝑋 ∩ 𝑌)))
32	6	adantr 480	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑧 ∈ ((𝑋 ∩ 𝑌) ∖ {𝐶})) → 𝐹:𝑋⟶ℂ)
33		inss1 4237	. . . . . . . . 9 ⊢ (𝑋 ∩ 𝑌) ⊆ 𝑋
34		eldifi 4131	. . . . . . . . . 10 ⊢ (𝑧 ∈ ((𝑋 ∩ 𝑌) ∖ {𝐶}) → 𝑧 ∈ (𝑋 ∩ 𝑌))
35	34	adantl 481	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑧 ∈ ((𝑋 ∩ 𝑌) ∖ {𝐶})) → 𝑧 ∈ (𝑋 ∩ 𝑌))
36	33, 35	sselid 3981	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑧 ∈ ((𝑋 ∩ 𝑌) ∖ {𝐶})) → 𝑧 ∈ 𝑋)
37	32, 36	ffvelcdmd 7105	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑧 ∈ ((𝑋 ∩ 𝑌) ∖ {𝐶})) → (𝐹‘𝑧) ∈ ℂ)
38	5, 6, 7	dvbss 25936	. . . . . . . . . 10 ⊢ (𝜑 → dom (𝑆 D 𝐹) ⊆ 𝑋)
39		reldv 25905	. . . . . . . . . . 11 ⊢ Rel (𝑆 D 𝐹)
40		releldm 5955	. . . . . . . . . . 11 ⊢ ((Rel (𝑆 D 𝐹) ∧ 𝐶(𝑆 D 𝐹)𝐾) → 𝐶 ∈ dom (𝑆 D 𝐹))
41	39, 1, 40	sylancr 587	. . . . . . . . . 10 ⊢ (𝜑 → 𝐶 ∈ dom (𝑆 D 𝐹))
42	38, 41	sseldd 3984	. . . . . . . . 9 ⊢ (𝜑 → 𝐶 ∈ 𝑋)
43	6, 42	ffvelcdmd 7105	. . . . . . . 8 ⊢ (𝜑 → (𝐹‘𝐶) ∈ ℂ)
44	43	adantr 480	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑧 ∈ ((𝑋 ∩ 𝑌) ∖ {𝐶})) → (𝐹‘𝐶) ∈ ℂ)
45	37, 44	subcld 11620	. . . . . 6 ⊢ ((𝜑 ∧ 𝑧 ∈ ((𝑋 ∩ 𝑌) ∖ {𝐶})) → ((𝐹‘𝑧) − (𝐹‘𝐶)) ∈ ℂ)
46	7, 5	sstrd 3994	. . . . . . . . 9 ⊢ (𝜑 → 𝑋 ⊆ ℂ)
47	46	adantr 480	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑧 ∈ ((𝑋 ∩ 𝑌) ∖ {𝐶})) → 𝑋 ⊆ ℂ)
48	47, 36	sseldd 3984	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑧 ∈ ((𝑋 ∩ 𝑌) ∖ {𝐶})) → 𝑧 ∈ ℂ)
49	46, 42	sseldd 3984	. . . . . . . 8 ⊢ (𝜑 → 𝐶 ∈ ℂ)
50	49	adantr 480	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑧 ∈ ((𝑋 ∩ 𝑌) ∖ {𝐶})) → 𝐶 ∈ ℂ)
51	48, 50	subcld 11620	. . . . . 6 ⊢ ((𝜑 ∧ 𝑧 ∈ ((𝑋 ∩ 𝑌) ∖ {𝐶})) → (𝑧 − 𝐶) ∈ ℂ)
52		eldifsni 4790	. . . . . . . 8 ⊢ (𝑧 ∈ ((𝑋 ∩ 𝑌) ∖ {𝐶}) → 𝑧 ≠ 𝐶)
53	52	adantl 481	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑧 ∈ ((𝑋 ∩ 𝑌) ∖ {𝐶})) → 𝑧 ≠ 𝐶)
54	48, 50, 53	subne0d 11629	. . . . . 6 ⊢ ((𝜑 ∧ 𝑧 ∈ ((𝑋 ∩ 𝑌) ∖ {𝐶})) → (𝑧 − 𝐶) ≠ 0)
55	45, 51, 54	divcld 12043	. . . . 5 ⊢ ((𝜑 ∧ 𝑧 ∈ ((𝑋 ∩ 𝑌) ∖ {𝐶})) → (((𝐹‘𝑧) − (𝐹‘𝐶)) / (𝑧 − 𝐶)) ∈ ℂ)
56	13	adantr 480	. . . . . 6 ⊢ ((𝜑 ∧ 𝑧 ∈ ((𝑋 ∩ 𝑌) ∖ {𝐶})) → 𝐺:𝑌⟶ℂ)
57		inss2 4238	. . . . . . 7 ⊢ (𝑋 ∩ 𝑌) ⊆ 𝑌
58	57, 35	sselid 3981	. . . . . 6 ⊢ ((𝜑 ∧ 𝑧 ∈ ((𝑋 ∩ 𝑌) ∖ {𝐶})) → 𝑧 ∈ 𝑌)
59	56, 58	ffvelcdmd 7105	. . . . 5 ⊢ ((𝜑 ∧ 𝑧 ∈ ((𝑋 ∩ 𝑌) ∖ {𝐶})) → (𝐺‘𝑧) ∈ ℂ)
60	55, 59	mulcld 11281	. . . 4 ⊢ ((𝜑 ∧ 𝑧 ∈ ((𝑋 ∩ 𝑌) ∖ {𝐶})) → ((((𝐹‘𝑧) − (𝐹‘𝐶)) / (𝑧 − 𝐶)) · (𝐺‘𝑧)) ∈ ℂ)
61		ssdif 4144	. . . . . . . 8 ⊢ ((𝑋 ∩ 𝑌) ⊆ 𝑌 → ((𝑋 ∩ 𝑌) ∖ {𝐶}) ⊆ (𝑌 ∖ {𝐶}))
62	57, 61	mp1i 13	. . . . . . 7 ⊢ (𝜑 → ((𝑋 ∩ 𝑌) ∖ {𝐶}) ⊆ (𝑌 ∖ {𝐶}))
63	62	sselda 3983	. . . . . 6 ⊢ ((𝜑 ∧ 𝑧 ∈ ((𝑋 ∩ 𝑌) ∖ {𝐶})) → 𝑧 ∈ (𝑌 ∖ {𝐶}))
64	14, 5	sstrd 3994	. . . . . . 7 ⊢ (𝜑 → 𝑌 ⊆ ℂ)
65	5, 13, 14	dvbss 25936	. . . . . . . 8 ⊢ (𝜑 → dom (𝑆 D 𝐺) ⊆ 𝑌)
66		reldv 25905	. . . . . . . . 9 ⊢ Rel (𝑆 D 𝐺)
67		releldm 5955	. . . . . . . . 9 ⊢ ((Rel (𝑆 D 𝐺) ∧ 𝐶(𝑆 D 𝐺)𝐿) → 𝐶 ∈ dom (𝑆 D 𝐺))
68	66, 11, 67	sylancr 587	. . . . . . . 8 ⊢ (𝜑 → 𝐶 ∈ dom (𝑆 D 𝐺))
69	65, 68	sseldd 3984	. . . . . . 7 ⊢ (𝜑 → 𝐶 ∈ 𝑌)
70	13, 64, 69	dvlem 25931	. . . . . 6 ⊢ ((𝜑 ∧ 𝑧 ∈ (𝑌 ∖ {𝐶})) → (((𝐺‘𝑧) − (𝐺‘𝐶)) / (𝑧 − 𝐶)) ∈ ℂ)
71	63, 70	syldan 591	. . . . 5 ⊢ ((𝜑 ∧ 𝑧 ∈ ((𝑋 ∩ 𝑌) ∖ {𝐶})) → (((𝐺‘𝑧) − (𝐺‘𝐶)) / (𝑧 − 𝐶)) ∈ ℂ)
72	71, 44	mulcld 11281	. . . 4 ⊢ ((𝜑 ∧ 𝑧 ∈ ((𝑋 ∩ 𝑌) ∖ {𝐶})) → ((((𝐺‘𝑧) − (𝐺‘𝐶)) / (𝑧 − 𝐶)) · (𝐹‘𝐶)) ∈ ℂ)
73		ssidd 4007	. . . 4 ⊢ (𝜑 → ℂ ⊆ ℂ)
74		txtopon 23599	. . . . . 6 ⊢ ((𝐽 ∈ (TopOn‘ℂ) ∧ 𝐽 ∈ (TopOn‘ℂ)) → (𝐽 ×_t 𝐽) ∈ (TopOn‘(ℂ × ℂ)))
75	19, 19, 74	mp2an 692	. . . . 5 ⊢ (𝐽 ×_t 𝐽) ∈ (TopOn‘(ℂ × ℂ))
76	75	toponrestid 22927	. . . 4 ⊢ (𝐽 ×_t 𝐽) = ((𝐽 ×_t 𝐽) ↾_t (ℂ × ℂ))
77	9	simprd 495	. . . . . . . 8 ⊢ (𝜑 → 𝐾 ∈ ((𝑧 ∈ (𝑋 ∖ {𝐶}) ↦ (((𝐹‘𝑧) − (𝐹‘𝐶)) / (𝑧 − 𝐶))) lim_ℂ 𝐶))
78	6, 46, 42	dvlem 25931	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑧 ∈ (𝑋 ∖ {𝐶})) → (((𝐹‘𝑧) − (𝐹‘𝐶)) / (𝑧 − 𝐶)) ∈ ℂ)
79	78	fmpttd 7135	. . . . . . . . . 10 ⊢ (𝜑 → (𝑧 ∈ (𝑋 ∖ {𝐶}) ↦ (((𝐹‘𝑧) − (𝐹‘𝐶)) / (𝑧 − 𝐶))):(𝑋 ∖ {𝐶})⟶ℂ)
80		ssdif 4144	. . . . . . . . . . 11 ⊢ ((𝑋 ∩ 𝑌) ⊆ 𝑋 → ((𝑋 ∩ 𝑌) ∖ {𝐶}) ⊆ (𝑋 ∖ {𝐶}))
81	33, 80	mp1i 13	. . . . . . . . . 10 ⊢ (𝜑 → ((𝑋 ∩ 𝑌) ∖ {𝐶}) ⊆ (𝑋 ∖ {𝐶}))
82	46	ssdifssd 4147	. . . . . . . . . 10 ⊢ (𝜑 → (𝑋 ∖ {𝐶}) ⊆ ℂ)
83		eqid 2737	. . . . . . . . . 10 ⊢ (𝐽 ↾_t ((𝑋 ∖ {𝐶}) ∪ {𝐶})) = (𝐽 ↾_t ((𝑋 ∖ {𝐶}) ∪ {𝐶}))
84	33, 7	sstrid 3995	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → (𝑋 ∩ 𝑌) ⊆ 𝑆)
85	84, 25	sseqtrd 4020	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (𝑋 ∩ 𝑌) ⊆ ∪ (𝐽 ↾_t 𝑆))
86		difssd 4137	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (∪ (𝐽 ↾_t 𝑆) ∖ 𝑋) ⊆ ∪ (𝐽 ↾_t 𝑆))
87	85, 86	unssd 4192	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → ((𝑋 ∩ 𝑌) ∪ (∪ (𝐽 ↾_t 𝑆) ∖ 𝑋)) ⊆ ∪ (𝐽 ↾_t 𝑆))
88		ssun1 4178	. . . . . . . . . . . . . . . 16 ⊢ (𝑋 ∩ 𝑌) ⊆ ((𝑋 ∩ 𝑌) ∪ (∪ (𝐽 ↾_t 𝑆) ∖ 𝑋))
89	88	a1i 11	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (𝑋 ∩ 𝑌) ⊆ ((𝑋 ∩ 𝑌) ∪ (∪ (𝐽 ↾_t 𝑆) ∖ 𝑋)))
90	28	ntrss 23063	. . . . . . . . . . . . . . 15 ⊢ (((𝐽 ↾_t 𝑆) ∈ Top ∧ ((𝑋 ∩ 𝑌) ∪ (∪ (𝐽 ↾_t 𝑆) ∖ 𝑋)) ⊆ ∪ (𝐽 ↾_t 𝑆) ∧ (𝑋 ∩ 𝑌) ⊆ ((𝑋 ∩ 𝑌) ∪ (∪ (𝐽 ↾_t 𝑆) ∖ 𝑋))) → ((int‘(𝐽 ↾_t 𝑆))‘(𝑋 ∩ 𝑌)) ⊆ ((int‘(𝐽 ↾_t 𝑆))‘((𝑋 ∩ 𝑌) ∪ (∪ (𝐽 ↾_t 𝑆) ∖ 𝑋))))
91	23, 87, 89, 90	syl3anc 1373	. . . . . . . . . . . . . 14 ⊢ (𝜑 → ((int‘(𝐽 ↾_t 𝑆))‘(𝑋 ∩ 𝑌)) ⊆ ((int‘(𝐽 ↾_t 𝑆))‘((𝑋 ∩ 𝑌) ∪ (∪ (𝐽 ↾_t 𝑆) ∖ 𝑋))))
92		eqid 2737	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑥 ∈ (𝑋 ∖ {𝐶}) ↦ (((𝐹‘𝑥) − (𝐹‘𝐶)) / (𝑥 − 𝐶))) = (𝑥 ∈ (𝑋 ∖ {𝐶}) ↦ (((𝐹‘𝑥) − (𝐹‘𝐶)) / (𝑥 − 𝐶)))
93	2, 3, 92, 5, 6, 7	eldv 25933	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → (𝐶(𝑆 D 𝐹)𝐾 ↔ (𝐶 ∈ ((int‘(𝐽 ↾_t 𝑆))‘𝑋) ∧ 𝐾 ∈ ((𝑥 ∈ (𝑋 ∖ {𝐶}) ↦ (((𝐹‘𝑥) − (𝐹‘𝐶)) / (𝑥 − 𝐶))) lim_ℂ 𝐶))))
94	1, 93	mpbid 232	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → (𝐶 ∈ ((int‘(𝐽 ↾_t 𝑆))‘𝑋) ∧ 𝐾 ∈ ((𝑥 ∈ (𝑋 ∖ {𝐶}) ↦ (((𝐹‘𝑥) − (𝐹‘𝐶)) / (𝑥 − 𝐶))) lim_ℂ 𝐶)))
95	94	simpld 494	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → 𝐶 ∈ ((int‘(𝐽 ↾_t 𝑆))‘𝑋))
96		eqid 2737	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑥 ∈ (𝑌 ∖ {𝐶}) ↦ (((𝐺‘𝑥) − (𝐺‘𝐶)) / (𝑥 − 𝐶))) = (𝑥 ∈ (𝑌 ∖ {𝐶}) ↦ (((𝐺‘𝑥) − (𝐺‘𝐶)) / (𝑥 − 𝐶)))
97	2, 3, 96, 5, 13, 14	eldv 25933	. . . . . . . . . . . . . . . . . 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 4200	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → 𝐶 ∈ (((int‘(𝐽 ↾_t 𝑆))‘𝑋) ∩ ((int‘(𝐽 ↾_t 𝑆))‘𝑌)))
101	100, 30	eleqtrrd 2844	. . . . . . . . . . . . . 14 ⊢ (𝜑 → 𝐶 ∈ ((int‘(𝐽 ↾_t 𝑆))‘(𝑋 ∩ 𝑌)))
102	91, 101	sseldd 3984	. . . . . . . . . . . . 13 ⊢ (𝜑 → 𝐶 ∈ ((int‘(𝐽 ↾_t 𝑆))‘((𝑋 ∩ 𝑌) ∪ (∪ (𝐽 ↾_t 𝑆) ∖ 𝑋))))
103	102, 42	elind 4200	. . . . . . . . . . . 12 ⊢ (𝜑 → 𝐶 ∈ (((int‘(𝐽 ↾_t 𝑆))‘((𝑋 ∩ 𝑌) ∪ (∪ (𝐽 ↾_t 𝑆) ∖ 𝑋))) ∩ 𝑋))
104	33	a1i 11	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (𝑋 ∩ 𝑌) ⊆ 𝑋)
105		eqid 2737	. . . . . . . . . . . . . . 15 ⊢ ((𝐽 ↾_t 𝑆) ↾_t 𝑋) = ((𝐽 ↾_t 𝑆) ↾_t 𝑋)
106	28, 105	restntr 23190	. . . . . . . . . . . . . 14 ⊢ (((𝐽 ↾_t 𝑆) ∈ Top ∧ 𝑋 ⊆ ∪ (𝐽 ↾_t 𝑆) ∧ (𝑋 ∩ 𝑌) ⊆ 𝑋) → ((int‘((𝐽 ↾_t 𝑆) ↾_t 𝑋))‘(𝑋 ∩ 𝑌)) = (((int‘(𝐽 ↾_t 𝑆))‘((𝑋 ∩ 𝑌) ∪ (∪ (𝐽 ↾_t 𝑆) ∖ 𝑋))) ∩ 𝑋))
107	23, 26, 104, 106	syl3anc 1373	. . . . . . . . . . . . 13 ⊢ (𝜑 → ((int‘((𝐽 ↾_t 𝑆) ↾_t 𝑋))‘(𝑋 ∩ 𝑌)) = (((int‘(𝐽 ↾_t 𝑆))‘((𝑋 ∩ 𝑌) ∪ (∪ (𝐽 ↾_t 𝑆) ∖ 𝑋))) ∩ 𝑋))
108	3	cnfldtop 24804	. . . . . . . . . . . . . . . . 17 ⊢ 𝐽 ∈ Top
109	108	a1i 11	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → 𝐽 ∈ Top)
110		cnex 11236	. . . . . . . . . . . . . . . . 17 ⊢ ℂ ∈ V
111		ssexg 5323	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑆 ⊆ ℂ ∧ ℂ ∈ V) → 𝑆 ∈ V)
112	5, 110, 111	sylancl 586	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → 𝑆 ∈ V)
113		restabs 23173	. . . . . . . . . . . . . . . 16 ⊢ ((𝐽 ∈ Top ∧ 𝑋 ⊆ 𝑆 ∧ 𝑆 ∈ V) → ((𝐽 ↾_t 𝑆) ↾_t 𝑋) = (𝐽 ↾_t 𝑋))
114	109, 7, 112, 113	syl3anc 1373	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → ((𝐽 ↾_t 𝑆) ↾_t 𝑋) = (𝐽 ↾_t 𝑋))
115	114	fveq2d 6910	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (int‘((𝐽 ↾_t 𝑆) ↾_t 𝑋)) = (int‘(𝐽 ↾_t 𝑋)))
116	115	fveq1d 6908	. . . . . . . . . . . . 13 ⊢ (𝜑 → ((int‘((𝐽 ↾_t 𝑆) ↾_t 𝑋))‘(𝑋 ∩ 𝑌)) = ((int‘(𝐽 ↾_t 𝑋))‘(𝑋 ∩ 𝑌)))
117	107, 116	eqtr3d 2779	. . . . . . . . . . . 12 ⊢ (𝜑 → (((int‘(𝐽 ↾_t 𝑆))‘((𝑋 ∩ 𝑌) ∪ (∪ (𝐽 ↾_t 𝑆) ∖ 𝑋))) ∩ 𝑋) = ((int‘(𝐽 ↾_t 𝑋))‘(𝑋 ∩ 𝑌)))
118	103, 117	eleqtrd 2843	. . . . . . . . . . 11 ⊢ (𝜑 → 𝐶 ∈ ((int‘(𝐽 ↾_t 𝑋))‘(𝑋 ∩ 𝑌)))
119		undif1 4476	. . . . . . . . . . . . . . 15 ⊢ ((𝑋 ∖ {𝐶}) ∪ {𝐶}) = (𝑋 ∪ {𝐶})
120	42	snssd 4809	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → {𝐶} ⊆ 𝑋)
121		ssequn2 4189	. . . . . . . . . . . . . . . 16 ⊢ ({𝐶} ⊆ 𝑋 ↔ (𝑋 ∪ {𝐶}) = 𝑋)
122	120, 121	sylib 218	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (𝑋 ∪ {𝐶}) = 𝑋)
123	119, 122	eqtrid 2789	. . . . . . . . . . . . . 14 ⊢ (𝜑 → ((𝑋 ∖ {𝐶}) ∪ {𝐶}) = 𝑋)
124	123	oveq2d 7447	. . . . . . . . . . . . 13 ⊢ (𝜑 → (𝐽 ↾_t ((𝑋 ∖ {𝐶}) ∪ {𝐶})) = (𝐽 ↾_t 𝑋))
125	124	fveq2d 6910	. . . . . . . . . . . 12 ⊢ (𝜑 → (int‘(𝐽 ↾_t ((𝑋 ∖ {𝐶}) ∪ {𝐶}))) = (int‘(𝐽 ↾_t 𝑋)))
126		undif1 4476	. . . . . . . . . . . . 13 ⊢ (((𝑋 ∩ 𝑌) ∖ {𝐶}) ∪ {𝐶}) = ((𝑋 ∩ 𝑌) ∪ {𝐶})
127	42, 69	elind 4200	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → 𝐶 ∈ (𝑋 ∩ 𝑌))
128	127	snssd 4809	. . . . . . . . . . . . . 14 ⊢ (𝜑 → {𝐶} ⊆ (𝑋 ∩ 𝑌))
129		ssequn2 4189	. . . . . . . . . . . . . 14 ⊢ ({𝐶} ⊆ (𝑋 ∩ 𝑌) ↔ ((𝑋 ∩ 𝑌) ∪ {𝐶}) = (𝑋 ∩ 𝑌))
130	128, 129	sylib 218	. . . . . . . . . . . . 13 ⊢ (𝜑 → ((𝑋 ∩ 𝑌) ∪ {𝐶}) = (𝑋 ∩ 𝑌))
131	126, 130	eqtrid 2789	. . . . . . . . . . . 12 ⊢ (𝜑 → (((𝑋 ∩ 𝑌) ∖ {𝐶}) ∪ {𝐶}) = (𝑋 ∩ 𝑌))
132	125, 131	fveq12d 6913	. . . . . . . . . . 11 ⊢ (𝜑 → ((int‘(𝐽 ↾_t ((𝑋 ∖ {𝐶}) ∪ {𝐶})))‘(((𝑋 ∩ 𝑌) ∖ {𝐶}) ∪ {𝐶})) = ((int‘(𝐽 ↾_t 𝑋))‘(𝑋 ∩ 𝑌)))
133	118, 132	eleqtrrd 2844	. . . . . . . . . 10 ⊢ (𝜑 → 𝐶 ∈ ((int‘(𝐽 ↾_t ((𝑋 ∖ {𝐶}) ∪ {𝐶})))‘(((𝑋 ∩ 𝑌) ∖ {𝐶}) ∪ {𝐶})))
134	79, 81, 82, 3, 83, 133	limcres 25921	. . . . . . . . 9 ⊢ (𝜑 → (((𝑧 ∈ (𝑋 ∖ {𝐶}) ↦ (((𝐹‘𝑧) − (𝐹‘𝐶)) / (𝑧 − 𝐶))) ↾ ((𝑋 ∩ 𝑌) ∖ {𝐶})) lim_ℂ 𝐶) = ((𝑧 ∈ (𝑋 ∖ {𝐶}) ↦ (((𝐹‘𝑧) − (𝐹‘𝐶)) / (𝑧 − 𝐶))) lim_ℂ 𝐶))
135	81	resmptd 6058	. . . . . . . . . 10 ⊢ (𝜑 → ((𝑧 ∈ (𝑋 ∖ {𝐶}) ↦ (((𝐹‘𝑧) − (𝐹‘𝐶)) / (𝑧 − 𝐶))) ↾ ((𝑋 ∩ 𝑌) ∖ {𝐶})) = (𝑧 ∈ ((𝑋 ∩ 𝑌) ∖ {𝐶}) ↦ (((𝐹‘𝑧) − (𝐹‘𝐶)) / (𝑧 − 𝐶))))
136	135	oveq1d 7446	. . . . . . . . 9 ⊢ (𝜑 → (((𝑧 ∈ (𝑋 ∖ {𝐶}) ↦ (((𝐹‘𝑧) − (𝐹‘𝐶)) / (𝑧 − 𝐶))) ↾ ((𝑋 ∩ 𝑌) ∖ {𝐶})) lim_ℂ 𝐶) = ((𝑧 ∈ ((𝑋 ∩ 𝑌) ∖ {𝐶}) ↦ (((𝐹‘𝑧) − (𝐹‘𝐶)) / (𝑧 − 𝐶))) lim_ℂ 𝐶))
137	134, 136	eqtr3d 2779	. . . . . . . 8 ⊢ (𝜑 → ((𝑧 ∈ (𝑋 ∖ {𝐶}) ↦ (((𝐹‘𝑧) − (𝐹‘𝐶)) / (𝑧 − 𝐶))) lim_ℂ 𝐶) = ((𝑧 ∈ ((𝑋 ∩ 𝑌) ∖ {𝐶}) ↦ (((𝐹‘𝑧) − (𝐹‘𝐶)) / (𝑧 − 𝐶))) lim_ℂ 𝐶))
138	77, 137	eleqtrd 2843	. . . . . . 7 ⊢ (𝜑 → 𝐾 ∈ ((𝑧 ∈ ((𝑋 ∩ 𝑌) ∖ {𝐶}) ↦ (((𝐹‘𝑧) − (𝐹‘𝐶)) / (𝑧 − 𝐶))) lim_ℂ 𝐶))
139		eqid 2737	. . . . . . . . . . . 12 ⊢ (𝐽 ↾_t 𝑌) = (𝐽 ↾_t 𝑌)
140	139, 3	dvcnp2 25955	. . . . . . . . . . 11 ⊢ (((𝑆 ⊆ ℂ ∧ 𝐺:𝑌⟶ℂ ∧ 𝑌 ⊆ 𝑆) ∧ 𝐶 ∈ dom (𝑆 D 𝐺)) → 𝐺 ∈ (((𝐽 ↾_t 𝑌) CnP 𝐽)‘𝐶))
141	5, 13, 14, 68, 140	syl31anc 1375	. . . . . . . . . 10 ⊢ (𝜑 → 𝐺 ∈ (((𝐽 ↾_t 𝑌) CnP 𝐽)‘𝐶))
142	3, 139	cnplimc 25922	. . . . . . . . . . 11 ⊢ ((𝑌 ⊆ ℂ ∧ 𝐶 ∈ 𝑌) → (𝐺 ∈ (((𝐽 ↾_t 𝑌) CnP 𝐽)‘𝐶) ↔ (𝐺:𝑌⟶ℂ ∧ (𝐺‘𝐶) ∈ (𝐺 lim_ℂ 𝐶))))
143	64, 69, 142	syl2anc 584	. . . . . . . . . 10 ⊢ (𝜑 → (𝐺 ∈ (((𝐽 ↾_t 𝑌) CnP 𝐽)‘𝐶) ↔ (𝐺:𝑌⟶ℂ ∧ (𝐺‘𝐶) ∈ (𝐺 lim_ℂ 𝐶))))
144	141, 143	mpbid 232	. . . . . . . . 9 ⊢ (𝜑 → (𝐺:𝑌⟶ℂ ∧ (𝐺‘𝐶) ∈ (𝐺 lim_ℂ 𝐶)))
145	144	simprd 495	. . . . . . . 8 ⊢ (𝜑 → (𝐺‘𝐶) ∈ (𝐺 lim_ℂ 𝐶))
146		difss 4136	. . . . . . . . . . . 12 ⊢ ((𝑋 ∩ 𝑌) ∖ {𝐶}) ⊆ (𝑋 ∩ 𝑌)
147	146, 57	sstri 3993	. . . . . . . . . . 11 ⊢ ((𝑋 ∩ 𝑌) ∖ {𝐶}) ⊆ 𝑌
148	147	a1i 11	. . . . . . . . . 10 ⊢ (𝜑 → ((𝑋 ∩ 𝑌) ∖ {𝐶}) ⊆ 𝑌)
149		eqid 2737	. . . . . . . . . 10 ⊢ (𝐽 ↾_t (𝑌 ∪ {𝐶})) = (𝐽 ↾_t (𝑌 ∪ {𝐶}))
150		difssd 4137	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (∪ (𝐽 ↾_t 𝑆) ∖ 𝑌) ⊆ ∪ (𝐽 ↾_t 𝑆))
151	85, 150	unssd 4192	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → ((𝑋 ∩ 𝑌) ∪ (∪ (𝐽 ↾_t 𝑆) ∖ 𝑌)) ⊆ ∪ (𝐽 ↾_t 𝑆))
152		ssun1 4178	. . . . . . . . . . . . . . . 16 ⊢ (𝑋 ∩ 𝑌) ⊆ ((𝑋 ∩ 𝑌) ∪ (∪ (𝐽 ↾_t 𝑆) ∖ 𝑌))
153	152	a1i 11	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (𝑋 ∩ 𝑌) ⊆ ((𝑋 ∩ 𝑌) ∪ (∪ (𝐽 ↾_t 𝑆) ∖ 𝑌)))
154	28	ntrss 23063	. . . . . . . . . . . . . . 15 ⊢ (((𝐽 ↾_t 𝑆) ∈ Top ∧ ((𝑋 ∩ 𝑌) ∪ (∪ (𝐽 ↾_t 𝑆) ∖ 𝑌)) ⊆ ∪ (𝐽 ↾_t 𝑆) ∧ (𝑋 ∩ 𝑌) ⊆ ((𝑋 ∩ 𝑌) ∪ (∪ (𝐽 ↾_t 𝑆) ∖ 𝑌))) → ((int‘(𝐽 ↾_t 𝑆))‘(𝑋 ∩ 𝑌)) ⊆ ((int‘(𝐽 ↾_t 𝑆))‘((𝑋 ∩ 𝑌) ∪ (∪ (𝐽 ↾_t 𝑆) ∖ 𝑌))))
155	23, 151, 153, 154	syl3anc 1373	. . . . . . . . . . . . . 14 ⊢ (𝜑 → ((int‘(𝐽 ↾_t 𝑆))‘(𝑋 ∩ 𝑌)) ⊆ ((int‘(𝐽 ↾_t 𝑆))‘((𝑋 ∩ 𝑌) ∪ (∪ (𝐽 ↾_t 𝑆) ∖ 𝑌))))
156	155, 101	sseldd 3984	. . . . . . . . . . . . 13 ⊢ (𝜑 → 𝐶 ∈ ((int‘(𝐽 ↾_t 𝑆))‘((𝑋 ∩ 𝑌) ∪ (∪ (𝐽 ↾_t 𝑆) ∖ 𝑌))))
157	156, 69	elind 4200	. . . . . . . . . . . 12 ⊢ (𝜑 → 𝐶 ∈ (((int‘(𝐽 ↾_t 𝑆))‘((𝑋 ∩ 𝑌) ∪ (∪ (𝐽 ↾_t 𝑆) ∖ 𝑌))) ∩ 𝑌))
158	57	a1i 11	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (𝑋 ∩ 𝑌) ⊆ 𝑌)
159		eqid 2737	. . . . . . . . . . . . . . 15 ⊢ ((𝐽 ↾_t 𝑆) ↾_t 𝑌) = ((𝐽 ↾_t 𝑆) ↾_t 𝑌)
160	28, 159	restntr 23190	. . . . . . . . . . . . . 14 ⊢ (((𝐽 ↾_t 𝑆) ∈ Top ∧ 𝑌 ⊆ ∪ (𝐽 ↾_t 𝑆) ∧ (𝑋 ∩ 𝑌) ⊆ 𝑌) → ((int‘((𝐽 ↾_t 𝑆) ↾_t 𝑌))‘(𝑋 ∩ 𝑌)) = (((int‘(𝐽 ↾_t 𝑆))‘((𝑋 ∩ 𝑌) ∪ (∪ (𝐽 ↾_t 𝑆) ∖ 𝑌))) ∩ 𝑌))
161	23, 27, 158, 160	syl3anc 1373	. . . . . . . . . . . . 13 ⊢ (𝜑 → ((int‘((𝐽 ↾_t 𝑆) ↾_t 𝑌))‘(𝑋 ∩ 𝑌)) = (((int‘(𝐽 ↾_t 𝑆))‘((𝑋 ∩ 𝑌) ∪ (∪ (𝐽 ↾_t 𝑆) ∖ 𝑌))) ∩ 𝑌))
162		restabs 23173	. . . . . . . . . . . . . . . 16 ⊢ ((𝐽 ∈ Top ∧ 𝑌 ⊆ 𝑆 ∧ 𝑆 ∈ V) → ((𝐽 ↾_t 𝑆) ↾_t 𝑌) = (𝐽 ↾_t 𝑌))
163	109, 14, 112, 162	syl3anc 1373	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → ((𝐽 ↾_t 𝑆) ↾_t 𝑌) = (𝐽 ↾_t 𝑌))
164	163	fveq2d 6910	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (int‘((𝐽 ↾_t 𝑆) ↾_t 𝑌)) = (int‘(𝐽 ↾_t 𝑌)))
165	164	fveq1d 6908	. . . . . . . . . . . . 13 ⊢ (𝜑 → ((int‘((𝐽 ↾_t 𝑆) ↾_t 𝑌))‘(𝑋 ∩ 𝑌)) = ((int‘(𝐽 ↾_t 𝑌))‘(𝑋 ∩ 𝑌)))
166	161, 165	eqtr3d 2779	. . . . . . . . . . . 12 ⊢ (𝜑 → (((int‘(𝐽 ↾_t 𝑆))‘((𝑋 ∩ 𝑌) ∪ (∪ (𝐽 ↾_t 𝑆) ∖ 𝑌))) ∩ 𝑌) = ((int‘(𝐽 ↾_t 𝑌))‘(𝑋 ∩ 𝑌)))
167	157, 166	eleqtrd 2843	. . . . . . . . . . 11 ⊢ (𝜑 → 𝐶 ∈ ((int‘(𝐽 ↾_t 𝑌))‘(𝑋 ∩ 𝑌)))
168	69	snssd 4809	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → {𝐶} ⊆ 𝑌)
169		ssequn2 4189	. . . . . . . . . . . . . . 15 ⊢ ({𝐶} ⊆ 𝑌 ↔ (𝑌 ∪ {𝐶}) = 𝑌)
170	168, 169	sylib 218	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (𝑌 ∪ {𝐶}) = 𝑌)
171	170	oveq2d 7447	. . . . . . . . . . . . 13 ⊢ (𝜑 → (𝐽 ↾_t (𝑌 ∪ {𝐶})) = (𝐽 ↾_t 𝑌))
172	171	fveq2d 6910	. . . . . . . . . . . 12 ⊢ (𝜑 → (int‘(𝐽 ↾_t (𝑌 ∪ {𝐶}))) = (int‘(𝐽 ↾_t 𝑌)))
173	172, 131	fveq12d 6913	. . . . . . . . . . 11 ⊢ (𝜑 → ((int‘(𝐽 ↾_t (𝑌 ∪ {𝐶})))‘(((𝑋 ∩ 𝑌) ∖ {𝐶}) ∪ {𝐶})) = ((int‘(𝐽 ↾_t 𝑌))‘(𝑋 ∩ 𝑌)))
174	167, 173	eleqtrrd 2844	. . . . . . . . . 10 ⊢ (𝜑 → 𝐶 ∈ ((int‘(𝐽 ↾_t (𝑌 ∪ {𝐶})))‘(((𝑋 ∩ 𝑌) ∖ {𝐶}) ∪ {𝐶})))
175	13, 148, 64, 3, 149, 174	limcres 25921	. . . . . . . . 9 ⊢ (𝜑 → ((𝐺 ↾ ((𝑋 ∩ 𝑌) ∖ {𝐶})) lim_ℂ 𝐶) = (𝐺 lim_ℂ 𝐶))
176	13, 148	feqresmpt 6978	. . . . . . . . . 10 ⊢ (𝜑 → (𝐺 ↾ ((𝑋 ∩ 𝑌) ∖ {𝐶})) = (𝑧 ∈ ((𝑋 ∩ 𝑌) ∖ {𝐶}) ↦ (𝐺‘𝑧)))
177	176	oveq1d 7446	. . . . . . . . 9 ⊢ (𝜑 → ((𝐺 ↾ ((𝑋 ∩ 𝑌) ∖ {𝐶})) lim_ℂ 𝐶) = ((𝑧 ∈ ((𝑋 ∩ 𝑌) ∖ {𝐶}) ↦ (𝐺‘𝑧)) lim_ℂ 𝐶))
178	175, 177	eqtr3d 2779	. . . . . . . 8 ⊢ (𝜑 → (𝐺 lim_ℂ 𝐶) = ((𝑧 ∈ ((𝑋 ∩ 𝑌) ∖ {𝐶}) ↦ (𝐺‘𝑧)) lim_ℂ 𝐶))
179	145, 178	eleqtrd 2843	. . . . . . 7 ⊢ (𝜑 → (𝐺‘𝐶) ∈ ((𝑧 ∈ ((𝑋 ∩ 𝑌) ∖ {𝐶}) ↦ (𝐺‘𝑧)) lim_ℂ 𝐶))
180	3	mpomulcn 24891	. . . . . . . 8 ⊢ (𝑢 ∈ ℂ, 𝑣 ∈ ℂ ↦ (𝑢 · 𝑣)) ∈ ((𝐽 ×_t 𝐽) Cn 𝐽)
181	5, 6, 7	dvcl 25934	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝐶(𝑆 D 𝐹)𝐾) → 𝐾 ∈ ℂ)
182	1, 181	mpdan 687	. . . . . . . . 9 ⊢ (𝜑 → 𝐾 ∈ ℂ)
183	13, 69	ffvelcdmd 7105	. . . . . . . . 9 ⊢ (𝜑 → (𝐺‘𝐶) ∈ ℂ)
184	182, 183	opelxpd 5724	. . . . . . . 8 ⊢ (𝜑 → ⟨𝐾, (𝐺‘𝐶)⟩ ∈ (ℂ × ℂ))
185	75	toponunii 22922	. . . . . . . . 9 ⊢ (ℂ × ℂ) = ∪ (𝐽 ×_t 𝐽)
186	185	cncnpi 23286	. . . . . . . 8 ⊢ (((𝑢 ∈ ℂ, 𝑣 ∈ ℂ ↦ (𝑢 · 𝑣)) ∈ ((𝐽 ×_t 𝐽) Cn 𝐽) ∧ ⟨𝐾, (𝐺‘𝐶)⟩ ∈ (ℂ × ℂ)) → (𝑢 ∈ ℂ, 𝑣 ∈ ℂ ↦ (𝑢 · 𝑣)) ∈ (((𝐽 ×_t 𝐽) CnP 𝐽)‘⟨𝐾, (𝐺‘𝐶)⟩))
187	180, 184, 186	sylancr 587	. . . . . . 7 ⊢ (𝜑 → (𝑢 ∈ ℂ, 𝑣 ∈ ℂ ↦ (𝑢 · 𝑣)) ∈ (((𝐽 ×_t 𝐽) CnP 𝐽)‘⟨𝐾, (𝐺‘𝐶)⟩))
188	55, 59, 73, 73, 3, 76, 138, 179, 187	limccnp2 25927	. . . . . 6 ⊢ (𝜑 → (𝐾(𝑢 ∈ ℂ, 𝑣 ∈ ℂ ↦ (𝑢 · 𝑣))(𝐺‘𝐶)) ∈ ((𝑧 ∈ ((𝑋 ∩ 𝑌) ∖ {𝐶}) ↦ ((((𝐹‘𝑧) − (𝐹‘𝐶)) / (𝑧 − 𝐶))(𝑢 ∈ ℂ, 𝑣 ∈ ℂ ↦ (𝑢 · 𝑣))(𝐺‘𝑧))) lim_ℂ 𝐶))
189		df-mpt 5226	. . . . . . 7 ⊢ (𝑧 ∈ ((𝑋 ∩ 𝑌) ∖ {𝐶}) ↦ ((((𝐹‘𝑧) − (𝐹‘𝐶)) / (𝑧 − 𝐶))(𝑢 ∈ ℂ, 𝑣 ∈ ℂ ↦ (𝑢 · 𝑣))(𝐺‘𝑧))) = {⟨𝑧, 𝑤⟩ ∣ (𝑧 ∈ ((𝑋 ∩ 𝑌) ∖ {𝐶}) ∧ 𝑤 = ((((𝐹‘𝑧) − (𝐹‘𝐶)) / (𝑧 − 𝐶))(𝑢 ∈ ℂ, 𝑣 ∈ ℂ ↦ (𝑢 · 𝑣))(𝐺‘𝑧)))}
190	189	oveq1i 7441	. . . . . 6 ⊢ ((𝑧 ∈ ((𝑋 ∩ 𝑌) ∖ {𝐶}) ↦ ((((𝐹‘𝑧) − (𝐹‘𝐶)) / (𝑧 − 𝐶))(𝑢 ∈ ℂ, 𝑣 ∈ ℂ ↦ (𝑢 · 𝑣))(𝐺‘𝑧))) lim_ℂ 𝐶) = ({⟨𝑧, 𝑤⟩ ∣ (𝑧 ∈ ((𝑋 ∩ 𝑌) ∖ {𝐶}) ∧ 𝑤 = ((((𝐹‘𝑧) − (𝐹‘𝐶)) / (𝑧 − 𝐶))(𝑢 ∈ ℂ, 𝑣 ∈ ℂ ↦ (𝑢 · 𝑣))(𝐺‘𝑧)))} lim_ℂ 𝐶)
191	188, 190	eleqtrdi 2851	. . . . 5 ⊢ (𝜑 → (𝐾(𝑢 ∈ ℂ, 𝑣 ∈ ℂ ↦ (𝑢 · 𝑣))(𝐺‘𝐶)) ∈ ({⟨𝑧, 𝑤⟩ ∣ (𝑧 ∈ ((𝑋 ∩ 𝑌) ∖ {𝐶}) ∧ 𝑤 = ((((𝐹‘𝑧) − (𝐹‘𝐶)) / (𝑧 − 𝐶))(𝑢 ∈ ℂ, 𝑣 ∈ ℂ ↦ (𝑢 · 𝑣))(𝐺‘𝑧)))} lim_ℂ 𝐶))
192		ovmpot 7594	. . . . . 6 ⊢ ((𝐾 ∈ ℂ ∧ (𝐺‘𝐶) ∈ ℂ) → (𝐾(𝑢 ∈ ℂ, 𝑣 ∈ ℂ ↦ (𝑢 · 𝑣))(𝐺‘𝐶)) = (𝐾 · (𝐺‘𝐶)))
193	182, 183, 192	syl2anc 584	. . . . 5 ⊢ (𝜑 → (𝐾(𝑢 ∈ ℂ, 𝑣 ∈ ℂ ↦ (𝑢 · 𝑣))(𝐺‘𝐶)) = (𝐾 · (𝐺‘𝐶)))
194		ovmpot 7594	. . . . . . . . . . 11 ⊢ (((((𝐹‘𝑧) − (𝐹‘𝐶)) / (𝑧 − 𝐶)) ∈ ℂ ∧ (𝐺‘𝑧) ∈ ℂ) → ((((𝐹‘𝑧) − (𝐹‘𝐶)) / (𝑧 − 𝐶))(𝑢 ∈ ℂ, 𝑣 ∈ ℂ ↦ (𝑢 · 𝑣))(𝐺‘𝑧)) = ((((𝐹‘𝑧) − (𝐹‘𝐶)) / (𝑧 − 𝐶)) · (𝐺‘𝑧)))
195	55, 59, 194	syl2anc 584	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑧 ∈ ((𝑋 ∩ 𝑌) ∖ {𝐶})) → ((((𝐹‘𝑧) − (𝐹‘𝐶)) / (𝑧 − 𝐶))(𝑢 ∈ ℂ, 𝑣 ∈ ℂ ↦ (𝑢 · 𝑣))(𝐺‘𝑧)) = ((((𝐹‘𝑧) − (𝐹‘𝐶)) / (𝑧 − 𝐶)) · (𝐺‘𝑧)))
196	195	eqeq2d 2748	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑧 ∈ ((𝑋 ∩ 𝑌) ∖ {𝐶})) → (𝑤 = ((((𝐹‘𝑧) − (𝐹‘𝐶)) / (𝑧 − 𝐶))(𝑢 ∈ ℂ, 𝑣 ∈ ℂ ↦ (𝑢 · 𝑣))(𝐺‘𝑧)) ↔ 𝑤 = ((((𝐹‘𝑧) − (𝐹‘𝐶)) / (𝑧 − 𝐶)) · (𝐺‘𝑧))))
197	196	pm5.32da 579	. . . . . . . 8 ⊢ (𝜑 → ((𝑧 ∈ ((𝑋 ∩ 𝑌) ∖ {𝐶}) ∧ 𝑤 = ((((𝐹‘𝑧) − (𝐹‘𝐶)) / (𝑧 − 𝐶))(𝑢 ∈ ℂ, 𝑣 ∈ ℂ ↦ (𝑢 · 𝑣))(𝐺‘𝑧))) ↔ (𝑧 ∈ ((𝑋 ∩ 𝑌) ∖ {𝐶}) ∧ 𝑤 = ((((𝐹‘𝑧) − (𝐹‘𝐶)) / (𝑧 − 𝐶)) · (𝐺‘𝑧)))))
198	197	opabbidv 5209	. . . . . . 7 ⊢ (𝜑 → {⟨𝑧, 𝑤⟩ ∣ (𝑧 ∈ ((𝑋 ∩ 𝑌) ∖ {𝐶}) ∧ 𝑤 = ((((𝐹‘𝑧) − (𝐹‘𝐶)) / (𝑧 − 𝐶))(𝑢 ∈ ℂ, 𝑣 ∈ ℂ ↦ (𝑢 · 𝑣))(𝐺‘𝑧)))} = {⟨𝑧, 𝑤⟩ ∣ (𝑧 ∈ ((𝑋 ∩ 𝑌) ∖ {𝐶}) ∧ 𝑤 = ((((𝐹‘𝑧) − (𝐹‘𝐶)) / (𝑧 − 𝐶)) · (𝐺‘𝑧)))})
199		df-mpt 5226	. . . . . . 7 ⊢ (𝑧 ∈ ((𝑋 ∩ 𝑌) ∖ {𝐶}) ↦ ((((𝐹‘𝑧) − (𝐹‘𝐶)) / (𝑧 − 𝐶)) · (𝐺‘𝑧))) = {⟨𝑧, 𝑤⟩ ∣ (𝑧 ∈ ((𝑋 ∩ 𝑌) ∖ {𝐶}) ∧ 𝑤 = ((((𝐹‘𝑧) − (𝐹‘𝐶)) / (𝑧 − 𝐶)) · (𝐺‘𝑧)))}
200	198, 199	eqtr4di 2795	. . . . . 6 ⊢ (𝜑 → {⟨𝑧, 𝑤⟩ ∣ (𝑧 ∈ ((𝑋 ∩ 𝑌) ∖ {𝐶}) ∧ 𝑤 = ((((𝐹‘𝑧) − (𝐹‘𝐶)) / (𝑧 − 𝐶))(𝑢 ∈ ℂ, 𝑣 ∈ ℂ ↦ (𝑢 · 𝑣))(𝐺‘𝑧)))} = (𝑧 ∈ ((𝑋 ∩ 𝑌) ∖ {𝐶}) ↦ ((((𝐹‘𝑧) − (𝐹‘𝐶)) / (𝑧 − 𝐶)) · (𝐺‘𝑧))))
201	200	oveq1d 7446	. . . . 5 ⊢ (𝜑 → ({⟨𝑧, 𝑤⟩ ∣ (𝑧 ∈ ((𝑋 ∩ 𝑌) ∖ {𝐶}) ∧ 𝑤 = ((((𝐹‘𝑧) − (𝐹‘𝐶)) / (𝑧 − 𝐶))(𝑢 ∈ ℂ, 𝑣 ∈ ℂ ↦ (𝑢 · 𝑣))(𝐺‘𝑧)))} lim_ℂ 𝐶) = ((𝑧 ∈ ((𝑋 ∩ 𝑌) ∖ {𝐶}) ↦ ((((𝐹‘𝑧) − (𝐹‘𝐶)) / (𝑧 − 𝐶)) · (𝐺‘𝑧))) lim_ℂ 𝐶))
202	191, 193, 201	3eltr3d 2855	. . . 4 ⊢ (𝜑 → (𝐾 · (𝐺‘𝐶)) ∈ ((𝑧 ∈ ((𝑋 ∩ 𝑌) ∖ {𝐶}) ↦ ((((𝐹‘𝑧) − (𝐹‘𝐶)) / (𝑧 − 𝐶)) · (𝐺‘𝑧))) lim_ℂ 𝐶))
203	16	simprd 495	. . . . . . . 8 ⊢ (𝜑 → 𝐿 ∈ ((𝑧 ∈ (𝑌 ∖ {𝐶}) ↦ (((𝐺‘𝑧) − (𝐺‘𝐶)) / (𝑧 − 𝐶))) lim_ℂ 𝐶))
204	70	fmpttd 7135	. . . . . . . . . 10 ⊢ (𝜑 → (𝑧 ∈ (𝑌 ∖ {𝐶}) ↦ (((𝐺‘𝑧) − (𝐺‘𝐶)) / (𝑧 − 𝐶))):(𝑌 ∖ {𝐶})⟶ℂ)
205	64	ssdifssd 4147	. . . . . . . . . 10 ⊢ (𝜑 → (𝑌 ∖ {𝐶}) ⊆ ℂ)
206		eqid 2737	. . . . . . . . . 10 ⊢ (𝐽 ↾_t ((𝑌 ∖ {𝐶}) ∪ {𝐶})) = (𝐽 ↾_t ((𝑌 ∖ {𝐶}) ∪ {𝐶}))
207		undif1 4476	. . . . . . . . . . . . . . 15 ⊢ ((𝑌 ∖ {𝐶}) ∪ {𝐶}) = (𝑌 ∪ {𝐶})
208	207, 170	eqtrid 2789	. . . . . . . . . . . . . 14 ⊢ (𝜑 → ((𝑌 ∖ {𝐶}) ∪ {𝐶}) = 𝑌)
209	208	oveq2d 7447	. . . . . . . . . . . . 13 ⊢ (𝜑 → (𝐽 ↾_t ((𝑌 ∖ {𝐶}) ∪ {𝐶})) = (𝐽 ↾_t 𝑌))
210	209	fveq2d 6910	. . . . . . . . . . . 12 ⊢ (𝜑 → (int‘(𝐽 ↾_t ((𝑌 ∖ {𝐶}) ∪ {𝐶}))) = (int‘(𝐽 ↾_t 𝑌)))
211	210, 131	fveq12d 6913	. . . . . . . . . . 11 ⊢ (𝜑 → ((int‘(𝐽 ↾_t ((𝑌 ∖ {𝐶}) ∪ {𝐶})))‘(((𝑋 ∩ 𝑌) ∖ {𝐶}) ∪ {𝐶})) = ((int‘(𝐽 ↾_t 𝑌))‘(𝑋 ∩ 𝑌)))
212	167, 211	eleqtrrd 2844	. . . . . . . . . 10 ⊢ (𝜑 → 𝐶 ∈ ((int‘(𝐽 ↾_t ((𝑌 ∖ {𝐶}) ∪ {𝐶})))‘(((𝑋 ∩ 𝑌) ∖ {𝐶}) ∪ {𝐶})))
213	204, 62, 205, 3, 206, 212	limcres 25921	. . . . . . . . 9 ⊢ (𝜑 → (((𝑧 ∈ (𝑌 ∖ {𝐶}) ↦ (((𝐺‘𝑧) − (𝐺‘𝐶)) / (𝑧 − 𝐶))) ↾ ((𝑋 ∩ 𝑌) ∖ {𝐶})) lim_ℂ 𝐶) = ((𝑧 ∈ (𝑌 ∖ {𝐶}) ↦ (((𝐺‘𝑧) − (𝐺‘𝐶)) / (𝑧 − 𝐶))) lim_ℂ 𝐶))
214	62	resmptd 6058	. . . . . . . . . 10 ⊢ (𝜑 → ((𝑧 ∈ (𝑌 ∖ {𝐶}) ↦ (((𝐺‘𝑧) − (𝐺‘𝐶)) / (𝑧 − 𝐶))) ↾ ((𝑋 ∩ 𝑌) ∖ {𝐶})) = (𝑧 ∈ ((𝑋 ∩ 𝑌) ∖ {𝐶}) ↦ (((𝐺‘𝑧) − (𝐺‘𝐶)) / (𝑧 − 𝐶))))
215	214	oveq1d 7446	. . . . . . . . 9 ⊢ (𝜑 → (((𝑧 ∈ (𝑌 ∖ {𝐶}) ↦ (((𝐺‘𝑧) − (𝐺‘𝐶)) / (𝑧 − 𝐶))) ↾ ((𝑋 ∩ 𝑌) ∖ {𝐶})) lim_ℂ 𝐶) = ((𝑧 ∈ ((𝑋 ∩ 𝑌) ∖ {𝐶}) ↦ (((𝐺‘𝑧) − (𝐺‘𝐶)) / (𝑧 − 𝐶))) lim_ℂ 𝐶))
216	213, 215	eqtr3d 2779	. . . . . . . 8 ⊢ (𝜑 → ((𝑧 ∈ (𝑌 ∖ {𝐶}) ↦ (((𝐺‘𝑧) − (𝐺‘𝐶)) / (𝑧 − 𝐶))) lim_ℂ 𝐶) = ((𝑧 ∈ ((𝑋 ∩ 𝑌) ∖ {𝐶}) ↦ (((𝐺‘𝑧) − (𝐺‘𝐶)) / (𝑧 − 𝐶))) lim_ℂ 𝐶))
217	203, 216	eleqtrd 2843	. . . . . . 7 ⊢ (𝜑 → 𝐿 ∈ ((𝑧 ∈ ((𝑋 ∩ 𝑌) ∖ {𝐶}) ↦ (((𝐺‘𝑧) − (𝐺‘𝐶)) / (𝑧 − 𝐶))) lim_ℂ 𝐶))
218	84, 5	sstrd 3994	. . . . . . . . . 10 ⊢ (𝜑 → (𝑋 ∩ 𝑌) ⊆ ℂ)
219		cncfmptc 24938	. . . . . . . . . 10 ⊢ (((𝐹‘𝐶) ∈ ℂ ∧ (𝑋 ∩ 𝑌) ⊆ ℂ ∧ ℂ ⊆ ℂ) → (𝑧 ∈ (𝑋 ∩ 𝑌) ↦ (𝐹‘𝐶)) ∈ ((𝑋 ∩ 𝑌)–cn→ℂ))
220	43, 218, 73, 219	syl3anc 1373	. . . . . . . . 9 ⊢ (𝜑 → (𝑧 ∈ (𝑋 ∩ 𝑌) ↦ (𝐹‘𝐶)) ∈ ((𝑋 ∩ 𝑌)–cn→ℂ))
221		eqidd 2738	. . . . . . . . 9 ⊢ (𝑧 = 𝐶 → (𝐹‘𝐶) = (𝐹‘𝐶))
222	220, 127, 221	cnmptlimc 25925	. . . . . . . 8 ⊢ (𝜑 → (𝐹‘𝐶) ∈ ((𝑧 ∈ (𝑋 ∩ 𝑌) ↦ (𝐹‘𝐶)) lim_ℂ 𝐶))
223	43	adantr 480	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑧 ∈ (𝑋 ∩ 𝑌)) → (𝐹‘𝐶) ∈ ℂ)
224	223	fmpttd 7135	. . . . . . . . . 10 ⊢ (𝜑 → (𝑧 ∈ (𝑋 ∩ 𝑌) ↦ (𝐹‘𝐶)):(𝑋 ∩ 𝑌)⟶ℂ)
225	224	limcdif 25911	. . . . . . . . 9 ⊢ (𝜑 → ((𝑧 ∈ (𝑋 ∩ 𝑌) ↦ (𝐹‘𝐶)) lim_ℂ 𝐶) = (((𝑧 ∈ (𝑋 ∩ 𝑌) ↦ (𝐹‘𝐶)) ↾ ((𝑋 ∩ 𝑌) ∖ {𝐶})) lim_ℂ 𝐶))
226		resmpt 6055	. . . . . . . . . . 11 ⊢ (((𝑋 ∩ 𝑌) ∖ {𝐶}) ⊆ (𝑋 ∩ 𝑌) → ((𝑧 ∈ (𝑋 ∩ 𝑌) ↦ (𝐹‘𝐶)) ↾ ((𝑋 ∩ 𝑌) ∖ {𝐶})) = (𝑧 ∈ ((𝑋 ∩ 𝑌) ∖ {𝐶}) ↦ (𝐹‘𝐶)))
227	146, 226	mp1i 13	. . . . . . . . . 10 ⊢ (𝜑 → ((𝑧 ∈ (𝑋 ∩ 𝑌) ↦ (𝐹‘𝐶)) ↾ ((𝑋 ∩ 𝑌) ∖ {𝐶})) = (𝑧 ∈ ((𝑋 ∩ 𝑌) ∖ {𝐶}) ↦ (𝐹‘𝐶)))
228	227	oveq1d 7446	. . . . . . . . 9 ⊢ (𝜑 → (((𝑧 ∈ (𝑋 ∩ 𝑌) ↦ (𝐹‘𝐶)) ↾ ((𝑋 ∩ 𝑌) ∖ {𝐶})) lim_ℂ 𝐶) = ((𝑧 ∈ ((𝑋 ∩ 𝑌) ∖ {𝐶}) ↦ (𝐹‘𝐶)) lim_ℂ 𝐶))
229	225, 228	eqtrd 2777	. . . . . . . 8 ⊢ (𝜑 → ((𝑧 ∈ (𝑋 ∩ 𝑌) ↦ (𝐹‘𝐶)) lim_ℂ 𝐶) = ((𝑧 ∈ ((𝑋 ∩ 𝑌) ∖ {𝐶}) ↦ (𝐹‘𝐶)) lim_ℂ 𝐶))
230	222, 229	eleqtrd 2843	. . . . . . 7 ⊢ (𝜑 → (𝐹‘𝐶) ∈ ((𝑧 ∈ ((𝑋 ∩ 𝑌) ∖ {𝐶}) ↦ (𝐹‘𝐶)) lim_ℂ 𝐶))
231	5, 13, 14	dvcl 25934	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝐶(𝑆 D 𝐺)𝐿) → 𝐿 ∈ ℂ)
232	11, 231	mpdan 687	. . . . . . . . 9 ⊢ (𝜑 → 𝐿 ∈ ℂ)
233	232, 43	opelxpd 5724	. . . . . . . 8 ⊢ (𝜑 → ⟨𝐿, (𝐹‘𝐶)⟩ ∈ (ℂ × ℂ))
234	185	cncnpi 23286	. . . . . . . 8 ⊢ (((𝑢 ∈ ℂ, 𝑣 ∈ ℂ ↦ (𝑢 · 𝑣)) ∈ ((𝐽 ×_t 𝐽) Cn 𝐽) ∧ ⟨𝐿, (𝐹‘𝐶)⟩ ∈ (ℂ × ℂ)) → (𝑢 ∈ ℂ, 𝑣 ∈ ℂ ↦ (𝑢 · 𝑣)) ∈ (((𝐽 ×_t 𝐽) CnP 𝐽)‘⟨𝐿, (𝐹‘𝐶)⟩))
235	180, 233, 234	sylancr 587	. . . . . . 7 ⊢ (𝜑 → (𝑢 ∈ ℂ, 𝑣 ∈ ℂ ↦ (𝑢 · 𝑣)) ∈ (((𝐽 ×_t 𝐽) CnP 𝐽)‘⟨𝐿, (𝐹‘𝐶)⟩))
236	71, 44, 73, 73, 3, 76, 217, 230, 235	limccnp2 25927	. . . . . 6 ⊢ (𝜑 → (𝐿(𝑢 ∈ ℂ, 𝑣 ∈ ℂ ↦ (𝑢 · 𝑣))(𝐹‘𝐶)) ∈ ((𝑧 ∈ ((𝑋 ∩ 𝑌) ∖ {𝐶}) ↦ ((((𝐺‘𝑧) − (𝐺‘𝐶)) / (𝑧 − 𝐶))(𝑢 ∈ ℂ, 𝑣 ∈ ℂ ↦ (𝑢 · 𝑣))(𝐹‘𝐶))) lim_ℂ 𝐶))
237		df-mpt 5226	. . . . . . 7 ⊢ (𝑧 ∈ ((𝑋 ∩ 𝑌) ∖ {𝐶}) ↦ ((((𝐺‘𝑧) − (𝐺‘𝐶)) / (𝑧 − 𝐶))(𝑢 ∈ ℂ, 𝑣 ∈ ℂ ↦ (𝑢 · 𝑣))(𝐹‘𝐶))) = {⟨𝑧, 𝑤⟩ ∣ (𝑧 ∈ ((𝑋 ∩ 𝑌) ∖ {𝐶}) ∧ 𝑤 = ((((𝐺‘𝑧) − (𝐺‘𝐶)) / (𝑧 − 𝐶))(𝑢 ∈ ℂ, 𝑣 ∈ ℂ ↦ (𝑢 · 𝑣))(𝐹‘𝐶)))}
238	237	oveq1i 7441	. . . . . 6 ⊢ ((𝑧 ∈ ((𝑋 ∩ 𝑌) ∖ {𝐶}) ↦ ((((𝐺‘𝑧) − (𝐺‘𝐶)) / (𝑧 − 𝐶))(𝑢 ∈ ℂ, 𝑣 ∈ ℂ ↦ (𝑢 · 𝑣))(𝐹‘𝐶))) lim_ℂ 𝐶) = ({⟨𝑧, 𝑤⟩ ∣ (𝑧 ∈ ((𝑋 ∩ 𝑌) ∖ {𝐶}) ∧ 𝑤 = ((((𝐺‘𝑧) − (𝐺‘𝐶)) / (𝑧 − 𝐶))(𝑢 ∈ ℂ, 𝑣 ∈ ℂ ↦ (𝑢 · 𝑣))(𝐹‘𝐶)))} lim_ℂ 𝐶)
239	236, 238	eleqtrdi 2851	. . . . 5 ⊢ (𝜑 → (𝐿(𝑢 ∈ ℂ, 𝑣 ∈ ℂ ↦ (𝑢 · 𝑣))(𝐹‘𝐶)) ∈ ({⟨𝑧, 𝑤⟩ ∣ (𝑧 ∈ ((𝑋 ∩ 𝑌) ∖ {𝐶}) ∧ 𝑤 = ((((𝐺‘𝑧) − (𝐺‘𝐶)) / (𝑧 − 𝐶))(𝑢 ∈ ℂ, 𝑣 ∈ ℂ ↦ (𝑢 · 𝑣))(𝐹‘𝐶)))} lim_ℂ 𝐶))
240		ovmpot 7594	. . . . . 6 ⊢ ((𝐿 ∈ ℂ ∧ (𝐹‘𝐶) ∈ ℂ) → (𝐿(𝑢 ∈ ℂ, 𝑣 ∈ ℂ ↦ (𝑢 · 𝑣))(𝐹‘𝐶)) = (𝐿 · (𝐹‘𝐶)))
241	232, 43, 240	syl2anc 584	. . . . 5 ⊢ (𝜑 → (𝐿(𝑢 ∈ ℂ, 𝑣 ∈ ℂ ↦ (𝑢 · 𝑣))(𝐹‘𝐶)) = (𝐿 · (𝐹‘𝐶)))
242	42	adantr 480	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑧 ∈ ((𝑋 ∩ 𝑌) ∖ {𝐶})) → 𝐶 ∈ 𝑋)
243	32, 242	ffvelcdmd 7105	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑧 ∈ ((𝑋 ∩ 𝑌) ∖ {𝐶})) → (𝐹‘𝐶) ∈ ℂ)
244		ovmpot 7594	. . . . . . . . . . 11 ⊢ (((((𝐺‘𝑧) − (𝐺‘𝐶)) / (𝑧 − 𝐶)) ∈ ℂ ∧ (𝐹‘𝐶) ∈ ℂ) → ((((𝐺‘𝑧) − (𝐺‘𝐶)) / (𝑧 − 𝐶))(𝑢 ∈ ℂ, 𝑣 ∈ ℂ ↦ (𝑢 · 𝑣))(𝐹‘𝐶)) = ((((𝐺‘𝑧) − (𝐺‘𝐶)) / (𝑧 − 𝐶)) · (𝐹‘𝐶)))
245	71, 243, 244	syl2anc 584	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑧 ∈ ((𝑋 ∩ 𝑌) ∖ {𝐶})) → ((((𝐺‘𝑧) − (𝐺‘𝐶)) / (𝑧 − 𝐶))(𝑢 ∈ ℂ, 𝑣 ∈ ℂ ↦ (𝑢 · 𝑣))(𝐹‘𝐶)) = ((((𝐺‘𝑧) − (𝐺‘𝐶)) / (𝑧 − 𝐶)) · (𝐹‘𝐶)))
246	245	eqeq2d 2748	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑧 ∈ ((𝑋 ∩ 𝑌) ∖ {𝐶})) → (𝑤 = ((((𝐺‘𝑧) − (𝐺‘𝐶)) / (𝑧 − 𝐶))(𝑢 ∈ ℂ, 𝑣 ∈ ℂ ↦ (𝑢 · 𝑣))(𝐹‘𝐶)) ↔ 𝑤 = ((((𝐺‘𝑧) − (𝐺‘𝐶)) / (𝑧 − 𝐶)) · (𝐹‘𝐶))))
247	246	pm5.32da 579	. . . . . . . 8 ⊢ (𝜑 → ((𝑧 ∈ ((𝑋 ∩ 𝑌) ∖ {𝐶}) ∧ 𝑤 = ((((𝐺‘𝑧) − (𝐺‘𝐶)) / (𝑧 − 𝐶))(𝑢 ∈ ℂ, 𝑣 ∈ ℂ ↦ (𝑢 · 𝑣))(𝐹‘𝐶))) ↔ (𝑧 ∈ ((𝑋 ∩ 𝑌) ∖ {𝐶}) ∧ 𝑤 = ((((𝐺‘𝑧) − (𝐺‘𝐶)) / (𝑧 − 𝐶)) · (𝐹‘𝐶)))))
248	247	opabbidv 5209	. . . . . . 7 ⊢ (𝜑 → {⟨𝑧, 𝑤⟩ ∣ (𝑧 ∈ ((𝑋 ∩ 𝑌) ∖ {𝐶}) ∧ 𝑤 = ((((𝐺‘𝑧) − (𝐺‘𝐶)) / (𝑧 − 𝐶))(𝑢 ∈ ℂ, 𝑣 ∈ ℂ ↦ (𝑢 · 𝑣))(𝐹‘𝐶)))} = {⟨𝑧, 𝑤⟩ ∣ (𝑧 ∈ ((𝑋 ∩ 𝑌) ∖ {𝐶}) ∧ 𝑤 = ((((𝐺‘𝑧) − (𝐺‘𝐶)) / (𝑧 − 𝐶)) · (𝐹‘𝐶)))})
249		df-mpt 5226	. . . . . . 7 ⊢ (𝑧 ∈ ((𝑋 ∩ 𝑌) ∖ {𝐶}) ↦ ((((𝐺‘𝑧) − (𝐺‘𝐶)) / (𝑧 − 𝐶)) · (𝐹‘𝐶))) = {⟨𝑧, 𝑤⟩ ∣ (𝑧 ∈ ((𝑋 ∩ 𝑌) ∖ {𝐶}) ∧ 𝑤 = ((((𝐺‘𝑧) − (𝐺‘𝐶)) / (𝑧 − 𝐶)) · (𝐹‘𝐶)))}
250	248, 249	eqtr4di 2795	. . . . . 6 ⊢ (𝜑 → {⟨𝑧, 𝑤⟩ ∣ (𝑧 ∈ ((𝑋 ∩ 𝑌) ∖ {𝐶}) ∧ 𝑤 = ((((𝐺‘𝑧) − (𝐺‘𝐶)) / (𝑧 − 𝐶))(𝑢 ∈ ℂ, 𝑣 ∈ ℂ ↦ (𝑢 · 𝑣))(𝐹‘𝐶)))} = (𝑧 ∈ ((𝑋 ∩ 𝑌) ∖ {𝐶}) ↦ ((((𝐺‘𝑧) − (𝐺‘𝐶)) / (𝑧 − 𝐶)) · (𝐹‘𝐶))))
251	250	oveq1d 7446	. . . . 5 ⊢ (𝜑 → ({⟨𝑧, 𝑤⟩ ∣ (𝑧 ∈ ((𝑋 ∩ 𝑌) ∖ {𝐶}) ∧ 𝑤 = ((((𝐺‘𝑧) − (𝐺‘𝐶)) / (𝑧 − 𝐶))(𝑢 ∈ ℂ, 𝑣 ∈ ℂ ↦ (𝑢 · 𝑣))(𝐹‘𝐶)))} lim_ℂ 𝐶) = ((𝑧 ∈ ((𝑋 ∩ 𝑌) ∖ {𝐶}) ↦ ((((𝐺‘𝑧) − (𝐺‘𝐶)) / (𝑧 − 𝐶)) · (𝐹‘𝐶))) lim_ℂ 𝐶))
252	239, 241, 251	3eltr3d 2855	. . . 4 ⊢ (𝜑 → (𝐿 · (𝐹‘𝐶)) ∈ ((𝑧 ∈ ((𝑋 ∩ 𝑌) ∖ {𝐶}) ↦ ((((𝐺‘𝑧) − (𝐺‘𝐶)) / (𝑧 − 𝐶)) · (𝐹‘𝐶))) lim_ℂ 𝐶))
253	3	addcn 24887	. . . . 5 ⊢ + ∈ ((𝐽 ×_t 𝐽) Cn 𝐽)
254	182, 183	mulcld 11281	. . . . . 6 ⊢ (𝜑 → (𝐾 · (𝐺‘𝐶)) ∈ ℂ)
255	232, 43	mulcld 11281	. . . . . 6 ⊢ (𝜑 → (𝐿 · (𝐹‘𝐶)) ∈ ℂ)
256	254, 255	opelxpd 5724	. . . . 5 ⊢ (𝜑 → ⟨(𝐾 · (𝐺‘𝐶)), (𝐿 · (𝐹‘𝐶))⟩ ∈ (ℂ × ℂ))
257	185	cncnpi 23286	. . . . 5 ⊢ (( + ∈ ((𝐽 ×_t 𝐽) Cn 𝐽) ∧ ⟨(𝐾 · (𝐺‘𝐶)), (𝐿 · (𝐹‘𝐶))⟩ ∈ (ℂ × ℂ)) → + ∈ (((𝐽 ×_t 𝐽) CnP 𝐽)‘⟨(𝐾 · (𝐺‘𝐶)), (𝐿 · (𝐹‘𝐶))⟩))
258	253, 256, 257	sylancr 587	. . . 4 ⊢ (𝜑 → + ∈ (((𝐽 ×_t 𝐽) CnP 𝐽)‘⟨(𝐾 · (𝐺‘𝐶)), (𝐿 · (𝐹‘𝐶))⟩))
259	60, 72, 73, 73, 3, 76, 202, 252, 258	limccnp2 25927	. . 3 ⊢ (𝜑 → ((𝐾 · (𝐺‘𝐶)) + (𝐿 · (𝐹‘𝐶))) ∈ ((𝑧 ∈ ((𝑋 ∩ 𝑌) ∖ {𝐶}) ↦ (((((𝐹‘𝑧) − (𝐹‘𝐶)) / (𝑧 − 𝐶)) · (𝐺‘𝑧)) + ((((𝐺‘𝑧) − (𝐺‘𝐶)) / (𝑧 − 𝐶)) · (𝐹‘𝐶)))) lim_ℂ 𝐶))
260	37, 243	subcld 11620	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑧 ∈ ((𝑋 ∩ 𝑌) ∖ {𝐶})) → ((𝐹‘𝑧) − (𝐹‘𝐶)) ∈ ℂ)
261	260, 59	mulcld 11281	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑧 ∈ ((𝑋 ∩ 𝑌) ∖ {𝐶})) → (((𝐹‘𝑧) − (𝐹‘𝐶)) · (𝐺‘𝑧)) ∈ ℂ)
262	69	adantr 480	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑧 ∈ ((𝑋 ∩ 𝑌) ∖ {𝐶})) → 𝐶 ∈ 𝑌)
263	56, 262	ffvelcdmd 7105	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑧 ∈ ((𝑋 ∩ 𝑌) ∖ {𝐶})) → (𝐺‘𝐶) ∈ ℂ)
264	59, 263	subcld 11620	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑧 ∈ ((𝑋 ∩ 𝑌) ∖ {𝐶})) → ((𝐺‘𝑧) − (𝐺‘𝐶)) ∈ ℂ)
265	264, 243	mulcld 11281	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑧 ∈ ((𝑋 ∩ 𝑌) ∖ {𝐶})) → (((𝐺‘𝑧) − (𝐺‘𝐶)) · (𝐹‘𝐶)) ∈ ℂ)
266	47, 242	sseldd 3984	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑧 ∈ ((𝑋 ∩ 𝑌) ∖ {𝐶})) → 𝐶 ∈ ℂ)
267	48, 266	subcld 11620	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑧 ∈ ((𝑋 ∩ 𝑌) ∖ {𝐶})) → (𝑧 − 𝐶) ∈ ℂ)
268	261, 265, 267, 54	divdird 12081	. . . . . 6 ⊢ ((𝜑 ∧ 𝑧 ∈ ((𝑋 ∩ 𝑌) ∖ {𝐶})) → (((((𝐹‘𝑧) − (𝐹‘𝐶)) · (𝐺‘𝑧)) + (((𝐺‘𝑧) − (𝐺‘𝐶)) · (𝐹‘𝐶))) / (𝑧 − 𝐶)) = (((((𝐹‘𝑧) − (𝐹‘𝐶)) · (𝐺‘𝑧)) / (𝑧 − 𝐶)) + ((((𝐺‘𝑧) − (𝐺‘𝐶)) · (𝐹‘𝐶)) / (𝑧 − 𝐶))))
269	37, 59	mulcld 11281	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑧 ∈ ((𝑋 ∩ 𝑌) ∖ {𝐶})) → ((𝐹‘𝑧) · (𝐺‘𝑧)) ∈ ℂ)
270	243, 59	mulcld 11281	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑧 ∈ ((𝑋 ∩ 𝑌) ∖ {𝐶})) → ((𝐹‘𝐶) · (𝐺‘𝑧)) ∈ ℂ)
271	243, 263	mulcld 11281	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑧 ∈ ((𝑋 ∩ 𝑌) ∖ {𝐶})) → ((𝐹‘𝐶) · (𝐺‘𝐶)) ∈ ℂ)
272	269, 270, 271	npncand 11644	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑧 ∈ ((𝑋 ∩ 𝑌) ∖ {𝐶})) → ((((𝐹‘𝑧) · (𝐺‘𝑧)) − ((𝐹‘𝐶) · (𝐺‘𝑧))) + (((𝐹‘𝐶) · (𝐺‘𝑧)) − ((𝐹‘𝐶) · (𝐺‘𝐶)))) = (((𝐹‘𝑧) · (𝐺‘𝑧)) − ((𝐹‘𝐶) · (𝐺‘𝐶))))
273	37, 243, 59	subdird 11720	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑧 ∈ ((𝑋 ∩ 𝑌) ∖ {𝐶})) → (((𝐹‘𝑧) − (𝐹‘𝐶)) · (𝐺‘𝑧)) = (((𝐹‘𝑧) · (𝐺‘𝑧)) − ((𝐹‘𝐶) · (𝐺‘𝑧))))
274	264, 243	mulcomd 11282	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑧 ∈ ((𝑋 ∩ 𝑌) ∖ {𝐶})) → (((𝐺‘𝑧) − (𝐺‘𝐶)) · (𝐹‘𝐶)) = ((𝐹‘𝐶) · ((𝐺‘𝑧) − (𝐺‘𝐶))))
275	243, 59, 263	subdid 11719	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑧 ∈ ((𝑋 ∩ 𝑌) ∖ {𝐶})) → ((𝐹‘𝐶) · ((𝐺‘𝑧) − (𝐺‘𝐶))) = (((𝐹‘𝐶) · (𝐺‘𝑧)) − ((𝐹‘𝐶) · (𝐺‘𝐶))))
276	274, 275	eqtrd 2777	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑧 ∈ ((𝑋 ∩ 𝑌) ∖ {𝐶})) → (((𝐺‘𝑧) − (𝐺‘𝐶)) · (𝐹‘𝐶)) = (((𝐹‘𝐶) · (𝐺‘𝑧)) − ((𝐹‘𝐶) · (𝐺‘𝐶))))
277	273, 276	oveq12d 7449	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑧 ∈ ((𝑋 ∩ 𝑌) ∖ {𝐶})) → ((((𝐹‘𝑧) − (𝐹‘𝐶)) · (𝐺‘𝑧)) + (((𝐺‘𝑧) − (𝐺‘𝐶)) · (𝐹‘𝐶))) = ((((𝐹‘𝑧) · (𝐺‘𝑧)) − ((𝐹‘𝐶) · (𝐺‘𝑧))) + (((𝐹‘𝐶) · (𝐺‘𝑧)) − ((𝐹‘𝐶) · (𝐺‘𝐶)))))
278	6	ffnd 6737	. . . . . . . . . . . 12 ⊢ (𝜑 → 𝐹 Fn 𝑋)
279	278	adantr 480	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑧 ∈ ((𝑋 ∩ 𝑌) ∖ {𝐶})) → 𝐹 Fn 𝑋)
280	13	ffnd 6737	. . . . . . . . . . . 12 ⊢ (𝜑 → 𝐺 Fn 𝑌)
281	280	adantr 480	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑧 ∈ ((𝑋 ∩ 𝑌) ∖ {𝐶})) → 𝐺 Fn 𝑌)
282		ssexg 5323	. . . . . . . . . . . . 13 ⊢ ((𝑋 ⊆ ℂ ∧ ℂ ∈ V) → 𝑋 ∈ V)
283	46, 110, 282	sylancl 586	. . . . . . . . . . . 12 ⊢ (𝜑 → 𝑋 ∈ V)
284	283	adantr 480	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑧 ∈ ((𝑋 ∩ 𝑌) ∖ {𝐶})) → 𝑋 ∈ V)
285		ssexg 5323	. . . . . . . . . . . . 13 ⊢ ((𝑌 ⊆ ℂ ∧ ℂ ∈ V) → 𝑌 ∈ V)
286	64, 110, 285	sylancl 586	. . . . . . . . . . . 12 ⊢ (𝜑 → 𝑌 ∈ V)
287	286	adantr 480	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑧 ∈ ((𝑋 ∩ 𝑌) ∖ {𝐶})) → 𝑌 ∈ V)
288		eqid 2737	. . . . . . . . . . 11 ⊢ (𝑋 ∩ 𝑌) = (𝑋 ∩ 𝑌)
289		eqidd 2738	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑧 ∈ ((𝑋 ∩ 𝑌) ∖ {𝐶})) ∧ 𝑧 ∈ 𝑋) → (𝐹‘𝑧) = (𝐹‘𝑧))
290		eqidd 2738	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑧 ∈ ((𝑋 ∩ 𝑌) ∖ {𝐶})) ∧ 𝑧 ∈ 𝑌) → (𝐺‘𝑧) = (𝐺‘𝑧))
291	279, 281, 284, 287, 288, 289, 290	ofval 7708	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑧 ∈ ((𝑋 ∩ 𝑌) ∖ {𝐶})) ∧ 𝑧 ∈ (𝑋 ∩ 𝑌)) → ((𝐹 ∘_f · 𝐺)‘𝑧) = ((𝐹‘𝑧) · (𝐺‘𝑧)))
292	35, 291	mpdan 687	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑧 ∈ ((𝑋 ∩ 𝑌) ∖ {𝐶})) → ((𝐹 ∘_f · 𝐺)‘𝑧) = ((𝐹‘𝑧) · (𝐺‘𝑧)))
293		eqidd 2738	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑧 ∈ ((𝑋 ∩ 𝑌) ∖ {𝐶})) ∧ 𝐶 ∈ 𝑋) → (𝐹‘𝐶) = (𝐹‘𝐶))
294		eqidd 2738	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑧 ∈ ((𝑋 ∩ 𝑌) ∖ {𝐶})) ∧ 𝐶 ∈ 𝑌) → (𝐺‘𝐶) = (𝐺‘𝐶))
295	279, 281, 284, 287, 288, 293, 294	ofval 7708	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑧 ∈ ((𝑋 ∩ 𝑌) ∖ {𝐶})) ∧ 𝐶 ∈ (𝑋 ∩ 𝑌)) → ((𝐹 ∘_f · 𝐺)‘𝐶) = ((𝐹‘𝐶) · (𝐺‘𝐶)))
296	127, 295	mpidan 689	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑧 ∈ ((𝑋 ∩ 𝑌) ∖ {𝐶})) → ((𝐹 ∘_f · 𝐺)‘𝐶) = ((𝐹‘𝐶) · (𝐺‘𝐶)))
297	292, 296	oveq12d 7449	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑧 ∈ ((𝑋 ∩ 𝑌) ∖ {𝐶})) → (((𝐹 ∘_f · 𝐺)‘𝑧) − ((𝐹 ∘_f · 𝐺)‘𝐶)) = (((𝐹‘𝑧) · (𝐺‘𝑧)) − ((𝐹‘𝐶) · (𝐺‘𝐶))))
298	272, 277, 297	3eqtr4d 2787	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑧 ∈ ((𝑋 ∩ 𝑌) ∖ {𝐶})) → ((((𝐹‘𝑧) − (𝐹‘𝐶)) · (𝐺‘𝑧)) + (((𝐺‘𝑧) − (𝐺‘𝐶)) · (𝐹‘𝐶))) = (((𝐹 ∘_f · 𝐺)‘𝑧) − ((𝐹 ∘_f · 𝐺)‘𝐶)))
299	298	oveq1d 7446	. . . . . 6 ⊢ ((𝜑 ∧ 𝑧 ∈ ((𝑋 ∩ 𝑌) ∖ {𝐶})) → (((((𝐹‘𝑧) − (𝐹‘𝐶)) · (𝐺‘𝑧)) + (((𝐺‘𝑧) − (𝐺‘𝐶)) · (𝐹‘𝐶))) / (𝑧 − 𝐶)) = ((((𝐹 ∘_f · 𝐺)‘𝑧) − ((𝐹 ∘_f · 𝐺)‘𝐶)) / (𝑧 − 𝐶)))
300	260, 59, 267, 54	div23d 12080	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑧 ∈ ((𝑋 ∩ 𝑌) ∖ {𝐶})) → ((((𝐹‘𝑧) − (𝐹‘𝐶)) · (𝐺‘𝑧)) / (𝑧 − 𝐶)) = ((((𝐹‘𝑧) − (𝐹‘𝐶)) / (𝑧 − 𝐶)) · (𝐺‘𝑧)))
301	264, 243, 267, 54	div23d 12080	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑧 ∈ ((𝑋 ∩ 𝑌) ∖ {𝐶})) → ((((𝐺‘𝑧) − (𝐺‘𝐶)) · (𝐹‘𝐶)) / (𝑧 − 𝐶)) = ((((𝐺‘𝑧) − (𝐺‘𝐶)) / (𝑧 − 𝐶)) · (𝐹‘𝐶)))
302	300, 301	oveq12d 7449	. . . . . 6 ⊢ ((𝜑 ∧ 𝑧 ∈ ((𝑋 ∩ 𝑌) ∖ {𝐶})) → (((((𝐹‘𝑧) − (𝐹‘𝐶)) · (𝐺‘𝑧)) / (𝑧 − 𝐶)) + ((((𝐺‘𝑧) − (𝐺‘𝐶)) · (𝐹‘𝐶)) / (𝑧 − 𝐶))) = (((((𝐹‘𝑧) − (𝐹‘𝐶)) / (𝑧 − 𝐶)) · (𝐺‘𝑧)) + ((((𝐺‘𝑧) − (𝐺‘𝐶)) / (𝑧 − 𝐶)) · (𝐹‘𝐶))))
303	268, 299, 302	3eqtr3d 2785	. . . . 5 ⊢ ((𝜑 ∧ 𝑧 ∈ ((𝑋 ∩ 𝑌) ∖ {𝐶})) → ((((𝐹 ∘_f · 𝐺)‘𝑧) − ((𝐹 ∘_f · 𝐺)‘𝐶)) / (𝑧 − 𝐶)) = (((((𝐹‘𝑧) − (𝐹‘𝐶)) / (𝑧 − 𝐶)) · (𝐺‘𝑧)) + ((((𝐺‘𝑧) − (𝐺‘𝐶)) / (𝑧 − 𝐶)) · (𝐹‘𝐶))))
304	303	mpteq2dva 5242	. . . 4 ⊢ (𝜑 → (𝑧 ∈ ((𝑋 ∩ 𝑌) ∖ {𝐶}) ↦ ((((𝐹 ∘_f · 𝐺)‘𝑧) − ((𝐹 ∘_f · 𝐺)‘𝐶)) / (𝑧 − 𝐶))) = (𝑧 ∈ ((𝑋 ∩ 𝑌) ∖ {𝐶}) ↦ (((((𝐹‘𝑧) − (𝐹‘𝐶)) / (𝑧 − 𝐶)) · (𝐺‘𝑧)) + ((((𝐺‘𝑧) − (𝐺‘𝐶)) / (𝑧 − 𝐶)) · (𝐹‘𝐶)))))
305	304	oveq1d 7446	. . 3 ⊢ (𝜑 → ((𝑧 ∈ ((𝑋 ∩ 𝑌) ∖ {𝐶}) ↦ ((((𝐹 ∘_f · 𝐺)‘𝑧) − ((𝐹 ∘_f · 𝐺)‘𝐶)) / (𝑧 − 𝐶))) lim_ℂ 𝐶) = ((𝑧 ∈ ((𝑋 ∩ 𝑌) ∖ {𝐶}) ↦ (((((𝐹‘𝑧) − (𝐹‘𝐶)) / (𝑧 − 𝐶)) · (𝐺‘𝑧)) + ((((𝐺‘𝑧) − (𝐺‘𝐶)) / (𝑧 − 𝐶)) · (𝐹‘𝐶)))) lim_ℂ 𝐶))
306	259, 305	eleqtrrd 2844	. 2 ⊢ (𝜑 → ((𝐾 · (𝐺‘𝐶)) + (𝐿 · (𝐹‘𝐶))) ∈ ((𝑧 ∈ ((𝑋 ∩ 𝑌) ∖ {𝐶}) ↦ ((((𝐹 ∘_f · 𝐺)‘𝑧) − ((𝐹 ∘_f · 𝐺)‘𝐶)) / (𝑧 − 𝐶))) lim_ℂ 𝐶))
307		eqid 2737	. . 3 ⊢ (𝑧 ∈ ((𝑋 ∩ 𝑌) ∖ {𝐶}) ↦ ((((𝐹 ∘_f · 𝐺)‘𝑧) − ((𝐹 ∘_f · 𝐺)‘𝐶)) / (𝑧 − 𝐶))) = (𝑧 ∈ ((𝑋 ∩ 𝑌) ∖ {𝐶}) ↦ ((((𝐹 ∘_f · 𝐺)‘𝑧) − ((𝐹 ∘_f · 𝐺)‘𝐶)) / (𝑧 − 𝐶)))
308		mulcl 11239	. . . . 5 ⊢ ((𝑥 ∈ ℂ ∧ 𝑦 ∈ ℂ) → (𝑥 · 𝑦) ∈ ℂ)
309	308	adantl 481	. . . 4 ⊢ ((𝜑 ∧ (𝑥 ∈ ℂ ∧ 𝑦 ∈ ℂ)) → (𝑥 · 𝑦) ∈ ℂ)
310	309, 6, 13, 283, 286, 288	off 7715	. . 3 ⊢ (𝜑 → (𝐹 ∘_f · 𝐺):(𝑋 ∩ 𝑌)⟶ℂ)
311	2, 3, 307, 5, 310, 84	eldv 25933	. 2 ⊢ (𝜑 → (𝐶(𝑆 D (𝐹 ∘_f · 𝐺))((𝐾 · (𝐺‘𝐶)) + (𝐿 · (𝐹‘𝐶))) ↔ (𝐶 ∈ ((int‘(𝐽 ↾_t 𝑆))‘(𝑋 ∩ 𝑌)) ∧ ((𝐾 · (𝐺‘𝐶)) + (𝐿 · (𝐹‘𝐶))) ∈ ((𝑧 ∈ ((𝑋 ∩ 𝑌) ∖ {𝐶}) ↦ ((((𝐹 ∘_f · 𝐺)‘𝑧) − ((𝐹 ∘_f · 𝐺)‘𝐶)) / (𝑧 − 𝐶))) lim_ℂ 𝐶))))
312	31, 306, 311	mpbir2and 713	1 ⊢ (𝜑 → 𝐶(𝑆 D (𝐹 ∘_f · 𝐺))((𝐾 · (𝐺‘𝐶)) + (𝐿 · (𝐹‘𝐶))))

Colors of variables: wff setvar class

Syntax hints: → wi 4 ↔ wb 206 ∧ wa 395 = wceq 1540 ∈ wcel 2108 ≠ wne 2940 Vcvv 3480 ∖ cdif 3948 ∪ cun 3949 ∩ cin 3950 ⊆ wss 3951 {csn 4626 ⟨cop 4632 ∪ cuni 4907 class class class wbr 5143 {copab 5205 ↦ cmpt 5225 × cxp 5683 dom cdm 5685 ↾ cres 5687 Rel wrel 5690 Fn wfn 6556 ⟶wf 6557 ‘cfv 6561 (class class class)co 7431 ∈ cmpo 7433 ∘_f cof 7695 ℂcc 11153 + caddc 11158 · cmul 11160 − cmin 11492 / cdiv 11920 ↾_t crest 17465 TopOpenctopn 17466 ℂ_fldccnfld 21364 Topctop 22899 TopOnctopon 22916 intcnt 23025 Cn ccn 23232 CnP ccnp 23233 ×_t ctx 23568 –cn→ccncf 24902 lim_ℂ climc 25897 D cdv 25898

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1795 ax-4 1809 ax-5 1910 ax-6 1967 ax-7 2007 ax-8 2110 ax-9 2118 ax-10 2141 ax-11 2157 ax-12 2177 ax-ext 2708 ax-rep 5279 ax-sep 5296 ax-nul 5306 ax-pow 5365 ax-pr 5432 ax-un 7755 ax-cnex 11211 ax-resscn 11212 ax-1cn 11213 ax-icn 11214 ax-addcl 11215 ax-addrcl 11216 ax-mulcl 11217 ax-mulrcl 11218 ax-mulcom 11219 ax-addass 11220 ax-mulass 11221 ax-distr 11222 ax-i2m1 11223 ax-1ne0 11224 ax-1rid 11225 ax-rnegex 11226 ax-rrecex 11227 ax-cnre 11228 ax-pre-lttri 11229 ax-pre-lttrn 11230 ax-pre-ltadd 11231 ax-pre-mulgt0 11232 ax-pre-sup 11233 ax-addf 11234

This theorem depends on definitions: df-bi 207 df-an 396 df-or 849 df-3or 1088 df-3an 1089 df-tru 1543 df-fal 1553 df-ex 1780 df-nf 1784 df-sb 2065 df-mo 2540 df-eu 2569 df-clab 2715 df-cleq 2729 df-clel 2816 df-nfc 2892 df-ne 2941 df-nel 3047 df-ral 3062 df-rex 3071 df-rmo 3380 df-reu 3381 df-rab 3437 df-v 3482 df-sbc 3789 df-csb 3900 df-dif 3954 df-un 3956 df-in 3958 df-ss 3968 df-pss 3971 df-nul 4334 df-if 4526 df-pw 4602 df-sn 4627 df-pr 4629 df-tp 4631 df-op 4633 df-uni 4908 df-int 4947 df-iun 4993 df-iin 4994 df-br 5144 df-opab 5206 df-mpt 5226 df-tr 5260 df-id 5578 df-eprel 5584 df-po 5592 df-so 5593 df-fr 5637 df-se 5638 df-we 5639 df-xp 5691 df-rel 5692 df-cnv 5693 df-co 5694 df-dm 5695 df-rn 5696 df-res 5697 df-ima 5698 df-pred 6321 df-ord 6387 df-on 6388 df-lim 6389 df-suc 6390 df-iota 6514 df-fun 6563 df-fn 6564 df-f 6565 df-f1 6566 df-fo 6567 df-f1o 6568 df-fv 6569 df-isom 6570 df-riota 7388 df-ov 7434 df-oprab 7435 df-mpo 7436 df-of 7697 df-om 7888 df-1st 8014 df-2nd 8015 df-supp 8186 df-frecs 8306 df-wrecs 8337 df-recs 8411 df-rdg 8450 df-1o 8506 df-2o 8507 df-er 8745 df-map 8868 df-pm 8869 df-ixp 8938 df-en 8986 df-dom 8987 df-sdom 8988 df-fin 8989 df-fsupp 9402 df-fi 9451 df-sup 9482 df-inf 9483 df-oi 9550 df-card 9979 df-pnf 11297 df-mnf 11298 df-xr 11299 df-ltxr 11300 df-le 11301 df-sub 11494 df-neg 11495 df-div 11921 df-nn 12267 df-2 12329 df-3 12330 df-4 12331 df-5 12332 df-6 12333 df-7 12334 df-8 12335 df-9 12336 df-n0 12527 df-z 12614 df-dec 12734 df-uz 12879 df-q 12991 df-rp 13035 df-xneg 13154 df-xadd 13155 df-xmul 13156 df-icc 13394 df-fz 13548 df-fzo 13695 df-seq 14043 df-exp 14103 df-hash 14370 df-cj 15138 df-re 15139 df-im 15140 df-sqrt 15274 df-abs 15275 df-struct 17184 df-sets 17201 df-slot 17219 df-ndx 17231 df-base 17248 df-ress 17275 df-plusg 17310 df-mulr 17311 df-starv 17312 df-sca 17313 df-vsca 17314 df-ip 17315 df-tset 17316 df-ple 17317 df-ds 17319 df-unif 17320 df-hom 17321 df-cco 17322 df-rest 17467 df-topn 17468 df-0g 17486 df-gsum 17487 df-topgen 17488 df-pt 17489 df-prds 17492 df-xrs 17547 df-qtop 17552 df-imas 17553 df-xps 17555 df-mre 17629 df-mrc 17630 df-acs 17632 df-mgm 18653 df-sgrp 18732 df-mnd 18748 df-submnd 18797 df-mulg 19086 df-cntz 19335 df-cmn 19800 df-psmet 21356 df-xmet 21357 df-met 21358 df-bl 21359 df-mopn 21360 df-cnfld 21365 df-top 22900 df-topon 22917 df-topsp 22939 df-bases 22953 df-cld 23027 df-ntr 23028 df-cls 23029 df-cn 23235 df-cnp 23236 df-tx 23570 df-hmeo 23763 df-xms 24330 df-ms 24331 df-tms 24332 df-cncf 24904 df-limc 25901 df-dv 25902

This theorem is referenced by: dvmul 25978 dvmulf 25980 dvef 26018

W3C validator