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 · 𝐺 ) ) ( ( 𝐾 · ( 𝐺𝐶 ) ) + ( 𝐿 · ( 𝐹𝐶 ) ) ) )