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 ⊢ 𝐹 = ( 𝑥 ∈ 𝒫 ℕ ↦ ( 𝑛 ∈ ℕ ↦ 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 ⊢ ( 𝐴 ⊆ ℕ → ( 𝐹 ‘ 𝐴 ) : ℕ ⟶ ℝ )