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 ⊢ ( 𝜑 → 𝐴 ∈ ℤ )
geolim3.b1 ⊢ ( 𝜑 → 𝐵 ∈ ℂ )
geolim3.b2 ⊢ ( 𝜑 → ( abs ‘ 𝐵 ) < 1 )
geolim3.c ⊢ ( 𝜑 → 𝐶 ∈ ℂ )
geolim3.f ⊢ 𝐹 = ( 𝑘 ∈ ( ℤ≥ ‘ 𝐴 ) ↦ ( 𝐶 · ( 𝐵 ↑ ( 𝑘 − 𝐴 ) ) ) )
Assertion geolim3 ( 𝜑 → seq 𝐴 ( + , 𝐹 ) ⇝ ( 𝐶 / ( 1 − 𝐵 ) ) )

Proof

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