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