Metamath Proof Explorer

Theorem pwm1geoser

Description: The n-th power of a number decreased by 1 expressed by the finite geometric series 1 + A ^ 1 + A ^ 2 + ... + A ^ ( N - 1 ) . (Contributed by AV, 14-Aug-2021) (Proof shortened by AV, 19-Aug-2021)

Ref Expression
Hypotheses pwm1geoser.a ⊢ φ → A ∈ ℂ
pwm1geoser.n ⊢ φ → N ∈ ℕ 0
Assertion pwm1geoser ⊢ φ → A N − 1 = A − 1 ⁢ ∑ k = 0 N − 1 A k

Proof

Step Hyp Ref Expression
1 pwm1geoser.a ⊢ φ → A ∈ ℂ
2 pwm1geoser.n ⊢ φ → N ∈ ℕ 0
3 2 nn0zd ⊢ φ → N ∈ ℤ
4 1exp ⊢ N ∈ ℤ → 1 N = 1
5 3 4 syl ⊢ φ → 1 N = 1
6 5 eqcomd ⊢ φ → 1 = 1 N
7 6 oveq2d ⊢ φ → A N − 1 = A N − 1 N
8 1cnd ⊢ φ → 1 ∈ ℂ
9 pwdif ⊢ N ∈ ℕ 0 ∧ A ∈ ℂ ∧ 1 ∈ ℂ → A N − 1 N = A − 1 ⁢ ∑ k ∈ 0 ..^ N A k ⁢ 1 N - k - 1
10 2 1 8 9 syl3anc ⊢ φ → A N − 1 N = A − 1 ⁢ ∑ k ∈ 0 ..^ N A k ⁢ 1 N - k - 1
11 fzoval ⊢ N ∈ ℤ → 0 ..^ N = 0 … N − 1
12 3 11 syl ⊢ φ → 0 ..^ N = 0 … N − 1
13 3 adantr ⊢ φ ∧ k ∈ 0 ..^ N → N ∈ ℤ
14 elfzoelz ⊢ k ∈ 0 ..^ N → k ∈ ℤ
15 14 adantl ⊢ φ ∧ k ∈ 0 ..^ N → k ∈ ℤ
16 13 15 zsubcld ⊢ φ ∧ k ∈ 0 ..^ N → N − k ∈ ℤ
17 peano2zm ⊢ N − k ∈ ℤ → N - k - 1 ∈ ℤ
18 1exp ⊢ N - k - 1 ∈ ℤ → 1 N - k - 1 = 1
19 16 17 18 3syl ⊢ φ ∧ k ∈ 0 ..^ N → 1 N - k - 1 = 1
20 19 oveq2d ⊢ φ ∧ k ∈ 0 ..^ N → A k ⁢ 1 N - k - 1 = A k ⋅ 1
21 1 adantr ⊢ φ ∧ k ∈ 0 ..^ N → A ∈ ℂ
22 elfzonn0 ⊢ k ∈ 0 ..^ N → k ∈ ℕ 0
23 22 adantl ⊢ φ ∧ k ∈ 0 ..^ N → k ∈ ℕ 0
24 21 23 expcld ⊢ φ ∧ k ∈ 0 ..^ N → A k ∈ ℂ
25 24 mulid1d ⊢ φ ∧ k ∈ 0 ..^ N → A k ⋅ 1 = A k
26 20 25 eqtrd ⊢ φ ∧ k ∈ 0 ..^ N → A k ⁢ 1 N - k - 1 = A k
27 12 26 sumeq12dv ⊢ φ → ∑ k ∈ 0 ..^ N A k ⁢ 1 N - k - 1 = ∑ k = 0 N − 1 A k
28 27 oveq2d ⊢ φ → A − 1 ⁢ ∑ k ∈ 0 ..^ N A k ⁢ 1 N - k - 1 = A − 1 ⁢ ∑ k = 0 N − 1 A k
29 7 10 28 3eqtrd ⊢ φ → A N − 1 = A − 1 ⁢ ∑ k = 0 N − 1 A k