Metamath Proof Explorer


Theorem dgrub2

Description: All the coefficients above the degree of F are zero. (Contributed by Mario Carneiro, 23-Jul-2014)

Ref Expression
Hypotheses dgrub.1 𝐴 = ( coeff ‘ 𝐹 )
dgrub.2 𝑁 = ( deg ‘ 𝐹 )
Assertion dgrub2 ( 𝐹 ∈ ( Poly ‘ 𝑆 ) → ( 𝐴 “ ( ℤ ‘ ( 𝑁 + 1 ) ) ) = { 0 } )

Proof

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 } )