Theorem geo2lim

Description: The value of the infinite geometric series 2 ^ -u 1 + 2 ^ -u 2 + ... , multiplied by a constant. (Contributed by Mario Carneiro, 15-Jun-2014)

	Ref	Expression
Hypothesis	geo2lim.1	⊢ 𝐹 = ( 𝑘 ∈ ℕ ↦ ( 𝐴 / ( 2 ↑ 𝑘 ) ) )
Assertion	geo2lim	⊢ ( 𝐴 ∈ ℂ → seq 1 ( + , 𝐹 ) ⇝ 𝐴 )

Proof

Step	Hyp	Ref	Expression
1		geo2lim.1	⊢ 𝐹 = ( 𝑘 ∈ ℕ ↦ ( 𝐴 / ( 2 ↑ 𝑘 ) ) )
2		nnuz	⊢ ℕ = ( ℤ≥ ‘ 1 )
3		1zzd	⊢ ( 𝐴 ∈ ℂ → 1 ∈ ℤ )
4		halfcn	⊢ ( 1 / 2 ) ∈ ℂ
5	4	a1i	⊢ ( 𝐴 ∈ ℂ → ( 1 / 2 ) ∈ ℂ )
6		halfre	⊢ ( 1 / 2 ) ∈ ℝ
7		halfge0	⊢ 0 ≤ ( 1 / 2 )
8		absid	⊢ ( ( ( 1 / 2 ) ∈ ℝ ∧ 0 ≤ ( 1 / 2 ) ) → ( abs ‘ ( 1 / 2 ) ) = ( 1 / 2 ) )
9	6 7 8	mp2an	⊢ ( abs ‘ ( 1 / 2 ) ) = ( 1 / 2 )
10		halflt1	⊢ ( 1 / 2 ) < 1
11	9 10	eqbrtri	⊢ ( abs ‘ ( 1 / 2 ) ) < 1
12	11	a1i	⊢ ( 𝐴 ∈ ℂ → ( abs ‘ ( 1 / 2 ) ) < 1 )
13	5 12	expcnv	⊢ ( 𝐴 ∈ ℂ → ( 𝑘 ∈ ℕ0 ↦ ( ( 1 / 2 ) ↑ 𝑘 ) ) ⇝ 0 )
14		id	⊢ ( 𝐴 ∈ ℂ → 𝐴 ∈ ℂ )
15		nnex	⊢ ℕ ∈ V
16	15	mptex	⊢ ( 𝑘 ∈ ℕ ↦ ( 𝐴 / ( 2 ↑ 𝑘 ) ) ) ∈ V
17	1 16	eqeltri	⊢ 𝐹 ∈ V
18	17	a1i	⊢ ( 𝐴 ∈ ℂ → 𝐹 ∈ V )
19		nnnn0	⊢ ( 𝑗 ∈ ℕ → 𝑗 ∈ ℕ0 )
20	19	adantl	⊢ ( ( 𝐴 ∈ ℂ ∧ 𝑗 ∈ ℕ ) → 𝑗 ∈ ℕ0 )
21		oveq2	⊢ ( 𝑘 = 𝑗 → ( ( 1 / 2 ) ↑ 𝑘 ) = ( ( 1 / 2 ) ↑ 𝑗 ) )
22		eqid	⊢ ( 𝑘 ∈ ℕ0 ↦ ( ( 1 / 2 ) ↑ 𝑘 ) ) = ( 𝑘 ∈ ℕ0 ↦ ( ( 1 / 2 ) ↑ 𝑘 ) )
23		ovex	⊢ ( ( 1 / 2 ) ↑ 𝑗 ) ∈ V
24	21 22 23	fvmpt	⊢ ( 𝑗 ∈ ℕ0 → ( ( 𝑘 ∈ ℕ0 ↦ ( ( 1 / 2 ) ↑ 𝑘 ) ) ‘ 𝑗 ) = ( ( 1 / 2 ) ↑ 𝑗 ) )
25	20 24	syl	⊢ ( ( 𝐴 ∈ ℂ ∧ 𝑗 ∈ ℕ ) → ( ( 𝑘 ∈ ℕ0 ↦ ( ( 1 / 2 ) ↑ 𝑘 ) ) ‘ 𝑗 ) = ( ( 1 / 2 ) ↑ 𝑗 ) )
26		2cn	⊢ 2 ∈ ℂ
27		2ne0	⊢ 2 ≠ 0
28		nnz	⊢ ( 𝑗 ∈ ℕ → 𝑗 ∈ ℤ )
29	28	adantl	⊢ ( ( 𝐴 ∈ ℂ ∧ 𝑗 ∈ ℕ ) → 𝑗 ∈ ℤ )
30		exprec	⊢ ( ( 2 ∈ ℂ ∧ 2 ≠ 0 ∧ 𝑗 ∈ ℤ ) → ( ( 1 / 2 ) ↑ 𝑗 ) = ( 1 / ( 2 ↑ 𝑗 ) ) )
31	26 27 29 30	mp3an12i	⊢ ( ( 𝐴 ∈ ℂ ∧ 𝑗 ∈ ℕ ) → ( ( 1 / 2 ) ↑ 𝑗 ) = ( 1 / ( 2 ↑ 𝑗 ) ) )
32	25 31	eqtrd	⊢ ( ( 𝐴 ∈ ℂ ∧ 𝑗 ∈ ℕ ) → ( ( 𝑘 ∈ ℕ0 ↦ ( ( 1 / 2 ) ↑ 𝑘 ) ) ‘ 𝑗 ) = ( 1 / ( 2 ↑ 𝑗 ) ) )
33		2nn	⊢ 2 ∈ ℕ
34		nnexpcl	⊢ ( ( 2 ∈ ℕ ∧ 𝑗 ∈ ℕ0 ) → ( 2 ↑ 𝑗 ) ∈ ℕ )
35	33 20 34	sylancr	⊢ ( ( 𝐴 ∈ ℂ ∧ 𝑗 ∈ ℕ ) → ( 2 ↑ 𝑗 ) ∈ ℕ )
36	35	nnrecred	⊢ ( ( 𝐴 ∈ ℂ ∧ 𝑗 ∈ ℕ ) → ( 1 / ( 2 ↑ 𝑗 ) ) ∈ ℝ )
37	36	recnd	⊢ ( ( 𝐴 ∈ ℂ ∧ 𝑗 ∈ ℕ ) → ( 1 / ( 2 ↑ 𝑗 ) ) ∈ ℂ )
38	32 37	eqeltrd	⊢ ( ( 𝐴 ∈ ℂ ∧ 𝑗 ∈ ℕ ) → ( ( 𝑘 ∈ ℕ0 ↦ ( ( 1 / 2 ) ↑ 𝑘 ) ) ‘ 𝑗 ) ∈ ℂ )
39		simpl	⊢ ( ( 𝐴 ∈ ℂ ∧ 𝑗 ∈ ℕ ) → 𝐴 ∈ ℂ )
40	35	nncnd	⊢ ( ( 𝐴 ∈ ℂ ∧ 𝑗 ∈ ℕ ) → ( 2 ↑ 𝑗 ) ∈ ℂ )
41	35	nnne0d	⊢ ( ( 𝐴 ∈ ℂ ∧ 𝑗 ∈ ℕ ) → ( 2 ↑ 𝑗 ) ≠ 0 )
42	39 40 41	divrecd	⊢ ( ( 𝐴 ∈ ℂ ∧ 𝑗 ∈ ℕ ) → ( 𝐴 / ( 2 ↑ 𝑗 ) ) = ( 𝐴 · ( 1 / ( 2 ↑ 𝑗 ) ) ) )
43		oveq2	⊢ ( 𝑘 = 𝑗 → ( 2 ↑ 𝑘 ) = ( 2 ↑ 𝑗 ) )
44	43	oveq2d	⊢ ( 𝑘 = 𝑗 → ( 𝐴 / ( 2 ↑ 𝑘 ) ) = ( 𝐴 / ( 2 ↑ 𝑗 ) ) )
45		ovex	⊢ ( 𝐴 / ( 2 ↑ 𝑗 ) ) ∈ V
46	44 1 45	fvmpt	⊢ ( 𝑗 ∈ ℕ → ( 𝐹 ‘ 𝑗 ) = ( 𝐴 / ( 2 ↑ 𝑗 ) ) )
47	46	adantl	⊢ ( ( 𝐴 ∈ ℂ ∧ 𝑗 ∈ ℕ ) → ( 𝐹 ‘ 𝑗 ) = ( 𝐴 / ( 2 ↑ 𝑗 ) ) )
48	32	oveq2d	⊢ ( ( 𝐴 ∈ ℂ ∧ 𝑗 ∈ ℕ ) → ( 𝐴 · ( ( 𝑘 ∈ ℕ0 ↦ ( ( 1 / 2 ) ↑ 𝑘 ) ) ‘ 𝑗 ) ) = ( 𝐴 · ( 1 / ( 2 ↑ 𝑗 ) ) ) )
49	42 47 48	3eqtr4d	⊢ ( ( 𝐴 ∈ ℂ ∧ 𝑗 ∈ ℕ ) → ( 𝐹 ‘ 𝑗 ) = ( 𝐴 · ( ( 𝑘 ∈ ℕ0 ↦ ( ( 1 / 2 ) ↑ 𝑘 ) ) ‘ 𝑗 ) ) )
50	2 3 13 14 18 38 49	climmulc2	⊢ ( 𝐴 ∈ ℂ → 𝐹 ⇝ ( 𝐴 · 0 ) )
51		mul01	⊢ ( 𝐴 ∈ ℂ → ( 𝐴 · 0 ) = 0 )
52	50 51	breqtrd	⊢ ( 𝐴 ∈ ℂ → 𝐹 ⇝ 0 )
53		seqex	⊢ seq 1 ( + , 𝐹 ) ∈ V
54	53	a1i	⊢ ( 𝐴 ∈ ℂ → seq 1 ( + , 𝐹 ) ∈ V )
55	39 40 41	divcld	⊢ ( ( 𝐴 ∈ ℂ ∧ 𝑗 ∈ ℕ ) → ( 𝐴 / ( 2 ↑ 𝑗 ) ) ∈ ℂ )
56	47 55	eqeltrd	⊢ ( ( 𝐴 ∈ ℂ ∧ 𝑗 ∈ ℕ ) → ( 𝐹 ‘ 𝑗 ) ∈ ℂ )
57	47	oveq2d	⊢ ( ( 𝐴 ∈ ℂ ∧ 𝑗 ∈ ℕ ) → ( 𝐴 − ( 𝐹 ‘ 𝑗 ) ) = ( 𝐴 − ( 𝐴 / ( 2 ↑ 𝑗 ) ) ) )
58		geo2sum	⊢ ( ( 𝑗 ∈ ℕ ∧ 𝐴 ∈ ℂ ) → Σ 𝑛 ∈ ( 1 ... 𝑗 ) ( 𝐴 / ( 2 ↑ 𝑛 ) ) = ( 𝐴 − ( 𝐴 / ( 2 ↑ 𝑗 ) ) ) )
59	58	ancoms	⊢ ( ( 𝐴 ∈ ℂ ∧ 𝑗 ∈ ℕ ) → Σ 𝑛 ∈ ( 1 ... 𝑗 ) ( 𝐴 / ( 2 ↑ 𝑛 ) ) = ( 𝐴 − ( 𝐴 / ( 2 ↑ 𝑗 ) ) ) )
60		elfznn	⊢ ( 𝑛 ∈ ( 1 ... 𝑗 ) → 𝑛 ∈ ℕ )
61	60	adantl	⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝑗 ∈ ℕ ) ∧ 𝑛 ∈ ( 1 ... 𝑗 ) ) → 𝑛 ∈ ℕ )
62		oveq2	⊢ ( 𝑘 = 𝑛 → ( 2 ↑ 𝑘 ) = ( 2 ↑ 𝑛 ) )
63	62	oveq2d	⊢ ( 𝑘 = 𝑛 → ( 𝐴 / ( 2 ↑ 𝑘 ) ) = ( 𝐴 / ( 2 ↑ 𝑛 ) ) )
64		ovex	⊢ ( 𝐴 / ( 2 ↑ 𝑛 ) ) ∈ V
65	63 1 64	fvmpt	⊢ ( 𝑛 ∈ ℕ → ( 𝐹 ‘ 𝑛 ) = ( 𝐴 / ( 2 ↑ 𝑛 ) ) )
66	61 65	syl	⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝑗 ∈ ℕ ) ∧ 𝑛 ∈ ( 1 ... 𝑗 ) ) → ( 𝐹 ‘ 𝑛 ) = ( 𝐴 / ( 2 ↑ 𝑛 ) ) )
67		simpr	⊢ ( ( 𝐴 ∈ ℂ ∧ 𝑗 ∈ ℕ ) → 𝑗 ∈ ℕ )
68	67 2	eleqtrdi	⊢ ( ( 𝐴 ∈ ℂ ∧ 𝑗 ∈ ℕ ) → 𝑗 ∈ ( ℤ≥ ‘ 1 ) )
69		simpll	⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝑗 ∈ ℕ ) ∧ 𝑛 ∈ ( 1 ... 𝑗 ) ) → 𝐴 ∈ ℂ )
70		nnnn0	⊢ ( 𝑛 ∈ ℕ → 𝑛 ∈ ℕ0 )
71		nnexpcl	⊢ ( ( 2 ∈ ℕ ∧ 𝑛 ∈ ℕ0 ) → ( 2 ↑ 𝑛 ) ∈ ℕ )
72	33 70 71	sylancr	⊢ ( 𝑛 ∈ ℕ → ( 2 ↑ 𝑛 ) ∈ ℕ )
73	61 72	syl	⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝑗 ∈ ℕ ) ∧ 𝑛 ∈ ( 1 ... 𝑗 ) ) → ( 2 ↑ 𝑛 ) ∈ ℕ )
74	73	nncnd	⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝑗 ∈ ℕ ) ∧ 𝑛 ∈ ( 1 ... 𝑗 ) ) → ( 2 ↑ 𝑛 ) ∈ ℂ )
75	73	nnne0d	⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝑗 ∈ ℕ ) ∧ 𝑛 ∈ ( 1 ... 𝑗 ) ) → ( 2 ↑ 𝑛 ) ≠ 0 )
76	69 74 75	divcld	⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝑗 ∈ ℕ ) ∧ 𝑛 ∈ ( 1 ... 𝑗 ) ) → ( 𝐴 / ( 2 ↑ 𝑛 ) ) ∈ ℂ )
77	66 68 76	fsumser	⊢ ( ( 𝐴 ∈ ℂ ∧ 𝑗 ∈ ℕ ) → Σ 𝑛 ∈ ( 1 ... 𝑗 ) ( 𝐴 / ( 2 ↑ 𝑛 ) ) = ( seq 1 ( + , 𝐹 ) ‘ 𝑗 ) )
78	57 59 77	3eqtr2rd	⊢ ( ( 𝐴 ∈ ℂ ∧ 𝑗 ∈ ℕ ) → ( seq 1 ( + , 𝐹 ) ‘ 𝑗 ) = ( 𝐴 − ( 𝐹 ‘ 𝑗 ) ) )
79	2 3 52 14 54 56 78	climsubc2	⊢ ( 𝐴 ∈ ℂ → seq 1 ( + , 𝐹 ) ⇝ ( 𝐴 − 0 ) )
80		subid1	⊢ ( 𝐴 ∈ ℂ → ( 𝐴 − 0 ) = 𝐴 )
81	79 80	breqtrd	⊢ ( 𝐴 ∈ ℂ → seq 1 ( + , 𝐹 ) ⇝ 𝐴 )