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 ffvelcdmda ⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ ℂ ) ∧ 𝑘 ∈ ℕ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 ffvelcdmda ⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ ℂ ) ∧ 𝑘 ∈ ℕ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 eqtrid ⊢ ( 𝜑 → ℕ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 eqtrid ⊢ ( 𝜑 → ℕ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 + 𝐵 ) ‘ 𝑘 ) · ( 𝑧 ↑ 𝑘 ) ) ) )