Metamath Proof Explorer

Theorem rpnnen2lem9

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 rpnnen2lem9 
|- ( M e. NN -> sum_ k e. ( ZZ>= ` M ) ( ( F ` ( NN \ { M } ) ) ` k ) = ( 0 + ( ( ( 1 / 3 ) ^ ( M + 1 ) ) / ( 1 - ( 1 / 3 ) ) ) ) )

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 eqidd 
 |-  ( ( M e. NN /\ k e. ( ZZ>= ` M ) ) -> ( ( F ` ( NN \ { M } ) ) ` k ) = ( ( F ` ( NN \ { M } ) ) ` k ) )
5 eluznn 
 |-  ( ( M e. NN /\ k e. ( ZZ>= ` M ) ) -> k e. NN )
6 difss 
 |-  ( NN \ { M } ) C_ NN
7 1 rpnnen2lem2 
 |-  ( ( NN \ { M } ) C_ NN -> ( F ` ( NN \ { M } ) ) : NN --> RR )
8 6 7 ax-mp 
 |-  ( F ` ( NN \ { M } ) ) : NN --> RR
9 8 ffvelcdmi 
 |-  ( k e. NN -> ( ( F ` ( NN \ { M } ) ) ` k ) e. RR )
10 9 recnd 
 |-  ( k e. NN -> ( ( F ` ( NN \ { M } ) ) ` k ) e. CC )
11 5 10 syl 
 |-  ( ( M e. NN /\ k e. ( ZZ>= ` M ) ) -> ( ( F ` ( NN \ { M } ) ) ` k ) e. CC )
12 1 rpnnen2lem5 
 |-  ( ( ( NN \ { M } ) C_ NN /\ M e. NN ) -> seq M ( + , ( F ` ( NN \ { M } ) ) ) e. dom ~~> )
13 6 12 mpan 
 |-  ( M e. NN -> seq M ( + , ( F ` ( NN \ { M } ) ) ) e. dom ~~> )
14 2 3 4 11 13 isum1p 
 |-  ( M e. NN -> sum_ k e. ( ZZ>= ` M ) ( ( F ` ( NN \ { M } ) ) ` k ) = ( ( ( F ` ( NN \ { M } ) ) ` M ) + sum_ k e. ( ZZ>= ` ( M + 1 ) ) ( ( F ` ( NN \ { M } ) ) ` k ) ) )
