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	$$⊢\phi \to A\in ℂ$$
	pwm1geoser.n	$$⊢\phi \to N\in {\mathbb{N}}_0$$
Assertion	pwm1geoser	$$⊢\phi \to A^N-1=\left(A-1\right)\sum _{k=0}^{N-1}{A}^k$$

Proof

Step	Hyp	Ref	Expression
1		pwm1geoser.a	$$⊢\phi \to A\in ℂ$$
2		pwm1geoser.n	$$⊢\phi \to N\in {\mathbb{N}}_0$$
3	2	nn0zd	$$⊢\phi \to N\in \mathbb{Z}$$
4		1exp	$$⊢N\in \mathbb{Z}\to 1^N=1$$
5	3 4	syl	$$⊢\phi \to 1^N=1$$
6	5	eqcomd	$$⊢\phi \to 1=1^N$$
7	6	oveq2d	$$⊢\phi \to A^N-1=A^N-1^N$$
8		1cnd	$$⊢\phi \to 1\in ℂ$$
9		pwdif	$$⊢\left(N\in {\mathbb{N}}_0\wedge A\in ℂ\wedge 1\in ℂ\right)\to A^N-1^N=\left(A-1\right)\sum _{k\in \left(0..^N\right)}{A}^k{1}^{N-k-1}$$
10	2 1 8 9	syl3anc	$$⊢\phi \to A^N-1^N=\left(A-1\right)\sum _{k\in \left(0..^N\right)}{A}^k{1}^{N-k-1}$$
11		fzoval	$$⊢N\in \mathbb{Z}\to \left(0..^N\right)=\left(0\dots N-1\right)$$
12	3 11	syl	$$⊢\phi \to \left(0..^N\right)=\left(0\dots N-1\right)$$
13	3	adantr	$$⊢\left(\phi \wedge k\in \left(0..^N\right)\right)\to N\in \mathbb{Z}$$
14		elfzoelz	$$⊢k\in \left(0..^N\right)\to k\in \mathbb{Z}$$
15	14	adantl	$$⊢\left(\phi \wedge k\in \left(0..^N\right)\right)\to k\in \mathbb{Z}$$
16	13 15	zsubcld	$$⊢\left(\phi \wedge k\in \left(0..^N\right)\right)\to N-k\in \mathbb{Z}$$
17		peano2zm	$$⊢N-k\in \mathbb{Z}\to N-k-1\in \mathbb{Z}$$
18		1exp	$$⊢N-k-1\in \mathbb{Z}\to 1^{N-k-1}=1$$
19	16 17 18	3syl	$$⊢\left(\phi \wedge k\in \left(0..^N\right)\right)\to 1^{N-k-1}=1$$
20	19	oveq2d	$$⊢\left(\phi \wedge k\in \left(0..^N\right)\right)\to A^k{1}^{N-k-1}=A^k\cdot 1$$
21	1	adantr	$$⊢\left(\phi \wedge k\in \left(0..^N\right)\right)\to A\in ℂ$$
22		elfzonn0	$$⊢k\in \left(0..^N\right)\to k\in {\mathbb{N}}_0$$
23	22	adantl	$$⊢\left(\phi \wedge k\in \left(0..^N\right)\right)\to k\in {\mathbb{N}}_0$$
24	21 23	expcld	$$⊢\left(\phi \wedge k\in \left(0..^N\right)\right)\to A^k\in ℂ$$
25	24	mulridd	$$⊢\left(\phi \wedge k\in \left(0..^N\right)\right)\to A^k\cdot 1=A^k$$
26	20 25	eqtrd	$$⊢\left(\phi \wedge k\in \left(0..^N\right)\right)\to A^k{1}^{N-k-1}=A^k$$
27	12 26	sumeq12dv	$$⊢\phi \to \sum _{k\in \left(0..^N\right)}{A}^k{1}^{N-k-1}=\sum _{k=0}^{N-1}{A}^k$$
28	27	oveq2d	$$⊢\phi \to \left(A-1\right)\sum _{k\in \left(0..^N\right)}{A}^k{1}^{N-k-1}=\left(A-1\right)\sum _{k=0}^{N-1}{A}^k$$
29	7 10 28	3eqtrd	$$⊢\phi \to A^N-1=\left(A-1\right)\sum _{k=0}^{N-1}{A}^k$$