Metamath Proof Explorer

Theorem rpnnen2lem6

Description: Lemma for rpnnen2 . (Contributed by Mario Carneiro, 13-May-2013) (Revised by Mario Carneiro, 30-Apr-2014)

Ref Expression
Hypothesis rpnnen2.1 
|- F = ( x e. ~P NN |-> ( n e. NN |-> if ( n e. x , ( ( 1 / 3 ) ^ n ) , 0 ) ) )
Assertion rpnnen2lem6 
|- ( ( A C_ NN /\ M e. NN ) -> sum_ k e. ( ZZ>= ` M ) ( ( F ` A ) ` k ) e. RR )

Proof

Step Hyp Ref Expression
1 rpnnen2.1 
 |-  F = ( x e. ~P NN |-> ( n e. NN |-> if ( n e. x , ( ( 1 / 3 ) ^ n ) , 0 ) ) )
2 eqid 
 |-  ( ZZ>= ` M ) = ( ZZ>= ` M )
3 nnz 
 |-  ( M e. NN -> M e. ZZ )
4 3 adantl 
 |-  ( ( A C_ NN /\ M e. NN ) -> M e. ZZ )
5 eqidd 
 |-  ( ( ( A C_ NN /\ M e. NN ) /\ k e. ( ZZ>= ` M ) ) -> ( ( F ` A ) ` k ) = ( ( F ` A ) ` k ) )
6 1 rpnnen2lem2 
 |-  ( A C_ NN -> ( F ` A ) : NN --> RR )
7 6 ad2antrr 
 |-  ( ( ( A C_ NN /\ M e. NN ) /\ k e. ( ZZ>= ` M ) ) -> ( F ` A ) : NN --> RR )
8 eluznn 
 |-  ( ( M e. NN /\ k e. ( ZZ>= ` M ) ) -> k e. NN )
9 8 adantll 
 |-  ( ( ( A C_ NN /\ M e. NN ) /\ k e. ( ZZ>= ` M ) ) -> k e. NN )
10 7 9 ffvelrnd 
 |-  ( ( ( A C_ NN /\ M e. NN ) /\ k e. ( ZZ>= ` M ) ) -> ( ( F ` A ) ` k ) e. RR )
11 1 rpnnen2lem5 
 |-  ( ( A C_ NN /\ M e. NN ) -> seq M ( + , ( F ` A ) ) e. dom ~~> )
12 2 4 5 10 11 isumrecl 
 |-  ( ( A C_ NN /\ M e. NN ) -> sum_ k e. ( ZZ>= ` M ) ( ( F ` A ) ` k ) e. RR )