Theorem mncn0

Description: A monic polynomial is not zero. (Contributed by Stefan O'Rear, 5-Dec-2014)

	Ref	Expression
Assertion	mncn0	|- ( P e. ( Monic ` S ) -> P =/= 0p )

Proof

Step	Hyp	Ref	Expression
1		mnccoe	|- ( P e. ( Monic ` S ) -> ( ( coeff ` P ) ` ( deg ` P ) ) = 1 )
2		coe0	|- ( coeff ` 0p ) = ( NN0 X. { 0 } )
3	2	fveq1i	|- ( ( coeff ` 0p ) ` ( deg ` 0p ) ) = ( ( NN0 X. { 0 } ) ` ( deg ` 0p ) )
4		dgr0	|- ( deg ` 0p ) = 0
5		0nn0	|- 0 e. NN0
6	4 5	eqeltri	|- ( deg ` 0p ) e. NN0
7		c0ex	|- 0 e. _V
8	7	fvconst2	|- ( ( deg ` 0p ) e. NN0 -> ( ( NN0 X. { 0 } ) ` ( deg ` 0p ) ) = 0 )
9	6 8	ax-mp	|- ( ( NN0 X. { 0 } ) ` ( deg ` 0p ) ) = 0
10	3 9	eqtri	|- ( ( coeff ` 0p ) ` ( deg ` 0p ) ) = 0
11		0ne1	|- 0 =/= 1
12	10 11	eqnetri	|- ( ( coeff ` 0p ) ` ( deg ` 0p ) ) =/= 1
13		fveq2	|- ( P = 0p -> ( coeff ` P ) = ( coeff ` 0p ) )
14		fveq2	|- ( P = 0p -> ( deg ` P ) = ( deg ` 0p ) )
15	13 14	fveq12d	|- ( P = 0p -> ( ( coeff ` P ) ` ( deg ` P ) ) = ( ( coeff ` 0p ) ` ( deg ` 0p ) ) )
16	15	neeq1d	|- ( P = 0p -> ( ( ( coeff ` P ) ` ( deg ` P ) ) =/= 1 <-> ( ( coeff ` 0p ) ` ( deg ` 0p ) ) =/= 1 ) )
17	12 16	mpbiri	|- ( P = 0p -> ( ( coeff ` P ) ` ( deg ` P ) ) =/= 1 )
18	17	necon2i	|- ( ( ( coeff ` P ) ` ( deg ` P ) ) = 1 -> P =/= 0p )
19	1 18	syl	|- ( P e. ( Monic ` S ) -> P =/= 0p )