Metamath Proof Explorer


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 , < ) )