This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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