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 syl6eq 
 |-  ( 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 syl6eq 
 |-  ( 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 syl6eq 
 |-  ( 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 syl5eqr 
 |-  ( ( 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 ) )