dgrle

Description: Given an explicit expression for a polynomial, the degree is at most the highest term in the sum. (Contributed by Mario Carneiro, 24-Jul-2014)

	Ref	Expression
Hypotheses	dgrle.1	\|- ( ph -> F e. ( Poly ` S ) )
	dgrle.2	\|- ( ph -> N e. NN0 )
	dgrle.3	\|- ( ( ph /\ k e. ( 0 ... N ) ) -> A e. CC )
	dgrle.4	\|- ( ph -> F = ( z e. CC \|-> sum_ k e. ( 0 ... N ) ( A x. ( z ^ k ) ) ) )
Assertion	dgrle	\|- ( ph -> ( deg ` F ) <_ N )

Proof

Step	Hyp	Ref	Expression
1		dgrle.1	\|- ( ph -> F e. ( Poly ` S ) )
2		dgrle.2	\|- ( ph -> N e. NN0 )
3		dgrle.3	\|- ( ( ph /\ k e. ( 0 ... N ) ) -> A e. CC )
4		dgrle.4	\|- ( ph -> F = ( z e. CC \|-> sum_ k e. ( 0 ... N ) ( A x. ( z ^ k ) ) ) )
5	1 2 3 4	coeeq2	\|- ( ph -> ( coeff ` F ) = ( k e. NN0 \|-> if ( k <_ N , A , 0 ) ) )
6	5	ad2antrr	\|- ( ( ( ph /\ m e. NN0 ) /\ -. m <_ N ) -> ( coeff ` F ) = ( k e. NN0 \|-> if ( k <_ N , A , 0 ) ) )
7	6	fveq1d	\|- ( ( ( ph /\ m e. NN0 ) /\ -. m <_ N ) -> ( ( coeff ` F ) ` m ) = ( ( k e. NN0 \|-> if ( k <_ N , A , 0 ) ) ` m ) )
8		nfcv	\|- F/_ k m
9		nfv	\|- F/ k -. m <_ N
10		nffvmpt1	\|- F/_ k ( ( k e. NN0 \|-> if ( k <_ N , A , 0 ) ) ` m )
11	10	nfeq1	\|- F/ k ( ( k e. NN0 \|-> if ( k <_ N , A , 0 ) ) ` m ) = 0
12	9 11	nfim	\|- F/ k ( -. m <_ N -> ( ( k e. NN0 \|-> if ( k <_ N , A , 0 ) ) ` m ) = 0 )
13		breq1	\|- ( k = m -> ( k <_ N <-> m <_ N ) )
14	13	notbid	\|- ( k = m -> ( -. k <_ N <-> -. m <_ N ) )
15		fveqeq2	\|- ( k = m -> ( ( ( k e. NN0 \|-> if ( k <_ N , A , 0 ) ) ` k ) = 0 <-> ( ( k e. NN0 \|-> if ( k <_ N , A , 0 ) ) ` m ) = 0 ) )
16	14 15	imbi12d	\|- ( k = m -> ( ( -. k <_ N -> ( ( k e. NN0 \|-> if ( k <_ N , A , 0 ) ) ` k ) = 0 ) <-> ( -. m <_ N -> ( ( k e. NN0 \|-> if ( k <_ N , A , 0 ) ) ` m ) = 0 ) ) )
17		iffalse	\|- ( -. k <_ N -> if ( k <_ N , A , 0 ) = 0 )
18	17	fveq2d	\|- ( -. k <_ N -> ( _I ` if ( k <_ N , A , 0 ) ) = ( _I ` 0 ) )
19		0cn	\|- 0 e. CC
20		fvi	\|- ( 0 e. CC -> ( _I ` 0 ) = 0 )
21	19 20	ax-mp	\|- ( _I ` 0 ) = 0
22	18 21	eqtrdi	\|- ( -. k <_ N -> ( _I ` if ( k <_ N , A , 0 ) ) = 0 )
23		eqid	\|- ( k e. NN0 \|-> if ( k <_ N , A , 0 ) ) = ( k e. NN0 \|-> if ( k <_ N , A , 0 ) )
24	23	fvmpt2i	\|- ( k e. NN0 -> ( ( k e. NN0 \|-> if ( k <_ N , A , 0 ) ) ` k ) = ( _I ` if ( k <_ N , A , 0 ) ) )
25	24	eqeq1d	\|- ( k e. NN0 -> ( ( ( k e. NN0 \|-> if ( k <_ N , A , 0 ) ) ` k ) = 0 <-> ( _I ` if ( k <_ N , A , 0 ) ) = 0 ) )
26	22 25	imbitrrid	\|- ( k e. NN0 -> ( -. k <_ N -> ( ( k e. NN0 \|-> if ( k <_ N , A , 0 ) ) ` k ) = 0 ) )
27	8 12 16 26	vtoclgaf	\|- ( m e. NN0 -> ( -. m <_ N -> ( ( k e. NN0 \|-> if ( k <_ N , A , 0 ) ) ` m ) = 0 ) )
28	27	imp	\|- ( ( m e. NN0 /\ -. m <_ N ) -> ( ( k e. NN0 \|-> if ( k <_ N , A , 0 ) ) ` m ) = 0 )
29	28	adantll	\|- ( ( ( ph /\ m e. NN0 ) /\ -. m <_ N ) -> ( ( k e. NN0 \|-> if ( k <_ N , A , 0 ) ) ` m ) = 0 )
30	7 29	eqtrd	\|- ( ( ( ph /\ m e. NN0 ) /\ -. m <_ N ) -> ( ( coeff ` F ) ` m ) = 0 )
31	30	ex	\|- ( ( ph /\ m e. NN0 ) -> ( -. m <_ N -> ( ( coeff ` F ) ` m ) = 0 ) )
32	31	necon1ad	\|- ( ( ph /\ m e. NN0 ) -> ( ( ( coeff ` F ) ` m ) =/= 0 -> m <_ N ) )
33	32	ralrimiva	\|- ( ph -> A. m e. NN0 ( ( ( coeff ` F ) ` m ) =/= 0 -> m <_ N ) )
34		eqid	\|- ( coeff ` F ) = ( coeff ` F )
35	34	coef3	\|- ( F e. ( Poly ` S ) -> ( coeff ` F ) : NN0 --> CC )
36	1 35	syl	\|- ( ph -> ( coeff ` F ) : NN0 --> CC )
37		plyco0	\|- ( ( N e. NN0 /\ ( coeff ` F ) : NN0 --> CC ) -> ( ( ( coeff ` F ) " ( ZZ>= ` ( N + 1 ) ) ) = { 0 } <-> A. m e. NN0 ( ( ( coeff ` F ) ` m ) =/= 0 -> m <_ N ) ) )
38	2 36 37	syl2anc	\|- ( ph -> ( ( ( coeff ` F ) " ( ZZ>= ` ( N + 1 ) ) ) = { 0 } <-> A. m e. NN0 ( ( ( coeff ` F ) ` m ) =/= 0 -> m <_ N ) ) )
39	33 38	mpbird	\|- ( ph -> ( ( coeff ` F ) " ( ZZ>= ` ( N + 1 ) ) ) = { 0 } )
40		eqid	\|- ( deg ` F ) = ( deg ` F )
41	34 40	dgrlb	\|- ( ( F e. ( Poly ` S ) /\ N e. NN0 /\ ( ( coeff ` F ) " ( ZZ>= ` ( N + 1 ) ) ) = { 0 } ) -> ( deg ` F ) <_ N )
42	1 2 39 41	syl3anc	\|- ( ph -> ( deg ` F ) <_ N )

Metamath Proof Explorer

Theorem dgrle

Proof