Metamath Proof Explorer


Theorem georeclim

Description: The limit of a geometric series of reciprocals. (Contributed by Paul Chapman, 28-Dec-2007) (Revised by Mario Carneiro, 26-Apr-2014)

Ref Expression
Hypotheses georeclim.1 ( 𝜑𝐴 ∈ ℂ )
georeclim.2 ( 𝜑 → 1 < ( abs ‘ 𝐴 ) )
georeclim.3 ( ( 𝜑𝑘 ∈ ℕ0 ) → ( 𝐹𝑘 ) = ( ( 1 / 𝐴 ) ↑ 𝑘 ) )
Assertion georeclim ( 𝜑 → seq 0 ( + , 𝐹 ) ⇝ ( 𝐴 / ( 𝐴 − 1 ) ) )

Proof

Step Hyp Ref Expression
1 georeclim.1 ( 𝜑𝐴 ∈ ℂ )
2 georeclim.2 ( 𝜑 → 1 < ( abs ‘ 𝐴 ) )
3 georeclim.3 ( ( 𝜑𝑘 ∈ ℕ0 ) → ( 𝐹𝑘 ) = ( ( 1 / 𝐴 ) ↑ 𝑘 ) )
4 0le1 0 ≤ 1
5 0re 0 ∈ ℝ
6 1re 1 ∈ ℝ
7 5 6 lenlti ( 0 ≤ 1 ↔ ¬ 1 < 0 )
8 4 7 mpbi ¬ 1 < 0
9 fveq2 ( 𝐴 = 0 → ( abs ‘ 𝐴 ) = ( abs ‘ 0 ) )
10 abs0 ( abs ‘ 0 ) = 0
11 9 10 syl6eq ( 𝐴 = 0 → ( abs ‘ 𝐴 ) = 0 )
12 11 breq2d ( 𝐴 = 0 → ( 1 < ( abs ‘ 𝐴 ) ↔ 1 < 0 ) )
13 8 12 mtbiri ( 𝐴 = 0 → ¬ 1 < ( abs ‘ 𝐴 ) )
14 13 necon2ai ( 1 < ( abs ‘ 𝐴 ) → 𝐴 ≠ 0 )
15 2 14 syl ( 𝜑𝐴 ≠ 0 )
16 1 15 reccld ( 𝜑 → ( 1 / 𝐴 ) ∈ ℂ )
17 1cnd ( 𝜑 → 1 ∈ ℂ )
18 17 1 15 absdivd ( 𝜑 → ( abs ‘ ( 1 / 𝐴 ) ) = ( ( abs ‘ 1 ) / ( abs ‘ 𝐴 ) ) )
19 abs1 ( abs ‘ 1 ) = 1
20 19 oveq1i ( ( abs ‘ 1 ) / ( abs ‘ 𝐴 ) ) = ( 1 / ( abs ‘ 𝐴 ) )
21 18 20 syl6eq ( 𝜑 → ( abs ‘ ( 1 / 𝐴 ) ) = ( 1 / ( abs ‘ 𝐴 ) ) )
22 1 15 absrpcld ( 𝜑 → ( abs ‘ 𝐴 ) ∈ ℝ+ )
23 22 recgt1d ( 𝜑 → ( 1 < ( abs ‘ 𝐴 ) ↔ ( 1 / ( abs ‘ 𝐴 ) ) < 1 ) )
24 2 23 mpbid ( 𝜑 → ( 1 / ( abs ‘ 𝐴 ) ) < 1 )
25 21 24 eqbrtrd ( 𝜑 → ( abs ‘ ( 1 / 𝐴 ) ) < 1 )
26 16 25 3 geolim ( 𝜑 → seq 0 ( + , 𝐹 ) ⇝ ( 1 / ( 1 − ( 1 / 𝐴 ) ) ) )
27 1 17 1 15 divsubdird ( 𝜑 → ( ( 𝐴 − 1 ) / 𝐴 ) = ( ( 𝐴 / 𝐴 ) − ( 1 / 𝐴 ) ) )
28 1 15 dividd ( 𝜑 → ( 𝐴 / 𝐴 ) = 1 )
29 28 oveq1d ( 𝜑 → ( ( 𝐴 / 𝐴 ) − ( 1 / 𝐴 ) ) = ( 1 − ( 1 / 𝐴 ) ) )
30 27 29 eqtrd ( 𝜑 → ( ( 𝐴 − 1 ) / 𝐴 ) = ( 1 − ( 1 / 𝐴 ) ) )
31 30 oveq2d ( 𝜑 → ( 1 / ( ( 𝐴 − 1 ) / 𝐴 ) ) = ( 1 / ( 1 − ( 1 / 𝐴 ) ) ) )
32 ax-1cn 1 ∈ ℂ
33 subcl ( ( 𝐴 ∈ ℂ ∧ 1 ∈ ℂ ) → ( 𝐴 − 1 ) ∈ ℂ )
34 1 32 33 sylancl ( 𝜑 → ( 𝐴 − 1 ) ∈ ℂ )
35 6 ltnri ¬ 1 < 1
36 fveq2 ( 𝐴 = 1 → ( abs ‘ 𝐴 ) = ( abs ‘ 1 ) )
37 36 19 syl6eq ( 𝐴 = 1 → ( abs ‘ 𝐴 ) = 1 )
38 37 breq2d ( 𝐴 = 1 → ( 1 < ( abs ‘ 𝐴 ) ↔ 1 < 1 ) )
39 35 38 mtbiri ( 𝐴 = 1 → ¬ 1 < ( abs ‘ 𝐴 ) )
40 39 necon2ai ( 1 < ( abs ‘ 𝐴 ) → 𝐴 ≠ 1 )
41 2 40 syl ( 𝜑𝐴 ≠ 1 )
42 subeq0 ( ( 𝐴 ∈ ℂ ∧ 1 ∈ ℂ ) → ( ( 𝐴 − 1 ) = 0 ↔ 𝐴 = 1 ) )
43 1 32 42 sylancl ( 𝜑 → ( ( 𝐴 − 1 ) = 0 ↔ 𝐴 = 1 ) )
44 43 necon3bid ( 𝜑 → ( ( 𝐴 − 1 ) ≠ 0 ↔ 𝐴 ≠ 1 ) )
45 41 44 mpbird ( 𝜑 → ( 𝐴 − 1 ) ≠ 0 )
46 34 1 45 15 recdivd ( 𝜑 → ( 1 / ( ( 𝐴 − 1 ) / 𝐴 ) ) = ( 𝐴 / ( 𝐴 − 1 ) ) )
47 31 46 eqtr3d ( 𝜑 → ( 1 / ( 1 − ( 1 / 𝐴 ) ) ) = ( 𝐴 / ( 𝐴 − 1 ) ) )
48 26 47 breqtrd ( 𝜑 → seq 0 ( + , 𝐹 ) ⇝ ( 𝐴 / ( 𝐴 − 1 ) ) )