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

Metamath Proof Explorer

Theorem vmaf

Description: Functionality of the von Mangoldt function. (Contributed by Mario Carneiro, 7-Apr-2016)

Ref Expression
Assertion vmaf Λ : ℕ ⟶ ℝ

Proof

Step Hyp Ref Expression
1 fvex ⊢ ( log ‘ ∪ 𝑠 ) ∈ V
2 c0ex ⊢ 0 ∈ V
3 1 2 ifex ⊢ if ( ( ♯ ‘ 𝑠 ) = 1 , ( log ‘ ∪ 𝑠 ) , 0 ) ∈ V
4 3 csbex ⊢ ⦋ { 𝑝 ∈ ℙ ∣ 𝑝 ∥ 𝑥 } / 𝑠 ⦌ if ( ( ♯ ‘ 𝑠 ) = 1 , ( log ‘ ∪ 𝑠 ) , 0 ) ∈ V
5 4 a1i ⊢ ( ( ⊤ ∧ 𝑥 ∈ ℕ ) → ⦋ { 𝑝 ∈ ℙ ∣ 𝑝 ∥ 𝑥 } / 𝑠 ⦌ if ( ( ♯ ‘ 𝑠 ) = 1 , ( log ‘ ∪ 𝑠 ) , 0 ) ∈ V )
6 df-vma ⊢ Λ = ( 𝑥 ∈ ℕ ↦ ⦋ { 𝑝 ∈ ℙ ∣ 𝑝 ∥ 𝑥 } / 𝑠 ⦌ if ( ( ♯ ‘ 𝑠 ) = 1 , ( log ‘ ∪ 𝑠 ) , 0 ) )
7 6 a1i ⊢ ( ⊤ → Λ = ( 𝑥 ∈ ℕ ↦ ⦋ { 𝑝 ∈ ℙ ∣ 𝑝 ∥ 𝑥 } / 𝑠 ⦌ if ( ( ♯ ‘ 𝑠 ) = 1 , ( log ‘ ∪ 𝑠 ) , 0 ) ) )
8 vmacl ⊢ ( 𝑛 ∈ ℕ → ( Λ ‘ 𝑛 ) ∈ ℝ )
9 8 adantl ⊢ ( ( ⊤ ∧ 𝑛 ∈ ℕ ) → ( Λ ‘ 𝑛 ) ∈ ℝ )
10 5 7 9 fmpt2d ⊢ ( ⊤ → Λ : ℕ ⟶ ℝ )
11 10 mptru ⊢ Λ : ℕ ⟶ ℝ