Metamath Proof Explorer

Theorem dgreq0

Description: The leading coefficient of a polynomial is nonzero, unless the entire polynomial is zero. (Contributed by Mario Carneiro, 22-Jul-2014) (Proof shortened by Fan Zheng, 21-Jun-2016)

Ref Expression
Hypotheses dgreq0.1 ⊢ 𝑁 = ( deg ‘ 𝐹 )
dgreq0.2 ⊢ 𝐴 = ( coeff ‘ 𝐹 )
Assertion dgreq0 ( 𝐹 ∈ ( Poly ‘ 𝑆 ) → ( 𝐹 = 0𝑝 ↔ ( 𝐴 ‘ 𝑁 ) = 0 ) )

Proof

Step Hyp Ref Expression
1 dgreq0.1 ⊢ 𝑁 = ( deg ‘ 𝐹 )
2 dgreq0.2 ⊢ 𝐴 = ( coeff ‘ 𝐹 )
3 fveq2 ⊢ ( 𝐹 = 0𝑝 → ( coeff ‘ 𝐹 ) = ( coeff ‘ 0𝑝 ) )
4 2 3 eqtrid ⊢ ( 𝐹 = 0𝑝 → 𝐴 = ( coeff ‘ 0𝑝 ) )
5 coe0 ⊢ ( coeff ‘ 0𝑝 ) = ( ℕ0 × { 0 } )
6 4 5 eqtrdi ⊢ ( 𝐹 = 0𝑝 → 𝐴 = ( ℕ0 × { 0 } ) )
7 fveq2 ⊢ ( 𝐹 = 0𝑝 → ( deg ‘ 𝐹 ) = ( deg ‘ 0𝑝 ) )
8 1 7 eqtrid ⊢ ( 𝐹 = 0𝑝 → 𝑁 = ( deg ‘ 0𝑝 ) )
9 dgr0 ⊢ ( deg ‘ 0𝑝 ) = 0
10 8 9 eqtrdi ⊢ ( 𝐹 = 0𝑝 → 𝑁 = 0 )
11 6 10 fveq12d ⊢ ( 𝐹 = 0𝑝 → ( 𝐴 ‘ 𝑁 ) = ( ( ℕ0 × { 0 } ) ‘ 0 ) )
12 0nn0 ⊢ 0 ∈ ℕ0
13 fvconst2g ⊢ ( ( 0 ∈ ℕ0 ∧ 0 ∈ ℕ0 ) → ( ( ℕ0 × { 0 } ) ‘ 0 ) = 0 )
14 12 12 13 mp2an ⊢ ( ( ℕ0 × { 0 } ) ‘ 0 ) = 0
15 11 14 eqtrdi ⊢ ( 𝐹 = 0𝑝 → ( 𝐴 ‘ 𝑁 ) = 0 )
16 2 coefv0 ⊢ ( 𝐹 ∈ ( Poly ‘ 𝑆 ) → ( 𝐹 ‘ 0 ) = ( 𝐴 ‘ 0 ) )
17 16 adantr ⊢ ( ( 𝐹 ∈ ( Poly ‘ 𝑆 ) ∧ ( 𝐴 ‘ 𝑁 ) = 0 ) → ( 𝐹 ‘ 0 ) = ( 𝐴 ‘ 0 ) )
18 simpr ⊢ ( ( ( 𝐹 ∈ ( Poly ‘ 𝑆 ) ∧ ( 𝐴 ‘ 𝑁 ) = 0 ) ∧ 𝑁 ∈ ℕ ) → 𝑁 ∈ ℕ )
19 18 nnred ⊢ ( ( ( 𝐹 ∈ ( Poly ‘ 𝑆 ) ∧ ( 𝐴 ‘ 𝑁 ) = 0 ) ∧ 𝑁 ∈ ℕ ) → 𝑁 ∈ ℝ )
20 19 ltm1d ⊢ ( ( ( 𝐹 ∈ ( Poly ‘ 𝑆 ) ∧ ( 𝐴 ‘ 𝑁 ) = 0 ) ∧ 𝑁 ∈ ℕ ) → ( 𝑁 − 1 ) < 𝑁 )
21 nnre ⊢ ( 𝑁 ∈ ℕ → 𝑁 ∈ ℝ )
22 21 adantl ⊢ ( ( ( 𝐹 ∈ ( Poly ‘ 𝑆 ) ∧ ( 𝐴 ‘ 𝑁 ) = 0 ) ∧ 𝑁 ∈ ℕ ) → 𝑁 ∈ ℝ )
23 peano2rem ⊢ ( 𝑁 ∈ ℝ → ( 𝑁 − 1 ) ∈ ℝ )
24 22 23 syl ⊢ ( ( ( 𝐹 ∈ ( Poly ‘ 𝑆 ) ∧ ( 𝐴 ‘ 𝑁 ) = 0 ) ∧ 𝑁 ∈ ℕ ) → ( 𝑁 − 1 ) ∈ ℝ )
25 simpll ⊢ ( ( ( 𝐹 ∈ ( Poly ‘ 𝑆 ) ∧ ( 𝐴 ‘ 𝑁 ) = 0 ) ∧ 𝑁 ∈ ℕ ) → 𝐹 ∈ ( Poly ‘ 𝑆 ) )
26 nnm1nn0 ⊢ ( 𝑁 ∈ ℕ → ( 𝑁 − 1 ) ∈ ℕ0 )
27 26 adantl ⊢ ( ( ( 𝐹 ∈ ( Poly ‘ 𝑆 ) ∧ ( 𝐴 ‘ 𝑁 ) = 0 ) ∧ 𝑁 ∈ ℕ ) → ( 𝑁 − 1 ) ∈ ℕ0 )
28 2 1 dgrub ⊢ ( ( 𝐹 ∈ ( Poly ‘ 𝑆 ) ∧ 𝑘 ∈ ℕ0 ∧ ( 𝐴 ‘ 𝑘 ) ≠ 0 ) → 𝑘 ≤ 𝑁 )
29 28 3expia ⊢ ( ( 𝐹 ∈ ( Poly ‘ 𝑆 ) ∧ 𝑘 ∈ ℕ0 ) → ( ( 𝐴 ‘ 𝑘 ) ≠ 0 → 𝑘 ≤ 𝑁 ) )
30 29 ad2ant2rl ⊢ ( ( ( 𝐹 ∈ ( Poly ‘ 𝑆 ) ∧ ( 𝐴 ‘ 𝑁 ) = 0 ) ∧ ( 𝑁 ∈ ℕ ∧ 𝑘 ∈ ℕ0 ) ) → ( ( 𝐴 ‘ 𝑘 ) ≠ 0 → 𝑘 ≤ 𝑁 ) )
31 simplr ⊢ ( ( ( 𝐹 ∈ ( Poly ‘ 𝑆 ) ∧ ( 𝐴 ‘ 𝑁 ) = 0 ) ∧ ( 𝑁 ∈ ℕ ∧ 𝑘 ∈ ℕ0 ) ) → ( 𝐴 ‘ 𝑁 ) = 0 )
32 fveqeq2 ⊢ ( 𝑁 = 𝑘 → ( ( 𝐴 ‘ 𝑁 ) = 0 ↔ ( 𝐴 ‘ 𝑘 ) = 0 ) )
33 31 32 syl5ibcom ⊢ ( ( ( 𝐹 ∈ ( Poly ‘ 𝑆 ) ∧ ( 𝐴 ‘ 𝑁 ) = 0 ) ∧ ( 𝑁 ∈ ℕ ∧ 𝑘 ∈ ℕ0 ) ) → ( 𝑁 = 𝑘 → ( 𝐴 ‘ 𝑘 ) = 0 ) )
34 33 necon3d ⊢ ( ( ( 𝐹 ∈ ( Poly ‘ 𝑆 ) ∧ ( 𝐴 ‘ 𝑁 ) = 0 ) ∧ ( 𝑁 ∈ ℕ ∧ 𝑘 ∈ ℕ0 ) ) → ( ( 𝐴 ‘ 𝑘 ) ≠ 0 → 𝑁 ≠ 𝑘 ) )
35 30 34 jcad ⊢ ( ( ( 𝐹 ∈ ( Poly ‘ 𝑆 ) ∧ ( 𝐴 ‘ 𝑁 ) = 0 ) ∧ ( 𝑁 ∈ ℕ ∧ 𝑘 ∈ ℕ0 ) ) → ( ( 𝐴 ‘ 𝑘 ) ≠ 0 → ( 𝑘 ≤ 𝑁 ∧ 𝑁 ≠ 𝑘 ) ) )
36 nn0re ⊢ ( 𝑘 ∈ ℕ0 → 𝑘 ∈ ℝ )
37 36 ad2antll ⊢ ( ( ( 𝐹 ∈ ( Poly ‘ 𝑆 ) ∧ ( 𝐴 ‘ 𝑁 ) = 0 ) ∧ ( 𝑁 ∈ ℕ ∧ 𝑘 ∈ ℕ0 ) ) → 𝑘 ∈ ℝ )
38 21 ad2antrl ⊢ ( ( ( 𝐹 ∈ ( Poly ‘ 𝑆 ) ∧ ( 𝐴 ‘ 𝑁 ) = 0 ) ∧ ( 𝑁 ∈ ℕ ∧ 𝑘 ∈ ℕ0 ) ) → 𝑁 ∈ ℝ )
39 37 38 ltlend ⊢ ( ( ( 𝐹 ∈ ( Poly ‘ 𝑆 ) ∧ ( 𝐴 ‘ 𝑁 ) = 0 ) ∧ ( 𝑁 ∈ ℕ ∧ 𝑘 ∈ ℕ0 ) ) → ( 𝑘 < 𝑁 ↔ ( 𝑘 ≤ 𝑁 ∧ 𝑁 ≠ 𝑘 ) ) )
40 nn0z ⊢ ( 𝑘 ∈ ℕ0 → 𝑘 ∈ ℤ )
41 40 ad2antll ⊢ ( ( ( 𝐹 ∈ ( Poly ‘ 𝑆 ) ∧ ( 𝐴 ‘ 𝑁 ) = 0 ) ∧ ( 𝑁 ∈ ℕ ∧ 𝑘 ∈ ℕ0 ) ) → 𝑘 ∈ ℤ )
42 nnz ⊢ ( 𝑁 ∈ ℕ → 𝑁 ∈ ℤ )
43 42 ad2antrl ⊢ ( ( ( 𝐹 ∈ ( Poly ‘ 𝑆 ) ∧ ( 𝐴 ‘ 𝑁 ) = 0 ) ∧ ( 𝑁 ∈ ℕ ∧ 𝑘 ∈ ℕ0 ) ) → 𝑁 ∈ ℤ )
44 zltlem1 ⊢ ( ( 𝑘 ∈ ℤ ∧ 𝑁 ∈ ℤ ) → ( 𝑘 < 𝑁 ↔ 𝑘 ≤ ( 𝑁 − 1 ) ) )
45 41 43 44 syl2anc ⊢ ( ( ( 𝐹 ∈ ( Poly ‘ 𝑆 ) ∧ ( 𝐴 ‘ 𝑁 ) = 0 ) ∧ ( 𝑁 ∈ ℕ ∧ 𝑘 ∈ ℕ0 ) ) → ( 𝑘 < 𝑁 ↔ 𝑘 ≤ ( 𝑁 − 1 ) ) )
46 39 45 bitr3d ⊢ ( ( ( 𝐹 ∈ ( Poly ‘ 𝑆 ) ∧ ( 𝐴 ‘ 𝑁 ) = 0 ) ∧ ( 𝑁 ∈ ℕ ∧ 𝑘 ∈ ℕ0 ) ) → ( ( 𝑘 ≤ 𝑁 ∧ 𝑁 ≠ 𝑘 ) ↔ 𝑘 ≤ ( 𝑁 − 1 ) ) )
47 35 46 sylibd ⊢ ( ( ( 𝐹 ∈ ( Poly ‘ 𝑆 ) ∧ ( 𝐴 ‘ 𝑁 ) = 0 ) ∧ ( 𝑁 ∈ ℕ ∧ 𝑘 ∈ ℕ0 ) ) → ( ( 𝐴 ‘ 𝑘 ) ≠ 0 → 𝑘 ≤ ( 𝑁 − 1 ) ) )
48 47 expr ⊢ ( ( ( 𝐹 ∈ ( Poly ‘ 𝑆 ) ∧ ( 𝐴 ‘ 𝑁 ) = 0 ) ∧ 𝑁 ∈ ℕ ) → ( 𝑘 ∈ ℕ0 → ( ( 𝐴 ‘ 𝑘 ) ≠ 0 → 𝑘 ≤ ( 𝑁 − 1 ) ) ) )
49 48 ralrimiv ⊢ ( ( ( 𝐹 ∈ ( Poly ‘ 𝑆 ) ∧ ( 𝐴 ‘ 𝑁 ) = 0 ) ∧ 𝑁 ∈ ℕ ) → ∀ 𝑘 ∈ ℕ0 ( ( 𝐴 ‘ 𝑘 ) ≠ 0 → 𝑘 ≤ ( 𝑁 − 1 ) ) )
50 2 coef3 ⊢ ( 𝐹 ∈ ( Poly ‘ 𝑆 ) → 𝐴 : ℕ0 ⟶ ℂ )
51 50 ad2antrr ⊢ ( ( ( 𝐹 ∈ ( Poly ‘ 𝑆 ) ∧ ( 𝐴 ‘ 𝑁 ) = 0 ) ∧ 𝑁 ∈ ℕ ) → 𝐴 : ℕ0 ⟶ ℂ )
52 plyco0 ⊢ ( ( ( 𝑁 − 1 ) ∈ ℕ0 ∧ 𝐴 : ℕ0 ⟶ ℂ ) → ( ( 𝐴 “ ( ℤ≥ ‘ ( ( 𝑁 − 1 ) + 1 ) ) ) = { 0 } ↔ ∀ 𝑘 ∈ ℕ0 ( ( 𝐴 ‘ 𝑘 ) ≠ 0 → 𝑘 ≤ ( 𝑁 − 1 ) ) ) )
53 27 51 52 syl2anc ⊢ ( ( ( 𝐹 ∈ ( Poly ‘ 𝑆 ) ∧ ( 𝐴 ‘ 𝑁 ) = 0 ) ∧ 𝑁 ∈ ℕ ) → ( ( 𝐴 “ ( ℤ≥ ‘ ( ( 𝑁 − 1 ) + 1 ) ) ) = { 0 } ↔ ∀ 𝑘 ∈ ℕ0 ( ( 𝐴 ‘ 𝑘 ) ≠ 0 → 𝑘 ≤ ( 𝑁 − 1 ) ) ) )
54 49 53 mpbird ⊢ ( ( ( 𝐹 ∈ ( Poly ‘ 𝑆 ) ∧ ( 𝐴 ‘ 𝑁 ) = 0 ) ∧ 𝑁 ∈ ℕ ) → ( 𝐴 “ ( ℤ≥ ‘ ( ( 𝑁 − 1 ) + 1 ) ) ) = { 0 } )
55 2 1 dgrlb ⊢ ( ( 𝐹 ∈ ( Poly ‘ 𝑆 ) ∧ ( 𝑁 − 1 ) ∈ ℕ0 ∧ ( 𝐴 “ ( ℤ≥ ‘ ( ( 𝑁 − 1 ) + 1 ) ) ) = { 0 } ) → 𝑁 ≤ ( 𝑁 − 1 ) )
56 25 27 54 55 syl3anc ⊢ ( ( ( 𝐹 ∈ ( Poly ‘ 𝑆 ) ∧ ( 𝐴 ‘ 𝑁 ) = 0 ) ∧ 𝑁 ∈ ℕ ) → 𝑁 ≤ ( 𝑁 − 1 ) )
57 22 24 56 lensymd ⊢ ( ( ( 𝐹 ∈ ( Poly ‘ 𝑆 ) ∧ ( 𝐴 ‘ 𝑁 ) = 0 ) ∧ 𝑁 ∈ ℕ ) → ¬ ( 𝑁 − 1 ) < 𝑁 )
58 20 57 pm2.65da ⊢ ( ( 𝐹 ∈ ( Poly ‘ 𝑆 ) ∧ ( 𝐴 ‘ 𝑁 ) = 0 ) → ¬ 𝑁 ∈ ℕ )
59 dgrcl ⊢ ( 𝐹 ∈ ( Poly ‘ 𝑆 ) → ( deg ‘ 𝐹 ) ∈ ℕ0 )
60 1 59 eqeltrid ⊢ ( 𝐹 ∈ ( Poly ‘ 𝑆 ) → 𝑁 ∈ ℕ0 )
61 60 adantr ⊢ ( ( 𝐹 ∈ ( Poly ‘ 𝑆 ) ∧ ( 𝐴 ‘ 𝑁 ) = 0 ) → 𝑁 ∈ ℕ0 )
62 elnn0 ⊢ ( 𝑁 ∈ ℕ0 ↔ ( 𝑁 ∈ ℕ ∨ 𝑁 = 0 ) )
63 61 62 sylib ⊢ ( ( 𝐹 ∈ ( Poly ‘ 𝑆 ) ∧ ( 𝐴 ‘ 𝑁 ) = 0 ) → ( 𝑁 ∈ ℕ ∨ 𝑁 = 0 ) )
64 63 ord ⊢ ( ( 𝐹 ∈ ( Poly ‘ 𝑆 ) ∧ ( 𝐴 ‘ 𝑁 ) = 0 ) → ( ¬ 𝑁 ∈ ℕ → 𝑁 = 0 ) )
65 58 64 mpd ⊢ ( ( 𝐹 ∈ ( Poly ‘ 𝑆 ) ∧ ( 𝐴 ‘ 𝑁 ) = 0 ) → 𝑁 = 0 )
66 65 fveq2d ⊢ ( ( 𝐹 ∈ ( Poly ‘ 𝑆 ) ∧ ( 𝐴 ‘ 𝑁 ) = 0 ) → ( 𝐴 ‘ 𝑁 ) = ( 𝐴 ‘ 0 ) )
67 simpr ⊢ ( ( 𝐹 ∈ ( Poly ‘ 𝑆 ) ∧ ( 𝐴 ‘ 𝑁 ) = 0 ) → ( 𝐴 ‘ 𝑁 ) = 0 )
68 17 66 67 3eqtr2d ⊢ ( ( 𝐹 ∈ ( Poly ‘ 𝑆 ) ∧ ( 𝐴 ‘ 𝑁 ) = 0 ) → ( 𝐹 ‘ 0 ) = 0 )
69 68 sneqd ⊢ ( ( 𝐹 ∈ ( Poly ‘ 𝑆 ) ∧ ( 𝐴 ‘ 𝑁 ) = 0 ) → { ( 𝐹 ‘ 0 ) } = { 0 } )
70 69 xpeq2d ⊢ ( ( 𝐹 ∈ ( Poly ‘ 𝑆 ) ∧ ( 𝐴 ‘ 𝑁 ) = 0 ) → ( ℂ × { ( 𝐹 ‘ 0 ) } ) = ( ℂ × { 0 } ) )
71 1 65 eqtr3id ⊢ ( ( 𝐹 ∈ ( Poly ‘ 𝑆 ) ∧ ( 𝐴 ‘ 𝑁 ) = 0 ) → ( deg ‘ 𝐹 ) = 0 )
72 0dgrb ⊢ ( 𝐹 ∈ ( Poly ‘ 𝑆 ) → ( ( deg ‘ 𝐹 ) = 0 ↔ 𝐹 = ( ℂ × { ( 𝐹 ‘ 0 ) } ) ) )
73 72 adantr ⊢ ( ( 𝐹 ∈ ( Poly ‘ 𝑆 ) ∧ ( 𝐴 ‘ 𝑁 ) = 0 ) → ( ( deg ‘ 𝐹 ) = 0 ↔ 𝐹 = ( ℂ × { ( 𝐹 ‘ 0 ) } ) ) )
74 71 73 mpbid ⊢ ( ( 𝐹 ∈ ( Poly ‘ 𝑆 ) ∧ ( 𝐴 ‘ 𝑁 ) = 0 ) → 𝐹 = ( ℂ × { ( 𝐹 ‘ 0 ) } ) )
75 df-0p ⊢ 0𝑝 = ( ℂ × { 0 } )
76 75 a1i ⊢ ( ( 𝐹 ∈ ( Poly ‘ 𝑆 ) ∧ ( 𝐴 ‘ 𝑁 ) = 0 ) → 0𝑝 = ( ℂ × { 0 } ) )
77 70 74 76 3eqtr4d ⊢ ( ( 𝐹 ∈ ( Poly ‘ 𝑆 ) ∧ ( 𝐴 ‘ 𝑁 ) = 0 ) → 𝐹 = 0𝑝 )
78 77 ex ⊢ ( 𝐹 ∈ ( Poly ‘ 𝑆 ) → ( ( 𝐴 ‘ 𝑁 ) = 0 → 𝐹 = 0𝑝 ) )
79 15 78 impbid2 ⊢ ( 𝐹 ∈ ( Poly ‘ 𝑆 ) → ( 𝐹 = 0𝑝 ↔ ( 𝐴 ‘ 𝑁 ) = 0 ) )