Step |
Hyp |
Ref |
Expression |
1 |
|
dgrle.1 |
⊢ ( 𝜑 → 𝐹 ∈ ( Poly ‘ 𝑆 ) ) |
2 |
|
dgrle.2 |
⊢ ( 𝜑 → 𝑁 ∈ ℕ0 ) |
3 |
|
dgrle.3 |
⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 0 ... 𝑁 ) ) → 𝐴 ∈ ℂ ) |
4 |
|
dgrle.4 |
⊢ ( 𝜑 → 𝐹 = ( 𝑧 ∈ ℂ ↦ Σ 𝑘 ∈ ( 0 ... 𝑁 ) ( 𝐴 · ( 𝑧 ↑ 𝑘 ) ) ) ) |
5 |
1 2 3 4
|
coeeq2 |
⊢ ( 𝜑 → ( coeff ‘ 𝐹 ) = ( 𝑘 ∈ ℕ0 ↦ if ( 𝑘 ≤ 𝑁 , 𝐴 , 0 ) ) ) |
6 |
5
|
ad2antrr |
⊢ ( ( ( 𝜑 ∧ 𝑚 ∈ ℕ0 ) ∧ ¬ 𝑚 ≤ 𝑁 ) → ( coeff ‘ 𝐹 ) = ( 𝑘 ∈ ℕ0 ↦ if ( 𝑘 ≤ 𝑁 , 𝐴 , 0 ) ) ) |
7 |
6
|
fveq1d |
⊢ ( ( ( 𝜑 ∧ 𝑚 ∈ ℕ0 ) ∧ ¬ 𝑚 ≤ 𝑁 ) → ( ( coeff ‘ 𝐹 ) ‘ 𝑚 ) = ( ( 𝑘 ∈ ℕ0 ↦ if ( 𝑘 ≤ 𝑁 , 𝐴 , 0 ) ) ‘ 𝑚 ) ) |
8 |
|
nfcv |
⊢ Ⅎ 𝑘 𝑚 |
9 |
|
nfv |
⊢ Ⅎ 𝑘 ¬ 𝑚 ≤ 𝑁 |
10 |
|
nffvmpt1 |
⊢ Ⅎ 𝑘 ( ( 𝑘 ∈ ℕ0 ↦ if ( 𝑘 ≤ 𝑁 , 𝐴 , 0 ) ) ‘ 𝑚 ) |
11 |
10
|
nfeq1 |
⊢ Ⅎ 𝑘 ( ( 𝑘 ∈ ℕ0 ↦ if ( 𝑘 ≤ 𝑁 , 𝐴 , 0 ) ) ‘ 𝑚 ) = 0 |
12 |
9 11
|
nfim |
⊢ Ⅎ 𝑘 ( ¬ 𝑚 ≤ 𝑁 → ( ( 𝑘 ∈ ℕ0 ↦ if ( 𝑘 ≤ 𝑁 , 𝐴 , 0 ) ) ‘ 𝑚 ) = 0 ) |
13 |
|
breq1 |
⊢ ( 𝑘 = 𝑚 → ( 𝑘 ≤ 𝑁 ↔ 𝑚 ≤ 𝑁 ) ) |
14 |
13
|
notbid |
⊢ ( 𝑘 = 𝑚 → ( ¬ 𝑘 ≤ 𝑁 ↔ ¬ 𝑚 ≤ 𝑁 ) ) |
15 |
|
fveqeq2 |
⊢ ( 𝑘 = 𝑚 → ( ( ( 𝑘 ∈ ℕ0 ↦ if ( 𝑘 ≤ 𝑁 , 𝐴 , 0 ) ) ‘ 𝑘 ) = 0 ↔ ( ( 𝑘 ∈ ℕ0 ↦ if ( 𝑘 ≤ 𝑁 , 𝐴 , 0 ) ) ‘ 𝑚 ) = 0 ) ) |
16 |
14 15
|
imbi12d |
⊢ ( 𝑘 = 𝑚 → ( ( ¬ 𝑘 ≤ 𝑁 → ( ( 𝑘 ∈ ℕ0 ↦ if ( 𝑘 ≤ 𝑁 , 𝐴 , 0 ) ) ‘ 𝑘 ) = 0 ) ↔ ( ¬ 𝑚 ≤ 𝑁 → ( ( 𝑘 ∈ ℕ0 ↦ if ( 𝑘 ≤ 𝑁 , 𝐴 , 0 ) ) ‘ 𝑚 ) = 0 ) ) ) |
17 |
|
iffalse |
⊢ ( ¬ 𝑘 ≤ 𝑁 → if ( 𝑘 ≤ 𝑁 , 𝐴 , 0 ) = 0 ) |
18 |
17
|
fveq2d |
⊢ ( ¬ 𝑘 ≤ 𝑁 → ( I ‘ if ( 𝑘 ≤ 𝑁 , 𝐴 , 0 ) ) = ( I ‘ 0 ) ) |
19 |
|
0cn |
⊢ 0 ∈ ℂ |
20 |
|
fvi |
⊢ ( 0 ∈ ℂ → ( I ‘ 0 ) = 0 ) |
21 |
19 20
|
ax-mp |
⊢ ( I ‘ 0 ) = 0 |
22 |
18 21
|
eqtrdi |
⊢ ( ¬ 𝑘 ≤ 𝑁 → ( I ‘ if ( 𝑘 ≤ 𝑁 , 𝐴 , 0 ) ) = 0 ) |
23 |
|
eqid |
⊢ ( 𝑘 ∈ ℕ0 ↦ if ( 𝑘 ≤ 𝑁 , 𝐴 , 0 ) ) = ( 𝑘 ∈ ℕ0 ↦ if ( 𝑘 ≤ 𝑁 , 𝐴 , 0 ) ) |
24 |
23
|
fvmpt2i |
⊢ ( 𝑘 ∈ ℕ0 → ( ( 𝑘 ∈ ℕ0 ↦ if ( 𝑘 ≤ 𝑁 , 𝐴 , 0 ) ) ‘ 𝑘 ) = ( I ‘ if ( 𝑘 ≤ 𝑁 , 𝐴 , 0 ) ) ) |
25 |
24
|
eqeq1d |
⊢ ( 𝑘 ∈ ℕ0 → ( ( ( 𝑘 ∈ ℕ0 ↦ if ( 𝑘 ≤ 𝑁 , 𝐴 , 0 ) ) ‘ 𝑘 ) = 0 ↔ ( I ‘ if ( 𝑘 ≤ 𝑁 , 𝐴 , 0 ) ) = 0 ) ) |
26 |
22 25
|
syl5ibr |
⊢ ( 𝑘 ∈ ℕ0 → ( ¬ 𝑘 ≤ 𝑁 → ( ( 𝑘 ∈ ℕ0 ↦ if ( 𝑘 ≤ 𝑁 , 𝐴 , 0 ) ) ‘ 𝑘 ) = 0 ) ) |
27 |
8 12 16 26
|
vtoclgaf |
⊢ ( 𝑚 ∈ ℕ0 → ( ¬ 𝑚 ≤ 𝑁 → ( ( 𝑘 ∈ ℕ0 ↦ if ( 𝑘 ≤ 𝑁 , 𝐴 , 0 ) ) ‘ 𝑚 ) = 0 ) ) |
28 |
27
|
imp |
⊢ ( ( 𝑚 ∈ ℕ0 ∧ ¬ 𝑚 ≤ 𝑁 ) → ( ( 𝑘 ∈ ℕ0 ↦ if ( 𝑘 ≤ 𝑁 , 𝐴 , 0 ) ) ‘ 𝑚 ) = 0 ) |
29 |
28
|
adantll |
⊢ ( ( ( 𝜑 ∧ 𝑚 ∈ ℕ0 ) ∧ ¬ 𝑚 ≤ 𝑁 ) → ( ( 𝑘 ∈ ℕ0 ↦ if ( 𝑘 ≤ 𝑁 , 𝐴 , 0 ) ) ‘ 𝑚 ) = 0 ) |
30 |
7 29
|
eqtrd |
⊢ ( ( ( 𝜑 ∧ 𝑚 ∈ ℕ0 ) ∧ ¬ 𝑚 ≤ 𝑁 ) → ( ( coeff ‘ 𝐹 ) ‘ 𝑚 ) = 0 ) |
31 |
30
|
ex |
⊢ ( ( 𝜑 ∧ 𝑚 ∈ ℕ0 ) → ( ¬ 𝑚 ≤ 𝑁 → ( ( coeff ‘ 𝐹 ) ‘ 𝑚 ) = 0 ) ) |
32 |
31
|
necon1ad |
⊢ ( ( 𝜑 ∧ 𝑚 ∈ ℕ0 ) → ( ( ( coeff ‘ 𝐹 ) ‘ 𝑚 ) ≠ 0 → 𝑚 ≤ 𝑁 ) ) |
33 |
32
|
ralrimiva |
⊢ ( 𝜑 → ∀ 𝑚 ∈ ℕ0 ( ( ( coeff ‘ 𝐹 ) ‘ 𝑚 ) ≠ 0 → 𝑚 ≤ 𝑁 ) ) |
34 |
|
eqid |
⊢ ( coeff ‘ 𝐹 ) = ( coeff ‘ 𝐹 ) |
35 |
34
|
coef3 |
⊢ ( 𝐹 ∈ ( Poly ‘ 𝑆 ) → ( coeff ‘ 𝐹 ) : ℕ0 ⟶ ℂ ) |
36 |
1 35
|
syl |
⊢ ( 𝜑 → ( coeff ‘ 𝐹 ) : ℕ0 ⟶ ℂ ) |
37 |
|
plyco0 |
⊢ ( ( 𝑁 ∈ ℕ0 ∧ ( coeff ‘ 𝐹 ) : ℕ0 ⟶ ℂ ) → ( ( ( coeff ‘ 𝐹 ) “ ( ℤ≥ ‘ ( 𝑁 + 1 ) ) ) = { 0 } ↔ ∀ 𝑚 ∈ ℕ0 ( ( ( coeff ‘ 𝐹 ) ‘ 𝑚 ) ≠ 0 → 𝑚 ≤ 𝑁 ) ) ) |
38 |
2 36 37
|
syl2anc |
⊢ ( 𝜑 → ( ( ( coeff ‘ 𝐹 ) “ ( ℤ≥ ‘ ( 𝑁 + 1 ) ) ) = { 0 } ↔ ∀ 𝑚 ∈ ℕ0 ( ( ( coeff ‘ 𝐹 ) ‘ 𝑚 ) ≠ 0 → 𝑚 ≤ 𝑁 ) ) ) |
39 |
33 38
|
mpbird |
⊢ ( 𝜑 → ( ( coeff ‘ 𝐹 ) “ ( ℤ≥ ‘ ( 𝑁 + 1 ) ) ) = { 0 } ) |
40 |
|
eqid |
⊢ ( deg ‘ 𝐹 ) = ( deg ‘ 𝐹 ) |
41 |
34 40
|
dgrlb |
⊢ ( ( 𝐹 ∈ ( Poly ‘ 𝑆 ) ∧ 𝑁 ∈ ℕ0 ∧ ( ( coeff ‘ 𝐹 ) “ ( ℤ≥ ‘ ( 𝑁 + 1 ) ) ) = { 0 } ) → ( deg ‘ 𝐹 ) ≤ 𝑁 ) |
42 |
1 2 39 41
|
syl3anc |
⊢ ( 𝜑 → ( deg ‘ 𝐹 ) ≤ 𝑁 ) |