Metamath Proof Explorer

Theorem vmaval

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

Ref Expression
Hypothesis vmaval.1 
|- S = { p e. Prime | p || A }
Assertion vmaval 
|- ( A e. NN -> ( Lam ` A ) = if ( ( # ` S ) = 1 , ( log ` U. S ) , 0 ) )

Proof

Step Hyp Ref Expression
1 vmaval.1 
 |-  S = { p e. Prime | p || A }
2 prmex 
 |-  Prime e. _V
3 2 rabex 
 |-  { p e. Prime | p || x } e. _V
4 3 a1i 
 |-  ( x = A -> { p e. Prime | p || x } e. _V )
5 id 
 |-  ( s = { p e. Prime | p || x } -> s = { p e. Prime | p || x } )
6 breq2 
 |-  ( x = A -> ( p || x <-> p || A ) )
7 6 rabbidv 
 |-  ( x = A -> { p e. Prime | p || x } = { p e. Prime | p || A } )
8 7 1 eqtr4di 
 |-  ( x = A -> { p e. Prime | p || x } = S )
9 5 8 sylan9eqr 
 |-  ( ( x = A /\ s = { p e. Prime | p || x } ) -> s = S )
10 9 fveqeq2d 
 |-  ( ( x = A /\ s = { p e. Prime | p || x } ) -> ( ( # ` s ) = 1 <-> ( # ` S ) = 1 ) )
11 9 unieqd 
 |-  ( ( x = A /\ s = { p e. Prime | p || x } ) -> U. s = U. S )
12 11 fveq2d 
 |-  ( ( x = A /\ s = { p e. Prime | p || x } ) -> ( log ` U. s ) = ( log ` U. S ) )
13 10 12 ifbieq1d 
 |-  ( ( x = A /\ s = { p e. Prime | p || x } ) -> if ( ( # ` s ) = 1 , ( log ` U. s ) , 0 ) = if ( ( # ` S ) = 1 , ( log ` U. S ) , 0 ) )
14 4 13 csbied 
 |-  ( x = A -> [_ { p e. Prime | p || x } / s ]_ if ( ( # ` s ) = 1 , ( log ` U. s ) , 0 ) = if ( ( # ` S ) = 1 , ( log ` U. S ) , 0 ) )
15 df-vma 
 |-  Lam = ( x e. NN |-> [_ { p e. Prime | p || x } / s ]_ if ( ( # ` s ) = 1 , ( log ` U. s ) , 0 ) )
16 fvex 
 |-  ( log ` U. S ) e. _V
17 c0ex 
 |-  0 e. _V
18 16 17 ifex 
 |-  if ( ( # ` S ) = 1 , ( log ` U. S ) , 0 ) e. _V
19 14 15 18 fvmpt 
 |-  ( A e. NN -> ( Lam ` A ) = if ( ( # ` S ) = 1 , ( log ` U. S ) , 0 ) )