Metamath Proof Explorer

Theorem rpnnen2lem8

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 rpnnen2lem8 
|- ( ( A C_ NN /\ M e. NN ) -> sum_ k e. NN ( ( F ` A ) ` k ) = ( sum_ k e. ( 1 ... ( M - 1 ) ) ( ( F ` A ) ` k ) + sum_ k e. ( ZZ>= ` M ) ( ( F ` A ) ` k ) ) )

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 nnuz 
 |-  NN = ( ZZ>= ` 1 )
3 eqid 
 |-  ( ZZ>= ` M ) = ( ZZ>= ` M )
4 simpr 
 |-  ( ( A C_ NN /\ M e. NN ) -> M e. NN )
5 eqidd 
 |-  ( ( ( A C_ NN /\ M e. NN ) /\ k e. NN ) -> ( ( F ` A ) ` k ) = ( ( F ` A ) ` k ) )
6 1 rpnnen2lem2 
 |-  ( A C_ NN -> ( F ` A ) : NN --> RR )
7 6 adantr 
 |-  ( ( A C_ NN /\ M e. NN ) -> ( F ` A ) : NN --> RR )
8 7 ffvelrnda 
 |-  ( ( ( A C_ NN /\ M e. NN ) /\ k e. NN ) -> ( ( F ` A ) ` k ) e. RR )
9 8 recnd 
 |-  ( ( ( A C_ NN /\ M e. NN ) /\ k e. NN ) -> ( ( F ` A ) ` k ) e. CC )
10 1nn 
 |-  1 e. NN
11 1 rpnnen2lem5 
 |-  ( ( A C_ NN /\ 1 e. NN ) -> seq 1 ( + , ( F ` A ) ) e. dom ~~> )
12 10 11 mpan2 
 |-  ( A C_ NN -> seq 1 ( + , ( F ` A ) ) e. dom ~~> )
13 12 adantr 
 |-  ( ( A C_ NN /\ M e. NN ) -> seq 1 ( + , ( F ` A ) ) e. dom ~~> )
14 2 3 4 5 9 13 isumsplit 
 |-  ( ( A C_ NN /\ M e. NN ) -> sum_ k e. NN ( ( F ` A ) ` k ) = ( sum_ k e. ( 1 ... ( M - 1 ) ) ( ( F ` A ) ` k ) + sum_ k e. ( ZZ>= ` M ) ( ( F ` A ) ` k ) ) )