Step | Hyp | Ref
| Expression |
1 | | pwp1fsum.a |
. . . 4
⊢ (𝜑 → 𝐴 ∈ ℂ) |
2 | | 1cnd 9935 |
. . . 4
⊢ (𝜑 → 1 ∈
ℂ) |
3 | | fzfid 12634 |
. . . . 5
⊢ (𝜑 → (0...(𝑁 − 1)) ∈ Fin) |
4 | | neg1cn 11001 |
. . . . . . . 8
⊢ -1 ∈
ℂ |
5 | 4 | a1i 11 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑘 ∈ (0...(𝑁 − 1))) → -1 ∈
ℂ) |
6 | | elfznn0 12302 |
. . . . . . . 8
⊢ (𝑘 ∈ (0...(𝑁 − 1)) → 𝑘 ∈ ℕ0) |
7 | 6 | adantl 481 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑘 ∈ (0...(𝑁 − 1))) → 𝑘 ∈ ℕ0) |
8 | 5, 7 | expcld 12870 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑘 ∈ (0...(𝑁 − 1))) → (-1↑𝑘) ∈
ℂ) |
9 | 1 | adantr 480 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑘 ∈ (0...(𝑁 − 1))) → 𝐴 ∈ ℂ) |
10 | 9, 7 | expcld 12870 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑘 ∈ (0...(𝑁 − 1))) → (𝐴↑𝑘) ∈ ℂ) |
11 | 8, 10 | mulcld 9939 |
. . . . 5
⊢ ((𝜑 ∧ 𝑘 ∈ (0...(𝑁 − 1))) → ((-1↑𝑘) · (𝐴↑𝑘)) ∈ ℂ) |
12 | 3, 11 | fsumcl 14311 |
. . . 4
⊢ (𝜑 → Σ𝑘 ∈ (0...(𝑁 − 1))((-1↑𝑘) · (𝐴↑𝑘)) ∈ ℂ) |
13 | 1, 2, 12 | adddird 9944 |
. . 3
⊢ (𝜑 → ((𝐴 + 1) · Σ𝑘 ∈ (0...(𝑁 − 1))((-1↑𝑘) · (𝐴↑𝑘))) = ((𝐴 · Σ𝑘 ∈ (0...(𝑁 − 1))((-1↑𝑘) · (𝐴↑𝑘))) + (1 · Σ𝑘 ∈ (0...(𝑁 − 1))((-1↑𝑘) · (𝐴↑𝑘))))) |
14 | 3, 1, 11 | fsummulc2 14358 |
. . . . 5
⊢ (𝜑 → (𝐴 · Σ𝑘 ∈ (0...(𝑁 − 1))((-1↑𝑘) · (𝐴↑𝑘))) = Σ𝑘 ∈ (0...(𝑁 − 1))(𝐴 · ((-1↑𝑘) · (𝐴↑𝑘)))) |
15 | 9, 11 | mulcomd 9940 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑘 ∈ (0...(𝑁 − 1))) → (𝐴 · ((-1↑𝑘) · (𝐴↑𝑘))) = (((-1↑𝑘) · (𝐴↑𝑘)) · 𝐴)) |
16 | 8, 10, 9 | mulassd 9942 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑘 ∈ (0...(𝑁 − 1))) → (((-1↑𝑘) · (𝐴↑𝑘)) · 𝐴) = ((-1↑𝑘) · ((𝐴↑𝑘) · 𝐴))) |
17 | | expp1 12729 |
. . . . . . . . . . 11
⊢ ((𝐴 ∈ ℂ ∧ 𝑘 ∈ ℕ0)
→ (𝐴↑(𝑘 + 1)) = ((𝐴↑𝑘) · 𝐴)) |
18 | 1, 6, 17 | syl2an 493 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑘 ∈ (0...(𝑁 − 1))) → (𝐴↑(𝑘 + 1)) = ((𝐴↑𝑘) · 𝐴)) |
19 | 18 | eqcomd 2616 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑘 ∈ (0...(𝑁 − 1))) → ((𝐴↑𝑘) · 𝐴) = (𝐴↑(𝑘 + 1))) |
20 | 19 | oveq2d 6565 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑘 ∈ (0...(𝑁 − 1))) → ((-1↑𝑘) · ((𝐴↑𝑘) · 𝐴)) = ((-1↑𝑘) · (𝐴↑(𝑘 + 1)))) |
21 | 15, 16, 20 | 3eqtrd 2648 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑘 ∈ (0...(𝑁 − 1))) → (𝐴 · ((-1↑𝑘) · (𝐴↑𝑘))) = ((-1↑𝑘) · (𝐴↑(𝑘 + 1)))) |
22 | 21 | ralrimiva 2949 |
. . . . . 6
⊢ (𝜑 → ∀𝑘 ∈ (0...(𝑁 − 1))(𝐴 · ((-1↑𝑘) · (𝐴↑𝑘))) = ((-1↑𝑘) · (𝐴↑(𝑘 + 1)))) |
23 | 22 | sumeq2d 14280 |
. . . . 5
⊢ (𝜑 → Σ𝑘 ∈ (0...(𝑁 − 1))(𝐴 · ((-1↑𝑘) · (𝐴↑𝑘))) = Σ𝑘 ∈ (0...(𝑁 − 1))((-1↑𝑘) · (𝐴↑(𝑘 + 1)))) |
24 | 14, 23 | eqtrd 2644 |
. . . 4
⊢ (𝜑 → (𝐴 · Σ𝑘 ∈ (0...(𝑁 − 1))((-1↑𝑘) · (𝐴↑𝑘))) = Σ𝑘 ∈ (0...(𝑁 − 1))((-1↑𝑘) · (𝐴↑(𝑘 + 1)))) |
25 | 12 | mulid2d 9937 |
. . . 4
⊢ (𝜑 → (1 · Σ𝑘 ∈ (0...(𝑁 − 1))((-1↑𝑘) · (𝐴↑𝑘))) = Σ𝑘 ∈ (0...(𝑁 − 1))((-1↑𝑘) · (𝐴↑𝑘))) |
26 | 24, 25 | oveq12d 6567 |
. . 3
⊢ (𝜑 → ((𝐴 · Σ𝑘 ∈ (0...(𝑁 − 1))((-1↑𝑘) · (𝐴↑𝑘))) + (1 · Σ𝑘 ∈ (0...(𝑁 − 1))((-1↑𝑘) · (𝐴↑𝑘)))) = (Σ𝑘 ∈ (0...(𝑁 − 1))((-1↑𝑘) · (𝐴↑(𝑘 + 1))) + Σ𝑘 ∈ (0...(𝑁 − 1))((-1↑𝑘) · (𝐴↑𝑘)))) |
27 | | 1zzd 11285 |
. . . . . . 7
⊢ (𝜑 → 1 ∈
ℤ) |
28 | | 0zd 11266 |
. . . . . . 7
⊢ (𝜑 → 0 ∈
ℤ) |
29 | | pwp1fsum.n |
. . . . . . . 8
⊢ (𝜑 → 𝑁 ∈ ℕ) |
30 | | nnz 11276 |
. . . . . . . . 9
⊢ (𝑁 ∈ ℕ → 𝑁 ∈
ℤ) |
31 | | peano2zm 11297 |
. . . . . . . . 9
⊢ (𝑁 ∈ ℤ → (𝑁 − 1) ∈
ℤ) |
32 | 30, 31 | syl 17 |
. . . . . . . 8
⊢ (𝑁 ∈ ℕ → (𝑁 − 1) ∈
ℤ) |
33 | 29, 32 | syl 17 |
. . . . . . 7
⊢ (𝜑 → (𝑁 − 1) ∈ ℤ) |
34 | | peano2nn0 11210 |
. . . . . . . . . . 11
⊢ (𝑘 ∈ ℕ0
→ (𝑘 + 1) ∈
ℕ0) |
35 | 6, 34 | syl 17 |
. . . . . . . . . 10
⊢ (𝑘 ∈ (0...(𝑁 − 1)) → (𝑘 + 1) ∈
ℕ0) |
36 | 35 | adantl 481 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑘 ∈ (0...(𝑁 − 1))) → (𝑘 + 1) ∈
ℕ0) |
37 | 9, 36 | expcld 12870 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑘 ∈ (0...(𝑁 − 1))) → (𝐴↑(𝑘 + 1)) ∈ ℂ) |
38 | 8, 37 | mulcld 9939 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑘 ∈ (0...(𝑁 − 1))) → ((-1↑𝑘) · (𝐴↑(𝑘 + 1))) ∈ ℂ) |
39 | | oveq2 6557 |
. . . . . . . 8
⊢ (𝑘 = (𝑙 − 1) → (-1↑𝑘) = (-1↑(𝑙 − 1))) |
40 | | oveq1 6556 |
. . . . . . . . 9
⊢ (𝑘 = (𝑙 − 1) → (𝑘 + 1) = ((𝑙 − 1) + 1)) |
41 | 40 | oveq2d 6565 |
. . . . . . . 8
⊢ (𝑘 = (𝑙 − 1) → (𝐴↑(𝑘 + 1)) = (𝐴↑((𝑙 − 1) + 1))) |
42 | 39, 41 | oveq12d 6567 |
. . . . . . 7
⊢ (𝑘 = (𝑙 − 1) → ((-1↑𝑘) · (𝐴↑(𝑘 + 1))) = ((-1↑(𝑙 − 1)) · (𝐴↑((𝑙 − 1) + 1)))) |
43 | 27, 28, 33, 38, 42 | fsumshft 14354 |
. . . . . 6
⊢ (𝜑 → Σ𝑘 ∈ (0...(𝑁 − 1))((-1↑𝑘) · (𝐴↑(𝑘 + 1))) = Σ𝑙 ∈ ((0 + 1)...((𝑁 − 1) + 1))((-1↑(𝑙 − 1)) · (𝐴↑((𝑙 − 1) + 1)))) |
44 | | elfzelz 12213 |
. . . . . . . . . . . . 13
⊢ (𝑙 ∈ ((0 + 1)...((𝑁 − 1) + 1)) → 𝑙 ∈
ℤ) |
45 | 44 | zcnd 11359 |
. . . . . . . . . . . 12
⊢ (𝑙 ∈ ((0 + 1)...((𝑁 − 1) + 1)) → 𝑙 ∈
ℂ) |
46 | 45 | adantl 481 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑙 ∈ ((0 + 1)...((𝑁 − 1) + 1))) → 𝑙 ∈ ℂ) |
47 | | npcan1 10334 |
. . . . . . . . . . 11
⊢ (𝑙 ∈ ℂ → ((𝑙 − 1) + 1) = 𝑙) |
48 | 46, 47 | syl 17 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑙 ∈ ((0 + 1)...((𝑁 − 1) + 1))) → ((𝑙 − 1) + 1) = 𝑙) |
49 | 48 | oveq2d 6565 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑙 ∈ ((0 + 1)...((𝑁 − 1) + 1))) → (𝐴↑((𝑙 − 1) + 1)) = (𝐴↑𝑙)) |
50 | 49 | oveq2d 6565 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑙 ∈ ((0 + 1)...((𝑁 − 1) + 1))) → ((-1↑(𝑙 − 1)) · (𝐴↑((𝑙 − 1) + 1))) = ((-1↑(𝑙 − 1)) · (𝐴↑𝑙))) |
51 | 50 | ralrimiva 2949 |
. . . . . . 7
⊢ (𝜑 → ∀𝑙 ∈ ((0 + 1)...((𝑁 − 1) + 1))((-1↑(𝑙 − 1)) · (𝐴↑((𝑙 − 1) + 1))) = ((-1↑(𝑙 − 1)) · (𝐴↑𝑙))) |
52 | 51 | sumeq2d 14280 |
. . . . . 6
⊢ (𝜑 → Σ𝑙 ∈ ((0 + 1)...((𝑁 − 1) + 1))((-1↑(𝑙 − 1)) · (𝐴↑((𝑙 − 1) + 1))) = Σ𝑙 ∈ ((0 + 1)...((𝑁 − 1) +
1))((-1↑(𝑙 − 1))
· (𝐴↑𝑙))) |
53 | 29 | nncnd 10913 |
. . . . . . . . . 10
⊢ (𝜑 → 𝑁 ∈ ℂ) |
54 | | npcan1 10334 |
. . . . . . . . . 10
⊢ (𝑁 ∈ ℂ → ((𝑁 − 1) + 1) = 𝑁) |
55 | 53, 54 | syl 17 |
. . . . . . . . 9
⊢ (𝜑 → ((𝑁 − 1) + 1) = 𝑁) |
56 | | 0p1e1 11009 |
. . . . . . . . . . . 12
⊢ (0 + 1) =
1 |
57 | 56 | fveq2i 6106 |
. . . . . . . . . . 11
⊢
(ℤ≥‘(0 + 1)) =
(ℤ≥‘1) |
58 | | nnuz 11599 |
. . . . . . . . . . 11
⊢ ℕ =
(ℤ≥‘1) |
59 | 57, 58 | eqtr4i 2635 |
. . . . . . . . . 10
⊢
(ℤ≥‘(0 + 1)) = ℕ |
60 | 59 | a1i 11 |
. . . . . . . . 9
⊢ (𝜑 →
(ℤ≥‘(0 + 1)) = ℕ) |
61 | 29, 55, 60 | 3eltr4d 2703 |
. . . . . . . 8
⊢ (𝜑 → ((𝑁 − 1) + 1) ∈
(ℤ≥‘(0 + 1))) |
62 | 56 | oveq1i 6559 |
. . . . . . . . . . 11
⊢ ((0 +
1)...((𝑁 − 1) + 1)) =
(1...((𝑁 − 1) +
1)) |
63 | 62 | eleq2i 2680 |
. . . . . . . . . 10
⊢ (𝑙 ∈ ((0 + 1)...((𝑁 − 1) + 1)) ↔ 𝑙 ∈ (1...((𝑁 − 1) + 1))) |
64 | | elfznn 12241 |
. . . . . . . . . . . 12
⊢ (𝑙 ∈ (1...((𝑁 − 1) + 1)) → 𝑙 ∈ ℕ) |
65 | 4 | a1i 11 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑙 ∈ ℕ) → -1 ∈
ℂ) |
66 | | nnm1nn0 11211 |
. . . . . . . . . . . . . . . 16
⊢ (𝑙 ∈ ℕ → (𝑙 − 1) ∈
ℕ0) |
67 | 66 | adantl 481 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑙 ∈ ℕ) → (𝑙 − 1) ∈
ℕ0) |
68 | 65, 67 | expcld 12870 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑙 ∈ ℕ) → (-1↑(𝑙 − 1)) ∈
ℂ) |
69 | 1 | adantr 480 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑙 ∈ ℕ) → 𝐴 ∈ ℂ) |
70 | | nnnn0 11176 |
. . . . . . . . . . . . . . . 16
⊢ (𝑙 ∈ ℕ → 𝑙 ∈
ℕ0) |
71 | 70 | adantl 481 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑙 ∈ ℕ) → 𝑙 ∈ ℕ0) |
72 | 69, 71 | expcld 12870 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑙 ∈ ℕ) → (𝐴↑𝑙) ∈ ℂ) |
73 | 68, 72 | mulcld 9939 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑙 ∈ ℕ) → ((-1↑(𝑙 − 1)) · (𝐴↑𝑙)) ∈ ℂ) |
74 | 73 | expcom 450 |
. . . . . . . . . . . 12
⊢ (𝑙 ∈ ℕ → (𝜑 → ((-1↑(𝑙 − 1)) · (𝐴↑𝑙)) ∈ ℂ)) |
75 | 64, 74 | syl 17 |
. . . . . . . . . . 11
⊢ (𝑙 ∈ (1...((𝑁 − 1) + 1)) → (𝜑 → ((-1↑(𝑙 − 1)) · (𝐴↑𝑙)) ∈ ℂ)) |
76 | 75 | com12 32 |
. . . . . . . . . 10
⊢ (𝜑 → (𝑙 ∈ (1...((𝑁 − 1) + 1)) → ((-1↑(𝑙 − 1)) · (𝐴↑𝑙)) ∈ ℂ)) |
77 | 63, 76 | syl5bi 231 |
. . . . . . . . 9
⊢ (𝜑 → (𝑙 ∈ ((0 + 1)...((𝑁 − 1) + 1)) → ((-1↑(𝑙 − 1)) · (𝐴↑𝑙)) ∈ ℂ)) |
78 | 77 | imp 444 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑙 ∈ ((0 + 1)...((𝑁 − 1) + 1))) → ((-1↑(𝑙 − 1)) · (𝐴↑𝑙)) ∈ ℂ) |
79 | | oveq1 6556 |
. . . . . . . . . 10
⊢ (𝑙 = ((𝑁 − 1) + 1) → (𝑙 − 1) = (((𝑁 − 1) + 1) −
1)) |
80 | 79 | oveq2d 6565 |
. . . . . . . . 9
⊢ (𝑙 = ((𝑁 − 1) + 1) → (-1↑(𝑙 − 1)) = (-1↑(((𝑁 − 1) + 1) −
1))) |
81 | | oveq2 6557 |
. . . . . . . . 9
⊢ (𝑙 = ((𝑁 − 1) + 1) → (𝐴↑𝑙) = (𝐴↑((𝑁 − 1) + 1))) |
82 | 80, 81 | oveq12d 6567 |
. . . . . . . 8
⊢ (𝑙 = ((𝑁 − 1) + 1) → ((-1↑(𝑙 − 1)) · (𝐴↑𝑙)) = ((-1↑(((𝑁 − 1) + 1) − 1)) · (𝐴↑((𝑁 − 1) + 1)))) |
83 | 61, 78, 82 | fsumm1 14324 |
. . . . . . 7
⊢ (𝜑 → Σ𝑙 ∈ ((0 + 1)...((𝑁 − 1) + 1))((-1↑(𝑙 − 1)) · (𝐴↑𝑙)) = (Σ𝑙 ∈ ((0 + 1)...(((𝑁 − 1) + 1) − 1))((-1↑(𝑙 − 1)) · (𝐴↑𝑙)) + ((-1↑(((𝑁 − 1) + 1) − 1)) · (𝐴↑((𝑁 − 1) + 1))))) |
84 | 33 | zcnd 11359 |
. . . . . . . . . . . 12
⊢ (𝜑 → (𝑁 − 1) ∈ ℂ) |
85 | | pncan1 10333 |
. . . . . . . . . . . 12
⊢ ((𝑁 − 1) ∈ ℂ
→ (((𝑁 − 1) + 1)
− 1) = (𝑁 −
1)) |
86 | 84, 85 | syl 17 |
. . . . . . . . . . 11
⊢ (𝜑 → (((𝑁 − 1) + 1) − 1) = (𝑁 − 1)) |
87 | 86 | oveq2d 6565 |
. . . . . . . . . 10
⊢ (𝜑 → ((0 + 1)...(((𝑁 − 1) + 1) − 1)) =
((0 + 1)...(𝑁 −
1))) |
88 | 87 | sumeq1d 14279 |
. . . . . . . . 9
⊢ (𝜑 → Σ𝑙 ∈ ((0 + 1)...(((𝑁 − 1) + 1) − 1))((-1↑(𝑙 − 1)) · (𝐴↑𝑙)) = Σ𝑙 ∈ ((0 + 1)...(𝑁 − 1))((-1↑(𝑙 − 1)) · (𝐴↑𝑙))) |
89 | | oveq1 6556 |
. . . . . . . . . . . 12
⊢ (𝑙 = 𝑘 → (𝑙 − 1) = (𝑘 − 1)) |
90 | 89 | oveq2d 6565 |
. . . . . . . . . . 11
⊢ (𝑙 = 𝑘 → (-1↑(𝑙 − 1)) = (-1↑(𝑘 − 1))) |
91 | | oveq2 6557 |
. . . . . . . . . . 11
⊢ (𝑙 = 𝑘 → (𝐴↑𝑙) = (𝐴↑𝑘)) |
92 | 90, 91 | oveq12d 6567 |
. . . . . . . . . 10
⊢ (𝑙 = 𝑘 → ((-1↑(𝑙 − 1)) · (𝐴↑𝑙)) = ((-1↑(𝑘 − 1)) · (𝐴↑𝑘))) |
93 | 92 | cbvsumv 14274 |
. . . . . . . . 9
⊢
Σ𝑙 ∈ ((0
+ 1)...(𝑁 −
1))((-1↑(𝑙 − 1))
· (𝐴↑𝑙)) = Σ𝑘 ∈ ((0 + 1)...(𝑁 − 1))((-1↑(𝑘 − 1)) · (𝐴↑𝑘)) |
94 | 88, 93 | syl6eq 2660 |
. . . . . . . 8
⊢ (𝜑 → Σ𝑙 ∈ ((0 + 1)...(((𝑁 − 1) + 1) − 1))((-1↑(𝑙 − 1)) · (𝐴↑𝑙)) = Σ𝑘 ∈ ((0 + 1)...(𝑁 − 1))((-1↑(𝑘 − 1)) · (𝐴↑𝑘))) |
95 | 86 | oveq2d 6565 |
. . . . . . . . 9
⊢ (𝜑 → (-1↑(((𝑁 − 1) + 1) − 1)) =
(-1↑(𝑁 −
1))) |
96 | 55 | oveq2d 6565 |
. . . . . . . . 9
⊢ (𝜑 → (𝐴↑((𝑁 − 1) + 1)) = (𝐴↑𝑁)) |
97 | 95, 96 | oveq12d 6567 |
. . . . . . . 8
⊢ (𝜑 → ((-1↑(((𝑁 − 1) + 1) − 1))
· (𝐴↑((𝑁 − 1) + 1))) =
((-1↑(𝑁 − 1))
· (𝐴↑𝑁))) |
98 | 94, 97 | oveq12d 6567 |
. . . . . . 7
⊢ (𝜑 → (Σ𝑙 ∈ ((0 + 1)...(((𝑁 − 1) + 1) − 1))((-1↑(𝑙 − 1)) · (𝐴↑𝑙)) + ((-1↑(((𝑁 − 1) + 1) − 1)) · (𝐴↑((𝑁 − 1) + 1)))) = (Σ𝑘 ∈ ((0 + 1)...(𝑁 − 1))((-1↑(𝑘 − 1)) · (𝐴↑𝑘)) + ((-1↑(𝑁 − 1)) · (𝐴↑𝑁)))) |
99 | 83, 98 | eqtrd 2644 |
. . . . . 6
⊢ (𝜑 → Σ𝑙 ∈ ((0 + 1)...((𝑁 − 1) + 1))((-1↑(𝑙 − 1)) · (𝐴↑𝑙)) = (Σ𝑘 ∈ ((0 + 1)...(𝑁 − 1))((-1↑(𝑘 − 1)) · (𝐴↑𝑘)) + ((-1↑(𝑁 − 1)) · (𝐴↑𝑁)))) |
100 | 43, 52, 99 | 3eqtrd 2648 |
. . . . 5
⊢ (𝜑 → Σ𝑘 ∈ (0...(𝑁 − 1))((-1↑𝑘) · (𝐴↑(𝑘 + 1))) = (Σ𝑘 ∈ ((0 + 1)...(𝑁 − 1))((-1↑(𝑘 − 1)) · (𝐴↑𝑘)) + ((-1↑(𝑁 − 1)) · (𝐴↑𝑁)))) |
101 | | nnm1nn0 11211 |
. . . . . . . . 9
⊢ (𝑁 ∈ ℕ → (𝑁 − 1) ∈
ℕ0) |
102 | | elnn0uz 11601 |
. . . . . . . . 9
⊢ ((𝑁 − 1) ∈
ℕ0 ↔ (𝑁 − 1) ∈
(ℤ≥‘0)) |
103 | 101, 102 | sylib 207 |
. . . . . . . 8
⊢ (𝑁 ∈ ℕ → (𝑁 − 1) ∈
(ℤ≥‘0)) |
104 | 29, 103 | syl 17 |
. . . . . . 7
⊢ (𝜑 → (𝑁 − 1) ∈
(ℤ≥‘0)) |
105 | | oveq2 6557 |
. . . . . . . . 9
⊢ (𝑘 = 0 → (-1↑𝑘) =
(-1↑0)) |
106 | | exp0 12726 |
. . . . . . . . . 10
⊢ (-1
∈ ℂ → (-1↑0) = 1) |
107 | 4, 106 | ax-mp 5 |
. . . . . . . . 9
⊢
(-1↑0) = 1 |
108 | 105, 107 | syl6eq 2660 |
. . . . . . . 8
⊢ (𝑘 = 0 → (-1↑𝑘) = 1) |
109 | | oveq2 6557 |
. . . . . . . 8
⊢ (𝑘 = 0 → (𝐴↑𝑘) = (𝐴↑0)) |
110 | 108, 109 | oveq12d 6567 |
. . . . . . 7
⊢ (𝑘 = 0 → ((-1↑𝑘) · (𝐴↑𝑘)) = (1 · (𝐴↑0))) |
111 | 104, 11, 110 | fsum1p 14326 |
. . . . . 6
⊢ (𝜑 → Σ𝑘 ∈ (0...(𝑁 − 1))((-1↑𝑘) · (𝐴↑𝑘)) = ((1 · (𝐴↑0)) + Σ𝑘 ∈ ((0 + 1)...(𝑁 − 1))((-1↑𝑘) · (𝐴↑𝑘)))) |
112 | | exp0 12726 |
. . . . . . . . . 10
⊢ (𝐴 ∈ ℂ → (𝐴↑0) = 1) |
113 | 1, 112 | syl 17 |
. . . . . . . . 9
⊢ (𝜑 → (𝐴↑0) = 1) |
114 | 113 | oveq2d 6565 |
. . . . . . . 8
⊢ (𝜑 → (1 · (𝐴↑0)) = (1 ·
1)) |
115 | | 1t1e1 11052 |
. . . . . . . 8
⊢ (1
· 1) = 1 |
116 | 114, 115 | syl6eq 2660 |
. . . . . . 7
⊢ (𝜑 → (1 · (𝐴↑0)) = 1) |
117 | 116 | oveq1d 6564 |
. . . . . 6
⊢ (𝜑 → ((1 · (𝐴↑0)) + Σ𝑘 ∈ ((0 + 1)...(𝑁 − 1))((-1↑𝑘) · (𝐴↑𝑘))) = (1 + Σ𝑘 ∈ ((0 + 1)...(𝑁 − 1))((-1↑𝑘) · (𝐴↑𝑘)))) |
118 | | fzfid 12634 |
. . . . . . . 8
⊢ (𝜑 → ((0 + 1)...(𝑁 − 1)) ∈
Fin) |
119 | | elfznn 12241 |
. . . . . . . . . . 11
⊢ (𝑘 ∈ (1...(𝑁 − 1)) → 𝑘 ∈ ℕ) |
120 | 4 | a1i 11 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → -1 ∈
ℂ) |
121 | | nnnn0 11176 |
. . . . . . . . . . . . . . 15
⊢ (𝑘 ∈ ℕ → 𝑘 ∈
ℕ0) |
122 | 121 | adantl 481 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → 𝑘 ∈ ℕ0) |
123 | 120, 122 | expcld 12870 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (-1↑𝑘) ∈
ℂ) |
124 | 1 | adantr 480 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → 𝐴 ∈ ℂ) |
125 | 124, 122 | expcld 12870 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (𝐴↑𝑘) ∈ ℂ) |
126 | 123, 125 | mulcld 9939 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → ((-1↑𝑘) · (𝐴↑𝑘)) ∈ ℂ) |
127 | 126 | expcom 450 |
. . . . . . . . . . 11
⊢ (𝑘 ∈ ℕ → (𝜑 → ((-1↑𝑘) · (𝐴↑𝑘)) ∈ ℂ)) |
128 | 119, 127 | syl 17 |
. . . . . . . . . 10
⊢ (𝑘 ∈ (1...(𝑁 − 1)) → (𝜑 → ((-1↑𝑘) · (𝐴↑𝑘)) ∈ ℂ)) |
129 | 56 | oveq1i 6559 |
. . . . . . . . . 10
⊢ ((0 +
1)...(𝑁 − 1)) =
(1...(𝑁 −
1)) |
130 | 128, 129 | eleq2s 2706 |
. . . . . . . . 9
⊢ (𝑘 ∈ ((0 + 1)...(𝑁 − 1)) → (𝜑 → ((-1↑𝑘) · (𝐴↑𝑘)) ∈ ℂ)) |
131 | 130 | impcom 445 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑘 ∈ ((0 + 1)...(𝑁 − 1))) → ((-1↑𝑘) · (𝐴↑𝑘)) ∈ ℂ) |
132 | 118, 131 | fsumcl 14311 |
. . . . . . 7
⊢ (𝜑 → Σ𝑘 ∈ ((0 + 1)...(𝑁 − 1))((-1↑𝑘) · (𝐴↑𝑘)) ∈ ℂ) |
133 | 2, 132 | addcomd 10117 |
. . . . . 6
⊢ (𝜑 → (1 + Σ𝑘 ∈ ((0 + 1)...(𝑁 − 1))((-1↑𝑘) · (𝐴↑𝑘))) = (Σ𝑘 ∈ ((0 + 1)...(𝑁 − 1))((-1↑𝑘) · (𝐴↑𝑘)) + 1)) |
134 | 111, 117,
133 | 3eqtrd 2648 |
. . . . 5
⊢ (𝜑 → Σ𝑘 ∈ (0...(𝑁 − 1))((-1↑𝑘) · (𝐴↑𝑘)) = (Σ𝑘 ∈ ((0 + 1)...(𝑁 − 1))((-1↑𝑘) · (𝐴↑𝑘)) + 1)) |
135 | 100, 134 | oveq12d 6567 |
. . . 4
⊢ (𝜑 → (Σ𝑘 ∈ (0...(𝑁 − 1))((-1↑𝑘) · (𝐴↑(𝑘 + 1))) + Σ𝑘 ∈ (0...(𝑁 − 1))((-1↑𝑘) · (𝐴↑𝑘))) = ((Σ𝑘 ∈ ((0 + 1)...(𝑁 − 1))((-1↑(𝑘 − 1)) · (𝐴↑𝑘)) + ((-1↑(𝑁 − 1)) · (𝐴↑𝑁))) + (Σ𝑘 ∈ ((0 + 1)...(𝑁 − 1))((-1↑𝑘) · (𝐴↑𝑘)) + 1))) |
136 | | nnm1nn0 11211 |
. . . . . . . . . . . . . 14
⊢ (𝑘 ∈ ℕ → (𝑘 − 1) ∈
ℕ0) |
137 | 136 | adantl 481 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (𝑘 − 1) ∈
ℕ0) |
138 | 120, 137 | expcld 12870 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (-1↑(𝑘 − 1)) ∈
ℂ) |
139 | 138, 125 | mulcld 9939 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → ((-1↑(𝑘 − 1)) · (𝐴↑𝑘)) ∈ ℂ) |
140 | 139 | expcom 450 |
. . . . . . . . . 10
⊢ (𝑘 ∈ ℕ → (𝜑 → ((-1↑(𝑘 − 1)) · (𝐴↑𝑘)) ∈ ℂ)) |
141 | 119, 140 | syl 17 |
. . . . . . . . 9
⊢ (𝑘 ∈ (1...(𝑁 − 1)) → (𝜑 → ((-1↑(𝑘 − 1)) · (𝐴↑𝑘)) ∈ ℂ)) |
142 | 141, 129 | eleq2s 2706 |
. . . . . . . 8
⊢ (𝑘 ∈ ((0 + 1)...(𝑁 − 1)) → (𝜑 → ((-1↑(𝑘 − 1)) · (𝐴↑𝑘)) ∈ ℂ)) |
143 | 142 | impcom 445 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑘 ∈ ((0 + 1)...(𝑁 − 1))) → ((-1↑(𝑘 − 1)) · (𝐴↑𝑘)) ∈ ℂ) |
144 | 118, 143 | fsumcl 14311 |
. . . . . 6
⊢ (𝜑 → Σ𝑘 ∈ ((0 + 1)...(𝑁 − 1))((-1↑(𝑘 − 1)) · (𝐴↑𝑘)) ∈ ℂ) |
145 | 4 | a1i 11 |
. . . . . . . 8
⊢ (𝜑 → -1 ∈
ℂ) |
146 | 29, 101 | syl 17 |
. . . . . . . 8
⊢ (𝜑 → (𝑁 − 1) ∈
ℕ0) |
147 | 145, 146 | expcld 12870 |
. . . . . . 7
⊢ (𝜑 → (-1↑(𝑁 − 1)) ∈
ℂ) |
148 | | nnnn0 11176 |
. . . . . . . . 9
⊢ (𝑁 ∈ ℕ → 𝑁 ∈
ℕ0) |
149 | 29, 148 | syl 17 |
. . . . . . . 8
⊢ (𝜑 → 𝑁 ∈
ℕ0) |
150 | 1, 149 | expcld 12870 |
. . . . . . 7
⊢ (𝜑 → (𝐴↑𝑁) ∈ ℂ) |
151 | 147, 150 | mulcld 9939 |
. . . . . 6
⊢ (𝜑 → ((-1↑(𝑁 − 1)) · (𝐴↑𝑁)) ∈ ℂ) |
152 | 144, 151 | addcld 9938 |
. . . . 5
⊢ (𝜑 → (Σ𝑘 ∈ ((0 + 1)...(𝑁 − 1))((-1↑(𝑘 − 1)) · (𝐴↑𝑘)) + ((-1↑(𝑁 − 1)) · (𝐴↑𝑁))) ∈ ℂ) |
153 | 152, 132,
2 | addassd 9941 |
. . . 4
⊢ (𝜑 → (((Σ𝑘 ∈ ((0 + 1)...(𝑁 − 1))((-1↑(𝑘 − 1)) · (𝐴↑𝑘)) + ((-1↑(𝑁 − 1)) · (𝐴↑𝑁))) + Σ𝑘 ∈ ((0 + 1)...(𝑁 − 1))((-1↑𝑘) · (𝐴↑𝑘))) + 1) = ((Σ𝑘 ∈ ((0 + 1)...(𝑁 − 1))((-1↑(𝑘 − 1)) · (𝐴↑𝑘)) + ((-1↑(𝑁 − 1)) · (𝐴↑𝑁))) + (Σ𝑘 ∈ ((0 + 1)...(𝑁 − 1))((-1↑𝑘) · (𝐴↑𝑘)) + 1))) |
154 | 144, 151 | addcomd 10117 |
. . . . . . 7
⊢ (𝜑 → (Σ𝑘 ∈ ((0 + 1)...(𝑁 − 1))((-1↑(𝑘 − 1)) · (𝐴↑𝑘)) + ((-1↑(𝑁 − 1)) · (𝐴↑𝑁))) = (((-1↑(𝑁 − 1)) · (𝐴↑𝑁)) + Σ𝑘 ∈ ((0 + 1)...(𝑁 − 1))((-1↑(𝑘 − 1)) · (𝐴↑𝑘)))) |
155 | 154 | oveq1d 6564 |
. . . . . 6
⊢ (𝜑 → ((Σ𝑘 ∈ ((0 + 1)...(𝑁 − 1))((-1↑(𝑘 − 1)) · (𝐴↑𝑘)) + ((-1↑(𝑁 − 1)) · (𝐴↑𝑁))) + Σ𝑘 ∈ ((0 + 1)...(𝑁 − 1))((-1↑𝑘) · (𝐴↑𝑘))) = ((((-1↑(𝑁 − 1)) · (𝐴↑𝑁)) + Σ𝑘 ∈ ((0 + 1)...(𝑁 − 1))((-1↑(𝑘 − 1)) · (𝐴↑𝑘))) + Σ𝑘 ∈ ((0 + 1)...(𝑁 − 1))((-1↑𝑘) · (𝐴↑𝑘)))) |
156 | 151, 144,
132 | addassd 9941 |
. . . . . 6
⊢ (𝜑 → ((((-1↑(𝑁 − 1)) · (𝐴↑𝑁)) + Σ𝑘 ∈ ((0 + 1)...(𝑁 − 1))((-1↑(𝑘 − 1)) · (𝐴↑𝑘))) + Σ𝑘 ∈ ((0 + 1)...(𝑁 − 1))((-1↑𝑘) · (𝐴↑𝑘))) = (((-1↑(𝑁 − 1)) · (𝐴↑𝑁)) + (Σ𝑘 ∈ ((0 + 1)...(𝑁 − 1))((-1↑(𝑘 − 1)) · (𝐴↑𝑘)) + Σ𝑘 ∈ ((0 + 1)...(𝑁 − 1))((-1↑𝑘) · (𝐴↑𝑘))))) |
157 | | nncn 10905 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑘 ∈ ℕ → 𝑘 ∈
ℂ) |
158 | | npcan1 10334 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑘 ∈ ℂ → ((𝑘 − 1) + 1) = 𝑘) |
159 | 157, 158 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑘 ∈ ℕ → ((𝑘 − 1) + 1) = 𝑘) |
160 | 159 | eqcomd 2616 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑘 ∈ ℕ → 𝑘 = ((𝑘 − 1) + 1)) |
161 | 160 | oveq2d 6565 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑘 ∈ ℕ →
(-1↑𝑘) =
(-1↑((𝑘 − 1) +
1))) |
162 | 4 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑘 ∈ ℕ → -1 ∈
ℂ) |
163 | 162, 136 | expp1d 12871 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑘 ∈ ℕ →
(-1↑((𝑘 − 1) +
1)) = ((-1↑(𝑘 −
1)) · -1)) |
164 | 162, 136 | expcld 12870 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑘 ∈ ℕ →
(-1↑(𝑘 − 1))
∈ ℂ) |
165 | 164, 162 | mulcomd 9940 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑘 ∈ ℕ →
((-1↑(𝑘 − 1))
· -1) = (-1 · (-1↑(𝑘 − 1)))) |
166 | 161, 163,
165 | 3eqtrd 2648 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑘 ∈ ℕ →
(-1↑𝑘) = (-1 ·
(-1↑(𝑘 −
1)))) |
167 | 166 | oveq2d 6565 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑘 ∈ ℕ →
((-1↑(𝑘 − 1)) +
(-1↑𝑘)) =
((-1↑(𝑘 − 1)) +
(-1 · (-1↑(𝑘
− 1))))) |
168 | 164 | mulm1d 10361 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑘 ∈ ℕ → (-1
· (-1↑(𝑘
− 1))) = -(-1↑(𝑘
− 1))) |
169 | 168 | oveq2d 6565 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑘 ∈ ℕ →
((-1↑(𝑘 − 1)) +
(-1 · (-1↑(𝑘
− 1)))) = ((-1↑(𝑘 − 1)) + -(-1↑(𝑘 − 1)))) |
170 | 164 | negidd 10261 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑘 ∈ ℕ →
((-1↑(𝑘 − 1)) +
-(-1↑(𝑘 − 1))) =
0) |
171 | 167, 169,
170 | 3eqtrd 2648 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑘 ∈ ℕ →
((-1↑(𝑘 − 1)) +
(-1↑𝑘)) =
0) |
172 | 171 | adantl 481 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → ((-1↑(𝑘 − 1)) + (-1↑𝑘)) = 0) |
173 | 172 | oveq1d 6564 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (((-1↑(𝑘 − 1)) + (-1↑𝑘)) · (𝐴↑𝑘)) = (0 · (𝐴↑𝑘))) |
174 | 138, 123,
125 | adddird 9944 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (((-1↑(𝑘 − 1)) + (-1↑𝑘)) · (𝐴↑𝑘)) = (((-1↑(𝑘 − 1)) · (𝐴↑𝑘)) + ((-1↑𝑘) · (𝐴↑𝑘)))) |
175 | 125 | mul02d 10113 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (0 · (𝐴↑𝑘)) = 0) |
176 | 173, 174,
175 | 3eqtr3d 2652 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (((-1↑(𝑘 − 1)) · (𝐴↑𝑘)) + ((-1↑𝑘) · (𝐴↑𝑘))) = 0) |
177 | 176 | expcom 450 |
. . . . . . . . . . . . 13
⊢ (𝑘 ∈ ℕ → (𝜑 → (((-1↑(𝑘 − 1)) · (𝐴↑𝑘)) + ((-1↑𝑘) · (𝐴↑𝑘))) = 0)) |
178 | 119, 177 | syl 17 |
. . . . . . . . . . . 12
⊢ (𝑘 ∈ (1...(𝑁 − 1)) → (𝜑 → (((-1↑(𝑘 − 1)) · (𝐴↑𝑘)) + ((-1↑𝑘) · (𝐴↑𝑘))) = 0)) |
179 | 178, 129 | eleq2s 2706 |
. . . . . . . . . . 11
⊢ (𝑘 ∈ ((0 + 1)...(𝑁 − 1)) → (𝜑 → (((-1↑(𝑘 − 1)) · (𝐴↑𝑘)) + ((-1↑𝑘) · (𝐴↑𝑘))) = 0)) |
180 | 179 | impcom 445 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑘 ∈ ((0 + 1)...(𝑁 − 1))) → (((-1↑(𝑘 − 1)) · (𝐴↑𝑘)) + ((-1↑𝑘) · (𝐴↑𝑘))) = 0) |
181 | 180 | sumeq2dv 14281 |
. . . . . . . . 9
⊢ (𝜑 → Σ𝑘 ∈ ((0 + 1)...(𝑁 − 1))(((-1↑(𝑘 − 1)) · (𝐴↑𝑘)) + ((-1↑𝑘) · (𝐴↑𝑘))) = Σ𝑘 ∈ ((0 + 1)...(𝑁 − 1))0) |
182 | 118, 143,
131 | fsumadd 14317 |
. . . . . . . . 9
⊢ (𝜑 → Σ𝑘 ∈ ((0 + 1)...(𝑁 − 1))(((-1↑(𝑘 − 1)) · (𝐴↑𝑘)) + ((-1↑𝑘) · (𝐴↑𝑘))) = (Σ𝑘 ∈ ((0 + 1)...(𝑁 − 1))((-1↑(𝑘 − 1)) · (𝐴↑𝑘)) + Σ𝑘 ∈ ((0 + 1)...(𝑁 − 1))((-1↑𝑘) · (𝐴↑𝑘)))) |
183 | 118 | olcd 407 |
. . . . . . . . . 10
⊢ (𝜑 → (((0 + 1)...(𝑁 − 1)) ⊆
(ℤ≥‘1) ∨ ((0 + 1)...(𝑁 − 1)) ∈ Fin)) |
184 | | sumz 14300 |
. . . . . . . . . 10
⊢ ((((0 +
1)...(𝑁 − 1)) ⊆
(ℤ≥‘1) ∨ ((0 + 1)...(𝑁 − 1)) ∈ Fin) → Σ𝑘 ∈ ((0 + 1)...(𝑁 − 1))0 =
0) |
185 | 183, 184 | syl 17 |
. . . . . . . . 9
⊢ (𝜑 → Σ𝑘 ∈ ((0 + 1)...(𝑁 − 1))0 = 0) |
186 | 181, 182,
185 | 3eqtr3d 2652 |
. . . . . . . 8
⊢ (𝜑 → (Σ𝑘 ∈ ((0 + 1)...(𝑁 − 1))((-1↑(𝑘 − 1)) · (𝐴↑𝑘)) + Σ𝑘 ∈ ((0 + 1)...(𝑁 − 1))((-1↑𝑘) · (𝐴↑𝑘))) = 0) |
187 | 186 | oveq2d 6565 |
. . . . . . 7
⊢ (𝜑 → (((-1↑(𝑁 − 1)) · (𝐴↑𝑁)) + (Σ𝑘 ∈ ((0 + 1)...(𝑁 − 1))((-1↑(𝑘 − 1)) · (𝐴↑𝑘)) + Σ𝑘 ∈ ((0 + 1)...(𝑁 − 1))((-1↑𝑘) · (𝐴↑𝑘)))) = (((-1↑(𝑁 − 1)) · (𝐴↑𝑁)) + 0)) |
188 | 151 | addid1d 10115 |
. . . . . . 7
⊢ (𝜑 → (((-1↑(𝑁 − 1)) · (𝐴↑𝑁)) + 0) = ((-1↑(𝑁 − 1)) · (𝐴↑𝑁))) |
189 | 187, 188 | eqtrd 2644 |
. . . . . 6
⊢ (𝜑 → (((-1↑(𝑁 − 1)) · (𝐴↑𝑁)) + (Σ𝑘 ∈ ((0 + 1)...(𝑁 − 1))((-1↑(𝑘 − 1)) · (𝐴↑𝑘)) + Σ𝑘 ∈ ((0 + 1)...(𝑁 − 1))((-1↑𝑘) · (𝐴↑𝑘)))) = ((-1↑(𝑁 − 1)) · (𝐴↑𝑁))) |
190 | 155, 156,
189 | 3eqtrd 2648 |
. . . . 5
⊢ (𝜑 → ((Σ𝑘 ∈ ((0 + 1)...(𝑁 − 1))((-1↑(𝑘 − 1)) · (𝐴↑𝑘)) + ((-1↑(𝑁 − 1)) · (𝐴↑𝑁))) + Σ𝑘 ∈ ((0 + 1)...(𝑁 − 1))((-1↑𝑘) · (𝐴↑𝑘))) = ((-1↑(𝑁 − 1)) · (𝐴↑𝑁))) |
191 | 190 | oveq1d 6564 |
. . . 4
⊢ (𝜑 → (((Σ𝑘 ∈ ((0 + 1)...(𝑁 − 1))((-1↑(𝑘 − 1)) · (𝐴↑𝑘)) + ((-1↑(𝑁 − 1)) · (𝐴↑𝑁))) + Σ𝑘 ∈ ((0 + 1)...(𝑁 − 1))((-1↑𝑘) · (𝐴↑𝑘))) + 1) = (((-1↑(𝑁 − 1)) · (𝐴↑𝑁)) + 1)) |
192 | 135, 153,
191 | 3eqtr2d 2650 |
. . 3
⊢ (𝜑 → (Σ𝑘 ∈ (0...(𝑁 − 1))((-1↑𝑘) · (𝐴↑(𝑘 + 1))) + Σ𝑘 ∈ (0...(𝑁 − 1))((-1↑𝑘) · (𝐴↑𝑘))) = (((-1↑(𝑁 − 1)) · (𝐴↑𝑁)) + 1)) |
193 | 13, 26, 192 | 3eqtrd 2648 |
. 2
⊢ (𝜑 → ((𝐴 + 1) · Σ𝑘 ∈ (0...(𝑁 − 1))((-1↑𝑘) · (𝐴↑𝑘))) = (((-1↑(𝑁 − 1)) · (𝐴↑𝑁)) + 1)) |
194 | 193 | eqcomd 2616 |
1
⊢ (𝜑 → (((-1↑(𝑁 − 1)) · (𝐴↑𝑁)) + 1) = ((𝐴 + 1) · Σ𝑘 ∈ (0...(𝑁 − 1))((-1↑𝑘) · (𝐴↑𝑘)))) |