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 \mathbb{N}}\left(\frac{1}{2^k}\right)=1$$

Proof

Step	Hyp	Ref	Expression
1		2cn	$$⊢2\in ℂ$$
2	1	a1i	$$⊢k\in \mathbb{N}\to 2\in ℂ$$
3		2ne0	$$⊢2\ne 0$$
4	3	a1i	$$⊢k\in \mathbb{N}\to 2\ne 0$$
5		nnz	$$⊢k\in \mathbb{N}\to k\in \mathbb{Z}$$
6	2 4 5	exprecd	$$⊢k\in \mathbb{N}\to {\left(\frac{1}{2}\right)}^k=\frac{1}{2^k}$$
7	6	sumeq2i	$$⊢\sum _{k\in \mathbb{N}}{\left(\frac{1}{2}\right)}^k=\sum _{k\in \mathbb{N}}\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 \mathbb{N}}{\left(\frac{1}{2}\right)}^k=\frac{\frac{1}{2}}{1-\left(\frac{1}{2}\right)}$$
16	8 14 15	mp2an	$$⊢\sum _{k\in \mathbb{N}}{\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 \mathbb{N}}{\left(\frac{1}{2}\right)}^k=1$$
24	7 23	eqtr3i	$$⊢\sum _{k\in \mathbb{N}}\left(\frac{1}{2^k}\right)=1$$