Metamath Proof Explorer


Theorem plyaddlem1

Description: Derive the coefficient function for the sum 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 plyaddlem1 ( 𝜑 → ( 𝐹f + 𝐺 ) = ( 𝑧 ∈ ℂ ↦ Σ 𝑘 ∈ ( 0 ... if ( 𝑀𝑁 , 𝑁 , 𝑀 ) ) ( ( ( 𝐴f + 𝐵 ) ‘ 𝑘 ) · ( 𝑧𝑘 ) ) ) )

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 fzfid ( ( 𝜑𝑧 ∈ ℂ ) → ( 0 ... if ( 𝑀𝑁 , 𝑁 , 𝑀 ) ) ∈ Fin )
19 elfznn0 ( 𝑘 ∈ ( 0 ... if ( 𝑀𝑁 , 𝑁 , 𝑀 ) ) → 𝑘 ∈ ℕ0 )
20 5 adantr ( ( 𝜑𝑧 ∈ ℂ ) → 𝐴 : ℕ0 ⟶ ℂ )
21 20 ffvelrnda ( ( ( 𝜑𝑧 ∈ ℂ ) ∧ 𝑘 ∈ ℕ0 ) → ( 𝐴𝑘 ) ∈ ℂ )
22 expcl ( ( 𝑧 ∈ ℂ ∧ 𝑘 ∈ ℕ0 ) → ( 𝑧𝑘 ) ∈ ℂ )
23 22 adantll ( ( ( 𝜑𝑧 ∈ ℂ ) ∧ 𝑘 ∈ ℕ0 ) → ( 𝑧𝑘 ) ∈ ℂ )
24 21 23 mulcld ( ( ( 𝜑𝑧 ∈ ℂ ) ∧ 𝑘 ∈ ℕ0 ) → ( ( 𝐴𝑘 ) · ( 𝑧𝑘 ) ) ∈ ℂ )
25 19 24 sylan2 ( ( ( 𝜑𝑧 ∈ ℂ ) ∧ 𝑘 ∈ ( 0 ... if ( 𝑀𝑁 , 𝑁 , 𝑀 ) ) ) → ( ( 𝐴𝑘 ) · ( 𝑧𝑘 ) ) ∈ ℂ )
26 6 adantr ( ( 𝜑𝑧 ∈ ℂ ) → 𝐵 : ℕ0 ⟶ ℂ )
27 26 ffvelrnda ( ( ( 𝜑𝑧 ∈ ℂ ) ∧ 𝑘 ∈ ℕ0 ) → ( 𝐵𝑘 ) ∈ ℂ )
28 27 23 mulcld ( ( ( 𝜑𝑧 ∈ ℂ ) ∧ 𝑘 ∈ ℕ0 ) → ( ( 𝐵𝑘 ) · ( 𝑧𝑘 ) ) ∈ ℂ )
29 19 28 sylan2 ( ( ( 𝜑𝑧 ∈ ℂ ) ∧ 𝑘 ∈ ( 0 ... if ( 𝑀𝑁 , 𝑁 , 𝑀 ) ) ) → ( ( 𝐵𝑘 ) · ( 𝑧𝑘 ) ) ∈ ℂ )
30 18 25 29 fsumadd ( ( 𝜑𝑧 ∈ ℂ ) → Σ 𝑘 ∈ ( 0 ... if ( 𝑀𝑁 , 𝑁 , 𝑀 ) ) ( ( ( 𝐴𝑘 ) · ( 𝑧𝑘 ) ) + ( ( 𝐵𝑘 ) · ( 𝑧𝑘 ) ) ) = ( Σ 𝑘 ∈ ( 0 ... if ( 𝑀𝑁 , 𝑁 , 𝑀 ) ) ( ( 𝐴𝑘 ) · ( 𝑧𝑘 ) ) + Σ 𝑘 ∈ ( 0 ... if ( 𝑀𝑁 , 𝑁 , 𝑀 ) ) ( ( 𝐵𝑘 ) · ( 𝑧𝑘 ) ) ) )
31 5 ffnd ( 𝜑𝐴 Fn ℕ0 )
32 6 ffnd ( 𝜑𝐵 Fn ℕ0 )
33 nn0ex 0 ∈ V
34 33 a1i ( 𝜑 → ℕ0 ∈ V )
35 inidm ( ℕ0 ∩ ℕ0 ) = ℕ0
36 eqidd ( ( 𝜑𝑘 ∈ ℕ0 ) → ( 𝐴𝑘 ) = ( 𝐴𝑘 ) )
37 eqidd ( ( 𝜑𝑘 ∈ ℕ0 ) → ( 𝐵𝑘 ) = ( 𝐵𝑘 ) )
38 31 32 34 34 35 36 37 ofval ( ( 𝜑𝑘 ∈ ℕ0 ) → ( ( 𝐴f + 𝐵 ) ‘ 𝑘 ) = ( ( 𝐴𝑘 ) + ( 𝐵𝑘 ) ) )
39 38 adantlr ( ( ( 𝜑𝑧 ∈ ℂ ) ∧ 𝑘 ∈ ℕ0 ) → ( ( 𝐴f + 𝐵 ) ‘ 𝑘 ) = ( ( 𝐴𝑘 ) + ( 𝐵𝑘 ) ) )
40 39 oveq1d ( ( ( 𝜑𝑧 ∈ ℂ ) ∧ 𝑘 ∈ ℕ0 ) → ( ( ( 𝐴f + 𝐵 ) ‘ 𝑘 ) · ( 𝑧𝑘 ) ) = ( ( ( 𝐴𝑘 ) + ( 𝐵𝑘 ) ) · ( 𝑧𝑘 ) ) )
41 21 27 23 adddird ( ( ( 𝜑𝑧 ∈ ℂ ) ∧ 𝑘 ∈ ℕ0 ) → ( ( ( 𝐴𝑘 ) + ( 𝐵𝑘 ) ) · ( 𝑧𝑘 ) ) = ( ( ( 𝐴𝑘 ) · ( 𝑧𝑘 ) ) + ( ( 𝐵𝑘 ) · ( 𝑧𝑘 ) ) ) )
42 40 41 eqtrd ( ( ( 𝜑𝑧 ∈ ℂ ) ∧ 𝑘 ∈ ℕ0 ) → ( ( ( 𝐴f + 𝐵 ) ‘ 𝑘 ) · ( 𝑧𝑘 ) ) = ( ( ( 𝐴𝑘 ) · ( 𝑧𝑘 ) ) + ( ( 𝐵𝑘 ) · ( 𝑧𝑘 ) ) ) )
43 19 42 sylan2 ( ( ( 𝜑𝑧 ∈ ℂ ) ∧ 𝑘 ∈ ( 0 ... if ( 𝑀𝑁 , 𝑁 , 𝑀 ) ) ) → ( ( ( 𝐴f + 𝐵 ) ‘ 𝑘 ) · ( 𝑧𝑘 ) ) = ( ( ( 𝐴𝑘 ) · ( 𝑧𝑘 ) ) + ( ( 𝐵𝑘 ) · ( 𝑧𝑘 ) ) ) )
44 43 sumeq2dv ( ( 𝜑𝑧 ∈ ℂ ) → Σ 𝑘 ∈ ( 0 ... if ( 𝑀𝑁 , 𝑁 , 𝑀 ) ) ( ( ( 𝐴f + 𝐵 ) ‘ 𝑘 ) · ( 𝑧𝑘 ) ) = Σ 𝑘 ∈ ( 0 ... if ( 𝑀𝑁 , 𝑁 , 𝑀 ) ) ( ( ( 𝐴𝑘 ) · ( 𝑧𝑘 ) ) + ( ( 𝐵𝑘 ) · ( 𝑧𝑘 ) ) ) )
45 3 nn0zd ( 𝜑𝑀 ∈ ℤ )
46 4 3 ifcld ( 𝜑 → if ( 𝑀𝑁 , 𝑁 , 𝑀 ) ∈ ℕ0 )
47 46 nn0zd ( 𝜑 → if ( 𝑀𝑁 , 𝑁 , 𝑀 ) ∈ ℤ )
48 3 nn0red ( 𝜑𝑀 ∈ ℝ )
49 4 nn0red ( 𝜑𝑁 ∈ ℝ )
50 max1 ( ( 𝑀 ∈ ℝ ∧ 𝑁 ∈ ℝ ) → 𝑀 ≤ if ( 𝑀𝑁 , 𝑁 , 𝑀 ) )
51 48 49 50 syl2anc ( 𝜑𝑀 ≤ if ( 𝑀𝑁 , 𝑁 , 𝑀 ) )
52 eluz2 ( if ( 𝑀𝑁 , 𝑁 , 𝑀 ) ∈ ( ℤ𝑀 ) ↔ ( 𝑀 ∈ ℤ ∧ if ( 𝑀𝑁 , 𝑁 , 𝑀 ) ∈ ℤ ∧ 𝑀 ≤ if ( 𝑀𝑁 , 𝑁 , 𝑀 ) ) )
53 45 47 51 52 syl3anbrc ( 𝜑 → if ( 𝑀𝑁 , 𝑁 , 𝑀 ) ∈ ( ℤ𝑀 ) )
54 fzss2 ( if ( 𝑀𝑁 , 𝑁 , 𝑀 ) ∈ ( ℤ𝑀 ) → ( 0 ... 𝑀 ) ⊆ ( 0 ... if ( 𝑀𝑁 , 𝑁 , 𝑀 ) ) )
55 53 54 syl ( 𝜑 → ( 0 ... 𝑀 ) ⊆ ( 0 ... if ( 𝑀𝑁 , 𝑁 , 𝑀 ) ) )
56 55 adantr ( ( 𝜑𝑧 ∈ ℂ ) → ( 0 ... 𝑀 ) ⊆ ( 0 ... if ( 𝑀𝑁 , 𝑁 , 𝑀 ) ) )
57 elfznn0 ( 𝑘 ∈ ( 0 ... 𝑀 ) → 𝑘 ∈ ℕ0 )
58 57 24 sylan2 ( ( ( 𝜑𝑧 ∈ ℂ ) ∧ 𝑘 ∈ ( 0 ... 𝑀 ) ) → ( ( 𝐴𝑘 ) · ( 𝑧𝑘 ) ) ∈ ℂ )
59 eldifn ( 𝑘 ∈ ( ( 0 ... if ( 𝑀𝑁 , 𝑁 , 𝑀 ) ) ∖ ( 0 ... 𝑀 ) ) → ¬ 𝑘 ∈ ( 0 ... 𝑀 ) )
60 59 adantl ( ( ( 𝜑𝑧 ∈ ℂ ) ∧ 𝑘 ∈ ( ( 0 ... if ( 𝑀𝑁 , 𝑁 , 𝑀 ) ) ∖ ( 0 ... 𝑀 ) ) ) → ¬ 𝑘 ∈ ( 0 ... 𝑀 ) )
61 eldifi ( 𝑘 ∈ ( ( 0 ... if ( 𝑀𝑁 , 𝑁 , 𝑀 ) ) ∖ ( 0 ... 𝑀 ) ) → 𝑘 ∈ ( 0 ... if ( 𝑀𝑁 , 𝑁 , 𝑀 ) ) )
62 61 19 syl ( 𝑘 ∈ ( ( 0 ... if ( 𝑀𝑁 , 𝑁 , 𝑀 ) ) ∖ ( 0 ... 𝑀 ) ) → 𝑘 ∈ ℕ0 )
63 62 adantl ( ( ( 𝜑𝑧 ∈ ℂ ) ∧ 𝑘 ∈ ( ( 0 ... if ( 𝑀𝑁 , 𝑁 , 𝑀 ) ) ∖ ( 0 ... 𝑀 ) ) ) → 𝑘 ∈ ℕ0 )
64 nn0uz 0 = ( ℤ ‘ 0 )
65 peano2nn0 ( 𝑀 ∈ ℕ0 → ( 𝑀 + 1 ) ∈ ℕ0 )
66 3 65 syl ( 𝜑 → ( 𝑀 + 1 ) ∈ ℕ0 )
67 66 64 eleqtrdi ( 𝜑 → ( 𝑀 + 1 ) ∈ ( ℤ ‘ 0 ) )
68 uzsplit ( ( 𝑀 + 1 ) ∈ ( ℤ ‘ 0 ) → ( ℤ ‘ 0 ) = ( ( 0 ... ( ( 𝑀 + 1 ) − 1 ) ) ∪ ( ℤ ‘ ( 𝑀 + 1 ) ) ) )
69 67 68 syl ( 𝜑 → ( ℤ ‘ 0 ) = ( ( 0 ... ( ( 𝑀 + 1 ) − 1 ) ) ∪ ( ℤ ‘ ( 𝑀 + 1 ) ) ) )
70 64 69 syl5eq ( 𝜑 → ℕ0 = ( ( 0 ... ( ( 𝑀 + 1 ) − 1 ) ) ∪ ( ℤ ‘ ( 𝑀 + 1 ) ) ) )
71 3 nn0cnd ( 𝜑𝑀 ∈ ℂ )
72 ax-1cn 1 ∈ ℂ
73 pncan ( ( 𝑀 ∈ ℂ ∧ 1 ∈ ℂ ) → ( ( 𝑀 + 1 ) − 1 ) = 𝑀 )
74 71 72 73 sylancl ( 𝜑 → ( ( 𝑀 + 1 ) − 1 ) = 𝑀 )
75 74 oveq2d ( 𝜑 → ( 0 ... ( ( 𝑀 + 1 ) − 1 ) ) = ( 0 ... 𝑀 ) )
76 75 uneq1d ( 𝜑 → ( ( 0 ... ( ( 𝑀 + 1 ) − 1 ) ) ∪ ( ℤ ‘ ( 𝑀 + 1 ) ) ) = ( ( 0 ... 𝑀 ) ∪ ( ℤ ‘ ( 𝑀 + 1 ) ) ) )
77 70 76 eqtrd ( 𝜑 → ℕ0 = ( ( 0 ... 𝑀 ) ∪ ( ℤ ‘ ( 𝑀 + 1 ) ) ) )
78 77 ad2antrr ( ( ( 𝜑𝑧 ∈ ℂ ) ∧ 𝑘 ∈ ( ( 0 ... if ( 𝑀𝑁 , 𝑁 , 𝑀 ) ) ∖ ( 0 ... 𝑀 ) ) ) → ℕ0 = ( ( 0 ... 𝑀 ) ∪ ( ℤ ‘ ( 𝑀 + 1 ) ) ) )
79 63 78 eleqtrd ( ( ( 𝜑𝑧 ∈ ℂ ) ∧ 𝑘 ∈ ( ( 0 ... if ( 𝑀𝑁 , 𝑁 , 𝑀 ) ) ∖ ( 0 ... 𝑀 ) ) ) → 𝑘 ∈ ( ( 0 ... 𝑀 ) ∪ ( ℤ ‘ ( 𝑀 + 1 ) ) ) )
80 elun ( 𝑘 ∈ ( ( 0 ... 𝑀 ) ∪ ( ℤ ‘ ( 𝑀 + 1 ) ) ) ↔ ( 𝑘 ∈ ( 0 ... 𝑀 ) ∨ 𝑘 ∈ ( ℤ ‘ ( 𝑀 + 1 ) ) ) )
81 79 80 sylib ( ( ( 𝜑𝑧 ∈ ℂ ) ∧ 𝑘 ∈ ( ( 0 ... if ( 𝑀𝑁 , 𝑁 , 𝑀 ) ) ∖ ( 0 ... 𝑀 ) ) ) → ( 𝑘 ∈ ( 0 ... 𝑀 ) ∨ 𝑘 ∈ ( ℤ ‘ ( 𝑀 + 1 ) ) ) )
82 81 ord ( ( ( 𝜑𝑧 ∈ ℂ ) ∧ 𝑘 ∈ ( ( 0 ... if ( 𝑀𝑁 , 𝑁 , 𝑀 ) ) ∖ ( 0 ... 𝑀 ) ) ) → ( ¬ 𝑘 ∈ ( 0 ... 𝑀 ) → 𝑘 ∈ ( ℤ ‘ ( 𝑀 + 1 ) ) ) )
83 60 82 mpd ( ( ( 𝜑𝑧 ∈ ℂ ) ∧ 𝑘 ∈ ( ( 0 ... if ( 𝑀𝑁 , 𝑁 , 𝑀 ) ) ∖ ( 0 ... 𝑀 ) ) ) → 𝑘 ∈ ( ℤ ‘ ( 𝑀 + 1 ) ) )
84 5 ffund ( 𝜑 → Fun 𝐴 )
85 ssun2 ( ℤ ‘ ( 𝑀 + 1 ) ) ⊆ ( ( 0 ... ( ( 𝑀 + 1 ) − 1 ) ) ∪ ( ℤ ‘ ( 𝑀 + 1 ) ) )
86 85 70 sseqtrrid ( 𝜑 → ( ℤ ‘ ( 𝑀 + 1 ) ) ⊆ ℕ0 )
87 5 fdmd ( 𝜑 → dom 𝐴 = ℕ0 )
88 86 87 sseqtrrd ( 𝜑 → ( ℤ ‘ ( 𝑀 + 1 ) ) ⊆ dom 𝐴 )
89 funfvima2 ( ( Fun 𝐴 ∧ ( ℤ ‘ ( 𝑀 + 1 ) ) ⊆ dom 𝐴 ) → ( 𝑘 ∈ ( ℤ ‘ ( 𝑀 + 1 ) ) → ( 𝐴𝑘 ) ∈ ( 𝐴 “ ( ℤ ‘ ( 𝑀 + 1 ) ) ) ) )
90 84 88 89 syl2anc ( 𝜑 → ( 𝑘 ∈ ( ℤ ‘ ( 𝑀 + 1 ) ) → ( 𝐴𝑘 ) ∈ ( 𝐴 “ ( ℤ ‘ ( 𝑀 + 1 ) ) ) ) )
91 90 ad2antrr ( ( ( 𝜑𝑧 ∈ ℂ ) ∧ 𝑘 ∈ ( ( 0 ... if ( 𝑀𝑁 , 𝑁 , 𝑀 ) ) ∖ ( 0 ... 𝑀 ) ) ) → ( 𝑘 ∈ ( ℤ ‘ ( 𝑀 + 1 ) ) → ( 𝐴𝑘 ) ∈ ( 𝐴 “ ( ℤ ‘ ( 𝑀 + 1 ) ) ) ) )
92 83 91 mpd ( ( ( 𝜑𝑧 ∈ ℂ ) ∧ 𝑘 ∈ ( ( 0 ... if ( 𝑀𝑁 , 𝑁 , 𝑀 ) ) ∖ ( 0 ... 𝑀 ) ) ) → ( 𝐴𝑘 ) ∈ ( 𝐴 “ ( ℤ ‘ ( 𝑀 + 1 ) ) ) )
93 7 ad2antrr ( ( ( 𝜑𝑧 ∈ ℂ ) ∧ 𝑘 ∈ ( ( 0 ... if ( 𝑀𝑁 , 𝑁 , 𝑀 ) ) ∖ ( 0 ... 𝑀 ) ) ) → ( 𝐴 “ ( ℤ ‘ ( 𝑀 + 1 ) ) ) = { 0 } )
94 92 93 eleqtrd ( ( ( 𝜑𝑧 ∈ ℂ ) ∧ 𝑘 ∈ ( ( 0 ... if ( 𝑀𝑁 , 𝑁 , 𝑀 ) ) ∖ ( 0 ... 𝑀 ) ) ) → ( 𝐴𝑘 ) ∈ { 0 } )
95 elsni ( ( 𝐴𝑘 ) ∈ { 0 } → ( 𝐴𝑘 ) = 0 )
96 94 95 syl ( ( ( 𝜑𝑧 ∈ ℂ ) ∧ 𝑘 ∈ ( ( 0 ... if ( 𝑀𝑁 , 𝑁 , 𝑀 ) ) ∖ ( 0 ... 𝑀 ) ) ) → ( 𝐴𝑘 ) = 0 )
97 96 oveq1d ( ( ( 𝜑𝑧 ∈ ℂ ) ∧ 𝑘 ∈ ( ( 0 ... if ( 𝑀𝑁 , 𝑁 , 𝑀 ) ) ∖ ( 0 ... 𝑀 ) ) ) → ( ( 𝐴𝑘 ) · ( 𝑧𝑘 ) ) = ( 0 · ( 𝑧𝑘 ) ) )
98 62 23 sylan2 ( ( ( 𝜑𝑧 ∈ ℂ ) ∧ 𝑘 ∈ ( ( 0 ... if ( 𝑀𝑁 , 𝑁 , 𝑀 ) ) ∖ ( 0 ... 𝑀 ) ) ) → ( 𝑧𝑘 ) ∈ ℂ )
99 98 mul02d ( ( ( 𝜑𝑧 ∈ ℂ ) ∧ 𝑘 ∈ ( ( 0 ... if ( 𝑀𝑁 , 𝑁 , 𝑀 ) ) ∖ ( 0 ... 𝑀 ) ) ) → ( 0 · ( 𝑧𝑘 ) ) = 0 )
100 97 99 eqtrd ( ( ( 𝜑𝑧 ∈ ℂ ) ∧ 𝑘 ∈ ( ( 0 ... if ( 𝑀𝑁 , 𝑁 , 𝑀 ) ) ∖ ( 0 ... 𝑀 ) ) ) → ( ( 𝐴𝑘 ) · ( 𝑧𝑘 ) ) = 0 )
101 56 58 100 18 fsumss ( ( 𝜑𝑧 ∈ ℂ ) → Σ 𝑘 ∈ ( 0 ... 𝑀 ) ( ( 𝐴𝑘 ) · ( 𝑧𝑘 ) ) = Σ 𝑘 ∈ ( 0 ... if ( 𝑀𝑁 , 𝑁 , 𝑀 ) ) ( ( 𝐴𝑘 ) · ( 𝑧𝑘 ) ) )
102 4 nn0zd ( 𝜑𝑁 ∈ ℤ )
103 max2 ( ( 𝑀 ∈ ℝ ∧ 𝑁 ∈ ℝ ) → 𝑁 ≤ if ( 𝑀𝑁 , 𝑁 , 𝑀 ) )
104 48 49 103 syl2anc ( 𝜑𝑁 ≤ if ( 𝑀𝑁 , 𝑁 , 𝑀 ) )
105 eluz2 ( if ( 𝑀𝑁 , 𝑁 , 𝑀 ) ∈ ( ℤ𝑁 ) ↔ ( 𝑁 ∈ ℤ ∧ if ( 𝑀𝑁 , 𝑁 , 𝑀 ) ∈ ℤ ∧ 𝑁 ≤ if ( 𝑀𝑁 , 𝑁 , 𝑀 ) ) )
106 102 47 104 105 syl3anbrc ( 𝜑 → if ( 𝑀𝑁 , 𝑁 , 𝑀 ) ∈ ( ℤ𝑁 ) )
107 fzss2 ( if ( 𝑀𝑁 , 𝑁 , 𝑀 ) ∈ ( ℤ𝑁 ) → ( 0 ... 𝑁 ) ⊆ ( 0 ... if ( 𝑀𝑁 , 𝑁 , 𝑀 ) ) )
108 106 107 syl ( 𝜑 → ( 0 ... 𝑁 ) ⊆ ( 0 ... if ( 𝑀𝑁 , 𝑁 , 𝑀 ) ) )
109 108 adantr ( ( 𝜑𝑧 ∈ ℂ ) → ( 0 ... 𝑁 ) ⊆ ( 0 ... if ( 𝑀𝑁 , 𝑁 , 𝑀 ) ) )
110 elfznn0 ( 𝑘 ∈ ( 0 ... 𝑁 ) → 𝑘 ∈ ℕ0 )
111 110 28 sylan2 ( ( ( 𝜑𝑧 ∈ ℂ ) ∧ 𝑘 ∈ ( 0 ... 𝑁 ) ) → ( ( 𝐵𝑘 ) · ( 𝑧𝑘 ) ) ∈ ℂ )
112 eldifn ( 𝑘 ∈ ( ( 0 ... if ( 𝑀𝑁 , 𝑁 , 𝑀 ) ) ∖ ( 0 ... 𝑁 ) ) → ¬ 𝑘 ∈ ( 0 ... 𝑁 ) )
113 112 adantl ( ( ( 𝜑𝑧 ∈ ℂ ) ∧ 𝑘 ∈ ( ( 0 ... if ( 𝑀𝑁 , 𝑁 , 𝑀 ) ) ∖ ( 0 ... 𝑁 ) ) ) → ¬ 𝑘 ∈ ( 0 ... 𝑁 ) )
114 eldifi ( 𝑘 ∈ ( ( 0 ... if ( 𝑀𝑁 , 𝑁 , 𝑀 ) ) ∖ ( 0 ... 𝑁 ) ) → 𝑘 ∈ ( 0 ... if ( 𝑀𝑁 , 𝑁 , 𝑀 ) ) )
115 114 19 syl ( 𝑘 ∈ ( ( 0 ... if ( 𝑀𝑁 , 𝑁 , 𝑀 ) ) ∖ ( 0 ... 𝑁 ) ) → 𝑘 ∈ ℕ0 )
116 115 adantl ( ( ( 𝜑𝑧 ∈ ℂ ) ∧ 𝑘 ∈ ( ( 0 ... if ( 𝑀𝑁 , 𝑁 , 𝑀 ) ) ∖ ( 0 ... 𝑁 ) ) ) → 𝑘 ∈ ℕ0 )
117 peano2nn0 ( 𝑁 ∈ ℕ0 → ( 𝑁 + 1 ) ∈ ℕ0 )
118 4 117 syl ( 𝜑 → ( 𝑁 + 1 ) ∈ ℕ0 )
119 118 64 eleqtrdi ( 𝜑 → ( 𝑁 + 1 ) ∈ ( ℤ ‘ 0 ) )
120 uzsplit ( ( 𝑁 + 1 ) ∈ ( ℤ ‘ 0 ) → ( ℤ ‘ 0 ) = ( ( 0 ... ( ( 𝑁 + 1 ) − 1 ) ) ∪ ( ℤ ‘ ( 𝑁 + 1 ) ) ) )
121 119 120 syl ( 𝜑 → ( ℤ ‘ 0 ) = ( ( 0 ... ( ( 𝑁 + 1 ) − 1 ) ) ∪ ( ℤ ‘ ( 𝑁 + 1 ) ) ) )
122 64 121 syl5eq ( 𝜑 → ℕ0 = ( ( 0 ... ( ( 𝑁 + 1 ) − 1 ) ) ∪ ( ℤ ‘ ( 𝑁 + 1 ) ) ) )
123 4 nn0cnd ( 𝜑𝑁 ∈ ℂ )
124 pncan ( ( 𝑁 ∈ ℂ ∧ 1 ∈ ℂ ) → ( ( 𝑁 + 1 ) − 1 ) = 𝑁 )
125 123 72 124 sylancl ( 𝜑 → ( ( 𝑁 + 1 ) − 1 ) = 𝑁 )
126 125 oveq2d ( 𝜑 → ( 0 ... ( ( 𝑁 + 1 ) − 1 ) ) = ( 0 ... 𝑁 ) )
127 126 uneq1d ( 𝜑 → ( ( 0 ... ( ( 𝑁 + 1 ) − 1 ) ) ∪ ( ℤ ‘ ( 𝑁 + 1 ) ) ) = ( ( 0 ... 𝑁 ) ∪ ( ℤ ‘ ( 𝑁 + 1 ) ) ) )
128 122 127 eqtrd ( 𝜑 → ℕ0 = ( ( 0 ... 𝑁 ) ∪ ( ℤ ‘ ( 𝑁 + 1 ) ) ) )
129 128 ad2antrr ( ( ( 𝜑𝑧 ∈ ℂ ) ∧ 𝑘 ∈ ( ( 0 ... if ( 𝑀𝑁 , 𝑁 , 𝑀 ) ) ∖ ( 0 ... 𝑁 ) ) ) → ℕ0 = ( ( 0 ... 𝑁 ) ∪ ( ℤ ‘ ( 𝑁 + 1 ) ) ) )
130 116 129 eleqtrd ( ( ( 𝜑𝑧 ∈ ℂ ) ∧ 𝑘 ∈ ( ( 0 ... if ( 𝑀𝑁 , 𝑁 , 𝑀 ) ) ∖ ( 0 ... 𝑁 ) ) ) → 𝑘 ∈ ( ( 0 ... 𝑁 ) ∪ ( ℤ ‘ ( 𝑁 + 1 ) ) ) )
131 elun ( 𝑘 ∈ ( ( 0 ... 𝑁 ) ∪ ( ℤ ‘ ( 𝑁 + 1 ) ) ) ↔ ( 𝑘 ∈ ( 0 ... 𝑁 ) ∨ 𝑘 ∈ ( ℤ ‘ ( 𝑁 + 1 ) ) ) )
132 130 131 sylib ( ( ( 𝜑𝑧 ∈ ℂ ) ∧ 𝑘 ∈ ( ( 0 ... if ( 𝑀𝑁 , 𝑁 , 𝑀 ) ) ∖ ( 0 ... 𝑁 ) ) ) → ( 𝑘 ∈ ( 0 ... 𝑁 ) ∨ 𝑘 ∈ ( ℤ ‘ ( 𝑁 + 1 ) ) ) )
133 132 ord ( ( ( 𝜑𝑧 ∈ ℂ ) ∧ 𝑘 ∈ ( ( 0 ... if ( 𝑀𝑁 , 𝑁 , 𝑀 ) ) ∖ ( 0 ... 𝑁 ) ) ) → ( ¬ 𝑘 ∈ ( 0 ... 𝑁 ) → 𝑘 ∈ ( ℤ ‘ ( 𝑁 + 1 ) ) ) )
134 113 133 mpd ( ( ( 𝜑𝑧 ∈ ℂ ) ∧ 𝑘 ∈ ( ( 0 ... if ( 𝑀𝑁 , 𝑁 , 𝑀 ) ) ∖ ( 0 ... 𝑁 ) ) ) → 𝑘 ∈ ( ℤ ‘ ( 𝑁 + 1 ) ) )
135 6 ffund ( 𝜑 → Fun 𝐵 )
136 ssun2 ( ℤ ‘ ( 𝑁 + 1 ) ) ⊆ ( ( 0 ... ( ( 𝑁 + 1 ) − 1 ) ) ∪ ( ℤ ‘ ( 𝑁 + 1 ) ) )
137 136 122 sseqtrrid ( 𝜑 → ( ℤ ‘ ( 𝑁 + 1 ) ) ⊆ ℕ0 )
138 6 fdmd ( 𝜑 → dom 𝐵 = ℕ0 )
139 137 138 sseqtrrd ( 𝜑 → ( ℤ ‘ ( 𝑁 + 1 ) ) ⊆ dom 𝐵 )
140 funfvima2 ( ( Fun 𝐵 ∧ ( ℤ ‘ ( 𝑁 + 1 ) ) ⊆ dom 𝐵 ) → ( 𝑘 ∈ ( ℤ ‘ ( 𝑁 + 1 ) ) → ( 𝐵𝑘 ) ∈ ( 𝐵 “ ( ℤ ‘ ( 𝑁 + 1 ) ) ) ) )
141 135 139 140 syl2anc ( 𝜑 → ( 𝑘 ∈ ( ℤ ‘ ( 𝑁 + 1 ) ) → ( 𝐵𝑘 ) ∈ ( 𝐵 “ ( ℤ ‘ ( 𝑁 + 1 ) ) ) ) )
142 141 ad2antrr ( ( ( 𝜑𝑧 ∈ ℂ ) ∧ 𝑘 ∈ ( ( 0 ... if ( 𝑀𝑁 , 𝑁 , 𝑀 ) ) ∖ ( 0 ... 𝑁 ) ) ) → ( 𝑘 ∈ ( ℤ ‘ ( 𝑁 + 1 ) ) → ( 𝐵𝑘 ) ∈ ( 𝐵 “ ( ℤ ‘ ( 𝑁 + 1 ) ) ) ) )
143 134 142 mpd ( ( ( 𝜑𝑧 ∈ ℂ ) ∧ 𝑘 ∈ ( ( 0 ... if ( 𝑀𝑁 , 𝑁 , 𝑀 ) ) ∖ ( 0 ... 𝑁 ) ) ) → ( 𝐵𝑘 ) ∈ ( 𝐵 “ ( ℤ ‘ ( 𝑁 + 1 ) ) ) )
144 8 ad2antrr ( ( ( 𝜑𝑧 ∈ ℂ ) ∧ 𝑘 ∈ ( ( 0 ... if ( 𝑀𝑁 , 𝑁 , 𝑀 ) ) ∖ ( 0 ... 𝑁 ) ) ) → ( 𝐵 “ ( ℤ ‘ ( 𝑁 + 1 ) ) ) = { 0 } )
145 143 144 eleqtrd ( ( ( 𝜑𝑧 ∈ ℂ ) ∧ 𝑘 ∈ ( ( 0 ... if ( 𝑀𝑁 , 𝑁 , 𝑀 ) ) ∖ ( 0 ... 𝑁 ) ) ) → ( 𝐵𝑘 ) ∈ { 0 } )
146 elsni ( ( 𝐵𝑘 ) ∈ { 0 } → ( 𝐵𝑘 ) = 0 )
147 145 146 syl ( ( ( 𝜑𝑧 ∈ ℂ ) ∧ 𝑘 ∈ ( ( 0 ... if ( 𝑀𝑁 , 𝑁 , 𝑀 ) ) ∖ ( 0 ... 𝑁 ) ) ) → ( 𝐵𝑘 ) = 0 )
148 147 oveq1d ( ( ( 𝜑𝑧 ∈ ℂ ) ∧ 𝑘 ∈ ( ( 0 ... if ( 𝑀𝑁 , 𝑁 , 𝑀 ) ) ∖ ( 0 ... 𝑁 ) ) ) → ( ( 𝐵𝑘 ) · ( 𝑧𝑘 ) ) = ( 0 · ( 𝑧𝑘 ) ) )
149 115 23 sylan2 ( ( ( 𝜑𝑧 ∈ ℂ ) ∧ 𝑘 ∈ ( ( 0 ... if ( 𝑀𝑁 , 𝑁 , 𝑀 ) ) ∖ ( 0 ... 𝑁 ) ) ) → ( 𝑧𝑘 ) ∈ ℂ )
150 149 mul02d ( ( ( 𝜑𝑧 ∈ ℂ ) ∧ 𝑘 ∈ ( ( 0 ... if ( 𝑀𝑁 , 𝑁 , 𝑀 ) ) ∖ ( 0 ... 𝑁 ) ) ) → ( 0 · ( 𝑧𝑘 ) ) = 0 )
151 148 150 eqtrd ( ( ( 𝜑𝑧 ∈ ℂ ) ∧ 𝑘 ∈ ( ( 0 ... if ( 𝑀𝑁 , 𝑁 , 𝑀 ) ) ∖ ( 0 ... 𝑁 ) ) ) → ( ( 𝐵𝑘 ) · ( 𝑧𝑘 ) ) = 0 )
152 109 111 151 18 fsumss ( ( 𝜑𝑧 ∈ ℂ ) → Σ 𝑘 ∈ ( 0 ... 𝑁 ) ( ( 𝐵𝑘 ) · ( 𝑧𝑘 ) ) = Σ 𝑘 ∈ ( 0 ... if ( 𝑀𝑁 , 𝑁 , 𝑀 ) ) ( ( 𝐵𝑘 ) · ( 𝑧𝑘 ) ) )
153 101 152 oveq12d ( ( 𝜑𝑧 ∈ ℂ ) → ( Σ 𝑘 ∈ ( 0 ... 𝑀 ) ( ( 𝐴𝑘 ) · ( 𝑧𝑘 ) ) + Σ 𝑘 ∈ ( 0 ... 𝑁 ) ( ( 𝐵𝑘 ) · ( 𝑧𝑘 ) ) ) = ( Σ 𝑘 ∈ ( 0 ... if ( 𝑀𝑁 , 𝑁 , 𝑀 ) ) ( ( 𝐴𝑘 ) · ( 𝑧𝑘 ) ) + Σ 𝑘 ∈ ( 0 ... if ( 𝑀𝑁 , 𝑁 , 𝑀 ) ) ( ( 𝐵𝑘 ) · ( 𝑧𝑘 ) ) ) )
154 30 44 153 3eqtr4d ( ( 𝜑𝑧 ∈ ℂ ) → Σ 𝑘 ∈ ( 0 ... if ( 𝑀𝑁 , 𝑁 , 𝑀 ) ) ( ( ( 𝐴f + 𝐵 ) ‘ 𝑘 ) · ( 𝑧𝑘 ) ) = ( Σ 𝑘 ∈ ( 0 ... 𝑀 ) ( ( 𝐴𝑘 ) · ( 𝑧𝑘 ) ) + Σ 𝑘 ∈ ( 0 ... 𝑁 ) ( ( 𝐵𝑘 ) · ( 𝑧𝑘 ) ) ) )
155 154 mpteq2dva ( 𝜑 → ( 𝑧 ∈ ℂ ↦ Σ 𝑘 ∈ ( 0 ... if ( 𝑀𝑁 , 𝑁 , 𝑀 ) ) ( ( ( 𝐴f + 𝐵 ) ‘ 𝑘 ) · ( 𝑧𝑘 ) ) ) = ( 𝑧 ∈ ℂ ↦ ( Σ 𝑘 ∈ ( 0 ... 𝑀 ) ( ( 𝐴𝑘 ) · ( 𝑧𝑘 ) ) + Σ 𝑘 ∈ ( 0 ... 𝑁 ) ( ( 𝐵𝑘 ) · ( 𝑧𝑘 ) ) ) ) )
156 17 155 eqtr4d ( 𝜑 → ( 𝐹f + 𝐺 ) = ( 𝑧 ∈ ℂ ↦ Σ 𝑘 ∈ ( 0 ... if ( 𝑀𝑁 , 𝑁 , 𝑀 ) ) ( ( ( 𝐴f + 𝐵 ) ‘ 𝑘 ) · ( 𝑧𝑘 ) ) ) )