Metamath Proof Explorer

Theorem muval2

Description: The value of the Möbius function at a squarefree number. (Contributed by Mario Carneiro, 3-Oct-2014)

Ref Expression
Assertion muval2 
|- ( ( A e. NN /\ ( mmu ` A ) =/= 0 ) -> ( mmu ` A ) = ( -u 1 ^ ( # ` { p e. Prime | p || A } ) ) )

Proof

Step Hyp Ref Expression
1 df-ne 
 |-  ( ( mmu ` A ) =/= 0 <-> -. ( mmu ` A ) = 0 )
2 ifeqor 
 |-  ( if ( E. p e. Prime ( p ^ 2 ) || A , 0 , ( -u 1 ^ ( # ` { p e. Prime | p || A } ) ) ) = 0 \/ if ( E. p e. Prime ( p ^ 2 ) || A , 0 , ( -u 1 ^ ( # ` { p e. Prime | p || A } ) ) ) = ( -u 1 ^ ( # ` { p e. Prime | p || A } ) ) )
3 muval 
 |-  ( A e. NN -> ( mmu ` A ) = if ( E. p e. Prime ( p ^ 2 ) || A , 0 , ( -u 1 ^ ( # ` { p e. Prime | p || A } ) ) ) )
4 3 eqeq1d 
 |-  ( A e. NN -> ( ( mmu ` A ) = 0 <-> if ( E. p e. Prime ( p ^ 2 ) || A , 0 , ( -u 1 ^ ( # ` { p e. Prime | p || A } ) ) ) = 0 ) )
5 3 eqeq1d 
 |-  ( A e. NN -> ( ( mmu ` A ) = ( -u 1 ^ ( # ` { p e. Prime | p || A } ) ) <-> if ( E. p e. Prime ( p ^ 2 ) || A , 0 , ( -u 1 ^ ( # ` { p e. Prime | p || A } ) ) ) = ( -u 1 ^ ( # ` { p e. Prime | p || A } ) ) ) )
6 4 5 orbi12d 
 |-  ( A e. NN -> ( ( ( mmu ` A ) = 0 \/ ( mmu ` A ) = ( -u 1 ^ ( # ` { p e. Prime | p || A } ) ) ) <-> ( if ( E. p e. Prime ( p ^ 2 ) || A , 0 , ( -u 1 ^ ( # ` { p e. Prime | p || A } ) ) ) = 0 \/ if ( E. p e. Prime ( p ^ 2 ) || A , 0 , ( -u 1 ^ ( # ` { p e. Prime | p || A } ) ) ) = ( -u 1 ^ ( # ` { p e. Prime | p || A } ) ) ) ) )
7 2 6 mpbiri 
 |-  ( A e. NN -> ( ( mmu ` A ) = 0 \/ ( mmu ` A ) = ( -u 1 ^ ( # ` { p e. Prime | p || A } ) ) ) )
8 7 ord 
 |-  ( A e. NN -> ( -. ( mmu ` A ) = 0 -> ( mmu ` A ) = ( -u 1 ^ ( # ` { p e. Prime | p || A } ) ) ) )
9 1 8 biimtrid 
 |-  ( A e. NN -> ( ( mmu ` A ) =/= 0 -> ( mmu ` A ) = ( -u 1 ^ ( # ` { p e. Prime | p || A } ) ) ) )
10 9 imp 
 |-  ( ( A e. NN /\ ( mmu ` A ) =/= 0 ) -> ( mmu ` A ) = ( -u 1 ^ ( # ` { p e. Prime | p || A } ) ) )