Theorem georeclim

Description: The limit of a geometric series of reciprocals. (Contributed by Paul Chapman, 28-Dec-2007) (Revised by Mario Carneiro, 26-Apr-2014)

	Ref	Expression
Hypotheses	georeclim.1	$$⊢\phi \to A\in ℂ$$
	georeclim.2	$$⊢\phi \to 1<\left|A\right|$$
	georeclim.3	$$⊢\left(\phi \wedge k\in {\mathbb{N}}_0\right)\to F\left(k\right)={\left(\frac{1}{A}\right)}^k$$
Assertion	georeclim	$$⊢\phi \to seq0\left(+,F\right)⇝\left(\frac{A}{A-1}\right)$$

Proof

Step	Hyp	Ref	Expression
1		georeclim.1	$$⊢\phi \to A\in ℂ$$
2		georeclim.2	$$⊢\phi \to 1<\left|A\right|$$
3		georeclim.3	$$⊢\left(\phi \wedge k\in {\mathbb{N}}_0\right)\to F\left(k\right)={\left(\frac{1}{A}\right)}^k$$
4		0le1	$$⊢0\le 1$$
5		0re	$$⊢0\in ℝ$$
6		1re	$$⊢1\in ℝ$$
7	5 6	lenlti	$$⊢0\le 1\leftrightarrow \neg 1<0$$
8	4 7	mpbi	$$⊢\neg 1<0$$
9		fveq2	$$⊢A=0\to \left|A\right|=\left|0\right|$$
10		abs0	$$⊢\left|0\right|=0$$
11	9 10	eqtrdi	$$⊢A=0\to \left|A\right|=0$$
12	11	breq2d	$$⊢A=0\to \left(1<\left|A\right|\leftrightarrow 1<0\right)$$
13	8 12	mtbiri	$$⊢A=0\to \neg 1<\left|A\right|$$
14	13	necon2ai	$$⊢1<\left|A\right|\to A\ne 0$$
15	2 14	syl	$$⊢\phi \to A\ne 0$$
16	1 15	reccld	$$⊢\phi \to \frac{1}{A}\in ℂ$$
17		1cnd	$$⊢\phi \to 1\in ℂ$$
18	17 1 15	absdivd	$$⊢\phi \to \left|\frac{1}{A}\right|=\frac{\left|1\right|}{\left|A\right|}$$
19		abs1	$$⊢\left|1\right|=1$$
20	19	oveq1i	$$⊢\frac{\left|1\right|}{\left|A\right|}=\frac{1}{\left|A\right|}$$
21	18 20	eqtrdi	$$⊢\phi \to \left|\frac{1}{A}\right|=\frac{1}{\left|A\right|}$$
22	1 15	absrpcld	$$⊢\phi \to \left|A\right|\in {ℝ}^{+}$$
23	22	recgt1d	$$⊢\phi \to \left(1<\left|A\right|\leftrightarrow \frac{1}{\left|A\right|}<1\right)$$
24	2 23	mpbid	$$⊢\phi \to \frac{1}{\left|A\right|}<1$$
25	21 24	eqbrtrd	$$⊢\phi \to \left|\frac{1}{A}\right|<1$$
26	16 25 3	geolim	$$⊢\phi \to seq0\left(+,F\right)⇝\left(\frac{1}{1-\left(\frac{1}{A}\right)}\right)$$
27	1 17 1 15	divsubdird	$$⊢\phi \to \frac{A-1}{A}=\left(\frac{A}{A}\right)-\left(\frac{1}{A}\right)$$
28	1 15	dividd	$$⊢\phi \to \frac{A}{A}=1$$
29	28	oveq1d	$$⊢\phi \to \left(\frac{A}{A}\right)-\left(\frac{1}{A}\right)=1-\left(\frac{1}{A}\right)$$
30	27 29	eqtrd	$$⊢\phi \to \frac{A-1}{A}=1-\left(\frac{1}{A}\right)$$
31	30	oveq2d	$$⊢\phi \to \frac{1}{\frac{A-1}{A}}=\frac{1}{1-\left(\frac{1}{A}\right)}$$
32		ax-1cn	$$⊢1\in ℂ$$
33		subcl	$$⊢\left(A\in ℂ\wedge 1\in ℂ\right)\to A-1\in ℂ$$
34	1 32 33	sylancl	$$⊢\phi \to A-1\in ℂ$$
35	6	ltnri	$$⊢\neg 1<1$$
36		fveq2	$$⊢A=1\to \left|A\right|=\left|1\right|$$
37	36 19	eqtrdi	$$⊢A=1\to \left|A\right|=1$$
38	37	breq2d	$$⊢A=1\to \left(1<\left|A\right|\leftrightarrow 1<1\right)$$
39	35 38	mtbiri	$$⊢A=1\to \neg 1<\left|A\right|$$
40	39	necon2ai	$$⊢1<\left|A\right|\to A\ne 1$$
41	2 40	syl	$$⊢\phi \to A\ne 1$$
42		subeq0	$$⊢\left(A\in ℂ\wedge 1\in ℂ\right)\to \left(A-1=0\leftrightarrow A=1\right)$$
43	1 32 42	sylancl	$$⊢\phi \to \left(A-1=0\leftrightarrow A=1\right)$$
44	43	necon3bid	$$⊢\phi \to \left(A-1\ne 0\leftrightarrow A\ne 1\right)$$
45	41 44	mpbird	$$⊢\phi \to A-1\ne 0$$
46	34 1 45 15	recdivd	$$⊢\phi \to \frac{1}{\frac{A-1}{A}}=\frac{A}{A-1}$$
47	31 46	eqtr3d	$$⊢\phi \to \frac{1}{1-\left(\frac{1}{A}\right)}=\frac{A}{A-1}$$
48	26 47	breqtrd	$$⊢\phi \to seq0\left(+,F\right)⇝\left(\frac{A}{A-1}\right)$$