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 
|- Lam = ( x e. NN |-> [_ { p e. Prime | p || x } / s ]_ if ( ( # ` s ) = 1 , ( log ` U. s ) , 0 ) )

Detailed syntax breakdown

Step Hyp Ref Expression
0 cvma 
 |-  Lam
1 vx 
 |-  x
2 cn 
 |-  NN
3 vp 
 |-  p
4 cprime 
 |-  Prime
5 3 cv 
 |-  p
6 cdvds 
 |-  ||
7 1 cv 
 |-  x
8 5 7 6 wbr 
 |-  p || x
9 8 3 4 crab 
 |-  { p e. Prime | p || x }
10 vs 
 |-  s
11 chash 
 |-  #
12 10 cv 
 |-  s
13 12 11 cfv 
 |-  ( # ` s )
14 c1 
 |-  1
15 13 14 wceq 
 |-  ( # ` s ) = 1
16 clog 
 |-  log
17 12 cuni 
 |-  U. s
18 17 16 cfv 
 |-  ( log ` U. s )
19 cc0 
 |-  0
20 15 18 19 cif 
 |-  if ( ( # ` s ) = 1 , ( log ` U. s ) , 0 )
21 10 9 20 csb 
 |-  [_ { p e. Prime | p || x } / s ]_ if ( ( # ` s ) = 1 , ( log ` U. s ) , 0 )
22 1 2 21 cmpt 
 |-  ( x e. NN |-> [_ { p e. Prime | p || x } / s ]_ if ( ( # ` s ) = 1 , ( log ` U. s ) , 0 ) )
23 0 22 wceq 
 |-  Lam = ( x e. NN |-> [_ { p e. Prime | p || x } / s ]_ if ( ( # ` s ) = 1 , ( log ` U. s ) , 0 ) )