This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem rpnnen2lem2

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

Ref Expression
Hypothesis rpnnen2.1 
|- F = ( x e. ~P NN |-> ( n e. NN |-> if ( n e. x , ( ( 1 / 3 ) ^ n ) , 0 ) ) )
Assertion rpnnen2lem2 
|- ( A C_ NN -> ( F ` A ) : NN --> 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 nnex 
 |-  NN e. _V
3 2 elpw2 
 |-  ( A e. ~P NN <-> A C_ NN )
4 eleq2 
 |-  ( x = A -> ( n e. x <-> n e. A ) )
5 4 ifbid 
 |-  ( x = A -> if ( n e. x , ( ( 1 / 3 ) ^ n ) , 0 ) = if ( n e. A , ( ( 1 / 3 ) ^ n ) , 0 ) )
6 5 mpteq2dv 
 |-  ( x = A -> ( n e. NN |-> if ( n e. x , ( ( 1 / 3 ) ^ n ) , 0 ) ) = ( n e. NN |-> if ( n e. A , ( ( 1 / 3 ) ^ n ) , 0 ) ) )
7 2 mptex 
 |-  ( n e. NN |-> if ( n e. A , ( ( 1 / 3 ) ^ n ) , 0 ) ) e. _V
8 6 1 7 fvmpt 
 |-  ( A e. ~P NN -> ( F ` A ) = ( n e. NN |-> if ( n e. A , ( ( 1 / 3 ) ^ n ) , 0 ) ) )
9 3 8 sylbir 
 |-  ( A C_ NN -> ( F ` A ) = ( n e. NN |-> if ( n e. A , ( ( 1 / 3 ) ^ n ) , 0 ) ) )
10 1re 
 |-  1 e. RR
11 3nn 
 |-  3 e. NN
12 nndivre 
 |-  ( ( 1 e. RR /\ 3 e. NN ) -> ( 1 / 3 ) e. RR )
13 10 11 12 mp2an 
 |-  ( 1 / 3 ) e. RR
14 nnnn0 
 |-  ( n e. NN -> n e. NN0 )
15 reexpcl 
 |-  ( ( ( 1 / 3 ) e. RR /\ n e. NN0 ) -> ( ( 1 / 3 ) ^ n ) e. RR )
16 13 14 15 sylancr 
 |-  ( n e. NN -> ( ( 1 / 3 ) ^ n ) e. RR )
17 0re 
 |-  0 e. RR
18 ifcl 
 |-  ( ( ( ( 1 / 3 ) ^ n ) e. RR /\ 0 e. RR ) -> if ( n e. A , ( ( 1 / 3 ) ^ n ) , 0 ) e. RR )
19 16 17 18 sylancl 
 |-  ( n e. NN -> if ( n e. A , ( ( 1 / 3 ) ^ n ) , 0 ) e. RR )
20 19 adantl 
 |-  ( ( A C_ NN /\ n e. NN ) -> if ( n e. A , ( ( 1 / 3 ) ^ n ) , 0 ) e. RR )
21 9 20 fmpt3d 
 |-  ( A C_ NN -> ( F ` A ) : NN --> RR )