This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 ) )