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
|- N = ( deg ` F )
dgreq0.2
|- A = ( coeff ` F )
Assertion dgreq0
|- ( F e. ( Poly ` S ) -> ( F = 0p <-> ( A ` N ) = 0 ) )

Proof

Step Hyp Ref Expression
1 dgreq0.1
 |-  N = ( deg ` F )
2 dgreq0.2
 |-  A = ( coeff ` F )
3 fveq2
 |-  ( F = 0p -> ( coeff ` F ) = ( coeff ` 0p ) )
4 2 3 syl5eq
 |-  ( F = 0p -> A = ( coeff ` 0p ) )
5 coe0
 |-  ( coeff ` 0p ) = ( NN0 X. { 0 } )
6 4 5 eqtrdi
 |-  ( F = 0p -> A = ( NN0 X. { 0 } ) )
7 fveq2
 |-  ( F = 0p -> ( deg ` F ) = ( deg ` 0p ) )
8 1 7 syl5eq
 |-  ( F = 0p -> N = ( deg ` 0p ) )
9 dgr0
 |-  ( deg ` 0p ) = 0
10 8 9 eqtrdi
 |-  ( F = 0p -> N = 0 )
11 6 10 fveq12d
 |-  ( F = 0p -> ( A ` N ) = ( ( NN0 X. { 0 } ) ` 0 ) )
12 0nn0
 |-  0 e. NN0
13 fvconst2g
 |-  ( ( 0 e. NN0 /\ 0 e. NN0 ) -> ( ( NN0 X. { 0 } ) ` 0 ) = 0 )
14 12 12 13 mp2an
 |-  ( ( NN0 X. { 0 } ) ` 0 ) = 0
15 11 14 eqtrdi
 |-  ( F = 0p -> ( A ` N ) = 0 )
16 2 coefv0
 |-  ( F e. ( Poly ` S ) -> ( F ` 0 ) = ( A ` 0 ) )
17 16 adantr
 |-  ( ( F e. ( Poly ` S ) /\ ( A ` N ) = 0 ) -> ( F ` 0 ) = ( A ` 0 ) )
18 simpr
 |-  ( ( ( F e. ( Poly ` S ) /\ ( A ` N ) = 0 ) /\ N e. NN ) -> N e. NN )
19 18 nnred
 |-  ( ( ( F e. ( Poly ` S ) /\ ( A ` N ) = 0 ) /\ N e. NN ) -> N e. RR )
20 19 ltm1d
 |-  ( ( ( F e. ( Poly ` S ) /\ ( A ` N ) = 0 ) /\ N e. NN ) -> ( N - 1 ) < N )
21 nnre
 |-  ( N e. NN -> N e. RR )
22 21 adantl
 |-  ( ( ( F e. ( Poly ` S ) /\ ( A ` N ) = 0 ) /\ N e. NN ) -> N e. RR )
23 peano2rem
 |-  ( N e. RR -> ( N - 1 ) e. RR )
24 22 23 syl
 |-  ( ( ( F e. ( Poly ` S ) /\ ( A ` N ) = 0 ) /\ N e. NN ) -> ( N - 1 ) e. RR )
25 simpll
 |-  ( ( ( F e. ( Poly ` S ) /\ ( A ` N ) = 0 ) /\ N e. NN ) -> F e. ( Poly ` S ) )
26 nnm1nn0
 |-  ( N e. NN -> ( N - 1 ) e. NN0 )
27 26 adantl
 |-  ( ( ( F e. ( Poly ` S ) /\ ( A ` N ) = 0 ) /\ N e. NN ) -> ( N - 1 ) e. NN0 )
28 2 1 dgrub
 |-  ( ( F e. ( Poly ` S ) /\ k e. NN0 /\ ( A ` k ) =/= 0 ) -> k <_ N )
29 28 3expia
 |-  ( ( F e. ( Poly ` S ) /\ k e. NN0 ) -> ( ( A ` k ) =/= 0 -> k <_ N ) )
30 29 ad2ant2rl
 |-  ( ( ( F e. ( Poly ` S ) /\ ( A ` N ) = 0 ) /\ ( N e. NN /\ k e. NN0 ) ) -> ( ( A ` k ) =/= 0 -> k <_ N ) )
31 simplr
 |-  ( ( ( F e. ( Poly ` S ) /\ ( A ` N ) = 0 ) /\ ( N e. NN /\ k e. NN0 ) ) -> ( A ` N ) = 0 )
32 fveqeq2
 |-  ( N = k -> ( ( A ` N ) = 0 <-> ( A ` k ) = 0 ) )
33 31 32 syl5ibcom
 |-  ( ( ( F e. ( Poly ` S ) /\ ( A ` N ) = 0 ) /\ ( N e. NN /\ k e. NN0 ) ) -> ( N = k -> ( A ` k ) = 0 ) )
34 33 necon3d
 |-  ( ( ( F e. ( Poly ` S ) /\ ( A ` N ) = 0 ) /\ ( N e. NN /\ k e. NN0 ) ) -> ( ( A ` k ) =/= 0 -> N =/= k ) )
35 30 34 jcad
 |-  ( ( ( F e. ( Poly ` S ) /\ ( A ` N ) = 0 ) /\ ( N e. NN /\ k e. NN0 ) ) -> ( ( A ` k ) =/= 0 -> ( k <_ N /\ N =/= k ) ) )
36 nn0re
 |-  ( k e. NN0 -> k e. RR )
37 36 ad2antll
 |-  ( ( ( F e. ( Poly ` S ) /\ ( A ` N ) = 0 ) /\ ( N e. NN /\ k e. NN0 ) ) -> k e. RR )
38 21 ad2antrl
 |-  ( ( ( F e. ( Poly ` S ) /\ ( A ` N ) = 0 ) /\ ( N e. NN /\ k e. NN0 ) ) -> N e. RR )
39 37 38 ltlend
 |-  ( ( ( F e. ( Poly ` S ) /\ ( A ` N ) = 0 ) /\ ( N e. NN /\ k e. NN0 ) ) -> ( k < N <-> ( k <_ N /\ N =/= k ) ) )
40 nn0z
 |-  ( k e. NN0 -> k e. ZZ )
41 40 ad2antll
 |-  ( ( ( F e. ( Poly ` S ) /\ ( A ` N ) = 0 ) /\ ( N e. NN /\ k e. NN0 ) ) -> k e. ZZ )
42 nnz
 |-  ( N e. NN -> N e. ZZ )
43 42 ad2antrl
 |-  ( ( ( F e. ( Poly ` S ) /\ ( A ` N ) = 0 ) /\ ( N e. NN /\ k e. NN0 ) ) -> N e. ZZ )
44 zltlem1
 |-  ( ( k e. ZZ /\ N e. ZZ ) -> ( k < N <-> k <_ ( N - 1 ) ) )
45 41 43 44 syl2anc
 |-  ( ( ( F e. ( Poly ` S ) /\ ( A ` N ) = 0 ) /\ ( N e. NN /\ k e. NN0 ) ) -> ( k < N <-> k <_ ( N - 1 ) ) )
46 39 45 bitr3d
 |-  ( ( ( F e. ( Poly ` S ) /\ ( A ` N ) = 0 ) /\ ( N e. NN /\ k e. NN0 ) ) -> ( ( k <_ N /\ N =/= k ) <-> k <_ ( N - 1 ) ) )
47 35 46 sylibd
 |-  ( ( ( F e. ( Poly ` S ) /\ ( A ` N ) = 0 ) /\ ( N e. NN /\ k e. NN0 ) ) -> ( ( A ` k ) =/= 0 -> k <_ ( N - 1 ) ) )
48 47 expr
 |-  ( ( ( F e. ( Poly ` S ) /\ ( A ` N ) = 0 ) /\ N e. NN ) -> ( k e. NN0 -> ( ( A ` k ) =/= 0 -> k <_ ( N - 1 ) ) ) )
