Metamath Proof Explorer


Theorem plymullem1

Description: Derive the coefficient function for the product of two polynomials. (Contributed by Mario Carneiro, 23-Jul-2014)

Ref Expression
Hypotheses plyaddlem.1 ( 𝜑𝐹 ∈ ( Poly ‘ 𝑆 ) )
plyaddlem.2 ( 𝜑𝐺 ∈ ( Poly ‘ 𝑆 ) )
plyaddlem.m ( 𝜑𝑀 ∈ ℕ0 )
plyaddlem.n ( 𝜑𝑁 ∈ ℕ0 )
plyaddlem.a ( 𝜑𝐴 : ℕ0 ⟶ ℂ )
plyaddlem.b ( 𝜑𝐵 : ℕ0 ⟶ ℂ )
plyaddlem.a2 ( 𝜑 → ( 𝐴 “ ( ℤ ‘ ( 𝑀 + 1 ) ) ) = { 0 } )
plyaddlem.b2 ( 𝜑 → ( 𝐵 “ ( ℤ ‘ ( 𝑁 + 1 ) ) ) = { 0 } )
plyaddlem.f ( 𝜑𝐹 = ( 𝑧 ∈ ℂ ↦ Σ 𝑘 ∈ ( 0 ... 𝑀 ) ( ( 𝐴𝑘 ) · ( 𝑧𝑘 ) ) ) )
plyaddlem.g ( 𝜑𝐺 = ( 𝑧 ∈ ℂ ↦ Σ 𝑘 ∈ ( 0 ... 𝑁 ) ( ( 𝐵𝑘 ) · ( 𝑧𝑘 ) ) ) )
Assertion plymullem1 ( 𝜑 → ( 𝐹f · 𝐺 ) = ( 𝑧 ∈ ℂ ↦ Σ 𝑛 ∈ ( 0 ... ( 𝑀 + 𝑁 ) ) ( Σ 𝑘 ∈ ( 0 ... 𝑛 ) ( ( 𝐴𝑘 ) · ( 𝐵 ‘ ( 𝑛𝑘 ) ) ) · ( 𝑧𝑛 ) ) ) )

Proof

