This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 ⊢ ( 𝜑 → 𝐴 ∈ ℂ )
pwm1geoser.n ⊢ ( 𝜑 → 𝑁 ∈ ℕ0 )
Assertion pwm1geoser ( 𝜑 → ( ( 𝐴 ↑ 𝑁 ) − 1 ) = ( ( 𝐴 − 1 ) · Σ 𝑘 ∈ ( 0 ... ( 𝑁 − 1 ) ) ( 𝐴 ↑ 𝑘 ) ) )

Proof

Step Hyp Ref Expression
1 pwm1geoser.a ⊢ ( 𝜑 → 𝐴 ∈ ℂ )
2 pwm1geoser.n ⊢ ( 𝜑 → 𝑁 ∈ ℕ0 )
3 2 nn0zd ⊢ ( 𝜑 → 𝑁 ∈ ℤ )
4 1exp ⊢ ( 𝑁 ∈ ℤ → ( 1 ↑ 𝑁 ) = 1 )
5 3 4 syl ⊢ ( 𝜑 → ( 1 ↑ 𝑁 ) = 1 )
6 5 eqcomd ⊢ ( 𝜑 → 1 = ( 1 ↑ 𝑁 ) )
7 6 oveq2d ⊢ ( 𝜑 → ( ( 𝐴 ↑ 𝑁 ) − 1 ) = ( ( 𝐴 ↑ 𝑁 ) − ( 1 ↑ 𝑁 ) ) )
8 1cnd ⊢ ( 𝜑 → 1 ∈ ℂ )
9 pwdif ⊢ ( ( 𝑁 ∈ ℕ0 ∧ 𝐴 ∈ ℂ ∧ 1 ∈ ℂ ) → ( ( 𝐴 ↑ 𝑁 ) − ( 1 ↑ 𝑁 ) ) = ( ( 𝐴 − 1 ) · Σ 𝑘 ∈ ( 0 ..^ 𝑁 ) ( ( 𝐴 ↑ 𝑘 ) · ( 1 ↑ ( ( 𝑁 − 𝑘 ) − 1 ) ) ) ) )
10 2 1 8 9 syl3anc ⊢ ( 𝜑 → ( ( 𝐴 ↑ 𝑁 ) − ( 1 ↑ 𝑁 ) ) = ( ( 𝐴 − 1 ) · Σ 𝑘 ∈ ( 0 ..^ 𝑁 ) ( ( 𝐴 ↑ 𝑘 ) · ( 1 ↑ ( ( 𝑁 − 𝑘 ) − 1 ) ) ) ) )
11 fzoval ⊢ ( 𝑁 ∈ ℤ → ( 0 ..^ 𝑁 ) = ( 0 ... ( 𝑁 − 1 ) ) )
12 3 11 syl ⊢ ( 𝜑 → ( 0 ..^ 𝑁 ) = ( 0 ... ( 𝑁 − 1 ) ) )
13 3 adantr ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 0 ..^ 𝑁 ) ) → 𝑁 ∈ ℤ )
14 elfzoelz ⊢ ( 𝑘 ∈ ( 0 ..^ 𝑁 ) → 𝑘 ∈ ℤ )
15 14 adantl ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 0 ..^ 𝑁 ) ) → 𝑘 ∈ ℤ )
16 13 15 zsubcld ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 0 ..^ 𝑁 ) ) → ( 𝑁 − 𝑘 ) ∈ ℤ )
17 peano2zm ⊢ ( ( 𝑁 − 𝑘 ) ∈ ℤ → ( ( 𝑁 − 𝑘 ) − 1 ) ∈ ℤ )
18 1exp ⊢ ( ( ( 𝑁 − 𝑘 ) − 1 ) ∈ ℤ → ( 1 ↑ ( ( 𝑁 − 𝑘 ) − 1 ) ) = 1 )
19 16 17 18 3syl ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 0 ..^ 𝑁 ) ) → ( 1 ↑ ( ( 𝑁 − 𝑘 ) − 1 ) ) = 1 )
20 19 oveq2d ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 0 ..^ 𝑁 ) ) → ( ( 𝐴 ↑ 𝑘 ) · ( 1 ↑ ( ( 𝑁 − 𝑘 ) − 1 ) ) ) = ( ( 𝐴 ↑ 𝑘 ) · 1 ) )
21 1 adantr ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 0 ..^ 𝑁 ) ) → 𝐴 ∈ ℂ )
22 elfzonn0 ⊢ ( 𝑘 ∈ ( 0 ..^ 𝑁 ) → 𝑘 ∈ ℕ0 )
23 22 adantl ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 0 ..^ 𝑁 ) ) → 𝑘 ∈ ℕ0 )
24 21 23 expcld ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 0 ..^ 𝑁 ) ) → ( 𝐴 ↑ 𝑘 ) ∈ ℂ )
25 24 mulridd ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 0 ..^ 𝑁 ) ) → ( ( 𝐴 ↑ 𝑘 ) · 1 ) = ( 𝐴 ↑ 𝑘 ) )
26 20 25 eqtrd ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 0 ..^ 𝑁 ) ) → ( ( 𝐴 ↑ 𝑘 ) · ( 1 ↑ ( ( 𝑁 − 𝑘 ) − 1 ) ) ) = ( 𝐴 ↑ 𝑘 ) )
27 12 26 sumeq12dv ⊢ ( 𝜑 → Σ 𝑘 ∈ ( 0 ..^ 𝑁 ) ( ( 𝐴 ↑ 𝑘 ) · ( 1 ↑ ( ( 𝑁 − 𝑘 ) − 1 ) ) ) = Σ 𝑘 ∈ ( 0 ... ( 𝑁 − 1 ) ) ( 𝐴 ↑ 𝑘 ) )
28 27 oveq2d ⊢ ( 𝜑 → ( ( 𝐴 − 1 ) · Σ 𝑘 ∈ ( 0 ..^ 𝑁 ) ( ( 𝐴 ↑ 𝑘 ) · ( 1 ↑ ( ( 𝑁 − 𝑘 ) − 1 ) ) ) ) = ( ( 𝐴 − 1 ) · Σ 𝑘 ∈ ( 0 ... ( 𝑁 − 1 ) ) ( 𝐴 ↑ 𝑘 ) ) )
29 7 10 28 3eqtrd ⊢ ( 𝜑 → ( ( 𝐴 ↑ 𝑁 ) − 1 ) = ( ( 𝐴 − 1 ) · Σ 𝑘 ∈ ( 0 ... ( 𝑁 − 1 ) ) ( 𝐴 ↑ 𝑘 ) ) )