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	⊢ ( 𝑁 ∈ ℕ0 → Σ 𝑘 ∈ ( 0 ..^ 𝑁 ) ( 2 ↑ 𝑘 ) = ( ( 2 ↑ 𝑁 ) − 1 ) )

Proof

Step	Hyp	Ref	Expression
1		nn0z	⊢ ( 𝑁 ∈ ℕ0 → 𝑁 ∈ ℤ )
2		fzoval	⊢ ( 𝑁 ∈ ℤ → ( 0 ..^ 𝑁 ) = ( 0 ... ( 𝑁 − 1 ) ) )
3	1 2	syl	⊢ ( 𝑁 ∈ ℕ0 → ( 0 ..^ 𝑁 ) = ( 0 ... ( 𝑁 − 1 ) ) )
4	3	sumeq1d	⊢ ( 𝑁 ∈ ℕ0 → Σ 𝑘 ∈ ( 0 ..^ 𝑁 ) ( 2 ↑ 𝑘 ) = Σ 𝑘 ∈ ( 0 ... ( 𝑁 − 1 ) ) ( 2 ↑ 𝑘 ) )
5		2cn	⊢ 2 ∈ ℂ
6	5	a1i	⊢ ( 𝑁 ∈ ℕ0 → 2 ∈ ℂ )
7		1ne2	⊢ 1 ≠ 2
8	7	necomi	⊢ 2 ≠ 1
9	8	a1i	⊢ ( 𝑁 ∈ ℕ0 → 2 ≠ 1 )
10		id	⊢ ( 𝑁 ∈ ℕ0 → 𝑁 ∈ ℕ0 )
11	6 9 10	geoser	⊢ ( 𝑁 ∈ ℕ0 → Σ 𝑘 ∈ ( 0 ... ( 𝑁 − 1 ) ) ( 2 ↑ 𝑘 ) = ( ( 1 − ( 2 ↑ 𝑁 ) ) / ( 1 − 2 ) ) )
12	6 10	expcld	⊢ ( 𝑁 ∈ ℕ0 → ( 2 ↑ 𝑁 ) ∈ ℂ )
13		ax-1cn	⊢ 1 ∈ ℂ
14	13	a1i	⊢ ( 𝑁 ∈ ℕ0 → 1 ∈ ℂ )
15	12 14	subcld	⊢ ( 𝑁 ∈ ℕ0 → ( ( 2 ↑ 𝑁 ) − 1 ) ∈ ℂ )
16		ax-1ne0	⊢ 1 ≠ 0
17	16	a1i	⊢ ( 𝑁 ∈ ℕ0 → 1 ≠ 0 )
18	15 14 17	div2negd	⊢ ( 𝑁 ∈ ℕ0 → ( - ( ( 2 ↑ 𝑁 ) − 1 ) / - 1 ) = ( ( ( 2 ↑ 𝑁 ) − 1 ) / 1 ) )
19	12 14	negsubdi2d	⊢ ( 𝑁 ∈ ℕ0 → - ( ( 2 ↑ 𝑁 ) − 1 ) = ( 1 − ( 2 ↑ 𝑁 ) ) )
20		2m1e1	⊢ ( 2 − 1 ) = 1
21	20	negeqi	⊢ - ( 2 − 1 ) = - 1
22	5 13	negsubdi2i	⊢ - ( 2 − 1 ) = ( 1 − 2 )
23	21 22	eqtr3i	⊢ - 1 = ( 1 − 2 )
24	23	a1i	⊢ ( 𝑁 ∈ ℕ0 → - 1 = ( 1 − 2 ) )
25	19 24	oveq12d	⊢ ( 𝑁 ∈ ℕ0 → ( - ( ( 2 ↑ 𝑁 ) − 1 ) / - 1 ) = ( ( 1 − ( 2 ↑ 𝑁 ) ) / ( 1 − 2 ) ) )
26	15	div1d	⊢ ( 𝑁 ∈ ℕ0 → ( ( ( 2 ↑ 𝑁 ) − 1 ) / 1 ) = ( ( 2 ↑ 𝑁 ) − 1 ) )
27	18 25 26	3eqtr3d	⊢ ( 𝑁 ∈ ℕ0 → ( ( 1 − ( 2 ↑ 𝑁 ) ) / ( 1 − 2 ) ) = ( ( 2 ↑ 𝑁 ) − 1 ) )
28	4 11 27	3eqtrd	⊢ ( 𝑁 ∈ ℕ0 → Σ 𝑘 ∈ ( 0 ..^ 𝑁 ) ( 2 ↑ 𝑘 ) = ( ( 2 ↑ 𝑁 ) − 1 ) )