Metamath Proof Explorer

Theorem vmaf

Description: Functionality of the von Mangoldt function. (Contributed by Mario Carneiro, 7-Apr-2016)

Ref Expression
Assertion vmaf 
|- Lam : NN --> RR

Proof

Step Hyp Ref Expression
1 fvex 
 |-  ( log ` U. s ) e. _V
2 c0ex 
 |-  0 e. _V
3 1 2 ifex 
 |-  if ( ( # ` s ) = 1 , ( log ` U. s ) , 0 ) e. _V
4 3 csbex 
 |-  [_ { p e. Prime | p || x } / s ]_ if ( ( # ` s ) = 1 , ( log ` U. s ) , 0 ) e. _V
5 4 a1i 
 |-  ( ( T. /\ x e. NN ) -> [_ { p e. Prime | p || x } / s ]_ if ( ( # ` s ) = 1 , ( log ` U. s ) , 0 ) e. _V )
6 df-vma 
 |-  Lam = ( x e. NN |-> [_ { p e. Prime | p || x } / s ]_ if ( ( # ` s ) = 1 , ( log ` U. s ) , 0 ) )
7 6 a1i 
 |-  ( T. -> Lam = ( x e. NN |-> [_ { p e. Prime | p || x } / s ]_ if ( ( # ` s ) = 1 , ( log ` U. s ) , 0 ) ) )
8 vmacl 
 |-  ( n e. NN -> ( Lam ` n ) e. RR )
9 8 adantl 
 |-  ( ( T. /\ n e. NN ) -> ( Lam ` n ) e. RR )
10 5 7 9 fmpt2d 
 |-  ( T. -> Lam : NN --> RR )
11 10 mptru 
 |-  Lam : NN --> RR