Proof of Theorem ply1termlem
Step | Hyp | Ref
| Expression |
1 | | simplr 788 |
. . . . . . 7
⊢ (((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ0)
∧ 𝑧 ∈ ℂ)
→ 𝑁 ∈
ℕ0) |
2 | | nn0uz 11598 |
. . . . . . 7
⊢
ℕ0 = (ℤ≥‘0) |
3 | 1, 2 | syl6eleq 2698 |
. . . . . 6
⊢ (((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ0)
∧ 𝑧 ∈ ℂ)
→ 𝑁 ∈
(ℤ≥‘0)) |
4 | | fzss1 12251 |
. . . . . 6
⊢ (𝑁 ∈
(ℤ≥‘0) → (𝑁...𝑁) ⊆ (0...𝑁)) |
5 | 3, 4 | syl 17 |
. . . . 5
⊢ (((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ0)
∧ 𝑧 ∈ ℂ)
→ (𝑁...𝑁) ⊆ (0...𝑁)) |
6 | | elfz1eq 12223 |
. . . . . . . . 9
⊢ (𝑘 ∈ (𝑁...𝑁) → 𝑘 = 𝑁) |
7 | 6 | adantl 481 |
. . . . . . . 8
⊢ ((((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ0)
∧ 𝑧 ∈ ℂ)
∧ 𝑘 ∈ (𝑁...𝑁)) → 𝑘 = 𝑁) |
8 | | iftrue 4042 |
. . . . . . . 8
⊢ (𝑘 = 𝑁 → if(𝑘 = 𝑁, 𝐴, 0) = 𝐴) |
9 | 7, 8 | syl 17 |
. . . . . . 7
⊢ ((((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ0)
∧ 𝑧 ∈ ℂ)
∧ 𝑘 ∈ (𝑁...𝑁)) → if(𝑘 = 𝑁, 𝐴, 0) = 𝐴) |
10 | | simpll 786 |
. . . . . . . 8
⊢ (((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ0)
∧ 𝑧 ∈ ℂ)
→ 𝐴 ∈
ℂ) |
11 | 10 | adantr 480 |
. . . . . . 7
⊢ ((((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ0)
∧ 𝑧 ∈ ℂ)
∧ 𝑘 ∈ (𝑁...𝑁)) → 𝐴 ∈ ℂ) |
12 | 9, 11 | eqeltrd 2688 |
. . . . . 6
⊢ ((((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ0)
∧ 𝑧 ∈ ℂ)
∧ 𝑘 ∈ (𝑁...𝑁)) → if(𝑘 = 𝑁, 𝐴, 0) ∈ ℂ) |
13 | | simplr 788 |
. . . . . . 7
⊢ ((((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ0)
∧ 𝑧 ∈ ℂ)
∧ 𝑘 ∈ (𝑁...𝑁)) → 𝑧 ∈ ℂ) |
14 | 1 | adantr 480 |
. . . . . . . 8
⊢ ((((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ0)
∧ 𝑧 ∈ ℂ)
∧ 𝑘 ∈ (𝑁...𝑁)) → 𝑁 ∈
ℕ0) |
15 | 7, 14 | eqeltrd 2688 |
. . . . . . 7
⊢ ((((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ0)
∧ 𝑧 ∈ ℂ)
∧ 𝑘 ∈ (𝑁...𝑁)) → 𝑘 ∈ ℕ0) |
16 | 13, 15 | expcld 12870 |
. . . . . 6
⊢ ((((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ0)
∧ 𝑧 ∈ ℂ)
∧ 𝑘 ∈ (𝑁...𝑁)) → (𝑧↑𝑘) ∈ ℂ) |
17 | 12, 16 | mulcld 9939 |
. . . . 5
⊢ ((((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ0)
∧ 𝑧 ∈ ℂ)
∧ 𝑘 ∈ (𝑁...𝑁)) → (if(𝑘 = 𝑁, 𝐴, 0) · (𝑧↑𝑘)) ∈ ℂ) |
18 | | eldifn 3695 |
. . . . . . . . . 10
⊢ (𝑘 ∈ ((0...𝑁) ∖ (𝑁...𝑁)) → ¬ 𝑘 ∈ (𝑁...𝑁)) |
19 | 18 | adantl 481 |
. . . . . . . . 9
⊢ ((((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ0)
∧ 𝑧 ∈ ℂ)
∧ 𝑘 ∈ ((0...𝑁) ∖ (𝑁...𝑁))) → ¬ 𝑘 ∈ (𝑁...𝑁)) |
20 | 1 | adantr 480 |
. . . . . . . . . . 11
⊢ ((((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ0)
∧ 𝑧 ∈ ℂ)
∧ 𝑘 ∈ ((0...𝑁) ∖ (𝑁...𝑁))) → 𝑁 ∈
ℕ0) |
21 | 20 | nn0zd 11356 |
. . . . . . . . . 10
⊢ ((((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ0)
∧ 𝑧 ∈ ℂ)
∧ 𝑘 ∈ ((0...𝑁) ∖ (𝑁...𝑁))) → 𝑁 ∈ ℤ) |
22 | | fzsn 12254 |
. . . . . . . . . . . 12
⊢ (𝑁 ∈ ℤ → (𝑁...𝑁) = {𝑁}) |
23 | 22 | eleq2d 2673 |
. . . . . . . . . . 11
⊢ (𝑁 ∈ ℤ → (𝑘 ∈ (𝑁...𝑁) ↔ 𝑘 ∈ {𝑁})) |
24 | | elsn2g 4157 |
. . . . . . . . . . 11
⊢ (𝑁 ∈ ℤ → (𝑘 ∈ {𝑁} ↔ 𝑘 = 𝑁)) |
25 | 23, 24 | bitrd 267 |
. . . . . . . . . 10
⊢ (𝑁 ∈ ℤ → (𝑘 ∈ (𝑁...𝑁) ↔ 𝑘 = 𝑁)) |
26 | 21, 25 | syl 17 |
. . . . . . . . 9
⊢ ((((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ0)
∧ 𝑧 ∈ ℂ)
∧ 𝑘 ∈ ((0...𝑁) ∖ (𝑁...𝑁))) → (𝑘 ∈ (𝑁...𝑁) ↔ 𝑘 = 𝑁)) |
27 | 19, 26 | mtbid 313 |
. . . . . . . 8
⊢ ((((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ0)
∧ 𝑧 ∈ ℂ)
∧ 𝑘 ∈ ((0...𝑁) ∖ (𝑁...𝑁))) → ¬ 𝑘 = 𝑁) |
28 | 27 | iffalsed 4047 |
. . . . . . 7
⊢ ((((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ0)
∧ 𝑧 ∈ ℂ)
∧ 𝑘 ∈ ((0...𝑁) ∖ (𝑁...𝑁))) → if(𝑘 = 𝑁, 𝐴, 0) = 0) |
29 | 28 | oveq1d 6564 |
. . . . . 6
⊢ ((((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ0)
∧ 𝑧 ∈ ℂ)
∧ 𝑘 ∈ ((0...𝑁) ∖ (𝑁...𝑁))) → (if(𝑘 = 𝑁, 𝐴, 0) · (𝑧↑𝑘)) = (0 · (𝑧↑𝑘))) |
30 | | simpr 476 |
. . . . . . . 8
⊢ (((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ0)
∧ 𝑧 ∈ ℂ)
→ 𝑧 ∈
ℂ) |
31 | | eldifi 3694 |
. . . . . . . . 9
⊢ (𝑘 ∈ ((0...𝑁) ∖ (𝑁...𝑁)) → 𝑘 ∈ (0...𝑁)) |
32 | | elfznn0 12302 |
. . . . . . . . 9
⊢ (𝑘 ∈ (0...𝑁) → 𝑘 ∈ ℕ0) |
33 | 31, 32 | syl 17 |
. . . . . . . 8
⊢ (𝑘 ∈ ((0...𝑁) ∖ (𝑁...𝑁)) → 𝑘 ∈ ℕ0) |
34 | | expcl 12740 |
. . . . . . . 8
⊢ ((𝑧 ∈ ℂ ∧ 𝑘 ∈ ℕ0)
→ (𝑧↑𝑘) ∈
ℂ) |
35 | 30, 33, 34 | syl2an 493 |
. . . . . . 7
⊢ ((((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ0)
∧ 𝑧 ∈ ℂ)
∧ 𝑘 ∈ ((0...𝑁) ∖ (𝑁...𝑁))) → (𝑧↑𝑘) ∈ ℂ) |
36 | 35 | mul02d 10113 |
. . . . . 6
⊢ ((((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ0)
∧ 𝑧 ∈ ℂ)
∧ 𝑘 ∈ ((0...𝑁) ∖ (𝑁...𝑁))) → (0 · (𝑧↑𝑘)) = 0) |
37 | 29, 36 | eqtrd 2644 |
. . . . 5
⊢ ((((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ0)
∧ 𝑧 ∈ ℂ)
∧ 𝑘 ∈ ((0...𝑁) ∖ (𝑁...𝑁))) → (if(𝑘 = 𝑁, 𝐴, 0) · (𝑧↑𝑘)) = 0) |
38 | | fzfid 12634 |
. . . . 5
⊢ (((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ0)
∧ 𝑧 ∈ ℂ)
→ (0...𝑁) ∈
Fin) |
39 | 5, 17, 37, 38 | fsumss 14303 |
. . . 4
⊢ (((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ0)
∧ 𝑧 ∈ ℂ)
→ Σ𝑘 ∈
(𝑁...𝑁)(if(𝑘 = 𝑁, 𝐴, 0) · (𝑧↑𝑘)) = Σ𝑘 ∈ (0...𝑁)(if(𝑘 = 𝑁, 𝐴, 0) · (𝑧↑𝑘))) |
40 | 1 | nn0zd 11356 |
. . . . 5
⊢ (((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ0)
∧ 𝑧 ∈ ℂ)
→ 𝑁 ∈
ℤ) |
41 | 30, 1 | expcld 12870 |
. . . . . 6
⊢ (((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ0)
∧ 𝑧 ∈ ℂ)
→ (𝑧↑𝑁) ∈
ℂ) |
42 | 10, 41 | mulcld 9939 |
. . . . 5
⊢ (((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ0)
∧ 𝑧 ∈ ℂ)
→ (𝐴 · (𝑧↑𝑁)) ∈ ℂ) |
43 | | oveq2 6557 |
. . . . . . 7
⊢ (𝑘 = 𝑁 → (𝑧↑𝑘) = (𝑧↑𝑁)) |
44 | 8, 43 | oveq12d 6567 |
. . . . . 6
⊢ (𝑘 = 𝑁 → (if(𝑘 = 𝑁, 𝐴, 0) · (𝑧↑𝑘)) = (𝐴 · (𝑧↑𝑁))) |
45 | 44 | fsum1 14320 |
. . . . 5
⊢ ((𝑁 ∈ ℤ ∧ (𝐴 · (𝑧↑𝑁)) ∈ ℂ) → Σ𝑘 ∈ (𝑁...𝑁)(if(𝑘 = 𝑁, 𝐴, 0) · (𝑧↑𝑘)) = (𝐴 · (𝑧↑𝑁))) |
46 | 40, 42, 45 | syl2anc 691 |
. . . 4
⊢ (((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ0)
∧ 𝑧 ∈ ℂ)
→ Σ𝑘 ∈
(𝑁...𝑁)(if(𝑘 = 𝑁, 𝐴, 0) · (𝑧↑𝑘)) = (𝐴 · (𝑧↑𝑁))) |
47 | 39, 46 | eqtr3d 2646 |
. . 3
⊢ (((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ0)
∧ 𝑧 ∈ ℂ)
→ Σ𝑘 ∈
(0...𝑁)(if(𝑘 = 𝑁, 𝐴, 0) · (𝑧↑𝑘)) = (𝐴 · (𝑧↑𝑁))) |
48 | 47 | mpteq2dva 4672 |
. 2
⊢ ((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ0)
→ (𝑧 ∈ ℂ
↦ Σ𝑘 ∈
(0...𝑁)(if(𝑘 = 𝑁, 𝐴, 0) · (𝑧↑𝑘))) = (𝑧 ∈ ℂ ↦ (𝐴 · (𝑧↑𝑁)))) |
49 | | ply1term.1 |
. 2
⊢ 𝐹 = (𝑧 ∈ ℂ ↦ (𝐴 · (𝑧↑𝑁))) |
50 | 48, 49 | syl6reqr 2663 |
1
⊢ ((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ0)
→ 𝐹 = (𝑧 ∈ ℂ ↦
Σ𝑘 ∈ (0...𝑁)(if(𝑘 = 𝑁, 𝐴, 0) · (𝑧↑𝑘)))) |