Theorem gg-dvmulbr

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

	Ref	Expression
Hypotheses	gg-dvadd.f	⊢ ( 𝜑 → 𝐹 : 𝑋 ⟶ ℂ )
	gg-dvadd.x	⊢ ( 𝜑 → 𝑋 ⊆ 𝑆 )
	gg-dvadd.g	⊢ ( 𝜑 → 𝐺 : 𝑌 ⟶ ℂ )
	gg-dvadd.y	⊢ ( 𝜑 → 𝑌 ⊆ 𝑆 )
	gg-dvaddbr.s	⊢ ( 𝜑 → 𝑆 ⊆ ℂ )
	gg-dvadd.k	⊢ ( 𝜑 → 𝐾 ∈ 𝑉 )
	gg-dvadd.l	⊢ ( 𝜑 → 𝐿 ∈ 𝑉 )
	gg-dvadd.bf	⊢ ( 𝜑 → 𝐶 ( 𝑆 D 𝐹 ) 𝐾 )
	gg-dvadd.bg	⊢ ( 𝜑 → 𝐶 ( 𝑆 D 𝐺 ) 𝐿 )
	gg-dvadd.j	⊢ 𝐽 = ( TopOpen ‘ ℂfld )
Assertion	gg-dvmulbr	⊢ ( 𝜑 → 𝐶 ( 𝑆 D ( 𝐹 ∘f · 𝐺 ) ) ( ( 𝐾 · ( 𝐺 ‘ 𝐶 ) ) + ( 𝐿 · ( 𝐹 ‘ 𝐶 ) ) ) )

Proof

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