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	⊢ Σ 𝑘 ∈ ℕ ( 1 / ( 2 ↑ 𝑘 ) ) = 1

Proof

Step	Hyp	Ref	Expression
1		2cn	⊢ 2 ∈ ℂ
2	1	a1i	⊢ ( 𝑘 ∈ ℕ → 2 ∈ ℂ )
3		2ne0	⊢ 2 ≠ 0
4	3	a1i	⊢ ( 𝑘 ∈ ℕ → 2 ≠ 0 )
5		nnz	⊢ ( 𝑘 ∈ ℕ → 𝑘 ∈ ℤ )
6	2 4 5	exprecd	⊢ ( 𝑘 ∈ ℕ → ( ( 1 / 2 ) ↑ 𝑘 ) = ( 1 / ( 2 ↑ 𝑘 ) ) )
7	6	sumeq2i	⊢ Σ 𝑘 ∈ ℕ ( ( 1 / 2 ) ↑ 𝑘 ) = Σ 𝑘 ∈ ℕ ( 1 / ( 2 ↑ 𝑘 ) )
8		halfcn	⊢ ( 1 / 2 ) ∈ ℂ
9		halfre	⊢ ( 1 / 2 ) ∈ ℝ
10		halfge0	⊢ 0 ≤ ( 1 / 2 )
11		absid	⊢ ( ( ( 1 / 2 ) ∈ ℝ ∧ 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 ) ∈ ℂ ∧ ( abs ‘ ( 1 / 2 ) ) < 1 ) → Σ 𝑘 ∈ ℕ ( ( 1 / 2 ) ↑ 𝑘 ) = ( ( 1 / 2 ) / ( 1 − ( 1 / 2 ) ) ) )
16	8 14 15	mp2an	⊢ Σ 𝑘 ∈ ℕ ( ( 1 / 2 ) ↑ 𝑘 ) = ( ( 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	⊢ Σ 𝑘 ∈ ℕ ( ( 1 / 2 ) ↑ 𝑘 ) = 1
24	7 23	eqtr3i	⊢ Σ 𝑘 ∈ ℕ ( 1 / ( 2 ↑ 𝑘 ) ) = 1