Metamath Proof Explorer

Theorem rpnnen2lem5

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 rpnnen2lem5 
|- ( ( A C_ NN /\ M e. NN ) -> seq M ( + , ( F ` A ) ) e. dom ~~> )

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 1nn 
 |-  1 e. NN
4 3 a1i 
 |-  ( A C_ NN -> 1 e. NN )
5 ssid 
 |-  NN C_ NN
6 1 rpnnen2lem2 
 |-  ( NN C_ NN -> ( F ` NN ) : NN --> RR )
7 5 6 mp1i 
 |-  ( A C_ NN -> ( F ` NN ) : NN --> RR )
8 7 ffvelrnda 
 |-  ( ( A C_ NN /\ k e. NN ) -> ( ( F ` NN ) ` k ) e. RR )
9 1 rpnnen2lem2 
 |-  ( A C_ NN -> ( F ` A ) : NN --> RR )
10 9 ffvelrnda 
 |-  ( ( A C_ NN /\ k e. NN ) -> ( ( F ` A ) ` k ) e. RR )
11 1 rpnnen2lem3 
 |-  seq 1 ( + , ( F ` NN ) ) ~~> ( 1 / 2 )
12 seqex 
 |-  seq 1 ( + , ( F ` NN ) ) e. _V
13 ovex 
 |-  ( 1 / 2 ) e. _V
14 12 13 breldm 
 |-  ( seq 1 ( + , ( F ` NN ) ) ~~> ( 1 / 2 ) -> seq 1 ( + , ( F ` NN ) ) e. dom ~~> )
15 11 14 mp1i 
 |-  ( A C_ NN -> seq 1 ( + , ( F ` NN ) ) e. dom ~~> )
16 elnnuz 
 |-  ( k e. NN <-> k e. ( ZZ>= ` 1 ) )
17 1 rpnnen2lem4 
 |-  ( ( A C_ NN /\ NN C_ NN /\ k e. NN ) -> ( 0 <_ ( ( F ` A ) ` k ) /\ ( ( F ` A ) ` k ) <_ ( ( F ` NN ) ` k ) ) )
18 5 17 mp3an2 
 |-  ( ( A C_ NN /\ k e. NN ) -> ( 0 <_ ( ( F ` A ) ` k ) /\ ( ( F ` A ) ` k ) <_ ( ( F ` NN ) ` k ) ) )
19 16 18 sylan2br 
 |-  ( ( A C_ NN /\ k e. ( ZZ>= ` 1 ) ) -> ( 0 <_ ( ( F ` A ) ` k ) /\ ( ( F ` A ) ` k ) <_ ( ( F ` NN ) ` k ) ) )
20 19 simpld 
 |-  ( ( A C_ NN /\ k e. ( ZZ>= ` 1 ) ) -> 0 <_ ( ( F ` A ) ` k ) )
21 19 simprd 
 |-  ( ( A C_ NN /\ k e. ( ZZ>= ` 1 ) ) -> ( ( F ` A ) ` k ) <_ ( ( F ` NN ) ` k ) )
22 2 4 8 10 15 20 21 cvgcmp 
 |-  ( A C_ NN -> seq 1 ( + , ( F ` A ) ) e. dom ~~> )
23 22 adantr 
 |-  ( ( A C_ NN /\ M e. NN ) -> seq 1 ( + , ( F ` A ) ) e. dom ~~> )
24 simpr 
 |-  ( ( A C_ NN /\ M e. NN ) -> M e. NN )
25 10 adantlr 
 |-  ( ( ( A C_ NN /\ M e. NN ) /\ k e. NN ) -> ( ( F ` A ) ` k ) e. RR )
26 25 recnd 
 |-  ( ( ( A C_ NN /\ M e. NN ) /\ k e. NN ) -> ( ( F ` A ) ` k ) e. CC )
27 2 24 26 iserex 
 |-  ( ( A C_ NN /\ M e. NN ) -> ( seq 1 ( + , ( F ` A ) ) e. dom ~~> <-> seq M ( + , ( F ` A ) ) e. dom ~~> ) )
28 23 27 mpbid 
 |-  ( ( A C_ NN /\ M e. NN ) -> seq M ( + , ( F ` A ) ) e. dom ~~> )