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 ) ) ( 𝐴 ↑ 𝑘 ) ) )