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	⊢ 𝐹 = ( 𝑥 ∈ 𝒫 ℕ ↦ ( 𝑛 ∈ ℕ ↦ if ( 𝑛 ∈ 𝑥 , ( ( 1 / 3 ) ↑ 𝑛 ) , 0 ) ) )
Assertion	rpnnen2lem2	⊢ ( 𝐴 ⊆ ℕ → ( 𝐹 ‘ 𝐴 ) : ℕ ⟶ ℝ )

Proof

Step	Hyp	Ref	Expression
1		rpnnen2.1	⊢ 𝐹 = ( 𝑥 ∈ 𝒫 ℕ ↦ ( 𝑛 ∈ ℕ ↦ if ( 𝑛 ∈ 𝑥 , ( ( 1 / 3 ) ↑ 𝑛 ) , 0 ) ) )
2		nnex	⊢ ℕ ∈ V
3	2	elpw2	⊢ ( 𝐴 ∈ 𝒫 ℕ ↔ 𝐴 ⊆ ℕ )
4		eleq2	⊢ ( 𝑥 = 𝐴 → ( 𝑛 ∈ 𝑥 ↔ 𝑛 ∈ 𝐴 ) )
5	4	ifbid	⊢ ( 𝑥 = 𝐴 → if ( 𝑛 ∈ 𝑥 , ( ( 1 / 3 ) ↑ 𝑛 ) , 0 ) = if ( 𝑛 ∈ 𝐴 , ( ( 1 / 3 ) ↑ 𝑛 ) , 0 ) )
6	5	mpteq2dv	⊢ ( 𝑥 = 𝐴 → ( 𝑛 ∈ ℕ ↦ if ( 𝑛 ∈ 𝑥 , ( ( 1 / 3 ) ↑ 𝑛 ) , 0 ) ) = ( 𝑛 ∈ ℕ ↦ if ( 𝑛 ∈ 𝐴 , ( ( 1 / 3 ) ↑ 𝑛 ) , 0 ) ) )
7	2	mptex	⊢ ( 𝑛 ∈ ℕ ↦ if ( 𝑛 ∈ 𝐴 , ( ( 1 / 3 ) ↑ 𝑛 ) , 0 ) ) ∈ V
8	6 1 7	fvmpt	⊢ ( 𝐴 ∈ 𝒫 ℕ → ( 𝐹 ‘ 𝐴 ) = ( 𝑛 ∈ ℕ ↦ if ( 𝑛 ∈ 𝐴 , ( ( 1 / 3 ) ↑ 𝑛 ) , 0 ) ) )
9	3 8	sylbir	⊢ ( 𝐴 ⊆ ℕ → ( 𝐹 ‘ 𝐴 ) = ( 𝑛 ∈ ℕ ↦ if ( 𝑛 ∈ 𝐴 , ( ( 1 / 3 ) ↑ 𝑛 ) , 0 ) ) )
10		1re	⊢ 1 ∈ ℝ
11		3nn	⊢ 3 ∈ ℕ
12		nndivre	⊢ ( ( 1 ∈ ℝ ∧ 3 ∈ ℕ ) → ( 1 / 3 ) ∈ ℝ )
13	10 11 12	mp2an	⊢ ( 1 / 3 ) ∈ ℝ
14		nnnn0	⊢ ( 𝑛 ∈ ℕ → 𝑛 ∈ ℕ0 )
15		reexpcl	⊢ ( ( ( 1 / 3 ) ∈ ℝ ∧ 𝑛 ∈ ℕ0 ) → ( ( 1 / 3 ) ↑ 𝑛 ) ∈ ℝ )
16	13 14 15	sylancr	⊢ ( 𝑛 ∈ ℕ → ( ( 1 / 3 ) ↑ 𝑛 ) ∈ ℝ )
17		0re	⊢ 0 ∈ ℝ
18		ifcl	⊢ ( ( ( ( 1 / 3 ) ↑ 𝑛 ) ∈ ℝ ∧ 0 ∈ ℝ ) → if ( 𝑛 ∈ 𝐴 , ( ( 1 / 3 ) ↑ 𝑛 ) , 0 ) ∈ ℝ )
19	16 17 18	sylancl	⊢ ( 𝑛 ∈ ℕ → if ( 𝑛 ∈ 𝐴 , ( ( 1 / 3 ) ↑ 𝑛 ) , 0 ) ∈ ℝ )
20	19	adantl	⊢ ( ( 𝐴 ⊆ ℕ ∧ 𝑛 ∈ ℕ ) → if ( 𝑛 ∈ 𝐴 , ( ( 1 / 3 ) ↑ 𝑛 ) , 0 ) ∈ ℝ )
21	9 20	fmpt3d	⊢ ( 𝐴 ⊆ ℕ → ( 𝐹 ‘ 𝐴 ) : ℕ ⟶ ℝ )