This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 
|- ( ( P e. ( Poly ` ZZ ) /\ N e. NN0 /\ ( ( coeff ` P ) ` N ) =/= 0 ) -> P =/= 0p )

Proof

Step Hyp Ref Expression
1 fveq2 
 |-  ( P = 0p -> ( coeff ` P ) = ( coeff ` 0p ) )
2 coe0 
 |-  ( coeff ` 0p ) = ( NN0 X. { 0 } )
3 2 a1i 
 |-  ( P = 0p -> ( coeff ` 0p ) = ( NN0 X. { 0 } ) )
4 1 3 eqtrd 
 |-  ( P = 0p -> ( coeff ` P ) = ( NN0 X. { 0 } ) )
5 4 fveq1d 
 |-  ( P = 0p -> ( ( coeff ` P ) ` N ) = ( ( NN0 X. { 0 } ) ` N ) )
6 5 adantl 
 |-  ( ( N e. NN0 /\ P = 0p ) -> ( ( coeff ` P ) ` N ) = ( ( NN0 X. { 0 } ) ` N ) )
7 id 
 |-  ( N e. NN0 -> N e. NN0 )
8 c0ex 
 |-  0 e. _V
9 8 fvconst2 
 |-  ( N e. NN0 -> ( ( NN0 X. { 0 } ) ` N ) = 0 )
10 7 9 syl 
 |-  ( N e. NN0 -> ( ( NN0 X. { 0 } ) ` N ) = 0 )
11 10 adantr 
 |-  ( ( N e. NN0 /\ P = 0p ) -> ( ( NN0 X. { 0 } ) ` N ) = 0 )
12 6 11 eqtrd 
 |-  ( ( N e. NN0 /\ P = 0p ) -> ( ( coeff ` P ) ` N ) = 0 )
13 12 3ad2antl2 
 |-  ( ( ( P e. ( Poly ` ZZ ) /\ N e. NN0 /\ ( ( coeff ` P ) ` N ) =/= 0 ) /\ P = 0p ) -> ( ( coeff ` P ) ` N ) = 0 )
14 neneq 
 |-  ( ( ( coeff ` P ) ` N ) =/= 0 -> -. ( ( coeff ` P ) ` N ) = 0 )
15 14 adantr 
 |-  ( ( ( ( coeff ` P ) ` N ) =/= 0 /\ P = 0p ) -> -. ( ( coeff ` P ) ` N ) = 0 )
16 15 3ad2antl3 
 |-  ( ( ( P e. ( Poly ` ZZ ) /\ N e. NN0 /\ ( ( coeff ` P ) ` N ) =/= 0 ) /\ P = 0p ) -> -. ( ( coeff ` P ) ` N ) = 0 )
17 13 16 pm2.65da 
 |-  ( ( P e. ( Poly ` ZZ ) /\ N e. NN0 /\ ( ( coeff ` P ) ` N ) =/= 0 ) -> -. P = 0p )
18 17 neqned 
 |-  ( ( P e. ( Poly ` ZZ ) /\ N e. NN0 /\ ( ( coeff ` P ) ` N ) =/= 0 ) -> P =/= 0p )