Theorem geo2sum2

Description: The value of the finite geometric series 1 + 2 + 4 + 8 + ... + 2 ^ ( N - 1 ) . (Contributed by Mario Carneiro, 7-Sep-2016)

	Ref	Expression
Assertion	geo2sum2	$$⊢N\in {\mathbb{N}}_0\to \sum _{k\in \left(0..^N\right)}{2}^k=2^N-1$$

Proof

Step	Hyp	Ref	Expression
1		nn0z	$$⊢N\in {\mathbb{N}}_0\to N\in \mathbb{Z}$$
2		fzoval	$$⊢N\in \mathbb{Z}\to \left(0..^N\right)=\left(0\dots N-1\right)$$
3	1 2	syl	$$⊢N\in {\mathbb{N}}_0\to \left(0..^N\right)=\left(0\dots N-1\right)$$
4	3	sumeq1d	$$⊢N\in {\mathbb{N}}_0\to \sum _{k\in \left(0..^N\right)}{2}^k=\sum _{k=0}^{N-1}{2}^k$$
5		2cn	$$⊢2\in ℂ$$
6	5	a1i	$$⊢N\in {\mathbb{N}}_0\to 2\in ℂ$$
7		1ne2	$$⊢1\ne 2$$
8	7	necomi	$$⊢2\ne 1$$
9	8	a1i	$$⊢N\in {\mathbb{N}}_0\to 2\ne 1$$
10		id	$$⊢N\in {\mathbb{N}}_0\to N\in {\mathbb{N}}_0$$
11	6 9 10	geoser	$$⊢N\in {\mathbb{N}}_0\to \sum _{k=0}^{N-1}{2}^k=\frac{1-2^N}{1-2}$$
12	6 10	expcld	$$⊢N\in {\mathbb{N}}_0\to 2^N\in ℂ$$
13		ax-1cn	$$⊢1\in ℂ$$
14	13	a1i	$$⊢N\in {\mathbb{N}}_0\to 1\in ℂ$$
15	12 14	subcld	$$⊢N\in {\mathbb{N}}_0\to 2^N-1\in ℂ$$
16		ax-1ne0	$$⊢1\ne 0$$
17	16	a1i	$$⊢N\in {\mathbb{N}}_0\to 1\ne 0$$
18	15 14 17	div2negd	$$⊢N\in {\mathbb{N}}_0\to \frac{-\left(2^N-1\right)}{-1}=\frac{2^N-1}{1}$$
19	12 14	negsubdi2d	$$⊢N\in {\mathbb{N}}_0\to -\left(2^N-1\right)=1-2^N$$
20		2m1e1	$$⊢2-1=1$$
21	20	negeqi	$$⊢-\left(2-1\right)=-1$$
22	5 13	negsubdi2i	$$⊢-\left(2-1\right)=1-2$$
23	21 22	eqtr3i	$$⊢-1=1-2$$
24	23	a1i	$$⊢N\in {\mathbb{N}}_0\to -1=1-2$$
25	19 24	oveq12d	$$⊢N\in {\mathbb{N}}_0\to \frac{-\left(2^N-1\right)}{-1}=\frac{1-2^N}{1-2}$$
26	15	div1d	$$⊢N\in {\mathbb{N}}_0\to \frac{2^N-1}{1}=2^N-1$$
27	18 25 26	3eqtr3d	$$⊢N\in {\mathbb{N}}_0\to \frac{1-2^N}{1-2}=2^N-1$$
28	4 11 27	3eqtrd	$$⊢N\in {\mathbb{N}}_0\to \sum _{k\in \left(0..^N\right)}{2}^k=2^N-1$$