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

Metamath Proof Explorer

Theorem n0p

Description: A polynomial with a nonzero coefficient is not the zero polynomial. (Contributed by Glauco Siliprandi, 5-Apr-2020)

Ref Expression
Assertion n0p ⊢ P ∈ Poly ⁡ ℤ ∧ N ∈ ℕ 0 ∧ coeff ⁡ P ⁡ N ≠ 0 → P ≠ 0 𝑝

Proof

Step Hyp Ref Expression
1 fveq2 ⊢ P = 0 𝑝 → coeff ⁡ P = coeff ⁡ 0 𝑝
2 coe0 ⊢ coeff ⁡ 0 𝑝 = ℕ 0 × 0
3 2 a1i ⊢ P = 0 𝑝 → coeff ⁡ 0 𝑝 = ℕ 0 × 0
4 1 3 eqtrd ⊢ P = 0 𝑝 → coeff ⁡ P = ℕ 0 × 0
5 4 fveq1d ⊢ P = 0 𝑝 → coeff ⁡ P ⁡ N = ℕ 0 × 0 ⁡ N
6 5 adantl ⊢ N ∈ ℕ 0 ∧ P = 0 𝑝 → coeff ⁡ P ⁡ N = ℕ 0 × 0 ⁡ N
7 id ⊢ N ∈ ℕ 0 → N ∈ ℕ 0
8 c0ex ⊢ 0 ∈ V
9 8 fvconst2 ⊢ N ∈ ℕ 0 → ℕ 0 × 0 ⁡ N = 0
10 7 9 syl ⊢ N ∈ ℕ 0 → ℕ 0 × 0 ⁡ N = 0
11 10 adantr ⊢ N ∈ ℕ 0 ∧ P = 0 𝑝 → ℕ 0 × 0 ⁡ N = 0
12 6 11 eqtrd ⊢ N ∈ ℕ 0 ∧ P = 0 𝑝 → coeff ⁡ P ⁡ N = 0
13 12 3ad2antl2 ⊢ P ∈ Poly ⁡ ℤ ∧ N ∈ ℕ 0 ∧ coeff ⁡ P ⁡ N ≠ 0 ∧ P = 0 𝑝 → coeff ⁡ P ⁡ N = 0
14 neneq ⊢ coeff ⁡ P ⁡ N ≠ 0 → ¬ coeff ⁡ P ⁡ N = 0
15 14 adantr ⊢ coeff ⁡ P ⁡ N ≠ 0 ∧ P = 0 𝑝 → ¬ coeff ⁡ P ⁡ N = 0
16 15 3ad2antl3 ⊢ P ∈ Poly ⁡ ℤ ∧ N ∈ ℕ 0 ∧ coeff ⁡ P ⁡ N ≠ 0 ∧ P = 0 𝑝 → ¬ coeff ⁡ P ⁡ N = 0
17 13 16 pm2.65da ⊢ P ∈ Poly ⁡ ℤ ∧ N ∈ ℕ 0 ∧ coeff ⁡ P ⁡ N ≠ 0 → ¬ P = 0 𝑝
18 17 neqned ⊢ P ∈ Poly ⁡ ℤ ∧ N ∈ ℕ 0 ∧ coeff ⁡ P ⁡ N ≠ 0 → P ≠ 0 𝑝