# 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 ${⊢}\sum _{{k}\in ℕ}\left(\frac{1}{{2}^{{k}}}\right)=1$

### Proof

Step Hyp Ref Expression
1 2cn ${⊢}2\in ℂ$
2 1 a1i ${⊢}{k}\in ℕ\to 2\in ℂ$
3 2ne0 ${⊢}2\ne 0$
4 3 a1i ${⊢}{k}\in ℕ\to 2\ne 0$
5 nnz ${⊢}{k}\in ℕ\to {k}\in ℤ$
6 2 4 5 exprecd ${⊢}{k}\in ℕ\to {\left(\frac{1}{2}\right)}^{{k}}=\frac{1}{{2}^{{k}}}$
7 6 sumeq2i ${⊢}\sum _{{k}\in ℕ}{\left(\frac{1}{2}\right)}^{{k}}=\sum _{{k}\in ℕ}\left(\frac{1}{{2}^{{k}}}\right)$
8 halfcn ${⊢}\frac{1}{2}\in ℂ$
9 halfre ${⊢}\frac{1}{2}\in ℝ$
10 halfge0 ${⊢}0\le \frac{1}{2}$
11 absid ${⊢}\left(\frac{1}{2}\in ℝ\wedge 0\le \frac{1}{2}\right)\to \left|\frac{1}{2}\right|=\frac{1}{2}$
12 9 10 11 mp2an ${⊢}\left|\frac{1}{2}\right|=\frac{1}{2}$
13 halflt1 ${⊢}\frac{1}{2}<1$
14 12 13 eqbrtri ${⊢}\left|\frac{1}{2}\right|<1$
15 geoisum1 ${⊢}\left(\frac{1}{2}\in ℂ\wedge \left|\frac{1}{2}\right|<1\right)\to \sum _{{k}\in ℕ}{\left(\frac{1}{2}\right)}^{{k}}=\frac{\frac{1}{2}}{1-\left(\frac{1}{2}\right)}$
16 8 14 15 mp2an ${⊢}\sum _{{k}\in ℕ}{\left(\frac{1}{2}\right)}^{{k}}=\frac{\frac{1}{2}}{1-\left(\frac{1}{2}\right)}$
17 1mhlfehlf ${⊢}1-\left(\frac{1}{2}\right)=\frac{1}{2}$
18 17 oveq2i ${⊢}\frac{\frac{1}{2}}{1-\left(\frac{1}{2}\right)}=\frac{\frac{1}{2}}{\frac{1}{2}}$
19 ax-1cn ${⊢}1\in ℂ$
20 ax-1ne0 ${⊢}1\ne 0$
21 19 1 20 3 divne0i ${⊢}\frac{1}{2}\ne 0$
22 8 21 dividi ${⊢}\frac{\frac{1}{2}}{\frac{1}{2}}=1$
23 16 18 22 3eqtri ${⊢}\sum _{{k}\in ℕ}{\left(\frac{1}{2}\right)}^{{k}}=1$
24 7 23 eqtr3i ${⊢}\sum _{{k}\in ℕ}\left(\frac{1}{{2}^{{k}}}\right)=1$