Metamath Proof Explorer

Theorem aaliou3lem4

Description: Lemma for aaliou3 . (Contributed by Stefan O'Rear, 16-Nov-2014)

Ref Expression
Hypotheses aaliou3lem.c 
|- F = ( a e. NN |-> ( 2 ^ -u ( ! ` a ) ) )
aaliou3lem.d 
|- L = sum_ b e. NN ( F ` b )
aaliou3lem.e 
|- H = ( c e. NN |-> sum_ b e. ( 1 ... c ) ( F ` b ) )
Assertion aaliou3lem4 
|- L e. RR

Proof

Step Hyp Ref Expression
1 aaliou3lem.c 
 |-  F = ( a e. NN |-> ( 2 ^ -u ( ! ` a ) ) )
2 aaliou3lem.d 
 |-  L = sum_ b e. NN ( F ` b )
3 aaliou3lem.e 
 |-  H = ( c e. NN |-> sum_ b e. ( 1 ... c ) ( F ` b ) )
4 nnuz 
 |-  NN = ( ZZ>= ` 1 )
5 4 sumeq1i 
 |-  sum_ b e. NN ( F ` b ) = sum_ b e. ( ZZ>= ` 1 ) ( F ` b )
6 2 5 eqtri 
 |-  L = sum_ b e. ( ZZ>= ` 1 ) ( F ` b )
7 1nn 
 |-  1 e. NN
8 eqid 
 |-  ( c e. ( ZZ>= ` 1 ) |-> ( ( 2 ^ -u ( ! ` 1 ) ) x. ( ( 1 / 2 ) ^ ( c - 1 ) ) ) ) = ( c e. ( ZZ>= ` 1 ) |-> ( ( 2 ^ -u ( ! ` 1 ) ) x. ( ( 1 / 2 ) ^ ( c - 1 ) ) ) )
9 8 1 aaliou3lem3 
 |-  ( 1 e. NN -> ( seq 1 ( + , F ) e. dom ~~> /\ sum_ b e. ( ZZ>= ` 1 ) ( F ` b ) e. RR+ /\ sum_ b e. ( ZZ>= ` 1 ) ( F ` b ) <_ ( 2 x. ( 2 ^ -u ( ! ` 1 ) ) ) ) )
10 9 simp2d 
 |-  ( 1 e. NN -> sum_ b e. ( ZZ>= ` 1 ) ( F ` b ) e. RR+ )
11 rpre 
 |-  ( sum_ b e. ( ZZ>= ` 1 ) ( F ` b ) e. RR+ -> sum_ b e. ( ZZ>= ` 1 ) ( F ` b ) e. RR )
12 7 10 11 mp2b 
 |-  sum_ b e. ( ZZ>= ` 1 ) ( F ` b ) e. RR
13 6 12 eqeltri 
 |-  L e. RR