Theorem ne0p

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

	Ref	Expression
Assertion	ne0p	|- ( ( A e. CC /\ ( F ` A ) =/= 0 ) -> F =/= 0p )

Proof

Step	Hyp	Ref	Expression
1		0pval	|- ( A e. CC -> ( 0p ` A ) = 0 )
2		fveq1	|- ( F = 0p -> ( F ` A ) = ( 0p ` A ) )
3	2	eqeq1d	|- ( F = 0p -> ( ( F ` A ) = 0 <-> ( 0p ` A ) = 0 ) )
4	1 3	syl5ibrcom	|- ( A e. CC -> ( F = 0p -> ( F ` A ) = 0 ) )
5	4	necon3d	|- ( A e. CC -> ( ( F ` A ) =/= 0 -> F =/= 0p ) )
6	5	imp	|- ( ( A e. CC /\ ( F ` A ) =/= 0 ) -> F =/= 0p )