This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 Λ = ( 𝑥 ∈ ℕ ↦ ⦋ { 𝑝 ∈ ℙ ∣ 𝑝 ∥ 𝑥 } / 𝑠 ⦌ 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 ) )