Definition df-dgr

Description: Define the degree of a polynomial. (Contributed by Mario Carneiro, 22-Jul-2014)

	Ref	Expression
Assertion	df-dgr	⊢ deg = ( 𝑓 ∈ ( Poly ‘ ℂ ) ↦ sup ( ( ◡ ( coeff ‘ 𝑓 ) “ ( ℂ ∖ { 0 } ) ) , ℕ0 , < ) )

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cdgr	⊢ deg
1		vf	⊢ 𝑓
2		cply	⊢ Poly
3		cc	⊢ ℂ
4	3 2	cfv	⊢ ( Poly ‘ ℂ )
5		ccoe	⊢ coeff
6	1	cv	⊢ 𝑓
7	6 5	cfv	⊢ ( coeff ‘ 𝑓 )
8	7	ccnv	⊢ ◡ ( coeff ‘ 𝑓 )
9		cc0	⊢ 0
10	9	csn	⊢ { 0 }
11	3 10	cdif	⊢ ( ℂ ∖ { 0 } )
12	8 11	cima	⊢ ( ◡ ( coeff ‘ 𝑓 ) “ ( ℂ ∖ { 0 } ) )
13		cn0	⊢ ℕ0
14		clt	⊢ <
15	12 13 14	csup	⊢ sup ( ( ◡ ( coeff ‘ 𝑓 ) “ ( ℂ ∖ { 0 } ) ) , ℕ0 , < )
16	1 4 15	cmpt	⊢ ( 𝑓 ∈ ( Poly ‘ ℂ ) ↦ sup ( ( ◡ ( coeff ‘ 𝑓 ) “ ( ℂ ∖ { 0 } ) ) , ℕ0 , < ) )
17	0 16	wceq	⊢ deg = ( 𝑓 ∈ ( Poly ‘ ℂ ) ↦ sup ( ( ◡ ( coeff ‘ 𝑓 ) “ ( ℂ ∖ { 0 } ) ) , ℕ0 , < ) )