Theorem geolim

Description: The partial sums in the infinite series 1 + A ^ 1 + A ^ 2 ... converge to ( 1 / ( 1 - A ) ) . (Contributed by NM, 15-May-2006)

	Ref	Expression
Hypotheses	geolim.1	$$⊢\phi \to A\in ℂ$$
	geolim.2	$$⊢\phi \to \left|A\right|<1$$
	geolim.3	$$⊢\left(\phi \wedge k\in {\mathbb{N}}_0\right)\to F\left(k\right)=A^k$$
Assertion	geolim	$$⊢\phi \to seq0\left(+,F\right)⇝\left(\frac{1}{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		geolim.3	$$⊢\left(\phi \wedge k\in {\mathbb{N}}_0\right)\to F\left(k\right)=A^k$$
4		nn0uz	$$⊢{\mathbb{N}}_0={\mathbb{Z}}_{\ge 0}$$
5		0zd	$$⊢\phi \to 0\in \mathbb{Z}$$
6	1 2	expcnv	$$⊢\phi \to \left(n\in {\mathbb{N}}_0⟼A^n\right)⇝0$$
7		ax-1cn	$$⊢1\in ℂ$$
8		subcl	$$⊢\left(1\in ℂ\wedge A\in ℂ\right)\to 1-A\in ℂ$$
9	7 1 8	sylancr	$$⊢\phi \to 1-A\in ℂ$$
10		1re	$$⊢1\in ℝ$$
11	10	ltnri	$$⊢\neg 1<1$$
12		fveq2	$$⊢A=1\to \left|A\right|=\left|1\right|$$
13		abs1	$$⊢\left|1\right|=1$$
14	12 13	eqtrdi	$$⊢A=1\to \left|A\right|=1$$
15	14	breq1d	$$⊢A=1\to \left(\left|A\right|<1\leftrightarrow 1<1\right)$$
16	11 15	mtbiri	$$⊢A=1\to \neg \left|A\right|<1$$
17	16	necon2ai	$$⊢\left|A\right|<1\to A\ne 1$$
18	2 17	syl	$$⊢\phi \to A\ne 1$$
19	18	necomd	$$⊢\phi \to 1\ne A$$
20		subeq0	$$⊢\left(1\in ℂ\wedge A\in ℂ\right)\to \left(1-A=0\leftrightarrow 1=A\right)$$
21	7 1 20	sylancr	$$⊢\phi \to \left(1-A=0\leftrightarrow 1=A\right)$$
22	21	necon3bid	$$⊢\phi \to \left(1-A\ne 0\leftrightarrow 1\ne A\right)$$
23	19 22	mpbird	$$⊢\phi \to 1-A\ne 0$$
24	1 9 23	divcld	$$⊢\phi \to \frac{A}{1-A}\in ℂ$$
25		nn0ex	$$⊢{\mathbb{N}}_0\in \mathrm{V}$$
26	25	mptex	$$⊢\left(n\in {\mathbb{N}}_0⟼\frac{A^{n+1}}{1-A}\right)\in \mathrm{V}$$
27	26	a1i	$$⊢\phi \to \left(n\in {\mathbb{N}}_0⟼\frac{A^{n+1}}{1-A}\right)\in \mathrm{V}$$
28		oveq2	$$⊢n=j\to A^n=A^j$$
29		eqid	$$⊢\left(n\in {\mathbb{N}}_0⟼A^n\right)=\left(n\in {\mathbb{N}}_0⟼A^n\right)$$
30		ovex	$$⊢A^j\in \mathrm{V}$$
31	28 29 30	fvmpt	$$⊢j\in {\mathbb{N}}_0\to \left(n\in {\mathbb{N}}_0⟼A^n\right)\left(j\right)=A^j$$
32	31	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$$
33		expcl	$$⊢\left(A\in ℂ\wedge j\in {\mathbb{N}}_0\right)\to A^j\in ℂ$$
34	1 33	sylan	$$⊢\left(\phi \wedge j\in {\mathbb{N}}_0\right)\to A^j\in ℂ$$
35	32 34	eqeltrd	$$⊢\left(\phi \wedge j\in {\mathbb{N}}_0\right)\to \left(n\in {\mathbb{N}}_0⟼A^n\right)\left(j\right)\in ℂ$$
36		expp1	$$⊢\left(A\in ℂ\wedge j\in {\mathbb{N}}_0\right)\to A^{j+1}=A^{j}A$$
37	1 36	sylan	$$⊢\left(\phi \wedge j\in {\mathbb{N}}_0\right)\to A^{j+1}=A^{j}A$$
38	1	adantr	$$⊢\left(\phi \wedge j\in {\mathbb{N}}_0\right)\to A\in ℂ$$
39	34 38	mulcomd	$$⊢\left(\phi \wedge j\in {\mathbb{N}}_0\right)\to A^{j}A=A{A}^j$$
40	37 39	eqtrd	$$⊢\left(\phi \wedge j\in {\mathbb{N}}_0\right)\to A^{j+1}=A{A}^j$$
41	40	oveq1d	$$⊢\left(\phi \wedge j\in {\mathbb{N}}_0\right)\to \frac{A^{j+1}}{1-A}=\frac{A{A}^j}{1-A}$$
42	9	adantr	$$⊢\left(\phi \wedge j\in {\mathbb{N}}_0\right)\to 1-A\in ℂ$$
43	23	adantr	$$⊢\left(\phi \wedge j\in {\mathbb{N}}_0\right)\to 1-A\ne 0$$
44	38 34 42 43	div23d	$$⊢\left(\phi \wedge j\in {\mathbb{N}}_0\right)\to \frac{A{A}^j}{1-A}=\left(\frac{A}{1-A}\right)A^j$$
45	41 44	eqtrd	$$⊢\left(\phi \wedge j\in {\mathbb{N}}_0\right)\to \frac{A^{j+1}}{1-A}=\left(\frac{A}{1-A}\right)A^j$$
46		oveq1	$$⊢n=j\to n+1=j+1$$
47	46	oveq2d	$$⊢n=j\to A^{n+1}=A^{j+1}$$
48	47	oveq1d	$$⊢n=j\to \frac{A^{n+1}}{1-A}=\frac{A^{j+1}}{1-A}$$
49		eqid	$$⊢\left(n\in {\mathbb{N}}_0⟼\frac{A^{n+1}}{1-A}\right)=\left(n\in {\mathbb{N}}_0⟼\frac{A^{n+1}}{1-A}\right)$$
50		ovex	$$⊢\frac{A^{j+1}}{1-A}\in \mathrm{V}$$
51	48 49 50	fvmpt	$$⊢j\in {\mathbb{N}}_0\to \left(n\in {\mathbb{N}}_0⟼\frac{A^{n+1}}{1-A}\right)\left(j\right)=\frac{A^{j+1}}{1-A}$$
52	51	adantl	$$⊢\left(\phi \wedge j\in {\mathbb{N}}_0\right)\to \left(n\in {\mathbb{N}}_0⟼\frac{A^{n+1}}{1-A}\right)\left(j\right)=\frac{A^{j+1}}{1-A}$$
53	32	oveq2d	$$⊢\left(\phi \wedge j\in {\mathbb{N}}_0\right)\to \left(\frac{A}{1-A}\right)\left(n\in {\mathbb{N}}_0⟼A^n\right)\left(j\right)=\left(\frac{A}{1-A}\right)A^j$$
54	45 52 53	3eqtr4d	$$⊢\left(\phi \wedge j\in {\mathbb{N}}_0\right)\to \left(n\in {\mathbb{N}}_0⟼\frac{A^{n+1}}{1-A}\right)\left(j\right)=\left(\frac{A}{1-A}\right)\left(n\in {\mathbb{N}}_0⟼A^n\right)\left(j\right)$$
55	4 5 6 24 27 35 54	climmulc2	$$⊢\phi \to \left(n\in {\mathbb{N}}_0⟼\frac{A^{n+1}}{1-A}\right)⇝\left(\frac{A}{1-A}\right)\cdot 0$$
56	24	mul01d	$$⊢\phi \to \left(\frac{A}{1-A}\right)\cdot 0=0$$
57	55 56	breqtrd	$$⊢\phi \to \left(n\in {\mathbb{N}}_0⟼\frac{A^{n+1}}{1-A}\right)⇝0$$
58	9 23	reccld	$$⊢\phi \to \frac{1}{1-A}\in ℂ$$
59		seqex	$$⊢seq0\left(+,F\right)\in \mathrm{V}$$
60	59	a1i	$$⊢\phi \to seq0\left(+,F\right)\in \mathrm{V}$$
61		peano2nn0	$$⊢j\in {\mathbb{N}}_0\to j+1\in {\mathbb{N}}_0$$
62		expcl	$$⊢\left(A\in ℂ\wedge j+1\in {\mathbb{N}}_0\right)\to A^{j+1}\in ℂ$$
63	1 61 62	syl2an	$$⊢\left(\phi \wedge j\in {\mathbb{N}}_0\right)\to A^{j+1}\in ℂ$$
64	63 42 43	divcld	$$⊢\left(\phi \wedge j\in {\mathbb{N}}_0\right)\to \frac{A^{j+1}}{1-A}\in ℂ$$
65	52 64	eqeltrd	$$⊢\left(\phi \wedge j\in {\mathbb{N}}_0\right)\to \left(n\in {\mathbb{N}}_0⟼\frac{A^{n+1}}{1-A}\right)\left(j\right)\in ℂ$$
66		nn0cn	$$⊢j\in {\mathbb{N}}_0\to j\in ℂ$$
67	66	adantl	$$⊢\left(\phi \wedge j\in {\mathbb{N}}_0\right)\to j\in ℂ$$
68		pncan	$$⊢\left(j\in ℂ\wedge 1\in ℂ\right)\to j+1-1=j$$
69	67 7 68	sylancl	$$⊢\left(\phi \wedge j\in {\mathbb{N}}_0\right)\to j+1-1=j$$
70	69	oveq2d	$$⊢\left(\phi \wedge j\in {\mathbb{N}}_0\right)\to \left(0\dots j+1-1\right)=\left(0\dots j\right)$$
71	70	sumeq1d	$$⊢\left(\phi \wedge j\in {\mathbb{N}}_0\right)\to \sum _{k=0}^{j+1-1}{A}^k=\sum _{k=0}^j{A}^k$$
72	7	a1i	$$⊢\left(\phi \wedge j\in {\mathbb{N}}_0\right)\to 1\in ℂ$$
73	72 63 42 43	divsubdird	$$⊢\left(\phi \wedge j\in {\mathbb{N}}_0\right)\to \frac{1-A^{j+1}}{1-A}=\left(\frac{1}{1-A}\right)-\left(\frac{A^{j+1}}{1-A}\right)$$
74	18	adantr	$$⊢\left(\phi \wedge j\in {\mathbb{N}}_0\right)\to A\ne 1$$
75	61	adantl	$$⊢\left(\phi \wedge j\in {\mathbb{N}}_0\right)\to j+1\in {\mathbb{N}}_0$$
76	38 74 75	geoser	$$⊢\left(\phi \wedge j\in {\mathbb{N}}_0\right)\to \sum _{k=0}^{j+1-1}{A}^k=\frac{1-A^{j+1}}{1-A}$$
77	52	oveq2d	$$⊢\left(\phi \wedge j\in {\mathbb{N}}_0\right)\to \left(\frac{1}{1-A}\right)-\left(n\in {\mathbb{N}}_0⟼\frac{A^{n+1}}{1-A}\right)\left(j\right)=\left(\frac{1}{1-A}\right)-\left(\frac{A^{j+1}}{1-A}\right)$$
78	73 76 77	3eqtr4d	$$⊢\left(\phi \wedge j\in {\mathbb{N}}_0\right)\to \sum _{k=0}^{j+1-1}{A}^k=\left(\frac{1}{1-A}\right)-\left(n\in {\mathbb{N}}_0⟼\frac{A^{n+1}}{1-A}\right)\left(j\right)$$
79		simpll	$$⊢\left(\left(\phi \wedge j\in {\mathbb{N}}_0\right)\wedge k\in \left(0\dots j\right)\right)\to \phi$$
80		elfznn0	$$⊢k\in \left(0\dots j\right)\to k\in {\mathbb{N}}_0$$
81	80	adantl	$$⊢\left(\left(\phi \wedge j\in {\mathbb{N}}_0\right)\wedge k\in \left(0\dots j\right)\right)\to k\in {\mathbb{N}}_0$$
82	79 81 3	syl2anc	$$⊢\left(\left(\phi \wedge j\in {\mathbb{N}}_0\right)\wedge k\in \left(0\dots j\right)\right)\to F\left(k\right)=A^k$$
83		simpr	$$⊢\left(\phi \wedge j\in {\mathbb{N}}_0\right)\to j\in {\mathbb{N}}_0$$
84	83 4	eleqtrdi	$$⊢\left(\phi \wedge j\in {\mathbb{N}}_0\right)\to j\in {\mathbb{Z}}_{\ge 0}$$
85	79 1	syl	$$⊢\left(\left(\phi \wedge j\in {\mathbb{N}}_0\right)\wedge k\in \left(0\dots j\right)\right)\to A\in ℂ$$
86	85 81	expcld	$$⊢\left(\left(\phi \wedge j\in {\mathbb{N}}_0\right)\wedge k\in \left(0\dots j\right)\right)\to A^k\in ℂ$$
87	82 84 86	fsumser	$$⊢\left(\phi \wedge j\in {\mathbb{N}}_0\right)\to \sum _{k=0}^j{A}^k=seq0\left(+,F\right)\left(j\right)$$
88	71 78 87	3eqtr3rd	$$⊢\left(\phi \wedge j\in {\mathbb{N}}_0\right)\to seq0\left(+,F\right)\left(j\right)=\left(\frac{1}{1-A}\right)-\left(n\in {\mathbb{N}}_0⟼\frac{A^{n+1}}{1-A}\right)\left(j\right)$$
89	4 5 57 58 60 65 88	climsubc2	$$⊢\phi \to seq0\left(+,F\right)⇝\left(\left(\frac{1}{1-A}\right)-0\right)$$
90	58	subid1d	$$⊢\phi \to \left(\frac{1}{1-A}\right)-0=\frac{1}{1-A}$$
91	89 90	breqtrd	$$⊢\phi \to seq0\left(+,F\right)⇝\left(\frac{1}{1-A}\right)$$