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 ⊢ φ → A ∈ ℂ
georeclim.2 ⊢ φ → 1 < A
georeclim.3 ⊢ φ ∧ k ∈ ℕ 0 → F ⁡ k = 1 A k
Assertion georeclim ⊢ φ → seq 0 + F ⇝ A A − 1

Proof

Step Hyp Ref Expression
1 georeclim.1 ⊢ φ → A ∈ ℂ
2 georeclim.2 ⊢ φ → 1 < A
3 georeclim.3 ⊢ φ ∧ k ∈ ℕ 0 → F ⁡ k = 1 A k
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 ⊢ A = 0 → A = 0
10 abs0 ⊢ 0 = 0
11 9 10 eqtrdi ⊢ A = 0 → A = 0
12 11 breq2d ⊢ A = 0 → 1 < A ↔ 1 < 0
13 8 12 mtbiri ⊢ A = 0 → ¬ 1 < A
14 13 necon2ai ⊢ 1 < A → A ≠ 0
15 2 14 syl ⊢ φ → A ≠ 0
16 1 15 reccld ⊢ φ → 1 A ∈ ℂ
17 1cnd ⊢ φ → 1 ∈ ℂ
18 17 1 15 absdivd ⊢ φ → 1 A = 1 A
19 abs1 ⊢ 1 = 1
20 19 oveq1i ⊢ 1 A = 1 A
21 18 20 eqtrdi ⊢ φ → 1 A = 1 A
22 1 15 absrpcld ⊢ φ → A ∈ ℝ +
23 22 recgt1d ⊢ φ → 1 < A ↔ 1 A < 1
24 2 23 mpbid ⊢ φ → 1 A < 1
25 21 24 eqbrtrd ⊢ φ → 1 A < 1
26 16 25 3 geolim ⊢ φ → seq 0 + F ⇝ 1 1 − 1 A
27 1 17 1 15 divsubdird ⊢ φ → A − 1 A = A A − 1 A
28 1 15 dividd ⊢ φ → A A = 1
29 28 oveq1d ⊢ φ → A A − 1 A = 1 − 1 A
30 27 29 eqtrd ⊢ φ → A − 1 A = 1 − 1 A
31 30 oveq2d ⊢ φ → 1 A − 1 A = 1 1 − 1 A
32 ax-1cn ⊢ 1 ∈ ℂ
33 subcl ⊢ A ∈ ℂ ∧ 1 ∈ ℂ → A − 1 ∈ ℂ
34 1 32 33 sylancl ⊢ φ → A − 1 ∈ ℂ
35 6 ltnri ⊢ ¬ 1 < 1
36 fveq2 ⊢ A = 1 → A = 1
37 36 19 eqtrdi ⊢ A = 1 → A = 1
38 37 breq2d ⊢ A = 1 → 1 < A ↔ 1 < 1
39 35 38 mtbiri ⊢ A = 1 → ¬ 1 < A
40 39 necon2ai ⊢ 1 < A → A ≠ 1
41 2 40 syl ⊢ φ → A ≠ 1
42 subeq0 ⊢ A ∈ ℂ ∧ 1 ∈ ℂ → A − 1 = 0 ↔ A = 1
43 1 32 42 sylancl ⊢ φ → A − 1 = 0 ↔ A = 1
44 43 necon3bid ⊢ φ → A − 1 ≠ 0 ↔ A ≠ 1
45 41 44 mpbird ⊢ φ → A − 1 ≠ 0
46 34 1 45 15 recdivd ⊢ φ → 1 A − 1 A = A A − 1
47 31 46 eqtr3d ⊢ φ → 1 1 − 1 A = A A − 1
48 26 47 breqtrd ⊢ φ → seq 0 + F ⇝ A A − 1