Metamath Proof Explorer

Theorem geolim3

Description: Geometric series convergence with arbitrary shift, radix, and multiplicative constant. (Contributed by Stefan O'Rear, 16-Nov-2014)

Ref Expression
Hypotheses geolim3.a ⊢ φ → A ∈ ℤ
geolim3.b1 ⊢ φ → B ∈ ℂ
geolim3.b2 ⊢ φ → B < 1
geolim3.c ⊢ φ → C ∈ ℂ
geolim3.f ⊢ F = k ∈ ℤ ≥ A ⟼ C ⁢ B k − A
Assertion geolim3 ⊢ φ → seq A + F ⇝ C 1 − B

Proof

Step Hyp Ref Expression
1 geolim3.a ⊢ φ → A ∈ ℤ
2 geolim3.b1 ⊢ φ → B ∈ ℂ
3 geolim3.b2 ⊢ φ → B < 1
4 geolim3.c ⊢ φ → C ∈ ℂ
5 geolim3.f ⊢ F = k ∈ ℤ ≥ A ⟼ C ⁢ B k − A
6 seqeq3 ⊢ F = k ∈ ℤ ≥ A ⟼ C ⁢ B k − A → seq A + F = seq A + k ∈ ℤ ≥ A ⟼ C ⁢ B k − A
7 5 6 ax-mp ⊢ seq A + F = seq A + k ∈ ℤ ≥ A ⟼ C ⁢ B k − A
8 nn0uz ⊢ ℕ 0 = ℤ ≥ 0
9 0zd ⊢ φ → 0 ∈ ℤ
10 oveq2 ⊢ k = a → B k = B a
11 eqid ⊢ k ∈ ℕ 0 ⟼ B k = k ∈ ℕ 0 ⟼ B k
12 ovex ⊢ B a ∈ V
13 10 11 12 fvmpt ⊢ a ∈ ℕ 0 → k ∈ ℕ 0 ⟼ B k ⁡ a = B a
14 13 adantl ⊢ φ ∧ a ∈ ℕ 0 → k ∈ ℕ 0 ⟼ B k ⁡ a = B a
15 2 3 14 geolim ⊢ φ → seq 0 + k ∈ ℕ 0 ⟼ B k ⇝ 1 1 − B
16 expcl ⊢ B ∈ ℂ ∧ a ∈ ℕ 0 → B a ∈ ℂ
17 2 16 sylan ⊢ φ ∧ a ∈ ℕ 0 → B a ∈ ℂ
18 14 17 eqeltrd ⊢ φ ∧ a ∈ ℕ 0 → k ∈ ℕ 0 ⟼ B k ⁡ a ∈ ℂ
19 1 zcnd ⊢ φ → A ∈ ℂ
20 nn0cn ⊢ a ∈ ℕ 0 → a ∈ ℂ
21 fvex ⊢ ℤ ≥ A ∈ V
22 21 mptex ⊢ k ∈ ℤ ≥ A ⟼ C ⁢ B k − A ∈ V
23 22 shftval4 ⊢ A ∈ ℂ ∧ a ∈ ℂ → k ∈ ℤ ≥ A ⟼ C ⁢ B k − A shift − A ⁡ a = k ∈ ℤ ≥ A ⟼ C ⁢ B k − A ⁡ A + a
24 19 20 23 syl2an ⊢ φ ∧ a ∈ ℕ 0 → k ∈ ℤ ≥ A ⟼ C ⁢ B k − A shift − A ⁡ a = k ∈ ℤ ≥ A ⟼ C ⁢ B k − A ⁡ A + a
25 uzid ⊢ A ∈ ℤ → A ∈ ℤ ≥ A
26 1 25 syl ⊢ φ → A ∈ ℤ ≥ A
27 uzaddcl ⊢ A ∈ ℤ ≥ A ∧ a ∈ ℕ 0 → A + a ∈ ℤ ≥ A
28 26 27 sylan ⊢ φ ∧ a ∈ ℕ 0 → A + a ∈ ℤ ≥ A
29 oveq1 ⊢ k = A + a → k − A = A + a - A
30 29 oveq2d ⊢ k = A + a → B k − A = B A + a - A
31 30 oveq2d ⊢ k = A + a → C ⁢ B k − A = C ⁢ B A + a - A
32 eqid ⊢ k ∈ ℤ ≥ A ⟼ C ⁢ B k − A = k ∈ ℤ ≥ A ⟼ C ⁢ B k − A
33 ovex ⊢ C ⁢ B A + a - A ∈ V
34 31 32 33 fvmpt ⊢ A + a ∈ ℤ ≥ A → k ∈ ℤ ≥ A ⟼ C ⁢ B k − A ⁡ A + a = C ⁢ B A + a - A
35 28 34 syl ⊢ φ ∧ a ∈ ℕ 0 → k ∈ ℤ ≥ A ⟼ C ⁢ B k − A ⁡ A + a = C ⁢ B A + a - A
36 pncan2 ⊢ A ∈ ℂ ∧ a ∈ ℂ → A + a - A = a
37 19 20 36 syl2an ⊢ φ ∧ a ∈ ℕ 0 → A + a - A = a
38 37 oveq2d ⊢ φ ∧ a ∈ ℕ 0 → B A + a - A = B a
39 38 14 eqtr4d ⊢ φ ∧ a ∈ ℕ 0 → B A + a - A = k ∈ ℕ 0 ⟼ B k ⁡ a
40 39 oveq2d ⊢ φ ∧ a ∈ ℕ 0 → C ⁢ B A + a - A = C ⁢ k ∈ ℕ 0 ⟼ B k ⁡ a
41 24 35 40 3eqtrd ⊢ φ ∧ a ∈ ℕ 0 → k ∈ ℤ ≥ A ⟼ C ⁢ B k − A shift − A ⁡ a = C ⁢ k ∈ ℕ 0 ⟼ B k ⁡ a
42 8 9 4 15 18 41 isermulc2 ⊢ φ → seq 0 + k ∈ ℤ ≥ A ⟼ C ⁢ B k − A shift − A ⇝ C ⁢ 1 1 − B
43 19 negidd ⊢ φ → A + − A = 0
44 43 seqeq1d ⊢ φ → seq A + − A + k ∈ ℤ ≥ A ⟼ C ⁢ B k − A shift − A = seq 0 + k ∈ ℤ ≥ A ⟼ C ⁢ B k − A shift − A
45 ax-1cn ⊢ 1 ∈ ℂ
46 subcl ⊢ 1 ∈ ℂ ∧ B ∈ ℂ → 1 − B ∈ ℂ
47 45 2 46 sylancr ⊢ φ → 1 − B ∈ ℂ
48 abs1 ⊢ 1 = 1
49 48 a1i ⊢ φ → 1 = 1
50 2 abscld ⊢ φ → B ∈ ℝ
51 50 3 gtned ⊢ φ → 1 ≠ B
52 49 51 eqnetrd ⊢ φ → 1 ≠ B
53 fveq2 ⊢ 1 = B → 1 = B
54 53 necon3i ⊢ 1 ≠ B → 1 ≠ B
55 52 54 syl ⊢ φ → 1 ≠ B
56 subeq0 ⊢ 1 ∈ ℂ ∧ B ∈ ℂ → 1 − B = 0 ↔ 1 = B
57 45 2 56 sylancr ⊢ φ → 1 − B = 0 ↔ 1 = B
58 57 necon3bid ⊢ φ → 1 − B ≠ 0 ↔ 1 ≠ B
59 55 58 mpbird ⊢ φ → 1 − B ≠ 0
60 4 47 59 divrecd ⊢ φ → C 1 − B = C ⁢ 1 1 − B
61 42 44 60 3brtr4d ⊢ φ → seq A + − A + k ∈ ℤ ≥ A ⟼ C ⁢ B k − A shift − A ⇝ C 1 − B
62 1 znegcld ⊢ φ → − A ∈ ℤ
63 22 isershft ⊢ A ∈ ℤ ∧ − A ∈ ℤ → seq A + k ∈ ℤ ≥ A ⟼ C ⁢ B k − A ⇝ C 1 − B ↔ seq A + − A + k ∈ ℤ ≥ A ⟼ C ⁢ B k − A shift − A ⇝ C 1 − B
64 1 62 63 syl2anc ⊢ φ → seq A + k ∈ ℤ ≥ A ⟼ C ⁢ B k − A ⇝ C 1 − B ↔ seq A + − A + k ∈ ℤ ≥ A ⟼ C ⁢ B k − A shift − A ⇝ C 1 − B
65 61 64 mpbird ⊢ φ → seq A + k ∈ ℤ ≥ A ⟼ C ⁢ B k − A ⇝ C 1 − B
66 7 65 eqbrtrid ⊢ φ → seq A + F ⇝ C 1 − B