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

Definition df-vma 20880
 Description: Define the von Mangoldt function, which gives the logarithm of the prime at a prime power, and is zero elsewhere. (Contributed by Mario Carneiro, 7-Apr-2016.)
Assertion
Ref Expression
df-vma Λ
Distinct variable group:   ,,

Detailed syntax breakdown of Definition df-vma
StepHypRef Expression
1 cvma 20874 . 2 Λ
2 vx . . 3
3 cn 10000 . . 3
4 vs . . . 4
5 vp . . . . . . 7
65cv 1651 . . . . . 6
72cv 1651 . . . . . 6
8 cdivides 12852 . . . . . 6
96, 7, 8wbr 4212 . . . . 5
10 cprime 13079 . . . . 5
119, 5, 10crab 2709 . . . 4
124cv 1651 . . . . . . 7
13 chash 11618 . . . . . . 7
1412, 13cfv 5454 . . . . . 6
15 c1 8991 . . . . . 6
1614, 15wceq 1652 . . . . 5
1712cuni 4015 . . . . . 6
18 clog 20452 . . . . . 6
1917, 18cfv 5454 . . . . 5
20 cc0 8990 . . . . 5
2116, 19, 20cif 3739 . . . 4
224, 11, 21csb 3251 . . 3
232, 3, 22cmpt 4266 . 2
241, 23wceq 1652 1 Λ
 Colors of variables: wff set class This definition is referenced by:  vmaval  20896  vmaf  20902
 Copyright terms: Public domain W3C validator