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	⊢ Λ = ( 𝑥 ∈ ℕ ↦ ⦋ { 𝑝 ∈ ℙ ∣ 𝑝 ∥ 𝑥 } / 𝑠 ⦌ if ( ( ♯ ‘ 𝑠 ) = 1 , ( log ‘ ∪ 𝑠 ) , 0 ) )

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cvma	⊢ Λ
1		vx	⊢ 𝑥
2		cn	⊢ ℕ
3		vp	⊢ 𝑝
4		cprime	⊢ ℙ
5	3	cv	⊢ 𝑝
6		cdvds	⊢ ∥
7	1	cv	⊢ 𝑥
8	5 7 6	wbr	⊢ 𝑝 ∥ 𝑥
9	8 3 4	crab	⊢ { 𝑝 ∈ ℙ ∣ 𝑝 ∥ 𝑥 }
10		vs	⊢ 𝑠
11		chash	⊢ ♯
12	10	cv	⊢ 𝑠
13	12 11	cfv	⊢ ( ♯ ‘ 𝑠 )
14		c1	⊢ 1
15	13 14	wceq	⊢ ( ♯ ‘ 𝑠 ) = 1
16		clog	⊢ log
17	12	cuni	⊢ ∪ 𝑠
18	17 16	cfv	⊢ ( log ‘ ∪ 𝑠 )
19		cc0	⊢ 0
20	15 18 19	cif	⊢ if ( ( ♯ ‘ 𝑠 ) = 1 , ( log ‘ ∪ 𝑠 ) , 0 )
21	10 9 20	csb	⊢ ⦋ { 𝑝 ∈ ℙ ∣ 𝑝 ∥ 𝑥 } / 𝑠 ⦌ if ( ( ♯ ‘ 𝑠 ) = 1 , ( log ‘ ∪ 𝑠 ) , 0 )
22	1 2 21	cmpt	⊢ ( 𝑥 ∈ ℕ ↦ ⦋ { 𝑝 ∈ ℙ ∣ 𝑝 ∥ 𝑥 } / 𝑠 ⦌ if ( ( ♯ ‘ 𝑠 ) = 1 , ( log ‘ ∪ 𝑠 ) , 0 ) )
23	0 22	wceq	⊢ Λ = ( 𝑥 ∈ ℕ ↦ ⦋ { 𝑝 ∈ ℙ ∣ 𝑝 ∥ 𝑥 } / 𝑠 ⦌ if ( ( ♯ ‘ 𝑠 ) = 1 , ( log ‘ ∪ 𝑠 ) , 0 ) )