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 ( 𝜑𝐹 ∈ ( 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 ‘ 𝐹 ) = 𝑁 )