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	⊢ Λ : ℕ ⟶ ℝ