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 e. NN ( 1 / ( 2 ^ k ) ) = 1

Proof

Step	Hyp	Ref	Expression
1		2cn	|- 2 e. CC
2	1	a1i	|- ( k e. NN -> 2 e. CC )
3		2ne0	|- 2 =/= 0
4	3	a1i	|- ( k e. NN -> 2 =/= 0 )
5		nnz	|- ( k e. NN -> k e. ZZ )
6	2 4 5	exprecd	|- ( k e. NN -> ( ( 1 / 2 ) ^ k ) = ( 1 / ( 2 ^ k ) ) )
7	6	sumeq2i	|- sum_ k e. NN ( ( 1 / 2 ) ^ k ) = sum_ k e. NN ( 1 / ( 2 ^ k ) )
8		halfcn	|- ( 1 / 2 ) e. CC
9		halfre	|- ( 1 / 2 ) e. RR
10		halfge0	|- 0 <_ ( 1 / 2 )
11		absid	|- ( ( ( 1 / 2 ) e. RR /\ 0 <_ ( 1 / 2 ) ) -> ( abs ` ( 1 / 2 ) ) = ( 1 / 2 ) )
12	9 10 11	mp2an	|- ( abs ` ( 1 / 2 ) ) = ( 1 / 2 )
13		halflt1	|- ( 1 / 2 ) < 1
14	12 13	eqbrtri	|- ( abs ` ( 1 / 2 ) ) < 1
15		geoisum1	|- ( ( ( 1 / 2 ) e. CC /\ ( abs ` ( 1 / 2 ) ) < 1 ) -> sum_ k e. NN ( ( 1 / 2 ) ^ k ) = ( ( 1 / 2 ) / ( 1 - ( 1 / 2 ) ) ) )
16	8 14 15	mp2an	|- sum_ k e. NN ( ( 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 e. CC
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	|- sum_ k e. NN ( ( 1 / 2 ) ^ k ) = 1
24	7 23	eqtr3i	|- sum_ k e. NN ( 1 / ( 2 ^ k ) ) = 1