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	$$⊢\left(P\in \mathrm{Poly}\left(\mathbb{Z}\right)\wedge N\in {\mathbb{N}}_0\wedge \mathrm{coeff}\left(P\right)\left(N\right)\ne 0\right)\to P\ne 0_{𝑝}$$

Proof

Step	Hyp	Ref	Expression
1		fveq2	$$⊢P=0_{𝑝}\to \mathrm{coeff}\left(P\right)=\mathrm{coeff}\left(0_{𝑝}\right)$$
2		coe0	$$⊢\mathrm{coeff}\left(0_{𝑝}\right)={\mathbb{N}}_0\times \left\{0\right\}$$
3	2	a1i	$$⊢P=0_{𝑝}\to \mathrm{coeff}\left(0_{𝑝}\right)={\mathbb{N}}_0\times \left\{0\right\}$$
4	1 3	eqtrd	$$⊢P=0_{𝑝}\to \mathrm{coeff}\left(P\right)={\mathbb{N}}_0\times \left\{0\right\}$$
5	4	fveq1d	$$⊢P=0_{𝑝}\to \mathrm{coeff}\left(P\right)\left(N\right)=\left({\mathbb{N}}_0\times \left\{0\right\}\right)\left(N\right)$$
6	5	adantl	$$⊢\left(N\in {\mathbb{N}}_0\wedge P=0_{𝑝}\right)\to \mathrm{coeff}\left(P\right)\left(N\right)=\left({\mathbb{N}}_0\times \left\{0\right\}\right)\left(N\right)$$
7		id	$$⊢N\in {\mathbb{N}}_0\to N\in {\mathbb{N}}_0$$
8		c0ex	$$⊢0\in \mathrm{V}$$
9	8	fvconst2	$$⊢N\in {\mathbb{N}}_0\to \left({\mathbb{N}}_0\times \left\{0\right\}\right)\left(N\right)=0$$
10	7 9	syl	$$⊢N\in {\mathbb{N}}_0\to \left({\mathbb{N}}_0\times \left\{0\right\}\right)\left(N\right)=0$$
11	10	adantr	$$⊢\left(N\in {\mathbb{N}}_0\wedge P=0_{𝑝}\right)\to \left({\mathbb{N}}_0\times \left\{0\right\}\right)\left(N\right)=0$$
12	6 11	eqtrd	$$⊢\left(N\in {\mathbb{N}}_0\wedge P=0_{𝑝}\right)\to \mathrm{coeff}\left(P\right)\left(N\right)=0$$
13	12	3ad2antl2	$$⊢\left(\left(P\in \mathrm{Poly}\left(\mathbb{Z}\right)\wedge N\in {\mathbb{N}}_0\wedge \mathrm{coeff}\left(P\right)\left(N\right)\ne 0\right)\wedge P=0_{𝑝}\right)\to \mathrm{coeff}\left(P\right)\left(N\right)=0$$
14		neneq	$$⊢\mathrm{coeff}\left(P\right)\left(N\right)\ne 0\to \neg \mathrm{coeff}\left(P\right)\left(N\right)=0$$
15	14	adantr	$$⊢\left(\mathrm{coeff}\left(P\right)\left(N\right)\ne 0\wedge P=0_{𝑝}\right)\to \neg \mathrm{coeff}\left(P\right)\left(N\right)=0$$
16	15	3ad2antl3	$$⊢\left(\left(P\in \mathrm{Poly}\left(\mathbb{Z}\right)\wedge N\in {\mathbb{N}}_0\wedge \mathrm{coeff}\left(P\right)\left(N\right)\ne 0\right)\wedge P=0_{𝑝}\right)\to \neg \mathrm{coeff}\left(P\right)\left(N\right)=0$$
17	13 16	pm2.65da	$$⊢\left(P\in \mathrm{Poly}\left(\mathbb{Z}\right)\wedge N\in {\mathbb{N}}_0\wedge \mathrm{coeff}\left(P\right)\left(N\right)\ne 0\right)\to \neg P=0_{𝑝}$$
18	17	neqned	$$⊢\left(P\in \mathrm{Poly}\left(\mathbb{Z}\right)\wedge N\in {\mathbb{N}}_0\wedge \mathrm{coeff}\left(P\right)\left(N\right)\ne 0\right)\to P\ne 0_{𝑝}$$