Metamath Proof Explorer

Theorem muval

Description: The value of the Möbius function. (Contributed by Mario Carneiro, 22-Sep-2014)

Ref Expression
Assertion muval 
|- ( A e. NN -> ( mmu ` A ) = if ( E. p e. Prime ( p ^ 2 ) || A , 0 , ( -u 1 ^ ( # ` { p e. Prime | p || A } ) ) ) )

Proof

Step Hyp Ref Expression
1 breq2 
 |-  ( x = A -> ( ( p ^ 2 ) || x <-> ( p ^ 2 ) || A ) )
2 1 rexbidv 
 |-  ( x = A -> ( E. p e. Prime ( p ^ 2 ) || x <-> E. p e. Prime ( p ^ 2 ) || A ) )
3 breq2 
 |-  ( x = A -> ( p || x <-> p || A ) )
4 3 rabbidv 
 |-  ( x = A -> { p e. Prime | p || x } = { p e. Prime | p || A } )
5 4 fveq2d 
 |-  ( x = A -> ( # ` { p e. Prime | p || x } ) = ( # ` { p e. Prime | p || A } ) )
6 5 oveq2d 
 |-  ( x = A -> ( -u 1 ^ ( # ` { p e. Prime | p || x } ) ) = ( -u 1 ^ ( # ` { p e. Prime | p || A } ) ) )
7 2 6 ifbieq2d 
 |-  ( x = A -> if ( E. p e. Prime ( p ^ 2 ) || x , 0 , ( -u 1 ^ ( # ` { p e. Prime | p || x } ) ) ) = if ( E. p e. Prime ( p ^ 2 ) || A , 0 , ( -u 1 ^ ( # ` { p e. Prime | p || A } ) ) ) )
8 df-mu 
 |-  mmu = ( x e. NN |-> if ( E. p e. Prime ( p ^ 2 ) || x , 0 , ( -u 1 ^ ( # ` { p e. Prime | p || x } ) ) ) )
9 c0ex 
 |-  0 e. _V
10 ovex 
 |-  ( -u 1 ^ ( # ` { p e. Prime | p || A } ) ) e. _V
11 9 10 ifex 
 |-  if ( E. p e. Prime ( p ^ 2 ) || A , 0 , ( -u 1 ^ ( # ` { p e. Prime | p || A } ) ) ) e. _V
12 7 8 11 fvmpt 
 |-  ( A e. NN -> ( mmu ` A ) = if ( E. p e. Prime ( p ^ 2 ) || A , 0 , ( -u 1 ^ ( # ` { p e. Prime | p || A } ) ) ) )