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 ) )