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	⊢ ( 𝜑 → 𝐹 ∈ ( Poly ‘ 𝑆 ) )
	dgreq.2	⊢ ( 𝜑 → 𝑁 ∈ ℕ0 )
	dgreq.3	⊢ ( 𝜑 → 𝐴 : ℕ0 ⟶ ℂ )
	dgreq.4	⊢ ( 𝜑 → ( 𝐴 “ ( ℤ≥ ‘ ( 𝑁 + 1 ) ) ) = { 0 } )
	dgreq.5	⊢ ( 𝜑 → 𝐹 = ( 𝑧 ∈ ℂ ↦ Σ 𝑘 ∈ ( 0 ... 𝑁 ) ( ( 𝐴 ‘ 𝑘 ) · ( 𝑧 ↑ 𝑘 ) ) ) )
	dgreq.6	⊢ ( 𝜑 → ( 𝐴 ‘ 𝑁 ) ≠ 0 )
Assertion	dgreq	⊢ ( 𝜑 → ( deg ‘ 𝐹 ) = 𝑁 )

Proof

Step	Hyp	Ref	Expression
1		dgreq.1	⊢ ( 𝜑 → 𝐹 ∈ ( Poly ‘ 𝑆 ) )
2		dgreq.2	⊢ ( 𝜑 → 𝑁 ∈ ℕ0 )
3		dgreq.3	⊢ ( 𝜑 → 𝐴 : ℕ0 ⟶ ℂ )
4		dgreq.4	⊢ ( 𝜑 → ( 𝐴 “ ( ℤ≥ ‘ ( 𝑁 + 1 ) ) ) = { 0 } )
5		dgreq.5	⊢ ( 𝜑 → 𝐹 = ( 𝑧 ∈ ℂ ↦ Σ 𝑘 ∈ ( 0 ... 𝑁 ) ( ( 𝐴 ‘ 𝑘 ) · ( 𝑧 ↑ 𝑘 ) ) ) )
6		dgreq.6	⊢ ( 𝜑 → ( 𝐴 ‘ 𝑁 ) ≠ 0 )
7		elfznn0	⊢ ( 𝑘 ∈ ( 0 ... 𝑁 ) → 𝑘 ∈ ℕ0 )
8		ffvelrn	⊢ ( ( 𝐴 : ℕ0 ⟶ ℂ ∧ 𝑘 ∈ ℕ0 ) → ( 𝐴 ‘ 𝑘 ) ∈ ℂ )
9	3 7 8	syl2an	⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 0 ... 𝑁 ) ) → ( 𝐴 ‘ 𝑘 ) ∈ ℂ )
10	1 2 9 5	dgrle	⊢ ( 𝜑 → ( deg ‘ 𝐹 ) ≤ 𝑁 )
11	1 2 3 4 5	coeeq	⊢ ( 𝜑 → ( coeff ‘ 𝐹 ) = 𝐴 )
12	11	fveq1d	⊢ ( 𝜑 → ( ( coeff ‘ 𝐹 ) ‘ 𝑁 ) = ( 𝐴 ‘ 𝑁 ) )
13	12 6	eqnetrd	⊢ ( 𝜑 → ( ( coeff ‘ 𝐹 ) ‘ 𝑁 ) ≠ 0 )
14		eqid	⊢ ( coeff ‘ 𝐹 ) = ( coeff ‘ 𝐹 )
15		eqid	⊢ ( deg ‘ 𝐹 ) = ( deg ‘ 𝐹 )
16	14 15	dgrub	⊢ ( ( 𝐹 ∈ ( Poly ‘ 𝑆 ) ∧ 𝑁 ∈ ℕ0 ∧ ( ( coeff ‘ 𝐹 ) ‘ 𝑁 ) ≠ 0 ) → 𝑁 ≤ ( deg ‘ 𝐹 ) )
17	1 2 13 16	syl3anc	⊢ ( 𝜑 → 𝑁 ≤ ( deg ‘ 𝐹 ) )
18		dgrcl	⊢ ( 𝐹 ∈ ( Poly ‘ 𝑆 ) → ( deg ‘ 𝐹 ) ∈ ℕ0 )
19	1 18	syl	⊢ ( 𝜑 → ( deg ‘ 𝐹 ) ∈ ℕ0 )
20	19	nn0red	⊢ ( 𝜑 → ( deg ‘ 𝐹 ) ∈ ℝ )
21	2	nn0red	⊢ ( 𝜑 → 𝑁 ∈ ℝ )
22	20 21	letri3d	⊢ ( 𝜑 → ( ( deg ‘ 𝐹 ) = 𝑁 ↔ ( ( deg ‘ 𝐹 ) ≤ 𝑁 ∧ 𝑁 ≤ ( deg ‘ 𝐹 ) ) ) )
23	10 17 22	mpbir2and	⊢ ( 𝜑 → ( deg ‘ 𝐹 ) = 𝑁 )