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 )