Theorem 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	⊢ ( 𝜑 → 𝐹 ∈ ( Poly ‘ 𝑆 ) )
	dgrle.2	⊢ ( 𝜑 → 𝑁 ∈ ℕ0 )
	dgrle.3	⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 0 ... 𝑁 ) ) → 𝐴 ∈ ℂ )
	dgrle.4	⊢ ( 𝜑 → 𝐹 = ( 𝑧 ∈ ℂ ↦ Σ 𝑘 ∈ ( 0 ... 𝑁 ) ( 𝐴 · ( 𝑧 ↑ 𝑘 ) ) ) )
Assertion	dgrle	⊢ ( 𝜑 → ( deg ‘ 𝐹 ) ≤ 𝑁 )

Proof

Step	Hyp	Ref	Expression
1		dgrle.1	⊢ ( 𝜑 → 𝐹 ∈ ( Poly ‘ 𝑆 ) )
2		dgrle.2	⊢ ( 𝜑 → 𝑁 ∈ ℕ0 )
3		dgrle.3	⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 0 ... 𝑁 ) ) → 𝐴 ∈ ℂ )
4		dgrle.4	⊢ ( 𝜑 → 𝐹 = ( 𝑧 ∈ ℂ ↦ Σ 𝑘 ∈ ( 0 ... 𝑁 ) ( 𝐴 · ( 𝑧 ↑ 𝑘 ) ) ) )
5	1 2 3 4	coeeq2	⊢ ( 𝜑 → ( coeff ‘ 𝐹 ) = ( 𝑘 ∈ ℕ0 ↦ if ( 𝑘 ≤ 𝑁 , 𝐴 , 0 ) ) )
6	5	ad2antrr	⊢ ( ( ( 𝜑 ∧ 𝑚 ∈ ℕ0 ) ∧ ¬ 𝑚 ≤ 𝑁 ) → ( coeff ‘ 𝐹 ) = ( 𝑘 ∈ ℕ0 ↦ if ( 𝑘 ≤ 𝑁 , 𝐴 , 0 ) ) )
7	6	fveq1d	⊢ ( ( ( 𝜑 ∧ 𝑚 ∈ ℕ0 ) ∧ ¬ 𝑚 ≤ 𝑁 ) → ( ( coeff ‘ 𝐹 ) ‘ 𝑚 ) = ( ( 𝑘 ∈ ℕ0 ↦ if ( 𝑘 ≤ 𝑁 , 𝐴 , 0 ) ) ‘ 𝑚 ) )
8		nfcv	⊢ Ⅎ 𝑘 𝑚
9		nfv	⊢ Ⅎ 𝑘 ¬ 𝑚 ≤ 𝑁
10		nffvmpt1	⊢ Ⅎ 𝑘 ( ( 𝑘 ∈ ℕ0 ↦ if ( 𝑘 ≤ 𝑁 , 𝐴 , 0 ) ) ‘ 𝑚 )
11	10	nfeq1	⊢ Ⅎ 𝑘 ( ( 𝑘 ∈ ℕ0 ↦ if ( 𝑘 ≤ 𝑁 , 𝐴 , 0 ) ) ‘ 𝑚 ) = 0
12	9 11	nfim	⊢ Ⅎ 𝑘 ( ¬ 𝑚 ≤ 𝑁 → ( ( 𝑘 ∈ ℕ0 ↦ if ( 𝑘 ≤ 𝑁 , 𝐴 , 0 ) ) ‘ 𝑚 ) = 0 )
13		breq1	⊢ ( 𝑘 = 𝑚 → ( 𝑘 ≤ 𝑁 ↔ 𝑚 ≤ 𝑁 ) )
14	13	notbid	⊢ ( 𝑘 = 𝑚 → ( ¬ 𝑘 ≤ 𝑁 ↔ ¬ 𝑚 ≤ 𝑁 ) )
15		fveqeq2	⊢ ( 𝑘 = 𝑚 → ( ( ( 𝑘 ∈ ℕ0 ↦ if ( 𝑘 ≤ 𝑁 , 𝐴 , 0 ) ) ‘ 𝑘 ) = 0 ↔ ( ( 𝑘 ∈ ℕ0 ↦ if ( 𝑘 ≤ 𝑁 , 𝐴 , 0 ) ) ‘ 𝑚 ) = 0 ) )
16	14 15	imbi12d	⊢ ( 𝑘 = 𝑚 → ( ( ¬ 𝑘 ≤ 𝑁 → ( ( 𝑘 ∈ ℕ0 ↦ if ( 𝑘 ≤ 𝑁 , 𝐴 , 0 ) ) ‘ 𝑘 ) = 0 ) ↔ ( ¬ 𝑚 ≤ 𝑁 → ( ( 𝑘 ∈ ℕ0 ↦ if ( 𝑘 ≤ 𝑁 , 𝐴 , 0 ) ) ‘ 𝑚 ) = 0 ) ) )
17		iffalse	⊢ ( ¬ 𝑘 ≤ 𝑁 → if ( 𝑘 ≤ 𝑁 , 𝐴 , 0 ) = 0 )
18	17	fveq2d	⊢ ( ¬ 𝑘 ≤ 𝑁 → ( I ‘ if ( 𝑘 ≤ 𝑁 , 𝐴 , 0 ) ) = ( I ‘ 0 ) )
19		0cn	⊢ 0 ∈ ℂ
20		fvi	⊢ ( 0 ∈ ℂ → ( I ‘ 0 ) = 0 )
21	19 20	ax-mp	⊢ ( I ‘ 0 ) = 0
22	18 21	eqtrdi	⊢ ( ¬ 𝑘 ≤ 𝑁 → ( I ‘ if ( 𝑘 ≤ 𝑁 , 𝐴 , 0 ) ) = 0 )
23		eqid	⊢ ( 𝑘 ∈ ℕ0 ↦ if ( 𝑘 ≤ 𝑁 , 𝐴 , 0 ) ) = ( 𝑘 ∈ ℕ0 ↦ if ( 𝑘 ≤ 𝑁 , 𝐴 , 0 ) )
24	23	fvmpt2i	⊢ ( 𝑘 ∈ ℕ0 → ( ( 𝑘 ∈ ℕ0 ↦ if ( 𝑘 ≤ 𝑁 , 𝐴 , 0 ) ) ‘ 𝑘 ) = ( I ‘ if ( 𝑘 ≤ 𝑁 , 𝐴 , 0 ) ) )
25	24	eqeq1d	⊢ ( 𝑘 ∈ ℕ0 → ( ( ( 𝑘 ∈ ℕ0 ↦ if ( 𝑘 ≤ 𝑁 , 𝐴 , 0 ) ) ‘ 𝑘 ) = 0 ↔ ( I ‘ if ( 𝑘 ≤ 𝑁 , 𝐴 , 0 ) ) = 0 ) )
26	22 25	imbitrrid	⊢ ( 𝑘 ∈ ℕ0 → ( ¬ 𝑘 ≤ 𝑁 → ( ( 𝑘 ∈ ℕ0 ↦ if ( 𝑘 ≤ 𝑁 , 𝐴 , 0 ) ) ‘ 𝑘 ) = 0 ) )
27	8 12 16 26	vtoclgaf	⊢ ( 𝑚 ∈ ℕ0 → ( ¬ 𝑚 ≤ 𝑁 → ( ( 𝑘 ∈ ℕ0 ↦ if ( 𝑘 ≤ 𝑁 , 𝐴 , 0 ) ) ‘ 𝑚 ) = 0 ) )
28	27	imp	⊢ ( ( 𝑚 ∈ ℕ0 ∧ ¬ 𝑚 ≤ 𝑁 ) → ( ( 𝑘 ∈ ℕ0 ↦ if ( 𝑘 ≤ 𝑁 , 𝐴 , 0 ) ) ‘ 𝑚 ) = 0 )
29	28	adantll	⊢ ( ( ( 𝜑 ∧ 𝑚 ∈ ℕ0 ) ∧ ¬ 𝑚 ≤ 𝑁 ) → ( ( 𝑘 ∈ ℕ0 ↦ if ( 𝑘 ≤ 𝑁 , 𝐴 , 0 ) ) ‘ 𝑚 ) = 0 )
30	7 29	eqtrd	⊢ ( ( ( 𝜑 ∧ 𝑚 ∈ ℕ0 ) ∧ ¬ 𝑚 ≤ 𝑁 ) → ( ( coeff ‘ 𝐹 ) ‘ 𝑚 ) = 0 )
31	30	ex	⊢ ( ( 𝜑 ∧ 𝑚 ∈ ℕ0 ) → ( ¬ 𝑚 ≤ 𝑁 → ( ( coeff ‘ 𝐹 ) ‘ 𝑚 ) = 0 ) )
32	31	necon1ad	⊢ ( ( 𝜑 ∧ 𝑚 ∈ ℕ0 ) → ( ( ( coeff ‘ 𝐹 ) ‘ 𝑚 ) ≠ 0 → 𝑚 ≤ 𝑁 ) )
33	32	ralrimiva	⊢ ( 𝜑 → ∀ 𝑚 ∈ ℕ0 ( ( ( coeff ‘ 𝐹 ) ‘ 𝑚 ) ≠ 0 → 𝑚 ≤ 𝑁 ) )
34		eqid	⊢ ( coeff ‘ 𝐹 ) = ( coeff ‘ 𝐹 )
35	34	coef3	⊢ ( 𝐹 ∈ ( Poly ‘ 𝑆 ) → ( coeff ‘ 𝐹 ) : ℕ0 ⟶ ℂ )
36	1 35	syl	⊢ ( 𝜑 → ( coeff ‘ 𝐹 ) : ℕ0 ⟶ ℂ )
37		plyco0	⊢ ( ( 𝑁 ∈ ℕ0 ∧ ( coeff ‘ 𝐹 ) : ℕ0 ⟶ ℂ ) → ( ( ( coeff ‘ 𝐹 ) “ ( ℤ≥ ‘ ( 𝑁 + 1 ) ) ) = { 0 } ↔ ∀ 𝑚 ∈ ℕ0 ( ( ( coeff ‘ 𝐹 ) ‘ 𝑚 ) ≠ 0 → 𝑚 ≤ 𝑁 ) ) )
38	2 36 37	syl2anc	⊢ ( 𝜑 → ( ( ( coeff ‘ 𝐹 ) “ ( ℤ≥ ‘ ( 𝑁 + 1 ) ) ) = { 0 } ↔ ∀ 𝑚 ∈ ℕ0 ( ( ( coeff ‘ 𝐹 ) ‘ 𝑚 ) ≠ 0 → 𝑚 ≤ 𝑁 ) ) )
39	33 38	mpbird	⊢ ( 𝜑 → ( ( coeff ‘ 𝐹 ) “ ( ℤ≥ ‘ ( 𝑁 + 1 ) ) ) = { 0 } )
40		eqid	⊢ ( deg ‘ 𝐹 ) = ( deg ‘ 𝐹 )
41	34 40	dgrlb	⊢ ( ( 𝐹 ∈ ( Poly ‘ 𝑆 ) ∧ 𝑁 ∈ ℕ0 ∧ ( ( coeff ‘ 𝐹 ) “ ( ℤ≥ ‘ ( 𝑁 + 1 ) ) ) = { 0 } ) → ( deg ‘ 𝐹 ) ≤ 𝑁 )
42	1 2 39 41	syl3anc	⊢ ( 𝜑 → ( deg ‘ 𝐹 ) ≤ 𝑁 )