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 25839

Description: The product rule for derivatives at a point. For the (simpler but more limited) function version, see dvmul 25842. (Contributed by Mario Carneiro, 9-Aug-2014.) (Revised by Mario Carneiro, 28-Dec-2016.) Avoid ax-mulf 11089 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 2729	. . . . . . 7 ⊢ (𝐽 ↾_t 𝑆) = (𝐽 ↾_t 𝑆)
3		dvadd.j	. . . . . . 7 ⊢ 𝐽 = (TopOpen‘ℂ_fld)
4		eqid 2729	. . . . . . 7 ⊢ (𝑧 ∈ (𝑋 ∖ {𝐶}) ↦ (((𝐹‘𝑧) − (𝐹‘𝐶)) / (𝑧 − 𝐶))) = (𝑧 ∈ (𝑋 ∖ {𝐶}) ↦ (((𝐹‘𝑧) − (𝐹‘𝐶)) / (𝑧 − 𝐶)))
5		dvaddbr.s	. . . . . . 7 ⊢ (𝜑 → 𝑆 ⊆ ℂ)
6		dvadd.f	. . . . . . 7 ⊢ (𝜑 → 𝐹:𝑋⟶ℂ)
7		dvadd.x	. . . . . . 7 ⊢ (𝜑 → 𝑋 ⊆ 𝑆)
8	2, 3, 4, 5, 6, 7	eldv 25797	. . . . . 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 2729	. . . . . . 7 ⊢ (𝑧 ∈ (𝑌 ∖ {𝐶}) ↦ (((𝐺‘𝑧) − (𝐺‘𝐶)) / (𝑧 − 𝐶))) = (𝑧 ∈ (𝑌 ∖ {𝐶}) ↦ (((𝐺‘𝑧) − (𝐺‘𝐶)) / (𝑧 − 𝐶)))
13		dvadd.g	. . . . . . 7 ⊢ (𝜑 → 𝐺:𝑌⟶ℂ)
14		dvadd.y	. . . . . . 7 ⊢ (𝜑 → 𝑌 ⊆ 𝑆)
15	2, 3, 12, 5, 13, 14	eldv 25797	. . . . . 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 4151	. . 3 ⊢ (𝜑 → 𝐶 ∈ (((int‘(𝐽 ↾_t 𝑆))‘𝑋) ∩ ((int‘(𝐽 ↾_t 𝑆))‘𝑌)))
19	3	cnfldtopon 24668	. . . . . 6 ⊢ 𝐽 ∈ (TopOn‘ℂ)
20		resttopon 23046	. . . . . 6 ⊢ ((𝐽 ∈ (TopOn‘ℂ) ∧ 𝑆 ⊆ ℂ) → (𝐽 ↾_t 𝑆) ∈ (TopOn‘𝑆))
21	19, 5, 20	sylancr 587	. . . . 5 ⊢ (𝜑 → (𝐽 ↾_t 𝑆) ∈ (TopOn‘𝑆))
22		topontop 22798	. . . . 5 ⊢ ((𝐽 ↾_t 𝑆) ∈ (TopOn‘𝑆) → (𝐽 ↾_t 𝑆) ∈ Top)
23	21, 22	syl 17	. . . 4 ⊢ (𝜑 → (𝐽 ↾_t 𝑆) ∈ Top)
24		toponuni 22799	. . . . . 6 ⊢ ((𝐽 ↾_t 𝑆) ∈ (TopOn‘𝑆) → 𝑆 = ∪ (𝐽 ↾_t 𝑆))
25	21, 24	syl 17	. . . . 5 ⊢ (𝜑 → 𝑆 = ∪ (𝐽 ↾_t 𝑆))
26	7, 25	sseqtrd 3972	. . . 4 ⊢ (𝜑 → 𝑋 ⊆ ∪ (𝐽 ↾_t 𝑆))
27	14, 25	sseqtrd 3972	. . . 4 ⊢ (𝜑 → 𝑌 ⊆ ∪ (𝐽 ↾_t 𝑆))
28		eqid 2729	. . . . 5 ⊢ ∪ (𝐽 ↾_t 𝑆) = ∪ (𝐽 ↾_t 𝑆)
29	28	ntrin 22946	. . . 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 2831	. 2 ⊢ (𝜑 → 𝐶 ∈ ((int‘(𝐽 ↾_t 𝑆))‘(𝑋 ∩ 𝑌)))
32	6	adantr 480	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑧 ∈ ((𝑋 ∩ 𝑌) ∖ {𝐶})) → 𝐹:𝑋⟶ℂ)
33		inss1 4188	. . . . . . . . 9 ⊢ (𝑋 ∩ 𝑌) ⊆ 𝑋
34		eldifi 4082	. . . . . . . . . 10 ⊢ (𝑧 ∈ ((𝑋 ∩ 𝑌) ∖ {𝐶}) → 𝑧 ∈ (𝑋 ∩ 𝑌))
35	34	adantl 481	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑧 ∈ ((𝑋 ∩ 𝑌) ∖ {𝐶})) → 𝑧 ∈ (𝑋 ∩ 𝑌))
36	33, 35	sselid 3933	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑧 ∈ ((𝑋 ∩ 𝑌) ∖ {𝐶})) → 𝑧 ∈ 𝑋)
37	32, 36	ffvelcdmd 7019	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑧 ∈ ((𝑋 ∩ 𝑌) ∖ {𝐶})) → (𝐹‘𝑧) ∈ ℂ)
38	5, 6, 7	dvbss 25800	. . . . . . . . . 10 ⊢ (𝜑 → dom (𝑆 D 𝐹) ⊆ 𝑋)
39		reldv 25769	. . . . . . . . . . 11 ⊢ Rel (𝑆 D 𝐹)
40		releldm 5886	. . . . . . . . . . 11 ⊢ ((Rel (𝑆 D 𝐹) ∧ 𝐶(𝑆 D 𝐹)𝐾) → 𝐶 ∈ dom (𝑆 D 𝐹))
41	39, 1, 40	sylancr 587	. . . . . . . . . 10 ⊢ (𝜑 → 𝐶 ∈ dom (𝑆 D 𝐹))
42	38, 41	sseldd 3936	. . . . . . . . 9 ⊢ (𝜑 → 𝐶 ∈ 𝑋)
43	6, 42	ffvelcdmd 7019	. . . . . . . 8 ⊢ (𝜑 → (𝐹‘𝐶) ∈ ℂ)
44	43	adantr 480	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑧 ∈ ((𝑋 ∩ 𝑌) ∖ {𝐶})) → (𝐹‘𝐶) ∈ ℂ)
45	37, 44	subcld 11475	. . . . . 6 ⊢ ((𝜑 ∧ 𝑧 ∈ ((𝑋 ∩ 𝑌) ∖ {𝐶})) → ((𝐹‘𝑧) − (𝐹‘𝐶)) ∈ ℂ)
46	7, 5	sstrd 3946	. . . . . . . . 9 ⊢ (𝜑 → 𝑋 ⊆ ℂ)
47	46	adantr 480	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑧 ∈ ((𝑋 ∩ 𝑌) ∖ {𝐶})) → 𝑋 ⊆ ℂ)
48	47, 36	sseldd 3936	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑧 ∈ ((𝑋 ∩ 𝑌) ∖ {𝐶})) → 𝑧 ∈ ℂ)
49	46, 42	sseldd 3936	. . . . . . . 8 ⊢ (𝜑 → 𝐶 ∈ ℂ)
50	49	adantr 480	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑧 ∈ ((𝑋 ∩ 𝑌) ∖ {𝐶})) → 𝐶 ∈ ℂ)
51	48, 50	subcld 11475	. . . . . 6 ⊢ ((𝜑 ∧ 𝑧 ∈ ((𝑋 ∩ 𝑌) ∖ {𝐶})) → (𝑧 − 𝐶) ∈ ℂ)
52		eldifsni 4741	. . . . . . . 8 ⊢ (𝑧 ∈ ((𝑋 ∩ 𝑌) ∖ {𝐶}) → 𝑧 ≠ 𝐶)
53	52	adantl 481	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑧 ∈ ((𝑋 ∩ 𝑌) ∖ {𝐶})) → 𝑧 ≠ 𝐶)
54	48, 50, 53	subne0d 11484	. . . . . 6 ⊢ ((𝜑 ∧ 𝑧 ∈ ((𝑋 ∩ 𝑌) ∖ {𝐶})) → (𝑧 − 𝐶) ≠ 0)
55	45, 51, 54	divcld 11900	. . . . 5 ⊢ ((𝜑 ∧ 𝑧 ∈ ((𝑋 ∩ 𝑌) ∖ {𝐶})) → (((𝐹‘𝑧) − (𝐹‘𝐶)) / (𝑧 − 𝐶)) ∈ ℂ)
56	13	adantr 480	. . . . . 6 ⊢ ((𝜑 ∧ 𝑧 ∈ ((𝑋 ∩ 𝑌) ∖ {𝐶})) → 𝐺:𝑌⟶ℂ)
57		inss2 4189	. . . . . . 7 ⊢ (𝑋 ∩ 𝑌) ⊆ 𝑌
58	57, 35	sselid 3933	. . . . . 6 ⊢ ((𝜑 ∧ 𝑧 ∈ ((𝑋 ∩ 𝑌) ∖ {𝐶})) → 𝑧 ∈ 𝑌)
59	56, 58	ffvelcdmd 7019	. . . . 5 ⊢ ((𝜑 ∧ 𝑧 ∈ ((𝑋 ∩ 𝑌) ∖ {𝐶})) → (𝐺‘𝑧) ∈ ℂ)
60	55, 59	mulcld 11135	. . . 4 ⊢ ((𝜑 ∧ 𝑧 ∈ ((𝑋 ∩ 𝑌) ∖ {𝐶})) → ((((𝐹‘𝑧) − (𝐹‘𝐶)) / (𝑧 − 𝐶)) · (𝐺‘𝑧)) ∈ ℂ)
61		ssdif 4095	. . . . . . . 8 ⊢ ((𝑋 ∩ 𝑌) ⊆ 𝑌 → ((𝑋 ∩ 𝑌) ∖ {𝐶}) ⊆ (𝑌 ∖ {𝐶}))
62	57, 61	mp1i 13	. . . . . . 7 ⊢ (𝜑 → ((𝑋 ∩ 𝑌) ∖ {𝐶}) ⊆ (𝑌 ∖ {𝐶}))
63	62	sselda 3935	. . . . . 6 ⊢ ((𝜑 ∧ 𝑧 ∈ ((𝑋 ∩ 𝑌) ∖ {𝐶})) → 𝑧 ∈ (𝑌 ∖ {𝐶}))
64	14, 5	sstrd 3946	. . . . . . 7 ⊢ (𝜑 → 𝑌 ⊆ ℂ)
65	5, 13, 14	dvbss 25800	. . . . . . . 8 ⊢ (𝜑 → dom (𝑆 D 𝐺) ⊆ 𝑌)
66		reldv 25769	. . . . . . . . 9 ⊢ Rel (𝑆 D 𝐺)
67		releldm 5886	. . . . . . . . 9 ⊢ ((Rel (𝑆 D 𝐺) ∧ 𝐶(𝑆 D 𝐺)𝐿) → 𝐶 ∈ dom (𝑆 D 𝐺))
68	66, 11, 67	sylancr 587	. . . . . . . 8 ⊢ (𝜑 → 𝐶 ∈ dom (𝑆 D 𝐺))
69	65, 68	sseldd 3936	. . . . . . 7 ⊢ (𝜑 → 𝐶 ∈ 𝑌)
70	13, 64, 69	dvlem 25795	. . . . . 6 ⊢ ((𝜑 ∧ 𝑧 ∈ (𝑌 ∖ {𝐶})) → (((𝐺‘𝑧) − (𝐺‘𝐶)) / (𝑧 − 𝐶)) ∈ ℂ)
71	63, 70	syldan 591	. . . . 5 ⊢ ((𝜑 ∧ 𝑧 ∈ ((𝑋 ∩ 𝑌) ∖ {𝐶})) → (((𝐺‘𝑧) − (𝐺‘𝐶)) / (𝑧 − 𝐶)) ∈ ℂ)
72	71, 44	mulcld 11135	. . . 4 ⊢ ((𝜑 ∧ 𝑧 ∈ ((𝑋 ∩ 𝑌) ∖ {𝐶})) → ((((𝐺‘𝑧) − (𝐺‘𝐶)) / (𝑧 − 𝐶)) · (𝐹‘𝐶)) ∈ ℂ)
73		ssidd 3959	. . . 4 ⊢ (𝜑 → ℂ ⊆ ℂ)
74		txtopon 23476	. . . . . 6 ⊢ ((𝐽 ∈ (TopOn‘ℂ) ∧ 𝐽 ∈ (TopOn‘ℂ)) → (𝐽 ×_t 𝐽) ∈ (TopOn‘(ℂ × ℂ)))
75	19, 19, 74	mp2an 692	. . . . 5 ⊢ (𝐽 ×_t 𝐽) ∈ (TopOn‘(ℂ × ℂ))
76	75	toponrestid 22806	. . . 4 ⊢ (𝐽 ×_t 𝐽) = ((𝐽 ×_t 𝐽) ↾_t (ℂ × ℂ))
77	9	simprd 495	. . . . . . . 8 ⊢ (𝜑 → 𝐾 ∈ ((𝑧 ∈ (𝑋 ∖ {𝐶}) ↦ (((𝐹‘𝑧) − (𝐹‘𝐶)) / (𝑧 − 𝐶))) lim_ℂ 𝐶))
78	6, 46, 42	dvlem 25795	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑧 ∈ (𝑋 ∖ {𝐶})) → (((𝐹‘𝑧) − (𝐹‘𝐶)) / (𝑧 − 𝐶)) ∈ ℂ)
79	78	fmpttd 7049	. . . . . . . . . 10 ⊢ (𝜑 → (𝑧 ∈ (𝑋 ∖ {𝐶}) ↦ (((𝐹‘𝑧) − (𝐹‘𝐶)) / (𝑧 − 𝐶))):(𝑋 ∖ {𝐶})⟶ℂ)
80		ssdif 4095	. . . . . . . . . . 11 ⊢ ((𝑋 ∩ 𝑌) ⊆ 𝑋 → ((𝑋 ∩ 𝑌) ∖ {𝐶}) ⊆ (𝑋 ∖ {𝐶}))
81	33, 80	mp1i 13	. . . . . . . . . 10 ⊢ (𝜑 → ((𝑋 ∩ 𝑌) ∖ {𝐶}) ⊆ (𝑋 ∖ {𝐶}))
82	46	ssdifssd 4098	. . . . . . . . . 10 ⊢ (𝜑 → (𝑋 ∖ {𝐶}) ⊆ ℂ)
83		eqid 2729	. . . . . . . . . 10 ⊢ (𝐽 ↾_t ((𝑋 ∖ {𝐶}) ∪ {𝐶})) = (𝐽 ↾_t ((𝑋 ∖ {𝐶}) ∪ {𝐶}))
84	33, 7	sstrid 3947	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → (𝑋 ∩ 𝑌) ⊆ 𝑆)
85	84, 25	sseqtrd 3972	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (𝑋 ∩ 𝑌) ⊆ ∪ (𝐽 ↾_t 𝑆))
86		difssd 4088	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (∪ (𝐽 ↾_t 𝑆) ∖ 𝑋) ⊆ ∪ (𝐽 ↾_t 𝑆))
87	85, 86	unssd 4143	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → ((𝑋 ∩ 𝑌) ∪ (∪ (𝐽 ↾_t 𝑆) ∖ 𝑋)) ⊆ ∪ (𝐽 ↾_t 𝑆))
88		ssun1 4129	. . . . . . . . . . . . . . . 16 ⊢ (𝑋 ∩ 𝑌) ⊆ ((𝑋 ∩ 𝑌) ∪ (∪ (𝐽 ↾_t 𝑆) ∖ 𝑋))
89	88	a1i 11	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (𝑋 ∩ 𝑌) ⊆ ((𝑋 ∩ 𝑌) ∪ (∪ (𝐽 ↾_t 𝑆) ∖ 𝑋)))
90	28	ntrss 22940	. . . . . . . . . . . . . . 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 2729	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑥 ∈ (𝑋 ∖ {𝐶}) ↦ (((𝐹‘𝑥) − (𝐹‘𝐶)) / (𝑥 − 𝐶))) = (𝑥 ∈ (𝑋 ∖ {𝐶}) ↦ (((𝐹‘𝑥) − (𝐹‘𝐶)) / (𝑥 − 𝐶)))
93	2, 3, 92, 5, 6, 7	eldv 25797	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → (𝐶(𝑆 D 𝐹)𝐾 ↔ (𝐶 ∈ ((int‘(𝐽 ↾_t 𝑆))‘𝑋) ∧ 𝐾 ∈ ((𝑥 ∈ (𝑋 ∖ {𝐶}) ↦ (((𝐹‘𝑥) − (𝐹‘𝐶)) / (𝑥 − 𝐶))) lim_ℂ 𝐶))))
94	1, 93	mpbid 232	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → (𝐶 ∈ ((int‘(𝐽 ↾_t 𝑆))‘𝑋) ∧ 𝐾 ∈ ((𝑥 ∈ (𝑋 ∖ {𝐶}) ↦ (((𝐹‘𝑥) − (𝐹‘𝐶)) / (𝑥 − 𝐶))) lim_ℂ 𝐶)))
95	94	simpld 494	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → 𝐶 ∈ ((int‘(𝐽 ↾_t 𝑆))‘𝑋))
96		eqid 2729	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑥 ∈ (𝑌 ∖ {𝐶}) ↦ (((𝐺‘𝑥) − (𝐺‘𝐶)) / (𝑥 − 𝐶))) = (𝑥 ∈ (𝑌 ∖ {𝐶}) ↦ (((𝐺‘𝑥) − (𝐺‘𝐶)) / (𝑥 − 𝐶)))
97	2, 3, 96, 5, 13, 14	eldv 25797	. . . . . . . . . . . . . . . . . 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 4151	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → 𝐶 ∈ (((int‘(𝐽 ↾_t 𝑆))‘𝑋) ∩ ((int‘(𝐽 ↾_t 𝑆))‘𝑌)))
101	100, 30	eleqtrrd 2831	. . . . . . . . . . . . . 14 ⊢ (𝜑 → 𝐶 ∈ ((int‘(𝐽 ↾_t 𝑆))‘(𝑋 ∩ 𝑌)))
102	91, 101	sseldd 3936	. . . . . . . . . . . . 13 ⊢ (𝜑 → 𝐶 ∈ ((int‘(𝐽 ↾_t 𝑆))‘((𝑋 ∩ 𝑌) ∪ (∪ (𝐽 ↾_t 𝑆) ∖ 𝑋))))
103	102, 42	elind 4151	. . . . . . . . . . . 12 ⊢ (𝜑 → 𝐶 ∈ (((int‘(𝐽 ↾_t 𝑆))‘((𝑋 ∩ 𝑌) ∪ (∪ (𝐽 ↾_t 𝑆) ∖ 𝑋))) ∩ 𝑋))
104	33	a1i 11	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (𝑋 ∩ 𝑌) ⊆ 𝑋)
105		eqid 2729	. . . . . . . . . . . . . . 15 ⊢ ((𝐽 ↾_t 𝑆) ↾_t 𝑋) = ((𝐽 ↾_t 𝑆) ↾_t 𝑋)
106	28, 105	restntr 23067	. . . . . . . . . . . . . 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 24669	. . . . . . . . . . . . . . . . 17 ⊢ 𝐽 ∈ Top
109	108	a1i 11	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → 𝐽 ∈ Top)
110		cnex 11090	. . . . . . . . . . . . . . . . 17 ⊢ ℂ ∈ V
111		ssexg 5262	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑆 ⊆ ℂ ∧ ℂ ∈ V) → 𝑆 ∈ V)
112	5, 110, 111	sylancl 586	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → 𝑆 ∈ V)
113		restabs 23050	. . . . . . . . . . . . . . . 16 ⊢ ((𝐽 ∈ Top ∧ 𝑋 ⊆ 𝑆 ∧ 𝑆 ∈ V) → ((𝐽 ↾_t 𝑆) ↾_t 𝑋) = (𝐽 ↾_t 𝑋))
114	109, 7, 112, 113	syl3anc 1373	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → ((𝐽 ↾_t 𝑆) ↾_t 𝑋) = (𝐽 ↾_t 𝑋))
115	114	fveq2d 6826	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (int‘((𝐽 ↾_t 𝑆) ↾_t 𝑋)) = (int‘(𝐽 ↾_t 𝑋)))
116	115	fveq1d 6824	. . . . . . . . . . . . 13 ⊢ (𝜑 → ((int‘((𝐽 ↾_t 𝑆) ↾_t 𝑋))‘(𝑋 ∩ 𝑌)) = ((int‘(𝐽 ↾_t 𝑋))‘(𝑋 ∩ 𝑌)))
117	107, 116	eqtr3d 2766	. . . . . . . . . . . 12 ⊢ (𝜑 → (((int‘(𝐽 ↾_t 𝑆))‘((𝑋 ∩ 𝑌) ∪ (∪ (𝐽 ↾_t 𝑆) ∖ 𝑋))) ∩ 𝑋) = ((int‘(𝐽 ↾_t 𝑋))‘(𝑋 ∩ 𝑌)))
118	103, 117	eleqtrd 2830	. . . . . . . . . . 11 ⊢ (𝜑 → 𝐶 ∈ ((int‘(𝐽 ↾_t 𝑋))‘(𝑋 ∩ 𝑌)))
119		undif1 4427	. . . . . . . . . . . . . . 15 ⊢ ((𝑋 ∖ {𝐶}) ∪ {𝐶}) = (𝑋 ∪ {𝐶})
120	42	snssd 4760	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → {𝐶} ⊆ 𝑋)
121		ssequn2 4140	. . . . . . . . . . . . . . . 16 ⊢ ({𝐶} ⊆ 𝑋 ↔ (𝑋 ∪ {𝐶}) = 𝑋)
122	120, 121	sylib 218	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (𝑋 ∪ {𝐶}) = 𝑋)
123	119, 122	eqtrid 2776	. . . . . . . . . . . . . 14 ⊢ (𝜑 → ((𝑋 ∖ {𝐶}) ∪ {𝐶}) = 𝑋)
124	123	oveq2d 7365	. . . . . . . . . . . . 13 ⊢ (𝜑 → (𝐽 ↾_t ((𝑋 ∖ {𝐶}) ∪ {𝐶})) = (𝐽 ↾_t 𝑋))
125	124	fveq2d 6826	. . . . . . . . . . . 12 ⊢ (𝜑 → (int‘(𝐽 ↾_t ((𝑋 ∖ {𝐶}) ∪ {𝐶}))) = (int‘(𝐽 ↾_t 𝑋)))
126		undif1 4427	. . . . . . . . . . . . 13 ⊢ (((𝑋 ∩ 𝑌) ∖ {𝐶}) ∪ {𝐶}) = ((𝑋 ∩ 𝑌) ∪ {𝐶})
127	42, 69	elind 4151	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → 𝐶 ∈ (𝑋 ∩ 𝑌))
128	127	snssd 4760	. . . . . . . . . . . . . 14 ⊢ (𝜑 → {𝐶} ⊆ (𝑋 ∩ 𝑌))
129		ssequn2 4140	. . . . . . . . . . . . . 14 ⊢ ({𝐶} ⊆ (𝑋 ∩ 𝑌) ↔ ((𝑋 ∩ 𝑌) ∪ {𝐶}) = (𝑋 ∩ 𝑌))
130	128, 129	sylib 218	. . . . . . . . . . . . 13 ⊢ (𝜑 → ((𝑋 ∩ 𝑌) ∪ {𝐶}) = (𝑋 ∩ 𝑌))
131	126, 130	eqtrid 2776	. . . . . . . . . . . 12 ⊢ (𝜑 → (((𝑋 ∩ 𝑌) ∖ {𝐶}) ∪ {𝐶}) = (𝑋 ∩ 𝑌))
132	125, 131	fveq12d 6829	. . . . . . . . . . 11 ⊢ (𝜑 → ((int‘(𝐽 ↾_t ((𝑋 ∖ {𝐶}) ∪ {𝐶})))‘(((𝑋 ∩ 𝑌) ∖ {𝐶}) ∪ {𝐶})) = ((int‘(𝐽 ↾_t 𝑋))‘(𝑋 ∩ 𝑌)))
133	118, 132	eleqtrrd 2831	. . . . . . . . . 10 ⊢ (𝜑 → 𝐶 ∈ ((int‘(𝐽 ↾_t ((𝑋 ∖ {𝐶}) ∪ {𝐶})))‘(((𝑋 ∩ 𝑌) ∖ {𝐶}) ∪ {𝐶})))
134	79, 81, 82, 3, 83, 133	limcres 25785	. . . . . . . . 9 ⊢ (𝜑 → (((𝑧 ∈ (𝑋 ∖ {𝐶}) ↦ (((𝐹‘𝑧) − (𝐹‘𝐶)) / (𝑧 − 𝐶))) ↾ ((𝑋 ∩ 𝑌) ∖ {𝐶})) lim_ℂ 𝐶) = ((𝑧 ∈ (𝑋 ∖ {𝐶}) ↦ (((𝐹‘𝑧) − (𝐹‘𝐶)) / (𝑧 − 𝐶))) lim_ℂ 𝐶))
135	81	resmptd 5991	. . . . . . . . . 10 ⊢ (𝜑 → ((𝑧 ∈ (𝑋 ∖ {𝐶}) ↦ (((𝐹‘𝑧) − (𝐹‘𝐶)) / (𝑧 − 𝐶))) ↾ ((𝑋 ∩ 𝑌) ∖ {𝐶})) = (𝑧 ∈ ((𝑋 ∩ 𝑌) ∖ {𝐶}) ↦ (((𝐹‘𝑧) − (𝐹‘𝐶)) / (𝑧 − 𝐶))))
136	135	oveq1d 7364	. . . . . . . . 9 ⊢ (𝜑 → (((𝑧 ∈ (𝑋 ∖ {𝐶}) ↦ (((𝐹‘𝑧) − (𝐹‘𝐶)) / (𝑧 − 𝐶))) ↾ ((𝑋 ∩ 𝑌) ∖ {𝐶})) lim_ℂ 𝐶) = ((𝑧 ∈ ((𝑋 ∩ 𝑌) ∖ {𝐶}) ↦ (((𝐹‘𝑧) − (𝐹‘𝐶)) / (𝑧 − 𝐶))) lim_ℂ 𝐶))
137	134, 136	eqtr3d 2766	. . . . . . . 8 ⊢ (𝜑 → ((𝑧 ∈ (𝑋 ∖ {𝐶}) ↦ (((𝐹‘𝑧) − (𝐹‘𝐶)) / (𝑧 − 𝐶))) lim_ℂ 𝐶) = ((𝑧 ∈ ((𝑋 ∩ 𝑌) ∖ {𝐶}) ↦ (((𝐹‘𝑧) − (𝐹‘𝐶)) / (𝑧 − 𝐶))) lim_ℂ 𝐶))
138	77, 137	eleqtrd 2830	. . . . . . 7 ⊢ (𝜑 → 𝐾 ∈ ((𝑧 ∈ ((𝑋 ∩ 𝑌) ∖ {𝐶}) ↦ (((𝐹‘𝑧) − (𝐹‘𝐶)) / (𝑧 − 𝐶))) lim_ℂ 𝐶))
139		eqid 2729	. . . . . . . . . . . 12 ⊢ (𝐽 ↾_t 𝑌) = (𝐽 ↾_t 𝑌)
140	139, 3	dvcnp2 25819	. . . . . . . . . . 11 ⊢ (((𝑆 ⊆ ℂ ∧ 𝐺:𝑌⟶ℂ ∧ 𝑌 ⊆ 𝑆) ∧ 𝐶 ∈ dom (𝑆 D 𝐺)) → 𝐺 ∈ (((𝐽 ↾_t 𝑌) CnP 𝐽)‘𝐶))
141	5, 13, 14, 68, 140	syl31anc 1375	. . . . . . . . . 10 ⊢ (𝜑 → 𝐺 ∈ (((𝐽 ↾_t 𝑌) CnP 𝐽)‘𝐶))
142	3, 139	cnplimc 25786	. . . . . . . . . . 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 4087	. . . . . . . . . . . 12 ⊢ ((𝑋 ∩ 𝑌) ∖ {𝐶}) ⊆ (𝑋 ∩ 𝑌)
147	146, 57	sstri 3945	. . . . . . . . . . 11 ⊢ ((𝑋 ∩ 𝑌) ∖ {𝐶}) ⊆ 𝑌
148	147	a1i 11	. . . . . . . . . 10 ⊢ (𝜑 → ((𝑋 ∩ 𝑌) ∖ {𝐶}) ⊆ 𝑌)
149		eqid 2729	. . . . . . . . . 10 ⊢ (𝐽 ↾_t (𝑌 ∪ {𝐶})) = (𝐽 ↾_t (𝑌 ∪ {𝐶}))
150		difssd 4088	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (∪ (𝐽 ↾_t 𝑆) ∖ 𝑌) ⊆ ∪ (𝐽 ↾_t 𝑆))
151	85, 150	unssd 4143	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → ((𝑋 ∩ 𝑌) ∪ (∪ (𝐽 ↾_t 𝑆) ∖ 𝑌)) ⊆ ∪ (𝐽 ↾_t 𝑆))
152		ssun1 4129	. . . . . . . . . . . . . . . 16 ⊢ (𝑋 ∩ 𝑌) ⊆ ((𝑋 ∩ 𝑌) ∪ (∪ (𝐽 ↾_t 𝑆) ∖ 𝑌))
153	152	a1i 11	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (𝑋 ∩ 𝑌) ⊆ ((𝑋 ∩ 𝑌) ∪ (∪ (𝐽 ↾_t 𝑆) ∖ 𝑌)))
154	28	ntrss 22940	. . . . . . . . . . . . . . 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 3936	. . . . . . . . . . . . 13 ⊢ (𝜑 → 𝐶 ∈ ((int‘(𝐽 ↾_t 𝑆))‘((𝑋 ∩ 𝑌) ∪ (∪ (𝐽 ↾_t 𝑆) ∖ 𝑌))))
157	156, 69	elind 4151	. . . . . . . . . . . 12 ⊢ (𝜑 → 𝐶 ∈ (((int‘(𝐽 ↾_t 𝑆))‘((𝑋 ∩ 𝑌) ∪ (∪ (𝐽 ↾_t 𝑆) ∖ 𝑌))) ∩ 𝑌))
158	57	a1i 11	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (𝑋 ∩ 𝑌) ⊆ 𝑌)
159		eqid 2729	. . . . . . . . . . . . . . 15 ⊢ ((𝐽 ↾_t 𝑆) ↾_t 𝑌) = ((𝐽 ↾_t 𝑆) ↾_t 𝑌)
160	28, 159	restntr 23067	. . . . . . . . . . . . . 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 23050	. . . . . . . . . . . . . . . 16 ⊢ ((𝐽 ∈ Top ∧ 𝑌 ⊆ 𝑆 ∧ 𝑆 ∈ V) → ((𝐽 ↾_t 𝑆) ↾_t 𝑌) = (𝐽 ↾_t 𝑌))
163	109, 14, 112, 162	syl3anc 1373	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → ((𝐽 ↾_t 𝑆) ↾_t 𝑌) = (𝐽 ↾_t 𝑌))
164	163	fveq2d 6826	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (int‘((𝐽 ↾_t 𝑆) ↾_t 𝑌)) = (int‘(𝐽 ↾_t 𝑌)))
165	164	fveq1d 6824	. . . . . . . . . . . . 13 ⊢ (𝜑 → ((int‘((𝐽 ↾_t 𝑆) ↾_t 𝑌))‘(𝑋 ∩ 𝑌)) = ((int‘(𝐽 ↾_t 𝑌))‘(𝑋 ∩ 𝑌)))
166	161, 165	eqtr3d 2766	. . . . . . . . . . . 12 ⊢ (𝜑 → (((int‘(𝐽 ↾_t 𝑆))‘((𝑋 ∩ 𝑌) ∪ (∪ (𝐽 ↾_t 𝑆) ∖ 𝑌))) ∩ 𝑌) = ((int‘(𝐽 ↾_t 𝑌))‘(𝑋 ∩ 𝑌)))
167	157, 166	eleqtrd 2830	. . . . . . . . . . 11 ⊢ (𝜑 → 𝐶 ∈ ((int‘(𝐽 ↾_t 𝑌))‘(𝑋 ∩ 𝑌)))
168	69	snssd 4760	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → {𝐶} ⊆ 𝑌)
169		ssequn2 4140	. . . . . . . . . . . . . . 15 ⊢ ({𝐶} ⊆ 𝑌 ↔ (𝑌 ∪ {𝐶}) = 𝑌)
170	168, 169	sylib 218	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (𝑌 ∪ {𝐶}) = 𝑌)
171	170	oveq2d 7365	. . . . . . . . . . . . 13 ⊢ (𝜑 → (𝐽 ↾_t (𝑌 ∪ {𝐶})) = (𝐽 ↾_t 𝑌))
172	171	fveq2d 6826	. . . . . . . . . . . 12 ⊢ (𝜑 → (int‘(𝐽 ↾_t (𝑌 ∪ {𝐶}))) = (int‘(𝐽 ↾_t 𝑌)))
173	172, 131	fveq12d 6829	. . . . . . . . . . 11 ⊢ (𝜑 → ((int‘(𝐽 ↾_t (𝑌 ∪ {𝐶})))‘(((𝑋 ∩ 𝑌) ∖ {𝐶}) ∪ {𝐶})) = ((int‘(𝐽 ↾_t 𝑌))‘(𝑋 ∩ 𝑌)))
174	167, 173	eleqtrrd 2831	. . . . . . . . . 10 ⊢ (𝜑 → 𝐶 ∈ ((int‘(𝐽 ↾_t (𝑌 ∪ {𝐶})))‘(((𝑋 ∩ 𝑌) ∖ {𝐶}) ∪ {𝐶})))
175	13, 148, 64, 3, 149, 174	limcres 25785	. . . . . . . . 9 ⊢ (𝜑 → ((𝐺 ↾ ((𝑋 ∩ 𝑌) ∖ {𝐶})) lim_ℂ 𝐶) = (𝐺 lim_ℂ 𝐶))
176	13, 148	feqresmpt 6892	. . . . . . . . . 10 ⊢ (𝜑 → (𝐺 ↾ ((𝑋 ∩ 𝑌) ∖ {𝐶})) = (𝑧 ∈ ((𝑋 ∩ 𝑌) ∖ {𝐶}) ↦ (𝐺‘𝑧)))
177	176	oveq1d 7364	. . . . . . . . 9 ⊢ (𝜑 → ((𝐺 ↾ ((𝑋 ∩ 𝑌) ∖ {𝐶})) lim_ℂ 𝐶) = ((𝑧 ∈ ((𝑋 ∩ 𝑌) ∖ {𝐶}) ↦ (𝐺‘𝑧)) lim_ℂ 𝐶))
178	175, 177	eqtr3d 2766	. . . . . . . 8 ⊢ (𝜑 → (𝐺 lim_ℂ 𝐶) = ((𝑧 ∈ ((𝑋 ∩ 𝑌) ∖ {𝐶}) ↦ (𝐺‘𝑧)) lim_ℂ 𝐶))
179	145, 178	eleqtrd 2830	. . . . . . 7 ⊢ (𝜑 → (𝐺‘𝐶) ∈ ((𝑧 ∈ ((𝑋 ∩ 𝑌) ∖ {𝐶}) ↦ (𝐺‘𝑧)) lim_ℂ 𝐶))
180	3	mpomulcn 24756	. . . . . . . 8 ⊢ (𝑢 ∈ ℂ, 𝑣 ∈ ℂ ↦ (𝑢 · 𝑣)) ∈ ((𝐽 ×_t 𝐽) Cn 𝐽)
181	5, 6, 7	dvcl 25798	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝐶(𝑆 D 𝐹)𝐾) → 𝐾 ∈ ℂ)
182	1, 181	mpdan 687	. . . . . . . . 9 ⊢ (𝜑 → 𝐾 ∈ ℂ)
183	13, 69	ffvelcdmd 7019	. . . . . . . . 9 ⊢ (𝜑 → (𝐺‘𝐶) ∈ ℂ)
184	182, 183	opelxpd 5658	. . . . . . . 8 ⊢ (𝜑 → ⟨𝐾, (𝐺‘𝐶)⟩ ∈ (ℂ × ℂ))
185	75	toponunii 22801	. . . . . . . . 9 ⊢ (ℂ × ℂ) = ∪ (𝐽 ×_t 𝐽)
186	185	cncnpi 23163	. . . . . . . 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 25791	. . . . . 6 ⊢ (𝜑 → (𝐾(𝑢 ∈ ℂ, 𝑣 ∈ ℂ ↦ (𝑢 · 𝑣))(𝐺‘𝐶)) ∈ ((𝑧 ∈ ((𝑋 ∩ 𝑌) ∖ {𝐶}) ↦ ((((𝐹‘𝑧) − (𝐹‘𝐶)) / (𝑧 − 𝐶))(𝑢 ∈ ℂ, 𝑣 ∈ ℂ ↦ (𝑢 · 𝑣))(𝐺‘𝑧))) lim_ℂ 𝐶))
189		df-mpt 5174	. . . . . . 7 ⊢ (𝑧 ∈ ((𝑋 ∩ 𝑌) ∖ {𝐶}) ↦ ((((𝐹‘𝑧) − (𝐹‘𝐶)) / (𝑧 − 𝐶))(𝑢 ∈ ℂ, 𝑣 ∈ ℂ ↦ (𝑢 · 𝑣))(𝐺‘𝑧))) = {⟨𝑧, 𝑤⟩ ∣ (𝑧 ∈ ((𝑋 ∩ 𝑌) ∖ {𝐶}) ∧ 𝑤 = ((((𝐹‘𝑧) − (𝐹‘𝐶)) / (𝑧 − 𝐶))(𝑢 ∈ ℂ, 𝑣 ∈ ℂ ↦ (𝑢 · 𝑣))(𝐺‘𝑧)))}
190	189	oveq1i 7359	. . . . . 6 ⊢ ((𝑧 ∈ ((𝑋 ∩ 𝑌) ∖ {𝐶}) ↦ ((((𝐹‘𝑧) − (𝐹‘𝐶)) / (𝑧 − 𝐶))(𝑢 ∈ ℂ, 𝑣 ∈ ℂ ↦ (𝑢 · 𝑣))(𝐺‘𝑧))) lim_ℂ 𝐶) = ({⟨𝑧, 𝑤⟩ ∣ (𝑧 ∈ ((𝑋 ∩ 𝑌) ∖ {𝐶}) ∧ 𝑤 = ((((𝐹‘𝑧) − (𝐹‘𝐶)) / (𝑧 − 𝐶))(𝑢 ∈ ℂ, 𝑣 ∈ ℂ ↦ (𝑢 · 𝑣))(𝐺‘𝑧)))} lim_ℂ 𝐶)
191	188, 190	eleqtrdi 2838	. . . . 5 ⊢ (𝜑 → (𝐾(𝑢 ∈ ℂ, 𝑣 ∈ ℂ ↦ (𝑢 · 𝑣))(𝐺‘𝐶)) ∈ ({⟨𝑧, 𝑤⟩ ∣ (𝑧 ∈ ((𝑋 ∩ 𝑌) ∖ {𝐶}) ∧ 𝑤 = ((((𝐹‘𝑧) − (𝐹‘𝐶)) / (𝑧 − 𝐶))(𝑢 ∈ ℂ, 𝑣 ∈ ℂ ↦ (𝑢 · 𝑣))(𝐺‘𝑧)))} lim_ℂ 𝐶))
192		ovmpot 7510	. . . . . 6 ⊢ ((𝐾 ∈ ℂ ∧ (𝐺‘𝐶) ∈ ℂ) → (𝐾(𝑢 ∈ ℂ, 𝑣 ∈ ℂ ↦ (𝑢 · 𝑣))(𝐺‘𝐶)) = (𝐾 · (𝐺‘𝐶)))
193	182, 183, 192	syl2anc 584	. . . . 5 ⊢ (𝜑 → (𝐾(𝑢 ∈ ℂ, 𝑣 ∈ ℂ ↦ (𝑢 · 𝑣))(𝐺‘𝐶)) = (𝐾 · (𝐺‘𝐶)))
194		ovmpot 7510	. . . . . . . . . . 11 ⊢ (((((𝐹‘𝑧) − (𝐹‘𝐶)) / (𝑧 − 𝐶)) ∈ ℂ ∧ (𝐺‘𝑧) ∈ ℂ) → ((((𝐹‘𝑧) − (𝐹‘𝐶)) / (𝑧 − 𝐶))(𝑢 ∈ ℂ, 𝑣 ∈ ℂ ↦ (𝑢 · 𝑣))(𝐺‘𝑧)) = ((((𝐹‘𝑧) − (𝐹‘𝐶)) / (𝑧 − 𝐶)) · (𝐺‘𝑧)))
195	55, 59, 194	syl2anc 584	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑧 ∈ ((𝑋 ∩ 𝑌) ∖ {𝐶})) → ((((𝐹‘𝑧) − (𝐹‘𝐶)) / (𝑧 − 𝐶))(𝑢 ∈ ℂ, 𝑣 ∈ ℂ ↦ (𝑢 · 𝑣))(𝐺‘𝑧)) = ((((𝐹‘𝑧) − (𝐹‘𝐶)) / (𝑧 − 𝐶)) · (𝐺‘𝑧)))
196	195	eqeq2d 2740	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑧 ∈ ((𝑋 ∩ 𝑌) ∖ {𝐶})) → (𝑤 = ((((𝐹‘𝑧) − (𝐹‘𝐶)) / (𝑧 − 𝐶))(𝑢 ∈ ℂ, 𝑣 ∈ ℂ ↦ (𝑢 · 𝑣))(𝐺‘𝑧)) ↔ 𝑤 = ((((𝐹‘𝑧) − (𝐹‘𝐶)) / (𝑧 − 𝐶)) · (𝐺‘𝑧))))
197	196	pm5.32da 579	. . . . . . . 8 ⊢ (𝜑 → ((𝑧 ∈ ((𝑋 ∩ 𝑌) ∖ {𝐶}) ∧ 𝑤 = ((((𝐹‘𝑧) − (𝐹‘𝐶)) / (𝑧 − 𝐶))(𝑢 ∈ ℂ, 𝑣 ∈ ℂ ↦ (𝑢 · 𝑣))(𝐺‘𝑧))) ↔ (𝑧 ∈ ((𝑋 ∩ 𝑌) ∖ {𝐶}) ∧ 𝑤 = ((((𝐹‘𝑧) − (𝐹‘𝐶)) / (𝑧 − 𝐶)) · (𝐺‘𝑧)))))
198	197	opabbidv 5158	. . . . . . 7 ⊢ (𝜑 → {⟨𝑧, 𝑤⟩ ∣ (𝑧 ∈ ((𝑋 ∩ 𝑌) ∖ {𝐶}) ∧ 𝑤 = ((((𝐹‘𝑧) − (𝐹‘𝐶)) / (𝑧 − 𝐶))(𝑢 ∈ ℂ, 𝑣 ∈ ℂ ↦ (𝑢 · 𝑣))(𝐺‘𝑧)))} = {⟨𝑧, 𝑤⟩ ∣ (𝑧 ∈ ((𝑋 ∩ 𝑌) ∖ {𝐶}) ∧ 𝑤 = ((((𝐹‘𝑧) − (𝐹‘𝐶)) / (𝑧 − 𝐶)) · (𝐺‘𝑧)))})
199		df-mpt 5174	. . . . . . 7 ⊢ (𝑧 ∈ ((𝑋 ∩ 𝑌) ∖ {𝐶}) ↦ ((((𝐹‘𝑧) − (𝐹‘𝐶)) / (𝑧 − 𝐶)) · (𝐺‘𝑧))) = {⟨𝑧, 𝑤⟩ ∣ (𝑧 ∈ ((𝑋 ∩ 𝑌) ∖ {𝐶}) ∧ 𝑤 = ((((𝐹‘𝑧) − (𝐹‘𝐶)) / (𝑧 − 𝐶)) · (𝐺‘𝑧)))}
200	198, 199	eqtr4di 2782	. . . . . 6 ⊢ (𝜑 → {⟨𝑧, 𝑤⟩ ∣ (𝑧 ∈ ((𝑋 ∩ 𝑌) ∖ {𝐶}) ∧ 𝑤 = ((((𝐹‘𝑧) − (𝐹‘𝐶)) / (𝑧 − 𝐶))(𝑢 ∈ ℂ, 𝑣 ∈ ℂ ↦ (𝑢 · 𝑣))(𝐺‘𝑧)))} = (𝑧 ∈ ((𝑋 ∩ 𝑌) ∖ {𝐶}) ↦ ((((𝐹‘𝑧) − (𝐹‘𝐶)) / (𝑧 − 𝐶)) · (𝐺‘𝑧))))
201	200	oveq1d 7364	. . . . 5 ⊢ (𝜑 → ({⟨𝑧, 𝑤⟩ ∣ (𝑧 ∈ ((𝑋 ∩ 𝑌) ∖ {𝐶}) ∧ 𝑤 = ((((𝐹‘𝑧) − (𝐹‘𝐶)) / (𝑧 − 𝐶))(𝑢 ∈ ℂ, 𝑣 ∈ ℂ ↦ (𝑢 · 𝑣))(𝐺‘𝑧)))} lim_ℂ 𝐶) = ((𝑧 ∈ ((𝑋 ∩ 𝑌) ∖ {𝐶}) ↦ ((((𝐹‘𝑧) − (𝐹‘𝐶)) / (𝑧 − 𝐶)) · (𝐺‘𝑧))) lim_ℂ 𝐶))
202	191, 193, 201	3eltr3d 2842	. . . 4 ⊢ (𝜑 → (𝐾 · (𝐺‘𝐶)) ∈ ((𝑧 ∈ ((𝑋 ∩ 𝑌) ∖ {𝐶}) ↦ ((((𝐹‘𝑧) − (𝐹‘𝐶)) / (𝑧 − 𝐶)) · (𝐺‘𝑧))) lim_ℂ 𝐶))
203	16	simprd 495	. . . . . . . 8 ⊢ (𝜑 → 𝐿 ∈ ((𝑧 ∈ (𝑌 ∖ {𝐶}) ↦ (((𝐺‘𝑧) − (𝐺‘𝐶)) / (𝑧 − 𝐶))) lim_ℂ 𝐶))
204	70	fmpttd 7049	. . . . . . . . . 10 ⊢ (𝜑 → (𝑧 ∈ (𝑌 ∖ {𝐶}) ↦ (((𝐺‘𝑧) − (𝐺‘𝐶)) / (𝑧 − 𝐶))):(𝑌 ∖ {𝐶})⟶ℂ)
205	64	ssdifssd 4098	. . . . . . . . . 10 ⊢ (𝜑 → (𝑌 ∖ {𝐶}) ⊆ ℂ)
206		eqid 2729	. . . . . . . . . 10 ⊢ (𝐽 ↾_t ((𝑌 ∖ {𝐶}) ∪ {𝐶})) = (𝐽 ↾_t ((𝑌 ∖ {𝐶}) ∪ {𝐶}))
207		undif1 4427	. . . . . . . . . . . . . . 15 ⊢ ((𝑌 ∖ {𝐶}) ∪ {𝐶}) = (𝑌 ∪ {𝐶})
208	207, 170	eqtrid 2776	. . . . . . . . . . . . . 14 ⊢ (𝜑 → ((𝑌 ∖ {𝐶}) ∪ {𝐶}) = 𝑌)
209	208	oveq2d 7365	. . . . . . . . . . . . 13 ⊢ (𝜑 → (𝐽 ↾_t ((𝑌 ∖ {𝐶}) ∪ {𝐶})) = (𝐽 ↾_t 𝑌))
210	209	fveq2d 6826	. . . . . . . . . . . 12 ⊢ (𝜑 → (int‘(𝐽 ↾_t ((𝑌 ∖ {𝐶}) ∪ {𝐶}))) = (int‘(𝐽 ↾_t 𝑌)))
211	210, 131	fveq12d 6829	. . . . . . . . . . 11 ⊢ (𝜑 → ((int‘(𝐽 ↾_t ((𝑌 ∖ {𝐶}) ∪ {𝐶})))‘(((𝑋 ∩ 𝑌) ∖ {𝐶}) ∪ {𝐶})) = ((int‘(𝐽 ↾_t 𝑌))‘(𝑋 ∩ 𝑌)))
212	167, 211	eleqtrrd 2831	. . . . . . . . . 10 ⊢ (𝜑 → 𝐶 ∈ ((int‘(𝐽 ↾_t ((𝑌 ∖ {𝐶}) ∪ {𝐶})))‘(((𝑋 ∩ 𝑌) ∖ {𝐶}) ∪ {𝐶})))
213	204, 62, 205, 3, 206, 212	limcres 25785	. . . . . . . . 9 ⊢ (𝜑 → (((𝑧 ∈ (𝑌 ∖ {𝐶}) ↦ (((𝐺‘𝑧) − (𝐺‘𝐶)) / (𝑧 − 𝐶))) ↾ ((𝑋 ∩ 𝑌) ∖ {𝐶})) lim_ℂ 𝐶) = ((𝑧 ∈ (𝑌 ∖ {𝐶}) ↦ (((𝐺‘𝑧) − (𝐺‘𝐶)) / (𝑧 − 𝐶))) lim_ℂ 𝐶))
214	62	resmptd 5991	. . . . . . . . . 10 ⊢ (𝜑 → ((𝑧 ∈ (𝑌 ∖ {𝐶}) ↦ (((𝐺‘𝑧) − (𝐺‘𝐶)) / (𝑧 − 𝐶))) ↾ ((𝑋 ∩ 𝑌) ∖ {𝐶})) = (𝑧 ∈ ((𝑋 ∩ 𝑌) ∖ {𝐶}) ↦ (((𝐺‘𝑧) − (𝐺‘𝐶)) / (𝑧 − 𝐶))))
215	214	oveq1d 7364	. . . . . . . . 9 ⊢ (𝜑 → (((𝑧 ∈ (𝑌 ∖ {𝐶}) ↦ (((𝐺‘𝑧) − (𝐺‘𝐶)) / (𝑧 − 𝐶))) ↾ ((𝑋 ∩ 𝑌) ∖ {𝐶})) lim_ℂ 𝐶) = ((𝑧 ∈ ((𝑋 ∩ 𝑌) ∖ {𝐶}) ↦ (((𝐺‘𝑧) − (𝐺‘𝐶)) / (𝑧 − 𝐶))) lim_ℂ 𝐶))
216	213, 215	eqtr3d 2766	. . . . . . . 8 ⊢ (𝜑 → ((𝑧 ∈ (𝑌 ∖ {𝐶}) ↦ (((𝐺‘𝑧) − (𝐺‘𝐶)) / (𝑧 − 𝐶))) lim_ℂ 𝐶) = ((𝑧 ∈ ((𝑋 ∩ 𝑌) ∖ {𝐶}) ↦ (((𝐺‘𝑧) − (𝐺‘𝐶)) / (𝑧 − 𝐶))) lim_ℂ 𝐶))
217	203, 216	eleqtrd 2830	. . . . . . 7 ⊢ (𝜑 → 𝐿 ∈ ((𝑧 ∈ ((𝑋 ∩ 𝑌) ∖ {𝐶}) ↦ (((𝐺‘𝑧) − (𝐺‘𝐶)) / (𝑧 − 𝐶))) lim_ℂ 𝐶))
218	84, 5	sstrd 3946	. . . . . . . . . 10 ⊢ (𝜑 → (𝑋 ∩ 𝑌) ⊆ ℂ)
219		cncfmptc 24803	. . . . . . . . . 10 ⊢ (((𝐹‘𝐶) ∈ ℂ ∧ (𝑋 ∩ 𝑌) ⊆ ℂ ∧ ℂ ⊆ ℂ) → (𝑧 ∈ (𝑋 ∩ 𝑌) ↦ (𝐹‘𝐶)) ∈ ((𝑋 ∩ 𝑌)–cn→ℂ))
220	43, 218, 73, 219	syl3anc 1373	. . . . . . . . 9 ⊢ (𝜑 → (𝑧 ∈ (𝑋 ∩ 𝑌) ↦ (𝐹‘𝐶)) ∈ ((𝑋 ∩ 𝑌)–cn→ℂ))
221		eqidd 2730	. . . . . . . . 9 ⊢ (𝑧 = 𝐶 → (𝐹‘𝐶) = (𝐹‘𝐶))
222	220, 127, 221	cnmptlimc 25789	. . . . . . . 8 ⊢ (𝜑 → (𝐹‘𝐶) ∈ ((𝑧 ∈ (𝑋 ∩ 𝑌) ↦ (𝐹‘𝐶)) lim_ℂ 𝐶))
223	43	adantr 480	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑧 ∈ (𝑋 ∩ 𝑌)) → (𝐹‘𝐶) ∈ ℂ)
224	223	fmpttd 7049	. . . . . . . . . 10 ⊢ (𝜑 → (𝑧 ∈ (𝑋 ∩ 𝑌) ↦ (𝐹‘𝐶)):(𝑋 ∩ 𝑌)⟶ℂ)
225	224	limcdif 25775	. . . . . . . . 9 ⊢ (𝜑 → ((𝑧 ∈ (𝑋 ∩ 𝑌) ↦ (𝐹‘𝐶)) lim_ℂ 𝐶) = (((𝑧 ∈ (𝑋 ∩ 𝑌) ↦ (𝐹‘𝐶)) ↾ ((𝑋 ∩ 𝑌) ∖ {𝐶})) lim_ℂ 𝐶))
226		resmpt 5988	. . . . . . . . . . 11 ⊢ (((𝑋 ∩ 𝑌) ∖ {𝐶}) ⊆ (𝑋 ∩ 𝑌) → ((𝑧 ∈ (𝑋 ∩ 𝑌) ↦ (𝐹‘𝐶)) ↾ ((𝑋 ∩ 𝑌) ∖ {𝐶})) = (𝑧 ∈ ((𝑋 ∩ 𝑌) ∖ {𝐶}) ↦ (𝐹‘𝐶)))
227	146, 226	mp1i 13	. . . . . . . . . 10 ⊢ (𝜑 → ((𝑧 ∈ (𝑋 ∩ 𝑌) ↦ (𝐹‘𝐶)) ↾ ((𝑋 ∩ 𝑌) ∖ {𝐶})) = (𝑧 ∈ ((𝑋 ∩ 𝑌) ∖ {𝐶}) ↦ (𝐹‘𝐶)))
228	227	oveq1d 7364	. . . . . . . . 9 ⊢ (𝜑 → (((𝑧 ∈ (𝑋 ∩ 𝑌) ↦ (𝐹‘𝐶)) ↾ ((𝑋 ∩ 𝑌) ∖ {𝐶})) lim_ℂ 𝐶) = ((𝑧 ∈ ((𝑋 ∩ 𝑌) ∖ {𝐶}) ↦ (𝐹‘𝐶)) lim_ℂ 𝐶))
229	225, 228	eqtrd 2764	. . . . . . . 8 ⊢ (𝜑 → ((𝑧 ∈ (𝑋 ∩ 𝑌) ↦ (𝐹‘𝐶)) lim_ℂ 𝐶) = ((𝑧 ∈ ((𝑋 ∩ 𝑌) ∖ {𝐶}) ↦ (𝐹‘𝐶)) lim_ℂ 𝐶))
230	222, 229	eleqtrd 2830	. . . . . . 7 ⊢ (𝜑 → (𝐹‘𝐶) ∈ ((𝑧 ∈ ((𝑋 ∩ 𝑌) ∖ {𝐶}) ↦ (𝐹‘𝐶)) lim_ℂ 𝐶))
231	5, 13, 14	dvcl 25798	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝐶(𝑆 D 𝐺)𝐿) → 𝐿 ∈ ℂ)
232	11, 231	mpdan 687	. . . . . . . . 9 ⊢ (𝜑 → 𝐿 ∈ ℂ)
233	232, 43	opelxpd 5658	. . . . . . . 8 ⊢ (𝜑 → ⟨𝐿, (𝐹‘𝐶)⟩ ∈ (ℂ × ℂ))
234	185	cncnpi 23163	. . . . . . . 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 25791	. . . . . 6 ⊢ (𝜑 → (𝐿(𝑢 ∈ ℂ, 𝑣 ∈ ℂ ↦ (𝑢 · 𝑣))(𝐹‘𝐶)) ∈ ((𝑧 ∈ ((𝑋 ∩ 𝑌) ∖ {𝐶}) ↦ ((((𝐺‘𝑧) − (𝐺‘𝐶)) / (𝑧 − 𝐶))(𝑢 ∈ ℂ, 𝑣 ∈ ℂ ↦ (𝑢 · 𝑣))(𝐹‘𝐶))) lim_ℂ 𝐶))
237		df-mpt 5174	. . . . . . 7 ⊢ (𝑧 ∈ ((𝑋 ∩ 𝑌) ∖ {𝐶}) ↦ ((((𝐺‘𝑧) − (𝐺‘𝐶)) / (𝑧 − 𝐶))(𝑢 ∈ ℂ, 𝑣 ∈ ℂ ↦ (𝑢 · 𝑣))(𝐹‘𝐶))) = {⟨𝑧, 𝑤⟩ ∣ (𝑧 ∈ ((𝑋 ∩ 𝑌) ∖ {𝐶}) ∧ 𝑤 = ((((𝐺‘𝑧) − (𝐺‘𝐶)) / (𝑧 − 𝐶))(𝑢 ∈ ℂ, 𝑣 ∈ ℂ ↦ (𝑢 · 𝑣))(𝐹‘𝐶)))}
238	237	oveq1i 7359	. . . . . 6 ⊢ ((𝑧 ∈ ((𝑋 ∩ 𝑌) ∖ {𝐶}) ↦ ((((𝐺‘𝑧) − (𝐺‘𝐶)) / (𝑧 − 𝐶))(𝑢 ∈ ℂ, 𝑣 ∈ ℂ ↦ (𝑢 · 𝑣))(𝐹‘𝐶))) lim_ℂ 𝐶) = ({⟨𝑧, 𝑤⟩ ∣ (𝑧 ∈ ((𝑋 ∩ 𝑌) ∖ {𝐶}) ∧ 𝑤 = ((((𝐺‘𝑧) − (𝐺‘𝐶)) / (𝑧 − 𝐶))(𝑢 ∈ ℂ, 𝑣 ∈ ℂ ↦ (𝑢 · 𝑣))(𝐹‘𝐶)))} lim_ℂ 𝐶)
239	236, 238	eleqtrdi 2838	. . . . 5 ⊢ (𝜑 → (𝐿(𝑢 ∈ ℂ, 𝑣 ∈ ℂ ↦ (𝑢 · 𝑣))(𝐹‘𝐶)) ∈ ({⟨𝑧, 𝑤⟩ ∣ (𝑧 ∈ ((𝑋 ∩ 𝑌) ∖ {𝐶}) ∧ 𝑤 = ((((𝐺‘𝑧) − (𝐺‘𝐶)) / (𝑧 − 𝐶))(𝑢 ∈ ℂ, 𝑣 ∈ ℂ ↦ (𝑢 · 𝑣))(𝐹‘𝐶)))} lim_ℂ 𝐶))
240		ovmpot 7510	. . . . . 6 ⊢ ((𝐿 ∈ ℂ ∧ (𝐹‘𝐶) ∈ ℂ) → (𝐿(𝑢 ∈ ℂ, 𝑣 ∈ ℂ ↦ (𝑢 · 𝑣))(𝐹‘𝐶)) = (𝐿 · (𝐹‘𝐶)))
241	232, 43, 240	syl2anc 584	. . . . 5 ⊢ (𝜑 → (𝐿(𝑢 ∈ ℂ, 𝑣 ∈ ℂ ↦ (𝑢 · 𝑣))(𝐹‘𝐶)) = (𝐿 · (𝐹‘𝐶)))
242	42	adantr 480	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑧 ∈ ((𝑋 ∩ 𝑌) ∖ {𝐶})) → 𝐶 ∈ 𝑋)
243	32, 242	ffvelcdmd 7019	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑧 ∈ ((𝑋 ∩ 𝑌) ∖ {𝐶})) → (𝐹‘𝐶) ∈ ℂ)
244		ovmpot 7510	. . . . . . . . . . 11 ⊢ (((((𝐺‘𝑧) − (𝐺‘𝐶)) / (𝑧 − 𝐶)) ∈ ℂ ∧ (𝐹‘𝐶) ∈ ℂ) → ((((𝐺‘𝑧) − (𝐺‘𝐶)) / (𝑧 − 𝐶))(𝑢 ∈ ℂ, 𝑣 ∈ ℂ ↦ (𝑢 · 𝑣))(𝐹‘𝐶)) = ((((𝐺‘𝑧) − (𝐺‘𝐶)) / (𝑧 − 𝐶)) · (𝐹‘𝐶)))
245	71, 243, 244	syl2anc 584	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑧 ∈ ((𝑋 ∩ 𝑌) ∖ {𝐶})) → ((((𝐺‘𝑧) − (𝐺‘𝐶)) / (𝑧 − 𝐶))(𝑢 ∈ ℂ, 𝑣 ∈ ℂ ↦ (𝑢 · 𝑣))(𝐹‘𝐶)) = ((((𝐺‘𝑧) − (𝐺‘𝐶)) / (𝑧 − 𝐶)) · (𝐹‘𝐶)))
246	245	eqeq2d 2740	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑧 ∈ ((𝑋 ∩ 𝑌) ∖ {𝐶})) → (𝑤 = ((((𝐺‘𝑧) − (𝐺‘𝐶)) / (𝑧 − 𝐶))(𝑢 ∈ ℂ, 𝑣 ∈ ℂ ↦ (𝑢 · 𝑣))(𝐹‘𝐶)) ↔ 𝑤 = ((((𝐺‘𝑧) − (𝐺‘𝐶)) / (𝑧 − 𝐶)) · (𝐹‘𝐶))))
247	246	pm5.32da 579	. . . . . . . 8 ⊢ (𝜑 → ((𝑧 ∈ ((𝑋 ∩ 𝑌) ∖ {𝐶}) ∧ 𝑤 = ((((𝐺‘𝑧) − (𝐺‘𝐶)) / (𝑧 − 𝐶))(𝑢 ∈ ℂ, 𝑣 ∈ ℂ ↦ (𝑢 · 𝑣))(𝐹‘𝐶))) ↔ (𝑧 ∈ ((𝑋 ∩ 𝑌) ∖ {𝐶}) ∧ 𝑤 = ((((𝐺‘𝑧) − (𝐺‘𝐶)) / (𝑧 − 𝐶)) · (𝐹‘𝐶)))))
248	247	opabbidv 5158	. . . . . . 7 ⊢ (𝜑 → {⟨𝑧, 𝑤⟩ ∣ (𝑧 ∈ ((𝑋 ∩ 𝑌) ∖ {𝐶}) ∧ 𝑤 = ((((𝐺‘𝑧) − (𝐺‘𝐶)) / (𝑧 − 𝐶))(𝑢 ∈ ℂ, 𝑣 ∈ ℂ ↦ (𝑢 · 𝑣))(𝐹‘𝐶)))} = {⟨𝑧, 𝑤⟩ ∣ (𝑧 ∈ ((𝑋 ∩ 𝑌) ∖ {𝐶}) ∧ 𝑤 = ((((𝐺‘𝑧) − (𝐺‘𝐶)) / (𝑧 − 𝐶)) · (𝐹‘𝐶)))})
249		df-mpt 5174	. . . . . . 7 ⊢ (𝑧 ∈ ((𝑋 ∩ 𝑌) ∖ {𝐶}) ↦ ((((𝐺‘𝑧) − (𝐺‘𝐶)) / (𝑧 − 𝐶)) · (𝐹‘𝐶))) = {⟨𝑧, 𝑤⟩ ∣ (𝑧 ∈ ((𝑋 ∩ 𝑌) ∖ {𝐶}) ∧ 𝑤 = ((((𝐺‘𝑧) − (𝐺‘𝐶)) / (𝑧 − 𝐶)) · (𝐹‘𝐶)))}
250	248, 249	eqtr4di 2782	. . . . . 6 ⊢ (𝜑 → {⟨𝑧, 𝑤⟩ ∣ (𝑧 ∈ ((𝑋 ∩ 𝑌) ∖ {𝐶}) ∧ 𝑤 = ((((𝐺‘𝑧) − (𝐺‘𝐶)) / (𝑧 − 𝐶))(𝑢 ∈ ℂ, 𝑣 ∈ ℂ ↦ (𝑢 · 𝑣))(𝐹‘𝐶)))} = (𝑧 ∈ ((𝑋 ∩ 𝑌) ∖ {𝐶}) ↦ ((((𝐺‘𝑧) − (𝐺‘𝐶)) / (𝑧 − 𝐶)) · (𝐹‘𝐶))))
251	250	oveq1d 7364	. . . . 5 ⊢ (𝜑 → ({⟨𝑧, 𝑤⟩ ∣ (𝑧 ∈ ((𝑋 ∩ 𝑌) ∖ {𝐶}) ∧ 𝑤 = ((((𝐺‘𝑧) − (𝐺‘𝐶)) / (𝑧 − 𝐶))(𝑢 ∈ ℂ, 𝑣 ∈ ℂ ↦ (𝑢 · 𝑣))(𝐹‘𝐶)))} lim_ℂ 𝐶) = ((𝑧 ∈ ((𝑋 ∩ 𝑌) ∖ {𝐶}) ↦ ((((𝐺‘𝑧) − (𝐺‘𝐶)) / (𝑧 − 𝐶)) · (𝐹‘𝐶))) lim_ℂ 𝐶))
252	239, 241, 251	3eltr3d 2842	. . . 4 ⊢ (𝜑 → (𝐿 · (𝐹‘𝐶)) ∈ ((𝑧 ∈ ((𝑋 ∩ 𝑌) ∖ {𝐶}) ↦ ((((𝐺‘𝑧) − (𝐺‘𝐶)) / (𝑧 − 𝐶)) · (𝐹‘𝐶))) lim_ℂ 𝐶))
253	3	addcn 24752	. . . . 5 ⊢ + ∈ ((𝐽 ×_t 𝐽) Cn 𝐽)
254	182, 183	mulcld 11135	. . . . . 6 ⊢ (𝜑 → (𝐾 · (𝐺‘𝐶)) ∈ ℂ)
255	232, 43	mulcld 11135	. . . . . 6 ⊢ (𝜑 → (𝐿 · (𝐹‘𝐶)) ∈ ℂ)
256	254, 255	opelxpd 5658	. . . . 5 ⊢ (𝜑 → ⟨(𝐾 · (𝐺‘𝐶)), (𝐿 · (𝐹‘𝐶))⟩ ∈ (ℂ × ℂ))
257	185	cncnpi 23163	. . . . 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 25791	. . 3 ⊢ (𝜑 → ((𝐾 · (𝐺‘𝐶)) + (𝐿 · (𝐹‘𝐶))) ∈ ((𝑧 ∈ ((𝑋 ∩ 𝑌) ∖ {𝐶}) ↦ (((((𝐹‘𝑧) − (𝐹‘𝐶)) / (𝑧 − 𝐶)) · (𝐺‘𝑧)) + ((((𝐺‘𝑧) − (𝐺‘𝐶)) / (𝑧 − 𝐶)) · (𝐹‘𝐶)))) lim_ℂ 𝐶))
260	37, 243	subcld 11475	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑧 ∈ ((𝑋 ∩ 𝑌) ∖ {𝐶})) → ((𝐹‘𝑧) − (𝐹‘𝐶)) ∈ ℂ)
261	260, 59	mulcld 11135	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑧 ∈ ((𝑋 ∩ 𝑌) ∖ {𝐶})) → (((𝐹‘𝑧) − (𝐹‘𝐶)) · (𝐺‘𝑧)) ∈ ℂ)
262	69	adantr 480	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑧 ∈ ((𝑋 ∩ 𝑌) ∖ {𝐶})) → 𝐶 ∈ 𝑌)
263	56, 262	ffvelcdmd 7019	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑧 ∈ ((𝑋 ∩ 𝑌) ∖ {𝐶})) → (𝐺‘𝐶) ∈ ℂ)
264	59, 263	subcld 11475	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑧 ∈ ((𝑋 ∩ 𝑌) ∖ {𝐶})) → ((𝐺‘𝑧) − (𝐺‘𝐶)) ∈ ℂ)
265	264, 243	mulcld 11135	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑧 ∈ ((𝑋 ∩ 𝑌) ∖ {𝐶})) → (((𝐺‘𝑧) − (𝐺‘𝐶)) · (𝐹‘𝐶)) ∈ ℂ)
266	47, 242	sseldd 3936	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑧 ∈ ((𝑋 ∩ 𝑌) ∖ {𝐶})) → 𝐶 ∈ ℂ)
267	48, 266	subcld 11475	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑧 ∈ ((𝑋 ∩ 𝑌) ∖ {𝐶})) → (𝑧 − 𝐶) ∈ ℂ)
268	261, 265, 267, 54	divdird 11938	. . . . . 6 ⊢ ((𝜑 ∧ 𝑧 ∈ ((𝑋 ∩ 𝑌) ∖ {𝐶})) → (((((𝐹‘𝑧) − (𝐹‘𝐶)) · (𝐺‘𝑧)) + (((𝐺‘𝑧) − (𝐺‘𝐶)) · (𝐹‘𝐶))) / (𝑧 − 𝐶)) = (((((𝐹‘𝑧) − (𝐹‘𝐶)) · (𝐺‘𝑧)) / (𝑧 − 𝐶)) + ((((𝐺‘𝑧) − (𝐺‘𝐶)) · (𝐹‘𝐶)) / (𝑧 − 𝐶))))
269	37, 59	mulcld 11135	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑧 ∈ ((𝑋 ∩ 𝑌) ∖ {𝐶})) → ((𝐹‘𝑧) · (𝐺‘𝑧)) ∈ ℂ)
270	243, 59	mulcld 11135	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑧 ∈ ((𝑋 ∩ 𝑌) ∖ {𝐶})) → ((𝐹‘𝐶) · (𝐺‘𝑧)) ∈ ℂ)
271	243, 263	mulcld 11135	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑧 ∈ ((𝑋 ∩ 𝑌) ∖ {𝐶})) → ((𝐹‘𝐶) · (𝐺‘𝐶)) ∈ ℂ)
272	269, 270, 271	npncand 11499	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑧 ∈ ((𝑋 ∩ 𝑌) ∖ {𝐶})) → ((((𝐹‘𝑧) · (𝐺‘𝑧)) − ((𝐹‘𝐶) · (𝐺‘𝑧))) + (((𝐹‘𝐶) · (𝐺‘𝑧)) − ((𝐹‘𝐶) · (𝐺‘𝐶)))) = (((𝐹‘𝑧) · (𝐺‘𝑧)) − ((𝐹‘𝐶) · (𝐺‘𝐶))))
273	37, 243, 59	subdird 11577	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑧 ∈ ((𝑋 ∩ 𝑌) ∖ {𝐶})) → (((𝐹‘𝑧) − (𝐹‘𝐶)) · (𝐺‘𝑧)) = (((𝐹‘𝑧) · (𝐺‘𝑧)) − ((𝐹‘𝐶) · (𝐺‘𝑧))))
274	264, 243	mulcomd 11136	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑧 ∈ ((𝑋 ∩ 𝑌) ∖ {𝐶})) → (((𝐺‘𝑧) − (𝐺‘𝐶)) · (𝐹‘𝐶)) = ((𝐹‘𝐶) · ((𝐺‘𝑧) − (𝐺‘𝐶))))
275	243, 59, 263	subdid 11576	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑧 ∈ ((𝑋 ∩ 𝑌) ∖ {𝐶})) → ((𝐹‘𝐶) · ((𝐺‘𝑧) − (𝐺‘𝐶))) = (((𝐹‘𝐶) · (𝐺‘𝑧)) − ((𝐹‘𝐶) · (𝐺‘𝐶))))
276	274, 275	eqtrd 2764	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑧 ∈ ((𝑋 ∩ 𝑌) ∖ {𝐶})) → (((𝐺‘𝑧) − (𝐺‘𝐶)) · (𝐹‘𝐶)) = (((𝐹‘𝐶) · (𝐺‘𝑧)) − ((𝐹‘𝐶) · (𝐺‘𝐶))))
277	273, 276	oveq12d 7367	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑧 ∈ ((𝑋 ∩ 𝑌) ∖ {𝐶})) → ((((𝐹‘𝑧) − (𝐹‘𝐶)) · (𝐺‘𝑧)) + (((𝐺‘𝑧) − (𝐺‘𝐶)) · (𝐹‘𝐶))) = ((((𝐹‘𝑧) · (𝐺‘𝑧)) − ((𝐹‘𝐶) · (𝐺‘𝑧))) + (((𝐹‘𝐶) · (𝐺‘𝑧)) − ((𝐹‘𝐶) · (𝐺‘𝐶)))))
278	6	ffnd 6653	. . . . . . . . . . . 12 ⊢ (𝜑 → 𝐹 Fn 𝑋)
279	278	adantr 480	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑧 ∈ ((𝑋 ∩ 𝑌) ∖ {𝐶})) → 𝐹 Fn 𝑋)
280	13	ffnd 6653	. . . . . . . . . . . 12 ⊢ (𝜑 → 𝐺 Fn 𝑌)
281	280	adantr 480	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑧 ∈ ((𝑋 ∩ 𝑌) ∖ {𝐶})) → 𝐺 Fn 𝑌)
282		ssexg 5262	. . . . . . . . . . . . 13 ⊢ ((𝑋 ⊆ ℂ ∧ ℂ ∈ V) → 𝑋 ∈ V)
283	46, 110, 282	sylancl 586	. . . . . . . . . . . 12 ⊢ (𝜑 → 𝑋 ∈ V)
284	283	adantr 480	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑧 ∈ ((𝑋 ∩ 𝑌) ∖ {𝐶})) → 𝑋 ∈ V)
285		ssexg 5262	. . . . . . . . . . . . 13 ⊢ ((𝑌 ⊆ ℂ ∧ ℂ ∈ V) → 𝑌 ∈ V)
286	64, 110, 285	sylancl 586	. . . . . . . . . . . 12 ⊢ (𝜑 → 𝑌 ∈ V)
287	286	adantr 480	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑧 ∈ ((𝑋 ∩ 𝑌) ∖ {𝐶})) → 𝑌 ∈ V)
288		eqid 2729	. . . . . . . . . . 11 ⊢ (𝑋 ∩ 𝑌) = (𝑋 ∩ 𝑌)
289		eqidd 2730	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑧 ∈ ((𝑋 ∩ 𝑌) ∖ {𝐶})) ∧ 𝑧 ∈ 𝑋) → (𝐹‘𝑧) = (𝐹‘𝑧))
290		eqidd 2730	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑧 ∈ ((𝑋 ∩ 𝑌) ∖ {𝐶})) ∧ 𝑧 ∈ 𝑌) → (𝐺‘𝑧) = (𝐺‘𝑧))
291	279, 281, 284, 287, 288, 289, 290	ofval 7624	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑧 ∈ ((𝑋 ∩ 𝑌) ∖ {𝐶})) ∧ 𝑧 ∈ (𝑋 ∩ 𝑌)) → ((𝐹 ∘_f · 𝐺)‘𝑧) = ((𝐹‘𝑧) · (𝐺‘𝑧)))
292	35, 291	mpdan 687	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑧 ∈ ((𝑋 ∩ 𝑌) ∖ {𝐶})) → ((𝐹 ∘_f · 𝐺)‘𝑧) = ((𝐹‘𝑧) · (𝐺‘𝑧)))
293		eqidd 2730	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑧 ∈ ((𝑋 ∩ 𝑌) ∖ {𝐶})) ∧ 𝐶 ∈ 𝑋) → (𝐹‘𝐶) = (𝐹‘𝐶))
294		eqidd 2730	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑧 ∈ ((𝑋 ∩ 𝑌) ∖ {𝐶})) ∧ 𝐶 ∈ 𝑌) → (𝐺‘𝐶) = (𝐺‘𝐶))
295	279, 281, 284, 287, 288, 293, 294	ofval 7624	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑧 ∈ ((𝑋 ∩ 𝑌) ∖ {𝐶})) ∧ 𝐶 ∈ (𝑋 ∩ 𝑌)) → ((𝐹 ∘_f · 𝐺)‘𝐶) = ((𝐹‘𝐶) · (𝐺‘𝐶)))
296	127, 295	mpidan 689	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑧 ∈ ((𝑋 ∩ 𝑌) ∖ {𝐶})) → ((𝐹 ∘_f · 𝐺)‘𝐶) = ((𝐹‘𝐶) · (𝐺‘𝐶)))
297	292, 296	oveq12d 7367	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑧 ∈ ((𝑋 ∩ 𝑌) ∖ {𝐶})) → (((𝐹 ∘_f · 𝐺)‘𝑧) − ((𝐹 ∘_f · 𝐺)‘𝐶)) = (((𝐹‘𝑧) · (𝐺‘𝑧)) − ((𝐹‘𝐶) · (𝐺‘𝐶))))
298	272, 277, 297	3eqtr4d 2774	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑧 ∈ ((𝑋 ∩ 𝑌) ∖ {𝐶})) → ((((𝐹‘𝑧) − (𝐹‘𝐶)) · (𝐺‘𝑧)) + (((𝐺‘𝑧) − (𝐺‘𝐶)) · (𝐹‘𝐶))) = (((𝐹 ∘_f · 𝐺)‘𝑧) − ((𝐹 ∘_f · 𝐺)‘𝐶)))
299	298	oveq1d 7364	. . . . . 6 ⊢ ((𝜑 ∧ 𝑧 ∈ ((𝑋 ∩ 𝑌) ∖ {𝐶})) → (((((𝐹‘𝑧) − (𝐹‘𝐶)) · (𝐺‘𝑧)) + (((𝐺‘𝑧) − (𝐺‘𝐶)) · (𝐹‘𝐶))) / (𝑧 − 𝐶)) = ((((𝐹 ∘_f · 𝐺)‘𝑧) − ((𝐹 ∘_f · 𝐺)‘𝐶)) / (𝑧 − 𝐶)))
300	260, 59, 267, 54	div23d 11937	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑧 ∈ ((𝑋 ∩ 𝑌) ∖ {𝐶})) → ((((𝐹‘𝑧) − (𝐹‘𝐶)) · (𝐺‘𝑧)) / (𝑧 − 𝐶)) = ((((𝐹‘𝑧) − (𝐹‘𝐶)) / (𝑧 − 𝐶)) · (𝐺‘𝑧)))
301	264, 243, 267, 54	div23d 11937	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑧 ∈ ((𝑋 ∩ 𝑌) ∖ {𝐶})) → ((((𝐺‘𝑧) − (𝐺‘𝐶)) · (𝐹‘𝐶)) / (𝑧 − 𝐶)) = ((((𝐺‘𝑧) − (𝐺‘𝐶)) / (𝑧 − 𝐶)) · (𝐹‘𝐶)))
302	300, 301	oveq12d 7367	. . . . . 6 ⊢ ((𝜑 ∧ 𝑧 ∈ ((𝑋 ∩ 𝑌) ∖ {𝐶})) → (((((𝐹‘𝑧) − (𝐹‘𝐶)) · (𝐺‘𝑧)) / (𝑧 − 𝐶)) + ((((𝐺‘𝑧) − (𝐺‘𝐶)) · (𝐹‘𝐶)) / (𝑧 − 𝐶))) = (((((𝐹‘𝑧) − (𝐹‘𝐶)) / (𝑧 − 𝐶)) · (𝐺‘𝑧)) + ((((𝐺‘𝑧) − (𝐺‘𝐶)) / (𝑧 − 𝐶)) · (𝐹‘𝐶))))
303	268, 299, 302	3eqtr3d 2772	. . . . 5 ⊢ ((𝜑 ∧ 𝑧 ∈ ((𝑋 ∩ 𝑌) ∖ {𝐶})) → ((((𝐹 ∘_f · 𝐺)‘𝑧) − ((𝐹 ∘_f · 𝐺)‘𝐶)) / (𝑧 − 𝐶)) = (((((𝐹‘𝑧) − (𝐹‘𝐶)) / (𝑧 − 𝐶)) · (𝐺‘𝑧)) + ((((𝐺‘𝑧) − (𝐺‘𝐶)) / (𝑧 − 𝐶)) · (𝐹‘𝐶))))
304	303	mpteq2dva 5185	. . . 4 ⊢ (𝜑 → (𝑧 ∈ ((𝑋 ∩ 𝑌) ∖ {𝐶}) ↦ ((((𝐹 ∘_f · 𝐺)‘𝑧) − ((𝐹 ∘_f · 𝐺)‘𝐶)) / (𝑧 − 𝐶))) = (𝑧 ∈ ((𝑋 ∩ 𝑌) ∖ {𝐶}) ↦ (((((𝐹‘𝑧) − (𝐹‘𝐶)) / (𝑧 − 𝐶)) · (𝐺‘𝑧)) + ((((𝐺‘𝑧) − (𝐺‘𝐶)) / (𝑧 − 𝐶)) · (𝐹‘𝐶)))))
305	304	oveq1d 7364	. . 3 ⊢ (𝜑 → ((𝑧 ∈ ((𝑋 ∩ 𝑌) ∖ {𝐶}) ↦ ((((𝐹 ∘_f · 𝐺)‘𝑧) − ((𝐹 ∘_f · 𝐺)‘𝐶)) / (𝑧 − 𝐶))) lim_ℂ 𝐶) = ((𝑧 ∈ ((𝑋 ∩ 𝑌) ∖ {𝐶}) ↦ (((((𝐹‘𝑧) − (𝐹‘𝐶)) / (𝑧 − 𝐶)) · (𝐺‘𝑧)) + ((((𝐺‘𝑧) − (𝐺‘𝐶)) / (𝑧 − 𝐶)) · (𝐹‘𝐶)))) lim_ℂ 𝐶))
306	259, 305	eleqtrrd 2831	. 2 ⊢ (𝜑 → ((𝐾 · (𝐺‘𝐶)) + (𝐿 · (𝐹‘𝐶))) ∈ ((𝑧 ∈ ((𝑋 ∩ 𝑌) ∖ {𝐶}) ↦ ((((𝐹 ∘_f · 𝐺)‘𝑧) − ((𝐹 ∘_f · 𝐺)‘𝐶)) / (𝑧 − 𝐶))) lim_ℂ 𝐶))
307		eqid 2729	. . 3 ⊢ (𝑧 ∈ ((𝑋 ∩ 𝑌) ∖ {𝐶}) ↦ ((((𝐹 ∘_f · 𝐺)‘𝑧) − ((𝐹 ∘_f · 𝐺)‘𝐶)) / (𝑧 − 𝐶))) = (𝑧 ∈ ((𝑋 ∩ 𝑌) ∖ {𝐶}) ↦ ((((𝐹 ∘_f · 𝐺)‘𝑧) − ((𝐹 ∘_f · 𝐺)‘𝐶)) / (𝑧 − 𝐶)))
308		mulcl 11093	. . . . 5 ⊢ ((𝑥 ∈ ℂ ∧ 𝑦 ∈ ℂ) → (𝑥 · 𝑦) ∈ ℂ)
309	308	adantl 481	. . . 4 ⊢ ((𝜑 ∧ (𝑥 ∈ ℂ ∧ 𝑦 ∈ ℂ)) → (𝑥 · 𝑦) ∈ ℂ)
310	309, 6, 13, 283, 286, 288	off 7631	. . 3 ⊢ (𝜑 → (𝐹 ∘_f · 𝐺):(𝑋 ∩ 𝑌)⟶ℂ)
311	2, 3, 307, 5, 310, 84	eldv 25797	. 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 2109 ≠ wne 2925 Vcvv 3436 ∖ cdif 3900 ∪ cun 3901 ∩ cin 3902 ⊆ wss 3903 {csn 4577 ⟨cop 4583 ∪ cuni 4858 class class class wbr 5092 {copab 5154 ↦ cmpt 5173 × cxp 5617 dom cdm 5619 ↾ cres 5621 Rel wrel 5624 Fn wfn 6477 ⟶wf 6478 ‘cfv 6482 (class class class)co 7349 ∈ cmpo 7351 ∘_f cof 7611 ℂcc 11007 + caddc 11012 · cmul 11014 − cmin 11347 / cdiv 11777 ↾_t crest 17324 TopOpenctopn 17325 ℂ_fldccnfld 21261 Topctop 22778 TopOnctopon 22795 intcnt 22902 Cn ccn 23109 CnP ccnp 23110 ×_t ctx 23445 –cn→ccncf 24767 lim_ℂ climc 25761 D cdv 25762

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 2008 ax-8 2111 ax-9 2119 ax-10 2142 ax-11 2158 ax-12 2178 ax-ext 2701 ax-rep 5218 ax-sep 5235 ax-nul 5245 ax-pow 5304 ax-pr 5371 ax-un 7671 ax-cnex 11065 ax-resscn 11066 ax-1cn 11067 ax-icn 11068 ax-addcl 11069 ax-addrcl 11070 ax-mulcl 11071 ax-mulrcl 11072 ax-mulcom 11073 ax-addass 11074 ax-mulass 11075 ax-distr 11076 ax-i2m1 11077 ax-1ne0 11078 ax-1rid 11079 ax-rnegex 11080 ax-rrecex 11081 ax-cnre 11082 ax-pre-lttri 11083 ax-pre-lttrn 11084 ax-pre-ltadd 11085 ax-pre-mulgt0 11086 ax-pre-sup 11087 ax-addf 11088

This theorem depends on definitions: df-bi 207 df-an 396 df-or 848 df-3or 1087 df-3an 1088 df-tru 1543 df-fal 1553 df-ex 1780 df-nf 1784 df-sb 2066 df-mo 2533 df-eu 2562 df-clab 2708 df-cleq 2721 df-clel 2803 df-nfc 2878 df-ne 2926 df-nel 3030 df-ral 3045 df-rex 3054 df-rmo 3343 df-reu 3344 df-rab 3395 df-v 3438 df-sbc 3743 df-csb 3852 df-dif 3906 df-un 3908 df-in 3910 df-ss 3920 df-pss 3923 df-nul 4285 df-if 4477 df-pw 4553 df-sn 4578 df-pr 4580 df-tp 4582 df-op 4584 df-uni 4859 df-int 4897 df-iun 4943 df-iin 4944 df-br 5093 df-opab 5155 df-mpt 5174 df-tr 5200 df-id 5514 df-eprel 5519 df-po 5527 df-so 5528 df-fr 5572 df-se 5573 df-we 5574 df-xp 5625 df-rel 5626 df-cnv 5627 df-co 5628 df-dm 5629 df-rn 5630 df-res 5631 df-ima 5632 df-pred 6249 df-ord 6310 df-on 6311 df-lim 6312 df-suc 6313 df-iota 6438 df-fun 6484 df-fn 6485 df-f 6486 df-f1 6487 df-fo 6488 df-f1o 6489 df-fv 6490 df-isom 6491 df-riota 7306 df-ov 7352 df-oprab 7353 df-mpo 7354 df-of 7613 df-om 7800 df-1st 7924 df-2nd 7925 df-supp 8094 df-frecs 8214 df-wrecs 8245 df-recs 8294 df-rdg 8332 df-1o 8388 df-2o 8389 df-er 8625 df-map 8755 df-pm 8756 df-ixp 8825 df-en 8873 df-dom 8874 df-sdom 8875 df-fin 8876 df-fsupp 9252 df-fi 9301 df-sup 9332 df-inf 9333 df-oi 9402 df-card 9835 df-pnf 11151 df-mnf 11152 df-xr 11153 df-ltxr 11154 df-le 11155 df-sub 11349 df-neg 11350 df-div 11778 df-nn 12129 df-2 12191 df-3 12192 df-4 12193 df-5 12194 df-6 12195 df-7 12196 df-8 12197 df-9 12198 df-n0 12385 df-z 12472 df-dec 12592 df-uz 12736 df-q 12850 df-rp 12894 df-xneg 13014 df-xadd 13015 df-xmul 13016 df-icc 13255 df-fz 13411 df-fzo 13558 df-seq 13909 df-exp 13969 df-hash 14238 df-cj 15006 df-re 15007 df-im 15008 df-sqrt 15142 df-abs 15143 df-struct 17058 df-sets 17075 df-slot 17093 df-ndx 17105 df-base 17121 df-ress 17142 df-plusg 17174 df-mulr 17175 df-starv 17176 df-sca 17177 df-vsca 17178 df-ip 17179 df-tset 17180 df-ple 17181 df-ds 17183 df-unif 17184 df-hom 17185 df-cco 17186 df-rest 17326 df-topn 17327 df-0g 17345 df-gsum 17346 df-topgen 17347 df-pt 17348 df-prds 17351 df-xrs 17406 df-qtop 17411 df-imas 17412 df-xps 17414 df-mre 17488 df-mrc 17489 df-acs 17491 df-mgm 18514 df-sgrp 18593 df-mnd 18609 df-submnd 18658 df-mulg 18947 df-cntz 19196 df-cmn 19661 df-psmet 21253 df-xmet 21254 df-met 21255 df-bl 21256 df-mopn 21257 df-cnfld 21262 df-top 22779 df-topon 22796 df-topsp 22818 df-bases 22831 df-cld 22904 df-ntr 22905 df-cls 22906 df-cn 23112 df-cnp 23113 df-tx 23447 df-hmeo 23640 df-xms 24206 df-ms 24207 df-tms 24208 df-cncf 24769 df-limc 25765 df-dv 25766

This theorem is referenced by: dvmul 25842 dvmulf 25844 dvef 25882

W3C validator