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

Metamath Proof Explorer

Theorem dgrcl

Description: The degree of any polynomial is a nonnegative integer. (Contributed by Mario Carneiro, 22-Jul-2014)

Ref Expression
Assertion dgrcl ( 𝐹 ∈ ( Poly ‘ 𝑆 ) → ( deg ‘ 𝐹 ) ∈ ℕ0 )

Proof

Step Hyp Ref Expression
1 eqid ⊢ ( coeff ‘ 𝐹 ) = ( coeff ‘ 𝐹 )
2 1 dgrval ⊢ ( 𝐹 ∈ ( Poly ‘ 𝑆 ) → ( deg ‘ 𝐹 ) = sup ( ( ◡ ( coeff ‘ 𝐹 ) “ ( ℂ ∖ { 0 } ) ) , ℕ0 , < ) )
3 nn0ssre ⊢ ℕ0 ⊆ ℝ
4 ltso ⊢ < Or ℝ
5 soss ⊢ ( ℕ0 ⊆ ℝ → ( < Or ℝ → < Or ℕ0 ) )
6 3 4 5 mp2 ⊢ < Or ℕ0
7 6 a1i ⊢ ( 𝐹 ∈ ( Poly ‘ 𝑆 ) → < Or ℕ0 )
8 0zd ⊢ ( 𝐹 ∈ ( Poly ‘ 𝑆 ) → 0 ∈ ℤ )
9 cnvimass ⊢ ( ◡ ( coeff ‘ 𝐹 ) “ ( ℂ ∖ { 0 } ) ) ⊆ dom ( coeff ‘ 𝐹 )
10 1 coef ⊢ ( 𝐹 ∈ ( Poly ‘ 𝑆 ) → ( coeff ‘ 𝐹 ) : ℕ0 ⟶ ( 𝑆 ∪ { 0 } ) )
11 9 10 fssdm ⊢ ( 𝐹 ∈ ( Poly ‘ 𝑆 ) → ( ◡ ( coeff ‘ 𝐹 ) “ ( ℂ ∖ { 0 } ) ) ⊆ ℕ0 )
12 1 dgrlem ⊢ ( 𝐹 ∈ ( Poly ‘ 𝑆 ) → ( ( coeff ‘ 𝐹 ) : ℕ0 ⟶ ( 𝑆 ∪ { 0 } ) ∧ ∃ 𝑛 ∈ ℤ ∀ 𝑥 ∈ ( ◡ ( coeff ‘ 𝐹 ) “ ( ℂ ∖ { 0 } ) ) 𝑥 ≤ 𝑛 ) )
13 12 simprd ⊢ ( 𝐹 ∈ ( Poly ‘ 𝑆 ) → ∃ 𝑛 ∈ ℤ ∀ 𝑥 ∈ ( ◡ ( coeff ‘ 𝐹 ) “ ( ℂ ∖ { 0 } ) ) 𝑥 ≤ 𝑛 )
14 nn0uz ⊢ ℕ0 = ( ℤ≥ ‘ 0 )
15 14 uzsupss ⊢ ( ( 0 ∈ ℤ ∧ ( ◡ ( coeff ‘ 𝐹 ) “ ( ℂ ∖ { 0 } ) ) ⊆ ℕ0 ∧ ∃ 𝑛 ∈ ℤ ∀ 𝑥 ∈ ( ◡ ( coeff ‘ 𝐹 ) “ ( ℂ ∖ { 0 } ) ) 𝑥 ≤ 𝑛 ) → ∃ 𝑛 ∈ ℕ0 ( ∀ 𝑥 ∈ ( ◡ ( coeff ‘ 𝐹 ) “ ( ℂ ∖ { 0 } ) ) ¬ 𝑛 < 𝑥 ∧ ∀ 𝑥 ∈ ℕ0 ( 𝑥 < 𝑛 → ∃ 𝑦 ∈ ( ◡ ( coeff ‘ 𝐹 ) “ ( ℂ ∖ { 0 } ) ) 𝑥 < 𝑦 ) ) )
16 8 11 13 15 syl3anc ⊢ ( 𝐹 ∈ ( Poly ‘ 𝑆 ) → ∃ 𝑛 ∈ ℕ0 ( ∀ 𝑥 ∈ ( ◡ ( coeff ‘ 𝐹 ) “ ( ℂ ∖ { 0 } ) ) ¬ 𝑛 < 𝑥 ∧ ∀ 𝑥 ∈ ℕ0 ( 𝑥 < 𝑛 → ∃ 𝑦 ∈ ( ◡ ( coeff ‘ 𝐹 ) “ ( ℂ ∖ { 0 } ) ) 𝑥 < 𝑦 ) ) )
17 7 16 supcl ⊢ ( 𝐹 ∈ ( Poly ‘ 𝑆 ) → sup ( ( ◡ ( coeff ‘ 𝐹 ) “ ( ℂ ∖ { 0 } ) ) , ℕ0 , < ) ∈ ℕ0 )
18 2 17 eqeltrd ⊢ ( 𝐹 ∈ ( Poly ‘ 𝑆 ) → ( deg ‘ 𝐹 ) ∈ ℕ0 )