Description: Functionality of the von Mangoldt function. (Contributed by Mario Carneiro, 7-Apr-2016)
Ref | Expression | ||
---|---|---|---|
Assertion | vmaf | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | fvex | |
|
2 | c0ex | |
|
3 | 1 2 | ifex | |
4 | 3 | csbex | |
5 | 4 | a1i | |
6 | df-vma | |
|
7 | 6 | a1i | |
8 | vmacl | |
|
9 | 8 | adantl | |
10 | 5 7 9 | fmpt2d | |
11 | 10 | mptru | |