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 
|- F = ( k e. NN |-> ( A / ( 2 ^ k ) ) )
Assertion geo2lim 
|- ( A e. CC -> seq 1 ( + , F ) ~~> A )

Proof

Step Hyp Ref Expression
1 geo2lim.1 
 |-  F = ( k e. NN |-> ( A / ( 2 ^ k ) ) )
2 nnuz 
 |-  NN = ( ZZ>= ` 1 )
3 1zzd 
 |-  ( A e. CC -> 1 e. ZZ )
4 halfcn 
 |-  ( 1 / 2 ) e. CC
5 4 a1i 
 |-  ( A e. CC -> ( 1 / 2 ) e. CC )
6 halfre 
 |-  ( 1 / 2 ) e. RR
7 halfge0 
 |-  0 <_ ( 1 / 2 )
8 absid 
 |-  ( ( ( 1 / 2 ) e. RR /\ 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 
 |-  ( A e. CC -> ( abs ` ( 1 / 2 ) ) < 1 )
13 5 12 expcnv 
 |-  ( A e. CC -> ( k e. NN0 |-> ( ( 1 / 2 ) ^ k ) ) ~~> 0 )
14 id 
 |-  ( A e. CC -> A e. CC )
15 nnex 
 |-  NN e. _V
16 15 mptex 
 |-  ( k e. NN |-> ( A / ( 2 ^ k ) ) ) e. _V
17 1 16 eqeltri 
 |-  F e. _V
18 17 a1i 
 |-  ( A e. CC -> F e. _V )
19 nnnn0 
 |-  ( j e. NN -> j e. NN0 )
20 19 adantl 
 |-  ( ( A e. CC /\ j e. NN ) -> j e. NN0 )
21 oveq2 
 |-  ( k = j -> ( ( 1 / 2 ) ^ k ) = ( ( 1 / 2 ) ^ j ) )
22 eqid 
 |-  ( k e. NN0 |-> ( ( 1 / 2 ) ^ k ) ) = ( k e. NN0 |-> ( ( 1 / 2 ) ^ k ) )
23 ovex 
 |-  ( ( 1 / 2 ) ^ j ) e. _V
24 21 22 23 fvmpt 
 |-  ( j e. NN0 -> ( ( k e. NN0 |-> ( ( 1 / 2 ) ^ k ) ) ` j ) = ( ( 1 / 2 ) ^ j ) )
25 20 24 syl 
 |-  ( ( A e. CC /\ j e. NN ) -> ( ( k e. NN0 |-> ( ( 1 / 2 ) ^ k ) ) ` j ) = ( ( 1 / 2 ) ^ j ) )
26 2cn 
 |-  2 e. CC
27 2ne0 
 |-  2 =/= 0
28 nnz 
 |-  ( j e. NN -> j e. ZZ )
29 28 adantl 
 |-  ( ( A e. CC /\ j e. NN ) -> j e. ZZ )
30 exprec 
 |-  ( ( 2 e. CC /\ 2 =/= 0 /\ j e. ZZ ) -> ( ( 1 / 2 ) ^ j ) = ( 1 / ( 2 ^ j ) ) )
31 26 27 29 30 mp3an12i 
 |-  ( ( A e. CC /\ j e. NN ) -> ( ( 1 / 2 ) ^ j ) = ( 1 / ( 2 ^ j ) ) )
32 25 31 eqtrd 
 |-  ( ( A e. CC /\ j e. NN ) -> ( ( k e. NN0 |-> ( ( 1 / 2 ) ^ k ) ) ` j ) = ( 1 / ( 2 ^ j ) ) )
33 2nn 
 |-  2 e. NN
34 nnexpcl 
 |-  ( ( 2 e. NN /\ j e. NN0 ) -> ( 2 ^ j ) e. NN )
35 33 20 34 sylancr 
 |-  ( ( A e. CC /\ j e. NN ) -> ( 2 ^ j ) e. NN )
36 35 nnrecred 
 |-  ( ( A e. CC /\ j e. NN ) -> ( 1 / ( 2 ^ j ) ) e. RR )
37 36 recnd 
 |-  ( ( A e. CC /\ j e. NN ) -> ( 1 / ( 2 ^ j ) ) e. CC )
38 32 37 eqeltrd 
 |-  ( ( A e. CC /\ j e. NN ) -> ( ( k e. NN0 |-> ( ( 1 / 2 ) ^ k ) ) ` j ) e. CC )
39 simpl 
 |-  ( ( A e. CC /\ j e. NN ) -> A e. CC )
40 35 nncnd 
 |-  ( ( A e. CC /\ j e. NN ) -> ( 2 ^ j ) e. CC )
41 35 nnne0d 
 |-  ( ( A e. CC /\ j e. NN ) -> ( 2 ^ j ) =/= 0 )
42 39 40 41 divrecd 
 |-  ( ( A e. CC /\ j e. NN ) -> ( A / ( 2 ^ j ) ) = ( A x. ( 1 / ( 2 ^ j ) ) ) )
43 oveq2 
 |-  ( k = j -> ( 2 ^ k ) = ( 2 ^ j ) )
44 43 oveq2d 
 |-  ( k = j -> ( A / ( 2 ^ k ) ) = ( A / ( 2 ^ j ) ) )
45 ovex 
 |-  ( A / ( 2 ^ j ) ) e. _V
