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