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	$$⊢\phi \to A\in ℂ$$
	geolim.2	$$⊢\phi \to \left|A\right|<1$$
	geolim2.3	$$⊢\phi \to M\in {\mathbb{N}}_0$$
	geolim2.4	$$⊢\left(\phi \wedge k\in {\mathbb{Z}}_{\ge M}\right)\to F\left(k\right)=A^k$$
Assertion	geolim2	$$⊢\phi \to seqM\left(+,F\right)⇝\left(\frac{A^M}{1-A}\right)$$

Proof

Step	Hyp	Ref	Expression
1		geolim.1	$$⊢\phi \to A\in ℂ$$
2		geolim.2	$$⊢\phi \to \left|A\right|<1$$
3		geolim2.3	$$⊢\phi \to M\in {\mathbb{N}}_0$$
4		geolim2.4	$$⊢\left(\phi \wedge k\in {\mathbb{Z}}_{\ge M}\right)\to F\left(k\right)=A^k$$
5		eqid	$$⊢{\mathbb{Z}}_{\ge M}={\mathbb{Z}}_{\ge M}$$
6	3	nn0zd	$$⊢\phi \to M\in \mathbb{Z}$$
7	1	adantr	$$⊢\left(\phi \wedge k\in {\mathbb{Z}}_{\ge M}\right)\to A\in ℂ$$
8		eluznn0	$$⊢\left(M\in {\mathbb{N}}_0\wedge k\in {\mathbb{Z}}_{\ge M}\right)\to k\in {\mathbb{N}}_0$$
9	3 8	sylan	$$⊢\left(\phi \wedge k\in {\mathbb{Z}}_{\ge M}\right)\to k\in {\mathbb{N}}_0$$
10	7 9	expcld	$$⊢\left(\phi \wedge k\in {\mathbb{Z}}_{\ge M}\right)\to A^k\in ℂ$$
11		oveq2	$$⊢n=k\to A^n=A^k$$
12		eqid	$$⊢\left(n\in {\mathbb{N}}_0⟼A^n\right)=\left(n\in {\mathbb{N}}_0⟼A^n\right)$$
13		ovex	$$⊢A^k\in \mathrm{V}$$
14	11 12 13	fvmpt	$$⊢k\in {\mathbb{N}}_0\to \left(n\in {\mathbb{N}}_0⟼A^n\right)\left(k\right)=A^k$$
15	9 14	syl	$$⊢\left(\phi \wedge k\in {\mathbb{Z}}_{\ge M}\right)\to \left(n\in {\mathbb{N}}_0⟼A^n\right)\left(k\right)=A^k$$
16	15 4	eqtr4d	$$⊢\left(\phi \wedge k\in {\mathbb{Z}}_{\ge M}\right)\to \left(n\in {\mathbb{N}}_0⟼A^n\right)\left(k\right)=F\left(k\right)$$
17	6 16	seqfeq	$$⊢\phi \to seqM\left(+,\left(n\in {\mathbb{N}}_0⟼A^n\right)\right)=seqM\left(+,F\right)$$
18		oveq2	$$⊢n=j\to A^n=A^j$$
19		ovex	$$⊢A^j\in \mathrm{V}$$
20	18 12 19	fvmpt	$$⊢j\in {\mathbb{N}}_0\to \left(n\in {\mathbb{N}}_0⟼A^n\right)\left(j\right)=A^j$$
21	20	adantl	$$⊢\left(\phi \wedge j\in {\mathbb{N}}_0\right)\to \left(n\in {\mathbb{N}}_0⟼A^n\right)\left(j\right)=A^j$$
22	1 2 21	geolim	$$⊢\phi \to seq0\left(+,\left(n\in {\mathbb{N}}_0⟼A^n\right)\right)⇝\left(\frac{1}{1-A}\right)$$
23		seqex	$$⊢seq0\left(+,\left(n\in {\mathbb{N}}_0⟼A^n\right)\right)\in \mathrm{V}$$
24		ovex	$$⊢\frac{1}{1-A}\in \mathrm{V}$$
25	23 24	breldm	$$⊢seq0\left(+,\left(n\in {\mathbb{N}}_0⟼A^n\right)\right)⇝\left(\frac{1}{1-A}\right)\to seq0\left(+,\left(n\in {\mathbb{N}}_0⟼A^n\right)\right)\in \mathrm{dom}⇝$$
26	22 25	syl	$$⊢\phi \to seq0\left(+,\left(n\in {\mathbb{N}}_0⟼A^n\right)\right)\in \mathrm{dom}⇝$$
27		nn0uz	$$⊢{\mathbb{N}}_0={\mathbb{Z}}_{\ge 0}$$
28		expcl	$$⊢\left(A\in ℂ\wedge j\in {\mathbb{N}}_0\right)\to A^j\in ℂ$$
29	1 28	sylan	$$⊢\left(\phi \wedge j\in {\mathbb{N}}_0\right)\to A^j\in ℂ$$
30	21 29	eqeltrd	$$⊢\left(\phi \wedge j\in {\mathbb{N}}_0\right)\to \left(n\in {\mathbb{N}}_0⟼A^n\right)\left(j\right)\in ℂ$$
31	27 3 30	iserex	$$⊢\phi \to \left(seq0\left(+,\left(n\in {\mathbb{N}}_0⟼A^n\right)\right)\in \mathrm{dom}⇝\leftrightarrow seqM\left(+,\left(n\in {\mathbb{N}}_0⟼A^n\right)\right)\in \mathrm{dom}⇝\right)$$
32	26 31	mpbid	$$⊢\phi \to seqM\left(+,\left(n\in {\mathbb{N}}_0⟼A^n\right)\right)\in \mathrm{dom}⇝$$
33	17 32	eqeltrrd	$$⊢\phi \to seqM\left(+,F\right)\in \mathrm{dom}⇝$$
34	5 6 4 10 33	isumclim2	$$⊢\phi \to seqM\left(+,F\right)⇝\sum _{k\in {\mathbb{Z}}_{\ge M}}{A}^k$$
35	14	adantl	$$⊢\left(\phi \wedge k\in {\mathbb{N}}_0\right)\to \left(n\in {\mathbb{N}}_0⟼A^n\right)\left(k\right)=A^k$$
36		expcl	$$⊢\left(A\in ℂ\wedge k\in {\mathbb{N}}_0\right)\to A^k\in ℂ$$
37	1 36	sylan	$$⊢\left(\phi \wedge k\in {\mathbb{N}}_0\right)\to A^k\in ℂ$$
38	27 5 3 35 37 26	isumsplit	$$⊢\phi \to \sum _{k\in {\mathbb{N}}_0}{A}^k=\sum _{k=0}^{M-1}{A}^k+\sum _{k\in {\mathbb{Z}}_{\ge M}}{A}^k$$
39		0zd	$$⊢\phi \to 0\in \mathbb{Z}$$
40	27 39 35 37 22	isumclim	$$⊢\phi \to \sum _{k\in {\mathbb{N}}_0}{A}^k=\frac{1}{1-A}$$
41	38 40	eqtr3d	$$⊢\phi \to \sum _{k=0}^{M-1}{A}^k+\sum _{k\in {\mathbb{Z}}_{\ge M}}{A}^k=\frac{1}{1-A}$$
42		1re	$$⊢1\in ℝ$$
43	42	ltnri	$$⊢\neg 1<1$$
44		fveq2	$$⊢A=1\to \left|A\right|=\left|1\right|$$
45		abs1	$$⊢\left|1\right|=1$$
46	44 45	syl6eq	$$⊢A=1\to \left|A\right|=1$$
47	46	breq1d	$$⊢A=1\to \left(\left|A\right|<1\leftrightarrow 1<1\right)$$
48	43 47	mtbiri	$$⊢A=1\to \neg \left|A\right|<1$$
49	48	necon2ai	$$⊢\left|A\right|<1\to A\ne 1$$
50	2 49	syl	$$⊢\phi \to A\ne 1$$
51	1 50 3	geoser	$$⊢\phi \to \sum _{k=0}^{M-1}{A}^k=\frac{1-A^M}{1-A}$$
52	51	oveq1d	$$⊢\phi \to \sum _{k=0}^{M-1}{A}^k+\sum _{k\in {\mathbb{Z}}_{\ge M}}{A}^k=\left(\frac{1-A^M}{1-A}\right)+\sum _{k\in {\mathbb{Z}}_{\ge M}}{A}^k$$
53	41 52	eqtr3d	$$⊢\phi \to \frac{1}{1-A}=\left(\frac{1-A^M}{1-A}\right)+\sum _{k\in {\mathbb{Z}}_{\ge M}}{A}^k$$
54	53	oveq1d	$$⊢\phi \to \left(\frac{1}{1-A}\right)-\left(\frac{1-A^M}{1-A}\right)=\left(\frac{1-A^M}{1-A}\right)+\sum _{k\in {\mathbb{Z}}_{\ge M}}{A}^k-\left(\frac{1-A^M}{1-A}\right)$$
55		1cnd	$$⊢\phi \to 1\in ℂ$$
56		ax-1cn	$$⊢1\in ℂ$$
57	1 3	expcld	$$⊢\phi \to A^M\in ℂ$$
58		subcl	$$⊢\left(1\in ℂ\wedge A^M\in ℂ\right)\to 1-A^M\in ℂ$$
59	56 57 58	sylancr	$$⊢\phi \to 1-A^M\in ℂ$$
60		subcl	$$⊢\left(1\in ℂ\wedge A\in ℂ\right)\to 1-A\in ℂ$$
61	56 1 60	sylancr	$$⊢\phi \to 1-A\in ℂ$$
62	50	necomd	$$⊢\phi \to 1\ne A$$
63		subeq0	$$⊢\left(1\in ℂ\wedge A\in ℂ\right)\to \left(1-A=0\leftrightarrow 1=A\right)$$
64	56 1 63	sylancr	$$⊢\phi \to \left(1-A=0\leftrightarrow 1=A\right)$$
65	64	necon3bid	$$⊢\phi \to \left(1-A\ne 0\leftrightarrow 1\ne A\right)$$
66	62 65	mpbird	$$⊢\phi \to 1-A\ne 0$$
67	55 59 61 66	divsubdird	$$⊢\phi \to \frac{1-\left(1-A^M\right)}{1-A}=\left(\frac{1}{1-A}\right)-\left(\frac{1-A^M}{1-A}\right)$$
68		nncan	$$⊢\left(1\in ℂ\wedge A^M\in ℂ\right)\to 1-\left(1-A^M\right)=A^M$$
69	56 57 68	sylancr	$$⊢\phi \to 1-\left(1-A^M\right)=A^M$$
70	69	oveq1d	$$⊢\phi \to \frac{1-\left(1-A^M\right)}{1-A}=\frac{A^M}{1-A}$$
71	67 70	eqtr3d	$$⊢\phi \to \left(\frac{1}{1-A}\right)-\left(\frac{1-A^M}{1-A}\right)=\frac{A^M}{1-A}$$
72	59 61 66	divcld	$$⊢\phi \to \frac{1-A^M}{1-A}\in ℂ$$
73	5 6 15 10 32	isumcl	$$⊢\phi \to \sum _{k\in {\mathbb{Z}}_{\ge M}}{A}^k\in ℂ$$
74	72 73	pncan2d	$$⊢\phi \to \left(\frac{1-A^M}{1-A}\right)+\sum _{k\in {\mathbb{Z}}_{\ge M}}{A}^k-\left(\frac{1-A^M}{1-A}\right)=\sum _{k\in {\mathbb{Z}}_{\ge M}}{A}^k$$
75	54 71 74	3eqtr3rd	$$⊢\phi \to \sum _{k\in {\mathbb{Z}}_{\ge M}}{A}^k=\frac{A^M}{1-A}$$
76	34 75	breqtrd	$$⊢\phi \to seqM\left(+,F\right)⇝\left(\frac{A^M}{1-A}\right)$$