Step Hyp Ref Expression
1 plyaddlem.1 ( 𝜑𝐹 ∈ ( Poly ‘ 𝑆 ) )
2 plyaddlem.2 ( 𝜑𝐺 ∈ ( Poly ‘ 𝑆 ) )
3 plyaddlem.m ( 𝜑𝑀 ∈ ℕ0 )
4 plyaddlem.n ( 𝜑𝑁 ∈ ℕ0 )
5 plyaddlem.a ( 𝜑𝐴 : ℕ0 ⟶ ℂ )
6 plyaddlem.b ( 𝜑𝐵 : ℕ0 ⟶ ℂ )
7 plyaddlem.a2 ( 𝜑 → ( 𝐴 “ ( ℤ ‘ ( 𝑀 + 1 ) ) ) = { 0 } )
8 plyaddlem.b2 ( 𝜑 → ( 𝐵 “ ( ℤ ‘ ( 𝑁 + 1 ) ) ) = { 0 } )
9 plyaddlem.f ( 𝜑𝐹 = ( 𝑧 ∈ ℂ ↦ Σ 𝑘 ∈ ( 0 ... 𝑀 ) ( ( 𝐴𝑘 ) · ( 𝑧𝑘 ) ) ) )
10 plyaddlem.g ( 𝜑𝐺 = ( 𝑧 ∈ ℂ ↦ Σ 𝑘 ∈ ( 0 ... 𝑁 ) ( ( 𝐵𝑘 ) · ( 𝑧𝑘 ) ) ) )
11 cnex ℂ ∈ V
12 11 a1i ( 𝜑 → ℂ ∈ V )
13 sumex Σ 𝑘 ∈ ( 0 ... 𝑀 ) ( ( 𝐴𝑘 ) · ( 𝑧𝑘 ) ) ∈ V
14 13 a1i ( ( 𝜑𝑧 ∈ ℂ ) → Σ 𝑘 ∈ ( 0 ... 𝑀 ) ( ( 𝐴𝑘 ) · ( 𝑧𝑘 ) ) ∈ V )
15 sumex Σ 𝑘 ∈ ( 0 ... 𝑁 ) ( ( 𝐵𝑘 ) · ( 𝑧𝑘 ) ) ∈ V
16 15 a1i ( ( 𝜑𝑧 ∈ ℂ ) → Σ 𝑘 ∈ ( 0 ... 𝑁 ) ( ( 𝐵𝑘 ) · ( 𝑧𝑘 ) ) ∈ V )
17 12 14 16 9 10 offval2 ( 𝜑 → ( 𝐹f · 𝐺 ) = ( 𝑧 ∈ ℂ ↦ ( Σ 𝑘 ∈ ( 0 ... 𝑀 ) ( ( 𝐴𝑘 ) · ( 𝑧𝑘 ) ) · Σ 𝑘 ∈ ( 0 ... 𝑁 ) ( ( 𝐵𝑘 ) · ( 𝑧𝑘 ) ) ) ) )
18 fveq2 ( 𝑚 = 𝑛 → ( 𝐵𝑚 ) = ( 𝐵𝑛 ) )
19 oveq2 ( 𝑚 = 𝑛 → ( 𝑧𝑚 ) = ( 𝑧𝑛 ) )
20 18 19 oveq12d ( 𝑚 = 𝑛 → ( ( 𝐵𝑚 ) · ( 𝑧𝑚 ) ) = ( ( 𝐵𝑛 ) · ( 𝑧𝑛 ) ) )
21 20 oveq2d ( 𝑚 = 𝑛 → ( ( ( 𝐴𝑘 ) · ( 𝑧𝑘 ) ) · ( ( 𝐵𝑚 ) · ( 𝑧𝑚 ) ) ) = ( ( ( 𝐴𝑘 ) · ( 𝑧𝑘 ) ) · ( ( 𝐵𝑛 ) · ( 𝑧𝑛 ) ) ) )
22 fveq2 ( 𝑚 = ( 𝑛𝑘 ) → ( 𝐵𝑚 ) = ( 𝐵 ‘ ( 𝑛𝑘 ) ) )
23 oveq2 ( 𝑚 = ( 𝑛𝑘 ) → ( 𝑧𝑚 ) = ( 𝑧 ↑ ( 𝑛𝑘 ) ) )
24 22 23 oveq12d ( 𝑚 = ( 𝑛𝑘 ) → ( ( 𝐵𝑚 ) · ( 𝑧𝑚 ) ) = ( ( 𝐵 ‘ ( 𝑛𝑘 ) ) · ( 𝑧 ↑ ( 𝑛𝑘 ) ) ) )
25 24 oveq2d ( 𝑚 = ( 𝑛𝑘 ) → ( ( ( 𝐴𝑘 ) · ( 𝑧𝑘 ) ) · ( ( 𝐵𝑚 ) · ( 𝑧𝑚 ) ) ) = ( ( ( 𝐴𝑘 ) · ( 𝑧𝑘 ) ) · ( ( 𝐵 ‘ ( 𝑛𝑘 ) ) · ( 𝑧 ↑ ( 𝑛𝑘 ) ) ) ) )
26 elfznn0 ( 𝑘 ∈ ( 0 ... ( 𝑀 + 𝑁 ) ) → 𝑘 ∈ ℕ0 )
27 5 adantr ( ( 𝜑𝑧 ∈ ℂ ) → 𝐴 : ℕ0 ⟶ ℂ )
28 27 ffvelrnda ( ( ( 𝜑𝑧 ∈ ℂ ) ∧ 𝑘 ∈ ℕ0 ) → ( 𝐴𝑘 ) ∈ ℂ )
29 expcl ( ( 𝑧 ∈ ℂ ∧ 𝑘 ∈ ℕ0 ) → ( 𝑧𝑘 ) ∈ ℂ )
30 29 adantll ( ( ( 𝜑𝑧 ∈ ℂ ) ∧ 𝑘 ∈ ℕ0 ) → ( 𝑧𝑘 ) ∈ ℂ )
31 28 30 mulcld ( ( ( 𝜑𝑧 ∈ ℂ ) ∧ 𝑘 ∈ ℕ0 ) → ( ( 𝐴𝑘 ) · ( 𝑧𝑘 ) ) ∈ ℂ )
32 26 31 sylan2 ( ( ( 𝜑𝑧 ∈ ℂ ) ∧ 𝑘 ∈ ( 0 ... ( 𝑀 + 𝑁 ) ) ) → ( ( 𝐴𝑘 ) · ( 𝑧𝑘 ) ) ∈ ℂ )
33 elfznn0 ( 𝑛 ∈ ( 0 ... ( ( 𝑀 + 𝑁 ) − 𝑘 ) ) → 𝑛 ∈ ℕ0 )
34 6 adantr ( ( 𝜑𝑧 ∈ ℂ ) → 𝐵 : ℕ0 ⟶ ℂ )
35 34 ffvelrnda ( ( ( 𝜑𝑧 ∈ ℂ ) ∧ 𝑛 ∈ ℕ0 ) → ( 𝐵𝑛 ) ∈ ℂ )
36 expcl ( ( 𝑧 ∈ ℂ ∧ 𝑛 ∈ ℕ0 ) → ( 𝑧𝑛 ) ∈ ℂ )
37 36 adantll ( ( ( 𝜑𝑧 ∈ ℂ ) ∧ 𝑛 ∈ ℕ0 ) → ( 𝑧𝑛 ) ∈ ℂ )
38 35 37 mulcld ( ( ( 𝜑𝑧 ∈ ℂ ) ∧ 𝑛 ∈ ℕ0 ) → ( ( 𝐵𝑛 ) · ( 𝑧𝑛 ) ) ∈ ℂ )
39 33 38 sylan2 ( ( ( 𝜑𝑧 ∈ ℂ ) ∧ 𝑛 ∈ ( 0 ... ( ( 𝑀 + 𝑁 ) − 𝑘 ) ) ) → ( ( 𝐵𝑛 ) · ( 𝑧𝑛 ) ) ∈ ℂ )
40 32 39 anim12dan ( ( ( 𝜑𝑧 ∈ ℂ ) ∧ ( 𝑘 ∈ ( 0 ... ( 𝑀 + 𝑁 ) ) ∧ 𝑛 ∈ ( 0 ... ( ( 𝑀 + 𝑁 ) − 𝑘 ) ) ) ) → ( ( ( 𝐴𝑘 ) · ( 𝑧𝑘 ) ) ∈ ℂ ∧ ( ( 𝐵𝑛 ) · ( 𝑧𝑛 ) ) ∈ ℂ ) )
41 mulcl ( ( ( ( 𝐴𝑘 ) · ( 𝑧𝑘 ) ) ∈ ℂ ∧ ( ( 𝐵𝑛 ) · ( 𝑧𝑛 ) ) ∈ ℂ ) → ( ( ( 𝐴𝑘 ) · ( 𝑧𝑘 ) ) · ( ( 𝐵𝑛 ) · ( 𝑧𝑛 ) ) ) ∈ ℂ )
42 40 41 syl ( ( ( 𝜑𝑧 ∈ ℂ ) ∧ ( 𝑘 ∈ ( 0 ... ( 𝑀 + 𝑁 ) ) ∧ 𝑛 ∈ ( 0 ... ( ( 𝑀 + 𝑁 ) − 𝑘 ) ) ) ) → ( ( ( 𝐴𝑘 ) · ( 𝑧𝑘 ) ) · ( ( 𝐵𝑛 ) · ( 𝑧𝑛 ) ) ) ∈ ℂ )
43 21 25 42 fsum0diag2 ( ( 𝜑𝑧 ∈ ℂ ) → Σ 𝑘 ∈ ( 0 ... ( 𝑀 + 𝑁 ) ) Σ 𝑛 ∈ ( 0 ... ( ( 𝑀 + 𝑁 ) − 𝑘 ) ) ( ( ( 𝐴𝑘 ) · ( 𝑧𝑘 ) ) · ( ( 𝐵𝑛 ) · ( 𝑧𝑛 ) ) ) = Σ 𝑛 ∈ ( 0 ... ( 𝑀 + 𝑁 ) ) Σ 𝑘 ∈ ( 0 ... 𝑛 ) ( ( ( 𝐴𝑘 ) · ( 𝑧𝑘 ) ) · ( ( 𝐵 ‘ ( 𝑛𝑘 ) ) · ( 𝑧 ↑ ( 𝑛𝑘 ) ) ) ) )
44 3 nn0cnd ( 𝜑𝑀 ∈ ℂ )
45 44 ad2antrr ( ( ( 𝜑𝑧 ∈ ℂ ) ∧ 𝑘 ∈ ( 0 ... 𝑀 ) ) → 𝑀 ∈ ℂ )
46 4 nn0cnd ( 𝜑𝑁 ∈ ℂ )
47 46 ad2antrr ( ( ( 𝜑𝑧 ∈ ℂ ) ∧ 𝑘 ∈ ( 0 ... 𝑀 ) ) → 𝑁 ∈ ℂ )
48 elfznn0 ( 𝑘 ∈ ( 0 ... 𝑀 ) → 𝑘 ∈ ℕ0 )
49 48 adantl ( ( ( 𝜑𝑧 ∈ ℂ ) ∧ 𝑘 ∈ ( 0 ... 𝑀 ) ) → 𝑘 ∈ ℕ0 )
50 49 nn0cnd ( ( ( 𝜑𝑧 ∈ ℂ ) ∧ 𝑘 ∈ ( 0 ... 𝑀 ) ) → 𝑘 ∈ ℂ )
51 45 47 50 addsubd ( ( ( 𝜑𝑧 ∈ ℂ ) ∧ 𝑘 ∈ ( 0 ... 𝑀 ) ) → ( ( 𝑀 + 𝑁 ) − 𝑘 ) = ( ( 𝑀𝑘 ) + 𝑁 ) )
52 fznn0sub ( 𝑘 ∈ ( 0 ... 𝑀 ) → ( 𝑀𝑘 ) ∈ ℕ0 )
53 52 adantl ( ( ( 𝜑𝑧 ∈ ℂ ) ∧ 𝑘 ∈ ( 0 ... 𝑀 ) ) → ( 𝑀𝑘 ) ∈ ℕ0 )
54 nn0uz 0 = ( ℤ ‘ 0 )
55 53 54 eleqtrdi ( ( ( 𝜑𝑧 ∈ ℂ ) ∧ 𝑘 ∈ ( 0 ... 𝑀 ) ) → ( 𝑀𝑘 ) ∈ ( ℤ ‘ 0 ) )
56 4 nn0zd ( 𝜑𝑁 ∈ ℤ )
57 56 ad2antrr ( ( ( 𝜑𝑧 ∈ ℂ ) ∧ 𝑘 ∈ ( 0 ... 𝑀 ) ) → 𝑁 ∈ ℤ )
58 eluzadd ( ( ( 𝑀𝑘 ) ∈ ( ℤ ‘ 0 ) ∧ 𝑁 ∈ ℤ ) → ( ( 𝑀𝑘 ) + 𝑁 ) ∈ ( ℤ ‘ ( 0 + 𝑁 ) ) )
59 55 57 58 syl2anc ( ( ( 𝜑𝑧 ∈ ℂ ) ∧ 𝑘 ∈ ( 0 ... 𝑀 ) ) → ( ( 𝑀𝑘 ) + 𝑁 ) ∈ ( ℤ ‘ ( 0 + 𝑁 ) ) )
60 51 59 eqeltrd ( ( ( 𝜑𝑧 ∈ ℂ ) ∧ 𝑘 ∈ ( 0 ... 𝑀 ) ) → ( ( 𝑀 + 𝑁 ) − 𝑘 ) ∈ ( ℤ ‘ ( 0 + 𝑁 ) ) )
61 47 addid2d ( ( ( 𝜑𝑧 ∈ ℂ ) ∧ 𝑘 ∈ ( 0 ... 𝑀 ) ) → ( 0 + 𝑁 ) = 𝑁 )
62 61 fveq2d ( ( ( 𝜑𝑧 ∈ ℂ ) ∧ 𝑘 ∈ ( 0 ... 𝑀 ) ) → ( ℤ ‘ ( 0 + 𝑁 ) ) = ( ℤ𝑁 ) )
63 60 62 eleqtrd ( ( ( 𝜑𝑧 ∈ ℂ ) ∧ 𝑘 ∈ ( 0 ... 𝑀 ) ) → ( ( 𝑀 + 𝑁 ) − 𝑘 ) ∈ ( ℤ𝑁 ) )
64 fzss2 ( ( ( 𝑀 + 𝑁 ) − 𝑘 ) ∈ ( ℤ𝑁 ) → ( 0 ... 𝑁 ) ⊆ ( 0 ... ( ( 𝑀 + 𝑁 ) − 𝑘 ) ) )
65 63 64 syl ( ( ( 𝜑𝑧 ∈ ℂ ) ∧ 𝑘 ∈ ( 0 ... 𝑀 ) ) → ( 0 ... 𝑁 ) ⊆ ( 0 ... ( ( 𝑀 + 𝑁 ) − 𝑘 ) ) )
66 48 31 sylan2 ( ( ( 𝜑𝑧 ∈ ℂ ) ∧ 𝑘 ∈ ( 0 ... 𝑀 ) ) → ( ( 𝐴𝑘 ) · ( 𝑧𝑘 ) ) ∈ ℂ )
67 66 adantr ( ( ( ( 𝜑𝑧 ∈ ℂ ) ∧ 𝑘 ∈ ( 0 ... 𝑀 ) ) ∧ 𝑛 ∈ ( 0 ... 𝑁 ) ) → ( ( 𝐴𝑘 ) · ( 𝑧𝑘 ) ) ∈ ℂ )
68 elfznn0 ( 𝑛 ∈ ( 0 ... 𝑁 ) → 𝑛 ∈ ℕ0 )
69 68 38 sylan2 ( ( ( 𝜑𝑧 ∈ ℂ ) ∧ 𝑛 ∈ ( 0 ... 𝑁 ) ) → ( ( 𝐵𝑛 ) · ( 𝑧𝑛 ) ) ∈ ℂ )
70 69 adantlr ( ( ( ( 𝜑𝑧 ∈ ℂ ) ∧ 𝑘 ∈ ( 0 ... 𝑀 ) ) ∧ 𝑛 ∈ ( 0 ... 𝑁 ) ) → ( ( 𝐵𝑛 ) · ( 𝑧𝑛 ) ) ∈ ℂ )
71 67 70 mulcld ( ( ( ( 𝜑𝑧 ∈ ℂ ) ∧ 𝑘 ∈ ( 0 ... 𝑀 ) ) ∧ 𝑛 ∈ ( 0 ... 𝑁 ) ) → ( ( ( 𝐴𝑘 ) · ( 𝑧𝑘 ) ) · ( ( 𝐵𝑛 ) · ( 𝑧𝑛 ) ) ) ∈ ℂ )
72 eldifn ( 𝑛 ∈ ( ( 0 ... ( ( 𝑀 + 𝑁 ) − 𝑘 ) ) ∖ ( 0 ... 𝑁 ) ) → ¬ 𝑛 ∈ ( 0 ... 𝑁 ) )
73 72 adantl ( ( ( ( 𝜑𝑧 ∈ ℂ ) ∧ 𝑘 ∈ ( 0 ... 𝑀 ) ) ∧ 𝑛 ∈ ( ( 0 ... ( ( 𝑀 + 𝑁 ) − 𝑘 ) ) ∖ ( 0 ... 𝑁 ) ) ) → ¬ 𝑛 ∈ ( 0 ... 𝑁 ) )
74 eldifi ( 𝑛 ∈ ( ( 0 ... ( ( 𝑀 + 𝑁 ) − 𝑘 ) ) ∖ ( 0 ... 𝑁 ) ) → 𝑛 ∈ ( 0 ... ( ( 𝑀 + 𝑁 ) − 𝑘 ) ) )
75 74 33 syl ( 𝑛 ∈ ( ( 0 ... ( ( 𝑀 + 𝑁 ) − 𝑘 ) ) ∖ ( 0 ... 𝑁 ) ) → 𝑛 ∈ ℕ0 )
76 75 adantl ( ( ( ( 𝜑𝑧 ∈ ℂ ) ∧ 𝑘 ∈ ( 0 ... 𝑀 ) ) ∧ 𝑛 ∈ ( ( 0 ... ( ( 𝑀 + 𝑁 ) − 𝑘 ) ) ∖ ( 0 ... 𝑁 ) ) ) → 𝑛 ∈ ℕ0 )
77 peano2nn0 ( 𝑁 ∈ ℕ0 → ( 𝑁 + 1 ) ∈ ℕ0 )
78 4 77 syl ( 𝜑 → ( 𝑁 + 1 ) ∈ ℕ0 )
79 78 54 eleqtrdi ( 𝜑 → ( 𝑁 + 1 ) ∈ ( ℤ ‘ 0 ) )
80 uzsplit ( ( 𝑁 + 1 ) ∈ ( ℤ ‘ 0 ) → ( ℤ ‘ 0 ) = ( ( 0 ... ( ( 𝑁 + 1 ) − 1 ) ) ∪ ( ℤ ‘ ( 𝑁 + 1 ) ) ) )
81 79 80 syl ( 𝜑 → ( ℤ ‘ 0 ) = ( ( 0 ... ( ( 𝑁 + 1 ) − 1 ) ) ∪ ( ℤ ‘ ( 𝑁 + 1 ) ) ) )
82 54 81 syl5eq ( 𝜑 → ℕ0 = ( ( 0 ... ( ( 𝑁 + 1 ) − 1 ) ) ∪ ( ℤ ‘ ( 𝑁 + 1 ) ) ) )
83 ax-1cn 1 ∈ ℂ
84 pncan ( ( 𝑁 ∈ ℂ ∧ 1 ∈ ℂ ) → ( ( 𝑁 + 1 ) − 1 ) = 𝑁 )
85 46 83 84 sylancl ( 𝜑 → ( ( 𝑁 + 1 ) − 1 ) = 𝑁 )
86 85 oveq2d ( 𝜑 → ( 0 ... ( ( 𝑁 + 1 ) − 1 ) ) = ( 0 ... 𝑁 ) )
87 86 uneq1d ( 𝜑 → ( ( 0 ... ( ( 𝑁 + 1 ) − 1 ) ) ∪ ( ℤ ‘ ( 𝑁 + 1 ) ) ) = ( ( 0 ... 𝑁 ) ∪ ( ℤ ‘ ( 𝑁 + 1 ) ) ) )
88 82 87 eqtrd ( 𝜑 → ℕ0 = ( ( 0 ... 𝑁 ) ∪ ( ℤ ‘ ( 𝑁 + 1 ) ) ) )
89 88 ad3antrrr ( ( ( ( 𝜑𝑧 ∈ ℂ ) ∧ 𝑘 ∈ ( 0 ... 𝑀 ) ) ∧ 𝑛 ∈ ( ( 0 ... ( ( 𝑀 + 𝑁 ) − 𝑘 ) ) ∖ ( 0 ... 𝑁 ) ) ) → ℕ0 = ( ( 0 ... 𝑁 ) ∪ ( ℤ ‘ ( 𝑁 + 1 ) ) ) )
90 76 89 eleqtrd ( ( ( ( 𝜑𝑧 ∈ ℂ ) ∧ 𝑘 ∈ ( 0 ... 𝑀 ) ) ∧ 𝑛 ∈ ( ( 0 ... ( ( 𝑀 + 𝑁 ) − 𝑘 ) ) ∖ ( 0 ... 𝑁 ) ) ) → 𝑛 ∈ ( ( 0 ... 𝑁 ) ∪ ( ℤ ‘ ( 𝑁 + 1 ) ) ) )
91 elun ( 𝑛 ∈ ( ( 0 ... 𝑁 ) ∪ ( ℤ ‘ ( 𝑁 + 1 ) ) ) ↔ ( 𝑛 ∈ ( 0 ... 𝑁 ) ∨ 𝑛 ∈ ( ℤ ‘ ( 𝑁 + 1 ) ) ) )
92 90 91 sylib ( ( ( ( 𝜑𝑧 ∈ ℂ ) ∧ 𝑘 ∈ ( 0 ... 𝑀 ) ) ∧ 𝑛 ∈ ( ( 0 ... ( ( 𝑀 + 𝑁 ) − 𝑘 ) ) ∖ ( 0 ... 𝑁 ) ) ) → ( 𝑛 ∈ ( 0 ... 𝑁 ) ∨ 𝑛 ∈ ( ℤ ‘ ( 𝑁 + 1 ) ) ) )
93 92 ord ( ( ( ( 𝜑𝑧 ∈ ℂ ) ∧ 𝑘 ∈ ( 0 ... 𝑀 ) ) ∧ 𝑛 ∈ ( ( 0 ... ( ( 𝑀 + 𝑁 ) − 𝑘 ) ) ∖ ( 0 ... 𝑁 ) ) ) → ( ¬ 𝑛 ∈ ( 0 ... 𝑁 ) → 𝑛 ∈ ( ℤ ‘ ( 𝑁 + 1 ) ) ) )
94 73 93 mpd ( ( ( ( 𝜑𝑧 ∈ ℂ ) ∧ 𝑘 ∈ ( 0 ... 𝑀 ) ) ∧ 𝑛 ∈ ( ( 0 ... ( ( 𝑀 + 𝑁 ) − 𝑘 ) ) ∖ ( 0 ... 𝑁 ) ) ) → 𝑛 ∈ ( ℤ ‘ ( 𝑁 + 1 ) ) )
95 6 ffund ( 𝜑 → Fun 𝐵 )
96 ssun2 ( ℤ ‘ ( 𝑁 + 1 ) ) ⊆ ( ( 0 ... ( ( 𝑁 + 1 ) − 1 ) ) ∪ ( ℤ ‘ ( 𝑁 + 1 ) ) )
97 96 82 sseqtrrid ( 𝜑 → ( ℤ ‘ ( 𝑁 + 1 ) ) ⊆ ℕ0 )
98 6 fdmd ( 𝜑 → dom 𝐵 = ℕ0 )
99 97 98 sseqtrrd ( 𝜑 → ( ℤ ‘ ( 𝑁 + 1 ) ) ⊆ dom 𝐵 )
100 funfvima2 ( ( Fun 𝐵 ∧ ( ℤ ‘ ( 𝑁 + 1 ) ) ⊆ dom 𝐵 ) → ( 𝑛 ∈ ( ℤ ‘ ( 𝑁 + 1 ) ) → ( 𝐵𝑛 ) ∈ ( 𝐵 “ ( ℤ ‘ ( 𝑁 + 1 ) ) ) ) )
101 95 99 100 syl2anc ( 𝜑 → ( 𝑛 ∈ ( ℤ ‘ ( 𝑁 + 1 ) ) → ( 𝐵𝑛 ) ∈ ( 𝐵 “ ( ℤ ‘ ( 𝑁 + 1 ) ) ) ) )
102 101 ad3antrrr ( ( ( ( 𝜑𝑧 ∈ ℂ ) ∧ 𝑘 ∈ ( 0 ... 𝑀 ) ) ∧ 𝑛 ∈ ( ( 0 ... ( ( 𝑀 + 𝑁 ) − 𝑘 ) ) ∖ ( 0 ... 𝑁 ) ) ) → ( 𝑛 ∈ ( ℤ ‘ ( 𝑁 + 1 ) ) → ( 𝐵𝑛 ) ∈ ( 𝐵 “ ( ℤ ‘ ( 𝑁 + 1 ) ) ) ) )
103 94 102 mpd ( ( ( ( 𝜑𝑧 ∈ ℂ ) ∧ 𝑘 ∈ ( 0 ... 𝑀 ) ) ∧ 𝑛 ∈ ( ( 0 ... ( ( 𝑀 + 𝑁 ) − 𝑘 ) ) ∖ ( 0 ... 𝑁 ) ) ) → ( 𝐵𝑛 ) ∈ ( 𝐵 “ ( ℤ ‘ ( 𝑁 + 1 ) ) ) )
104 8 ad3antrrr ( ( ( ( 𝜑𝑧 ∈ ℂ ) ∧ 𝑘 ∈ ( 0 ... 𝑀 ) ) ∧ 𝑛 ∈ ( ( 0 ... ( ( 𝑀 + 𝑁 ) − 𝑘 ) ) ∖ ( 0 ... 𝑁 ) ) ) → ( 𝐵 “ ( ℤ ‘ ( 𝑁 + 1 ) ) ) = { 0 } )
105 103 104 eleqtrd ( ( ( ( 𝜑𝑧 ∈ ℂ ) ∧ 𝑘 ∈ ( 0 ... 𝑀 ) ) ∧ 𝑛 ∈ ( ( 0 ... ( ( 𝑀 + 𝑁 ) − 𝑘 ) ) ∖ ( 0 ... 𝑁 ) ) ) → ( 𝐵𝑛 ) ∈ { 0 } )
106 elsni ( ( 𝐵𝑛 ) ∈ { 0 } → ( 𝐵𝑛 ) = 0 )
107 105 106 syl ( ( ( ( 𝜑𝑧 ∈ ℂ ) ∧ 𝑘 ∈ ( 0 ... 𝑀 ) ) ∧ 𝑛 ∈ ( ( 0 ... ( ( 𝑀 + 𝑁 ) − 𝑘 ) ) ∖ ( 0 ... 𝑁 ) ) ) → ( 𝐵𝑛 ) = 0 )
108 107 oveq1d ( ( ( ( 𝜑𝑧 ∈ ℂ ) ∧ 𝑘 ∈ ( 0 ... 𝑀 ) ) ∧ 𝑛 ∈ ( ( 0 ... ( ( 𝑀 + 𝑁 ) − 𝑘 ) ) ∖ ( 0 ... 𝑁 ) ) ) → ( ( 𝐵𝑛 ) · ( 𝑧𝑛 ) ) = ( 0 · ( 𝑧𝑛 ) ) )
109 simplr ( ( ( 𝜑𝑧 ∈ ℂ ) ∧ 𝑘 ∈ ( 0 ... 𝑀 ) ) → 𝑧 ∈ ℂ )
110 109 75 36 syl2an ( ( ( ( 𝜑𝑧 ∈ ℂ ) ∧ 𝑘 ∈ ( 0 ... 𝑀 ) ) ∧ 𝑛 ∈ ( ( 0 ... ( ( 𝑀 + 𝑁 ) − 𝑘 ) ) ∖ ( 0 ... 𝑁 ) ) ) → ( 𝑧𝑛 ) ∈ ℂ )
111 110 mul02d ( ( ( ( 𝜑𝑧 ∈ ℂ ) ∧ 𝑘 ∈ ( 0 ... 𝑀 ) ) ∧ 𝑛 ∈ ( ( 0 ... ( ( 𝑀 + 𝑁 ) − 𝑘 ) ) ∖ ( 0 ... 𝑁 ) ) ) → ( 0 · ( 𝑧𝑛 ) ) = 0 )
112 108 111 eqtrd ( ( ( ( 𝜑𝑧 ∈ ℂ ) ∧ 𝑘 ∈ ( 0 ... 𝑀 ) ) ∧ 𝑛 ∈ ( ( 0 ... ( ( 𝑀 + 𝑁 ) − 𝑘 ) ) ∖ ( 0 ... 𝑁 ) ) ) → ( ( 𝐵𝑛 ) · ( 𝑧𝑛 ) ) = 0 )
113 112 oveq2d ( ( ( ( 𝜑𝑧 ∈ ℂ ) ∧ 𝑘 ∈ ( 0 ... 𝑀 ) ) ∧ 𝑛 ∈ ( ( 0 ... ( ( 𝑀 + 𝑁 ) − 𝑘 ) ) ∖ ( 0 ... 𝑁 ) ) ) → ( ( ( 𝐴𝑘 ) · ( 𝑧𝑘 ) ) · ( ( 𝐵𝑛 ) · ( 𝑧𝑛 ) ) ) = ( ( ( 𝐴𝑘 ) · ( 𝑧𝑘 ) ) · 0 ) )
114 66 adantr ( ( ( ( 𝜑𝑧 ∈ ℂ ) ∧ 𝑘 ∈ ( 0 ... 𝑀 ) ) ∧ 𝑛 ∈ ( ( 0 ... ( ( 𝑀 + 𝑁 ) − 𝑘 ) ) ∖ ( 0 ... 𝑁 ) ) ) → ( ( 𝐴𝑘 ) · ( 𝑧𝑘 ) ) ∈ ℂ )
115 114 mul01d ( ( ( ( 𝜑𝑧 ∈ ℂ ) ∧ 𝑘 ∈ ( 0 ... 𝑀 ) ) ∧ 𝑛 ∈ ( ( 0 ... ( ( 𝑀 + 𝑁 ) − 𝑘 ) ) ∖ ( 0 ... 𝑁 ) ) ) → ( ( ( 𝐴𝑘 ) · ( 𝑧𝑘 ) ) · 0 ) = 0 )
116 113 115 eqtrd ( ( ( ( 𝜑𝑧 ∈ ℂ ) ∧ 𝑘 ∈ ( 0 ... 𝑀 ) ) ∧ 𝑛 ∈ ( ( 0 ... ( ( 𝑀 + 𝑁 ) − 𝑘 ) ) ∖ ( 0 ... 𝑁 ) ) ) → ( ( ( 𝐴𝑘 ) · ( 𝑧𝑘 ) ) · ( ( 𝐵𝑛 ) · ( 𝑧𝑛 ) ) ) = 0 )
117 fzfid ( ( ( 𝜑𝑧 ∈ ℂ ) ∧ 𝑘 ∈ ( 0 ... 𝑀 ) ) → ( 0 ... ( ( 𝑀 + 𝑁 ) − 𝑘 ) ) ∈ Fin )
118 65 71 116 117 fsumss ( ( ( 𝜑𝑧 ∈ ℂ ) ∧ 𝑘 ∈ ( 0 ... 𝑀 ) ) → Σ 𝑛 ∈ ( 0 ... 𝑁 ) ( ( ( 𝐴𝑘 ) · ( 𝑧𝑘 ) ) · ( ( 𝐵𝑛 ) · ( 𝑧𝑛 ) ) ) = Σ 𝑛 ∈ ( 0 ... ( ( 𝑀 + 𝑁 ) − 𝑘 ) ) ( ( ( 𝐴𝑘 ) · ( 𝑧𝑘 ) ) · ( ( 𝐵𝑛 ) · ( 𝑧𝑛 ) ) ) )
119 118 sumeq2dv ( ( 𝜑𝑧 ∈ ℂ ) → Σ 𝑘 ∈ ( 0 ... 𝑀 ) Σ 𝑛 ∈ ( 0 ... 𝑁 ) ( ( ( 𝐴𝑘 ) · ( 𝑧𝑘 ) ) · ( ( 𝐵𝑛 ) · ( 𝑧𝑛 ) ) ) = Σ 𝑘 ∈ ( 0 ... 𝑀 ) Σ 𝑛 ∈ ( 0 ... ( ( 𝑀 + 𝑁 ) − 𝑘 ) ) ( ( ( 𝐴𝑘 ) · ( 𝑧𝑘 ) ) · ( ( 𝐵𝑛 ) · ( 𝑧𝑛 ) ) ) )
120 fzfid ( ( 𝜑𝑧 ∈ ℂ ) → ( 0 ... 𝑀 ) ∈ Fin )
121 fzfid ( ( 𝜑𝑧 ∈ ℂ ) → ( 0 ... 𝑁 ) ∈ Fin )
122 120 121 66 69 fsum2mul ( ( 𝜑𝑧 ∈ ℂ ) → Σ 𝑘 ∈ ( 0 ... 𝑀 ) Σ 𝑛 ∈ ( 0 ... 𝑁 ) ( ( ( 𝐴𝑘 ) · ( 𝑧𝑘 ) ) · ( ( 𝐵𝑛 ) · ( 𝑧𝑛 ) ) ) = ( Σ 𝑘 ∈ ( 0 ... 𝑀 ) ( ( 𝐴𝑘 ) · ( 𝑧𝑘 ) ) · Σ 𝑛 ∈ ( 0 ... 𝑁 ) ( ( 𝐵𝑛 ) · ( 𝑧𝑛 ) ) ) )
123 44 46 addcomd ( 𝜑 → ( 𝑀 + 𝑁 ) = ( 𝑁 + 𝑀 ) )
124 4 54 eleqtrdi ( 𝜑𝑁 ∈ ( ℤ ‘ 0 ) )
125 3 nn0zd ( 𝜑𝑀 ∈ ℤ )
126 eluzadd ( ( 𝑁 ∈ ( ℤ ‘ 0 ) ∧ 𝑀 ∈ ℤ ) → ( 𝑁 + 𝑀 ) ∈ ( ℤ ‘ ( 0 + 𝑀 ) ) )
127 124 125 126 syl2anc ( 𝜑 → ( 𝑁 + 𝑀 ) ∈ ( ℤ ‘ ( 0 + 𝑀 ) ) )
128 44 addid2d ( 𝜑 → ( 0 + 𝑀 ) = 𝑀 )
129 128 fveq2d ( 𝜑 → ( ℤ ‘ ( 0 + 𝑀 ) ) = ( ℤ𝑀 ) )
130 127 129 eleqtrd ( 𝜑 → ( 𝑁 + 𝑀 ) ∈ ( ℤ𝑀 ) )
131 123 130 eqeltrd ( 𝜑 → ( 𝑀 + 𝑁 ) ∈ ( ℤ𝑀 ) )
132 fzss2 ( ( 𝑀 + 𝑁 ) ∈ ( ℤ𝑀 ) → ( 0 ... 𝑀 ) ⊆ ( 0 ... ( 𝑀 + 𝑁 ) ) )
133 131 132 syl ( 𝜑 → ( 0 ... 𝑀 ) ⊆ ( 0 ... ( 𝑀 + 𝑁 ) ) )
134 133 adantr ( ( 𝜑𝑧 ∈ ℂ ) → ( 0 ... 𝑀 ) ⊆ ( 0 ... ( 𝑀 + 𝑁 ) ) )
135 66 adantr ( ( ( ( 𝜑𝑧 ∈ ℂ ) ∧ 𝑘 ∈ ( 0 ... 𝑀 ) ) ∧ 𝑛 ∈ ( 0 ... ( ( 𝑀 + 𝑁 ) − 𝑘 ) ) ) → ( ( 𝐴𝑘 ) · ( 𝑧𝑘 ) ) ∈ ℂ )
136 39 adantlr ( ( ( ( 𝜑𝑧 ∈ ℂ ) ∧ 𝑘 ∈ ( 0 ... 𝑀 ) ) ∧ 𝑛 ∈ ( 0 ... ( ( 𝑀 + 𝑁 ) − 𝑘 ) ) ) → ( ( 𝐵𝑛 ) · ( 𝑧𝑛 ) ) ∈ ℂ )
137 135 136 mulcld ( ( ( ( 𝜑𝑧 ∈ ℂ ) ∧ 𝑘 ∈ ( 0 ... 𝑀 ) ) ∧ 𝑛 ∈ ( 0 ... ( ( 𝑀 + 𝑁 ) − 𝑘 ) ) ) → ( ( ( 𝐴𝑘 ) · ( 𝑧𝑘 ) ) · ( ( 𝐵𝑛 ) · ( 𝑧𝑛 ) ) ) ∈ ℂ )
138 117 137 fsumcl ( ( ( 𝜑𝑧 ∈ ℂ ) ∧ 𝑘 ∈ ( 0 ... 𝑀 ) ) → Σ 𝑛 ∈ ( 0 ... ( ( 𝑀 + 𝑁 ) − 𝑘 ) ) ( ( ( 𝐴𝑘 ) · ( 𝑧𝑘 ) ) · ( ( 𝐵𝑛 ) · ( 𝑧𝑛 ) ) ) ∈ ℂ )
139 eldifn ( 𝑘 ∈ ( ( 0 ... ( 𝑀 + 𝑁 ) ) ∖ ( 0 ... 𝑀 ) ) → ¬ 𝑘 ∈ ( 0 ... 𝑀 ) )
140 139 adantl ( ( ( 𝜑𝑧 ∈ ℂ ) ∧ 𝑘 ∈ ( ( 0 ... ( 𝑀 + 𝑁 ) ) ∖ ( 0 ... 𝑀 ) ) ) → ¬ 𝑘 ∈ ( 0 ... 𝑀 ) )
141 eldifi ( 𝑘 ∈ ( ( 0 ... ( 𝑀 + 𝑁 ) ) ∖ ( 0 ... 𝑀 ) ) → 𝑘 ∈ ( 0 ... ( 𝑀 + 𝑁 ) ) )
142 141 26 syl ( 𝑘 ∈ ( ( 0 ... ( 𝑀 + 𝑁 ) ) ∖ ( 0 ... 𝑀 ) ) → 𝑘 ∈ ℕ0 )
143 142 adantl ( ( ( 𝜑𝑧 ∈ ℂ ) ∧ 𝑘 ∈ ( ( 0 ... ( 𝑀 + 𝑁 ) ) ∖ ( 0 ... 𝑀 ) ) ) → 𝑘 ∈ ℕ0 )
144 peano2nn0 ( 𝑀 ∈ ℕ0 → ( 𝑀 + 1 ) ∈ ℕ0 )
145 3 144 syl ( 𝜑 → ( 𝑀 + 1 ) ∈ ℕ0 )
146 145 54 eleqtrdi ( 𝜑 → ( 𝑀 + 1 ) ∈ ( ℤ ‘ 0 ) )
147 uzsplit ( ( 𝑀 + 1 ) ∈ ( ℤ ‘ 0 ) → ( ℤ ‘ 0 ) = ( ( 0 ... ( ( 𝑀 + 1 ) − 1 ) ) ∪ ( ℤ ‘ ( 𝑀 + 1 ) ) ) )
148 146 147 syl ( 𝜑 → ( ℤ ‘ 0 ) = ( ( 0 ... ( ( 𝑀 + 1 ) − 1 ) ) ∪ ( ℤ ‘ ( 𝑀 + 1 ) ) ) )
149 54 148 syl5eq ( 𝜑 → ℕ0 = ( ( 0 ... ( ( 𝑀 + 1 ) − 1 ) ) ∪ ( ℤ ‘ ( 𝑀 + 1 ) ) ) )
150 pncan ( ( 𝑀 ∈ ℂ ∧ 1 ∈ ℂ ) → ( ( 𝑀 + 1 ) − 1 ) = 𝑀 )
151 44 83 150 sylancl ( 𝜑 → ( ( 𝑀 + 1 ) − 1 ) = 𝑀 )
152 151 oveq2d ( 𝜑 → ( 0 ... ( ( 𝑀 + 1 ) − 1 ) ) = ( 0 ... 𝑀 ) )
153 152 uneq1d ( 𝜑 → ( ( 0 ... ( ( 𝑀 + 1 ) − 1 ) ) ∪ ( ℤ ‘ ( 𝑀 + 1 ) ) ) = ( ( 0 ... 𝑀 ) ∪ ( ℤ ‘ ( 𝑀 + 1 ) ) ) )
154 149 153 eqtrd ( 𝜑 → ℕ0 = ( ( 0 ... 𝑀 ) ∪ ( ℤ ‘ ( 𝑀 + 1 ) ) ) )
155 154 ad2antrr ( ( ( 𝜑𝑧 ∈ ℂ ) ∧ 𝑘 ∈ ( ( 0 ... ( 𝑀 + 𝑁 ) ) ∖ ( 0 ... 𝑀 ) ) ) → ℕ0 = ( ( 0 ... 𝑀 ) ∪ ( ℤ ‘ ( 𝑀 + 1 ) ) ) )
156 143 155 eleqtrd ( ( ( 𝜑𝑧 ∈ ℂ ) ∧ 𝑘 ∈ ( ( 0 ... ( 𝑀 + 𝑁 ) ) ∖ ( 0 ... 𝑀 ) ) ) → 𝑘 ∈ ( ( 0 ... 𝑀 ) ∪ ( ℤ ‘ ( 𝑀 + 1 ) ) ) )
157 elun ( 𝑘 ∈ ( ( 0 ... 𝑀 ) ∪ ( ℤ ‘ ( 𝑀 + 1 ) ) ) ↔ ( 𝑘 ∈ ( 0 ... 𝑀 ) ∨ 𝑘 ∈ ( ℤ ‘ ( 𝑀 + 1 ) ) ) )
158 156 157 sylib ( ( ( 𝜑𝑧 ∈ ℂ ) ∧ 𝑘 ∈ ( ( 0 ... ( 𝑀 + 𝑁 ) ) ∖ ( 0 ... 𝑀 ) ) ) → ( 𝑘 ∈ ( 0 ... 𝑀 ) ∨ 𝑘 ∈ ( ℤ ‘ ( 𝑀 + 1 ) ) ) )
159 158 ord ( ( ( 𝜑𝑧 ∈ ℂ ) ∧ 𝑘 ∈ ( ( 0 ... ( 𝑀 + 𝑁 ) ) ∖ ( 0 ... 𝑀 ) ) ) → ( ¬ 𝑘 ∈ ( 0 ... 𝑀 ) → 𝑘 ∈ ( ℤ ‘ ( 𝑀 + 1 ) ) ) )
160 140 159 mpd ( ( ( 𝜑𝑧 ∈ ℂ ) ∧ 𝑘 ∈ ( ( 0 ... ( 𝑀 + 𝑁 ) ) ∖ ( 0 ... 𝑀 ) ) ) → 𝑘 ∈ ( ℤ ‘ ( 𝑀 + 1 ) ) )
161 5 ffund ( 𝜑 → Fun 𝐴 )
162 ssun2 ( ℤ ‘ ( 𝑀 + 1 ) ) ⊆ ( ( 0 ... ( ( 𝑀 + 1 ) − 1 ) ) ∪ ( ℤ ‘ ( 𝑀 + 1 ) ) )
163 162 149 sseqtrrid ( 𝜑 → ( ℤ ‘ ( 𝑀 + 1 ) ) ⊆ ℕ0 )
164 5 fdmd ( 𝜑 → dom 𝐴 = ℕ0 )
165 163 164 sseqtrrd ( 𝜑 → ( ℤ ‘ ( 𝑀 + 1 ) ) ⊆ dom 𝐴 )
166 funfvima2 ( ( Fun 𝐴 ∧ ( ℤ ‘ ( 𝑀 + 1 ) ) ⊆ dom 𝐴 ) → ( 𝑘 ∈ ( ℤ ‘ ( 𝑀 + 1 ) ) → ( 𝐴𝑘 ) ∈ ( 𝐴 “ ( ℤ ‘ ( 𝑀 + 1 ) ) ) ) )
167 161 165 166 syl2anc ( 𝜑 → ( 𝑘 ∈ ( ℤ ‘ ( 𝑀 + 1 ) ) → ( 𝐴𝑘 ) ∈ ( 𝐴 “ ( ℤ ‘ ( 𝑀 + 1 ) ) ) ) )
168 167 ad2antrr ( ( ( 𝜑𝑧 ∈ ℂ ) ∧ 𝑘 ∈ ( ( 0 ... ( 𝑀 + 𝑁 ) ) ∖ ( 0 ... 𝑀 ) ) ) → ( 𝑘 ∈ ( ℤ ‘ ( 𝑀 + 1 ) ) → ( 𝐴𝑘 ) ∈ ( 𝐴 “ ( ℤ ‘ ( 𝑀 + 1 ) ) ) ) )
169 160 168 mpd ( ( ( 𝜑𝑧 ∈ ℂ ) ∧ 𝑘 ∈ ( ( 0 ... ( 𝑀 + 𝑁 ) ) ∖ ( 0 ... 𝑀 ) ) ) → ( 𝐴𝑘 ) ∈ ( 𝐴 “ ( ℤ ‘ ( 𝑀 + 1 ) ) ) )
170 7 ad2antrr ( ( ( 𝜑𝑧 ∈ ℂ ) ∧ 𝑘 ∈ ( ( 0 ... ( 𝑀 + 𝑁 ) ) ∖ ( 0 ... 𝑀 ) ) ) → ( 𝐴 “ ( ℤ ‘ ( 𝑀 + 1 ) ) ) = { 0 } )
171 169 170 eleqtrd ( ( ( 𝜑𝑧 ∈ ℂ ) ∧ 𝑘 ∈ ( ( 0 ... ( 𝑀 + 𝑁 ) ) ∖ ( 0 ... 𝑀 ) ) ) → ( 𝐴𝑘 ) ∈ { 0 } )
172 elsni ( ( 𝐴𝑘 ) ∈ { 0 } → ( 𝐴𝑘 ) = 0 )
173 171 172 syl ( ( ( 𝜑𝑧 ∈ ℂ ) ∧ 𝑘 ∈ ( ( 0 ... ( 𝑀 + 𝑁 ) ) ∖ ( 0 ... 𝑀 ) ) ) → ( 𝐴𝑘 ) = 0 )
174 173 oveq1d ( ( ( 𝜑𝑧 ∈ ℂ ) ∧ 𝑘 ∈ ( ( 0 ... ( 𝑀 + 𝑁 ) ) ∖ ( 0 ... 𝑀 ) ) ) → ( ( 𝐴𝑘 ) · ( 𝑧𝑘 ) ) = ( 0 · ( 𝑧𝑘 ) ) )
175 142 30 sylan2 ( ( ( 𝜑𝑧 ∈ ℂ ) ∧ 𝑘 ∈ ( ( 0 ... ( 𝑀 + 𝑁 ) ) ∖ ( 0 ... 𝑀 ) ) ) → ( 𝑧𝑘 ) ∈ ℂ )
176 175 mul02d ( ( ( 𝜑𝑧 ∈ ℂ ) ∧ 𝑘 ∈ ( ( 0 ... ( 𝑀 + 𝑁 ) ) ∖ ( 0 ... 𝑀 ) ) ) → ( 0 · ( 𝑧𝑘 ) ) = 0 )
177 174 176 eqtrd ( ( ( 𝜑𝑧 ∈ ℂ ) ∧ 𝑘 ∈ ( ( 0 ... ( 𝑀 + 𝑁 ) ) ∖ ( 0 ... 𝑀 ) ) ) → ( ( 𝐴𝑘 ) · ( 𝑧𝑘 ) ) = 0 )
178 177 adantr ( ( ( ( 𝜑𝑧 ∈ ℂ ) ∧ 𝑘 ∈ ( ( 0 ... ( 𝑀 + 𝑁 ) ) ∖ ( 0 ... 𝑀 ) ) ) ∧ 𝑛 ∈ ( 0 ... ( ( 𝑀 + 𝑁 ) − 𝑘 ) ) ) → ( ( 𝐴𝑘 ) · ( 𝑧𝑘 ) ) = 0 )
179 178 oveq1d ( ( ( ( 𝜑𝑧 ∈ ℂ ) ∧ 𝑘 ∈ ( ( 0 ... ( 𝑀 + 𝑁 ) ) ∖ ( 0 ... 𝑀 ) ) ) ∧ 𝑛 ∈ ( 0 ... ( ( 𝑀 + 𝑁 ) − 𝑘 ) ) ) → ( ( ( 𝐴𝑘 ) · ( 𝑧𝑘 ) ) · ( ( 𝐵𝑛 ) · ( 𝑧𝑛 ) ) ) = ( 0 · ( ( 𝐵𝑛 ) · ( 𝑧𝑛 ) ) ) )
180 39 adantlr ( ( ( ( 𝜑𝑧 ∈ ℂ ) ∧ 𝑘 ∈ ( ( 0 ... ( 𝑀 + 𝑁 ) ) ∖ ( 0 ... 𝑀 ) ) ) ∧ 𝑛 ∈ ( 0 ... ( ( 𝑀 + 𝑁 ) − 𝑘 ) ) ) → ( ( 𝐵𝑛 ) · ( 𝑧𝑛 ) ) ∈ ℂ )
181 180 mul02d ( ( ( ( 𝜑𝑧 ∈ ℂ ) ∧ 𝑘 ∈ ( ( 0 ... ( 𝑀 + 𝑁 ) ) ∖ ( 0 ... 𝑀 ) ) ) ∧ 𝑛 ∈ ( 0 ... ( ( 𝑀 + 𝑁 ) − 𝑘 ) ) ) → ( 0 · ( ( 𝐵𝑛 ) · ( 𝑧𝑛 ) ) ) = 0 )
182 179 181 eqtrd ( ( ( ( 𝜑𝑧 ∈ ℂ ) ∧ 𝑘 ∈ ( ( 0 ... ( 𝑀 + 𝑁 ) ) ∖ ( 0 ... 𝑀 ) ) ) ∧ 𝑛 ∈ ( 0 ... ( ( 𝑀 + 𝑁 ) − 𝑘 ) ) ) → ( ( ( 𝐴𝑘 ) · ( 𝑧𝑘 ) ) · ( ( 𝐵𝑛 ) · ( 𝑧𝑛 ) ) ) = 0 )
183 182 sumeq2dv ( ( ( 𝜑𝑧 ∈ ℂ ) ∧ 𝑘 ∈ ( ( 0 ... ( 𝑀 + 𝑁 ) ) ∖ ( 0 ... 𝑀 ) ) ) → Σ 𝑛 ∈ ( 0 ... ( ( 𝑀 + 𝑁 ) − 𝑘 ) ) ( ( ( 𝐴𝑘 ) · ( 𝑧𝑘 ) ) · ( ( 𝐵𝑛 ) · ( 𝑧𝑛 ) ) ) = Σ 𝑛 ∈ ( 0 ... ( ( 𝑀 + 𝑁 ) − 𝑘 ) ) 0 )
184 fzfid ( ( ( 𝜑𝑧 ∈ ℂ ) ∧ 𝑘 ∈ ( ( 0 ... ( 𝑀 + 𝑁 ) ) ∖ ( 0 ... 𝑀 ) ) ) → ( 0 ... ( ( 𝑀 + 𝑁 ) − 𝑘 ) ) ∈ Fin )
185 184 olcd ( ( ( 𝜑𝑧 ∈ ℂ ) ∧ 𝑘 ∈ ( ( 0 ... ( 𝑀 + 𝑁 ) ) ∖ ( 0 ... 𝑀 ) ) ) → ( ( 0 ... ( ( 𝑀 + 𝑁 ) − 𝑘 ) ) ⊆ ( ℤ ‘ 0 ) ∨ ( 0 ... ( ( 𝑀 + 𝑁 ) − 𝑘 ) ) ∈ Fin ) )
186 sumz ( ( ( 0 ... ( ( 𝑀 + 𝑁 ) − 𝑘 ) ) ⊆ ( ℤ ‘ 0 ) ∨ ( 0 ... ( ( 𝑀 + 𝑁 ) − 𝑘 ) ) ∈ Fin ) → Σ 𝑛 ∈ ( 0 ... ( ( 𝑀 + 𝑁 ) − 𝑘 ) ) 0 = 0 )
187 185 186 syl ( ( ( 𝜑𝑧 ∈ ℂ ) ∧ 𝑘 ∈ ( ( 0 ... ( 𝑀 + 𝑁 ) ) ∖ ( 0 ... 𝑀 ) ) ) → Σ 𝑛 ∈ ( 0 ... ( ( 𝑀 + 𝑁 ) − 𝑘 ) ) 0 = 0 )
188 183 187 eqtrd ( ( ( 𝜑𝑧 ∈ ℂ ) ∧ 𝑘 ∈ ( ( 0 ... ( 𝑀 + 𝑁 ) ) ∖ ( 0 ... 𝑀 ) ) ) → Σ 𝑛 ∈ ( 0 ... ( ( 𝑀 + 𝑁 ) − 𝑘 ) ) ( ( ( 𝐴𝑘 ) · ( 𝑧𝑘 ) ) · ( ( 𝐵𝑛 ) · ( 𝑧𝑛 ) ) ) = 0 )
189 fzfid ( ( 𝜑𝑧 ∈ ℂ ) → ( 0 ... ( 𝑀 + 𝑁 ) ) ∈ Fin )
190 134 138 188 189 fsumss ( ( 𝜑𝑧 ∈ ℂ ) → Σ 𝑘 ∈ ( 0 ... 𝑀 ) Σ 𝑛 ∈ ( 0 ... ( ( 𝑀 + 𝑁 ) − 𝑘 ) ) ( ( ( 𝐴𝑘 ) · ( 𝑧𝑘 ) ) · ( ( 𝐵𝑛 ) · ( 𝑧𝑛 ) ) ) = Σ 𝑘 ∈ ( 0 ... ( 𝑀 + 𝑁 ) ) Σ 𝑛 ∈ ( 0 ... ( ( 𝑀 + 𝑁 ) − 𝑘 ) ) ( ( ( 𝐴𝑘 ) · ( 𝑧𝑘 ) ) · ( ( 𝐵𝑛 ) · ( 𝑧𝑛 ) ) ) )
191 119 122 190 3eqtr3d ( ( 𝜑𝑧 ∈ ℂ ) → ( Σ 𝑘 ∈ ( 0 ... 𝑀 ) ( ( 𝐴𝑘 ) · ( 𝑧𝑘 ) ) · Σ 𝑛 ∈ ( 0 ... 𝑁 ) ( ( 𝐵𝑛 ) · ( 𝑧𝑛 ) ) ) = Σ 𝑘 ∈ ( 0 ... ( 𝑀 + 𝑁 ) ) Σ 𝑛 ∈ ( 0 ... ( ( 𝑀 + 𝑁 ) − 𝑘 ) ) ( ( ( 𝐴𝑘 ) · ( 𝑧𝑘 ) ) · ( ( 𝐵𝑛 ) · ( 𝑧𝑛 ) ) ) )
192 fzfid ( ( ( 𝜑𝑧 ∈ ℂ ) ∧ 𝑛 ∈ ( 0 ... ( 𝑀 + 𝑁 ) ) ) → ( 0 ... 𝑛 ) ∈ Fin )
193 elfznn0 ( 𝑛 ∈ ( 0 ... ( 𝑀 + 𝑁 ) ) → 𝑛 ∈ ℕ0 )
194 193 37 sylan2 ( ( ( 𝜑𝑧 ∈ ℂ ) ∧ 𝑛 ∈ ( 0 ... ( 𝑀 + 𝑁 ) ) ) → ( 𝑧𝑛 ) ∈ ℂ )
195 simpll ( ( ( 𝜑𝑧 ∈ ℂ ) ∧ 𝑛 ∈ ( 0 ... ( 𝑀 + 𝑁 ) ) ) → 𝜑 )
196 elfznn0 ( 𝑘 ∈ ( 0 ... 𝑛 ) → 𝑘 ∈ ℕ0 )
197 5 ffvelrnda ( ( 𝜑𝑘 ∈ ℕ0 ) → ( 𝐴𝑘 ) ∈ ℂ )
198 195 196 197 syl2an ( ( ( ( 𝜑𝑧 ∈ ℂ ) ∧ 𝑛 ∈ ( 0 ... ( 𝑀 + 𝑁 ) ) ) ∧ 𝑘 ∈ ( 0 ... 𝑛 ) ) → ( 𝐴𝑘 ) ∈ ℂ )
199 fznn0sub ( 𝑘 ∈ ( 0 ... 𝑛 ) → ( 𝑛𝑘 ) ∈ ℕ0 )
200 6 ffvelrnda ( ( 𝜑 ∧ ( 𝑛𝑘 ) ∈ ℕ0 ) → ( 𝐵 ‘ ( 𝑛𝑘 ) ) ∈ ℂ )
201 195 199 200 syl2an ( ( ( ( 𝜑𝑧 ∈ ℂ ) ∧ 𝑛 ∈ ( 0 ... ( 𝑀 + 𝑁 ) ) ) ∧ 𝑘 ∈ ( 0 ... 𝑛 ) ) → ( 𝐵 ‘ ( 𝑛𝑘 ) ) ∈ ℂ )
202 198 201 mulcld ( ( ( ( 𝜑𝑧 ∈ ℂ ) ∧ 𝑛 ∈ ( 0 ... ( 𝑀 + 𝑁 ) ) ) ∧ 𝑘 ∈ ( 0 ... 𝑛 ) ) → ( ( 𝐴𝑘 ) · ( 𝐵 ‘ ( 𝑛𝑘 ) ) ) ∈ ℂ )
203 192 194 202 fsummulc1 ( ( ( 𝜑𝑧 ∈ ℂ ) ∧ 𝑛 ∈ ( 0 ... ( 𝑀 + 𝑁 ) ) ) → ( Σ 𝑘 ∈ ( 0 ... 𝑛 ) ( ( 𝐴𝑘 ) · ( 𝐵 ‘ ( 𝑛𝑘 ) ) ) · ( 𝑧𝑛 ) ) = Σ 𝑘 ∈ ( 0 ... 𝑛 ) ( ( ( 𝐴𝑘 ) · ( 𝐵 ‘ ( 𝑛𝑘 ) ) ) · ( 𝑧𝑛 ) ) )
204 simplr ( ( ( 𝜑𝑧 ∈ ℂ ) ∧ 𝑛 ∈ ( 0 ... ( 𝑀 + 𝑁 ) ) ) → 𝑧 ∈ ℂ )
205 204 196 29 syl2an ( ( ( ( 𝜑𝑧 ∈ ℂ ) ∧ 𝑛 ∈ ( 0 ... ( 𝑀 + 𝑁 ) ) ) ∧ 𝑘 ∈ ( 0 ... 𝑛 ) ) → ( 𝑧𝑘 ) ∈ ℂ )
206 expcl ( ( 𝑧 ∈ ℂ ∧ ( 𝑛𝑘 ) ∈ ℕ0 ) → ( 𝑧 ↑ ( 𝑛𝑘 ) ) ∈ ℂ )
207 204 199 206 syl2an ( ( ( ( 𝜑𝑧 ∈ ℂ ) ∧ 𝑛 ∈ ( 0 ... ( 𝑀 + 𝑁 ) ) ) ∧ 𝑘 ∈ ( 0 ... 𝑛 ) ) → ( 𝑧 ↑ ( 𝑛𝑘 ) ) ∈ ℂ )
208 198 205 201 207 mul4d ( ( ( ( 𝜑𝑧 ∈ ℂ ) ∧ 𝑛 ∈ ( 0 ... ( 𝑀 + 𝑁 ) ) ) ∧ 𝑘 ∈ ( 0 ... 𝑛 ) ) → ( ( ( 𝐴𝑘 ) · ( 𝑧𝑘 ) ) · ( ( 𝐵 ‘ ( 𝑛𝑘 ) ) · ( 𝑧 ↑ ( 𝑛𝑘 ) ) ) ) = ( ( ( 𝐴𝑘 ) · ( 𝐵 ‘ ( 𝑛𝑘 ) ) ) · ( ( 𝑧𝑘 ) · ( 𝑧 ↑ ( 𝑛𝑘 ) ) ) ) )
209 204 adantr ( ( ( ( 𝜑𝑧 ∈ ℂ ) ∧ 𝑛 ∈ ( 0 ... ( 𝑀 + 𝑁 ) ) ) ∧ 𝑘 ∈ ( 0 ... 𝑛 ) ) → 𝑧 ∈ ℂ )
210 199 adantl ( ( ( ( 𝜑𝑧 ∈ ℂ ) ∧ 𝑛 ∈ ( 0 ... ( 𝑀 + 𝑁 ) ) ) ∧ 𝑘 ∈ ( 0 ... 𝑛 ) ) → ( 𝑛𝑘 ) ∈ ℕ0 )
211 196 adantl ( ( ( ( 𝜑𝑧 ∈ ℂ ) ∧ 𝑛 ∈ ( 0 ... ( 𝑀 + 𝑁 ) ) ) ∧ 𝑘 ∈ ( 0 ... 𝑛 ) ) → 𝑘 ∈ ℕ0 )
212 209 210 211 expaddd ( ( ( ( 𝜑𝑧 ∈ ℂ ) ∧ 𝑛 ∈ ( 0 ... ( 𝑀 + 𝑁 ) ) ) ∧ 𝑘 ∈ ( 0 ... 𝑛 ) ) → ( 𝑧 ↑ ( 𝑘 + ( 𝑛𝑘 ) ) ) = ( ( 𝑧𝑘 ) · ( 𝑧 ↑ ( 𝑛𝑘 ) ) ) )
213 211 nn0cnd ( ( ( ( 𝜑𝑧 ∈ ℂ ) ∧ 𝑛 ∈ ( 0 ... ( 𝑀 + 𝑁 ) ) ) ∧ 𝑘 ∈ ( 0 ... 𝑛 ) ) → 𝑘 ∈ ℂ )
214 193 ad2antlr ( ( ( ( 𝜑𝑧 ∈ ℂ ) ∧ 𝑛 ∈ ( 0 ... ( 𝑀 + 𝑁 ) ) ) ∧ 𝑘 ∈ ( 0 ... 𝑛 ) ) → 𝑛 ∈ ℕ0 )
215 214 nn0cnd ( ( ( ( 𝜑𝑧 ∈ ℂ ) ∧ 𝑛 ∈ ( 0 ... ( 𝑀 + 𝑁 ) ) ) ∧ 𝑘 ∈ ( 0 ... 𝑛 ) ) → 𝑛 ∈ ℂ )
216 213 215 pncan3d ( ( ( ( 𝜑𝑧 ∈ ℂ ) ∧ 𝑛 ∈ ( 0 ... ( 𝑀 + 𝑁 ) ) ) ∧ 𝑘 ∈ ( 0 ... 𝑛 ) ) → ( 𝑘 + ( 𝑛𝑘 ) ) = 𝑛 )
217 216 oveq2d ( ( ( ( 𝜑𝑧 ∈ ℂ ) ∧ 𝑛 ∈ ( 0 ... ( 𝑀 + 𝑁 ) ) ) ∧ 𝑘 ∈ ( 0 ... 𝑛 ) ) → ( 𝑧 ↑ ( 𝑘 + ( 𝑛𝑘 ) ) ) = ( 𝑧𝑛 ) )
218 212 217 eqtr3d ( ( ( ( 𝜑𝑧 ∈ ℂ ) ∧ 𝑛 ∈ ( 0 ... ( 𝑀 + 𝑁 ) ) ) ∧ 𝑘 ∈ ( 0 ... 𝑛 ) ) → ( ( 𝑧𝑘 ) · ( 𝑧 ↑ ( 𝑛𝑘 ) ) ) = ( 𝑧𝑛 ) )
219 218 oveq2d ( ( ( ( 𝜑𝑧 ∈ ℂ ) ∧ 𝑛 ∈ ( 0 ... ( 𝑀 + 𝑁 ) ) ) ∧ 𝑘 ∈ ( 0 ... 𝑛 ) ) → ( ( ( 𝐴𝑘 ) · ( 𝐵 ‘ ( 𝑛𝑘 ) ) ) · ( ( 𝑧𝑘 ) · ( 𝑧 ↑ ( 𝑛𝑘 ) ) ) ) = ( ( ( 𝐴𝑘 ) · ( 𝐵 ‘ ( 𝑛𝑘 ) ) ) · ( 𝑧𝑛 ) ) )
220 208 219 eqtrd ( ( ( ( 𝜑𝑧 ∈ ℂ ) ∧ 𝑛 ∈ ( 0 ... ( 𝑀 + 𝑁 ) ) ) ∧ 𝑘 ∈ ( 0 ... 𝑛 ) ) → ( ( ( 𝐴𝑘 ) · ( 𝑧𝑘 ) ) · ( ( 𝐵 ‘ ( 𝑛𝑘 ) ) · ( 𝑧 ↑ ( 𝑛𝑘 ) ) ) ) = ( ( ( 𝐴𝑘 ) · ( 𝐵 ‘ ( 𝑛𝑘 ) ) ) · ( 𝑧𝑛 ) ) )
221 220 sumeq2dv ( ( ( 𝜑𝑧 ∈ ℂ ) ∧ 𝑛 ∈ ( 0 ... ( 𝑀 + 𝑁 ) ) ) → Σ 𝑘 ∈ ( 0 ... 𝑛 ) ( ( ( 𝐴𝑘 ) · ( 𝑧𝑘 ) ) · ( ( 𝐵 ‘ ( 𝑛𝑘 ) ) · ( 𝑧 ↑ ( 𝑛𝑘 ) ) ) ) = Σ 𝑘 ∈ ( 0 ... 𝑛 ) ( ( ( 𝐴𝑘 ) · ( 𝐵 ‘ ( 𝑛𝑘 ) ) ) · ( 𝑧𝑛 ) ) )
222 203 221 eqtr4d ( ( ( 𝜑𝑧 ∈ ℂ ) ∧ 𝑛 ∈ ( 0 ... ( 𝑀 + 𝑁 ) ) ) → ( Σ 𝑘 ∈ ( 0 ... 𝑛 ) ( ( 𝐴𝑘 ) · ( 𝐵 ‘ ( 𝑛𝑘 ) ) ) · ( 𝑧𝑛 ) ) = Σ 𝑘 ∈ ( 0 ... 𝑛 ) ( ( ( 𝐴𝑘 ) · ( 𝑧𝑘 ) ) · ( ( 𝐵 ‘ ( 𝑛𝑘 ) ) · ( 𝑧 ↑ ( 𝑛𝑘 ) ) ) ) )
223 222 sumeq2dv ( ( 𝜑𝑧 ∈ ℂ ) → Σ 𝑛 ∈ ( 0 ... ( 𝑀 + 𝑁 ) ) ( Σ 𝑘 ∈ ( 0 ... 𝑛 ) ( ( 𝐴𝑘 ) · ( 𝐵 ‘ ( 𝑛𝑘 ) ) ) · ( 𝑧𝑛 ) ) = Σ 𝑛 ∈ ( 0 ... ( 𝑀 + 𝑁 ) ) Σ 𝑘 ∈ ( 0 ... 𝑛 ) ( ( ( 𝐴𝑘 ) · ( 𝑧𝑘 ) ) · ( ( 𝐵 ‘ ( 𝑛𝑘 ) ) · ( 𝑧 ↑ ( 𝑛𝑘 ) ) ) ) )
224 43 191 223 3eqtr4rd ( ( 𝜑𝑧 ∈ ℂ ) → Σ 𝑛 ∈ ( 0 ... ( 𝑀 + 𝑁 ) ) ( Σ 𝑘 ∈ ( 0 ... 𝑛 ) ( ( 𝐴𝑘 ) · ( 𝐵 ‘ ( 𝑛𝑘 ) ) ) · ( 𝑧𝑛 ) ) = ( Σ 𝑘 ∈ ( 0 ... 𝑀 ) ( ( 𝐴𝑘 ) · ( 𝑧𝑘 ) ) · Σ 𝑛 ∈ ( 0 ... 𝑁 ) ( ( 𝐵𝑛 ) · ( 𝑧𝑛 ) ) ) )
225 fveq2 ( 𝑛 = 𝑘 → ( 𝐵𝑛 ) = ( 𝐵𝑘 ) )
226 oveq2 ( 𝑛 = 𝑘 → ( 𝑧𝑛 ) = ( 𝑧𝑘 ) )
227 225 226 oveq12d ( 𝑛 = 𝑘 → ( ( 𝐵𝑛 ) · ( 𝑧𝑛 ) ) = ( ( 𝐵𝑘 ) · ( 𝑧𝑘 ) ) )
228 227 cbvsumv Σ 𝑛 ∈ ( 0 ... 𝑁 ) ( ( 𝐵𝑛 ) · ( 𝑧𝑛 ) ) = Σ 𝑘 ∈ ( 0 ... 𝑁 ) ( ( 𝐵𝑘 ) · ( 𝑧𝑘 ) )
229 228 oveq2i ( Σ 𝑘 ∈ ( 0 ... 𝑀 ) ( ( 𝐴𝑘 ) · ( 𝑧𝑘 ) ) · Σ 𝑛 ∈ ( 0 ... 𝑁 ) ( ( 𝐵𝑛 ) · ( 𝑧𝑛 ) ) ) = ( Σ 𝑘 ∈ ( 0 ... 𝑀 ) ( ( 𝐴𝑘 ) · ( 𝑧𝑘 ) ) · Σ 𝑘 ∈ ( 0 ... 𝑁 ) ( ( 𝐵𝑘 ) · ( 𝑧𝑘 ) ) )
230 224 229 eqtrdi ( ( 𝜑𝑧 ∈ ℂ ) → Σ 𝑛 ∈ ( 0 ... ( 𝑀 + 𝑁 ) ) ( Σ 𝑘 ∈ ( 0 ... 𝑛 ) ( ( 𝐴𝑘 ) · ( 𝐵 ‘ ( 𝑛𝑘 ) ) ) · ( 𝑧𝑛 ) ) = ( Σ 𝑘 ∈ ( 0 ... 𝑀 ) ( ( 𝐴𝑘 ) · ( 𝑧𝑘 ) ) · Σ 𝑘 ∈ ( 0 ... 𝑁 ) ( ( 𝐵𝑘 ) · ( 𝑧𝑘 ) ) ) )
231 230 mpteq2dva ( 𝜑 → ( 𝑧 ∈ ℂ ↦ Σ 𝑛 ∈ ( 0 ... ( 𝑀 + 𝑁 ) ) ( Σ 𝑘 ∈ ( 0 ... 𝑛 ) ( ( 𝐴𝑘 ) · ( 𝐵 ‘ ( 𝑛𝑘 ) ) ) · ( 𝑧𝑛 ) ) ) = ( 𝑧 ∈ ℂ ↦ ( Σ 𝑘 ∈ ( 0 ... 𝑀 ) ( ( 𝐴𝑘 ) · ( 𝑧𝑘 ) ) · Σ 𝑘 ∈ ( 0 ... 𝑁 ) ( ( 𝐵𝑘 ) · ( 𝑧𝑘 ) ) ) ) )
232 17 231 eqtr4d ( 𝜑 → ( 𝐹f · 𝐺 ) = ( 𝑧 ∈ ℂ ↦ Σ 𝑛 ∈ ( 0 ... ( 𝑀 + 𝑁 ) ) ( Σ 𝑘 ∈ ( 0 ... 𝑛 ) ( ( 𝐴𝑘 ) · ( 𝐵 ‘ ( 𝑛𝑘 ) ) ) · ( 𝑧𝑛 ) ) ) )