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