Theorem geoser

Description: The value of the finite geometric series 1 + A ^ 1 + A ^ 2 + ... + A ^ ( N - 1 ) . This is Metamath 100 proof #66. (Contributed by NM, 12-May-2006) (Proof shortened by Mario Carneiro, 15-Jun-2014)

	Ref	Expression
Hypotheses	geoser.1	$$⊢\phi \to A\in ℂ$$
	geoser.2	$$⊢\phi \to A\ne 1$$
	geoser.3	$$⊢\phi \to N\in {\mathbb{N}}_0$$
Assertion	geoser	$$⊢\phi \to \sum _{k=0}^{N-1}{A}^k=\frac{1-A^N}{1-A}$$

Proof

Step	Hyp	Ref	Expression
1		geoser.1	$$⊢\phi \to A\in ℂ$$
2		geoser.2	$$⊢\phi \to A\ne 1$$
3		geoser.3	$$⊢\phi \to N\in {\mathbb{N}}_0$$
4		0nn0	$$⊢0\in {\mathbb{N}}_0$$
5	4	a1i	$$⊢\phi \to 0\in {\mathbb{N}}_0$$
6		nn0uz	$$⊢{\mathbb{N}}_0={\mathbb{Z}}_{\ge 0}$$
7	3 6	eleqtrdi	$$⊢\phi \to N\in {\mathbb{Z}}_{\ge 0}$$
8	1 2 5 7	geoserg	$$⊢\phi \to \sum _{k\in \left(0..^N\right)}{A}^k=\frac{A^0-A^N}{1-A}$$
9	3	nn0zd	$$⊢\phi \to N\in \mathbb{Z}$$
10		fzoval	$$⊢N\in \mathbb{Z}\to \left(0..^N\right)=\left(0\dots N-1\right)$$
11	9 10	syl	$$⊢\phi \to \left(0..^N\right)=\left(0\dots N-1\right)$$
12	11	sumeq1d	$$⊢\phi \to \sum _{k\in \left(0..^N\right)}{A}^k=\sum _{k=0}^{N-1}{A}^k$$
13	1	exp0d	$$⊢\phi \to A^0=1$$
14	13	oveq1d	$$⊢\phi \to A^0-A^N=1-A^N$$
15	14	oveq1d	$$⊢\phi \to \frac{A^0-A^N}{1-A}=\frac{1-A^N}{1-A}$$
16	8 12 15	3eqtr3d	$$⊢\phi \to \sum _{k=0}^{N-1}{A}^k=\frac{1-A^N}{1-A}$$