Metamath Proof Explorer

Theorem coeeulem

Description: Lemma for coeeu . (Contributed by Mario Carneiro, 22-Jul-2014)

Ref Expression
Hypotheses coeeu.1 ⊢ ( 𝜑 → 𝐹 ∈ ( Poly ‘ 𝑆 ) )
coeeu.2 ⊢ ( 𝜑 → 𝐴 ∈ ( ℂ ↑m ℕ0 ) )
coeeu.3 ⊢ ( 𝜑 → 𝐵 ∈ ( ℂ ↑m ℕ0 ) )
coeeu.4 ⊢ ( 𝜑 → 𝑀 ∈ ℕ0 )
coeeu.5 ⊢ ( 𝜑 → 𝑁 ∈ ℕ0 )
coeeu.6 ⊢ ( 𝜑 → ( 𝐴 “ ( ℤ≥ ‘ ( 𝑀 + 1 ) ) ) = { 0 } )
coeeu.7 ⊢ ( 𝜑 → ( 𝐵 “ ( ℤ≥ ‘ ( 𝑁 + 1 ) ) ) = { 0 } )
coeeu.8 ⊢ ( 𝜑 → 𝐹 = ( 𝑧 ∈ ℂ ↦ Σ 𝑘 ∈ ( 0 ... 𝑀 ) ( ( 𝐴 ‘ 𝑘 ) · ( 𝑧 ↑ 𝑘 ) ) ) )
coeeu.9 ⊢ ( 𝜑 → 𝐹 = ( 𝑧 ∈ ℂ ↦ Σ 𝑘 ∈ ( 0 ... 𝑁 ) ( ( 𝐵 ‘ 𝑘 ) · ( 𝑧 ↑ 𝑘 ) ) ) )
Assertion coeeulem ( 𝜑 → 𝐴 = 𝐵 )

Proof

