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 ∈ 𝒫 ℕ ⟼ n ∈ ℕ ⟼ if n ∈ x 1 3 n 0
Assertion rpnnen2lem2 ⊢ A ⊆ ℕ → F ⁡ A : ℕ ⟶ ℝ

Proof

Step Hyp Ref Expression
1 rpnnen2.1 ⊢ F = x ∈ 𝒫 ℕ ⟼ n ∈ ℕ ⟼ if n ∈ x 1 3 n 0
2 nnex ⊢ ℕ ∈ V
3 2 elpw2 ⊢ A ∈ 𝒫 ℕ ↔ A ⊆ ℕ
4 eleq2 ⊢ x = A → n ∈ x ↔ n ∈ A
5 4 ifbid ⊢ x = A → if n ∈ x 1 3 n 0 = if n ∈ A 1 3 n 0
6 5 mpteq2dv ⊢ x = A → n ∈ ℕ ⟼ if n ∈ x 1 3 n 0 = n ∈ ℕ ⟼ if n ∈ A 1 3 n 0
7 2 mptex ⊢ n ∈ ℕ ⟼ if n ∈ A 1 3 n 0 ∈ V
8 6 1 7 fvmpt ⊢ A ∈ 𝒫 ℕ → F ⁡ A = n ∈ ℕ ⟼ if n ∈ A 1 3 n 0
9 3 8 sylbir ⊢ A ⊆ ℕ → F ⁡ A = n ∈ ℕ ⟼ if n ∈ A 1 3 n 0
10 1re ⊢ 1 ∈ ℝ
11 3nn ⊢ 3 ∈ ℕ
12 nndivre ⊢ 1 ∈ ℝ ∧ 3 ∈ ℕ → 1 3 ∈ ℝ
13 10 11 12 mp2an ⊢ 1 3 ∈ ℝ
14 nnnn0 ⊢ n ∈ ℕ → n ∈ ℕ 0
15 reexpcl ⊢ 1 3 ∈ ℝ ∧ n ∈ ℕ 0 → 1 3 n ∈ ℝ
16 13 14 15 sylancr ⊢ n ∈ ℕ → 1 3 n ∈ ℝ
17 0re ⊢ 0 ∈ ℝ
18 ifcl ⊢ 1 3 n ∈ ℝ ∧ 0 ∈ ℝ → if n ∈ A 1 3 n 0 ∈ ℝ
19 16 17 18 sylancl ⊢ n ∈ ℕ → if n ∈ A 1 3 n 0 ∈ ℝ
20 19 adantl ⊢ A ⊆ ℕ ∧ n ∈ ℕ → if n ∈ A 1 3 n 0 ∈ ℝ
21 9 20 fmpt3d ⊢ A ⊆ ℕ → F ⁡ A : ℕ ⟶ ℝ