Metamath Proof Explorer

Theorem mncn0

Description: A monic polynomial is not zero. (Contributed by Stefan O'Rear, 5-Dec-2014)

Ref Expression
Assertion mncn0 ⊢ P ∈ Monic ⁡ S → P ≠ 0 𝑝

Proof

Step Hyp Ref Expression
1 mnccoe ⊢ P ∈ Monic ⁡ S → coeff ⁡ P ⁡ deg ⁡ P = 1
2 coe0 ⊢ coeff ⁡ 0 𝑝 = ℕ 0 × 0
3 2 fveq1i ⊢ coeff ⁡ 0 𝑝 ⁡ deg ⁡ 0 𝑝 = ℕ 0 × 0 ⁡ deg ⁡ 0 𝑝
4 dgr0 ⊢ deg ⁡ 0 𝑝 = 0
5 0nn0 ⊢ 0 ∈ ℕ 0
6 4 5 eqeltri ⊢ deg ⁡ 0 𝑝 ∈ ℕ 0
7 c0ex ⊢ 0 ∈ V
8 7 fvconst2 ⊢ deg ⁡ 0 𝑝 ∈ ℕ 0 → ℕ 0 × 0 ⁡ deg ⁡ 0 𝑝 = 0
9 6 8 ax-mp ⊢ ℕ 0 × 0 ⁡ deg ⁡ 0 𝑝 = 0
10 3 9 eqtri ⊢ coeff ⁡ 0 𝑝 ⁡ deg ⁡ 0 𝑝 = 0
11 0ne1 ⊢ 0 ≠ 1
12 10 11 eqnetri ⊢ coeff ⁡ 0 𝑝 ⁡ deg ⁡ 0 𝑝 ≠ 1
13 fveq2 ⊢ P = 0 𝑝 → coeff ⁡ P = coeff ⁡ 0 𝑝
14 fveq2 ⊢ P = 0 𝑝 → deg ⁡ P = deg ⁡ 0 𝑝
15 13 14 fveq12d ⊢ P = 0 𝑝 → coeff ⁡ P ⁡ deg ⁡ P = coeff ⁡ 0 𝑝 ⁡ deg ⁡ 0 𝑝
16 15 neeq1d ⊢ P = 0 𝑝 → coeff ⁡ P ⁡ deg ⁡ P ≠ 1 ↔ coeff ⁡ 0 𝑝 ⁡ deg ⁡ 0 𝑝 ≠ 1
17 12 16 mpbiri ⊢ P = 0 𝑝 → coeff ⁡ P ⁡ deg ⁡ P ≠ 1
18 17 necon2i ⊢ coeff ⁡ P ⁡ deg ⁡ P = 1 → P ≠ 0 𝑝
19 1 18 syl ⊢ P ∈ Monic ⁡ S → P ≠ 0 𝑝