Metamath Proof Explorer

Theorem rpnnen2lem3

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

Ref Expression
Hypothesis rpnnen2.1 
|- F = ( x e. ~P NN |-> ( n e. NN |-> if ( n e. x , ( ( 1 / 3 ) ^ n ) , 0 ) ) )
Assertion rpnnen2lem3 
|- seq 1 ( + , ( F ` NN ) ) ~~> ( 1 / 2 )

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 1re 
 |-  1 e. RR
3 3nn 
 |-  3 e. NN
4 nndivre 
 |-  ( ( 1 e. RR /\ 3 e. NN ) -> ( 1 / 3 ) e. RR )
5 2 3 4 mp2an 
 |-  ( 1 / 3 ) e. RR
6 5 recni 
 |-  ( 1 / 3 ) e. CC
7 6 a1i 
 |-  ( T. -> ( 1 / 3 ) e. CC )
8 0re 
 |-  0 e. RR
9 3re 
 |-  3 e. RR
10 3pos 
 |-  0 < 3
11 9 10 recgt0ii 
 |-  0 < ( 1 / 3 )
12 8 5 11 ltleii 
 |-  0 <_ ( 1 / 3 )
13 absid 
 |-  ( ( ( 1 / 3 ) e. RR /\ 0 <_ ( 1 / 3 ) ) -> ( abs ` ( 1 / 3 ) ) = ( 1 / 3 ) )
14 5 12 13 mp2an 
 |-  ( abs ` ( 1 / 3 ) ) = ( 1 / 3 )
15 1lt3 
 |-  1 < 3
16 recgt1 
 |-  ( ( 3 e. RR /\ 0 < 3 ) -> ( 1 < 3 <-> ( 1 / 3 ) < 1 ) )
17 9 10 16 mp2an 
 |-  ( 1 < 3 <-> ( 1 / 3 ) < 1 )
18 15 17 mpbi 
 |-  ( 1 / 3 ) < 1
19 14 18 eqbrtri 
 |-  ( abs ` ( 1 / 3 ) ) < 1
20 19 a1i 
 |-  ( T. -> ( abs ` ( 1 / 3 ) ) < 1 )
21 1nn0 
 |-  1 e. NN0
22 21 a1i 
 |-  ( T. -> 1 e. NN0 )
23 ssid 
 |-  NN C_ NN
24 simpr 
 |-  ( ( T. /\ k e. ( ZZ>= ` 1 ) ) -> k e. ( ZZ>= ` 1 ) )
25 nnuz 
 |-  NN = ( ZZ>= ` 1 )
26 24 25 eleqtrrdi 
 |-  ( ( T. /\ k e. ( ZZ>= ` 1 ) ) -> k e. NN )
27 1 rpnnen2lem1 
 |-  ( ( NN C_ NN /\ k e. NN ) -> ( ( F ` NN ) ` k ) = if ( k e. NN , ( ( 1 / 3 ) ^ k ) , 0 ) )
28 23 26 27 sylancr 
 |-  ( ( T. /\ k e. ( ZZ>= ` 1 ) ) -> ( ( F ` NN ) ` k ) = if ( k e. NN , ( ( 1 / 3 ) ^ k ) , 0 ) )
29 26 iftrued 
 |-  ( ( T. /\ k e. ( ZZ>= ` 1 ) ) -> if ( k e. NN , ( ( 1 / 3 ) ^ k ) , 0 ) = ( ( 1 / 3 ) ^ k ) )
30 28 29 eqtrd 
 |-  ( ( T. /\ k e. ( ZZ>= ` 1 ) ) -> ( ( F ` NN ) ` k ) = ( ( 1 / 3 ) ^ k ) )
31 7 20 22 30 geolim2 
 |-  ( T. -> seq 1 ( + , ( F ` NN ) ) ~~> ( ( ( 1 / 3 ) ^ 1 ) / ( 1 - ( 1 / 3 ) ) ) )
32 31 mptru 
 |-  seq 1 ( + , ( F ` NN ) ) ~~> ( ( ( 1 / 3 ) ^ 1 ) / ( 1 - ( 1 / 3 ) ) )
33 exp1 
 |-  ( ( 1 / 3 ) e. CC -> ( ( 1 / 3 ) ^ 1 ) = ( 1 / 3 ) )
34 6 33 ax-mp 
 |-  ( ( 1 / 3 ) ^ 1 ) = ( 1 / 3 )
35 3cn 
 |-  3 e. CC
36 ax-1cn 
 |-  1 e. CC
37 3ne0 
 |-  3 =/= 0
38 35 37 pm3.2i 
 |-  ( 3 e. CC /\ 3 =/= 0 )
39 divsubdir 
 |-  ( ( 3 e. CC /\ 1 e. CC /\ ( 3 e. CC /\ 3 =/= 0 ) ) -> ( ( 3 - 1 ) / 3 ) = ( ( 3 / 3 ) - ( 1 / 3 ) ) )
40 35 36 38 39 mp3an 
 |-  ( ( 3 - 1 ) / 3 ) = ( ( 3 / 3 ) - ( 1 / 3 ) )
41 3m1e2 
 |-  ( 3 - 1 ) = 2
42 41 oveq1i 
 |-  ( ( 3 - 1 ) / 3 ) = ( 2 / 3 )
43 35 37 dividi 
 |-  ( 3 / 3 ) = 1
44 43 oveq1i 
 |-  ( ( 3 / 3 ) - ( 1 / 3 ) ) = ( 1 - ( 1 / 3 ) )
45 40 42 44 3eqtr3ri 
 |-  ( 1 - ( 1 / 3 ) ) = ( 2 / 3 )
46 34 45 oveq12i 
 |-  ( ( ( 1 / 3 ) ^ 1 ) / ( 1 - ( 1 / 3 ) ) ) = ( ( 1 / 3 ) / ( 2 / 3 ) )
47 2cnne0 
 |-  ( 2 e. CC /\ 2 =/= 0 )
48 divcan7 
 |-  ( ( 1 e. CC /\ ( 2 e. CC /\ 2 =/= 0 ) /\ ( 3 e. CC /\ 3 =/= 0 ) ) -> ( ( 1 / 3 ) / ( 2 / 3 ) ) = ( 1 / 2 ) )
49 36 47 38 48 mp3an 
 |-  ( ( 1 / 3 ) / ( 2 / 3 ) ) = ( 1 / 2 )
50 46 49 eqtri 
 |-  ( ( ( 1 / 3 ) ^ 1 ) / ( 1 - ( 1 / 3 ) ) ) = ( 1 / 2 )
51 32 50 breqtri 
 |-  seq 1 ( + , ( F ` NN ) ) ~~> ( 1 / 2 )