Theorem geoisumr

Description: The infinite sum of reciprocals 1 + ( 1 / A ) ^ 1 + ( 1 / A ) ^ 2 ... is A / ( A - 1 ) . (Contributed by rpenner, 3-Nov-2007) (Revised by Mario Carneiro, 26-Apr-2014)

	Ref	Expression
Assertion	geoisumr	⊢ ( ( 𝐴 ∈ ℂ ∧ 1 < ( abs ‘ 𝐴 ) ) → Σ 𝑘 ∈ ℕ0 ( ( 1 / 𝐴 ) ↑ 𝑘 ) = ( 𝐴 / ( 𝐴 − 1 ) ) )

Proof

Step	Hyp	Ref	Expression
1		nn0uz	⊢ ℕ0 = ( ℤ≥ ‘ 0 )
2		0zd	⊢ ( ( 𝐴 ∈ ℂ ∧ 1 < ( abs ‘ 𝐴 ) ) → 0 ∈ ℤ )
3		oveq2	⊢ ( 𝑛 = 𝑘 → ( ( 1 / 𝐴 ) ↑ 𝑛 ) = ( ( 1 / 𝐴 ) ↑ 𝑘 ) )
4		eqid	⊢ ( 𝑛 ∈ ℕ0 ↦ ( ( 1 / 𝐴 ) ↑ 𝑛 ) ) = ( 𝑛 ∈ ℕ0 ↦ ( ( 1 / 𝐴 ) ↑ 𝑛 ) )
5		ovex	⊢ ( ( 1 / 𝐴 ) ↑ 𝑘 ) ∈ V
6	3 4 5	fvmpt	⊢ ( 𝑘 ∈ ℕ0 → ( ( 𝑛 ∈ ℕ0 ↦ ( ( 1 / 𝐴 ) ↑ 𝑛 ) ) ‘ 𝑘 ) = ( ( 1 / 𝐴 ) ↑ 𝑘 ) )
7	6	adantl	⊢ ( ( ( 𝐴 ∈ ℂ ∧ 1 < ( abs ‘ 𝐴 ) ) ∧ 𝑘 ∈ ℕ0 ) → ( ( 𝑛 ∈ ℕ0 ↦ ( ( 1 / 𝐴 ) ↑ 𝑛 ) ) ‘ 𝑘 ) = ( ( 1 / 𝐴 ) ↑ 𝑘 ) )
8		0le1	⊢ 0 ≤ 1
9		0re	⊢ 0 ∈ ℝ
10		1re	⊢ 1 ∈ ℝ
11	9 10	lenlti	⊢ ( 0 ≤ 1 ↔ ¬ 1 < 0 )
12	8 11	mpbi	⊢ ¬ 1 < 0
13		fveq2	⊢ ( 𝐴 = 0 → ( abs ‘ 𝐴 ) = ( abs ‘ 0 ) )
14		abs0	⊢ ( abs ‘ 0 ) = 0
15	13 14	eqtrdi	⊢ ( 𝐴 = 0 → ( abs ‘ 𝐴 ) = 0 )
16	15	breq2d	⊢ ( 𝐴 = 0 → ( 1 < ( abs ‘ 𝐴 ) ↔ 1 < 0 ) )
17	12 16	mtbiri	⊢ ( 𝐴 = 0 → ¬ 1 < ( abs ‘ 𝐴 ) )
18	17	necon2ai	⊢ ( 1 < ( abs ‘ 𝐴 ) → 𝐴 ≠ 0 )
19		reccl	⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ) → ( 1 / 𝐴 ) ∈ ℂ )
20	18 19	sylan2	⊢ ( ( 𝐴 ∈ ℂ ∧ 1 < ( abs ‘ 𝐴 ) ) → ( 1 / 𝐴 ) ∈ ℂ )
21		expcl	⊢ ( ( ( 1 / 𝐴 ) ∈ ℂ ∧ 𝑘 ∈ ℕ0 ) → ( ( 1 / 𝐴 ) ↑ 𝑘 ) ∈ ℂ )
22	20 21	sylan	⊢ ( ( ( 𝐴 ∈ ℂ ∧ 1 < ( abs ‘ 𝐴 ) ) ∧ 𝑘 ∈ ℕ0 ) → ( ( 1 / 𝐴 ) ↑ 𝑘 ) ∈ ℂ )
23		simpl	⊢ ( ( 𝐴 ∈ ℂ ∧ 1 < ( abs ‘ 𝐴 ) ) → 𝐴 ∈ ℂ )
24		simpr	⊢ ( ( 𝐴 ∈ ℂ ∧ 1 < ( abs ‘ 𝐴 ) ) → 1 < ( abs ‘ 𝐴 ) )
25	23 24 7	georeclim	⊢ ( ( 𝐴 ∈ ℂ ∧ 1 < ( abs ‘ 𝐴 ) ) → seq 0 ( + , ( 𝑛 ∈ ℕ0 ↦ ( ( 1 / 𝐴 ) ↑ 𝑛 ) ) ) ⇝ ( 𝐴 / ( 𝐴 − 1 ) ) )
26	1 2 7 22 25	isumclim	⊢ ( ( 𝐴 ∈ ℂ ∧ 1 < ( abs ‘ 𝐴 ) ) → Σ 𝑘 ∈ ℕ0 ( ( 1 / 𝐴 ) ↑ 𝑘 ) = ( 𝐴 / ( 𝐴 − 1 ) ) )