Metamath Proof Explorer

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 ( + , 𝐹 ) ⇝ 𝐴 )