Metamath Proof Explorer

Theorem sge0ad2en

Description: The value of the infinite geometric series 2 ^ -u 1 + 2 ^ -u 2 + ... , multiplied by a constant. (Contributed by Glauco Siliprandi, 11-Oct-2020)

Ref Expression
Hypothesis sge0ad2en.1 
|- ( ph -> A e. ( 0 [,) +oo ) )
Assertion sge0ad2en 
|- ( ph -> ( sum^ ` ( n e. NN |-> ( A / ( 2 ^ n ) ) ) ) = A )

Proof

Step Hyp Ref Expression
1 sge0ad2en.1 
 |-  ( ph -> A e. ( 0 [,) +oo ) )
2 nfv 
 |-  F/ n ph
3 0xr 
 |-  0 e. RR*
4 3 a1i 
 |-  ( ( ph /\ n e. NN ) -> 0 e. RR* )
5 pnfxr 
 |-  +oo e. RR*
6 5 a1i 
 |-  ( ( ph /\ n e. NN ) -> +oo e. RR* )
7 rge0ssre 
 |-  ( 0 [,) +oo ) C_ RR
8 7 1 sselid 
 |-  ( ph -> A e. RR )
9 8 adantr 
 |-  ( ( ph /\ n e. NN ) -> A e. RR )
10 2re 
 |-  2 e. RR
11 10 a1i 
 |-  ( ( ph /\ n e. NN ) -> 2 e. RR )
12 nnnn0 
 |-  ( n e. NN -> n e. NN0 )
13 12 adantl 
 |-  ( ( ph /\ n e. NN ) -> n e. NN0 )
14 11 13 reexpcld 
 |-  ( ( ph /\ n e. NN ) -> ( 2 ^ n ) e. RR )
15 2cnd 
 |-  ( ( ph /\ n e. NN ) -> 2 e. CC )
16 2ne0 
 |-  2 =/= 0
17 16 a1i 
 |-  ( ( ph /\ n e. NN ) -> 2 =/= 0 )
18 13 nn0zd 
 |-  ( ( ph /\ n e. NN ) -> n e. ZZ )
19 15 17 18 expne0d 
 |-  ( ( ph /\ n e. NN ) -> ( 2 ^ n ) =/= 0 )
20 9 14 19 redivcld 
 |-  ( ( ph /\ n e. NN ) -> ( A / ( 2 ^ n ) ) e. RR )
21 20 rexrd 
 |-  ( ( ph /\ n e. NN ) -> ( A / ( 2 ^ n ) ) e. RR* )
22 2rp 
 |-  2 e. RR+
23 22 a1i 
 |-  ( ( ph /\ n e. NN ) -> 2 e. RR+ )
24 23 18 rpexpcld 
 |-  ( ( ph /\ n e. NN ) -> ( 2 ^ n ) e. RR+ )
25 3 a1i 
 |-  ( ph -> 0 e. RR* )
26 5 a1i 
 |-  ( ph -> +oo e. RR* )
27 icogelb 
 |-  ( ( 0 e. RR* /\ +oo e. RR* /\ A e. ( 0 [,) +oo ) ) -> 0 <_ A )
28 25 26 1 27 syl3anc 
 |-  ( ph -> 0 <_ A )
29 28 adantr 
 |-  ( ( ph /\ n e. NN ) -> 0 <_ A )
30 9 24 29 divge0d 
 |-  ( ( ph /\ n e. NN ) -> 0 <_ ( A / ( 2 ^ n ) ) )
31 20 ltpnfd 
 |-  ( ( ph /\ n e. NN ) -> ( A / ( 2 ^ n ) ) < +oo )
32 4 6 21 30 31 elicod 
 |-  ( ( ph /\ n e. NN ) -> ( A / ( 2 ^ n ) ) e. ( 0 [,) +oo ) )
33 1zzd 
 |-  ( ph -> 1 e. ZZ )
34 nnuz 
 |-  NN = ( ZZ>= ` 1 )
35 8 recnd 
 |-  ( ph -> A e. CC )
36 eqid 
 |-  ( n e. NN |-> ( A / ( 2 ^ n ) ) ) = ( n e. NN |-> ( A / ( 2 ^ n ) ) )
37 36 geo2lim 
 |-  ( A e. CC -> seq 1 ( + , ( n e. NN |-> ( A / ( 2 ^ n ) ) ) ) ~~> A )
38 35 37 syl 
 |-  ( ph -> seq 1 ( + , ( n e. NN |-> ( A / ( 2 ^ n ) ) ) ) ~~> A )
39 2 32 33 34 38 sge0isummpt 
 |-  ( ph -> ( sum^ ` ( n e. NN |-> ( A / ( 2 ^ n ) ) ) ) = A )