This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 ffvelcdm ⊢ ( ( 𝐴 : ℕ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 ‘ 𝐹 ) = 𝑁 )