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		ffvelcdm	\|- ( ( 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 )

Metamath Proof Explorer

Theorem dgreq

Proof