49 48 ralrimiv
 |-  ( ( ( F e. ( Poly ` S ) /\ ( A ` N ) = 0 ) /\ N e. NN ) -> A. k e. NN0 ( ( A ` k ) =/= 0 -> k <_ ( N - 1 ) ) )
50 2 coef3
 |-  ( F e. ( Poly ` S ) -> A : NN0 --> CC )
51 50 ad2antrr
 |-  ( ( ( F e. ( Poly ` S ) /\ ( A ` N ) = 0 ) /\ N e. NN ) -> A : NN0 --> CC )
52 plyco0
 |-  ( ( ( N - 1 ) e. NN0 /\ A : NN0 --> CC ) -> ( ( A " ( ZZ>= ` ( ( N - 1 ) + 1 ) ) ) = { 0 } <-> A. k e. NN0 ( ( A ` k ) =/= 0 -> k <_ ( N - 1 ) ) ) )
53 27 51 52 syl2anc
 |-  ( ( ( F e. ( Poly ` S ) /\ ( A ` N ) = 0 ) /\ N e. NN ) -> ( ( A " ( ZZ>= ` ( ( N - 1 ) + 1 ) ) ) = { 0 } <-> A. k e. NN0 ( ( A ` k ) =/= 0 -> k <_ ( N - 1 ) ) ) )
54 49 53 mpbird
 |-  ( ( ( F e. ( Poly ` S ) /\ ( A ` N ) = 0 ) /\ N e. NN ) -> ( A " ( ZZ>= ` ( ( N - 1 ) + 1 ) ) ) = { 0 } )
55 2 1 dgrlb
 |-  ( ( F e. ( Poly ` S ) /\ ( N - 1 ) e. NN0 /\ ( A " ( ZZ>= ` ( ( N - 1 ) + 1 ) ) ) = { 0 } ) -> N <_ ( N - 1 ) )
56 25 27 54 55 syl3anc
 |-  ( ( ( F e. ( Poly ` S ) /\ ( A ` N ) = 0 ) /\ N e. NN ) -> N <_ ( N - 1 ) )
57 22 24 56 lensymd
 |-  ( ( ( F e. ( Poly ` S ) /\ ( A ` N ) = 0 ) /\ N e. NN ) -> -. ( N - 1 ) < N )
58 20 57 pm2.65da
 |-  ( ( F e. ( Poly ` S ) /\ ( A ` N ) = 0 ) -> -. N e. NN )
59 dgrcl
 |-  ( F e. ( Poly ` S ) -> ( deg ` F ) e. NN0 )
60 1 59 eqeltrid
 |-  ( F e. ( Poly ` S ) -> N e. NN0 )
61 60 adantr
 |-  ( ( F e. ( Poly ` S ) /\ ( A ` N ) = 0 ) -> N e. NN0 )
62 elnn0
 |-  ( N e. NN0 <-> ( N e. NN \/ N = 0 ) )
63 61 62 sylib
 |-  ( ( F e. ( Poly ` S ) /\ ( A ` N ) = 0 ) -> ( N e. NN \/ N = 0 ) )
64 63 ord
 |-  ( ( F e. ( Poly ` S ) /\ ( A ` N ) = 0 ) -> ( -. N e. NN -> N = 0 ) )
65 58 64 mpd
 |-  ( ( F e. ( Poly ` S ) /\ ( A ` N ) = 0 ) -> N = 0 )
66 65 fveq2d
 |-  ( ( F e. ( Poly ` S ) /\ ( A ` N ) = 0 ) -> ( A ` N ) = ( A ` 0 ) )
67 simpr
 |-  ( ( F e. ( Poly ` S ) /\ ( A ` N ) = 0 ) -> ( A ` N ) = 0 )
68 17 66 67 3eqtr2d
 |-  ( ( F e. ( Poly ` S ) /\ ( A ` N ) = 0 ) -> ( F ` 0 ) = 0 )
69 68 sneqd
 |-  ( ( F e. ( Poly ` S ) /\ ( A ` N ) = 0 ) -> { ( F ` 0 ) } = { 0 } )
70 69 xpeq2d
 |-  ( ( F e. ( Poly ` S ) /\ ( A ` N ) = 0 ) -> ( CC X. { ( F ` 0 ) } ) = ( CC X. { 0 } ) )
71 1 65 eqtr3id
 |-  ( ( F e. ( Poly ` S ) /\ ( A ` N ) = 0 ) -> ( deg ` F ) = 0 )
72 0dgrb
 |-  ( F e. ( Poly ` S ) -> ( ( deg ` F ) = 0 <-> F = ( CC X. { ( F ` 0 ) } ) ) )
73 72 adantr
 |-  ( ( F e. ( Poly ` S ) /\ ( A ` N ) = 0 ) -> ( ( deg ` F ) = 0 <-> F = ( CC X. { ( F ` 0 ) } ) ) )
74 71 73 mpbid
 |-  ( ( F e. ( Poly ` S ) /\ ( A ` N ) = 0 ) -> F = ( CC X. { ( F ` 0 ) } ) )
75 df-0p
 |-  0p = ( CC X. { 0 } )
76 75 a1i
 |-  ( ( F e. ( Poly ` S ) /\ ( A ` N ) = 0 ) -> 0p = ( CC X. { 0 } ) )
77 70 74 76 3eqtr4d
 |-  ( ( F e. ( Poly ` S ) /\ ( A ` N ) = 0 ) -> F = 0p )
78 77 ex
 |-  ( F e. ( Poly ` S ) -> ( ( A ` N ) = 0 -> F = 0p ) )
79 15 78 impbid2
 |-  ( F e. ( Poly ` S ) -> ( F = 0p <-> ( A ` N ) = 0 ) )