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 − 𝐵 ) ) )