Metamath Proof Explorer

Theorem mule1

Description: The Möbius function takes on values in magnitude at most 1 . (Together with mucl , this implies that it takes a value in { -u 1 , 0 , 1 } for every positive integer.) (Contributed by Mario Carneiro, 22-Sep-2014)

Ref Expression
Assertion mule1 
|- ( A e. NN -> ( abs ` ( mmu ` A ) ) <_ 1 )

Proof

Step Hyp Ref Expression
1 muval 
 |-  ( A e. NN -> ( mmu ` A ) = if ( E. p e. Prime ( p ^ 2 ) || A , 0 , ( -u 1 ^ ( # ` { p e. Prime | p || A } ) ) ) )
2 iftrue 
 |-  ( E. p e. Prime ( p ^ 2 ) || A -> if ( E. p e. Prime ( p ^ 2 ) || A , 0 , ( -u 1 ^ ( # ` { p e. Prime | p || A } ) ) ) = 0 )
3 1 2 sylan9eq 
 |-  ( ( A e. NN /\ E. p e. Prime ( p ^ 2 ) || A ) -> ( mmu ` A ) = 0 )
4 3 fveq2d 
 |-  ( ( A e. NN /\ E. p e. Prime ( p ^ 2 ) || A ) -> ( abs ` ( mmu ` A ) ) = ( abs ` 0 ) )
5 abs0 
 |-  ( abs ` 0 ) = 0
6 0le1 
 |-  0 <_ 1
7 5 6 eqbrtri 
 |-  ( abs ` 0 ) <_ 1
8 4 7 eqbrtrdi 
 |-  ( ( A e. NN /\ E. p e. Prime ( p ^ 2 ) || A ) -> ( abs ` ( mmu ` A ) ) <_ 1 )
9 iffalse 
 |-  ( -. E. p e. Prime ( p ^ 2 ) || A -> if ( E. p e. Prime ( p ^ 2 ) || A , 0 , ( -u 1 ^ ( # ` { p e. Prime | p || A } ) ) ) = ( -u 1 ^ ( # ` { p e. Prime | p || A } ) ) )
10 1 9 sylan9eq 
 |-  ( ( A e. NN /\ -. E. p e. Prime ( p ^ 2 ) || A ) -> ( mmu ` A ) = ( -u 1 ^ ( # ` { p e. Prime | p || A } ) ) )
11 10 fveq2d 
 |-  ( ( A e. NN /\ -. E. p e. Prime ( p ^ 2 ) || A ) -> ( abs ` ( mmu ` A ) ) = ( abs ` ( -u 1 ^ ( # ` { p e. Prime | p || A } ) ) ) )
12 neg1cn 
 |-  -u 1 e. CC
13 prmdvdsfi 
 |-  ( A e. NN -> { p e. Prime | p || A } e. Fin )
14 hashcl 
 |-  ( { p e. Prime | p || A } e. Fin -> ( # ` { p e. Prime | p || A } ) e. NN0 )
15 13 14 syl 
 |-  ( A e. NN -> ( # ` { p e. Prime | p || A } ) e. NN0 )
16 absexp 
 |-  ( ( -u 1 e. CC /\ ( # ` { p e. Prime | p || A } ) e. NN0 ) -> ( abs ` ( -u 1 ^ ( # ` { p e. Prime | p || A } ) ) ) = ( ( abs ` -u 1 ) ^ ( # ` { p e. Prime | p || A } ) ) )
17 12 15 16 sylancr 
 |-  ( A e. NN -> ( abs ` ( -u 1 ^ ( # ` { p e. Prime | p || A } ) ) ) = ( ( abs ` -u 1 ) ^ ( # ` { p e. Prime | p || A } ) ) )
18 ax-1cn 
 |-  1 e. CC
19 18 absnegi 
 |-  ( abs ` -u 1 ) = ( abs ` 1 )
20 abs1 
 |-  ( abs ` 1 ) = 1
21 19 20 eqtri 
 |-  ( abs ` -u 1 ) = 1
22 21 oveq1i 
 |-  ( ( abs ` -u 1 ) ^ ( # ` { p e. Prime | p || A } ) ) = ( 1 ^ ( # ` { p e. Prime | p || A } ) )
23 15 nn0zd 
 |-  ( A e. NN -> ( # ` { p e. Prime | p || A } ) e. ZZ )
24 1exp 
 |-  ( ( # ` { p e. Prime | p || A } ) e. ZZ -> ( 1 ^ ( # ` { p e. Prime | p || A } ) ) = 1 )
25 23 24 syl 
 |-  ( A e. NN -> ( 1 ^ ( # ` { p e. Prime | p || A } ) ) = 1 )
26 22 25 syl5eq 
 |-  ( A e. NN -> ( ( abs ` -u 1 ) ^ ( # ` { p e. Prime | p || A } ) ) = 1 )
27 17 26 eqtrd 
 |-  ( A e. NN -> ( abs ` ( -u 1 ^ ( # ` { p e. Prime | p || A } ) ) ) = 1 )
28 27 adantr 
 |-  ( ( A e. NN /\ -. E. p e. Prime ( p ^ 2 ) || A ) -> ( abs ` ( -u 1 ^ ( # ` { p e. Prime | p || A } ) ) ) = 1 )
29 11 28 eqtrd 
 |-  ( ( A e. NN /\ -. E. p e. Prime ( p ^ 2 ) || A ) -> ( abs ` ( mmu ` A ) ) = 1 )
30 1le1 
 |-  1 <_ 1
31 29 30 eqbrtrdi 
 |-  ( ( A e. NN /\ -. E. p e. Prime ( p ^ 2 ) || A ) -> ( abs ` ( mmu ` A ) ) <_ 1 )
32 8 31 pm2.61dan 
 |-  ( A e. NN -> ( abs ` ( mmu ` A ) ) <_ 1 )