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	$$⊢\Lambda =\left(x\in \mathbb{N}⟼⦋\left\{p\in \mathbb{P}|p\parallel x\right\}/s⦌if\left(\left|s\right|=1,\log \bigcup s,0\right)\right)$$

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cvma	$$class\Lambda$$
1		vx	$$setvarx$$
2		cn	$$class\mathbb{N}$$
3		vp	$$setvarp$$
4		cprime	$$class\mathbb{P}$$
5	3	cv	$$setvarp$$
6		cdvds	$$class\parallel$$
7	1	cv	$$setvarx$$
8	5 7 6	wbr	$$wffp\parallel x$$
9	8 3 4	crab	$$class\left\{p\in \mathbb{P}|p\parallel x\right\}$$
10		vs	$$setvars$$
11		chash	$$class\left|.\right|$$
12	10	cv	$$setvars$$
13	12 11	cfv	$$class\left|s\right|$$
14		c1	$$class1$$
15	13 14	wceq	$$wff\left|s\right|=1$$
16		clog	$$classlog$$
17	12	cuni	$$class\bigcup s$$
18	17 16	cfv	$$class\log \bigcup s$$
19		cc0	$$class0$$
20	15 18 19	cif	$$classif\left(\left|s\right|=1,\log \bigcup s,0\right)$$
21	10 9 20	csb	$$class⦋\left\{p\in \mathbb{P}|p\parallel x\right\}/s⦌if\left(\left|s\right|=1,\log \bigcup s,0\right)$$
22	1 2 21	cmpt	$$class\left(x\in \mathbb{N}⟼⦋\left\{p\in \mathbb{P}|p\parallel x\right\}/s⦌if\left(\left|s\right|=1,\log \bigcup s,0\right)\right)$$
23	0 22	wceq	$$wff\Lambda =\left(x\in \mathbb{N}⟼⦋\left\{p\in \mathbb{P}|p\parallel x\right\}/s⦌if\left(\left|s\right|=1,\log \bigcup s,0\right)\right)$$