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 ffvelcdmda ⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ ℂ ) ∧ 𝑘 ∈ ℕ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 ffvelcdmda ⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ ℂ ) ∧ 𝑛 ∈ ℕ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 addlidd ⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ ℂ ) ∧ 𝑘 ∈ ( 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 eqtrid ⊢ ( 𝜑 → ℕ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 addlidd ⊢ ( 𝜑 → ( 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 eqtrid ⊢ ( 𝜑 → ℕ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 ffvelcdmda ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ0 ) → ( 𝐴 ‘ 𝑘 ) ∈ ℂ )
198 195 196 197 syl2an ⊢ ( ( ( ( 𝜑 ∧ 𝑧 ∈ ℂ ) ∧ 𝑛 ∈ ( 0 ... ( 𝑀 + 𝑁 ) ) ) ∧ 𝑘 ∈ ( 0 ... 𝑛 ) ) → ( 𝐴 ‘ 𝑘 ) ∈ ℂ )
199 fznn0sub ⊢ ( 𝑘 ∈ ( 0 ... 𝑛 ) → ( 𝑛 − 𝑘 ) ∈ ℕ0 )
200 6 ffvelcdmda ⊢ ( ( 𝜑 ∧ ( 𝑛 − 𝑘 ) ∈ ℕ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 ... 𝑛 ) ( ( 𝐴 ‘ 𝑘 ) · ( 𝐵 ‘ ( 𝑛 − 𝑘 ) ) ) · ( 𝑧 ↑ 𝑛 ) ) ) )