This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 eqtrdi ⊢ ( 𝐴 = 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 eqtrdi ⊢ ( 𝜑 → ( 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 eqtrdi ⊢ ( 𝐴 = 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 ) ) )