Step | Hyp | Ref
| Expression |
1 | | ssid 3587 |
. . . 4
⊢ ℂ
⊆ ℂ |
2 | | coe1term.1 |
. . . . 5
⊢ 𝐹 = (𝑧 ∈ ℂ ↦ (𝐴 · (𝑧↑𝑁))) |
3 | 2 | ply1term 23764 |
. . . 4
⊢ ((ℂ
⊆ ℂ ∧ 𝐴
∈ ℂ ∧ 𝑁
∈ ℕ0) → 𝐹 ∈
(Poly‘ℂ)) |
4 | 1, 3 | mp3an1 1403 |
. . 3
⊢ ((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ0)
→ 𝐹 ∈
(Poly‘ℂ)) |
5 | | simpr 476 |
. . 3
⊢ ((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ0)
→ 𝑁 ∈
ℕ0) |
6 | | simpl 472 |
. . . . . 6
⊢ ((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ0)
→ 𝐴 ∈
ℂ) |
7 | | 0cn 9911 |
. . . . . 6
⊢ 0 ∈
ℂ |
8 | | ifcl 4080 |
. . . . . 6
⊢ ((𝐴 ∈ ℂ ∧ 0 ∈
ℂ) → if(𝑛 =
𝑁, 𝐴, 0) ∈ ℂ) |
9 | 6, 7, 8 | sylancl 693 |
. . . . 5
⊢ ((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ0)
→ if(𝑛 = 𝑁, 𝐴, 0) ∈ ℂ) |
10 | 9 | adantr 480 |
. . . 4
⊢ (((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ0)
∧ 𝑛 ∈
ℕ0) → if(𝑛 = 𝑁, 𝐴, 0) ∈ ℂ) |
11 | | eqid 2610 |
. . . 4
⊢ (𝑛 ∈ ℕ0
↦ if(𝑛 = 𝑁, 𝐴, 0)) = (𝑛 ∈ ℕ0 ↦ if(𝑛 = 𝑁, 𝐴, 0)) |
12 | 10, 11 | fmptd 6292 |
. . 3
⊢ ((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ0)
→ (𝑛 ∈
ℕ0 ↦ if(𝑛 = 𝑁, 𝐴,
0)):ℕ0⟶ℂ) |
13 | | simpr 476 |
. . . . . . . 8
⊢ (((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ0)
∧ 𝑘 ∈
ℕ0) → 𝑘 ∈ ℕ0) |
14 | | ifcl 4080 |
. . . . . . . . . 10
⊢ ((𝐴 ∈ ℂ ∧ 0 ∈
ℂ) → if(𝑘 =
𝑁, 𝐴, 0) ∈ ℂ) |
15 | 6, 7, 14 | sylancl 693 |
. . . . . . . . 9
⊢ ((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ0)
→ if(𝑘 = 𝑁, 𝐴, 0) ∈ ℂ) |
16 | 15 | adantr 480 |
. . . . . . . 8
⊢ (((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ0)
∧ 𝑘 ∈
ℕ0) → if(𝑘 = 𝑁, 𝐴, 0) ∈ ℂ) |
17 | | eqeq1 2614 |
. . . . . . . . . 10
⊢ (𝑛 = 𝑘 → (𝑛 = 𝑁 ↔ 𝑘 = 𝑁)) |
18 | 17 | ifbid 4058 |
. . . . . . . . 9
⊢ (𝑛 = 𝑘 → if(𝑛 = 𝑁, 𝐴, 0) = if(𝑘 = 𝑁, 𝐴, 0)) |
19 | 18, 11 | fvmptg 6189 |
. . . . . . . 8
⊢ ((𝑘 ∈ ℕ0
∧ if(𝑘 = 𝑁, 𝐴, 0) ∈ ℂ) → ((𝑛 ∈ ℕ0
↦ if(𝑛 = 𝑁, 𝐴, 0))‘𝑘) = if(𝑘 = 𝑁, 𝐴, 0)) |
20 | 13, 16, 19 | syl2anc 691 |
. . . . . . 7
⊢ (((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ0)
∧ 𝑘 ∈
ℕ0) → ((𝑛 ∈ ℕ0 ↦ if(𝑛 = 𝑁, 𝐴, 0))‘𝑘) = if(𝑘 = 𝑁, 𝐴, 0)) |
21 | 20 | neeq1d 2841 |
. . . . . 6
⊢ (((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ0)
∧ 𝑘 ∈
ℕ0) → (((𝑛 ∈ ℕ0 ↦ if(𝑛 = 𝑁, 𝐴, 0))‘𝑘) ≠ 0 ↔ if(𝑘 = 𝑁, 𝐴, 0) ≠ 0)) |
22 | | nn0re 11178 |
. . . . . . . . 9
⊢ (𝑁 ∈ ℕ0
→ 𝑁 ∈
ℝ) |
23 | 22 | leidd 10473 |
. . . . . . . 8
⊢ (𝑁 ∈ ℕ0
→ 𝑁 ≤ 𝑁) |
24 | 23 | ad2antlr 759 |
. . . . . . 7
⊢ (((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ0)
∧ 𝑘 ∈
ℕ0) → 𝑁 ≤ 𝑁) |
25 | | iffalse 4045 |
. . . . . . . . 9
⊢ (¬
𝑘 = 𝑁 → if(𝑘 = 𝑁, 𝐴, 0) = 0) |
26 | 25 | necon1ai 2809 |
. . . . . . . 8
⊢ (if(𝑘 = 𝑁, 𝐴, 0) ≠ 0 → 𝑘 = 𝑁) |
27 | 26 | breq1d 4593 |
. . . . . . 7
⊢ (if(𝑘 = 𝑁, 𝐴, 0) ≠ 0 → (𝑘 ≤ 𝑁 ↔ 𝑁 ≤ 𝑁)) |
28 | 24, 27 | syl5ibrcom 236 |
. . . . . 6
⊢ (((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ0)
∧ 𝑘 ∈
ℕ0) → (if(𝑘 = 𝑁, 𝐴, 0) ≠ 0 → 𝑘 ≤ 𝑁)) |
29 | 21, 28 | sylbid 229 |
. . . . 5
⊢ (((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ0)
∧ 𝑘 ∈
ℕ0) → (((𝑛 ∈ ℕ0 ↦ if(𝑛 = 𝑁, 𝐴, 0))‘𝑘) ≠ 0 → 𝑘 ≤ 𝑁)) |
30 | 29 | ralrimiva 2949 |
. . . 4
⊢ ((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ0)
→ ∀𝑘 ∈
ℕ0 (((𝑛
∈ ℕ0 ↦ if(𝑛 = 𝑁, 𝐴, 0))‘𝑘) ≠ 0 → 𝑘 ≤ 𝑁)) |
31 | | plyco0 23752 |
. . . . 5
⊢ ((𝑁 ∈ ℕ0
∧ (𝑛 ∈
ℕ0 ↦ if(𝑛 = 𝑁, 𝐴, 0)):ℕ0⟶ℂ)
→ (((𝑛 ∈
ℕ0 ↦ if(𝑛 = 𝑁, 𝐴, 0)) “
(ℤ≥‘(𝑁 + 1))) = {0} ↔ ∀𝑘 ∈ ℕ0
(((𝑛 ∈
ℕ0 ↦ if(𝑛 = 𝑁, 𝐴, 0))‘𝑘) ≠ 0 → 𝑘 ≤ 𝑁))) |
32 | 5, 12, 31 | syl2anc 691 |
. . . 4
⊢ ((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ0)
→ (((𝑛 ∈
ℕ0 ↦ if(𝑛 = 𝑁, 𝐴, 0)) “
(ℤ≥‘(𝑁 + 1))) = {0} ↔ ∀𝑘 ∈ ℕ0
(((𝑛 ∈
ℕ0 ↦ if(𝑛 = 𝑁, 𝐴, 0))‘𝑘) ≠ 0 → 𝑘 ≤ 𝑁))) |
33 | 30, 32 | mpbird 246 |
. . 3
⊢ ((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ0)
→ ((𝑛 ∈
ℕ0 ↦ if(𝑛 = 𝑁, 𝐴, 0)) “
(ℤ≥‘(𝑁 + 1))) = {0}) |
34 | 2 | ply1termlem 23763 |
. . . 4
⊢ ((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ0)
→ 𝐹 = (𝑧 ∈ ℂ ↦
Σ𝑘 ∈ (0...𝑁)(if(𝑘 = 𝑁, 𝐴, 0) · (𝑧↑𝑘)))) |
35 | | elfznn0 12302 |
. . . . . . 7
⊢ (𝑘 ∈ (0...𝑁) → 𝑘 ∈ ℕ0) |
36 | 20 | oveq1d 6564 |
. . . . . . 7
⊢ (((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ0)
∧ 𝑘 ∈
ℕ0) → (((𝑛 ∈ ℕ0 ↦ if(𝑛 = 𝑁, 𝐴, 0))‘𝑘) · (𝑧↑𝑘)) = (if(𝑘 = 𝑁, 𝐴, 0) · (𝑧↑𝑘))) |
37 | 35, 36 | sylan2 490 |
. . . . . 6
⊢ (((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ0)
∧ 𝑘 ∈ (0...𝑁)) → (((𝑛 ∈ ℕ0 ↦ if(𝑛 = 𝑁, 𝐴, 0))‘𝑘) · (𝑧↑𝑘)) = (if(𝑘 = 𝑁, 𝐴, 0) · (𝑧↑𝑘))) |
38 | 37 | sumeq2dv 14281 |
. . . . 5
⊢ ((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ0)
→ Σ𝑘 ∈
(0...𝑁)(((𝑛 ∈ ℕ0
↦ if(𝑛 = 𝑁, 𝐴, 0))‘𝑘) · (𝑧↑𝑘)) = Σ𝑘 ∈ (0...𝑁)(if(𝑘 = 𝑁, 𝐴, 0) · (𝑧↑𝑘))) |
39 | 38 | mpteq2dv 4673 |
. . . 4
⊢ ((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ0)
→ (𝑧 ∈ ℂ
↦ Σ𝑘 ∈
(0...𝑁)(((𝑛 ∈ ℕ0
↦ if(𝑛 = 𝑁, 𝐴, 0))‘𝑘) · (𝑧↑𝑘))) = (𝑧 ∈ ℂ ↦ Σ𝑘 ∈ (0...𝑁)(if(𝑘 = 𝑁, 𝐴, 0) · (𝑧↑𝑘)))) |
40 | 34, 39 | eqtr4d 2647 |
. . 3
⊢ ((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ0)
→ 𝐹 = (𝑧 ∈ ℂ ↦
Σ𝑘 ∈ (0...𝑁)(((𝑛 ∈ ℕ0 ↦ if(𝑛 = 𝑁, 𝐴, 0))‘𝑘) · (𝑧↑𝑘)))) |
41 | 4, 5, 12, 33, 40 | coeeq 23787 |
. 2
⊢ ((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ0)
→ (coeff‘𝐹) =
(𝑛 ∈
ℕ0 ↦ if(𝑛 = 𝑁, 𝐴, 0))) |
42 | 4 | adantr 480 |
. . . 4
⊢ (((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ0)
∧ 𝐴 ≠ 0) →
𝐹 ∈
(Poly‘ℂ)) |
43 | 5 | adantr 480 |
. . . 4
⊢ (((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ0)
∧ 𝐴 ≠ 0) →
𝑁 ∈
ℕ0) |
44 | 12 | adantr 480 |
. . . 4
⊢ (((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ0)
∧ 𝐴 ≠ 0) →
(𝑛 ∈
ℕ0 ↦ if(𝑛 = 𝑁, 𝐴,
0)):ℕ0⟶ℂ) |
45 | 33 | adantr 480 |
. . . 4
⊢ (((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ0)
∧ 𝐴 ≠ 0) →
((𝑛 ∈
ℕ0 ↦ if(𝑛 = 𝑁, 𝐴, 0)) “
(ℤ≥‘(𝑁 + 1))) = {0}) |
46 | 40 | adantr 480 |
. . . 4
⊢ (((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ0)
∧ 𝐴 ≠ 0) →
𝐹 = (𝑧 ∈ ℂ ↦ Σ𝑘 ∈ (0...𝑁)(((𝑛 ∈ ℕ0 ↦ if(𝑛 = 𝑁, 𝐴, 0))‘𝑘) · (𝑧↑𝑘)))) |
47 | | iftrue 4042 |
. . . . . . . 8
⊢ (𝑛 = 𝑁 → if(𝑛 = 𝑁, 𝐴, 0) = 𝐴) |
48 | 47, 11 | fvmptg 6189 |
. . . . . . 7
⊢ ((𝑁 ∈ ℕ0
∧ 𝐴 ∈ ℂ)
→ ((𝑛 ∈
ℕ0 ↦ if(𝑛 = 𝑁, 𝐴, 0))‘𝑁) = 𝐴) |
49 | 48 | ancoms 468 |
. . . . . 6
⊢ ((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ0)
→ ((𝑛 ∈
ℕ0 ↦ if(𝑛 = 𝑁, 𝐴, 0))‘𝑁) = 𝐴) |
50 | 49 | neeq1d 2841 |
. . . . 5
⊢ ((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ0)
→ (((𝑛 ∈
ℕ0 ↦ if(𝑛 = 𝑁, 𝐴, 0))‘𝑁) ≠ 0 ↔ 𝐴 ≠ 0)) |
51 | 50 | biimpar 501 |
. . . 4
⊢ (((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ0)
∧ 𝐴 ≠ 0) →
((𝑛 ∈
ℕ0 ↦ if(𝑛 = 𝑁, 𝐴, 0))‘𝑁) ≠ 0) |
52 | 42, 43, 44, 45, 46, 51 | dgreq 23804 |
. . 3
⊢ (((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ0)
∧ 𝐴 ≠ 0) →
(deg‘𝐹) = 𝑁) |
53 | 52 | ex 449 |
. 2
⊢ ((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ0)
→ (𝐴 ≠ 0 →
(deg‘𝐹) = 𝑁)) |
54 | 41, 53 | jca 553 |
1
⊢ ((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ0)
→ ((coeff‘𝐹) =
(𝑛 ∈
ℕ0 ↦ if(𝑛 = 𝑁, 𝐴, 0)) ∧ (𝐴 ≠ 0 → (deg‘𝐹) = 𝑁))) |