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 syl5bi
 |-  ( 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 } ) ) )