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 ( ( 𝑃 ∈ ( Poly ‘ ℤ ) ∧ 𝑁 ∈ ℕ0 ∧ ( ( coeff ‘ 𝑃 ) ‘ 𝑁 ) ≠ 0 ) → 𝑃 ≠ 0𝑝 )

Proof

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