# Metamath Proof Explorer

## Definition df-vma

Description: Define the von Mangoldt function, which gives the logarithm of the prime at a prime power, and is zero elsewhere, see definition in ApostolNT p. 32. (Contributed by Mario Carneiro, 7-Apr-2016)

Ref Expression
Assertion df-vma

### Detailed syntax breakdown

Step Hyp Ref Expression
0 cvma ${class}\Lambda$
1 vx ${setvar}{x}$
2 cn ${class}ℕ$
3 vp ${setvar}{p}$
4 cprime ${class}ℙ$
5 3 cv ${setvar}{p}$
6 cdvds ${class}\parallel$
7 1 cv ${setvar}{x}$
8 5 7 6 wbr ${wff}{p}\parallel {x}$
9 8 3 4 crab ${class}\left\{{p}\in ℙ|{p}\parallel {x}\right\}$
10 vs ${setvar}{s}$
11 chash ${class}\left|.\right|$
12 10 cv ${setvar}{s}$
13 12 11 cfv ${class}\left|{s}\right|$
14 c1 ${class}1$
15 13 14 wceq ${wff}\left|{s}\right|=1$
16 clog ${class}log$
17 12 cuni ${class}\bigcup {s}$
18 17 16 cfv ${class}\mathrm{log}\bigcup {s}$
19 cc0 ${class}0$
20 15 18 19 cif ${class}if\left(\left|{s}\right|=1,\mathrm{log}\bigcup {s},0\right)$
21 10 9 20 csb
22 1 2 21 cmpt
23 0 22 wceq