MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  df-vma Structured version   Visualization version   GIF version

Definition df-vma 25667
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.)
Assertion
Ref Expression
df-vma Λ = (𝑥 ∈ ℕ ↦ {𝑝 ∈ ℙ ∣ 𝑝𝑥} / 𝑠if((♯‘𝑠) = 1, (log‘ 𝑠), 0))
Distinct variable group:   𝑠,𝑝,𝑥

Detailed syntax breakdown of Definition df-vma
StepHypRef Expression
1 cvma 25661 . 2 class Λ
2 vx . . 3 setvar 𝑥
3 cn 11630 . . 3 class
4 vs . . . 4 setvar 𝑠
5 vp . . . . . . 7 setvar 𝑝
65cv 1529 . . . . . 6 class 𝑝
72cv 1529 . . . . . 6 class 𝑥
8 cdvds 15599 . . . . . 6 class
96, 7, 8wbr 5057 . . . . 5 wff 𝑝𝑥
10 cprime 16007 . . . . 5 class
119, 5, 10crab 3140 . . . 4 class {𝑝 ∈ ℙ ∣ 𝑝𝑥}
124cv 1529 . . . . . . 7 class 𝑠
13 chash 13682 . . . . . . 7 class
1412, 13cfv 6348 . . . . . 6 class (♯‘𝑠)
15 c1 10530 . . . . . 6 class 1
1614, 15wceq 1530 . . . . 5 wff (♯‘𝑠) = 1
1712cuni 4830 . . . . . 6 class 𝑠
18 clog 25130 . . . . . 6 class log
1917, 18cfv 6348 . . . . 5 class (log‘ 𝑠)
20 cc0 10529 . . . . 5 class 0
2116, 19, 20cif 4465 . . . 4 class if((♯‘𝑠) = 1, (log‘ 𝑠), 0)
224, 11, 21csb 3881 . . 3 class {𝑝 ∈ ℙ ∣ 𝑝𝑥} / 𝑠if((♯‘𝑠) = 1, (log‘ 𝑠), 0)
232, 3, 22cmpt 5137 . 2 class (𝑥 ∈ ℕ ↦ {𝑝 ∈ ℙ ∣ 𝑝𝑥} / 𝑠if((♯‘𝑠) = 1, (log‘ 𝑠), 0))
241, 23wceq 1530 1 wff Λ = (𝑥 ∈ ℕ ↦ {𝑝 ∈ ℙ ∣ 𝑝𝑥} / 𝑠if((♯‘𝑠) = 1, (log‘ 𝑠), 0))
Colors of variables: wff setvar class
This definition is referenced by:  vmaval  25682  vmaf  25688
  Copyright terms: Public domain W3C validator