Metamath Proof Explorer


Theorem dgreq

Description: If the highest term in a polynomial expression is nonzero, then the polynomial's degree is completely determined. (Contributed by Mario Carneiro, 24-Jul-2014)

Ref Expression
Hypotheses dgreq.1
|- ( ph -> F e. ( Poly ` S ) )
dgreq.2
|- ( ph -> N e. NN0 )
dgreq.3
|- ( ph -> A : NN0 --> CC )
dgreq.4
|- ( ph -> ( A " ( ZZ>= ` ( N + 1 ) ) ) = { 0 } )
dgreq.5
|- ( ph -> F = ( z e. CC |-> sum_ k e. ( 0 ... N ) ( ( A ` k ) x. ( z ^ k ) ) ) )
dgreq.6
|- ( ph -> ( A ` N ) =/= 0 )
Assertion dgreq
|- ( ph -> ( deg ` F ) = N )

Proof

Step Hyp Ref Expression
1 dgreq.1
 |-  ( ph -> F e. ( Poly ` S ) )
2 dgreq.2
 |-  ( ph -> N e. NN0 )
3 dgreq.3
 |-  ( ph -> A : NN0 --> CC )
4 dgreq.4
 |-  ( ph -> ( A " ( ZZ>= ` ( N + 1 ) ) ) = { 0 } )
5 dgreq.5
 |-  ( ph -> F = ( z e. CC |-> sum_ k e. ( 0 ... N ) ( ( A ` k ) x. ( z ^ k ) ) ) )
6 dgreq.6
 |-  ( ph -> ( A ` N ) =/= 0 )
7 elfznn0
 |-  ( k e. ( 0 ... N ) -> k e. NN0 )
8 ffvelrn
 |-  ( ( A : NN0 --> CC /\ k e. NN0 ) -> ( A ` k ) e. CC )
9 3 7 8 syl2an
 |-  ( ( ph /\ k e. ( 0 ... N ) ) -> ( A ` k ) e. CC )
10 1 2 9 5 dgrle
 |-  ( ph -> ( deg ` F ) <_ N )
11 1 2 3 4 5 coeeq
 |-  ( ph -> ( coeff ` F ) = A )
12 11 fveq1d
 |-  ( ph -> ( ( coeff ` F ) ` N ) = ( A ` N ) )
13 12 6 eqnetrd
 |-  ( ph -> ( ( coeff ` F ) ` N ) =/= 0 )
14 eqid
 |-  ( coeff ` F ) = ( coeff ` F )
15 eqid
 |-  ( deg ` F ) = ( deg ` F )
16 14 15 dgrub
 |-  ( ( F e. ( Poly ` S ) /\ N e. NN0 /\ ( ( coeff ` F ) ` N ) =/= 0 ) -> N <_ ( deg ` F ) )
17 1 2 13 16 syl3anc
 |-  ( ph -> N <_ ( deg ` F ) )
18 dgrcl
 |-  ( F e. ( Poly ` S ) -> ( deg ` F ) e. NN0 )
19 1 18 syl
 |-  ( ph -> ( deg ` F ) e. NN0 )
20 19 nn0red
 |-  ( ph -> ( deg ` F ) e. RR )
21 2 nn0red
 |-  ( ph -> N e. RR )
22 20 21 letri3d
 |-  ( ph -> ( ( deg ` F ) = N <-> ( ( deg ` F ) <_ N /\ N <_ ( deg ` F ) ) ) )
23 10 17 22 mpbir2and
 |-  ( ph -> ( deg ` F ) = N )