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	⊢ ( 𝜑 → 𝐴 ∈ ℂ )
	georeclim.2	⊢ ( 𝜑 → 1 < ( abs ‘ 𝐴 ) )
	georeclim.3	⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ0 ) → ( 𝐹 ‘ 𝑘 ) = ( ( 1 / 𝐴 ) ↑ 𝑘 ) )
Assertion	georeclim	⊢ ( 𝜑 → seq 0 ( + , 𝐹 ) ⇝ ( 𝐴 / ( 𝐴 − 1 ) ) )

Proof

Step	Hyp	Ref	Expression
1		georeclim.1	⊢ ( 𝜑 → 𝐴 ∈ ℂ )
2		georeclim.2	⊢ ( 𝜑 → 1 < ( abs ‘ 𝐴 ) )
3		georeclim.3	⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ0 ) → ( 𝐹 ‘ 𝑘 ) = ( ( 1 / 𝐴 ) ↑ 𝑘 ) )
4		0le1	⊢ 0 ≤ 1
5		0re	⊢ 0 ∈ ℝ
6		1re	⊢ 1 ∈ ℝ
7	5 6	lenlti	⊢ ( 0 ≤ 1 ↔ ¬ 1 < 0 )
8	4 7	mpbi	⊢ ¬ 1 < 0
9		fveq2	⊢ ( 𝐴 = 0 → ( abs ‘ 𝐴 ) = ( abs ‘ 0 ) )
10		abs0	⊢ ( abs ‘ 0 ) = 0
11	9 10	eqtrdi	⊢ ( 𝐴 = 0 → ( abs ‘ 𝐴 ) = 0 )
12	11	breq2d	⊢ ( 𝐴 = 0 → ( 1 < ( abs ‘ 𝐴 ) ↔ 1 < 0 ) )
13	8 12	mtbiri	⊢ ( 𝐴 = 0 → ¬ 1 < ( abs ‘ 𝐴 ) )
14	13	necon2ai	⊢ ( 1 < ( abs ‘ 𝐴 ) → 𝐴 ≠ 0 )
15	2 14	syl	⊢ ( 𝜑 → 𝐴 ≠ 0 )
16	1 15	reccld	⊢ ( 𝜑 → ( 1 / 𝐴 ) ∈ ℂ )
17		1cnd	⊢ ( 𝜑 → 1 ∈ ℂ )
18	17 1 15	absdivd	⊢ ( 𝜑 → ( abs ‘ ( 1 / 𝐴 ) ) = ( ( abs ‘ 1 ) / ( abs ‘ 𝐴 ) ) )
19		abs1	⊢ ( abs ‘ 1 ) = 1
20	19	oveq1i	⊢ ( ( abs ‘ 1 ) / ( abs ‘ 𝐴 ) ) = ( 1 / ( abs ‘ 𝐴 ) )
21	18 20	eqtrdi	⊢ ( 𝜑 → ( abs ‘ ( 1 / 𝐴 ) ) = ( 1 / ( abs ‘ 𝐴 ) ) )
22	1 15	absrpcld	⊢ ( 𝜑 → ( abs ‘ 𝐴 ) ∈ ℝ+ )
23	22	recgt1d	⊢ ( 𝜑 → ( 1 < ( abs ‘ 𝐴 ) ↔ ( 1 / ( abs ‘ 𝐴 ) ) < 1 ) )
24	2 23	mpbid	⊢ ( 𝜑 → ( 1 / ( abs ‘ 𝐴 ) ) < 1 )
25	21 24	eqbrtrd	⊢ ( 𝜑 → ( abs ‘ ( 1 / 𝐴 ) ) < 1 )
26	16 25 3	geolim	⊢ ( 𝜑 → seq 0 ( + , 𝐹 ) ⇝ ( 1 / ( 1 − ( 1 / 𝐴 ) ) ) )
27	1 17 1 15	divsubdird	⊢ ( 𝜑 → ( ( 𝐴 − 1 ) / 𝐴 ) = ( ( 𝐴 / 𝐴 ) − ( 1 / 𝐴 ) ) )
28	1 15	dividd	⊢ ( 𝜑 → ( 𝐴 / 𝐴 ) = 1 )
29	28	oveq1d	⊢ ( 𝜑 → ( ( 𝐴 / 𝐴 ) − ( 1 / 𝐴 ) ) = ( 1 − ( 1 / 𝐴 ) ) )
30	27 29	eqtrd	⊢ ( 𝜑 → ( ( 𝐴 − 1 ) / 𝐴 ) = ( 1 − ( 1 / 𝐴 ) ) )
31	30	oveq2d	⊢ ( 𝜑 → ( 1 / ( ( 𝐴 − 1 ) / 𝐴 ) ) = ( 1 / ( 1 − ( 1 / 𝐴 ) ) ) )
32		ax-1cn	⊢ 1 ∈ ℂ
33		subcl	⊢ ( ( 𝐴 ∈ ℂ ∧ 1 ∈ ℂ ) → ( 𝐴 − 1 ) ∈ ℂ )
34	1 32 33	sylancl	⊢ ( 𝜑 → ( 𝐴 − 1 ) ∈ ℂ )
35	6	ltnri	⊢ ¬ 1 < 1
36		fveq2	⊢ ( 𝐴 = 1 → ( abs ‘ 𝐴 ) = ( abs ‘ 1 ) )
37	36 19	eqtrdi	⊢ ( 𝐴 = 1 → ( abs ‘ 𝐴 ) = 1 )
38	37	breq2d	⊢ ( 𝐴 = 1 → ( 1 < ( abs ‘ 𝐴 ) ↔ 1 < 1 ) )
39	35 38	mtbiri	⊢ ( 𝐴 = 1 → ¬ 1 < ( abs ‘ 𝐴 ) )
40	39	necon2ai	⊢ ( 1 < ( abs ‘ 𝐴 ) → 𝐴 ≠ 1 )
41	2 40	syl	⊢ ( 𝜑 → 𝐴 ≠ 1 )
42		subeq0	⊢ ( ( 𝐴 ∈ ℂ ∧ 1 ∈ ℂ ) → ( ( 𝐴 − 1 ) = 0 ↔ 𝐴 = 1 ) )
43	1 32 42	sylancl	⊢ ( 𝜑 → ( ( 𝐴 − 1 ) = 0 ↔ 𝐴 = 1 ) )
44	43	necon3bid	⊢ ( 𝜑 → ( ( 𝐴 − 1 ) ≠ 0 ↔ 𝐴 ≠ 1 ) )
45	41 44	mpbird	⊢ ( 𝜑 → ( 𝐴 − 1 ) ≠ 0 )
46	34 1 45 15	recdivd	⊢ ( 𝜑 → ( 1 / ( ( 𝐴 − 1 ) / 𝐴 ) ) = ( 𝐴 / ( 𝐴 − 1 ) ) )
47	31 46	eqtr3d	⊢ ( 𝜑 → ( 1 / ( 1 − ( 1 / 𝐴 ) ) ) = ( 𝐴 / ( 𝐴 − 1 ) ) )
48	26 47	breqtrd	⊢ ( 𝜑 → seq 0 ( + , 𝐹 ) ⇝ ( 𝐴 / ( 𝐴 − 1 ) ) )