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	|- ( ph -> A e. ZZ )
	geolim3.b1	|- ( ph -> B e. CC )
	geolim3.b2	|- ( ph -> ( abs ` B ) < 1 )
	geolim3.c	|- ( ph -> C e. CC )
	geolim3.f	|- F = ( k e. ( ZZ>= ` A ) |-> ( C x. ( B ^ ( k - A ) ) ) )
Assertion	geolim3	|- ( ph -> seq A ( + , F ) ~~> ( C / ( 1 - B ) ) )

Proof

Step	Hyp	Ref	Expression
1		geolim3.a	|- ( ph -> A e. ZZ )
2		geolim3.b1	|- ( ph -> B e. CC )
3		geolim3.b2	|- ( ph -> ( abs ` B ) < 1 )
4		geolim3.c	|- ( ph -> C e. CC )
5		geolim3.f	|- F = ( k e. ( ZZ>= ` A ) |-> ( C x. ( B ^ ( k - A ) ) ) )
6		seqeq3	|- ( F = ( k e. ( ZZ>= ` A ) |-> ( C x. ( B ^ ( k - A ) ) ) ) -> seq A ( + , F ) = seq A ( + , ( k e. ( ZZ>= ` A ) |-> ( C x. ( B ^ ( k - A ) ) ) ) ) )
7	5 6	ax-mp	|- seq A ( + , F ) = seq A ( + , ( k e. ( ZZ>= ` A ) |-> ( C x. ( B ^ ( k - A ) ) ) ) )
8		nn0uz	|- NN0 = ( ZZ>= ` 0 )
9		0zd	|- ( ph -> 0 e. ZZ )
10		oveq2	|- ( k = a -> ( B ^ k ) = ( B ^ a ) )
11		eqid	|- ( k e. NN0 |-> ( B ^ k ) ) = ( k e. NN0 |-> ( B ^ k ) )
12		ovex	|- ( B ^ a ) e. _V
13	10 11 12	fvmpt	|- ( a e. NN0 -> ( ( k e. NN0 |-> ( B ^ k ) ) ` a ) = ( B ^ a ) )
14	13	adantl	|- ( ( ph /\ a e. NN0 ) -> ( ( k e. NN0 |-> ( B ^ k ) ) ` a ) = ( B ^ a ) )
15	2 3 14	geolim	|- ( ph -> seq 0 ( + , ( k e. NN0 |-> ( B ^ k ) ) ) ~~> ( 1 / ( 1 - B ) ) )
16		expcl	|- ( ( B e. CC /\ a e. NN0 ) -> ( B ^ a ) e. CC )
17	2 16	sylan	|- ( ( ph /\ a e. NN0 ) -> ( B ^ a ) e. CC )
18	14 17	eqeltrd	|- ( ( ph /\ a e. NN0 ) -> ( ( k e. NN0 |-> ( B ^ k ) ) ` a ) e. CC )
19	1	zcnd	|- ( ph -> A e. CC )
20		nn0cn	|- ( a e. NN0 -> a e. CC )
21		fvex	|- ( ZZ>= ` A ) e. _V
22	21	mptex	|- ( k e. ( ZZ>= ` A ) |-> ( C x. ( B ^ ( k - A ) ) ) ) e. _V
23	22	shftval4	|- ( ( A e. CC /\ a e. CC ) -> ( ( ( k e. ( ZZ>= ` A ) |-> ( C x. ( B ^ ( k - A ) ) ) ) shift -u A ) ` a ) = ( ( k e. ( ZZ>= ` A ) |-> ( C x. ( B ^ ( k - A ) ) ) ) ` ( A + a ) ) )
24	19 20 23	syl2an	|- ( ( ph /\ a e. NN0 ) -> ( ( ( k e. ( ZZ>= ` A ) |-> ( C x. ( B ^ ( k - A ) ) ) ) shift -u A ) ` a ) = ( ( k e. ( ZZ>= ` A ) |-> ( C x. ( B ^ ( k - A ) ) ) ) ` ( A + a ) ) )
25		uzid	|- ( A e. ZZ -> A e. ( ZZ>= ` A ) )
26	1 25	syl	|- ( ph -> A e. ( ZZ>= ` A ) )
27		uzaddcl	|- ( ( A e. ( ZZ>= ` A ) /\ a e. NN0 ) -> ( A + a ) e. ( ZZ>= ` A ) )
28	26 27	sylan	|- ( ( ph /\ a e. NN0 ) -> ( A + a ) e. ( ZZ>= ` 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 x. ( B ^ ( k - A ) ) ) = ( C x. ( B ^ ( ( A + a ) - A ) ) ) )
32		eqid	|- ( k e. ( ZZ>= ` A ) |-> ( C x. ( B ^ ( k - A ) ) ) ) = ( k e. ( ZZ>= ` A ) |-> ( C x. ( B ^ ( k - A ) ) ) )
33		ovex	|- ( C x. ( B ^ ( ( A + a ) - A ) ) ) e. _V
34	31 32 33	fvmpt	|- ( ( A + a ) e. ( ZZ>= ` A ) -> ( ( k e. ( ZZ>= ` A ) |-> ( C x. ( B ^ ( k - A ) ) ) ) ` ( A + a ) ) = ( C x. ( B ^ ( ( A + a ) - A ) ) ) )
35	28 34	syl	|- ( ( ph /\ a e. NN0 ) -> ( ( k e. ( ZZ>= ` A ) |-> ( C x. ( B ^ ( k - A ) ) ) ) ` ( A + a ) ) = ( C x. ( B ^ ( ( A + a ) - A ) ) ) )
36		pncan2	|- ( ( A e. CC /\ a e. CC ) -> ( ( A + a ) - A ) = a )
37	19 20 36	syl2an	|- ( ( ph /\ a e. NN0 ) -> ( ( A + a ) - A ) = a )
38	37	oveq2d	|- ( ( ph /\ a e. NN0 ) -> ( B ^ ( ( A + a ) - A ) ) = ( B ^ a ) )
39	38 14	eqtr4d	|- ( ( ph /\ a e. NN0 ) -> ( B ^ ( ( A + a ) - A ) ) = ( ( k e. NN0 |-> ( B ^ k ) ) ` a ) )
40	39	oveq2d	|- ( ( ph /\ a e. NN0 ) -> ( C x. ( B ^ ( ( A + a ) - A ) ) ) = ( C x. ( ( k e. NN0 |-> ( B ^ k ) ) ` a ) ) )
41	24 35 40	3eqtrd	|- ( ( ph /\ a e. NN0 ) -> ( ( ( k e. ( ZZ>= ` A ) |-> ( C x. ( B ^ ( k - A ) ) ) ) shift -u A ) ` a ) = ( C x. ( ( k e. NN0 |-> ( B ^ k ) ) ` a ) ) )
42	8 9 4 15 18 41	isermulc2	|- ( ph -> seq 0 ( + , ( ( k e. ( ZZ>= ` A ) |-> ( C x. ( B ^ ( k - A ) ) ) ) shift -u A ) ) ~~> ( C x. ( 1 / ( 1 - B ) ) ) )
43	19	negidd	|- ( ph -> ( A + -u A ) = 0 )
44	43	seqeq1d	|- ( ph -> seq ( A + -u A ) ( + , ( ( k e. ( ZZ>= ` A ) |-> ( C x. ( B ^ ( k - A ) ) ) ) shift -u A ) ) = seq 0 ( + , ( ( k e. ( ZZ>= ` A ) |-> ( C x. ( B ^ ( k - A ) ) ) ) shift -u A ) ) )
45		ax-1cn	|- 1 e. CC
46		subcl	|- ( ( 1 e. CC /\ B e. CC ) -> ( 1 - B ) e. CC )
47	45 2 46	sylancr	|- ( ph -> ( 1 - B ) e. CC )
48		abs1	|- ( abs ` 1 ) = 1
49	48	a1i	|- ( ph -> ( abs ` 1 ) = 1 )
50	2	abscld	|- ( ph -> ( abs ` B ) e. RR )
51	50 3	gtned	|- ( ph -> 1 =/= ( abs ` B ) )
52	49 51	eqnetrd	|- ( ph -> ( abs ` 1 ) =/= ( abs ` B ) )
53		fveq2	|- ( 1 = B -> ( abs ` 1 ) = ( abs ` B ) )
54	53	necon3i	|- ( ( abs ` 1 ) =/= ( abs ` B ) -> 1 =/= B )
55	52 54	syl	|- ( ph -> 1 =/= B )
56		subeq0	|- ( ( 1 e. CC /\ B e. CC ) -> ( ( 1 - B ) = 0 <-> 1 = B ) )
57	45 2 56	sylancr	|- ( ph -> ( ( 1 - B ) = 0 <-> 1 = B ) )
58	57	necon3bid	|- ( ph -> ( ( 1 - B ) =/= 0 <-> 1 =/= B ) )
59	55 58	mpbird	|- ( ph -> ( 1 - B ) =/= 0 )
60	4 47 59	divrecd	|- ( ph -> ( C / ( 1 - B ) ) = ( C x. ( 1 / ( 1 - B ) ) ) )
61	42 44 60	3brtr4d	|- ( ph -> seq ( A + -u A ) ( + , ( ( k e. ( ZZ>= ` A ) |-> ( C x. ( B ^ ( k - A ) ) ) ) shift -u A ) ) ~~> ( C / ( 1 - B ) ) )
62	1	znegcld	|- ( ph -> -u A e. ZZ )
63	22	isershft	|- ( ( A e. ZZ /\ -u A e. ZZ ) -> ( seq A ( + , ( k e. ( ZZ>= ` A ) |-> ( C x. ( B ^ ( k - A ) ) ) ) ) ~~> ( C / ( 1 - B ) ) <-> seq ( A + -u A ) ( + , ( ( k e. ( ZZ>= ` A ) |-> ( C x. ( B ^ ( k - A ) ) ) ) shift -u A ) ) ~~> ( C / ( 1 - B ) ) ) )
64	1 62 63	syl2anc	|- ( ph -> ( seq A ( + , ( k e. ( ZZ>= ` A ) |-> ( C x. ( B ^ ( k - A ) ) ) ) ) ~~> ( C / ( 1 - B ) ) <-> seq ( A + -u A ) ( + , ( ( k e. ( ZZ>= ` A ) |-> ( C x. ( B ^ ( k - A ) ) ) ) shift -u A ) ) ~~> ( C / ( 1 - B ) ) ) )
65	61 64	mpbird	|- ( ph -> seq A ( + , ( k e. ( ZZ>= ` A ) |-> ( C x. ( B ^ ( k - A ) ) ) ) ) ~~> ( C / ( 1 - B ) ) )
66	7 65	eqbrtrid	|- ( ph -> seq A ( + , F ) ~~> ( C / ( 1 - B ) ) )