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 syl5eq ( 𝐹 = 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 syl5eq ( 𝐹 = 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 ) )