Step |
Hyp |
Ref |
Expression |
1 |
|
plyssc |
⊢ ( Poly ‘ 𝑆 ) ⊆ ( Poly ‘ ℂ ) |
2 |
1
|
sseli |
⊢ ( 𝐹 ∈ ( Poly ‘ 𝑆 ) → 𝐹 ∈ ( Poly ‘ ℂ ) ) |
3 |
|
elply2 |
⊢ ( 𝐹 ∈ ( Poly ‘ ℂ ) ↔ ( ℂ ⊆ ℂ ∧ ∃ 𝑛 ∈ ℕ0 ∃ 𝑎 ∈ ( ( ℂ ∪ { 0 } ) ↑m ℕ0 ) ( ( 𝑎 “ ( ℤ≥ ‘ ( 𝑛 + 1 ) ) ) = { 0 } ∧ 𝐹 = ( 𝑧 ∈ ℂ ↦ Σ 𝑘 ∈ ( 0 ... 𝑛 ) ( ( 𝑎 ‘ 𝑘 ) · ( 𝑧 ↑ 𝑘 ) ) ) ) ) ) |
4 |
3
|
simprbi |
⊢ ( 𝐹 ∈ ( Poly ‘ ℂ ) → ∃ 𝑛 ∈ ℕ0 ∃ 𝑎 ∈ ( ( ℂ ∪ { 0 } ) ↑m ℕ0 ) ( ( 𝑎 “ ( ℤ≥ ‘ ( 𝑛 + 1 ) ) ) = { 0 } ∧ 𝐹 = ( 𝑧 ∈ ℂ ↦ Σ 𝑘 ∈ ( 0 ... 𝑛 ) ( ( 𝑎 ‘ 𝑘 ) · ( 𝑧 ↑ 𝑘 ) ) ) ) ) |
5 |
|
rexcom |
⊢ ( ∃ 𝑛 ∈ ℕ0 ∃ 𝑎 ∈ ( ( ℂ ∪ { 0 } ) ↑m ℕ0 ) ( ( 𝑎 “ ( ℤ≥ ‘ ( 𝑛 + 1 ) ) ) = { 0 } ∧ 𝐹 = ( 𝑧 ∈ ℂ ↦ Σ 𝑘 ∈ ( 0 ... 𝑛 ) ( ( 𝑎 ‘ 𝑘 ) · ( 𝑧 ↑ 𝑘 ) ) ) ) ↔ ∃ 𝑎 ∈ ( ( ℂ ∪ { 0 } ) ↑m ℕ0 ) ∃ 𝑛 ∈ ℕ0 ( ( 𝑎 “ ( ℤ≥ ‘ ( 𝑛 + 1 ) ) ) = { 0 } ∧ 𝐹 = ( 𝑧 ∈ ℂ ↦ Σ 𝑘 ∈ ( 0 ... 𝑛 ) ( ( 𝑎 ‘ 𝑘 ) · ( 𝑧 ↑ 𝑘 ) ) ) ) ) |
6 |
4 5
|
sylib |
⊢ ( 𝐹 ∈ ( Poly ‘ ℂ ) → ∃ 𝑎 ∈ ( ( ℂ ∪ { 0 } ) ↑m ℕ0 ) ∃ 𝑛 ∈ ℕ0 ( ( 𝑎 “ ( ℤ≥ ‘ ( 𝑛 + 1 ) ) ) = { 0 } ∧ 𝐹 = ( 𝑧 ∈ ℂ ↦ Σ 𝑘 ∈ ( 0 ... 𝑛 ) ( ( 𝑎 ‘ 𝑘 ) · ( 𝑧 ↑ 𝑘 ) ) ) ) ) |
7 |
2 6
|
syl |
⊢ ( 𝐹 ∈ ( Poly ‘ 𝑆 ) → ∃ 𝑎 ∈ ( ( ℂ ∪ { 0 } ) ↑m ℕ0 ) ∃ 𝑛 ∈ ℕ0 ( ( 𝑎 “ ( ℤ≥ ‘ ( 𝑛 + 1 ) ) ) = { 0 } ∧ 𝐹 = ( 𝑧 ∈ ℂ ↦ Σ 𝑘 ∈ ( 0 ... 𝑛 ) ( ( 𝑎 ‘ 𝑘 ) · ( 𝑧 ↑ 𝑘 ) ) ) ) ) |
8 |
|
0cn |
⊢ 0 ∈ ℂ |
9 |
|
snssi |
⊢ ( 0 ∈ ℂ → { 0 } ⊆ ℂ ) |
10 |
8 9
|
ax-mp |
⊢ { 0 } ⊆ ℂ |
11 |
|
ssequn2 |
⊢ ( { 0 } ⊆ ℂ ↔ ( ℂ ∪ { 0 } ) = ℂ ) |
12 |
10 11
|
mpbi |
⊢ ( ℂ ∪ { 0 } ) = ℂ |
13 |
12
|
oveq1i |
⊢ ( ( ℂ ∪ { 0 } ) ↑m ℕ0 ) = ( ℂ ↑m ℕ0 ) |
14 |
13
|
rexeqi |
⊢ ( ∃ 𝑎 ∈ ( ( ℂ ∪ { 0 } ) ↑m ℕ0 ) ∃ 𝑛 ∈ ℕ0 ( ( 𝑎 “ ( ℤ≥ ‘ ( 𝑛 + 1 ) ) ) = { 0 } ∧ 𝐹 = ( 𝑧 ∈ ℂ ↦ Σ 𝑘 ∈ ( 0 ... 𝑛 ) ( ( 𝑎 ‘ 𝑘 ) · ( 𝑧 ↑ 𝑘 ) ) ) ) ↔ ∃ 𝑎 ∈ ( ℂ ↑m ℕ0 ) ∃ 𝑛 ∈ ℕ0 ( ( 𝑎 “ ( ℤ≥ ‘ ( 𝑛 + 1 ) ) ) = { 0 } ∧ 𝐹 = ( 𝑧 ∈ ℂ ↦ Σ 𝑘 ∈ ( 0 ... 𝑛 ) ( ( 𝑎 ‘ 𝑘 ) · ( 𝑧 ↑ 𝑘 ) ) ) ) ) |
15 |
7 14
|
sylib |
⊢ ( 𝐹 ∈ ( Poly ‘ 𝑆 ) → ∃ 𝑎 ∈ ( ℂ ↑m ℕ0 ) ∃ 𝑛 ∈ ℕ0 ( ( 𝑎 “ ( ℤ≥ ‘ ( 𝑛 + 1 ) ) ) = { 0 } ∧ 𝐹 = ( 𝑧 ∈ ℂ ↦ Σ 𝑘 ∈ ( 0 ... 𝑛 ) ( ( 𝑎 ‘ 𝑘 ) · ( 𝑧 ↑ 𝑘 ) ) ) ) ) |
16 |
|
reeanv |
⊢ ( ∃ 𝑛 ∈ ℕ0 ∃ 𝑚 ∈ ℕ0 ( ( ( 𝑎 “ ( ℤ≥ ‘ ( 𝑛 + 1 ) ) ) = { 0 } ∧ 𝐹 = ( 𝑧 ∈ ℂ ↦ Σ 𝑘 ∈ ( 0 ... 𝑛 ) ( ( 𝑎 ‘ 𝑘 ) · ( 𝑧 ↑ 𝑘 ) ) ) ) ∧ ( ( 𝑏 “ ( ℤ≥ ‘ ( 𝑚 + 1 ) ) ) = { 0 } ∧ 𝐹 = ( 𝑧 ∈ ℂ ↦ Σ 𝑘 ∈ ( 0 ... 𝑚 ) ( ( 𝑏 ‘ 𝑘 ) · ( 𝑧 ↑ 𝑘 ) ) ) ) ) ↔ ( ∃ 𝑛 ∈ ℕ0 ( ( 𝑎 “ ( ℤ≥ ‘ ( 𝑛 + 1 ) ) ) = { 0 } ∧ 𝐹 = ( 𝑧 ∈ ℂ ↦ Σ 𝑘 ∈ ( 0 ... 𝑛 ) ( ( 𝑎 ‘ 𝑘 ) · ( 𝑧 ↑ 𝑘 ) ) ) ) ∧ ∃ 𝑚 ∈ ℕ0 ( ( 𝑏 “ ( ℤ≥ ‘ ( 𝑚 + 1 ) ) ) = { 0 } ∧ 𝐹 = ( 𝑧 ∈ ℂ ↦ Σ 𝑘 ∈ ( 0 ... 𝑚 ) ( ( 𝑏 ‘ 𝑘 ) · ( 𝑧 ↑ 𝑘 ) ) ) ) ) ) |
17 |
|
simp1l |
⊢ ( ( ( 𝐹 ∈ ( Poly ‘ 𝑆 ) ∧ ( 𝑎 ∈ ( ℂ ↑m ℕ0 ) ∧ 𝑏 ∈ ( ℂ ↑m ℕ0 ) ) ) ∧ ( 𝑛 ∈ ℕ0 ∧ 𝑚 ∈ ℕ0 ) ∧ ( ( ( 𝑎 “ ( ℤ≥ ‘ ( 𝑛 + 1 ) ) ) = { 0 } ∧ 𝐹 = ( 𝑧 ∈ ℂ ↦ Σ 𝑘 ∈ ( 0 ... 𝑛 ) ( ( 𝑎 ‘ 𝑘 ) · ( 𝑧 ↑ 𝑘 ) ) ) ) ∧ ( ( 𝑏 “ ( ℤ≥ ‘ ( 𝑚 + 1 ) ) ) = { 0 } ∧ 𝐹 = ( 𝑧 ∈ ℂ ↦ Σ 𝑘 ∈ ( 0 ... 𝑚 ) ( ( 𝑏 ‘ 𝑘 ) · ( 𝑧 ↑ 𝑘 ) ) ) ) ) ) → 𝐹 ∈ ( Poly ‘ 𝑆 ) ) |
18 |
|
simp1rl |
⊢ ( ( ( 𝐹 ∈ ( Poly ‘ 𝑆 ) ∧ ( 𝑎 ∈ ( ℂ ↑m ℕ0 ) ∧ 𝑏 ∈ ( ℂ ↑m ℕ0 ) ) ) ∧ ( 𝑛 ∈ ℕ0 ∧ 𝑚 ∈ ℕ0 ) ∧ ( ( ( 𝑎 “ ( ℤ≥ ‘ ( 𝑛 + 1 ) ) ) = { 0 } ∧ 𝐹 = ( 𝑧 ∈ ℂ ↦ Σ 𝑘 ∈ ( 0 ... 𝑛 ) ( ( 𝑎 ‘ 𝑘 ) · ( 𝑧 ↑ 𝑘 ) ) ) ) ∧ ( ( 𝑏 “ ( ℤ≥ ‘ ( 𝑚 + 1 ) ) ) = { 0 } ∧ 𝐹 = ( 𝑧 ∈ ℂ ↦ Σ 𝑘 ∈ ( 0 ... 𝑚 ) ( ( 𝑏 ‘ 𝑘 ) · ( 𝑧 ↑ 𝑘 ) ) ) ) ) ) → 𝑎 ∈ ( ℂ ↑m ℕ0 ) ) |
19 |
|
simp1rr |
⊢ ( ( ( 𝐹 ∈ ( Poly ‘ 𝑆 ) ∧ ( 𝑎 ∈ ( ℂ ↑m ℕ0 ) ∧ 𝑏 ∈ ( ℂ ↑m ℕ0 ) ) ) ∧ ( 𝑛 ∈ ℕ0 ∧ 𝑚 ∈ ℕ0 ) ∧ ( ( ( 𝑎 “ ( ℤ≥ ‘ ( 𝑛 + 1 ) ) ) = { 0 } ∧ 𝐹 = ( 𝑧 ∈ ℂ ↦ Σ 𝑘 ∈ ( 0 ... 𝑛 ) ( ( 𝑎 ‘ 𝑘 ) · ( 𝑧 ↑ 𝑘 ) ) ) ) ∧ ( ( 𝑏 “ ( ℤ≥ ‘ ( 𝑚 + 1 ) ) ) = { 0 } ∧ 𝐹 = ( 𝑧 ∈ ℂ ↦ Σ 𝑘 ∈ ( 0 ... 𝑚 ) ( ( 𝑏 ‘ 𝑘 ) · ( 𝑧 ↑ 𝑘 ) ) ) ) ) ) → 𝑏 ∈ ( ℂ ↑m ℕ0 ) ) |
20 |
|
simp2l |
⊢ ( ( ( 𝐹 ∈ ( Poly ‘ 𝑆 ) ∧ ( 𝑎 ∈ ( ℂ ↑m ℕ0 ) ∧ 𝑏 ∈ ( ℂ ↑m ℕ0 ) ) ) ∧ ( 𝑛 ∈ ℕ0 ∧ 𝑚 ∈ ℕ0 ) ∧ ( ( ( 𝑎 “ ( ℤ≥ ‘ ( 𝑛 + 1 ) ) ) = { 0 } ∧ 𝐹 = ( 𝑧 ∈ ℂ ↦ Σ 𝑘 ∈ ( 0 ... 𝑛 ) ( ( 𝑎 ‘ 𝑘 ) · ( 𝑧 ↑ 𝑘 ) ) ) ) ∧ ( ( 𝑏 “ ( ℤ≥ ‘ ( 𝑚 + 1 ) ) ) = { 0 } ∧ 𝐹 = ( 𝑧 ∈ ℂ ↦ Σ 𝑘 ∈ ( 0 ... 𝑚 ) ( ( 𝑏 ‘ 𝑘 ) · ( 𝑧 ↑ 𝑘 ) ) ) ) ) ) → 𝑛 ∈ ℕ0 ) |
21 |
|
simp2r |
⊢ ( ( ( 𝐹 ∈ ( Poly ‘ 𝑆 ) ∧ ( 𝑎 ∈ ( ℂ ↑m ℕ0 ) ∧ 𝑏 ∈ ( ℂ ↑m ℕ0 ) ) ) ∧ ( 𝑛 ∈ ℕ0 ∧ 𝑚 ∈ ℕ0 ) ∧ ( ( ( 𝑎 “ ( ℤ≥ ‘ ( 𝑛 + 1 ) ) ) = { 0 } ∧ 𝐹 = ( 𝑧 ∈ ℂ ↦ Σ 𝑘 ∈ ( 0 ... 𝑛 ) ( ( 𝑎 ‘ 𝑘 ) · ( 𝑧 ↑ 𝑘 ) ) ) ) ∧ ( ( 𝑏 “ ( ℤ≥ ‘ ( 𝑚 + 1 ) ) ) = { 0 } ∧ 𝐹 = ( 𝑧 ∈ ℂ ↦ Σ 𝑘 ∈ ( 0 ... 𝑚 ) ( ( 𝑏 ‘ 𝑘 ) · ( 𝑧 ↑ 𝑘 ) ) ) ) ) ) → 𝑚 ∈ ℕ0 ) |
22 |
|
simp3ll |
⊢ ( ( ( 𝐹 ∈ ( Poly ‘ 𝑆 ) ∧ ( 𝑎 ∈ ( ℂ ↑m ℕ0 ) ∧ 𝑏 ∈ ( ℂ ↑m ℕ0 ) ) ) ∧ ( 𝑛 ∈ ℕ0 ∧ 𝑚 ∈ ℕ0 ) ∧ ( ( ( 𝑎 “ ( ℤ≥ ‘ ( 𝑛 + 1 ) ) ) = { 0 } ∧ 𝐹 = ( 𝑧 ∈ ℂ ↦ Σ 𝑘 ∈ ( 0 ... 𝑛 ) ( ( 𝑎 ‘ 𝑘 ) · ( 𝑧 ↑ 𝑘 ) ) ) ) ∧ ( ( 𝑏 “ ( ℤ≥ ‘ ( 𝑚 + 1 ) ) ) = { 0 } ∧ 𝐹 = ( 𝑧 ∈ ℂ ↦ Σ 𝑘 ∈ ( 0 ... 𝑚 ) ( ( 𝑏 ‘ 𝑘 ) · ( 𝑧 ↑ 𝑘 ) ) ) ) ) ) → ( 𝑎 “ ( ℤ≥ ‘ ( 𝑛 + 1 ) ) ) = { 0 } ) |
23 |
|
simp3rl |
⊢ ( ( ( 𝐹 ∈ ( Poly ‘ 𝑆 ) ∧ ( 𝑎 ∈ ( ℂ ↑m ℕ0 ) ∧ 𝑏 ∈ ( ℂ ↑m ℕ0 ) ) ) ∧ ( 𝑛 ∈ ℕ0 ∧ 𝑚 ∈ ℕ0 ) ∧ ( ( ( 𝑎 “ ( ℤ≥ ‘ ( 𝑛 + 1 ) ) ) = { 0 } ∧ 𝐹 = ( 𝑧 ∈ ℂ ↦ Σ 𝑘 ∈ ( 0 ... 𝑛 ) ( ( 𝑎 ‘ 𝑘 ) · ( 𝑧 ↑ 𝑘 ) ) ) ) ∧ ( ( 𝑏 “ ( ℤ≥ ‘ ( 𝑚 + 1 ) ) ) = { 0 } ∧ 𝐹 = ( 𝑧 ∈ ℂ ↦ Σ 𝑘 ∈ ( 0 ... 𝑚 ) ( ( 𝑏 ‘ 𝑘 ) · ( 𝑧 ↑ 𝑘 ) ) ) ) ) ) → ( 𝑏 “ ( ℤ≥ ‘ ( 𝑚 + 1 ) ) ) = { 0 } ) |
24 |
|
simp3lr |
⊢ ( ( ( 𝐹 ∈ ( Poly ‘ 𝑆 ) ∧ ( 𝑎 ∈ ( ℂ ↑m ℕ0 ) ∧ 𝑏 ∈ ( ℂ ↑m ℕ0 ) ) ) ∧ ( 𝑛 ∈ ℕ0 ∧ 𝑚 ∈ ℕ0 ) ∧ ( ( ( 𝑎 “ ( ℤ≥ ‘ ( 𝑛 + 1 ) ) ) = { 0 } ∧ 𝐹 = ( 𝑧 ∈ ℂ ↦ Σ 𝑘 ∈ ( 0 ... 𝑛 ) ( ( 𝑎 ‘ 𝑘 ) · ( 𝑧 ↑ 𝑘 ) ) ) ) ∧ ( ( 𝑏 “ ( ℤ≥ ‘ ( 𝑚 + 1 ) ) ) = { 0 } ∧ 𝐹 = ( 𝑧 ∈ ℂ ↦ Σ 𝑘 ∈ ( 0 ... 𝑚 ) ( ( 𝑏 ‘ 𝑘 ) · ( 𝑧 ↑ 𝑘 ) ) ) ) ) ) → 𝐹 = ( 𝑧 ∈ ℂ ↦ Σ 𝑘 ∈ ( 0 ... 𝑛 ) ( ( 𝑎 ‘ 𝑘 ) · ( 𝑧 ↑ 𝑘 ) ) ) ) |
25 |
|
oveq1 |
⊢ ( 𝑧 = 𝑤 → ( 𝑧 ↑ 𝑘 ) = ( 𝑤 ↑ 𝑘 ) ) |
26 |
25
|
oveq2d |
⊢ ( 𝑧 = 𝑤 → ( ( 𝑎 ‘ 𝑘 ) · ( 𝑧 ↑ 𝑘 ) ) = ( ( 𝑎 ‘ 𝑘 ) · ( 𝑤 ↑ 𝑘 ) ) ) |
27 |
26
|
sumeq2sdv |
⊢ ( 𝑧 = 𝑤 → Σ 𝑘 ∈ ( 0 ... 𝑛 ) ( ( 𝑎 ‘ 𝑘 ) · ( 𝑧 ↑ 𝑘 ) ) = Σ 𝑘 ∈ ( 0 ... 𝑛 ) ( ( 𝑎 ‘ 𝑘 ) · ( 𝑤 ↑ 𝑘 ) ) ) |
28 |
|
fveq2 |
⊢ ( 𝑘 = 𝑗 → ( 𝑎 ‘ 𝑘 ) = ( 𝑎 ‘ 𝑗 ) ) |
29 |
|
oveq2 |
⊢ ( 𝑘 = 𝑗 → ( 𝑤 ↑ 𝑘 ) = ( 𝑤 ↑ 𝑗 ) ) |
30 |
28 29
|
oveq12d |
⊢ ( 𝑘 = 𝑗 → ( ( 𝑎 ‘ 𝑘 ) · ( 𝑤 ↑ 𝑘 ) ) = ( ( 𝑎 ‘ 𝑗 ) · ( 𝑤 ↑ 𝑗 ) ) ) |
31 |
30
|
cbvsumv |
⊢ Σ 𝑘 ∈ ( 0 ... 𝑛 ) ( ( 𝑎 ‘ 𝑘 ) · ( 𝑤 ↑ 𝑘 ) ) = Σ 𝑗 ∈ ( 0 ... 𝑛 ) ( ( 𝑎 ‘ 𝑗 ) · ( 𝑤 ↑ 𝑗 ) ) |
32 |
27 31
|
eqtrdi |
⊢ ( 𝑧 = 𝑤 → Σ 𝑘 ∈ ( 0 ... 𝑛 ) ( ( 𝑎 ‘ 𝑘 ) · ( 𝑧 ↑ 𝑘 ) ) = Σ 𝑗 ∈ ( 0 ... 𝑛 ) ( ( 𝑎 ‘ 𝑗 ) · ( 𝑤 ↑ 𝑗 ) ) ) |
33 |
32
|
cbvmptv |
⊢ ( 𝑧 ∈ ℂ ↦ Σ 𝑘 ∈ ( 0 ... 𝑛 ) ( ( 𝑎 ‘ 𝑘 ) · ( 𝑧 ↑ 𝑘 ) ) ) = ( 𝑤 ∈ ℂ ↦ Σ 𝑗 ∈ ( 0 ... 𝑛 ) ( ( 𝑎 ‘ 𝑗 ) · ( 𝑤 ↑ 𝑗 ) ) ) |
34 |
24 33
|
eqtrdi |
⊢ ( ( ( 𝐹 ∈ ( Poly ‘ 𝑆 ) ∧ ( 𝑎 ∈ ( ℂ ↑m ℕ0 ) ∧ 𝑏 ∈ ( ℂ ↑m ℕ0 ) ) ) ∧ ( 𝑛 ∈ ℕ0 ∧ 𝑚 ∈ ℕ0 ) ∧ ( ( ( 𝑎 “ ( ℤ≥ ‘ ( 𝑛 + 1 ) ) ) = { 0 } ∧ 𝐹 = ( 𝑧 ∈ ℂ ↦ Σ 𝑘 ∈ ( 0 ... 𝑛 ) ( ( 𝑎 ‘ 𝑘 ) · ( 𝑧 ↑ 𝑘 ) ) ) ) ∧ ( ( 𝑏 “ ( ℤ≥ ‘ ( 𝑚 + 1 ) ) ) = { 0 } ∧ 𝐹 = ( 𝑧 ∈ ℂ ↦ Σ 𝑘 ∈ ( 0 ... 𝑚 ) ( ( 𝑏 ‘ 𝑘 ) · ( 𝑧 ↑ 𝑘 ) ) ) ) ) ) → 𝐹 = ( 𝑤 ∈ ℂ ↦ Σ 𝑗 ∈ ( 0 ... 𝑛 ) ( ( 𝑎 ‘ 𝑗 ) · ( 𝑤 ↑ 𝑗 ) ) ) ) |
35 |
|
simp3rr |
⊢ ( ( ( 𝐹 ∈ ( Poly ‘ 𝑆 ) ∧ ( 𝑎 ∈ ( ℂ ↑m ℕ0 ) ∧ 𝑏 ∈ ( ℂ ↑m ℕ0 ) ) ) ∧ ( 𝑛 ∈ ℕ0 ∧ 𝑚 ∈ ℕ0 ) ∧ ( ( ( 𝑎 “ ( ℤ≥ ‘ ( 𝑛 + 1 ) ) ) = { 0 } ∧ 𝐹 = ( 𝑧 ∈ ℂ ↦ Σ 𝑘 ∈ ( 0 ... 𝑛 ) ( ( 𝑎 ‘ 𝑘 ) · ( 𝑧 ↑ 𝑘 ) ) ) ) ∧ ( ( 𝑏 “ ( ℤ≥ ‘ ( 𝑚 + 1 ) ) ) = { 0 } ∧ 𝐹 = ( 𝑧 ∈ ℂ ↦ Σ 𝑘 ∈ ( 0 ... 𝑚 ) ( ( 𝑏 ‘ 𝑘 ) · ( 𝑧 ↑ 𝑘 ) ) ) ) ) ) → 𝐹 = ( 𝑧 ∈ ℂ ↦ Σ 𝑘 ∈ ( 0 ... 𝑚 ) ( ( 𝑏 ‘ 𝑘 ) · ( 𝑧 ↑ 𝑘 ) ) ) ) |
36 |
25
|
oveq2d |
⊢ ( 𝑧 = 𝑤 → ( ( 𝑏 ‘ 𝑘 ) · ( 𝑧 ↑ 𝑘 ) ) = ( ( 𝑏 ‘ 𝑘 ) · ( 𝑤 ↑ 𝑘 ) ) ) |
37 |
36
|
sumeq2sdv |
⊢ ( 𝑧 = 𝑤 → Σ 𝑘 ∈ ( 0 ... 𝑚 ) ( ( 𝑏 ‘ 𝑘 ) · ( 𝑧 ↑ 𝑘 ) ) = Σ 𝑘 ∈ ( 0 ... 𝑚 ) ( ( 𝑏 ‘ 𝑘 ) · ( 𝑤 ↑ 𝑘 ) ) ) |
38 |
|
fveq2 |
⊢ ( 𝑘 = 𝑗 → ( 𝑏 ‘ 𝑘 ) = ( 𝑏 ‘ 𝑗 ) ) |
39 |
38 29
|
oveq12d |
⊢ ( 𝑘 = 𝑗 → ( ( 𝑏 ‘ 𝑘 ) · ( 𝑤 ↑ 𝑘 ) ) = ( ( 𝑏 ‘ 𝑗 ) · ( 𝑤 ↑ 𝑗 ) ) ) |
40 |
39
|
cbvsumv |
⊢ Σ 𝑘 ∈ ( 0 ... 𝑚 ) ( ( 𝑏 ‘ 𝑘 ) · ( 𝑤 ↑ 𝑘 ) ) = Σ 𝑗 ∈ ( 0 ... 𝑚 ) ( ( 𝑏 ‘ 𝑗 ) · ( 𝑤 ↑ 𝑗 ) ) |
41 |
37 40
|
eqtrdi |
⊢ ( 𝑧 = 𝑤 → Σ 𝑘 ∈ ( 0 ... 𝑚 ) ( ( 𝑏 ‘ 𝑘 ) · ( 𝑧 ↑ 𝑘 ) ) = Σ 𝑗 ∈ ( 0 ... 𝑚 ) ( ( 𝑏 ‘ 𝑗 ) · ( 𝑤 ↑ 𝑗 ) ) ) |
42 |
41
|
cbvmptv |
⊢ ( 𝑧 ∈ ℂ ↦ Σ 𝑘 ∈ ( 0 ... 𝑚 ) ( ( 𝑏 ‘ 𝑘 ) · ( 𝑧 ↑ 𝑘 ) ) ) = ( 𝑤 ∈ ℂ ↦ Σ 𝑗 ∈ ( 0 ... 𝑚 ) ( ( 𝑏 ‘ 𝑗 ) · ( 𝑤 ↑ 𝑗 ) ) ) |
43 |
35 42
|
eqtrdi |
⊢ ( ( ( 𝐹 ∈ ( Poly ‘ 𝑆 ) ∧ ( 𝑎 ∈ ( ℂ ↑m ℕ0 ) ∧ 𝑏 ∈ ( ℂ ↑m ℕ0 ) ) ) ∧ ( 𝑛 ∈ ℕ0 ∧ 𝑚 ∈ ℕ0 ) ∧ ( ( ( 𝑎 “ ( ℤ≥ ‘ ( 𝑛 + 1 ) ) ) = { 0 } ∧ 𝐹 = ( 𝑧 ∈ ℂ ↦ Σ 𝑘 ∈ ( 0 ... 𝑛 ) ( ( 𝑎 ‘ 𝑘 ) · ( 𝑧 ↑ 𝑘 ) ) ) ) ∧ ( ( 𝑏 “ ( ℤ≥ ‘ ( 𝑚 + 1 ) ) ) = { 0 } ∧ 𝐹 = ( 𝑧 ∈ ℂ ↦ Σ 𝑘 ∈ ( 0 ... 𝑚 ) ( ( 𝑏 ‘ 𝑘 ) · ( 𝑧 ↑ 𝑘 ) ) ) ) ) ) → 𝐹 = ( 𝑤 ∈ ℂ ↦ Σ 𝑗 ∈ ( 0 ... 𝑚 ) ( ( 𝑏 ‘ 𝑗 ) · ( 𝑤 ↑ 𝑗 ) ) ) ) |
44 |
17 18 19 20 21 22 23 34 43
|
coeeulem |
⊢ ( ( ( 𝐹 ∈ ( Poly ‘ 𝑆 ) ∧ ( 𝑎 ∈ ( ℂ ↑m ℕ0 ) ∧ 𝑏 ∈ ( ℂ ↑m ℕ0 ) ) ) ∧ ( 𝑛 ∈ ℕ0 ∧ 𝑚 ∈ ℕ0 ) ∧ ( ( ( 𝑎 “ ( ℤ≥ ‘ ( 𝑛 + 1 ) ) ) = { 0 } ∧ 𝐹 = ( 𝑧 ∈ ℂ ↦ Σ 𝑘 ∈ ( 0 ... 𝑛 ) ( ( 𝑎 ‘ 𝑘 ) · ( 𝑧 ↑ 𝑘 ) ) ) ) ∧ ( ( 𝑏 “ ( ℤ≥ ‘ ( 𝑚 + 1 ) ) ) = { 0 } ∧ 𝐹 = ( 𝑧 ∈ ℂ ↦ Σ 𝑘 ∈ ( 0 ... 𝑚 ) ( ( 𝑏 ‘ 𝑘 ) · ( 𝑧 ↑ 𝑘 ) ) ) ) ) ) → 𝑎 = 𝑏 ) |
45 |
44
|
3expia |
⊢ ( ( ( 𝐹 ∈ ( Poly ‘ 𝑆 ) ∧ ( 𝑎 ∈ ( ℂ ↑m ℕ0 ) ∧ 𝑏 ∈ ( ℂ ↑m ℕ0 ) ) ) ∧ ( 𝑛 ∈ ℕ0 ∧ 𝑚 ∈ ℕ0 ) ) → ( ( ( ( 𝑎 “ ( ℤ≥ ‘ ( 𝑛 + 1 ) ) ) = { 0 } ∧ 𝐹 = ( 𝑧 ∈ ℂ ↦ Σ 𝑘 ∈ ( 0 ... 𝑛 ) ( ( 𝑎 ‘ 𝑘 ) · ( 𝑧 ↑ 𝑘 ) ) ) ) ∧ ( ( 𝑏 “ ( ℤ≥ ‘ ( 𝑚 + 1 ) ) ) = { 0 } ∧ 𝐹 = ( 𝑧 ∈ ℂ ↦ Σ 𝑘 ∈ ( 0 ... 𝑚 ) ( ( 𝑏 ‘ 𝑘 ) · ( 𝑧 ↑ 𝑘 ) ) ) ) ) → 𝑎 = 𝑏 ) ) |
46 |
45
|
rexlimdvva |
⊢ ( ( 𝐹 ∈ ( Poly ‘ 𝑆 ) ∧ ( 𝑎 ∈ ( ℂ ↑m ℕ0 ) ∧ 𝑏 ∈ ( ℂ ↑m ℕ0 ) ) ) → ( ∃ 𝑛 ∈ ℕ0 ∃ 𝑚 ∈ ℕ0 ( ( ( 𝑎 “ ( ℤ≥ ‘ ( 𝑛 + 1 ) ) ) = { 0 } ∧ 𝐹 = ( 𝑧 ∈ ℂ ↦ Σ 𝑘 ∈ ( 0 ... 𝑛 ) ( ( 𝑎 ‘ 𝑘 ) · ( 𝑧 ↑ 𝑘 ) ) ) ) ∧ ( ( 𝑏 “ ( ℤ≥ ‘ ( 𝑚 + 1 ) ) ) = { 0 } ∧ 𝐹 = ( 𝑧 ∈ ℂ ↦ Σ 𝑘 ∈ ( 0 ... 𝑚 ) ( ( 𝑏 ‘ 𝑘 ) · ( 𝑧 ↑ 𝑘 ) ) ) ) ) → 𝑎 = 𝑏 ) ) |
47 |
16 46
|
syl5bir |
⊢ ( ( 𝐹 ∈ ( Poly ‘ 𝑆 ) ∧ ( 𝑎 ∈ ( ℂ ↑m ℕ0 ) ∧ 𝑏 ∈ ( ℂ ↑m ℕ0 ) ) ) → ( ( ∃ 𝑛 ∈ ℕ0 ( ( 𝑎 “ ( ℤ≥ ‘ ( 𝑛 + 1 ) ) ) = { 0 } ∧ 𝐹 = ( 𝑧 ∈ ℂ ↦ Σ 𝑘 ∈ ( 0 ... 𝑛 ) ( ( 𝑎 ‘ 𝑘 ) · ( 𝑧 ↑ 𝑘 ) ) ) ) ∧ ∃ 𝑚 ∈ ℕ0 ( ( 𝑏 “ ( ℤ≥ ‘ ( 𝑚 + 1 ) ) ) = { 0 } ∧ 𝐹 = ( 𝑧 ∈ ℂ ↦ Σ 𝑘 ∈ ( 0 ... 𝑚 ) ( ( 𝑏 ‘ 𝑘 ) · ( 𝑧 ↑ 𝑘 ) ) ) ) ) → 𝑎 = 𝑏 ) ) |
48 |
47
|
ralrimivva |
⊢ ( 𝐹 ∈ ( Poly ‘ 𝑆 ) → ∀ 𝑎 ∈ ( ℂ ↑m ℕ0 ) ∀ 𝑏 ∈ ( ℂ ↑m ℕ0 ) ( ( ∃ 𝑛 ∈ ℕ0 ( ( 𝑎 “ ( ℤ≥ ‘ ( 𝑛 + 1 ) ) ) = { 0 } ∧ 𝐹 = ( 𝑧 ∈ ℂ ↦ Σ 𝑘 ∈ ( 0 ... 𝑛 ) ( ( 𝑎 ‘ 𝑘 ) · ( 𝑧 ↑ 𝑘 ) ) ) ) ∧ ∃ 𝑚 ∈ ℕ0 ( ( 𝑏 “ ( ℤ≥ ‘ ( 𝑚 + 1 ) ) ) = { 0 } ∧ 𝐹 = ( 𝑧 ∈ ℂ ↦ Σ 𝑘 ∈ ( 0 ... 𝑚 ) ( ( 𝑏 ‘ 𝑘 ) · ( 𝑧 ↑ 𝑘 ) ) ) ) ) → 𝑎 = 𝑏 ) ) |
49 |
|
imaeq1 |
⊢ ( 𝑎 = 𝑏 → ( 𝑎 “ ( ℤ≥ ‘ ( 𝑛 + 1 ) ) ) = ( 𝑏 “ ( ℤ≥ ‘ ( 𝑛 + 1 ) ) ) ) |
50 |
49
|
eqeq1d |
⊢ ( 𝑎 = 𝑏 → ( ( 𝑎 “ ( ℤ≥ ‘ ( 𝑛 + 1 ) ) ) = { 0 } ↔ ( 𝑏 “ ( ℤ≥ ‘ ( 𝑛 + 1 ) ) ) = { 0 } ) ) |
51 |
|
fveq1 |
⊢ ( 𝑎 = 𝑏 → ( 𝑎 ‘ 𝑘 ) = ( 𝑏 ‘ 𝑘 ) ) |
52 |
51
|
oveq1d |
⊢ ( 𝑎 = 𝑏 → ( ( 𝑎 ‘ 𝑘 ) · ( 𝑧 ↑ 𝑘 ) ) = ( ( 𝑏 ‘ 𝑘 ) · ( 𝑧 ↑ 𝑘 ) ) ) |
53 |
52
|
sumeq2sdv |
⊢ ( 𝑎 = 𝑏 → Σ 𝑘 ∈ ( 0 ... 𝑛 ) ( ( 𝑎 ‘ 𝑘 ) · ( 𝑧 ↑ 𝑘 ) ) = Σ 𝑘 ∈ ( 0 ... 𝑛 ) ( ( 𝑏 ‘ 𝑘 ) · ( 𝑧 ↑ 𝑘 ) ) ) |
54 |
53
|
mpteq2dv |
⊢ ( 𝑎 = 𝑏 → ( 𝑧 ∈ ℂ ↦ Σ 𝑘 ∈ ( 0 ... 𝑛 ) ( ( 𝑎 ‘ 𝑘 ) · ( 𝑧 ↑ 𝑘 ) ) ) = ( 𝑧 ∈ ℂ ↦ Σ 𝑘 ∈ ( 0 ... 𝑛 ) ( ( 𝑏 ‘ 𝑘 ) · ( 𝑧 ↑ 𝑘 ) ) ) ) |
55 |
54
|
eqeq2d |
⊢ ( 𝑎 = 𝑏 → ( 𝐹 = ( 𝑧 ∈ ℂ ↦ Σ 𝑘 ∈ ( 0 ... 𝑛 ) ( ( 𝑎 ‘ 𝑘 ) · ( 𝑧 ↑ 𝑘 ) ) ) ↔ 𝐹 = ( 𝑧 ∈ ℂ ↦ Σ 𝑘 ∈ ( 0 ... 𝑛 ) ( ( 𝑏 ‘ 𝑘 ) · ( 𝑧 ↑ 𝑘 ) ) ) ) ) |
56 |
50 55
|
anbi12d |
⊢ ( 𝑎 = 𝑏 → ( ( ( 𝑎 “ ( ℤ≥ ‘ ( 𝑛 + 1 ) ) ) = { 0 } ∧ 𝐹 = ( 𝑧 ∈ ℂ ↦ Σ 𝑘 ∈ ( 0 ... 𝑛 ) ( ( 𝑎 ‘ 𝑘 ) · ( 𝑧 ↑ 𝑘 ) ) ) ) ↔ ( ( 𝑏 “ ( ℤ≥ ‘ ( 𝑛 + 1 ) ) ) = { 0 } ∧ 𝐹 = ( 𝑧 ∈ ℂ ↦ Σ 𝑘 ∈ ( 0 ... 𝑛 ) ( ( 𝑏 ‘ 𝑘 ) · ( 𝑧 ↑ 𝑘 ) ) ) ) ) ) |
57 |
56
|
rexbidv |
⊢ ( 𝑎 = 𝑏 → ( ∃ 𝑛 ∈ ℕ0 ( ( 𝑎 “ ( ℤ≥ ‘ ( 𝑛 + 1 ) ) ) = { 0 } ∧ 𝐹 = ( 𝑧 ∈ ℂ ↦ Σ 𝑘 ∈ ( 0 ... 𝑛 ) ( ( 𝑎 ‘ 𝑘 ) · ( 𝑧 ↑ 𝑘 ) ) ) ) ↔ ∃ 𝑛 ∈ ℕ0 ( ( 𝑏 “ ( ℤ≥ ‘ ( 𝑛 + 1 ) ) ) = { 0 } ∧ 𝐹 = ( 𝑧 ∈ ℂ ↦ Σ 𝑘 ∈ ( 0 ... 𝑛 ) ( ( 𝑏 ‘ 𝑘 ) · ( 𝑧 ↑ 𝑘 ) ) ) ) ) ) |
58 |
|
fvoveq1 |
⊢ ( 𝑛 = 𝑚 → ( ℤ≥ ‘ ( 𝑛 + 1 ) ) = ( ℤ≥ ‘ ( 𝑚 + 1 ) ) ) |
59 |
58
|
imaeq2d |
⊢ ( 𝑛 = 𝑚 → ( 𝑏 “ ( ℤ≥ ‘ ( 𝑛 + 1 ) ) ) = ( 𝑏 “ ( ℤ≥ ‘ ( 𝑚 + 1 ) ) ) ) |
60 |
59
|
eqeq1d |
⊢ ( 𝑛 = 𝑚 → ( ( 𝑏 “ ( ℤ≥ ‘ ( 𝑛 + 1 ) ) ) = { 0 } ↔ ( 𝑏 “ ( ℤ≥ ‘ ( 𝑚 + 1 ) ) ) = { 0 } ) ) |
61 |
|
oveq2 |
⊢ ( 𝑛 = 𝑚 → ( 0 ... 𝑛 ) = ( 0 ... 𝑚 ) ) |
62 |
61
|
sumeq1d |
⊢ ( 𝑛 = 𝑚 → Σ 𝑘 ∈ ( 0 ... 𝑛 ) ( ( 𝑏 ‘ 𝑘 ) · ( 𝑧 ↑ 𝑘 ) ) = Σ 𝑘 ∈ ( 0 ... 𝑚 ) ( ( 𝑏 ‘ 𝑘 ) · ( 𝑧 ↑ 𝑘 ) ) ) |
63 |
62
|
mpteq2dv |
⊢ ( 𝑛 = 𝑚 → ( 𝑧 ∈ ℂ ↦ Σ 𝑘 ∈ ( 0 ... 𝑛 ) ( ( 𝑏 ‘ 𝑘 ) · ( 𝑧 ↑ 𝑘 ) ) ) = ( 𝑧 ∈ ℂ ↦ Σ 𝑘 ∈ ( 0 ... 𝑚 ) ( ( 𝑏 ‘ 𝑘 ) · ( 𝑧 ↑ 𝑘 ) ) ) ) |
64 |
63
|
eqeq2d |
⊢ ( 𝑛 = 𝑚 → ( 𝐹 = ( 𝑧 ∈ ℂ ↦ Σ 𝑘 ∈ ( 0 ... 𝑛 ) ( ( 𝑏 ‘ 𝑘 ) · ( 𝑧 ↑ 𝑘 ) ) ) ↔ 𝐹 = ( 𝑧 ∈ ℂ ↦ Σ 𝑘 ∈ ( 0 ... 𝑚 ) ( ( 𝑏 ‘ 𝑘 ) · ( 𝑧 ↑ 𝑘 ) ) ) ) ) |
65 |
60 64
|
anbi12d |
⊢ ( 𝑛 = 𝑚 → ( ( ( 𝑏 “ ( ℤ≥ ‘ ( 𝑛 + 1 ) ) ) = { 0 } ∧ 𝐹 = ( 𝑧 ∈ ℂ ↦ Σ 𝑘 ∈ ( 0 ... 𝑛 ) ( ( 𝑏 ‘ 𝑘 ) · ( 𝑧 ↑ 𝑘 ) ) ) ) ↔ ( ( 𝑏 “ ( ℤ≥ ‘ ( 𝑚 + 1 ) ) ) = { 0 } ∧ 𝐹 = ( 𝑧 ∈ ℂ ↦ Σ 𝑘 ∈ ( 0 ... 𝑚 ) ( ( 𝑏 ‘ 𝑘 ) · ( 𝑧 ↑ 𝑘 ) ) ) ) ) ) |
66 |
65
|
cbvrexvw |
⊢ ( ∃ 𝑛 ∈ ℕ0 ( ( 𝑏 “ ( ℤ≥ ‘ ( 𝑛 + 1 ) ) ) = { 0 } ∧ 𝐹 = ( 𝑧 ∈ ℂ ↦ Σ 𝑘 ∈ ( 0 ... 𝑛 ) ( ( 𝑏 ‘ 𝑘 ) · ( 𝑧 ↑ 𝑘 ) ) ) ) ↔ ∃ 𝑚 ∈ ℕ0 ( ( 𝑏 “ ( ℤ≥ ‘ ( 𝑚 + 1 ) ) ) = { 0 } ∧ 𝐹 = ( 𝑧 ∈ ℂ ↦ Σ 𝑘 ∈ ( 0 ... 𝑚 ) ( ( 𝑏 ‘ 𝑘 ) · ( 𝑧 ↑ 𝑘 ) ) ) ) ) |
67 |
57 66
|
bitrdi |
⊢ ( 𝑎 = 𝑏 → ( ∃ 𝑛 ∈ ℕ0 ( ( 𝑎 “ ( ℤ≥ ‘ ( 𝑛 + 1 ) ) ) = { 0 } ∧ 𝐹 = ( 𝑧 ∈ ℂ ↦ Σ 𝑘 ∈ ( 0 ... 𝑛 ) ( ( 𝑎 ‘ 𝑘 ) · ( 𝑧 ↑ 𝑘 ) ) ) ) ↔ ∃ 𝑚 ∈ ℕ0 ( ( 𝑏 “ ( ℤ≥ ‘ ( 𝑚 + 1 ) ) ) = { 0 } ∧ 𝐹 = ( 𝑧 ∈ ℂ ↦ Σ 𝑘 ∈ ( 0 ... 𝑚 ) ( ( 𝑏 ‘ 𝑘 ) · ( 𝑧 ↑ 𝑘 ) ) ) ) ) ) |
68 |
67
|
reu4 |
⊢ ( ∃! 𝑎 ∈ ( ℂ ↑m ℕ0 ) ∃ 𝑛 ∈ ℕ0 ( ( 𝑎 “ ( ℤ≥ ‘ ( 𝑛 + 1 ) ) ) = { 0 } ∧ 𝐹 = ( 𝑧 ∈ ℂ ↦ Σ 𝑘 ∈ ( 0 ... 𝑛 ) ( ( 𝑎 ‘ 𝑘 ) · ( 𝑧 ↑ 𝑘 ) ) ) ) ↔ ( ∃ 𝑎 ∈ ( ℂ ↑m ℕ0 ) ∃ 𝑛 ∈ ℕ0 ( ( 𝑎 “ ( ℤ≥ ‘ ( 𝑛 + 1 ) ) ) = { 0 } ∧ 𝐹 = ( 𝑧 ∈ ℂ ↦ Σ 𝑘 ∈ ( 0 ... 𝑛 ) ( ( 𝑎 ‘ 𝑘 ) · ( 𝑧 ↑ 𝑘 ) ) ) ) ∧ ∀ 𝑎 ∈ ( ℂ ↑m ℕ0 ) ∀ 𝑏 ∈ ( ℂ ↑m ℕ0 ) ( ( ∃ 𝑛 ∈ ℕ0 ( ( 𝑎 “ ( ℤ≥ ‘ ( 𝑛 + 1 ) ) ) = { 0 } ∧ 𝐹 = ( 𝑧 ∈ ℂ ↦ Σ 𝑘 ∈ ( 0 ... 𝑛 ) ( ( 𝑎 ‘ 𝑘 ) · ( 𝑧 ↑ 𝑘 ) ) ) ) ∧ ∃ 𝑚 ∈ ℕ0 ( ( 𝑏 “ ( ℤ≥ ‘ ( 𝑚 + 1 ) ) ) = { 0 } ∧ 𝐹 = ( 𝑧 ∈ ℂ ↦ Σ 𝑘 ∈ ( 0 ... 𝑚 ) ( ( 𝑏 ‘ 𝑘 ) · ( 𝑧 ↑ 𝑘 ) ) ) ) ) → 𝑎 = 𝑏 ) ) ) |
69 |
15 48 68
|
sylanbrc |
⊢ ( 𝐹 ∈ ( Poly ‘ 𝑆 ) → ∃! 𝑎 ∈ ( ℂ ↑m ℕ0 ) ∃ 𝑛 ∈ ℕ0 ( ( 𝑎 “ ( ℤ≥ ‘ ( 𝑛 + 1 ) ) ) = { 0 } ∧ 𝐹 = ( 𝑧 ∈ ℂ ↦ Σ 𝑘 ∈ ( 0 ... 𝑛 ) ( ( 𝑎 ‘ 𝑘 ) · ( 𝑧 ↑ 𝑘 ) ) ) ) ) |