15 1 rpnnen2lem1 
 |-  ( ( ( NN \ { M } ) C_ NN /\ M e. NN ) -> ( ( F ` ( NN \ { M } ) ) ` M ) = if ( M e. ( NN \ { M } ) , ( ( 1 / 3 ) ^ M ) , 0 ) )
16 6 15 mpan 
 |-  ( M e. NN -> ( ( F ` ( NN \ { M } ) ) ` M ) = if ( M e. ( NN \ { M } ) , ( ( 1 / 3 ) ^ M ) , 0 ) )
17 neldifsnd 
 |-  ( M e. NN -> -. M e. ( NN \ { M } ) )
18 17 iffalsed 
 |-  ( M e. NN -> if ( M e. ( NN \ { M } ) , ( ( 1 / 3 ) ^ M ) , 0 ) = 0 )
19 16 18 eqtrd 
 |-  ( M e. NN -> ( ( F ` ( NN \ { M } ) ) ` M ) = 0 )
20 eqid 
 |-  ( ZZ>= ` ( M + 1 ) ) = ( ZZ>= ` ( M + 1 ) )
21 peano2nn 
 |-  ( M e. NN -> ( M + 1 ) e. NN )
22 21 nnzd 
 |-  ( M e. NN -> ( M + 1 ) e. ZZ )
23 eqidd 
 |-  ( ( M e. NN /\ k e. ( ZZ>= ` ( M + 1 ) ) ) -> ( ( F ` ( NN \ { M } ) ) ` k ) = ( ( F ` ( NN \ { M } ) ) ` k ) )
24 eluznn 
 |-  ( ( ( M + 1 ) e. NN /\ k e. ( ZZ>= ` ( M + 1 ) ) ) -> k e. NN )
25 21 24 sylan 
 |-  ( ( M e. NN /\ k e. ( ZZ>= ` ( M + 1 ) ) ) -> k e. NN )
26 25 10 syl 
 |-  ( ( M e. NN /\ k e. ( ZZ>= ` ( M + 1 ) ) ) -> ( ( F ` ( NN \ { M } ) ) ` k ) e. CC )
27 1re 
 |-  1 e. RR
28 3nn 
 |-  3 e. NN
29 nndivre 
 |-  ( ( 1 e. RR /\ 3 e. NN ) -> ( 1 / 3 ) e. RR )
30 27 28 29 mp2an 
 |-  ( 1 / 3 ) e. RR
31 30 recni 
 |-  ( 1 / 3 ) e. CC
32 31 a1i 
 |-  ( M e. NN -> ( 1 / 3 ) e. CC )
33 0re 
 |-  0 e. RR
34 3re 
 |-  3 e. RR
35 3pos 
 |-  0 < 3
36 34 35 recgt0ii 
 |-  0 < ( 1 / 3 )
37 33 30 36 ltleii 
 |-  0 <_ ( 1 / 3 )
38 absid 
 |-  ( ( ( 1 / 3 ) e. RR /\ 0 <_ ( 1 / 3 ) ) -> ( abs ` ( 1 / 3 ) ) = ( 1 / 3 ) )
39 30 37 38 mp2an 
 |-  ( abs ` ( 1 / 3 ) ) = ( 1 / 3 )
40 1lt3 
 |-  1 < 3
41 recgt1 
 |-  ( ( 3 e. RR /\ 0 < 3 ) -> ( 1 < 3 <-> ( 1 / 3 ) < 1 ) )
42 34 35 41 mp2an 
 |-  ( 1 < 3 <-> ( 1 / 3 ) < 1 )
43 40 42 mpbi 
 |-  ( 1 / 3 ) < 1
44 39 43 eqbrtri 
 |-  ( abs ` ( 1 / 3 ) ) < 1
45 44 a1i 
 |-  ( M e. NN -> ( abs ` ( 1 / 3 ) ) < 1 )
46 21 nnnn0d 
 |-  ( M e. NN -> ( M + 1 ) e. NN0 )
47 1 rpnnen2lem1 
 |-  ( ( ( NN \ { M } ) C_ NN /\ k e. NN ) -> ( ( F ` ( NN \ { M } ) ) ` k ) = if ( k e. ( NN \ { M } ) , ( ( 1 / 3 ) ^ k ) , 0 ) )
48 6 47 mpan 
 |-  ( k e. NN -> ( ( F ` ( NN \ { M } ) ) ` k ) = if ( k e. ( NN \ { M } ) , ( ( 1 / 3 ) ^ k ) , 0 ) )
49 25 48 syl 
 |-  ( ( M e. NN /\ k e. ( ZZ>= ` ( M + 1 ) ) ) -> ( ( F ` ( NN \ { M } ) ) ` k ) = if ( k e. ( NN \ { M } ) , ( ( 1 / 3 ) ^ k ) , 0 ) )
50 nnre 
 |-  ( M e. NN -> M e. RR )
51 50 adantr 
 |-  ( ( M e. NN /\ k e. ( ZZ>= ` ( M + 1 ) ) ) -> M e. RR )
52 eluzle 
 |-  ( k e. ( ZZ>= ` ( M + 1 ) ) -> ( M + 1 ) <_ k )
53 52 adantl 
 |-  ( ( M e. NN /\ k e. ( ZZ>= ` ( M + 1 ) ) ) -> ( M + 1 ) <_ k )
54 nnltp1le 
 |-  ( ( M e. NN /\ k e. NN ) -> ( M < k <-> ( M + 1 ) <_ k ) )
55 25 54 syldan 
 |-  ( ( M e. NN /\ k e. ( ZZ>= ` ( M + 1 ) ) ) -> ( M < k <-> ( M + 1 ) <_ k ) )
56 53 55 mpbird 
 |-  ( ( M e. NN /\ k e. ( ZZ>= ` ( M + 1 ) ) ) -> M < k )
57 51 56 gtned 
 |-  ( ( M e. NN /\ k e. ( ZZ>= ` ( M + 1 ) ) ) -> k =/= M )
58 eldifsn 
 |-  ( k e. ( NN \ { M } ) <-> ( k e. NN /\ k =/= M ) )
59 25 57 58 sylanbrc 
 |-  ( ( M e. NN /\ k e. ( ZZ>= ` ( M + 1 ) ) ) -> k e. ( NN \ { M } ) )
60 59 iftrued 
 |-  ( ( M e. NN /\ k e. ( ZZ>= ` ( M + 1 ) ) ) -> if ( k e. ( NN \ { M } ) , ( ( 1 / 3 ) ^ k ) , 0 ) = ( ( 1 / 3 ) ^ k ) )
61 49 60 eqtrd 
 |-  ( ( M e. NN /\ k e. ( ZZ>= ` ( M + 1 ) ) ) -> ( ( F ` ( NN \ { M } ) ) ` k ) = ( ( 1 / 3 ) ^ k ) )
62 32 45 46 61 geolim2 
 |-  ( M e. NN -> seq ( M + 1 ) ( + , ( F ` ( NN \ { M } ) ) ) ~~> ( ( ( 1 / 3 ) ^ ( M + 1 ) ) / ( 1 - ( 1 / 3 ) ) ) )
63 20 22 23 26 62 isumclim 
 |-  ( M e. NN -> sum_ k e. ( ZZ>= ` ( M + 1 ) ) ( ( F ` ( NN \ { M } ) ) ` k ) = ( ( ( 1 / 3 ) ^ ( M + 1 ) ) / ( 1 - ( 1 / 3 ) ) ) )
64 19 63 oveq12d 
 |-  ( M e. NN -> ( ( ( F ` ( NN \ { M } ) ) ` M ) + sum_ k e. ( ZZ>= ` ( M + 1 ) ) ( ( F ` ( NN \ { M } ) ) ` k ) ) = ( 0 + ( ( ( 1 / 3 ) ^ ( M + 1 ) ) / ( 1 - ( 1 / 3 ) ) ) ) )
65 14 64 eqtrd 
 |-  ( M e. NN -> sum_ k e. ( ZZ>= ` M ) ( ( F ` ( NN \ { M } ) ) ` k ) = ( 0 + ( ( ( 1 / 3 ) ^ ( M + 1 ) ) / ( 1 - ( 1 / 3 ) ) ) ) )