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

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