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

Proof

Step	Hyp	Ref	Expression
1		geolim.1	⊢ ( 𝜑 → 𝐴 ∈ ℂ )
2		geolim.2	⊢ ( 𝜑 → ( abs ‘ 𝐴 ) < 1 )
3		geolim.3	⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ0 ) → ( 𝐹 ‘ 𝑘 ) = ( 𝐴 ↑ 𝑘 ) )
4		nn0uz	⊢ ℕ0 = ( ℤ≥ ‘ 0 )
5		0zd	⊢ ( 𝜑 → 0 ∈ ℤ )
6	1 2	expcnv	⊢ ( 𝜑 → ( 𝑛 ∈ ℕ0 ↦ ( 𝐴 ↑ 𝑛 ) ) ⇝ 0 )
7		ax-1cn	⊢ 1 ∈ ℂ
8		subcl	⊢ ( ( 1 ∈ ℂ ∧ 𝐴 ∈ ℂ ) → ( 1 − 𝐴 ) ∈ ℂ )
9	7 1 8	sylancr	⊢ ( 𝜑 → ( 1 − 𝐴 ) ∈ ℂ )
10		1re	⊢ 1 ∈ ℝ
11	10	ltnri	⊢ ¬ 1 < 1
12		fveq2	⊢ ( 𝐴 = 1 → ( abs ‘ 𝐴 ) = ( abs ‘ 1 ) )
13		abs1	⊢ ( abs ‘ 1 ) = 1
14	12 13	eqtrdi	⊢ ( 𝐴 = 1 → ( abs ‘ 𝐴 ) = 1 )
15	14	breq1d	⊢ ( 𝐴 = 1 → ( ( abs ‘ 𝐴 ) < 1 ↔ 1 < 1 ) )
16	11 15	mtbiri	⊢ ( 𝐴 = 1 → ¬ ( abs ‘ 𝐴 ) < 1 )
17	16	necon2ai	⊢ ( ( abs ‘ 𝐴 ) < 1 → 𝐴 ≠ 1 )
18	2 17	syl	⊢ ( 𝜑 → 𝐴 ≠ 1 )
19	18	necomd	⊢ ( 𝜑 → 1 ≠ 𝐴 )
20		subeq0	⊢ ( ( 1 ∈ ℂ ∧ 𝐴 ∈ ℂ ) → ( ( 1 − 𝐴 ) = 0 ↔ 1 = 𝐴 ) )
21	7 1 20	sylancr	⊢ ( 𝜑 → ( ( 1 − 𝐴 ) = 0 ↔ 1 = 𝐴 ) )
22	21	necon3bid	⊢ ( 𝜑 → ( ( 1 − 𝐴 ) ≠ 0 ↔ 1 ≠ 𝐴 ) )
23	19 22	mpbird	⊢ ( 𝜑 → ( 1 − 𝐴 ) ≠ 0 )
24	1 9 23	divcld	⊢ ( 𝜑 → ( 𝐴 / ( 1 − 𝐴 ) ) ∈ ℂ )
25		nn0ex	⊢ ℕ0 ∈ V
26	25	mptex	⊢ ( 𝑛 ∈ ℕ0 ↦ ( ( 𝐴 ↑ ( 𝑛 + 1 ) ) / ( 1 − 𝐴 ) ) ) ∈ V
27	26	a1i	⊢ ( 𝜑 → ( 𝑛 ∈ ℕ0 ↦ ( ( 𝐴 ↑ ( 𝑛 + 1 ) ) / ( 1 − 𝐴 ) ) ) ∈ V )
28		oveq2	⊢ ( 𝑛 = 𝑗 → ( 𝐴 ↑ 𝑛 ) = ( 𝐴 ↑ 𝑗 ) )
29		eqid	⊢ ( 𝑛 ∈ ℕ0 ↦ ( 𝐴 ↑ 𝑛 ) ) = ( 𝑛 ∈ ℕ0 ↦ ( 𝐴 ↑ 𝑛 ) )
30		ovex	⊢ ( 𝐴 ↑ 𝑗 ) ∈ V
31	28 29 30	fvmpt	⊢ ( 𝑗 ∈ ℕ0 → ( ( 𝑛 ∈ ℕ0 ↦ ( 𝐴 ↑ 𝑛 ) ) ‘ 𝑗 ) = ( 𝐴 ↑ 𝑗 ) )
32	31	adantl	⊢ ( ( 𝜑 ∧ 𝑗 ∈ ℕ0 ) → ( ( 𝑛 ∈ ℕ0 ↦ ( 𝐴 ↑ 𝑛 ) ) ‘ 𝑗 ) = ( 𝐴 ↑ 𝑗 ) )
33		expcl	⊢ ( ( 𝐴 ∈ ℂ ∧ 𝑗 ∈ ℕ0 ) → ( 𝐴 ↑ 𝑗 ) ∈ ℂ )
34	1 33	sylan	⊢ ( ( 𝜑 ∧ 𝑗 ∈ ℕ0 ) → ( 𝐴 ↑ 𝑗 ) ∈ ℂ )
35	32 34	eqeltrd	⊢ ( ( 𝜑 ∧ 𝑗 ∈ ℕ0 ) → ( ( 𝑛 ∈ ℕ0 ↦ ( 𝐴 ↑ 𝑛 ) ) ‘ 𝑗 ) ∈ ℂ )
36		expp1	⊢ ( ( 𝐴 ∈ ℂ ∧ 𝑗 ∈ ℕ0 ) → ( 𝐴 ↑ ( 𝑗 + 1 ) ) = ( ( 𝐴 ↑ 𝑗 ) · 𝐴 ) )
37	1 36	sylan	⊢ ( ( 𝜑 ∧ 𝑗 ∈ ℕ0 ) → ( 𝐴 ↑ ( 𝑗 + 1 ) ) = ( ( 𝐴 ↑ 𝑗 ) · 𝐴 ) )
38	1	adantr	⊢ ( ( 𝜑 ∧ 𝑗 ∈ ℕ0 ) → 𝐴 ∈ ℂ )
39	34 38	mulcomd	⊢ ( ( 𝜑 ∧ 𝑗 ∈ ℕ0 ) → ( ( 𝐴 ↑ 𝑗 ) · 𝐴 ) = ( 𝐴 · ( 𝐴 ↑ 𝑗 ) ) )
40	37 39	eqtrd	⊢ ( ( 𝜑 ∧ 𝑗 ∈ ℕ0 ) → ( 𝐴 ↑ ( 𝑗 + 1 ) ) = ( 𝐴 · ( 𝐴 ↑ 𝑗 ) ) )
41	40	oveq1d	⊢ ( ( 𝜑 ∧ 𝑗 ∈ ℕ0 ) → ( ( 𝐴 ↑ ( 𝑗 + 1 ) ) / ( 1 − 𝐴 ) ) = ( ( 𝐴 · ( 𝐴 ↑ 𝑗 ) ) / ( 1 − 𝐴 ) ) )
42	9	adantr	⊢ ( ( 𝜑 ∧ 𝑗 ∈ ℕ0 ) → ( 1 − 𝐴 ) ∈ ℂ )
43	23	adantr	⊢ ( ( 𝜑 ∧ 𝑗 ∈ ℕ0 ) → ( 1 − 𝐴 ) ≠ 0 )
44	38 34 42 43	div23d	⊢ ( ( 𝜑 ∧ 𝑗 ∈ ℕ0 ) → ( ( 𝐴 · ( 𝐴 ↑ 𝑗 ) ) / ( 1 − 𝐴 ) ) = ( ( 𝐴 / ( 1 − 𝐴 ) ) · ( 𝐴 ↑ 𝑗 ) ) )
45	41 44	eqtrd	⊢ ( ( 𝜑 ∧ 𝑗 ∈ ℕ0 ) → ( ( 𝐴 ↑ ( 𝑗 + 1 ) ) / ( 1 − 𝐴 ) ) = ( ( 𝐴 / ( 1 − 𝐴 ) ) · ( 𝐴 ↑ 𝑗 ) ) )
46		oveq1	⊢ ( 𝑛 = 𝑗 → ( 𝑛 + 1 ) = ( 𝑗 + 1 ) )
47	46	oveq2d	⊢ ( 𝑛 = 𝑗 → ( 𝐴 ↑ ( 𝑛 + 1 ) ) = ( 𝐴 ↑ ( 𝑗 + 1 ) ) )
48	47	oveq1d	⊢ ( 𝑛 = 𝑗 → ( ( 𝐴 ↑ ( 𝑛 + 1 ) ) / ( 1 − 𝐴 ) ) = ( ( 𝐴 ↑ ( 𝑗 + 1 ) ) / ( 1 − 𝐴 ) ) )
49		eqid	⊢ ( 𝑛 ∈ ℕ0 ↦ ( ( 𝐴 ↑ ( 𝑛 + 1 ) ) / ( 1 − 𝐴 ) ) ) = ( 𝑛 ∈ ℕ0 ↦ ( ( 𝐴 ↑ ( 𝑛 + 1 ) ) / ( 1 − 𝐴 ) ) )
50		ovex	⊢ ( ( 𝐴 ↑ ( 𝑗 + 1 ) ) / ( 1 − 𝐴 ) ) ∈ V
51	48 49 50	fvmpt	⊢ ( 𝑗 ∈ ℕ0 → ( ( 𝑛 ∈ ℕ0 ↦ ( ( 𝐴 ↑ ( 𝑛 + 1 ) ) / ( 1 − 𝐴 ) ) ) ‘ 𝑗 ) = ( ( 𝐴 ↑ ( 𝑗 + 1 ) ) / ( 1 − 𝐴 ) ) )
52	51	adantl	⊢ ( ( 𝜑 ∧ 𝑗 ∈ ℕ0 ) → ( ( 𝑛 ∈ ℕ0 ↦ ( ( 𝐴 ↑ ( 𝑛 + 1 ) ) / ( 1 − 𝐴 ) ) ) ‘ 𝑗 ) = ( ( 𝐴 ↑ ( 𝑗 + 1 ) ) / ( 1 − 𝐴 ) ) )
53	32	oveq2d	⊢ ( ( 𝜑 ∧ 𝑗 ∈ ℕ0 ) → ( ( 𝐴 / ( 1 − 𝐴 ) ) · ( ( 𝑛 ∈ ℕ0 ↦ ( 𝐴 ↑ 𝑛 ) ) ‘ 𝑗 ) ) = ( ( 𝐴 / ( 1 − 𝐴 ) ) · ( 𝐴 ↑ 𝑗 ) ) )
54	45 52 53	3eqtr4d	⊢ ( ( 𝜑 ∧ 𝑗 ∈ ℕ0 ) → ( ( 𝑛 ∈ ℕ0 ↦ ( ( 𝐴 ↑ ( 𝑛 + 1 ) ) / ( 1 − 𝐴 ) ) ) ‘ 𝑗 ) = ( ( 𝐴 / ( 1 − 𝐴 ) ) · ( ( 𝑛 ∈ ℕ0 ↦ ( 𝐴 ↑ 𝑛 ) ) ‘ 𝑗 ) ) )
55	4 5 6 24 27 35 54	climmulc2	⊢ ( 𝜑 → ( 𝑛 ∈ ℕ0 ↦ ( ( 𝐴 ↑ ( 𝑛 + 1 ) ) / ( 1 − 𝐴 ) ) ) ⇝ ( ( 𝐴 / ( 1 − 𝐴 ) ) · 0 ) )
56	24	mul01d	⊢ ( 𝜑 → ( ( 𝐴 / ( 1 − 𝐴 ) ) · 0 ) = 0 )
57	55 56	breqtrd	⊢ ( 𝜑 → ( 𝑛 ∈ ℕ0 ↦ ( ( 𝐴 ↑ ( 𝑛 + 1 ) ) / ( 1 − 𝐴 ) ) ) ⇝ 0 )
58	9 23	reccld	⊢ ( 𝜑 → ( 1 / ( 1 − 𝐴 ) ) ∈ ℂ )
59		seqex	⊢ seq 0 ( + , 𝐹 ) ∈ V
60	59	a1i	⊢ ( 𝜑 → seq 0 ( + , 𝐹 ) ∈ V )
61		peano2nn0	⊢ ( 𝑗 ∈ ℕ0 → ( 𝑗 + 1 ) ∈ ℕ0 )
62		expcl	⊢ ( ( 𝐴 ∈ ℂ ∧ ( 𝑗 + 1 ) ∈ ℕ0 ) → ( 𝐴 ↑ ( 𝑗 + 1 ) ) ∈ ℂ )
63	1 61 62	syl2an	⊢ ( ( 𝜑 ∧ 𝑗 ∈ ℕ0 ) → ( 𝐴 ↑ ( 𝑗 + 1 ) ) ∈ ℂ )
64	63 42 43	divcld	⊢ ( ( 𝜑 ∧ 𝑗 ∈ ℕ0 ) → ( ( 𝐴 ↑ ( 𝑗 + 1 ) ) / ( 1 − 𝐴 ) ) ∈ ℂ )
65	52 64	eqeltrd	⊢ ( ( 𝜑 ∧ 𝑗 ∈ ℕ0 ) → ( ( 𝑛 ∈ ℕ0 ↦ ( ( 𝐴 ↑ ( 𝑛 + 1 ) ) / ( 1 − 𝐴 ) ) ) ‘ 𝑗 ) ∈ ℂ )
66		nn0cn	⊢ ( 𝑗 ∈ ℕ0 → 𝑗 ∈ ℂ )
67	66	adantl	⊢ ( ( 𝜑 ∧ 𝑗 ∈ ℕ0 ) → 𝑗 ∈ ℂ )
68		pncan	⊢ ( ( 𝑗 ∈ ℂ ∧ 1 ∈ ℂ ) → ( ( 𝑗 + 1 ) − 1 ) = 𝑗 )
69	67 7 68	sylancl	⊢ ( ( 𝜑 ∧ 𝑗 ∈ ℕ0 ) → ( ( 𝑗 + 1 ) − 1 ) = 𝑗 )
70	69	oveq2d	⊢ ( ( 𝜑 ∧ 𝑗 ∈ ℕ0 ) → ( 0 ... ( ( 𝑗 + 1 ) − 1 ) ) = ( 0 ... 𝑗 ) )
71	70	sumeq1d	⊢ ( ( 𝜑 ∧ 𝑗 ∈ ℕ0 ) → Σ 𝑘 ∈ ( 0 ... ( ( 𝑗 + 1 ) − 1 ) ) ( 𝐴 ↑ 𝑘 ) = Σ 𝑘 ∈ ( 0 ... 𝑗 ) ( 𝐴 ↑ 𝑘 ) )
72	7	a1i	⊢ ( ( 𝜑 ∧ 𝑗 ∈ ℕ0 ) → 1 ∈ ℂ )
73	72 63 42 43	divsubdird	⊢ ( ( 𝜑 ∧ 𝑗 ∈ ℕ0 ) → ( ( 1 − ( 𝐴 ↑ ( 𝑗 + 1 ) ) ) / ( 1 − 𝐴 ) ) = ( ( 1 / ( 1 − 𝐴 ) ) − ( ( 𝐴 ↑ ( 𝑗 + 1 ) ) / ( 1 − 𝐴 ) ) ) )
74	18	adantr	⊢ ( ( 𝜑 ∧ 𝑗 ∈ ℕ0 ) → 𝐴 ≠ 1 )
75	61	adantl	⊢ ( ( 𝜑 ∧ 𝑗 ∈ ℕ0 ) → ( 𝑗 + 1 ) ∈ ℕ0 )
76	38 74 75	geoser	⊢ ( ( 𝜑 ∧ 𝑗 ∈ ℕ0 ) → Σ 𝑘 ∈ ( 0 ... ( ( 𝑗 + 1 ) − 1 ) ) ( 𝐴 ↑ 𝑘 ) = ( ( 1 − ( 𝐴 ↑ ( 𝑗 + 1 ) ) ) / ( 1 − 𝐴 ) ) )
77	52	oveq2d	⊢ ( ( 𝜑 ∧ 𝑗 ∈ ℕ0 ) → ( ( 1 / ( 1 − 𝐴 ) ) − ( ( 𝑛 ∈ ℕ0 ↦ ( ( 𝐴 ↑ ( 𝑛 + 1 ) ) / ( 1 − 𝐴 ) ) ) ‘ 𝑗 ) ) = ( ( 1 / ( 1 − 𝐴 ) ) − ( ( 𝐴 ↑ ( 𝑗 + 1 ) ) / ( 1 − 𝐴 ) ) ) )
78	73 76 77	3eqtr4d	⊢ ( ( 𝜑 ∧ 𝑗 ∈ ℕ0 ) → Σ 𝑘 ∈ ( 0 ... ( ( 𝑗 + 1 ) − 1 ) ) ( 𝐴 ↑ 𝑘 ) = ( ( 1 / ( 1 − 𝐴 ) ) − ( ( 𝑛 ∈ ℕ0 ↦ ( ( 𝐴 ↑ ( 𝑛 + 1 ) ) / ( 1 − 𝐴 ) ) ) ‘ 𝑗 ) ) )
79		simpll	⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ℕ0 ) ∧ 𝑘 ∈ ( 0 ... 𝑗 ) ) → 𝜑 )
80		elfznn0	⊢ ( 𝑘 ∈ ( 0 ... 𝑗 ) → 𝑘 ∈ ℕ0 )
81	80	adantl	⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ℕ0 ) ∧ 𝑘 ∈ ( 0 ... 𝑗 ) ) → 𝑘 ∈ ℕ0 )
82	79 81 3	syl2anc	⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ℕ0 ) ∧ 𝑘 ∈ ( 0 ... 𝑗 ) ) → ( 𝐹 ‘ 𝑘 ) = ( 𝐴 ↑ 𝑘 ) )
83		simpr	⊢ ( ( 𝜑 ∧ 𝑗 ∈ ℕ0 ) → 𝑗 ∈ ℕ0 )
84	83 4	eleqtrdi	⊢ ( ( 𝜑 ∧ 𝑗 ∈ ℕ0 ) → 𝑗 ∈ ( ℤ≥ ‘ 0 ) )
85	79 1	syl	⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ℕ0 ) ∧ 𝑘 ∈ ( 0 ... 𝑗 ) ) → 𝐴 ∈ ℂ )
86	85 81	expcld	⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ℕ0 ) ∧ 𝑘 ∈ ( 0 ... 𝑗 ) ) → ( 𝐴 ↑ 𝑘 ) ∈ ℂ )
87	82 84 86	fsumser	⊢ ( ( 𝜑 ∧ 𝑗 ∈ ℕ0 ) → Σ 𝑘 ∈ ( 0 ... 𝑗 ) ( 𝐴 ↑ 𝑘 ) = ( seq 0 ( + , 𝐹 ) ‘ 𝑗 ) )
88	71 78 87	3eqtr3rd	⊢ ( ( 𝜑 ∧ 𝑗 ∈ ℕ0 ) → ( seq 0 ( + , 𝐹 ) ‘ 𝑗 ) = ( ( 1 / ( 1 − 𝐴 ) ) − ( ( 𝑛 ∈ ℕ0 ↦ ( ( 𝐴 ↑ ( 𝑛 + 1 ) ) / ( 1 − 𝐴 ) ) ) ‘ 𝑗 ) ) )
89	4 5 57 58 60 65 88	climsubc2	⊢ ( 𝜑 → seq 0 ( + , 𝐹 ) ⇝ ( ( 1 / ( 1 − 𝐴 ) ) − 0 ) )
90	58	subid1d	⊢ ( 𝜑 → ( ( 1 / ( 1 − 𝐴 ) ) − 0 ) = ( 1 / ( 1 − 𝐴 ) ) )
91	89 90	breqtrd	⊢ ( 𝜑 → seq 0 ( + , 𝐹 ) ⇝ ( 1 / ( 1 − 𝐴 ) ) )