Theorem ne0p

Description: A test to show that a polynomial is nonzero. (Contributed by Mario Carneiro, 23-Jul-2014)

	Ref	Expression
Assertion	ne0p	$$⊢\left(A\in ℂ\wedge F\left(A\right)\ne 0\right)\to F\ne 0_{𝑝}$$

Proof

Step	Hyp	Ref	Expression
1		0pval	$$⊢A\in ℂ\to 0_{𝑝}\left(A\right)=0$$
2		fveq1	$$⊢F=0_{𝑝}\to F\left(A\right)=0_{𝑝}\left(A\right)$$
3	2	eqeq1d	$$⊢F=0_{𝑝}\to \left(F\left(A\right)=0\leftrightarrow 0_{𝑝}\left(A\right)=0\right)$$
4	1 3	syl5ibrcom	$$⊢A\in ℂ\to \left(F=0_{𝑝}\to F\left(A\right)=0\right)$$
5	4	necon3d	$$⊢A\in ℂ\to \left(F\left(A\right)\ne 0\to F\ne 0_{𝑝}\right)$$
6	5	imp	$$⊢\left(A\in ℂ\wedge F\left(A\right)\ne 0\right)\to F\ne 0_{𝑝}$$