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

Metamath Proof Explorer

Theorem geoihalfsum

Description: Prove that the infinite geometric series of 1/2, 1/2 + 1/4 + 1/8 + ... = 1. Uses geoisum1 . This is a representation of .111... in binary with an infinite number of 1's. Theorem 0.999... proves a similar claim for .999... in base 10. (Contributed by David A. Wheeler, 4-Jan-2017) (Proof shortened by AV, 9-Jul-2022)

Ref Expression
Assertion geoihalfsum ⊢ ∑ k ∈ ℕ 1 2 k = 1

Proof

Step Hyp Ref Expression
1 2cn ⊢ 2 ∈ ℂ
2 1 a1i ⊢ k ∈ ℕ → 2 ∈ ℂ
3 2ne0 ⊢ 2 ≠ 0
4 3 a1i ⊢ k ∈ ℕ → 2 ≠ 0
5 nnz ⊢ k ∈ ℕ → k ∈ ℤ
6 2 4 5 exprecd ⊢ k ∈ ℕ → 1 2 k = 1 2 k
7 6 sumeq2i ⊢ ∑ k ∈ ℕ 1 2 k = ∑ k ∈ ℕ 1 2 k
8 halfcn ⊢ 1 2 ∈ ℂ
9 halfre ⊢ 1 2 ∈ ℝ
10 halfge0 ⊢ 0 ≤ 1 2
11 absid ⊢ 1 2 ∈ ℝ ∧ 0 ≤ 1 2 → 1 2 = 1 2
12 9 10 11 mp2an ⊢ 1 2 = 1 2
13 halflt1 ⊢ 1 2 < 1
14 12 13 eqbrtri ⊢ 1 2 < 1
15 geoisum1 ⊢ 1 2 ∈ ℂ ∧ 1 2 < 1 → ∑ k ∈ ℕ 1 2 k = 1 2 1 − 1 2
16 8 14 15 mp2an ⊢ ∑ k ∈ ℕ 1 2 k = 1 2 1 − 1 2
17 1mhlfehlf ⊢ 1 − 1 2 = 1 2
18 17 oveq2i ⊢ 1 2 1 − 1 2 = 1 2 1 2
19 ax-1cn ⊢ 1 ∈ ℂ
20 ax-1ne0 ⊢ 1 ≠ 0
21 19 1 20 3 divne0i ⊢ 1 2 ≠ 0
22 8 21 dividi ⊢ 1 2 1 2 = 1
23 16 18 22 3eqtri ⊢ ∑ k ∈ ℕ 1 2 k = 1
24 7 23 eqtr3i ⊢ ∑ k ∈ ℕ 1 2 k = 1