Step | Hyp | Ref
| Expression |
1 | | dgrle.1 |
. 2
⊢ (𝜑 → 𝐹 ∈ (Poly‘𝑆)) |
2 | | dgrle.2 |
. 2
⊢ (𝜑 → 𝑁 ∈
ℕ0) |
3 | | dgrle.3 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑘 ∈ (0...𝑁)) → 𝐴 ∈ ℂ) |
4 | | dgrle.4 |
. . . . . . . . . 10
⊢ (𝜑 → 𝐹 = (𝑧 ∈ ℂ ↦ Σ𝑘 ∈ (0...𝑁)(𝐴 · (𝑧↑𝑘)))) |
5 | 1, 2, 3, 4 | coeeq2 23802 |
. . . . . . . . 9
⊢ (𝜑 → (coeff‘𝐹) = (𝑘 ∈ ℕ0 ↦ if(𝑘 ≤ 𝑁, 𝐴, 0))) |
6 | 5 | ad2antrr 758 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑚 ∈ ℕ0) ∧ ¬
𝑚 ≤ 𝑁) → (coeff‘𝐹) = (𝑘 ∈ ℕ0 ↦ if(𝑘 ≤ 𝑁, 𝐴, 0))) |
7 | 6 | fveq1d 6105 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑚 ∈ ℕ0) ∧ ¬
𝑚 ≤ 𝑁) → ((coeff‘𝐹)‘𝑚) = ((𝑘 ∈ ℕ0 ↦ if(𝑘 ≤ 𝑁, 𝐴, 0))‘𝑚)) |
8 | | nfcv 2751 |
. . . . . . . . . 10
⊢
Ⅎ𝑘𝑚 |
9 | | nfv 1830 |
. . . . . . . . . . 11
⊢
Ⅎ𝑘 ¬ 𝑚 ≤ 𝑁 |
10 | | nffvmpt1 6111 |
. . . . . . . . . . . 12
⊢
Ⅎ𝑘((𝑘 ∈ ℕ0 ↦ if(𝑘 ≤ 𝑁, 𝐴, 0))‘𝑚) |
11 | 10 | nfeq1 2764 |
. . . . . . . . . . 11
⊢
Ⅎ𝑘((𝑘 ∈ ℕ0
↦ if(𝑘 ≤ 𝑁, 𝐴, 0))‘𝑚) = 0 |
12 | 9, 11 | nfim 1813 |
. . . . . . . . . 10
⊢
Ⅎ𝑘(¬ 𝑚 ≤ 𝑁 → ((𝑘 ∈ ℕ0 ↦ if(𝑘 ≤ 𝑁, 𝐴, 0))‘𝑚) = 0) |
13 | | breq1 4586 |
. . . . . . . . . . . 12
⊢ (𝑘 = 𝑚 → (𝑘 ≤ 𝑁 ↔ 𝑚 ≤ 𝑁)) |
14 | 13 | notbid 307 |
. . . . . . . . . . 11
⊢ (𝑘 = 𝑚 → (¬ 𝑘 ≤ 𝑁 ↔ ¬ 𝑚 ≤ 𝑁)) |
15 | | fveq2 6103 |
. . . . . . . . . . . 12
⊢ (𝑘 = 𝑚 → ((𝑘 ∈ ℕ0 ↦ if(𝑘 ≤ 𝑁, 𝐴, 0))‘𝑘) = ((𝑘 ∈ ℕ0 ↦ if(𝑘 ≤ 𝑁, 𝐴, 0))‘𝑚)) |
16 | 15 | eqeq1d 2612 |
. . . . . . . . . . 11
⊢ (𝑘 = 𝑚 → (((𝑘 ∈ ℕ0 ↦ if(𝑘 ≤ 𝑁, 𝐴, 0))‘𝑘) = 0 ↔ ((𝑘 ∈ ℕ0 ↦ if(𝑘 ≤ 𝑁, 𝐴, 0))‘𝑚) = 0)) |
17 | 14, 16 | imbi12d 333 |
. . . . . . . . . 10
⊢ (𝑘 = 𝑚 → ((¬ 𝑘 ≤ 𝑁 → ((𝑘 ∈ ℕ0 ↦ if(𝑘 ≤ 𝑁, 𝐴, 0))‘𝑘) = 0) ↔ (¬ 𝑚 ≤ 𝑁 → ((𝑘 ∈ ℕ0 ↦ if(𝑘 ≤ 𝑁, 𝐴, 0))‘𝑚) = 0))) |
18 | | iffalse 4045 |
. . . . . . . . . . . . 13
⊢ (¬
𝑘 ≤ 𝑁 → if(𝑘 ≤ 𝑁, 𝐴, 0) = 0) |
19 | 18 | fveq2d 6107 |
. . . . . . . . . . . 12
⊢ (¬
𝑘 ≤ 𝑁 → ( I ‘if(𝑘 ≤ 𝑁, 𝐴, 0)) = ( I ‘0)) |
20 | | 0cn 9911 |
. . . . . . . . . . . . 13
⊢ 0 ∈
ℂ |
21 | | fvi 6165 |
. . . . . . . . . . . . 13
⊢ (0 ∈
ℂ → ( I ‘0) = 0) |
22 | 20, 21 | ax-mp 5 |
. . . . . . . . . . . 12
⊢ ( I
‘0) = 0 |
23 | 19, 22 | syl6eq 2660 |
. . . . . . . . . . 11
⊢ (¬
𝑘 ≤ 𝑁 → ( I ‘if(𝑘 ≤ 𝑁, 𝐴, 0)) = 0) |
24 | | eqid 2610 |
. . . . . . . . . . . . 13
⊢ (𝑘 ∈ ℕ0
↦ if(𝑘 ≤ 𝑁, 𝐴, 0)) = (𝑘 ∈ ℕ0 ↦ if(𝑘 ≤ 𝑁, 𝐴, 0)) |
25 | 24 | fvmpt2i 6199 |
. . . . . . . . . . . 12
⊢ (𝑘 ∈ ℕ0
→ ((𝑘 ∈
ℕ0 ↦ if(𝑘 ≤ 𝑁, 𝐴, 0))‘𝑘) = ( I ‘if(𝑘 ≤ 𝑁, 𝐴, 0))) |
26 | 25 | eqeq1d 2612 |
. . . . . . . . . . 11
⊢ (𝑘 ∈ ℕ0
→ (((𝑘 ∈
ℕ0 ↦ if(𝑘 ≤ 𝑁, 𝐴, 0))‘𝑘) = 0 ↔ ( I ‘if(𝑘 ≤ 𝑁, 𝐴, 0)) = 0)) |
27 | 23, 26 | syl5ibr 235 |
. . . . . . . . . 10
⊢ (𝑘 ∈ ℕ0
→ (¬ 𝑘 ≤ 𝑁 → ((𝑘 ∈ ℕ0 ↦ if(𝑘 ≤ 𝑁, 𝐴, 0))‘𝑘) = 0)) |
28 | 8, 12, 17, 27 | vtoclgaf 3244 |
. . . . . . . . 9
⊢ (𝑚 ∈ ℕ0
→ (¬ 𝑚 ≤ 𝑁 → ((𝑘 ∈ ℕ0 ↦ if(𝑘 ≤ 𝑁, 𝐴, 0))‘𝑚) = 0)) |
29 | 28 | imp 444 |
. . . . . . . 8
⊢ ((𝑚 ∈ ℕ0
∧ ¬ 𝑚 ≤ 𝑁) → ((𝑘 ∈ ℕ0 ↦ if(𝑘 ≤ 𝑁, 𝐴, 0))‘𝑚) = 0) |
30 | 29 | adantll 746 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑚 ∈ ℕ0) ∧ ¬
𝑚 ≤ 𝑁) → ((𝑘 ∈ ℕ0 ↦ if(𝑘 ≤ 𝑁, 𝐴, 0))‘𝑚) = 0) |
31 | 7, 30 | eqtrd 2644 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑚 ∈ ℕ0) ∧ ¬
𝑚 ≤ 𝑁) → ((coeff‘𝐹)‘𝑚) = 0) |
32 | 31 | ex 449 |
. . . . 5
⊢ ((𝜑 ∧ 𝑚 ∈ ℕ0) → (¬
𝑚 ≤ 𝑁 → ((coeff‘𝐹)‘𝑚) = 0)) |
33 | 32 | necon1ad 2799 |
. . . 4
⊢ ((𝜑 ∧ 𝑚 ∈ ℕ0) →
(((coeff‘𝐹)‘𝑚) ≠ 0 → 𝑚 ≤ 𝑁)) |
34 | 33 | ralrimiva 2949 |
. . 3
⊢ (𝜑 → ∀𝑚 ∈ ℕ0
(((coeff‘𝐹)‘𝑚) ≠ 0 → 𝑚 ≤ 𝑁)) |
35 | | eqid 2610 |
. . . . . 6
⊢
(coeff‘𝐹) =
(coeff‘𝐹) |
36 | 35 | coef3 23792 |
. . . . 5
⊢ (𝐹 ∈ (Poly‘𝑆) → (coeff‘𝐹):ℕ0⟶ℂ) |
37 | 1, 36 | syl 17 |
. . . 4
⊢ (𝜑 → (coeff‘𝐹):ℕ0⟶ℂ) |
38 | | plyco0 23752 |
. . . 4
⊢ ((𝑁 ∈ ℕ0
∧ (coeff‘𝐹):ℕ0⟶ℂ) →
(((coeff‘𝐹) “
(ℤ≥‘(𝑁 + 1))) = {0} ↔ ∀𝑚 ∈ ℕ0
(((coeff‘𝐹)‘𝑚) ≠ 0 → 𝑚 ≤ 𝑁))) |
39 | 2, 37, 38 | syl2anc 691 |
. . 3
⊢ (𝜑 → (((coeff‘𝐹) “
(ℤ≥‘(𝑁 + 1))) = {0} ↔ ∀𝑚 ∈ ℕ0
(((coeff‘𝐹)‘𝑚) ≠ 0 → 𝑚 ≤ 𝑁))) |
40 | 34, 39 | mpbird 246 |
. 2
⊢ (𝜑 → ((coeff‘𝐹) “
(ℤ≥‘(𝑁 + 1))) = {0}) |
41 | | eqid 2610 |
. . 3
⊢
(deg‘𝐹) =
(deg‘𝐹) |
42 | 35, 41 | dgrlb 23796 |
. 2
⊢ ((𝐹 ∈ (Poly‘𝑆) ∧ 𝑁 ∈ ℕ0 ∧
((coeff‘𝐹) “
(ℤ≥‘(𝑁 + 1))) = {0}) → (deg‘𝐹) ≤ 𝑁) |
43 | 1, 2, 40, 42 | syl3anc 1318 |
1
⊢ (𝜑 → (deg‘𝐹) ≤ 𝑁) |