| Step | Hyp | Ref
| Expression |
| 1 | | ssid 4006 |
. . . 4
⊢ ℂ
⊆ ℂ |
| 2 | | coe1term.1 |
. . . . 5
⊢ 𝐹 = (𝑧 ∈ ℂ ↦ (𝐴 · (𝑧↑𝑁))) |
| 3 | 2 | ply1term 26243 |
. . . 4
⊢ ((ℂ
⊆ ℂ ∧ 𝐴
∈ ℂ ∧ 𝑁
∈ ℕ0) → 𝐹 ∈
(Poly‘ℂ)) |
| 4 | 1, 3 | mp3an1 1450 |
. . 3
⊢ ((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ0)
→ 𝐹 ∈
(Poly‘ℂ)) |
| 5 | | simpr 484 |
. . 3
⊢ ((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ0)
→ 𝑁 ∈
ℕ0) |
| 6 | | simpl 482 |
. . . . . 6
⊢ ((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ0)
→ 𝐴 ∈
ℂ) |
| 7 | | 0cn 11253 |
. . . . . 6
⊢ 0 ∈
ℂ |
| 8 | | ifcl 4571 |
. . . . . 6
⊢ ((𝐴 ∈ ℂ ∧ 0 ∈
ℂ) → if(𝑛 =
𝑁, 𝐴, 0) ∈ ℂ) |
| 9 | 6, 7, 8 | sylancl 586 |
. . . . 5
⊢ ((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ0)
→ if(𝑛 = 𝑁, 𝐴, 0) ∈ ℂ) |
| 10 | 9 | adantr 480 |
. . . 4
⊢ (((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ0)
∧ 𝑛 ∈
ℕ0) → if(𝑛 = 𝑁, 𝐴, 0) ∈ ℂ) |
| 11 | 10 | fmpttd 7135 |
. . 3
⊢ ((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ0)
→ (𝑛 ∈
ℕ0 ↦ if(𝑛 = 𝑁, 𝐴,
0)):ℕ0⟶ℂ) |
| 12 | | eqid 2737 |
. . . . . . . 8
⊢ (𝑛 ∈ ℕ0
↦ if(𝑛 = 𝑁, 𝐴, 0)) = (𝑛 ∈ ℕ0 ↦ if(𝑛 = 𝑁, 𝐴, 0)) |
| 13 | | eqeq1 2741 |
. . . . . . . . 9
⊢ (𝑛 = 𝑘 → (𝑛 = 𝑁 ↔ 𝑘 = 𝑁)) |
| 14 | 13 | ifbid 4549 |
. . . . . . . 8
⊢ (𝑛 = 𝑘 → if(𝑛 = 𝑁, 𝐴, 0) = if(𝑘 = 𝑁, 𝐴, 0)) |
| 15 | | simpr 484 |
. . . . . . . 8
⊢ (((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ0)
∧ 𝑘 ∈
ℕ0) → 𝑘 ∈ ℕ0) |
| 16 | | ifcl 4571 |
. . . . . . . . . 10
⊢ ((𝐴 ∈ ℂ ∧ 0 ∈
ℂ) → if(𝑘 =
𝑁, 𝐴, 0) ∈ ℂ) |
| 17 | 6, 7, 16 | sylancl 586 |
. . . . . . . . 9
⊢ ((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ0)
→ if(𝑘 = 𝑁, 𝐴, 0) ∈ ℂ) |
| 18 | 17 | adantr 480 |
. . . . . . . 8
⊢ (((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ0)
∧ 𝑘 ∈
ℕ0) → if(𝑘 = 𝑁, 𝐴, 0) ∈ ℂ) |
| 19 | 12, 14, 15, 18 | fvmptd3 7039 |
. . . . . . 7
⊢ (((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ0)
∧ 𝑘 ∈
ℕ0) → ((𝑛 ∈ ℕ0 ↦ if(𝑛 = 𝑁, 𝐴, 0))‘𝑘) = if(𝑘 = 𝑁, 𝐴, 0)) |
| 20 | 19 | neeq1d 3000 |
. . . . . 6
⊢ (((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ0)
∧ 𝑘 ∈
ℕ0) → (((𝑛 ∈ ℕ0 ↦ if(𝑛 = 𝑁, 𝐴, 0))‘𝑘) ≠ 0 ↔ if(𝑘 = 𝑁, 𝐴, 0) ≠ 0)) |
| 21 | | nn0re 12535 |
. . . . . . . . 9
⊢ (𝑁 ∈ ℕ0
→ 𝑁 ∈
ℝ) |
| 22 | 21 | leidd 11829 |
. . . . . . . 8
⊢ (𝑁 ∈ ℕ0
→ 𝑁 ≤ 𝑁) |
| 23 | 22 | ad2antlr 727 |
. . . . . . 7
⊢ (((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ0)
∧ 𝑘 ∈
ℕ0) → 𝑁 ≤ 𝑁) |
| 24 | | iffalse 4534 |
. . . . . . . . 9
⊢ (¬
𝑘 = 𝑁 → if(𝑘 = 𝑁, 𝐴, 0) = 0) |
| 25 | 24 | necon1ai 2968 |
. . . . . . . 8
⊢ (if(𝑘 = 𝑁, 𝐴, 0) ≠ 0 → 𝑘 = 𝑁) |
| 26 | 25 | breq1d 5153 |
. . . . . . 7
⊢ (if(𝑘 = 𝑁, 𝐴, 0) ≠ 0 → (𝑘 ≤ 𝑁 ↔ 𝑁 ≤ 𝑁)) |
| 27 | 23, 26 | syl5ibrcom 247 |
. . . . . 6
⊢ (((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ0)
∧ 𝑘 ∈
ℕ0) → (if(𝑘 = 𝑁, 𝐴, 0) ≠ 0 → 𝑘 ≤ 𝑁)) |
| 28 | 20, 27 | sylbid 240 |
. . . . 5
⊢ (((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ0)
∧ 𝑘 ∈
ℕ0) → (((𝑛 ∈ ℕ0 ↦ if(𝑛 = 𝑁, 𝐴, 0))‘𝑘) ≠ 0 → 𝑘 ≤ 𝑁)) |
| 29 | 28 | ralrimiva 3146 |
. . . 4
⊢ ((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ0)
→ ∀𝑘 ∈
ℕ0 (((𝑛
∈ ℕ0 ↦ if(𝑛 = 𝑁, 𝐴, 0))‘𝑘) ≠ 0 → 𝑘 ≤ 𝑁)) |
| 30 | | plyco0 26231 |
. . . . 5
⊢ ((𝑁 ∈ ℕ0
∧ (𝑛 ∈
ℕ0 ↦ if(𝑛 = 𝑁, 𝐴, 0)):ℕ0⟶ℂ)
→ (((𝑛 ∈
ℕ0 ↦ if(𝑛 = 𝑁, 𝐴, 0)) “
(ℤ≥‘(𝑁 + 1))) = {0} ↔ ∀𝑘 ∈ ℕ0
(((𝑛 ∈
ℕ0 ↦ if(𝑛 = 𝑁, 𝐴, 0))‘𝑘) ≠ 0 → 𝑘 ≤ 𝑁))) |
| 31 | 5, 11, 30 | syl2anc 584 |
. . . 4
⊢ ((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ0)
→ (((𝑛 ∈
ℕ0 ↦ if(𝑛 = 𝑁, 𝐴, 0)) “
(ℤ≥‘(𝑁 + 1))) = {0} ↔ ∀𝑘 ∈ ℕ0
(((𝑛 ∈
ℕ0 ↦ if(𝑛 = 𝑁, 𝐴, 0))‘𝑘) ≠ 0 → 𝑘 ≤ 𝑁))) |
| 32 | 29, 31 | mpbird 257 |
. . 3
⊢ ((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ0)
→ ((𝑛 ∈
ℕ0 ↦ if(𝑛 = 𝑁, 𝐴, 0)) “
(ℤ≥‘(𝑁 + 1))) = {0}) |
| 33 | 2 | ply1termlem 26242 |
. . . 4
⊢ ((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ0)
→ 𝐹 = (𝑧 ∈ ℂ ↦
Σ𝑘 ∈ (0...𝑁)(if(𝑘 = 𝑁, 𝐴, 0) · (𝑧↑𝑘)))) |
| 34 | | elfznn0 13660 |
. . . . . . 7
⊢ (𝑘 ∈ (0...𝑁) → 𝑘 ∈ ℕ0) |
| 35 | 19 | oveq1d 7446 |
. . . . . . 7
⊢ (((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ0)
∧ 𝑘 ∈
ℕ0) → (((𝑛 ∈ ℕ0 ↦ if(𝑛 = 𝑁, 𝐴, 0))‘𝑘) · (𝑧↑𝑘)) = (if(𝑘 = 𝑁, 𝐴, 0) · (𝑧↑𝑘))) |
| 36 | 34, 35 | sylan2 593 |
. . . . . 6
⊢ (((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ0)
∧ 𝑘 ∈ (0...𝑁)) → (((𝑛 ∈ ℕ0 ↦ if(𝑛 = 𝑁, 𝐴, 0))‘𝑘) · (𝑧↑𝑘)) = (if(𝑘 = 𝑁, 𝐴, 0) · (𝑧↑𝑘))) |
| 37 | 36 | sumeq2dv 15738 |
. . . . 5
⊢ ((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ0)
→ Σ𝑘 ∈
(0...𝑁)(((𝑛 ∈ ℕ0
↦ if(𝑛 = 𝑁, 𝐴, 0))‘𝑘) · (𝑧↑𝑘)) = Σ𝑘 ∈ (0...𝑁)(if(𝑘 = 𝑁, 𝐴, 0) · (𝑧↑𝑘))) |
| 38 | 37 | mpteq2dv 5244 |
. . . 4
⊢ ((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ0)
→ (𝑧 ∈ ℂ
↦ Σ𝑘 ∈
(0...𝑁)(((𝑛 ∈ ℕ0
↦ if(𝑛 = 𝑁, 𝐴, 0))‘𝑘) · (𝑧↑𝑘))) = (𝑧 ∈ ℂ ↦ Σ𝑘 ∈ (0...𝑁)(if(𝑘 = 𝑁, 𝐴, 0) · (𝑧↑𝑘)))) |
| 39 | 33, 38 | eqtr4d 2780 |
. . 3
⊢ ((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ0)
→ 𝐹 = (𝑧 ∈ ℂ ↦
Σ𝑘 ∈ (0...𝑁)(((𝑛 ∈ ℕ0 ↦ if(𝑛 = 𝑁, 𝐴, 0))‘𝑘) · (𝑧↑𝑘)))) |
| 40 | 4, 5, 11, 32, 39 | coeeq 26266 |
. 2
⊢ ((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ0)
→ (coeff‘𝐹) =
(𝑛 ∈
ℕ0 ↦ if(𝑛 = 𝑁, 𝐴, 0))) |
| 41 | 4 | adantr 480 |
. . . 4
⊢ (((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ0)
∧ 𝐴 ≠ 0) →
𝐹 ∈
(Poly‘ℂ)) |
| 42 | 5 | adantr 480 |
. . . 4
⊢ (((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ0)
∧ 𝐴 ≠ 0) →
𝑁 ∈
ℕ0) |
| 43 | 11 | adantr 480 |
. . . 4
⊢ (((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ0)
∧ 𝐴 ≠ 0) →
(𝑛 ∈
ℕ0 ↦ if(𝑛 = 𝑁, 𝐴,
0)):ℕ0⟶ℂ) |
| 44 | 32 | adantr 480 |
. . . 4
⊢ (((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ0)
∧ 𝐴 ≠ 0) →
((𝑛 ∈
ℕ0 ↦ if(𝑛 = 𝑁, 𝐴, 0)) “
(ℤ≥‘(𝑁 + 1))) = {0}) |
| 45 | 39 | adantr 480 |
. . . 4
⊢ (((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ0)
∧ 𝐴 ≠ 0) →
𝐹 = (𝑧 ∈ ℂ ↦ Σ𝑘 ∈ (0...𝑁)(((𝑛 ∈ ℕ0 ↦ if(𝑛 = 𝑁, 𝐴, 0))‘𝑘) · (𝑧↑𝑘)))) |
| 46 | | iftrue 4531 |
. . . . . . . 8
⊢ (𝑛 = 𝑁 → if(𝑛 = 𝑁, 𝐴, 0) = 𝐴) |
| 47 | 46, 12 | fvmptg 7014 |
. . . . . . 7
⊢ ((𝑁 ∈ ℕ0
∧ 𝐴 ∈ ℂ)
→ ((𝑛 ∈
ℕ0 ↦ if(𝑛 = 𝑁, 𝐴, 0))‘𝑁) = 𝐴) |
| 48 | 47 | ancoms 458 |
. . . . . 6
⊢ ((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ0)
→ ((𝑛 ∈
ℕ0 ↦ if(𝑛 = 𝑁, 𝐴, 0))‘𝑁) = 𝐴) |
| 49 | 48 | neeq1d 3000 |
. . . . 5
⊢ ((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ0)
→ (((𝑛 ∈
ℕ0 ↦ if(𝑛 = 𝑁, 𝐴, 0))‘𝑁) ≠ 0 ↔ 𝐴 ≠ 0)) |
| 50 | 49 | biimpar 477 |
. . . 4
⊢ (((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ0)
∧ 𝐴 ≠ 0) →
((𝑛 ∈
ℕ0 ↦ if(𝑛 = 𝑁, 𝐴, 0))‘𝑁) ≠ 0) |
| 51 | 41, 42, 43, 44, 45, 50 | dgreq 26283 |
. . 3
⊢ (((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ0)
∧ 𝐴 ≠ 0) →
(deg‘𝐹) = 𝑁) |
| 52 | 51 | ex 412 |
. 2
⊢ ((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ0)
→ (𝐴 ≠ 0 →
(deg‘𝐹) = 𝑁)) |
| 53 | 40, 52 | jca 511 |
1
⊢ ((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ0)
→ ((coeff‘𝐹) =
(𝑛 ∈
ℕ0 ↦ if(𝑛 = 𝑁, 𝐴, 0)) ∧ (𝐴 ≠ 0 → (deg‘𝐹) = 𝑁))) |