Step Hyp Ref Expression
1 coeeu.1 ⊢ ( 𝜑 → 𝐹 ∈ ( Poly ‘ 𝑆 ) )
2 coeeu.2 ⊢ ( 𝜑 → 𝐴 ∈ ( ℂ ↑m ℕ0 ) )
3 coeeu.3 ⊢ ( 𝜑 → 𝐵 ∈ ( ℂ ↑m ℕ0 ) )
4 coeeu.4 ⊢ ( 𝜑 → 𝑀 ∈ ℕ0 )
5 coeeu.5 ⊢ ( 𝜑 → 𝑁 ∈ ℕ0 )
6 coeeu.6 ⊢ ( 𝜑 → ( 𝐴 “ ( ℤ≥ ‘ ( 𝑀 + 1 ) ) ) = { 0 } )
7 coeeu.7 ⊢ ( 𝜑 → ( 𝐵 “ ( ℤ≥ ‘ ( 𝑁 + 1 ) ) ) = { 0 } )
8 coeeu.8 ⊢ ( 𝜑 → 𝐹 = ( 𝑧 ∈ ℂ ↦ Σ 𝑘 ∈ ( 0 ... 𝑀 ) ( ( 𝐴 ‘ 𝑘 ) · ( 𝑧 ↑ 𝑘 ) ) ) )
9 coeeu.9 ⊢ ( 𝜑 → 𝐹 = ( 𝑧 ∈ ℂ ↦ Σ 𝑘 ∈ ( 0 ... 𝑁 ) ( ( 𝐵 ‘ 𝑘 ) · ( 𝑧 ↑ 𝑘 ) ) ) )
10 ssidd ⊢ ( 𝜑 → ℂ ⊆ ℂ )
11 4 5 nn0addcld ⊢ ( 𝜑 → ( 𝑀 + 𝑁 ) ∈ ℕ0 )
12 subcl ⊢ ( ( 𝑥 ∈ ℂ ∧ 𝑦 ∈ ℂ ) → ( 𝑥 − 𝑦 ) ∈ ℂ )
13 12 adantl ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ℂ ∧ 𝑦 ∈ ℂ ) ) → ( 𝑥 − 𝑦 ) ∈ ℂ )
14 cnex ⊢ ℂ ∈ V
15 nn0ex ⊢ ℕ0 ∈ V
16 14 15 elmap ⊢ ( 𝐴 ∈ ( ℂ ↑m ℕ0 ) ↔ 𝐴 : ℕ0 ⟶ ℂ )
17 2 16 sylib ⊢ ( 𝜑 → 𝐴 : ℕ0 ⟶ ℂ )
18 14 15 elmap ⊢ ( 𝐵 ∈ ( ℂ ↑m ℕ0 ) ↔ 𝐵 : ℕ0 ⟶ ℂ )
19 3 18 sylib ⊢ ( 𝜑 → 𝐵 : ℕ0 ⟶ ℂ )
20 15 a1i ⊢ ( 𝜑 → ℕ0 ∈ V )
21 inidm ⊢ ( ℕ0 ∩ ℕ0 ) = ℕ0
22 13 17 19 20 20 21 off ⊢ ( 𝜑 → ( 𝐴 ∘f − 𝐵 ) : ℕ0 ⟶ ℂ )
23 14 15 elmap ⊢ ( ( 𝐴 ∘f − 𝐵 ) ∈ ( ℂ ↑m ℕ0 ) ↔ ( 𝐴 ∘f − 𝐵 ) : ℕ0 ⟶ ℂ )
24 22 23 sylibr ⊢ ( 𝜑 → ( 𝐴 ∘f − 𝐵 ) ∈ ( ℂ ↑m ℕ0 ) )
25 0cn ⊢ 0 ∈ ℂ
26 snssi ⊢ ( 0 ∈ ℂ → { 0 } ⊆ ℂ )
27 25 26 ax-mp ⊢ { 0 } ⊆ ℂ
28 ssequn2 ⊢ ( { 0 } ⊆ ℂ ↔ ( ℂ ∪ { 0 } ) = ℂ )
29 27 28 mpbi ⊢ ( ℂ ∪ { 0 } ) = ℂ
30 29 oveq1i ⊢ ( ( ℂ ∪ { 0 } ) ↑m ℕ0 ) = ( ℂ ↑m ℕ0 )
31 24 30 eleqtrrdi ⊢ ( 𝜑 → ( 𝐴 ∘f − 𝐵 ) ∈ ( ( ℂ ∪ { 0 } ) ↑m ℕ0 ) )
32 11 nn0red ⊢ ( 𝜑 → ( 𝑀 + 𝑁 ) ∈ ℝ )
33 nn0re ⊢ ( 𝑘 ∈ ℕ0 → 𝑘 ∈ ℝ )
34 ltnle ⊢ ( ( ( 𝑀 + 𝑁 ) ∈ ℝ ∧ 𝑘 ∈ ℝ ) → ( ( 𝑀 + 𝑁 ) < 𝑘 ↔ ¬ 𝑘 ≤ ( 𝑀 + 𝑁 ) ) )
35 32 33 34 syl2an ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ0 ) → ( ( 𝑀 + 𝑁 ) < 𝑘 ↔ ¬ 𝑘 ≤ ( 𝑀 + 𝑁 ) ) )
36 17 ffnd ⊢ ( 𝜑 → 𝐴 Fn ℕ0 )
37 19 ffnd ⊢ ( 𝜑 → 𝐵 Fn ℕ0 )
38 eqidd ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ0 ) → ( 𝐴 ‘ 𝑘 ) = ( 𝐴 ‘ 𝑘 ) )
39 eqidd ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ0 ) → ( 𝐵 ‘ 𝑘 ) = ( 𝐵 ‘ 𝑘 ) )
40 36 37 20 20 21 38 39 ofval ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ0 ) → ( ( 𝐴 ∘f − 𝐵 ) ‘ 𝑘 ) = ( ( 𝐴 ‘ 𝑘 ) − ( 𝐵 ‘ 𝑘 ) ) )
41 40 adantrr ⊢ ( ( 𝜑 ∧ ( 𝑘 ∈ ℕ0 ∧ ( 𝑀 + 𝑁 ) < 𝑘 ) ) → ( ( 𝐴 ∘f − 𝐵 ) ‘ 𝑘 ) = ( ( 𝐴 ‘ 𝑘 ) − ( 𝐵 ‘ 𝑘 ) ) )
42 4 nn0red ⊢ ( 𝜑 → 𝑀 ∈ ℝ )
43 42 adantr ⊢ ( ( 𝜑 ∧ ( 𝑘 ∈ ℕ0 ∧ ( 𝑀 + 𝑁 ) < 𝑘 ) ) → 𝑀 ∈ ℝ )
44 32 adantr ⊢ ( ( 𝜑 ∧ ( 𝑘 ∈ ℕ0 ∧ ( 𝑀 + 𝑁 ) < 𝑘 ) ) → ( 𝑀 + 𝑁 ) ∈ ℝ )
45 33 adantl ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ0 ) → 𝑘 ∈ ℝ )
46 45 adantrr ⊢ ( ( 𝜑 ∧ ( 𝑘 ∈ ℕ0 ∧ ( 𝑀 + 𝑁 ) < 𝑘 ) ) → 𝑘 ∈ ℝ )
47 4 nn0cnd ⊢ ( 𝜑 → 𝑀 ∈ ℂ )
48 5 nn0cnd ⊢ ( 𝜑 → 𝑁 ∈ ℂ )
49 47 48 addcomd ⊢ ( 𝜑 → ( 𝑀 + 𝑁 ) = ( 𝑁 + 𝑀 ) )
50 nn0uz ⊢ ℕ0 = ( ℤ≥ ‘ 0 )
51 5 50 eleqtrdi ⊢ ( 𝜑 → 𝑁 ∈ ( ℤ≥ ‘ 0 ) )
52 4 nn0zd ⊢ ( 𝜑 → 𝑀 ∈ ℤ )
53 eluzadd ⊢ ( ( 𝑁 ∈ ( ℤ≥ ‘ 0 ) ∧ 𝑀 ∈ ℤ ) → ( 𝑁 + 𝑀 ) ∈ ( ℤ≥ ‘ ( 0 + 𝑀 ) ) )
54 51 52 53 syl2anc ⊢ ( 𝜑 → ( 𝑁 + 𝑀 ) ∈ ( ℤ≥ ‘ ( 0 + 𝑀 ) ) )
55 49 54 eqeltrd ⊢ ( 𝜑 → ( 𝑀 + 𝑁 ) ∈ ( ℤ≥ ‘ ( 0 + 𝑀 ) ) )
56 47 addlidd ⊢ ( 𝜑 → ( 0 + 𝑀 ) = 𝑀 )
57 56 fveq2d ⊢ ( 𝜑 → ( ℤ≥ ‘ ( 0 + 𝑀 ) ) = ( ℤ≥ ‘ 𝑀 ) )
58 55 57 eleqtrd ⊢ ( 𝜑 → ( 𝑀 + 𝑁 ) ∈ ( ℤ≥ ‘ 𝑀 ) )
59 eluzle ⊢ ( ( 𝑀 + 𝑁 ) ∈ ( ℤ≥ ‘ 𝑀 ) → 𝑀 ≤ ( 𝑀 + 𝑁 ) )
60 58 59 syl ⊢ ( 𝜑 → 𝑀 ≤ ( 𝑀 + 𝑁 ) )
61 60 adantr ⊢ ( ( 𝜑 ∧ ( 𝑘 ∈ ℕ0 ∧ ( 𝑀 + 𝑁 ) < 𝑘 ) ) → 𝑀 ≤ ( 𝑀 + 𝑁 ) )
62 simprr ⊢ ( ( 𝜑 ∧ ( 𝑘 ∈ ℕ0 ∧ ( 𝑀 + 𝑁 ) < 𝑘 ) ) → ( 𝑀 + 𝑁 ) < 𝑘 )
63 43 44 46 61 62 lelttrd ⊢ ( ( 𝜑 ∧ ( 𝑘 ∈ ℕ0 ∧ ( 𝑀 + 𝑁 ) < 𝑘 ) ) → 𝑀 < 𝑘 )
64 43 46 ltnled ⊢ ( ( 𝜑 ∧ ( 𝑘 ∈ ℕ0 ∧ ( 𝑀 + 𝑁 ) < 𝑘 ) ) → ( 𝑀 < 𝑘 ↔ ¬ 𝑘 ≤ 𝑀 ) )
65 63 64 mpbid ⊢ ( ( 𝜑 ∧ ( 𝑘 ∈ ℕ0 ∧ ( 𝑀 + 𝑁 ) < 𝑘 ) ) → ¬ 𝑘 ≤ 𝑀 )
66 plyco0 ⊢ ( ( 𝑀 ∈ ℕ0 ∧ 𝐴 : ℕ0 ⟶ ℂ ) → ( ( 𝐴 “ ( ℤ≥ ‘ ( 𝑀 + 1 ) ) ) = { 0 } ↔ ∀ 𝑘 ∈ ℕ0 ( ( 𝐴 ‘ 𝑘 ) ≠ 0 → 𝑘 ≤ 𝑀 ) ) )
67 4 17 66 syl2anc ⊢ ( 𝜑 → ( ( 𝐴 “ ( ℤ≥ ‘ ( 𝑀 + 1 ) ) ) = { 0 } ↔ ∀ 𝑘 ∈ ℕ0 ( ( 𝐴 ‘ 𝑘 ) ≠ 0 → 𝑘 ≤ 𝑀 ) ) )
68 6 67 mpbid ⊢ ( 𝜑 → ∀ 𝑘 ∈ ℕ0 ( ( 𝐴 ‘ 𝑘 ) ≠ 0 → 𝑘 ≤ 𝑀 ) )
69 68 r19.21bi ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ0 ) → ( ( 𝐴 ‘ 𝑘 ) ≠ 0 → 𝑘 ≤ 𝑀 ) )
70 69 adantrr ⊢ ( ( 𝜑 ∧ ( 𝑘 ∈ ℕ0 ∧ ( 𝑀 + 𝑁 ) < 𝑘 ) ) → ( ( 𝐴 ‘ 𝑘 ) ≠ 0 → 𝑘 ≤ 𝑀 ) )
71 70 necon1bd ⊢ ( ( 𝜑 ∧ ( 𝑘 ∈ ℕ0 ∧ ( 𝑀 + 𝑁 ) < 𝑘 ) ) → ( ¬ 𝑘 ≤ 𝑀 → ( 𝐴 ‘ 𝑘 ) = 0 ) )
72 65 71 mpd ⊢ ( ( 𝜑 ∧ ( 𝑘 ∈ ℕ0 ∧ ( 𝑀 + 𝑁 ) < 𝑘 ) ) → ( 𝐴 ‘ 𝑘 ) = 0 )
73 5 nn0red ⊢ ( 𝜑 → 𝑁 ∈ ℝ )
74 73 adantr ⊢ ( ( 𝜑 ∧ ( 𝑘 ∈ ℕ0 ∧ ( 𝑀 + 𝑁 ) < 𝑘 ) ) → 𝑁 ∈ ℝ )
75 4 50 eleqtrdi ⊢ ( 𝜑 → 𝑀 ∈ ( ℤ≥ ‘ 0 ) )
76 5 nn0zd ⊢ ( 𝜑 → 𝑁 ∈ ℤ )
77 eluzadd ⊢ ( ( 𝑀 ∈ ( ℤ≥ ‘ 0 ) ∧ 𝑁 ∈ ℤ ) → ( 𝑀 + 𝑁 ) ∈ ( ℤ≥ ‘ ( 0 + 𝑁 ) ) )
78 75 76 77 syl2anc ⊢ ( 𝜑 → ( 𝑀 + 𝑁 ) ∈ ( ℤ≥ ‘ ( 0 + 𝑁 ) ) )
79 48 addlidd ⊢ ( 𝜑 → ( 0 + 𝑁 ) = 𝑁 )
80 79 fveq2d ⊢ ( 𝜑 → ( ℤ≥ ‘ ( 0 + 𝑁 ) ) = ( ℤ≥ ‘ 𝑁 ) )
81 78 80 eleqtrd ⊢ ( 𝜑 → ( 𝑀 + 𝑁 ) ∈ ( ℤ≥ ‘ 𝑁 ) )
82 eluzle ⊢ ( ( 𝑀 + 𝑁 ) ∈ ( ℤ≥ ‘ 𝑁 ) → 𝑁 ≤ ( 𝑀 + 𝑁 ) )
83 81 82 syl ⊢ ( 𝜑 → 𝑁 ≤ ( 𝑀 + 𝑁 ) )
84 83 adantr ⊢ ( ( 𝜑 ∧ ( 𝑘 ∈ ℕ0 ∧ ( 𝑀 + 𝑁 ) < 𝑘 ) ) → 𝑁 ≤ ( 𝑀 + 𝑁 ) )
85 74 44 46 84 62 lelttrd ⊢ ( ( 𝜑 ∧ ( 𝑘 ∈ ℕ0 ∧ ( 𝑀 + 𝑁 ) < 𝑘 ) ) → 𝑁 < 𝑘 )
86 74 46 ltnled ⊢ ( ( 𝜑 ∧ ( 𝑘 ∈ ℕ0 ∧ ( 𝑀 + 𝑁 ) < 𝑘 ) ) → ( 𝑁 < 𝑘 ↔ ¬ 𝑘 ≤ 𝑁 ) )
87 85 86 mpbid ⊢ ( ( 𝜑 ∧ ( 𝑘 ∈ ℕ0 ∧ ( 𝑀 + 𝑁 ) < 𝑘 ) ) → ¬ 𝑘 ≤ 𝑁 )
88 plyco0 ⊢ ( ( 𝑁 ∈ ℕ0 ∧ 𝐵 : ℕ0 ⟶ ℂ ) → ( ( 𝐵 “ ( ℤ≥ ‘ ( 𝑁 + 1 ) ) ) = { 0 } ↔ ∀ 𝑘 ∈ ℕ0 ( ( 𝐵 ‘ 𝑘 ) ≠ 0 → 𝑘 ≤ 𝑁 ) ) )
89 5 19 88 syl2anc ⊢ ( 𝜑 → ( ( 𝐵 “ ( ℤ≥ ‘ ( 𝑁 + 1 ) ) ) = { 0 } ↔ ∀ 𝑘 ∈ ℕ0 ( ( 𝐵 ‘ 𝑘 ) ≠ 0 → 𝑘 ≤ 𝑁 ) ) )
90 7 89 mpbid ⊢ ( 𝜑 → ∀ 𝑘 ∈ ℕ0 ( ( 𝐵 ‘ 𝑘 ) ≠ 0 → 𝑘 ≤ 𝑁 ) )
91 90 r19.21bi ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ0 ) → ( ( 𝐵 ‘ 𝑘 ) ≠ 0 → 𝑘 ≤ 𝑁 ) )
92 91 adantrr ⊢ ( ( 𝜑 ∧ ( 𝑘 ∈ ℕ0 ∧ ( 𝑀 + 𝑁 ) < 𝑘 ) ) → ( ( 𝐵 ‘ 𝑘 ) ≠ 0 → 𝑘 ≤ 𝑁 ) )
93 92 necon1bd ⊢ ( ( 𝜑 ∧ ( 𝑘 ∈ ℕ0 ∧ ( 𝑀 + 𝑁 ) < 𝑘 ) ) → ( ¬ 𝑘 ≤ 𝑁 → ( 𝐵 ‘ 𝑘 ) = 0 ) )
94 87 93 mpd ⊢ ( ( 𝜑 ∧ ( 𝑘 ∈ ℕ0 ∧ ( 𝑀 + 𝑁 ) < 𝑘 ) ) → ( 𝐵 ‘ 𝑘 ) = 0 )
95 72 94 oveq12d ⊢ ( ( 𝜑 ∧ ( 𝑘 ∈ ℕ0 ∧ ( 𝑀 + 𝑁 ) < 𝑘 ) ) → ( ( 𝐴 ‘ 𝑘 ) − ( 𝐵 ‘ 𝑘 ) ) = ( 0 − 0 ) )
96 0m0e0 ⊢ ( 0 − 0 ) = 0
97 95 96 eqtrdi ⊢ ( ( 𝜑 ∧ ( 𝑘 ∈ ℕ0 ∧ ( 𝑀 + 𝑁 ) < 𝑘 ) ) → ( ( 𝐴 ‘ 𝑘 ) − ( 𝐵 ‘ 𝑘 ) ) = 0 )
98 41 97 eqtrd ⊢ ( ( 𝜑 ∧ ( 𝑘 ∈ ℕ0 ∧ ( 𝑀 + 𝑁 ) < 𝑘 ) ) → ( ( 𝐴 ∘f − 𝐵 ) ‘ 𝑘 ) = 0 )
99 98 expr ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ0 ) → ( ( 𝑀 + 𝑁 ) < 𝑘 → ( ( 𝐴 ∘f − 𝐵 ) ‘ 𝑘 ) = 0 ) )
100 35 99 sylbird ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ0 ) → ( ¬ 𝑘 ≤ ( 𝑀 + 𝑁 ) → ( ( 𝐴 ∘f − 𝐵 ) ‘ 𝑘 ) = 0 ) )
101 100 necon1ad ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ0 ) → ( ( ( 𝐴 ∘f − 𝐵 ) ‘ 𝑘 ) ≠ 0 → 𝑘 ≤ ( 𝑀 + 𝑁 ) ) )
102 101 ralrimiva ⊢ ( 𝜑 → ∀ 𝑘 ∈ ℕ0 ( ( ( 𝐴 ∘f − 𝐵 ) ‘ 𝑘 ) ≠ 0 → 𝑘 ≤ ( 𝑀 + 𝑁 ) ) )
103 plyco0 ⊢ ( ( ( 𝑀 + 𝑁 ) ∈ ℕ0 ∧ ( 𝐴 ∘f − 𝐵 ) : ℕ0 ⟶ ℂ ) → ( ( ( 𝐴 ∘f − 𝐵 ) “ ( ℤ≥ ‘ ( ( 𝑀 + 𝑁 ) + 1 ) ) ) = { 0 } ↔ ∀ 𝑘 ∈ ℕ0 ( ( ( 𝐴 ∘f − 𝐵 ) ‘ 𝑘 ) ≠ 0 → 𝑘 ≤ ( 𝑀 + 𝑁 ) ) ) )
104 11 22 103 syl2anc ⊢ ( 𝜑 → ( ( ( 𝐴 ∘f − 𝐵 ) “ ( ℤ≥ ‘ ( ( 𝑀 + 𝑁 ) + 1 ) ) ) = { 0 } ↔ ∀ 𝑘 ∈ ℕ0 ( ( ( 𝐴 ∘f − 𝐵 ) ‘ 𝑘 ) ≠ 0 → 𝑘 ≤ ( 𝑀 + 𝑁 ) ) ) )
105 102 104 mpbird ⊢ ( 𝜑 → ( ( 𝐴 ∘f − 𝐵 ) “ ( ℤ≥ ‘ ( ( 𝑀 + 𝑁 ) + 1 ) ) ) = { 0 } )
106 df-0p ⊢ 0𝑝 = ( ℂ × { 0 } )
107 fconstmpt ⊢ ( ℂ × { 0 } ) = ( 𝑧 ∈ ℂ ↦ 0 )
108 106 107 eqtri ⊢ 0𝑝 = ( 𝑧 ∈ ℂ ↦ 0 )
109 elfznn0 ⊢ ( 𝑘 ∈ ( 0 ... ( 𝑀 + 𝑁 ) ) → 𝑘 ∈ ℕ0 )
110 40 adantlr ⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ ℂ ) ∧ 𝑘 ∈ ℕ0 ) → ( ( 𝐴 ∘f − 𝐵 ) ‘ 𝑘 ) = ( ( 𝐴 ‘ 𝑘 ) − ( 𝐵 ‘ 𝑘 ) ) )
111 110 oveq1d ⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ ℂ ) ∧ 𝑘 ∈ ℕ0 ) → ( ( ( 𝐴 ∘f − 𝐵 ) ‘ 𝑘 ) · ( 𝑧 ↑ 𝑘 ) ) = ( ( ( 𝐴 ‘ 𝑘 ) − ( 𝐵 ‘ 𝑘 ) ) · ( 𝑧 ↑ 𝑘 ) ) )
112 17 adantr ⊢ ( ( 𝜑 ∧ 𝑧 ∈ ℂ ) → 𝐴 : ℕ0 ⟶ ℂ )
113 112 ffvelcdmda ⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ ℂ ) ∧ 𝑘 ∈ ℕ0 ) → ( 𝐴 ‘ 𝑘 ) ∈ ℂ )
114 19 adantr ⊢ ( ( 𝜑 ∧ 𝑧 ∈ ℂ ) → 𝐵 : ℕ0 ⟶ ℂ )
115 114 ffvelcdmda ⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ ℂ ) ∧ 𝑘 ∈ ℕ0 ) → ( 𝐵 ‘ 𝑘 ) ∈ ℂ )
116 expcl ⊢ ( ( 𝑧 ∈ ℂ ∧ 𝑘 ∈ ℕ0 ) → ( 𝑧 ↑ 𝑘 ) ∈ ℂ )
117 116 adantll ⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ ℂ ) ∧ 𝑘 ∈ ℕ0 ) → ( 𝑧 ↑ 𝑘 ) ∈ ℂ )
118 113 115 117 subdird ⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ ℂ ) ∧ 𝑘 ∈ ℕ0 ) → ( ( ( 𝐴 ‘ 𝑘 ) − ( 𝐵 ‘ 𝑘 ) ) · ( 𝑧 ↑ 𝑘 ) ) = ( ( ( 𝐴 ‘ 𝑘 ) · ( 𝑧 ↑ 𝑘 ) ) − ( ( 𝐵 ‘ 𝑘 ) · ( 𝑧 ↑ 𝑘 ) ) ) )
119 111 118 eqtrd ⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ ℂ ) ∧ 𝑘 ∈ ℕ0 ) → ( ( ( 𝐴 ∘f − 𝐵 ) ‘ 𝑘 ) · ( 𝑧 ↑ 𝑘 ) ) = ( ( ( 𝐴 ‘ 𝑘 ) · ( 𝑧 ↑ 𝑘 ) ) − ( ( 𝐵 ‘ 𝑘 ) · ( 𝑧 ↑ 𝑘 ) ) ) )
120 109 119 sylan2 ⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ ℂ ) ∧ 𝑘 ∈ ( 0 ... ( 𝑀 + 𝑁 ) ) ) → ( ( ( 𝐴 ∘f − 𝐵 ) ‘ 𝑘 ) · ( 𝑧 ↑ 𝑘 ) ) = ( ( ( 𝐴 ‘ 𝑘 ) · ( 𝑧 ↑ 𝑘 ) ) − ( ( 𝐵 ‘ 𝑘 ) · ( 𝑧 ↑ 𝑘 ) ) ) )
121 120 sumeq2dv ⊢ ( ( 𝜑 ∧ 𝑧 ∈ ℂ ) → Σ 𝑘 ∈ ( 0 ... ( 𝑀 + 𝑁 ) ) ( ( ( 𝐴 ∘f − 𝐵 ) ‘ 𝑘 ) · ( 𝑧 ↑ 𝑘 ) ) = Σ 𝑘 ∈ ( 0 ... ( 𝑀 + 𝑁 ) ) ( ( ( 𝐴 ‘ 𝑘 ) · ( 𝑧 ↑ 𝑘 ) ) − ( ( 𝐵 ‘ 𝑘 ) · ( 𝑧 ↑ 𝑘 ) ) ) )
122 fzfid ⊢ ( ( 𝜑 ∧ 𝑧 ∈ ℂ ) → ( 0 ... ( 𝑀 + 𝑁 ) ) ∈ Fin )
123 113 117 mulcld ⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ ℂ ) ∧ 𝑘 ∈ ℕ0 ) → ( ( 𝐴 ‘ 𝑘 ) · ( 𝑧 ↑ 𝑘 ) ) ∈ ℂ )
124 109 123 sylan2 ⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ ℂ ) ∧ 𝑘 ∈ ( 0 ... ( 𝑀 + 𝑁 ) ) ) → ( ( 𝐴 ‘ 𝑘 ) · ( 𝑧 ↑ 𝑘 ) ) ∈ ℂ )
125 115 117 mulcld ⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ ℂ ) ∧ 𝑘 ∈ ℕ0 ) → ( ( 𝐵 ‘ 𝑘 ) · ( 𝑧 ↑ 𝑘 ) ) ∈ ℂ )
126 109 125 sylan2 ⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ ℂ ) ∧ 𝑘 ∈ ( 0 ... ( 𝑀 + 𝑁 ) ) ) → ( ( 𝐵 ‘ 𝑘 ) · ( 𝑧 ↑ 𝑘 ) ) ∈ ℂ )
127 122 124 126 fsumsub ⊢ ( ( 𝜑 ∧ 𝑧 ∈ ℂ ) → Σ 𝑘 ∈ ( 0 ... ( 𝑀 + 𝑁 ) ) ( ( ( 𝐴 ‘ 𝑘 ) · ( 𝑧 ↑ 𝑘 ) ) − ( ( 𝐵 ‘ 𝑘 ) · ( 𝑧 ↑ 𝑘 ) ) ) = ( Σ 𝑘 ∈ ( 0 ... ( 𝑀 + 𝑁 ) ) ( ( 𝐴 ‘ 𝑘 ) · ( 𝑧 ↑ 𝑘 ) ) − Σ 𝑘 ∈ ( 0 ... ( 𝑀 + 𝑁 ) ) ( ( 𝐵 ‘ 𝑘 ) · ( 𝑧 ↑ 𝑘 ) ) ) )
128 122 124 fsumcl ⊢ ( ( 𝜑 ∧ 𝑧 ∈ ℂ ) → Σ 𝑘 ∈ ( 0 ... ( 𝑀 + 𝑁 ) ) ( ( 𝐴 ‘ 𝑘 ) · ( 𝑧 ↑ 𝑘 ) ) ∈ ℂ )
129 8 9 eqtr3d ⊢ ( 𝜑 → ( 𝑧 ∈ ℂ ↦ Σ 𝑘 ∈ ( 0 ... 𝑀 ) ( ( 𝐴 ‘ 𝑘 ) · ( 𝑧 ↑ 𝑘 ) ) ) = ( 𝑧 ∈ ℂ ↦ Σ 𝑘 ∈ ( 0 ... 𝑁 ) ( ( 𝐵 ‘ 𝑘 ) · ( 𝑧 ↑ 𝑘 ) ) ) )
130 129 fveq1d ⊢ ( 𝜑 → ( ( 𝑧 ∈ ℂ ↦ Σ 𝑘 ∈ ( 0 ... 𝑀 ) ( ( 𝐴 ‘ 𝑘 ) · ( 𝑧 ↑ 𝑘 ) ) ) ‘ 𝑧 ) = ( ( 𝑧 ∈ ℂ ↦ Σ 𝑘 ∈ ( 0 ... 𝑁 ) ( ( 𝐵 ‘ 𝑘 ) · ( 𝑧 ↑ 𝑘 ) ) ) ‘ 𝑧 ) )
131 130 adantr ⊢ ( ( 𝜑 ∧ 𝑧 ∈ ℂ ) → ( ( 𝑧 ∈ ℂ ↦ Σ 𝑘 ∈ ( 0 ... 𝑀 ) ( ( 𝐴 ‘ 𝑘 ) · ( 𝑧 ↑ 𝑘 ) ) ) ‘ 𝑧 ) = ( ( 𝑧 ∈ ℂ ↦ Σ 𝑘 ∈ ( 0 ... 𝑁 ) ( ( 𝐵 ‘ 𝑘 ) · ( 𝑧 ↑ 𝑘 ) ) ) ‘ 𝑧 ) )
132 simpr ⊢ ( ( 𝜑 ∧ 𝑧 ∈ ℂ ) → 𝑧 ∈ ℂ )
133 sumex ⊢ Σ 𝑘 ∈ ( 0 ... 𝑀 ) ( ( 𝐴 ‘ 𝑘 ) · ( 𝑧 ↑ 𝑘 ) ) ∈ V
134 eqid ⊢ ( 𝑧 ∈ ℂ ↦ Σ 𝑘 ∈ ( 0 ... 𝑀 ) ( ( 𝐴 ‘ 𝑘 ) · ( 𝑧 ↑ 𝑘 ) ) ) = ( 𝑧 ∈ ℂ ↦ Σ 𝑘 ∈ ( 0 ... 𝑀 ) ( ( 𝐴 ‘ 𝑘 ) · ( 𝑧 ↑ 𝑘 ) ) )
135 134 fvmpt2 ⊢ ( ( 𝑧 ∈ ℂ ∧ Σ 𝑘 ∈ ( 0 ... 𝑀 ) ( ( 𝐴 ‘ 𝑘 ) · ( 𝑧 ↑ 𝑘 ) ) ∈ V ) → ( ( 𝑧 ∈ ℂ ↦ Σ 𝑘 ∈ ( 0 ... 𝑀 ) ( ( 𝐴 ‘ 𝑘 ) · ( 𝑧 ↑ 𝑘 ) ) ) ‘ 𝑧 ) = Σ 𝑘 ∈ ( 0 ... 𝑀 ) ( ( 𝐴 ‘ 𝑘 ) · ( 𝑧 ↑ 𝑘 ) ) )
136 132 133 135 sylancl ⊢ ( ( 𝜑 ∧ 𝑧 ∈ ℂ ) → ( ( 𝑧 ∈ ℂ ↦ Σ 𝑘 ∈ ( 0 ... 𝑀 ) ( ( 𝐴 ‘ 𝑘 ) · ( 𝑧 ↑ 𝑘 ) ) ) ‘ 𝑧 ) = Σ 𝑘 ∈ ( 0 ... 𝑀 ) ( ( 𝐴 ‘ 𝑘 ) · ( 𝑧 ↑ 𝑘 ) ) )
137 fzss2 ⊢ ( ( 𝑀 + 𝑁 ) ∈ ( ℤ≥ ‘ 𝑀 ) → ( 0 ... 𝑀 ) ⊆ ( 0 ... ( 𝑀 + 𝑁 ) ) )
138 58 137 syl ⊢ ( 𝜑 → ( 0 ... 𝑀 ) ⊆ ( 0 ... ( 𝑀 + 𝑁 ) ) )
139 138 adantr ⊢ ( ( 𝜑 ∧ 𝑧 ∈ ℂ ) → ( 0 ... 𝑀 ) ⊆ ( 0 ... ( 𝑀 + 𝑁 ) ) )
140 139 sselda ⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ ℂ ) ∧ 𝑘 ∈ ( 0 ... 𝑀 ) ) → 𝑘 ∈ ( 0 ... ( 𝑀 + 𝑁 ) ) )
141 140 124 syldan ⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ ℂ ) ∧ 𝑘 ∈ ( 0 ... 𝑀 ) ) → ( ( 𝐴 ‘ 𝑘 ) · ( 𝑧 ↑ 𝑘 ) ) ∈ ℂ )
142 eldifn ⊢ ( 𝑘 ∈ ( ( 0 ... ( 𝑀 + 𝑁 ) ) ∖ ( 0 ... 𝑀 ) ) → ¬ 𝑘 ∈ ( 0 ... 𝑀 ) )
143 142 adantl ⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ ℂ ) ∧ 𝑘 ∈ ( ( 0 ... ( 𝑀 + 𝑁 ) ) ∖ ( 0 ... 𝑀 ) ) ) → ¬ 𝑘 ∈ ( 0 ... 𝑀 ) )
144 eldifi ⊢ ( 𝑘 ∈ ( ( 0 ... ( 𝑀 + 𝑁 ) ) ∖ ( 0 ... 𝑀 ) ) → 𝑘 ∈ ( 0 ... ( 𝑀 + 𝑁 ) ) )
145 144 109 syl ⊢ ( 𝑘 ∈ ( ( 0 ... ( 𝑀 + 𝑁 ) ) ∖ ( 0 ... 𝑀 ) ) → 𝑘 ∈ ℕ0 )
146 simpr ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ0 ) → 𝑘 ∈ ℕ0 )
147 146 50 eleqtrdi ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ0 ) → 𝑘 ∈ ( ℤ≥ ‘ 0 ) )
148 52 adantr ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ0 ) → 𝑀 ∈ ℤ )
149 elfz5 ⊢ ( ( 𝑘 ∈ ( ℤ≥ ‘ 0 ) ∧ 𝑀 ∈ ℤ ) → ( 𝑘 ∈ ( 0 ... 𝑀 ) ↔ 𝑘 ≤ 𝑀 ) )
150 147 148 149 syl2anc ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ0 ) → ( 𝑘 ∈ ( 0 ... 𝑀 ) ↔ 𝑘 ≤ 𝑀 ) )
151 69 150 sylibrd ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ0 ) → ( ( 𝐴 ‘ 𝑘 ) ≠ 0 → 𝑘 ∈ ( 0 ... 𝑀 ) ) )
152 151 adantlr ⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ ℂ ) ∧ 𝑘 ∈ ℕ0 ) → ( ( 𝐴 ‘ 𝑘 ) ≠ 0 → 𝑘 ∈ ( 0 ... 𝑀 ) ) )
153 152 necon1bd ⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ ℂ ) ∧ 𝑘 ∈ ℕ0 ) → ( ¬ 𝑘 ∈ ( 0 ... 𝑀 ) → ( 𝐴 ‘ 𝑘 ) = 0 ) )
154 145 153 sylan2 ⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ ℂ ) ∧ 𝑘 ∈ ( ( 0 ... ( 𝑀 + 𝑁 ) ) ∖ ( 0 ... 𝑀 ) ) ) → ( ¬ 𝑘 ∈ ( 0 ... 𝑀 ) → ( 𝐴 ‘ 𝑘 ) = 0 ) )
155 143 154 mpd ⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ ℂ ) ∧ 𝑘 ∈ ( ( 0 ... ( 𝑀 + 𝑁 ) ) ∖ ( 0 ... 𝑀 ) ) ) → ( 𝐴 ‘ 𝑘 ) = 0 )
156 155 oveq1d ⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ ℂ ) ∧ 𝑘 ∈ ( ( 0 ... ( 𝑀 + 𝑁 ) ) ∖ ( 0 ... 𝑀 ) ) ) → ( ( 𝐴 ‘ 𝑘 ) · ( 𝑧 ↑ 𝑘 ) ) = ( 0 · ( 𝑧 ↑ 𝑘 ) ) )
157 132 145 116 syl2an ⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ ℂ ) ∧ 𝑘 ∈ ( ( 0 ... ( 𝑀 + 𝑁 ) ) ∖ ( 0 ... 𝑀 ) ) ) → ( 𝑧 ↑ 𝑘 ) ∈ ℂ )
158 157 mul02d ⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ ℂ ) ∧ 𝑘 ∈ ( ( 0 ... ( 𝑀 + 𝑁 ) ) ∖ ( 0 ... 𝑀 ) ) ) → ( 0 · ( 𝑧 ↑ 𝑘 ) ) = 0 )
159 156 158 eqtrd ⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ ℂ ) ∧ 𝑘 ∈ ( ( 0 ... ( 𝑀 + 𝑁 ) ) ∖ ( 0 ... 𝑀 ) ) ) → ( ( 𝐴 ‘ 𝑘 ) · ( 𝑧 ↑ 𝑘 ) ) = 0 )
160 139 141 159 122 fsumss ⊢ ( ( 𝜑 ∧ 𝑧 ∈ ℂ ) → Σ 𝑘 ∈ ( 0 ... 𝑀 ) ( ( 𝐴 ‘ 𝑘 ) · ( 𝑧 ↑ 𝑘 ) ) = Σ 𝑘 ∈ ( 0 ... ( 𝑀 + 𝑁 ) ) ( ( 𝐴 ‘ 𝑘 ) · ( 𝑧 ↑ 𝑘 ) ) )
161 136 160 eqtrd ⊢ ( ( 𝜑 ∧ 𝑧 ∈ ℂ ) → ( ( 𝑧 ∈ ℂ ↦ Σ 𝑘 ∈ ( 0 ... 𝑀 ) ( ( 𝐴 ‘ 𝑘 ) · ( 𝑧 ↑ 𝑘 ) ) ) ‘ 𝑧 ) = Σ 𝑘 ∈ ( 0 ... ( 𝑀 + 𝑁 ) ) ( ( 𝐴 ‘ 𝑘 ) · ( 𝑧 ↑ 𝑘 ) ) )
162 sumex ⊢ Σ 𝑘 ∈ ( 0 ... 𝑁 ) ( ( 𝐵 ‘ 𝑘 ) · ( 𝑧 ↑ 𝑘 ) ) ∈ V
163 eqid ⊢ ( 𝑧 ∈ ℂ ↦ Σ 𝑘 ∈ ( 0 ... 𝑁 ) ( ( 𝐵 ‘ 𝑘 ) · ( 𝑧 ↑ 𝑘 ) ) ) = ( 𝑧 ∈ ℂ ↦ Σ 𝑘 ∈ ( 0 ... 𝑁 ) ( ( 𝐵 ‘ 𝑘 ) · ( 𝑧 ↑ 𝑘 ) ) )
164 163 fvmpt2 ⊢ ( ( 𝑧 ∈ ℂ ∧ Σ 𝑘 ∈ ( 0 ... 𝑁 ) ( ( 𝐵 ‘ 𝑘 ) · ( 𝑧 ↑ 𝑘 ) ) ∈ V ) → ( ( 𝑧 ∈ ℂ ↦ Σ 𝑘 ∈ ( 0 ... 𝑁 ) ( ( 𝐵 ‘ 𝑘 ) · ( 𝑧 ↑ 𝑘 ) ) ) ‘ 𝑧 ) = Σ 𝑘 ∈ ( 0 ... 𝑁 ) ( ( 𝐵 ‘ 𝑘 ) · ( 𝑧 ↑ 𝑘 ) ) )
165 132 162 164 sylancl ⊢ ( ( 𝜑 ∧ 𝑧 ∈ ℂ ) → ( ( 𝑧 ∈ ℂ ↦ Σ 𝑘 ∈ ( 0 ... 𝑁 ) ( ( 𝐵 ‘ 𝑘 ) · ( 𝑧 ↑ 𝑘 ) ) ) ‘ 𝑧 ) = Σ 𝑘 ∈ ( 0 ... 𝑁 ) ( ( 𝐵 ‘ 𝑘 ) · ( 𝑧 ↑ 𝑘 ) ) )
166 fzss2 ⊢ ( ( 𝑀 + 𝑁 ) ∈ ( ℤ≥ ‘ 𝑁 ) → ( 0 ... 𝑁 ) ⊆ ( 0 ... ( 𝑀 + 𝑁 ) ) )
167 81 166 syl ⊢ ( 𝜑 → ( 0 ... 𝑁 ) ⊆ ( 0 ... ( 𝑀 + 𝑁 ) ) )
168 167 adantr ⊢ ( ( 𝜑 ∧ 𝑧 ∈ ℂ ) → ( 0 ... 𝑁 ) ⊆ ( 0 ... ( 𝑀 + 𝑁 ) ) )
169 168 sselda ⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ ℂ ) ∧ 𝑘 ∈ ( 0 ... 𝑁 ) ) → 𝑘 ∈ ( 0 ... ( 𝑀 + 𝑁 ) ) )
170 169 126 syldan ⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ ℂ ) ∧ 𝑘 ∈ ( 0 ... 𝑁 ) ) → ( ( 𝐵 ‘ 𝑘 ) · ( 𝑧 ↑ 𝑘 ) ) ∈ ℂ )
171 eldifn ⊢ ( 𝑘 ∈ ( ( 0 ... ( 𝑀 + 𝑁 ) ) ∖ ( 0 ... 𝑁 ) ) → ¬ 𝑘 ∈ ( 0 ... 𝑁 ) )
172 171 adantl ⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ ℂ ) ∧ 𝑘 ∈ ( ( 0 ... ( 𝑀 + 𝑁 ) ) ∖ ( 0 ... 𝑁 ) ) ) → ¬ 𝑘 ∈ ( 0 ... 𝑁 ) )
173 eldifi ⊢ ( 𝑘 ∈ ( ( 0 ... ( 𝑀 + 𝑁 ) ) ∖ ( 0 ... 𝑁 ) ) → 𝑘 ∈ ( 0 ... ( 𝑀 + 𝑁 ) ) )
174 173 109 syl ⊢ ( 𝑘 ∈ ( ( 0 ... ( 𝑀 + 𝑁 ) ) ∖ ( 0 ... 𝑁 ) ) → 𝑘 ∈ ℕ0 )
175 76 adantr ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ0 ) → 𝑁 ∈ ℤ )
176 elfz5 ⊢ ( ( 𝑘 ∈ ( ℤ≥ ‘ 0 ) ∧ 𝑁 ∈ ℤ ) → ( 𝑘 ∈ ( 0 ... 𝑁 ) ↔ 𝑘 ≤ 𝑁 ) )
177 147 175 176 syl2anc ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ0 ) → ( 𝑘 ∈ ( 0 ... 𝑁 ) ↔ 𝑘 ≤ 𝑁 ) )
178 91 177 sylibrd ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ0 ) → ( ( 𝐵 ‘ 𝑘 ) ≠ 0 → 𝑘 ∈ ( 0 ... 𝑁 ) ) )
179 178 adantlr ⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ ℂ ) ∧ 𝑘 ∈ ℕ0 ) → ( ( 𝐵 ‘ 𝑘 ) ≠ 0 → 𝑘 ∈ ( 0 ... 𝑁 ) ) )
180 179 necon1bd ⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ ℂ ) ∧ 𝑘 ∈ ℕ0 ) → ( ¬ 𝑘 ∈ ( 0 ... 𝑁 ) → ( 𝐵 ‘ 𝑘 ) = 0 ) )
181 174 180 sylan2 ⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ ℂ ) ∧ 𝑘 ∈ ( ( 0 ... ( 𝑀 + 𝑁 ) ) ∖ ( 0 ... 𝑁 ) ) ) → ( ¬ 𝑘 ∈ ( 0 ... 𝑁 ) → ( 𝐵 ‘ 𝑘 ) = 0 ) )
182 172 181 mpd ⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ ℂ ) ∧ 𝑘 ∈ ( ( 0 ... ( 𝑀 + 𝑁 ) ) ∖ ( 0 ... 𝑁 ) ) ) → ( 𝐵 ‘ 𝑘 ) = 0 )
183 182 oveq1d ⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ ℂ ) ∧ 𝑘 ∈ ( ( 0 ... ( 𝑀 + 𝑁 ) ) ∖ ( 0 ... 𝑁 ) ) ) → ( ( 𝐵 ‘ 𝑘 ) · ( 𝑧 ↑ 𝑘 ) ) = ( 0 · ( 𝑧 ↑ 𝑘 ) ) )
184 132 174 116 syl2an ⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ ℂ ) ∧ 𝑘 ∈ ( ( 0 ... ( 𝑀 + 𝑁 ) ) ∖ ( 0 ... 𝑁 ) ) ) → ( 𝑧 ↑ 𝑘 ) ∈ ℂ )
185 184 mul02d ⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ ℂ ) ∧ 𝑘 ∈ ( ( 0 ... ( 𝑀 + 𝑁 ) ) ∖ ( 0 ... 𝑁 ) ) ) → ( 0 · ( 𝑧 ↑ 𝑘 ) ) = 0 )
186 183 185 eqtrd ⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ ℂ ) ∧ 𝑘 ∈ ( ( 0 ... ( 𝑀 + 𝑁 ) ) ∖ ( 0 ... 𝑁 ) ) ) → ( ( 𝐵 ‘ 𝑘 ) · ( 𝑧 ↑ 𝑘 ) ) = 0 )
187 168 170 186 122 fsumss ⊢ ( ( 𝜑 ∧ 𝑧 ∈ ℂ ) → Σ 𝑘 ∈ ( 0 ... 𝑁 ) ( ( 𝐵 ‘ 𝑘 ) · ( 𝑧 ↑ 𝑘 ) ) = Σ 𝑘 ∈ ( 0 ... ( 𝑀 + 𝑁 ) ) ( ( 𝐵 ‘ 𝑘 ) · ( 𝑧 ↑ 𝑘 ) ) )
188 165 187 eqtrd ⊢ ( ( 𝜑 ∧ 𝑧 ∈ ℂ ) → ( ( 𝑧 ∈ ℂ ↦ Σ 𝑘 ∈ ( 0 ... 𝑁 ) ( ( 𝐵 ‘ 𝑘 ) · ( 𝑧 ↑ 𝑘 ) ) ) ‘ 𝑧 ) = Σ 𝑘 ∈ ( 0 ... ( 𝑀 + 𝑁 ) ) ( ( 𝐵 ‘ 𝑘 ) · ( 𝑧 ↑ 𝑘 ) ) )
189 131 161 188 3eqtr3d ⊢ ( ( 𝜑 ∧ 𝑧 ∈ ℂ ) → Σ 𝑘 ∈ ( 0 ... ( 𝑀 + 𝑁 ) ) ( ( 𝐴 ‘ 𝑘 ) · ( 𝑧 ↑ 𝑘 ) ) = Σ 𝑘 ∈ ( 0 ... ( 𝑀 + 𝑁 ) ) ( ( 𝐵 ‘ 𝑘 ) · ( 𝑧 ↑ 𝑘 ) ) )
190 128 189 subeq0bd ⊢ ( ( 𝜑 ∧ 𝑧 ∈ ℂ ) → ( Σ 𝑘 ∈ ( 0 ... ( 𝑀 + 𝑁 ) ) ( ( 𝐴 ‘ 𝑘 ) · ( 𝑧 ↑ 𝑘 ) ) − Σ 𝑘 ∈ ( 0 ... ( 𝑀 + 𝑁 ) ) ( ( 𝐵 ‘ 𝑘 ) · ( 𝑧 ↑ 𝑘 ) ) ) = 0 )
191 121 127 190 3eqtrrd ⊢ ( ( 𝜑 ∧ 𝑧 ∈ ℂ ) → 0 = Σ 𝑘 ∈ ( 0 ... ( 𝑀 + 𝑁 ) ) ( ( ( 𝐴 ∘f − 𝐵 ) ‘ 𝑘 ) · ( 𝑧 ↑ 𝑘 ) ) )
192 191 mpteq2dva ⊢ ( 𝜑 → ( 𝑧 ∈ ℂ ↦ 0 ) = ( 𝑧 ∈ ℂ ↦ Σ 𝑘 ∈ ( 0 ... ( 𝑀 + 𝑁 ) ) ( ( ( 𝐴 ∘f − 𝐵 ) ‘ 𝑘 ) · ( 𝑧 ↑ 𝑘 ) ) ) )
193 108 192 eqtrid ⊢ ( 𝜑 → 0𝑝 = ( 𝑧 ∈ ℂ ↦ Σ 𝑘 ∈ ( 0 ... ( 𝑀 + 𝑁 ) ) ( ( ( 𝐴 ∘f − 𝐵 ) ‘ 𝑘 ) · ( 𝑧 ↑ 𝑘 ) ) ) )
194 10 11 31 105 193 plyeq0 ⊢ ( 𝜑 → ( 𝐴 ∘f − 𝐵 ) = ( ℕ0 × { 0 } ) )
195 ofsubeq0 ⊢ ( ( ℕ0 ∈ V ∧ 𝐴 : ℕ0 ⟶ ℂ ∧ 𝐵 : ℕ0 ⟶ ℂ ) → ( ( 𝐴 ∘f − 𝐵 ) = ( ℕ0 × { 0 } ) ↔ 𝐴 = 𝐵 ) )
196 15 17 19 195 mp3an2i ⊢ ( 𝜑 → ( ( 𝐴 ∘f − 𝐵 ) = ( ℕ0 × { 0 } ) ↔ 𝐴 = 𝐵 ) )
197 194 196 mpbid ⊢ ( 𝜑 → 𝐴 = 𝐵 )