MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  pwp1fsum Structured version   Visualization version   GIF version

Theorem pwp1fsum 15045
Description: The n-th power of a number increased by 1 expressed by a product with a finite sum. (Contributed by AV, 15-Aug-2021.)
Hypotheses
Ref Expression
pwp1fsum.a (𝜑𝐴 ∈ ℂ)
pwp1fsum.n (𝜑𝑁 ∈ ℕ)
Assertion
Ref Expression
pwp1fsum (𝜑 → (((-1↑(𝑁 − 1)) · (𝐴𝑁)) + 1) = ((𝐴 + 1) · Σ𝑘 ∈ (0...(𝑁 − 1))((-1↑𝑘) · (𝐴𝑘))))
Distinct variable groups:   𝐴,𝑘   𝑘,𝑁   𝜑,𝑘

Proof of Theorem pwp1fsum
Dummy variable 𝑙 is distinct from all other variables.
StepHypRef Expression
1 pwp1fsum.a . . . 4 (𝜑𝐴 ∈ ℂ)
2 1cnd 10007 . . . 4 (𝜑 → 1 ∈ ℂ)
3 fzfid 12719 . . . . 5 (𝜑 → (0...(𝑁 − 1)) ∈ Fin)
4 neg1cn 11075 . . . . . . . 8 -1 ∈ ℂ
54a1i 11 . . . . . . 7 ((𝜑𝑘 ∈ (0...(𝑁 − 1))) → -1 ∈ ℂ)
6 elfznn0 12381 . . . . . . . 8 (𝑘 ∈ (0...(𝑁 − 1)) → 𝑘 ∈ ℕ0)
76adantl 482 . . . . . . 7 ((𝜑𝑘 ∈ (0...(𝑁 − 1))) → 𝑘 ∈ ℕ0)
85, 7expcld 12955 . . . . . 6 ((𝜑𝑘 ∈ (0...(𝑁 − 1))) → (-1↑𝑘) ∈ ℂ)
91adantr 481 . . . . . . 7 ((𝜑𝑘 ∈ (0...(𝑁 − 1))) → 𝐴 ∈ ℂ)
109, 7expcld 12955 . . . . . 6 ((𝜑𝑘 ∈ (0...(𝑁 − 1))) → (𝐴𝑘) ∈ ℂ)
118, 10mulcld 10011 . . . . 5 ((𝜑𝑘 ∈ (0...(𝑁 − 1))) → ((-1↑𝑘) · (𝐴𝑘)) ∈ ℂ)
123, 11fsumcl 14404 . . . 4 (𝜑 → Σ𝑘 ∈ (0...(𝑁 − 1))((-1↑𝑘) · (𝐴𝑘)) ∈ ℂ)
131, 2, 12adddird 10016 . . 3 (𝜑 → ((𝐴 + 1) · Σ𝑘 ∈ (0...(𝑁 − 1))((-1↑𝑘) · (𝐴𝑘))) = ((𝐴 · Σ𝑘 ∈ (0...(𝑁 − 1))((-1↑𝑘) · (𝐴𝑘))) + (1 · Σ𝑘 ∈ (0...(𝑁 − 1))((-1↑𝑘) · (𝐴𝑘)))))
143, 1, 11fsummulc2 14451 . . . . 5 (𝜑 → (𝐴 · Σ𝑘 ∈ (0...(𝑁 − 1))((-1↑𝑘) · (𝐴𝑘))) = Σ𝑘 ∈ (0...(𝑁 − 1))(𝐴 · ((-1↑𝑘) · (𝐴𝑘))))
159, 11mulcomd 10012 . . . . . . . 8 ((𝜑𝑘 ∈ (0...(𝑁 − 1))) → (𝐴 · ((-1↑𝑘) · (𝐴𝑘))) = (((-1↑𝑘) · (𝐴𝑘)) · 𝐴))
168, 10, 9mulassd 10014 . . . . . . . 8 ((𝜑𝑘 ∈ (0...(𝑁 − 1))) → (((-1↑𝑘) · (𝐴𝑘)) · 𝐴) = ((-1↑𝑘) · ((𝐴𝑘) · 𝐴)))
17 expp1 12814 . . . . . . . . . . 11 ((𝐴 ∈ ℂ ∧ 𝑘 ∈ ℕ0) → (𝐴↑(𝑘 + 1)) = ((𝐴𝑘) · 𝐴))
181, 6, 17syl2an 494 . . . . . . . . . 10 ((𝜑𝑘 ∈ (0...(𝑁 − 1))) → (𝐴↑(𝑘 + 1)) = ((𝐴𝑘) · 𝐴))
1918eqcomd 2627 . . . . . . . . 9 ((𝜑𝑘 ∈ (0...(𝑁 − 1))) → ((𝐴𝑘) · 𝐴) = (𝐴↑(𝑘 + 1)))
2019oveq2d 6626 . . . . . . . 8 ((𝜑𝑘 ∈ (0...(𝑁 − 1))) → ((-1↑𝑘) · ((𝐴𝑘) · 𝐴)) = ((-1↑𝑘) · (𝐴↑(𝑘 + 1))))
2115, 16, 203eqtrd 2659 . . . . . . 7 ((𝜑𝑘 ∈ (0...(𝑁 − 1))) → (𝐴 · ((-1↑𝑘) · (𝐴𝑘))) = ((-1↑𝑘) · (𝐴↑(𝑘 + 1))))
2221ralrimiva 2961 . . . . . 6 (𝜑 → ∀𝑘 ∈ (0...(𝑁 − 1))(𝐴 · ((-1↑𝑘) · (𝐴𝑘))) = ((-1↑𝑘) · (𝐴↑(𝑘 + 1))))
2322sumeq2d 14373 . . . . 5 (𝜑 → Σ𝑘 ∈ (0...(𝑁 − 1))(𝐴 · ((-1↑𝑘) · (𝐴𝑘))) = Σ𝑘 ∈ (0...(𝑁 − 1))((-1↑𝑘) · (𝐴↑(𝑘 + 1))))
2414, 23eqtrd 2655 . . . 4 (𝜑 → (𝐴 · Σ𝑘 ∈ (0...(𝑁 − 1))((-1↑𝑘) · (𝐴𝑘))) = Σ𝑘 ∈ (0...(𝑁 − 1))((-1↑𝑘) · (𝐴↑(𝑘 + 1))))
2512mulid2d 10009 . . . 4 (𝜑 → (1 · Σ𝑘 ∈ (0...(𝑁 − 1))((-1↑𝑘) · (𝐴𝑘))) = Σ𝑘 ∈ (0...(𝑁 − 1))((-1↑𝑘) · (𝐴𝑘)))
2624, 25oveq12d 6628 . . 3 (𝜑 → ((𝐴 · Σ𝑘 ∈ (0...(𝑁 − 1))((-1↑𝑘) · (𝐴𝑘))) + (1 · Σ𝑘 ∈ (0...(𝑁 − 1))((-1↑𝑘) · (𝐴𝑘)))) = (Σ𝑘 ∈ (0...(𝑁 − 1))((-1↑𝑘) · (𝐴↑(𝑘 + 1))) + Σ𝑘 ∈ (0...(𝑁 − 1))((-1↑𝑘) · (𝐴𝑘))))
27 1zzd 11359 . . . . . . 7 (𝜑 → 1 ∈ ℤ)
28 0zd 11340 . . . . . . 7 (𝜑 → 0 ∈ ℤ)
29 pwp1fsum.n . . . . . . . 8 (𝜑𝑁 ∈ ℕ)
30 nnz 11350 . . . . . . . . 9 (𝑁 ∈ ℕ → 𝑁 ∈ ℤ)
31 peano2zm 11371 . . . . . . . . 9 (𝑁 ∈ ℤ → (𝑁 − 1) ∈ ℤ)
3230, 31syl 17 . . . . . . . 8 (𝑁 ∈ ℕ → (𝑁 − 1) ∈ ℤ)
3329, 32syl 17 . . . . . . 7 (𝜑 → (𝑁 − 1) ∈ ℤ)
34 peano2nn0 11284 . . . . . . . . . . 11 (𝑘 ∈ ℕ0 → (𝑘 + 1) ∈ ℕ0)
356, 34syl 17 . . . . . . . . . 10 (𝑘 ∈ (0...(𝑁 − 1)) → (𝑘 + 1) ∈ ℕ0)
3635adantl 482 . . . . . . . . 9 ((𝜑𝑘 ∈ (0...(𝑁 − 1))) → (𝑘 + 1) ∈ ℕ0)
379, 36expcld 12955 . . . . . . . 8 ((𝜑𝑘 ∈ (0...(𝑁 − 1))) → (𝐴↑(𝑘 + 1)) ∈ ℂ)
388, 37mulcld 10011 . . . . . . 7 ((𝜑𝑘 ∈ (0...(𝑁 − 1))) → ((-1↑𝑘) · (𝐴↑(𝑘 + 1))) ∈ ℂ)
39 oveq2 6618 . . . . . . . 8 (𝑘 = (𝑙 − 1) → (-1↑𝑘) = (-1↑(𝑙 − 1)))
40 oveq1 6617 . . . . . . . . 9 (𝑘 = (𝑙 − 1) → (𝑘 + 1) = ((𝑙 − 1) + 1))
4140oveq2d 6626 . . . . . . . 8 (𝑘 = (𝑙 − 1) → (𝐴↑(𝑘 + 1)) = (𝐴↑((𝑙 − 1) + 1)))
4239, 41oveq12d 6628 . . . . . . 7 (𝑘 = (𝑙 − 1) → ((-1↑𝑘) · (𝐴↑(𝑘 + 1))) = ((-1↑(𝑙 − 1)) · (𝐴↑((𝑙 − 1) + 1))))
4327, 28, 33, 38, 42fsumshft 14447 . . . . . 6 (𝜑 → Σ𝑘 ∈ (0...(𝑁 − 1))((-1↑𝑘) · (𝐴↑(𝑘 + 1))) = Σ𝑙 ∈ ((0 + 1)...((𝑁 − 1) + 1))((-1↑(𝑙 − 1)) · (𝐴↑((𝑙 − 1) + 1))))
44 elfzelz 12291 . . . . . . . . . . . . 13 (𝑙 ∈ ((0 + 1)...((𝑁 − 1) + 1)) → 𝑙 ∈ ℤ)
4544zcnd 11434 . . . . . . . . . . . 12 (𝑙 ∈ ((0 + 1)...((𝑁 − 1) + 1)) → 𝑙 ∈ ℂ)
4645adantl 482 . . . . . . . . . . 11 ((𝜑𝑙 ∈ ((0 + 1)...((𝑁 − 1) + 1))) → 𝑙 ∈ ℂ)
47 npcan1 10406 . . . . . . . . . . 11 (𝑙 ∈ ℂ → ((𝑙 − 1) + 1) = 𝑙)
4846, 47syl 17 . . . . . . . . . 10 ((𝜑𝑙 ∈ ((0 + 1)...((𝑁 − 1) + 1))) → ((𝑙 − 1) + 1) = 𝑙)
4948oveq2d 6626 . . . . . . . . 9 ((𝜑𝑙 ∈ ((0 + 1)...((𝑁 − 1) + 1))) → (𝐴↑((𝑙 − 1) + 1)) = (𝐴𝑙))
5049oveq2d 6626 . . . . . . . 8 ((𝜑𝑙 ∈ ((0 + 1)...((𝑁 − 1) + 1))) → ((-1↑(𝑙 − 1)) · (𝐴↑((𝑙 − 1) + 1))) = ((-1↑(𝑙 − 1)) · (𝐴𝑙)))
5150ralrimiva 2961 . . . . . . 7 (𝜑 → ∀𝑙 ∈ ((0 + 1)...((𝑁 − 1) + 1))((-1↑(𝑙 − 1)) · (𝐴↑((𝑙 − 1) + 1))) = ((-1↑(𝑙 − 1)) · (𝐴𝑙)))
5251sumeq2d 14373 . . . . . 6 (𝜑 → Σ𝑙 ∈ ((0 + 1)...((𝑁 − 1) + 1))((-1↑(𝑙 − 1)) · (𝐴↑((𝑙 − 1) + 1))) = Σ𝑙 ∈ ((0 + 1)...((𝑁 − 1) + 1))((-1↑(𝑙 − 1)) · (𝐴𝑙)))
5329nncnd 10987 . . . . . . . . . 10 (𝜑𝑁 ∈ ℂ)
54 npcan1 10406 . . . . . . . . . 10 (𝑁 ∈ ℂ → ((𝑁 − 1) + 1) = 𝑁)
5553, 54syl 17 . . . . . . . . 9 (𝜑 → ((𝑁 − 1) + 1) = 𝑁)
56 0p1e1 11083 . . . . . . . . . . . 12 (0 + 1) = 1
5756fveq2i 6156 . . . . . . . . . . 11 (ℤ‘(0 + 1)) = (ℤ‘1)
58 nnuz 11674 . . . . . . . . . . 11 ℕ = (ℤ‘1)
5957, 58eqtr4i 2646 . . . . . . . . . 10 (ℤ‘(0 + 1)) = ℕ
6059a1i 11 . . . . . . . . 9 (𝜑 → (ℤ‘(0 + 1)) = ℕ)
6129, 55, 603eltr4d 2713 . . . . . . . 8 (𝜑 → ((𝑁 − 1) + 1) ∈ (ℤ‘(0 + 1)))
6256oveq1i 6620 . . . . . . . . . . 11 ((0 + 1)...((𝑁 − 1) + 1)) = (1...((𝑁 − 1) + 1))
6362eleq2i 2690 . . . . . . . . . 10 (𝑙 ∈ ((0 + 1)...((𝑁 − 1) + 1)) ↔ 𝑙 ∈ (1...((𝑁 − 1) + 1)))
644a1i 11 . . . . . . . . . . . . . 14 ((𝜑𝑙 ∈ ℕ) → -1 ∈ ℂ)
65 nnm1nn0 11285 . . . . . . . . . . . . . . 15 (𝑙 ∈ ℕ → (𝑙 − 1) ∈ ℕ0)
6665adantl 482 . . . . . . . . . . . . . 14 ((𝜑𝑙 ∈ ℕ) → (𝑙 − 1) ∈ ℕ0)
6764, 66expcld 12955 . . . . . . . . . . . . 13 ((𝜑𝑙 ∈ ℕ) → (-1↑(𝑙 − 1)) ∈ ℂ)
681adantr 481 . . . . . . . . . . . . . 14 ((𝜑𝑙 ∈ ℕ) → 𝐴 ∈ ℂ)
69 nnnn0 11250 . . . . . . . . . . . . . . 15 (𝑙 ∈ ℕ → 𝑙 ∈ ℕ0)
7069adantl 482 . . . . . . . . . . . . . 14 ((𝜑𝑙 ∈ ℕ) → 𝑙 ∈ ℕ0)
7168, 70expcld 12955 . . . . . . . . . . . . 13 ((𝜑𝑙 ∈ ℕ) → (𝐴𝑙) ∈ ℂ)
7267, 71mulcld 10011 . . . . . . . . . . . 12 ((𝜑𝑙 ∈ ℕ) → ((-1↑(𝑙 − 1)) · (𝐴𝑙)) ∈ ℂ)
7372expcom 451 . . . . . . . . . . 11 (𝑙 ∈ ℕ → (𝜑 → ((-1↑(𝑙 − 1)) · (𝐴𝑙)) ∈ ℂ))
74 elfznn 12319 . . . . . . . . . . 11 (𝑙 ∈ (1...((𝑁 − 1) + 1)) → 𝑙 ∈ ℕ)
7573, 74syl11 33 . . . . . . . . . 10 (𝜑 → (𝑙 ∈ (1...((𝑁 − 1) + 1)) → ((-1↑(𝑙 − 1)) · (𝐴𝑙)) ∈ ℂ))
7663, 75syl5bi 232 . . . . . . . . 9 (𝜑 → (𝑙 ∈ ((0 + 1)...((𝑁 − 1) + 1)) → ((-1↑(𝑙 − 1)) · (𝐴𝑙)) ∈ ℂ))
7776imp 445 . . . . . . . 8 ((𝜑𝑙 ∈ ((0 + 1)...((𝑁 − 1) + 1))) → ((-1↑(𝑙 − 1)) · (𝐴𝑙)) ∈ ℂ)
78 oveq1 6617 . . . . . . . . . 10 (𝑙 = ((𝑁 − 1) + 1) → (𝑙 − 1) = (((𝑁 − 1) + 1) − 1))
7978oveq2d 6626 . . . . . . . . 9 (𝑙 = ((𝑁 − 1) + 1) → (-1↑(𝑙 − 1)) = (-1↑(((𝑁 − 1) + 1) − 1)))
80 oveq2 6618 . . . . . . . . 9 (𝑙 = ((𝑁 − 1) + 1) → (𝐴𝑙) = (𝐴↑((𝑁 − 1) + 1)))
8179, 80oveq12d 6628 . . . . . . . 8 (𝑙 = ((𝑁 − 1) + 1) → ((-1↑(𝑙 − 1)) · (𝐴𝑙)) = ((-1↑(((𝑁 − 1) + 1) − 1)) · (𝐴↑((𝑁 − 1) + 1))))
8261, 77, 81fsumm1 14417 . . . . . . 7 (𝜑 → Σ𝑙 ∈ ((0 + 1)...((𝑁 − 1) + 1))((-1↑(𝑙 − 1)) · (𝐴𝑙)) = (Σ𝑙 ∈ ((0 + 1)...(((𝑁 − 1) + 1) − 1))((-1↑(𝑙 − 1)) · (𝐴𝑙)) + ((-1↑(((𝑁 − 1) + 1) − 1)) · (𝐴↑((𝑁 − 1) + 1)))))
8333zcnd 11434 . . . . . . . . . . . 12 (𝜑 → (𝑁 − 1) ∈ ℂ)
84 pncan1 10405 . . . . . . . . . . . 12 ((𝑁 − 1) ∈ ℂ → (((𝑁 − 1) + 1) − 1) = (𝑁 − 1))
8583, 84syl 17 . . . . . . . . . . 11 (𝜑 → (((𝑁 − 1) + 1) − 1) = (𝑁 − 1))
8685oveq2d 6626 . . . . . . . . . 10 (𝜑 → ((0 + 1)...(((𝑁 − 1) + 1) − 1)) = ((0 + 1)...(𝑁 − 1)))
8786sumeq1d 14372 . . . . . . . . 9 (𝜑 → Σ𝑙 ∈ ((0 + 1)...(((𝑁 − 1) + 1) − 1))((-1↑(𝑙 − 1)) · (𝐴𝑙)) = Σ𝑙 ∈ ((0 + 1)...(𝑁 − 1))((-1↑(𝑙 − 1)) · (𝐴𝑙)))
88 oveq1 6617 . . . . . . . . . . . 12 (𝑙 = 𝑘 → (𝑙 − 1) = (𝑘 − 1))
8988oveq2d 6626 . . . . . . . . . . 11 (𝑙 = 𝑘 → (-1↑(𝑙 − 1)) = (-1↑(𝑘 − 1)))
90 oveq2 6618 . . . . . . . . . . 11 (𝑙 = 𝑘 → (𝐴𝑙) = (𝐴𝑘))
9189, 90oveq12d 6628 . . . . . . . . . 10 (𝑙 = 𝑘 → ((-1↑(𝑙 − 1)) · (𝐴𝑙)) = ((-1↑(𝑘 − 1)) · (𝐴𝑘)))
9291cbvsumv 14367 . . . . . . . . 9 Σ𝑙 ∈ ((0 + 1)...(𝑁 − 1))((-1↑(𝑙 − 1)) · (𝐴𝑙)) = Σ𝑘 ∈ ((0 + 1)...(𝑁 − 1))((-1↑(𝑘 − 1)) · (𝐴𝑘))
9387, 92syl6eq 2671 . . . . . . . 8 (𝜑 → Σ𝑙 ∈ ((0 + 1)...(((𝑁 − 1) + 1) − 1))((-1↑(𝑙 − 1)) · (𝐴𝑙)) = Σ𝑘 ∈ ((0 + 1)...(𝑁 − 1))((-1↑(𝑘 − 1)) · (𝐴𝑘)))
9485oveq2d 6626 . . . . . . . . 9 (𝜑 → (-1↑(((𝑁 − 1) + 1) − 1)) = (-1↑(𝑁 − 1)))
9555oveq2d 6626 . . . . . . . . 9 (𝜑 → (𝐴↑((𝑁 − 1) + 1)) = (𝐴𝑁))
9694, 95oveq12d 6628 . . . . . . . 8 (𝜑 → ((-1↑(((𝑁 − 1) + 1) − 1)) · (𝐴↑((𝑁 − 1) + 1))) = ((-1↑(𝑁 − 1)) · (𝐴𝑁)))
9793, 96oveq12d 6628 . . . . . . 7 (𝜑 → (Σ𝑙 ∈ ((0 + 1)...(((𝑁 − 1) + 1) − 1))((-1↑(𝑙 − 1)) · (𝐴𝑙)) + ((-1↑(((𝑁 − 1) + 1) − 1)) · (𝐴↑((𝑁 − 1) + 1)))) = (Σ𝑘 ∈ ((0 + 1)...(𝑁 − 1))((-1↑(𝑘 − 1)) · (𝐴𝑘)) + ((-1↑(𝑁 − 1)) · (𝐴𝑁))))
9882, 97eqtrd 2655 . . . . . 6 (𝜑 → Σ𝑙 ∈ ((0 + 1)...((𝑁 − 1) + 1))((-1↑(𝑙 − 1)) · (𝐴𝑙)) = (Σ𝑘 ∈ ((0 + 1)...(𝑁 − 1))((-1↑(𝑘 − 1)) · (𝐴𝑘)) + ((-1↑(𝑁 − 1)) · (𝐴𝑁))))
9943, 52, 983eqtrd 2659 . . . . 5 (𝜑 → Σ𝑘 ∈ (0...(𝑁 − 1))((-1↑𝑘) · (𝐴↑(𝑘 + 1))) = (Σ𝑘 ∈ ((0 + 1)...(𝑁 − 1))((-1↑(𝑘 − 1)) · (𝐴𝑘)) + ((-1↑(𝑁 − 1)) · (𝐴𝑁))))
100 nnm1nn0 11285 . . . . . . . . 9 (𝑁 ∈ ℕ → (𝑁 − 1) ∈ ℕ0)
101 elnn0uz 11676 . . . . . . . . 9 ((𝑁 − 1) ∈ ℕ0 ↔ (𝑁 − 1) ∈ (ℤ‘0))
102100, 101sylib 208 . . . . . . . 8 (𝑁 ∈ ℕ → (𝑁 − 1) ∈ (ℤ‘0))
10329, 102syl 17 . . . . . . 7 (𝜑 → (𝑁 − 1) ∈ (ℤ‘0))
104 oveq2 6618 . . . . . . . . 9 (𝑘 = 0 → (-1↑𝑘) = (-1↑0))
105 exp0 12811 . . . . . . . . . 10 (-1 ∈ ℂ → (-1↑0) = 1)
1064, 105ax-mp 5 . . . . . . . . 9 (-1↑0) = 1
107104, 106syl6eq 2671 . . . . . . . 8 (𝑘 = 0 → (-1↑𝑘) = 1)
108 oveq2 6618 . . . . . . . 8 (𝑘 = 0 → (𝐴𝑘) = (𝐴↑0))
109107, 108oveq12d 6628 . . . . . . 7 (𝑘 = 0 → ((-1↑𝑘) · (𝐴𝑘)) = (1 · (𝐴↑0)))
110103, 11, 109fsum1p 14419 . . . . . 6 (𝜑 → Σ𝑘 ∈ (0...(𝑁 − 1))((-1↑𝑘) · (𝐴𝑘)) = ((1 · (𝐴↑0)) + Σ𝑘 ∈ ((0 + 1)...(𝑁 − 1))((-1↑𝑘) · (𝐴𝑘))))
111 exp0 12811 . . . . . . . . . 10 (𝐴 ∈ ℂ → (𝐴↑0) = 1)
1121, 111syl 17 . . . . . . . . 9 (𝜑 → (𝐴↑0) = 1)
113112oveq2d 6626 . . . . . . . 8 (𝜑 → (1 · (𝐴↑0)) = (1 · 1))
114 1t1e1 11126 . . . . . . . 8 (1 · 1) = 1
115113, 114syl6eq 2671 . . . . . . 7 (𝜑 → (1 · (𝐴↑0)) = 1)
116115oveq1d 6625 . . . . . 6 (𝜑 → ((1 · (𝐴↑0)) + Σ𝑘 ∈ ((0 + 1)...(𝑁 − 1))((-1↑𝑘) · (𝐴𝑘))) = (1 + Σ𝑘 ∈ ((0 + 1)...(𝑁 − 1))((-1↑𝑘) · (𝐴𝑘))))
117 fzfid 12719 . . . . . . . 8 (𝜑 → ((0 + 1)...(𝑁 − 1)) ∈ Fin)
118 elfznn 12319 . . . . . . . . . . 11 (𝑘 ∈ (1...(𝑁 − 1)) → 𝑘 ∈ ℕ)
1194a1i 11 . . . . . . . . . . . . . 14 ((𝜑𝑘 ∈ ℕ) → -1 ∈ ℂ)
120 nnnn0 11250 . . . . . . . . . . . . . . 15 (𝑘 ∈ ℕ → 𝑘 ∈ ℕ0)
121120adantl 482 . . . . . . . . . . . . . 14 ((𝜑𝑘 ∈ ℕ) → 𝑘 ∈ ℕ0)
122119, 121expcld 12955 . . . . . . . . . . . . 13 ((𝜑𝑘 ∈ ℕ) → (-1↑𝑘) ∈ ℂ)
1231adantr 481 . . . . . . . . . . . . . 14 ((𝜑𝑘 ∈ ℕ) → 𝐴 ∈ ℂ)
124123, 121expcld 12955 . . . . . . . . . . . . 13 ((𝜑𝑘 ∈ ℕ) → (𝐴𝑘) ∈ ℂ)
125122, 124mulcld 10011 . . . . . . . . . . . 12 ((𝜑𝑘 ∈ ℕ) → ((-1↑𝑘) · (𝐴𝑘)) ∈ ℂ)
126125expcom 451 . . . . . . . . . . 11 (𝑘 ∈ ℕ → (𝜑 → ((-1↑𝑘) · (𝐴𝑘)) ∈ ℂ))
127118, 126syl 17 . . . . . . . . . 10 (𝑘 ∈ (1...(𝑁 − 1)) → (𝜑 → ((-1↑𝑘) · (𝐴𝑘)) ∈ ℂ))
12856oveq1i 6620 . . . . . . . . . 10 ((0 + 1)...(𝑁 − 1)) = (1...(𝑁 − 1))
129127, 128eleq2s 2716 . . . . . . . . 9 (𝑘 ∈ ((0 + 1)...(𝑁 − 1)) → (𝜑 → ((-1↑𝑘) · (𝐴𝑘)) ∈ ℂ))
130129impcom 446 . . . . . . . 8 ((𝜑𝑘 ∈ ((0 + 1)...(𝑁 − 1))) → ((-1↑𝑘) · (𝐴𝑘)) ∈ ℂ)
131117, 130fsumcl 14404 . . . . . . 7 (𝜑 → Σ𝑘 ∈ ((0 + 1)...(𝑁 − 1))((-1↑𝑘) · (𝐴𝑘)) ∈ ℂ)
1322, 131addcomd 10189 . . . . . 6 (𝜑 → (1 + Σ𝑘 ∈ ((0 + 1)...(𝑁 − 1))((-1↑𝑘) · (𝐴𝑘))) = (Σ𝑘 ∈ ((0 + 1)...(𝑁 − 1))((-1↑𝑘) · (𝐴𝑘)) + 1))
133110, 116, 1323eqtrd 2659 . . . . 5 (𝜑 → Σ𝑘 ∈ (0...(𝑁 − 1))((-1↑𝑘) · (𝐴𝑘)) = (Σ𝑘 ∈ ((0 + 1)...(𝑁 − 1))((-1↑𝑘) · (𝐴𝑘)) + 1))
13499, 133oveq12d 6628 . . . 4 (𝜑 → (Σ𝑘 ∈ (0...(𝑁 − 1))((-1↑𝑘) · (𝐴↑(𝑘 + 1))) + Σ𝑘 ∈ (0...(𝑁 − 1))((-1↑𝑘) · (𝐴𝑘))) = ((Σ𝑘 ∈ ((0 + 1)...(𝑁 − 1))((-1↑(𝑘 − 1)) · (𝐴𝑘)) + ((-1↑(𝑁 − 1)) · (𝐴𝑁))) + (Σ𝑘 ∈ ((0 + 1)...(𝑁 − 1))((-1↑𝑘) · (𝐴𝑘)) + 1)))
135 nnm1nn0 11285 . . . . . . . . . . . . . 14 (𝑘 ∈ ℕ → (𝑘 − 1) ∈ ℕ0)
136135adantl 482 . . . . . . . . . . . . 13 ((𝜑𝑘 ∈ ℕ) → (𝑘 − 1) ∈ ℕ0)
137119, 136expcld 12955 . . . . . . . . . . . 12 ((𝜑𝑘 ∈ ℕ) → (-1↑(𝑘 − 1)) ∈ ℂ)
138137, 124mulcld 10011 . . . . . . . . . . 11 ((𝜑𝑘 ∈ ℕ) → ((-1↑(𝑘 − 1)) · (𝐴𝑘)) ∈ ℂ)
139138expcom 451 . . . . . . . . . 10 (𝑘 ∈ ℕ → (𝜑 → ((-1↑(𝑘 − 1)) · (𝐴𝑘)) ∈ ℂ))
140118, 139syl 17 . . . . . . . . 9 (𝑘 ∈ (1...(𝑁 − 1)) → (𝜑 → ((-1↑(𝑘 − 1)) · (𝐴𝑘)) ∈ ℂ))
141140, 128eleq2s 2716 . . . . . . . 8 (𝑘 ∈ ((0 + 1)...(𝑁 − 1)) → (𝜑 → ((-1↑(𝑘 − 1)) · (𝐴𝑘)) ∈ ℂ))
142141impcom 446 . . . . . . 7 ((𝜑𝑘 ∈ ((0 + 1)...(𝑁 − 1))) → ((-1↑(𝑘 − 1)) · (𝐴𝑘)) ∈ ℂ)
143117, 142fsumcl 14404 . . . . . 6 (𝜑 → Σ𝑘 ∈ ((0 + 1)...(𝑁 − 1))((-1↑(𝑘 − 1)) · (𝐴𝑘)) ∈ ℂ)
1444a1i 11 . . . . . . . 8 (𝜑 → -1 ∈ ℂ)
14529, 100syl 17 . . . . . . . 8 (𝜑 → (𝑁 − 1) ∈ ℕ0)
146144, 145expcld 12955 . . . . . . 7 (𝜑 → (-1↑(𝑁 − 1)) ∈ ℂ)
147 nnnn0 11250 . . . . . . . . 9 (𝑁 ∈ ℕ → 𝑁 ∈ ℕ0)
14829, 147syl 17 . . . . . . . 8 (𝜑𝑁 ∈ ℕ0)
1491, 148expcld 12955 . . . . . . 7 (𝜑 → (𝐴𝑁) ∈ ℂ)
150146, 149mulcld 10011 . . . . . 6 (𝜑 → ((-1↑(𝑁 − 1)) · (𝐴𝑁)) ∈ ℂ)
151143, 150addcld 10010 . . . . 5 (𝜑 → (Σ𝑘 ∈ ((0 + 1)...(𝑁 − 1))((-1↑(𝑘 − 1)) · (𝐴𝑘)) + ((-1↑(𝑁 − 1)) · (𝐴𝑁))) ∈ ℂ)
152151, 131, 2addassd 10013 . . . 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)))
153143, 150addcomd 10189 . . . . . . 7 (𝜑 → (Σ𝑘 ∈ ((0 + 1)...(𝑁 − 1))((-1↑(𝑘 − 1)) · (𝐴𝑘)) + ((-1↑(𝑁 − 1)) · (𝐴𝑁))) = (((-1↑(𝑁 − 1)) · (𝐴𝑁)) + Σ𝑘 ∈ ((0 + 1)...(𝑁 − 1))((-1↑(𝑘 − 1)) · (𝐴𝑘))))
154153oveq1d 6625 . . . . . 6 (𝜑 → ((Σ𝑘 ∈ ((0 + 1)...(𝑁 − 1))((-1↑(𝑘 − 1)) · (𝐴𝑘)) + ((-1↑(𝑁 − 1)) · (𝐴𝑁))) + Σ𝑘 ∈ ((0 + 1)...(𝑁 − 1))((-1↑𝑘) · (𝐴𝑘))) = ((((-1↑(𝑁 − 1)) · (𝐴𝑁)) + Σ𝑘 ∈ ((0 + 1)...(𝑁 − 1))((-1↑(𝑘 − 1)) · (𝐴𝑘))) + Σ𝑘 ∈ ((0 + 1)...(𝑁 − 1))((-1↑𝑘) · (𝐴𝑘))))
155150, 143, 131addassd 10013 . . . . . 6 (𝜑 → ((((-1↑(𝑁 − 1)) · (𝐴𝑁)) + Σ𝑘 ∈ ((0 + 1)...(𝑁 − 1))((-1↑(𝑘 − 1)) · (𝐴𝑘))) + Σ𝑘 ∈ ((0 + 1)...(𝑁 − 1))((-1↑𝑘) · (𝐴𝑘))) = (((-1↑(𝑁 − 1)) · (𝐴𝑁)) + (Σ𝑘 ∈ ((0 + 1)...(𝑁 − 1))((-1↑(𝑘 − 1)) · (𝐴𝑘)) + Σ𝑘 ∈ ((0 + 1)...(𝑁 − 1))((-1↑𝑘) · (𝐴𝑘)))))
156 nncn 10979 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑘 ∈ ℕ → 𝑘 ∈ ℂ)
157 npcan1 10406 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑘 ∈ ℂ → ((𝑘 − 1) + 1) = 𝑘)
158156, 157syl 17 . . . . . . . . . . . . . . . . . . . . . 22 (𝑘 ∈ ℕ → ((𝑘 − 1) + 1) = 𝑘)
159158eqcomd 2627 . . . . . . . . . . . . . . . . . . . . 21 (𝑘 ∈ ℕ → 𝑘 = ((𝑘 − 1) + 1))
160159oveq2d 6626 . . . . . . . . . . . . . . . . . . . 20 (𝑘 ∈ ℕ → (-1↑𝑘) = (-1↑((𝑘 − 1) + 1)))
1614a1i 11 . . . . . . . . . . . . . . . . . . . . 21 (𝑘 ∈ ℕ → -1 ∈ ℂ)
162161, 135expp1d 12956 . . . . . . . . . . . . . . . . . . . 20 (𝑘 ∈ ℕ → (-1↑((𝑘 − 1) + 1)) = ((-1↑(𝑘 − 1)) · -1))
163161, 135expcld 12955 . . . . . . . . . . . . . . . . . . . . 21 (𝑘 ∈ ℕ → (-1↑(𝑘 − 1)) ∈ ℂ)
164163, 161mulcomd 10012 . . . . . . . . . . . . . . . . . . . 20 (𝑘 ∈ ℕ → ((-1↑(𝑘 − 1)) · -1) = (-1 · (-1↑(𝑘 − 1))))
165160, 162, 1643eqtrd 2659 . . . . . . . . . . . . . . . . . . 19 (𝑘 ∈ ℕ → (-1↑𝑘) = (-1 · (-1↑(𝑘 − 1))))
166165oveq2d 6626 . . . . . . . . . . . . . . . . . 18 (𝑘 ∈ ℕ → ((-1↑(𝑘 − 1)) + (-1↑𝑘)) = ((-1↑(𝑘 − 1)) + (-1 · (-1↑(𝑘 − 1)))))
167163mulm1d 10433 . . . . . . . . . . . . . . . . . . 19 (𝑘 ∈ ℕ → (-1 · (-1↑(𝑘 − 1))) = -(-1↑(𝑘 − 1)))
168167oveq2d 6626 . . . . . . . . . . . . . . . . . 18 (𝑘 ∈ ℕ → ((-1↑(𝑘 − 1)) + (-1 · (-1↑(𝑘 − 1)))) = ((-1↑(𝑘 − 1)) + -(-1↑(𝑘 − 1))))
169163negidd 10333 . . . . . . . . . . . . . . . . . 18 (𝑘 ∈ ℕ → ((-1↑(𝑘 − 1)) + -(-1↑(𝑘 − 1))) = 0)
170166, 168, 1693eqtrd 2659 . . . . . . . . . . . . . . . . 17 (𝑘 ∈ ℕ → ((-1↑(𝑘 − 1)) + (-1↑𝑘)) = 0)
171170adantl 482 . . . . . . . . . . . . . . . 16 ((𝜑𝑘 ∈ ℕ) → ((-1↑(𝑘 − 1)) + (-1↑𝑘)) = 0)
172171oveq1d 6625 . . . . . . . . . . . . . . 15 ((𝜑𝑘 ∈ ℕ) → (((-1↑(𝑘 − 1)) + (-1↑𝑘)) · (𝐴𝑘)) = (0 · (𝐴𝑘)))
173137, 122, 124adddird 10016 . . . . . . . . . . . . . . 15 ((𝜑𝑘 ∈ ℕ) → (((-1↑(𝑘 − 1)) + (-1↑𝑘)) · (𝐴𝑘)) = (((-1↑(𝑘 − 1)) · (𝐴𝑘)) + ((-1↑𝑘) · (𝐴𝑘))))
174124mul02d 10185 . . . . . . . . . . . . . . 15 ((𝜑𝑘 ∈ ℕ) → (0 · (𝐴𝑘)) = 0)
175172, 173, 1743eqtr3d 2663 . . . . . . . . . . . . . 14 ((𝜑𝑘 ∈ ℕ) → (((-1↑(𝑘 − 1)) · (𝐴𝑘)) + ((-1↑𝑘) · (𝐴𝑘))) = 0)
176175expcom 451 . . . . . . . . . . . . 13 (𝑘 ∈ ℕ → (𝜑 → (((-1↑(𝑘 − 1)) · (𝐴𝑘)) + ((-1↑𝑘) · (𝐴𝑘))) = 0))
177118, 176syl 17 . . . . . . . . . . . 12 (𝑘 ∈ (1...(𝑁 − 1)) → (𝜑 → (((-1↑(𝑘 − 1)) · (𝐴𝑘)) + ((-1↑𝑘) · (𝐴𝑘))) = 0))
178177, 128eleq2s 2716 . . . . . . . . . . 11 (𝑘 ∈ ((0 + 1)...(𝑁 − 1)) → (𝜑 → (((-1↑(𝑘 − 1)) · (𝐴𝑘)) + ((-1↑𝑘) · (𝐴𝑘))) = 0))
179178impcom 446 . . . . . . . . . 10 ((𝜑𝑘 ∈ ((0 + 1)...(𝑁 − 1))) → (((-1↑(𝑘 − 1)) · (𝐴𝑘)) + ((-1↑𝑘) · (𝐴𝑘))) = 0)
180179sumeq2dv 14374 . . . . . . . . 9 (𝜑 → Σ𝑘 ∈ ((0 + 1)...(𝑁 − 1))(((-1↑(𝑘 − 1)) · (𝐴𝑘)) + ((-1↑𝑘) · (𝐴𝑘))) = Σ𝑘 ∈ ((0 + 1)...(𝑁 − 1))0)
181117, 142, 130fsumadd 14410 . . . . . . . . 9 (𝜑 → Σ𝑘 ∈ ((0 + 1)...(𝑁 − 1))(((-1↑(𝑘 − 1)) · (𝐴𝑘)) + ((-1↑𝑘) · (𝐴𝑘))) = (Σ𝑘 ∈ ((0 + 1)...(𝑁 − 1))((-1↑(𝑘 − 1)) · (𝐴𝑘)) + Σ𝑘 ∈ ((0 + 1)...(𝑁 − 1))((-1↑𝑘) · (𝐴𝑘))))
182117olcd 408 . . . . . . . . . 10 (𝜑 → (((0 + 1)...(𝑁 − 1)) ⊆ (ℤ‘1) ∨ ((0 + 1)...(𝑁 − 1)) ∈ Fin))
183 sumz 14393 . . . . . . . . . 10 ((((0 + 1)...(𝑁 − 1)) ⊆ (ℤ‘1) ∨ ((0 + 1)...(𝑁 − 1)) ∈ Fin) → Σ𝑘 ∈ ((0 + 1)...(𝑁 − 1))0 = 0)
184182, 183syl 17 . . . . . . . . 9 (𝜑 → Σ𝑘 ∈ ((0 + 1)...(𝑁 − 1))0 = 0)
185180, 181, 1843eqtr3d 2663 . . . . . . . 8 (𝜑 → (Σ𝑘 ∈ ((0 + 1)...(𝑁 − 1))((-1↑(𝑘 − 1)) · (𝐴𝑘)) + Σ𝑘 ∈ ((0 + 1)...(𝑁 − 1))((-1↑𝑘) · (𝐴𝑘))) = 0)
186185oveq2d 6626 . . . . . . 7 (𝜑 → (((-1↑(𝑁 − 1)) · (𝐴𝑁)) + (Σ𝑘 ∈ ((0 + 1)...(𝑁 − 1))((-1↑(𝑘 − 1)) · (𝐴𝑘)) + Σ𝑘 ∈ ((0 + 1)...(𝑁 − 1))((-1↑𝑘) · (𝐴𝑘)))) = (((-1↑(𝑁 − 1)) · (𝐴𝑁)) + 0))
187150addid1d 10187 . . . . . . 7 (𝜑 → (((-1↑(𝑁 − 1)) · (𝐴𝑁)) + 0) = ((-1↑(𝑁 − 1)) · (𝐴𝑁)))
188186, 187eqtrd 2655 . . . . . 6 (𝜑 → (((-1↑(𝑁 − 1)) · (𝐴𝑁)) + (Σ𝑘 ∈ ((0 + 1)...(𝑁 − 1))((-1↑(𝑘 − 1)) · (𝐴𝑘)) + Σ𝑘 ∈ ((0 + 1)...(𝑁 − 1))((-1↑𝑘) · (𝐴𝑘)))) = ((-1↑(𝑁 − 1)) · (𝐴𝑁)))
189154, 155, 1883eqtrd 2659 . . . . 5 (𝜑 → ((Σ𝑘 ∈ ((0 + 1)...(𝑁 − 1))((-1↑(𝑘 − 1)) · (𝐴𝑘)) + ((-1↑(𝑁 − 1)) · (𝐴𝑁))) + Σ𝑘 ∈ ((0 + 1)...(𝑁 − 1))((-1↑𝑘) · (𝐴𝑘))) = ((-1↑(𝑁 − 1)) · (𝐴𝑁)))
190189oveq1d 6625 . . . 4 (𝜑 → (((Σ𝑘 ∈ ((0 + 1)...(𝑁 − 1))((-1↑(𝑘 − 1)) · (𝐴𝑘)) + ((-1↑(𝑁 − 1)) · (𝐴𝑁))) + Σ𝑘 ∈ ((0 + 1)...(𝑁 − 1))((-1↑𝑘) · (𝐴𝑘))) + 1) = (((-1↑(𝑁 − 1)) · (𝐴𝑁)) + 1))
191134, 152, 1903eqtr2d 2661 . . 3 (𝜑 → (Σ𝑘 ∈ (0...(𝑁 − 1))((-1↑𝑘) · (𝐴↑(𝑘 + 1))) + Σ𝑘 ∈ (0...(𝑁 − 1))((-1↑𝑘) · (𝐴𝑘))) = (((-1↑(𝑁 − 1)) · (𝐴𝑁)) + 1))
19213, 26, 1913eqtrd 2659 . 2 (𝜑 → ((𝐴 + 1) · Σ𝑘 ∈ (0...(𝑁 − 1))((-1↑𝑘) · (𝐴𝑘))) = (((-1↑(𝑁 − 1)) · (𝐴𝑁)) + 1))
193192eqcomd 2627 1 (𝜑 → (((-1↑(𝑁 − 1)) · (𝐴𝑁)) + 1) = ((𝐴 + 1) · Σ𝑘 ∈ (0...(𝑁 − 1))((-1↑𝑘) · (𝐴𝑘))))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wo 383  wa 384   = wceq 1480  wcel 1987  wss 3559  cfv 5852  (class class class)co 6610  Fincfn 7906  cc 9885  0cc0 9887  1c1 9888   + caddc 9890   · cmul 9892  cmin 10217  -cneg 10218  cn 10971  0cn0 11243  cz 11328  cuz 11638  ...cfz 12275  cexp 12807  Σcsu 14357
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1719  ax-4 1734  ax-5 1836  ax-6 1885  ax-7 1932  ax-8 1989  ax-9 1996  ax-10 2016  ax-11 2031  ax-12 2044  ax-13 2245  ax-ext 2601  ax-rep 4736  ax-sep 4746  ax-nul 4754  ax-pow 4808  ax-pr 4872  ax-un 6909  ax-inf2 8489  ax-cnex 9943  ax-resscn 9944  ax-1cn 9945  ax-icn 9946  ax-addcl 9947  ax-addrcl 9948  ax-mulcl 9949  ax-mulrcl 9950  ax-mulcom 9951  ax-addass 9952  ax-mulass 9953  ax-distr 9954  ax-i2m1 9955  ax-1ne0 9956  ax-1rid 9957  ax-rnegex 9958  ax-rrecex 9959  ax-cnre 9960  ax-pre-lttri 9961  ax-pre-lttrn 9962  ax-pre-ltadd 9963  ax-pre-mulgt0 9964  ax-pre-sup 9965
This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-3or 1037  df-3an 1038  df-tru 1483  df-fal 1486  df-ex 1702  df-nf 1707  df-sb 1878  df-eu 2473  df-mo 2474  df-clab 2608  df-cleq 2614  df-clel 2617  df-nfc 2750  df-ne 2791  df-nel 2894  df-ral 2912  df-rex 2913  df-reu 2914  df-rmo 2915  df-rab 2916  df-v 3191  df-sbc 3422  df-csb 3519  df-dif 3562  df-un 3564  df-in 3566  df-ss 3573  df-pss 3575  df-nul 3897  df-if 4064  df-pw 4137  df-sn 4154  df-pr 4156  df-tp 4158  df-op 4160  df-uni 4408  df-int 4446  df-iun 4492  df-br 4619  df-opab 4679  df-mpt 4680  df-tr 4718  df-eprel 4990  df-id 4994  df-po 5000  df-so 5001  df-fr 5038  df-se 5039  df-we 5040  df-xp 5085  df-rel 5086  df-cnv 5087  df-co 5088  df-dm 5089  df-rn 5090  df-res 5091  df-ima 5092  df-pred 5644  df-ord 5690  df-on 5691  df-lim 5692  df-suc 5693  df-iota 5815  df-fun 5854  df-fn 5855  df-f 5856  df-f1 5857  df-fo 5858  df-f1o 5859  df-fv 5860  df-isom 5861  df-riota 6571  df-ov 6613  df-oprab 6614  df-mpt2 6615  df-om 7020  df-1st 7120  df-2nd 7121  df-wrecs 7359  df-recs 7420  df-rdg 7458  df-1o 7512  df-oadd 7516  df-er 7694  df-en 7907  df-dom 7908  df-sdom 7909  df-fin 7910  df-sup 8299  df-oi 8366  df-card 8716  df-pnf 10027  df-mnf 10028  df-xr 10029  df-ltxr 10030  df-le 10031  df-sub 10219  df-neg 10220  df-div 10636  df-nn 10972  df-2 11030  df-3 11031  df-n0 11244  df-z 11329  df-uz 11639  df-rp 11784  df-fz 12276  df-fzo 12414  df-seq 12749  df-exp 12808  df-hash 13065  df-cj 13780  df-re 13781  df-im 13782  df-sqrt 13916  df-abs 13917  df-clim 14160  df-sum 14358
This theorem is referenced by:  oddpwp1fsum  15046
  Copyright terms: Public domain W3C validator