46 44 1 45 fvmpt 
 |-  ( j e. NN -> ( F ` j ) = ( A / ( 2 ^ j ) ) )
47 46 adantl 
 |-  ( ( A e. CC /\ j e. NN ) -> ( F ` j ) = ( A / ( 2 ^ j ) ) )
48 32 oveq2d 
 |-  ( ( A e. CC /\ j e. NN ) -> ( A x. ( ( k e. NN0 |-> ( ( 1 / 2 ) ^ k ) ) ` j ) ) = ( A x. ( 1 / ( 2 ^ j ) ) ) )
49 42 47 48 3eqtr4d 
 |-  ( ( A e. CC /\ j e. NN ) -> ( F ` j ) = ( A x. ( ( k e. NN0 |-> ( ( 1 / 2 ) ^ k ) ) ` j ) ) )
50 2 3 13 14 18 38 49 climmulc2 
 |-  ( A e. CC -> F ~~> ( A x. 0 ) )
51 mul01 
 |-  ( A e. CC -> ( A x. 0 ) = 0 )
52 50 51 breqtrd 
 |-  ( A e. CC -> F ~~> 0 )
53 seqex 
 |-  seq 1 ( + , F ) e. _V
54 53 a1i 
 |-  ( A e. CC -> seq 1 ( + , F ) e. _V )
55 39 40 41 divcld 
 |-  ( ( A e. CC /\ j e. NN ) -> ( A / ( 2 ^ j ) ) e. CC )
56 47 55 eqeltrd 
 |-  ( ( A e. CC /\ j e. NN ) -> ( F ` j ) e. CC )
57 47 oveq2d 
 |-  ( ( A e. CC /\ j e. NN ) -> ( A - ( F ` j ) ) = ( A - ( A / ( 2 ^ j ) ) ) )
58 geo2sum 
 |-  ( ( j e. NN /\ A e. CC ) -> sum_ n e. ( 1 ... j ) ( A / ( 2 ^ n ) ) = ( A - ( A / ( 2 ^ j ) ) ) )
59 58 ancoms 
 |-  ( ( A e. CC /\ j e. NN ) -> sum_ n e. ( 1 ... j ) ( A / ( 2 ^ n ) ) = ( A - ( A / ( 2 ^ j ) ) ) )
60 elfznn 
 |-  ( n e. ( 1 ... j ) -> n e. NN )
61 60 adantl 
 |-  ( ( ( A e. CC /\ j e. NN ) /\ n e. ( 1 ... j ) ) -> n e. NN )
62 oveq2 
 |-  ( k = n -> ( 2 ^ k ) = ( 2 ^ n ) )
63 62 oveq2d 
 |-  ( k = n -> ( A / ( 2 ^ k ) ) = ( A / ( 2 ^ n ) ) )
64 ovex 
 |-  ( A / ( 2 ^ n ) ) e. _V
65 63 1 64 fvmpt 
 |-  ( n e. NN -> ( F ` n ) = ( A / ( 2 ^ n ) ) )
66 61 65 syl 
 |-  ( ( ( A e. CC /\ j e. NN ) /\ n e. ( 1 ... j ) ) -> ( F ` n ) = ( A / ( 2 ^ n ) ) )
67 simpr 
 |-  ( ( A e. CC /\ j e. NN ) -> j e. NN )
68 67 2 eleqtrdi 
 |-  ( ( A e. CC /\ j e. NN ) -> j e. ( ZZ>= ` 1 ) )
69 simpll 
 |-  ( ( ( A e. CC /\ j e. NN ) /\ n e. ( 1 ... j ) ) -> A e. CC )
70 nnnn0 
 |-  ( n e. NN -> n e. NN0 )
71 nnexpcl 
 |-  ( ( 2 e. NN /\ n e. NN0 ) -> ( 2 ^ n ) e. NN )
72 33 70 71 sylancr 
 |-  ( n e. NN -> ( 2 ^ n ) e. NN )
73 61 72 syl 
 |-  ( ( ( A e. CC /\ j e. NN ) /\ n e. ( 1 ... j ) ) -> ( 2 ^ n ) e. NN )
74 73 nncnd 
 |-  ( ( ( A e. CC /\ j e. NN ) /\ n e. ( 1 ... j ) ) -> ( 2 ^ n ) e. CC )
75 73 nnne0d 
 |-  ( ( ( A e. CC /\ j e. NN ) /\ n e. ( 1 ... j ) ) -> ( 2 ^ n ) =/= 0 )
76 69 74 75 divcld 
 |-  ( ( ( A e. CC /\ j e. NN ) /\ n e. ( 1 ... j ) ) -> ( A / ( 2 ^ n ) ) e. CC )
77 66 68 76 fsumser 
 |-  ( ( A e. CC /\ j e. NN ) -> sum_ n e. ( 1 ... j ) ( A / ( 2 ^ n ) ) = ( seq 1 ( + , F ) ` j ) )
78 57 59 77 3eqtr2rd 
 |-  ( ( A e. CC /\ j e. NN ) -> ( seq 1 ( + , F ) ` j ) = ( A - ( F ` j ) ) )
79 2 3 52 14 54 56 78 climsubc2 
 |-  ( A e. CC -> seq 1 ( + , F ) ~~> ( A - 0 ) )
80 subid1 
 |-  ( A e. CC -> ( A - 0 ) = A )
81 79 80 breqtrd 
 |-  ( A e. CC -> seq 1 ( + , F ) ~~> A )