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 ⊢ A = coeff ⁡ F
dgrub.2 ⊢ N = deg ⁡ F
Assertion dgrub2 ⊢ F ∈ Poly ⁡ S → A ℤ ≥ N + 1 = 0

Proof

Step Hyp Ref Expression
1 dgrub.1 ⊢ A = coeff ⁡ F
2 dgrub.2 ⊢ N = deg ⁡ F
3 1 2 dgrub ⊢ F ∈ Poly ⁡ S ∧ k ∈ ℕ 0 ∧ A ⁡ k ≠ 0 → k ≤ N
4 3 3expia ⊢ F ∈ Poly ⁡ S ∧ k ∈ ℕ 0 → A ⁡ k ≠ 0 → k ≤ N
5 4 ralrimiva ⊢ F ∈ Poly ⁡ S → ∀ k ∈ ℕ 0 A ⁡ k ≠ 0 → k ≤ N
6 dgrcl ⊢ F ∈ Poly ⁡ S → deg ⁡ F ∈ ℕ 0
7 2 6 eqeltrid ⊢ F ∈ Poly ⁡ S → N ∈ ℕ 0
8 1 coef3 ⊢ F ∈ Poly ⁡ S → A : ℕ 0 ⟶ ℂ
9 plyco0 ⊢ N ∈ ℕ 0 ∧ A : ℕ 0 ⟶ ℂ → A ℤ ≥ N + 1 = 0 ↔ ∀ k ∈ ℕ 0 A ⁡ k ≠ 0 → k ≤ N
10 7 8 9 syl2anc ⊢ F ∈ Poly ⁡ S → A ℤ ≥ N + 1 = 0 ↔ ∀ k ∈ ℕ 0 A ⁡ k ≠ 0 → k ≤ N
11 5 10 mpbird ⊢ F ∈ Poly ⁡ S → A ℤ ≥ N + 1 = 0