Step |
Hyp |
Ref |
Expression |
1 |
|
dgrub.1 |
⊢ 𝐴 = ( coeff ‘ 𝐹 ) |
2 |
|
dgrub.2 |
⊢ 𝑁 = ( deg ‘ 𝐹 ) |
3 |
1 2
|
dgrub |
⊢ ( ( 𝐹 ∈ ( Poly ‘ 𝑆 ) ∧ 𝑘 ∈ ℕ0 ∧ ( 𝐴 ‘ 𝑘 ) ≠ 0 ) → 𝑘 ≤ 𝑁 ) |
4 |
3
|
3expia |
⊢ ( ( 𝐹 ∈ ( Poly ‘ 𝑆 ) ∧ 𝑘 ∈ ℕ0 ) → ( ( 𝐴 ‘ 𝑘 ) ≠ 0 → 𝑘 ≤ 𝑁 ) ) |
5 |
4
|
ralrimiva |
⊢ ( 𝐹 ∈ ( Poly ‘ 𝑆 ) → ∀ 𝑘 ∈ ℕ0 ( ( 𝐴 ‘ 𝑘 ) ≠ 0 → 𝑘 ≤ 𝑁 ) ) |
6 |
|
dgrcl |
⊢ ( 𝐹 ∈ ( Poly ‘ 𝑆 ) → ( deg ‘ 𝐹 ) ∈ ℕ0 ) |
7 |
2 6
|
eqeltrid |
⊢ ( 𝐹 ∈ ( Poly ‘ 𝑆 ) → 𝑁 ∈ ℕ0 ) |
8 |
1
|
coef3 |
⊢ ( 𝐹 ∈ ( Poly ‘ 𝑆 ) → 𝐴 : ℕ0 ⟶ ℂ ) |
9 |
|
plyco0 |
⊢ ( ( 𝑁 ∈ ℕ0 ∧ 𝐴 : ℕ0 ⟶ ℂ ) → ( ( 𝐴 “ ( ℤ≥ ‘ ( 𝑁 + 1 ) ) ) = { 0 } ↔ ∀ 𝑘 ∈ ℕ0 ( ( 𝐴 ‘ 𝑘 ) ≠ 0 → 𝑘 ≤ 𝑁 ) ) ) |
10 |
7 8 9
|
syl2anc |
⊢ ( 𝐹 ∈ ( Poly ‘ 𝑆 ) → ( ( 𝐴 “ ( ℤ≥ ‘ ( 𝑁 + 1 ) ) ) = { 0 } ↔ ∀ 𝑘 ∈ ℕ0 ( ( 𝐴 ‘ 𝑘 ) ≠ 0 → 𝑘 ≤ 𝑁 ) ) ) |
11 |
5 10
|
mpbird |
⊢ ( 𝐹 ∈ ( Poly ‘ 𝑆 ) → ( 𝐴 “ ( ℤ≥ ‘ ( 𝑁 + 1 ) ) ) = { 0 } ) |