Theorem geolim2

Description: The partial sums in the geometric series A ^ M + A ^ ( M + 1 ) ... converge to ( ( A ^ M ) / ( 1 - A ) ) . (Contributed by NM, 6-Jun-2006) (Revised by Mario Carneiro, 26-Apr-2014)

	Ref	Expression
Hypotheses	geolim.1	|- ( ph -> A e. CC )
	geolim.2	|- ( ph -> ( abs ` A ) < 1 )
	geolim2.3	|- ( ph -> M e. NN0 )
	geolim2.4	|- ( ( ph /\ k e. ( ZZ>= ` M ) ) -> ( F ` k ) = ( A ^ k ) )
Assertion	geolim2	|- ( ph -> seq M ( + , F ) ~~> ( ( A ^ M ) / ( 1 - A ) ) )

Proof

Step	Hyp	Ref	Expression
1		geolim.1	|- ( ph -> A e. CC )
2		geolim.2	|- ( ph -> ( abs ` A ) < 1 )
3		geolim2.3	|- ( ph -> M e. NN0 )
4		geolim2.4	|- ( ( ph /\ k e. ( ZZ>= ` M ) ) -> ( F ` k ) = ( A ^ k ) )
5		eqid	|- ( ZZ>= ` M ) = ( ZZ>= ` M )
6	3	nn0zd	|- ( ph -> M e. ZZ )
7	1	adantr	|- ( ( ph /\ k e. ( ZZ>= ` M ) ) -> A e. CC )
8		eluznn0	|- ( ( M e. NN0 /\ k e. ( ZZ>= ` M ) ) -> k e. NN0 )
9	3 8	sylan	|- ( ( ph /\ k e. ( ZZ>= ` M ) ) -> k e. NN0 )
10	7 9	expcld	|- ( ( ph /\ k e. ( ZZ>= ` M ) ) -> ( A ^ k ) e. CC )
11		oveq2	|- ( n = k -> ( A ^ n ) = ( A ^ k ) )
12		eqid	|- ( n e. NN0 |-> ( A ^ n ) ) = ( n e. NN0 |-> ( A ^ n ) )
13		ovex	|- ( A ^ k ) e. _V
14	11 12 13	fvmpt	|- ( k e. NN0 -> ( ( n e. NN0 |-> ( A ^ n ) ) ` k ) = ( A ^ k ) )
15	9 14	syl	|- ( ( ph /\ k e. ( ZZ>= ` M ) ) -> ( ( n e. NN0 |-> ( A ^ n ) ) ` k ) = ( A ^ k ) )
16	15 4	eqtr4d	|- ( ( ph /\ k e. ( ZZ>= ` M ) ) -> ( ( n e. NN0 |-> ( A ^ n ) ) ` k ) = ( F ` k ) )
17	6 16	seqfeq	|- ( ph -> seq M ( + , ( n e. NN0 |-> ( A ^ n ) ) ) = seq M ( + , F ) )
18		oveq2	|- ( n = j -> ( A ^ n ) = ( A ^ j ) )
19		ovex	|- ( A ^ j ) e. _V
20	18 12 19	fvmpt	|- ( j e. NN0 -> ( ( n e. NN0 |-> ( A ^ n ) ) ` j ) = ( A ^ j ) )
21	20	adantl	|- ( ( ph /\ j e. NN0 ) -> ( ( n e. NN0 |-> ( A ^ n ) ) ` j ) = ( A ^ j ) )
22	1 2 21	geolim	|- ( ph -> seq 0 ( + , ( n e. NN0 |-> ( A ^ n ) ) ) ~~> ( 1 / ( 1 - A ) ) )
23		seqex	|- seq 0 ( + , ( n e. NN0 |-> ( A ^ n ) ) ) e. _V
24		ovex	|- ( 1 / ( 1 - A ) ) e. _V
25	23 24	breldm	|- ( seq 0 ( + , ( n e. NN0 |-> ( A ^ n ) ) ) ~~> ( 1 / ( 1 - A ) ) -> seq 0 ( + , ( n e. NN0 |-> ( A ^ n ) ) ) e. dom ~~> )
26	22 25	syl	|- ( ph -> seq 0 ( + , ( n e. NN0 |-> ( A ^ n ) ) ) e. dom ~~> )
27		nn0uz	|- NN0 = ( ZZ>= ` 0 )
28		expcl	|- ( ( A e. CC /\ j e. NN0 ) -> ( A ^ j ) e. CC )
29	1 28	sylan	|- ( ( ph /\ j e. NN0 ) -> ( A ^ j ) e. CC )
30	21 29	eqeltrd	|- ( ( ph /\ j e. NN0 ) -> ( ( n e. NN0 |-> ( A ^ n ) ) ` j ) e. CC )
31	27 3 30	iserex	|- ( ph -> ( seq 0 ( + , ( n e. NN0 |-> ( A ^ n ) ) ) e. dom ~~> <-> seq M ( + , ( n e. NN0 |-> ( A ^ n ) ) ) e. dom ~~> ) )
32	26 31	mpbid	|- ( ph -> seq M ( + , ( n e. NN0 |-> ( A ^ n ) ) ) e. dom ~~> )
33	17 32	eqeltrrd	|- ( ph -> seq M ( + , F ) e. dom ~~> )
34	5 6 4 10 33	isumclim2	|- ( ph -> seq M ( + , F ) ~~> sum_ k e. ( ZZ>= ` M ) ( A ^ k ) )
35	14	adantl	|- ( ( ph /\ k e. NN0 ) -> ( ( n e. NN0 |-> ( A ^ n ) ) ` k ) = ( A ^ k ) )
36		expcl	|- ( ( A e. CC /\ k e. NN0 ) -> ( A ^ k ) e. CC )
37	1 36	sylan	|- ( ( ph /\ k e. NN0 ) -> ( A ^ k ) e. CC )
38	27 5 3 35 37 26	isumsplit	|- ( ph -> sum_ k e. NN0 ( A ^ k ) = ( sum_ k e. ( 0 ... ( M - 1 ) ) ( A ^ k ) + sum_ k e. ( ZZ>= ` M ) ( A ^ k ) ) )
39		0zd	|- ( ph -> 0 e. ZZ )
40	27 39 35 37 22	isumclim	|- ( ph -> sum_ k e. NN0 ( A ^ k ) = ( 1 / ( 1 - A ) ) )
41	38 40	eqtr3d	|- ( ph -> ( sum_ k e. ( 0 ... ( M - 1 ) ) ( A ^ k ) + sum_ k e. ( ZZ>= ` M ) ( A ^ k ) ) = ( 1 / ( 1 - A ) ) )
42		1re	|- 1 e. RR
43	42	ltnri	|- -. 1 < 1
44		fveq2	|- ( A = 1 -> ( abs ` A ) = ( abs ` 1 ) )
45		abs1	|- ( abs ` 1 ) = 1
46	44 45	eqtrdi	|- ( A = 1 -> ( abs ` A ) = 1 )
47	46	breq1d	|- ( A = 1 -> ( ( abs ` A ) < 1 <-> 1 < 1 ) )
48	43 47	mtbiri	|- ( A = 1 -> -. ( abs ` A ) < 1 )
49	48	necon2ai	|- ( ( abs ` A ) < 1 -> A =/= 1 )
50	2 49	syl	|- ( ph -> A =/= 1 )
51	1 50 3	geoser	|- ( ph -> sum_ k e. ( 0 ... ( M - 1 ) ) ( A ^ k ) = ( ( 1 - ( A ^ M ) ) / ( 1 - A ) ) )
52	51	oveq1d	|- ( ph -> ( sum_ k e. ( 0 ... ( M - 1 ) ) ( A ^ k ) + sum_ k e. ( ZZ>= ` M ) ( A ^ k ) ) = ( ( ( 1 - ( A ^ M ) ) / ( 1 - A ) ) + sum_ k e. ( ZZ>= ` M ) ( A ^ k ) ) )
53	41 52	eqtr3d	|- ( ph -> ( 1 / ( 1 - A ) ) = ( ( ( 1 - ( A ^ M ) ) / ( 1 - A ) ) + sum_ k e. ( ZZ>= ` M ) ( A ^ k ) ) )
54	53	oveq1d	|- ( ph -> ( ( 1 / ( 1 - A ) ) - ( ( 1 - ( A ^ M ) ) / ( 1 - A ) ) ) = ( ( ( ( 1 - ( A ^ M ) ) / ( 1 - A ) ) + sum_ k e. ( ZZ>= ` M ) ( A ^ k ) ) - ( ( 1 - ( A ^ M ) ) / ( 1 - A ) ) ) )
55		1cnd	|- ( ph -> 1 e. CC )
56		ax-1cn	|- 1 e. CC
57	1 3	expcld	|- ( ph -> ( A ^ M ) e. CC )
58		subcl	|- ( ( 1 e. CC /\ ( A ^ M ) e. CC ) -> ( 1 - ( A ^ M ) ) e. CC )
59	56 57 58	sylancr	|- ( ph -> ( 1 - ( A ^ M ) ) e. CC )
60		subcl	|- ( ( 1 e. CC /\ A e. CC ) -> ( 1 - A ) e. CC )
61	56 1 60	sylancr	|- ( ph -> ( 1 - A ) e. CC )
62	50	necomd	|- ( ph -> 1 =/= A )
63		subeq0	|- ( ( 1 e. CC /\ A e. CC ) -> ( ( 1 - A ) = 0 <-> 1 = A ) )
64	56 1 63	sylancr	|- ( ph -> ( ( 1 - A ) = 0 <-> 1 = A ) )
65	64	necon3bid	|- ( ph -> ( ( 1 - A ) =/= 0 <-> 1 =/= A ) )
66	62 65	mpbird	|- ( ph -> ( 1 - A ) =/= 0 )
67	55 59 61 66	divsubdird	|- ( ph -> ( ( 1 - ( 1 - ( A ^ M ) ) ) / ( 1 - A ) ) = ( ( 1 / ( 1 - A ) ) - ( ( 1 - ( A ^ M ) ) / ( 1 - A ) ) ) )
68		nncan	|- ( ( 1 e. CC /\ ( A ^ M ) e. CC ) -> ( 1 - ( 1 - ( A ^ M ) ) ) = ( A ^ M ) )
69	56 57 68	sylancr	|- ( ph -> ( 1 - ( 1 - ( A ^ M ) ) ) = ( A ^ M ) )
70	69	oveq1d	|- ( ph -> ( ( 1 - ( 1 - ( A ^ M ) ) ) / ( 1 - A ) ) = ( ( A ^ M ) / ( 1 - A ) ) )
71	67 70	eqtr3d	|- ( ph -> ( ( 1 / ( 1 - A ) ) - ( ( 1 - ( A ^ M ) ) / ( 1 - A ) ) ) = ( ( A ^ M ) / ( 1 - A ) ) )
72	59 61 66	divcld	|- ( ph -> ( ( 1 - ( A ^ M ) ) / ( 1 - A ) ) e. CC )
73	5 6 15 10 32	isumcl	|- ( ph -> sum_ k e. ( ZZ>= ` M ) ( A ^ k ) e. CC )
74	72 73	pncan2d	|- ( ph -> ( ( ( ( 1 - ( A ^ M ) ) / ( 1 - A ) ) + sum_ k e. ( ZZ>= ` M ) ( A ^ k ) ) - ( ( 1 - ( A ^ M ) ) / ( 1 - A ) ) ) = sum_ k e. ( ZZ>= ` M ) ( A ^ k ) )
75	54 71 74	3eqtr3rd	|- ( ph -> sum_ k e. ( ZZ>= ` M ) ( A ^ k ) = ( ( A ^ M ) / ( 1 - A ) ) )
76	34 75	breqtrd	|- ( ph -> seq M ( + , F ) ~~> ( ( A ^ M ) / ( 1 - A ) ) )