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 logsV
2 c0ex 0V
3 1 2 ifex ifs=1logs0V
4 3 csbex p|px/sifs=1logs0V
5 4 a1i xp|px/sifs=1logs0V
6 df-vma Λ=xp|px/sifs=1logs0
7 6 a1i Λ=xp|px/sifs=1logs0
8 vmacl nΛn
9 8 adantl nΛn
10 5 7 9 fmpt2d Λ:
11 10 mptru Λ: