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 Poly N 0 coeff P N 0 P 0 𝑝

Proof

Step Hyp Ref Expression
1 fveq2 P = 0 𝑝 coeff P = coeff 0 𝑝
2 coe0 coeff 0 𝑝 = 0 × 0
3 2 a1i P = 0 𝑝 coeff 0 𝑝 = 0 × 0
4 1 3 eqtrd P = 0 𝑝 coeff P = 0 × 0
5 4 fveq1d P = 0 𝑝 coeff P N = 0 × 0 N
6 5 adantl N 0 P = 0 𝑝 coeff P N = 0 × 0 N
7 id N 0 N 0
8 c0ex 0 V
9 8 fvconst2 N 0 0 × 0 N = 0
10 7 9 syl N 0 0 × 0 N = 0
11 10 adantr N 0 P = 0 𝑝 0 × 0 N = 0
12 6 11 eqtrd N 0 P = 0 𝑝 coeff P N = 0
13 12 3ad2antl2 P Poly N 0 coeff P N 0 P = 0 𝑝 coeff P N = 0
14 neneq coeff P N 0 ¬ coeff P N = 0
15 14 adantr coeff P N 0 P = 0 𝑝 ¬ coeff P N = 0
16 15 3ad2antl3 P Poly N 0 coeff P N 0 P = 0 𝑝 ¬ coeff P N = 0
17 13 16 pm2.65da P Poly N 0 coeff P N 0 ¬ P = 0 𝑝
18 17 neqned P Poly N 0 coeff P N 0 P 0 𝑝