Metamath Proof Explorer


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 A 1 < A k 0 1 A k = A A 1

Proof

Step Hyp Ref Expression
1 nn0uz 0 = 0
2 0zd A 1 < A 0
3 oveq2 n = k 1 A n = 1 A k
4 eqid n 0 1 A n = n 0 1 A n
5 ovex 1 A k V
6 3 4 5 fvmpt k 0 n 0 1 A n k = 1 A k
7 6 adantl A 1 < A k 0 n 0 1 A n k = 1 A k
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 A = 0 A = 0
14 abs0 0 = 0
15 13 14 eqtrdi A = 0 A = 0
16 15 breq2d A = 0 1 < A 1 < 0
17 12 16 mtbiri A = 0 ¬ 1 < A
18 17 necon2ai 1 < A A 0
19 reccl A A 0 1 A
20 18 19 sylan2 A 1 < A 1 A
21 expcl 1 A k 0 1 A k
22 20 21 sylan A 1 < A k 0 1 A k
23 simpl A 1 < A A
24 simpr A 1 < A 1 < A
25 23 24 7 georeclim A 1 < A seq 0 + n 0 1 A n A A 1
26 1 2 7 22 25 isumclim A 1 < A k 0 1 A k = A A 1