Metamath Proof Explorer

Theorem 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 and remove unnecessary hypotheses. (Revised by GG, 16-Mar-2025)

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

Proof

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