Metamath Proof Explorer


Theorem coeeulem

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

Ref Expression
Hypotheses coeeu.1 ( 𝜑𝐹 ∈ ( Poly ‘ 𝑆 ) )
coeeu.2 ( 𝜑𝐴 ∈ ( ℂ ↑m0 ) )
coeeu.3 ( 𝜑𝐵 ∈ ( ℂ ↑m0 ) )
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 ( 𝜑𝐴 ∈ ( ℂ ↑m0 ) )
3 coeeu.3 ( 𝜑𝐵 ∈ ( ℂ ↑m0 ) )
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 ( 𝐴 ∈ ( ℂ ↑m0 ) ↔ 𝐴 : ℕ0 ⟶ ℂ )
17 2 16 sylib ( 𝜑𝐴 : ℕ0 ⟶ ℂ )
18 14 15 elmap ( 𝐵 ∈ ( ℂ ↑m0 ) ↔ 𝐵 : ℕ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𝐵 ) ∈ ( ℂ ↑m0 ) ↔ ( 𝐴f𝐵 ) : ℕ0 ⟶ ℂ )
24 22 23 sylibr ( 𝜑 → ( 𝐴f𝐵 ) ∈ ( ℂ ↑m0 ) )
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 } ) ↑m0 ) = ( ℂ ↑m0 )
31 24 30 eleqtrrdi ( 𝜑 → ( 𝐴f𝐵 ) ∈ ( ( ℂ ∪ { 0 } ) ↑m0 ) )
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 addid2d ( 𝜑 → ( 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 addid2d ( 𝜑 → ( 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 ffvelrnda ( ( ( 𝜑𝑧 ∈ ℂ ) ∧ 𝑘 ∈ ℕ0 ) → ( 𝐴𝑘 ) ∈ ℂ )
114 19 adantr ( ( 𝜑𝑧 ∈ ℂ ) → 𝐵 : ℕ0 ⟶ ℂ )
115 114 ffvelrnda ( ( ( 𝜑𝑧 ∈ ℂ ) ∧ 𝑘 ∈ ℕ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 syl5eq ( 𝜑 → 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 ( 𝜑𝐴 = 𝐵 )