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 )