Step |
Hyp |
Ref |
Expression |
1 |
|
dgreq.1 |
⊢ ( 𝜑 → 𝐹 ∈ ( Poly ‘ 𝑆 ) ) |
2 |
|
dgreq.2 |
⊢ ( 𝜑 → 𝑁 ∈ ℕ0 ) |
3 |
|
dgreq.3 |
⊢ ( 𝜑 → 𝐴 : ℕ0 ⟶ ℂ ) |
4 |
|
dgreq.4 |
⊢ ( 𝜑 → ( 𝐴 “ ( ℤ≥ ‘ ( 𝑁 + 1 ) ) ) = { 0 } ) |
5 |
|
dgreq.5 |
⊢ ( 𝜑 → 𝐹 = ( 𝑧 ∈ ℂ ↦ Σ 𝑘 ∈ ( 0 ... 𝑁 ) ( ( 𝐴 ‘ 𝑘 ) · ( 𝑧 ↑ 𝑘 ) ) ) ) |
6 |
|
dgreq.6 |
⊢ ( 𝜑 → ( 𝐴 ‘ 𝑁 ) ≠ 0 ) |
7 |
|
elfznn0 |
⊢ ( 𝑘 ∈ ( 0 ... 𝑁 ) → 𝑘 ∈ ℕ0 ) |
8 |
|
ffvelrn |
⊢ ( ( 𝐴 : ℕ0 ⟶ ℂ ∧ 𝑘 ∈ ℕ0 ) → ( 𝐴 ‘ 𝑘 ) ∈ ℂ ) |
9 |
3 7 8
|
syl2an |
⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 0 ... 𝑁 ) ) → ( 𝐴 ‘ 𝑘 ) ∈ ℂ ) |
10 |
1 2 9 5
|
dgrle |
⊢ ( 𝜑 → ( deg ‘ 𝐹 ) ≤ 𝑁 ) |
11 |
1 2 3 4 5
|
coeeq |
⊢ ( 𝜑 → ( coeff ‘ 𝐹 ) = 𝐴 ) |
12 |
11
|
fveq1d |
⊢ ( 𝜑 → ( ( coeff ‘ 𝐹 ) ‘ 𝑁 ) = ( 𝐴 ‘ 𝑁 ) ) |
13 |
12 6
|
eqnetrd |
⊢ ( 𝜑 → ( ( coeff ‘ 𝐹 ) ‘ 𝑁 ) ≠ 0 ) |
14 |
|
eqid |
⊢ ( coeff ‘ 𝐹 ) = ( coeff ‘ 𝐹 ) |
15 |
|
eqid |
⊢ ( deg ‘ 𝐹 ) = ( deg ‘ 𝐹 ) |
16 |
14 15
|
dgrub |
⊢ ( ( 𝐹 ∈ ( Poly ‘ 𝑆 ) ∧ 𝑁 ∈ ℕ0 ∧ ( ( coeff ‘ 𝐹 ) ‘ 𝑁 ) ≠ 0 ) → 𝑁 ≤ ( deg ‘ 𝐹 ) ) |
17 |
1 2 13 16
|
syl3anc |
⊢ ( 𝜑 → 𝑁 ≤ ( deg ‘ 𝐹 ) ) |
18 |
|
dgrcl |
⊢ ( 𝐹 ∈ ( Poly ‘ 𝑆 ) → ( deg ‘ 𝐹 ) ∈ ℕ0 ) |
19 |
1 18
|
syl |
⊢ ( 𝜑 → ( deg ‘ 𝐹 ) ∈ ℕ0 ) |
20 |
19
|
nn0red |
⊢ ( 𝜑 → ( deg ‘ 𝐹 ) ∈ ℝ ) |
21 |
2
|
nn0red |
⊢ ( 𝜑 → 𝑁 ∈ ℝ ) |
22 |
20 21
|
letri3d |
⊢ ( 𝜑 → ( ( deg ‘ 𝐹 ) = 𝑁 ↔ ( ( deg ‘ 𝐹 ) ≤ 𝑁 ∧ 𝑁 ≤ ( deg ‘ 𝐹 ) ) ) ) |
23 |
10 17 22
|
mpbir2and |
⊢ ( 𝜑 → ( deg ‘ 𝐹 ) = 𝑁 ) |