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 )