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 ( 𝐴 ∈ β„• β†’ ( abs β€˜ ( ΞΌ β€˜ 𝐴 ) ) ≀ 1 )

Proof

Step Hyp Ref Expression
1 muval ⊒ ( 𝐴 ∈ β„• β†’ ( ΞΌ β€˜ 𝐴 ) = if ( βˆƒ 𝑝 ∈ β„™ ( 𝑝 ↑ 2 ) βˆ₯ 𝐴 , 0 , ( - 1 ↑ ( β™― β€˜ { 𝑝 ∈ β„™ ∣ 𝑝 βˆ₯ 𝐴 } ) ) ) )
2 iftrue ⊒ ( βˆƒ 𝑝 ∈ β„™ ( 𝑝 ↑ 2 ) βˆ₯ 𝐴 β†’ if ( βˆƒ 𝑝 ∈ β„™ ( 𝑝 ↑ 2 ) βˆ₯ 𝐴 , 0 , ( - 1 ↑ ( β™― β€˜ { 𝑝 ∈ β„™ ∣ 𝑝 βˆ₯ 𝐴 } ) ) ) = 0 )
3 1 2 sylan9eq ⊒ ( ( 𝐴 ∈ β„• ∧ βˆƒ 𝑝 ∈ β„™ ( 𝑝 ↑ 2 ) βˆ₯ 𝐴 ) β†’ ( ΞΌ β€˜ 𝐴 ) = 0 )
4 3 fveq2d ⊒ ( ( 𝐴 ∈ β„• ∧ βˆƒ 𝑝 ∈ β„™ ( 𝑝 ↑ 2 ) βˆ₯ 𝐴 ) β†’ ( abs β€˜ ( ΞΌ β€˜ 𝐴 ) ) = ( abs β€˜ 0 ) )
5 abs0 ⊒ ( abs β€˜ 0 ) = 0
6 0le1 ⊒ 0 ≀ 1
7 5 6 eqbrtri ⊒ ( abs β€˜ 0 ) ≀ 1
8 4 7 eqbrtrdi ⊒ ( ( 𝐴 ∈ β„• ∧ βˆƒ 𝑝 ∈ β„™ ( 𝑝 ↑ 2 ) βˆ₯ 𝐴 ) β†’ ( abs β€˜ ( ΞΌ β€˜ 𝐴 ) ) ≀ 1 )
9 iffalse ⊒ ( Β¬ βˆƒ 𝑝 ∈ β„™ ( 𝑝 ↑ 2 ) βˆ₯ 𝐴 β†’ if ( βˆƒ 𝑝 ∈ β„™ ( 𝑝 ↑ 2 ) βˆ₯ 𝐴 , 0 , ( - 1 ↑ ( β™― β€˜ { 𝑝 ∈ β„™ ∣ 𝑝 βˆ₯ 𝐴 } ) ) ) = ( - 1 ↑ ( β™― β€˜ { 𝑝 ∈ β„™ ∣ 𝑝 βˆ₯ 𝐴 } ) ) )
10 1 9 sylan9eq ⊒ ( ( 𝐴 ∈ β„• ∧ Β¬ βˆƒ 𝑝 ∈ β„™ ( 𝑝 ↑ 2 ) βˆ₯ 𝐴 ) β†’ ( ΞΌ β€˜ 𝐴 ) = ( - 1 ↑ ( β™― β€˜ { 𝑝 ∈ β„™ ∣ 𝑝 βˆ₯ 𝐴 } ) ) )
11 10 fveq2d ⊒ ( ( 𝐴 ∈ β„• ∧ Β¬ βˆƒ 𝑝 ∈ β„™ ( 𝑝 ↑ 2 ) βˆ₯ 𝐴 ) β†’ ( abs β€˜ ( ΞΌ β€˜ 𝐴 ) ) = ( abs β€˜ ( - 1 ↑ ( β™― β€˜ { 𝑝 ∈ β„™ ∣ 𝑝 βˆ₯ 𝐴 } ) ) ) )
12 neg1cn ⊒ - 1 ∈ β„‚
13 prmdvdsfi ⊒ ( 𝐴 ∈ β„• β†’ { 𝑝 ∈ β„™ ∣ 𝑝 βˆ₯ 𝐴 } ∈ Fin )
14 hashcl ⊒ ( { 𝑝 ∈ β„™ ∣ 𝑝 βˆ₯ 𝐴 } ∈ Fin β†’ ( β™― β€˜ { 𝑝 ∈ β„™ ∣ 𝑝 βˆ₯ 𝐴 } ) ∈ β„•0 )
15 13 14 syl ⊒ ( 𝐴 ∈ β„• β†’ ( β™― β€˜ { 𝑝 ∈ β„™ ∣ 𝑝 βˆ₯ 𝐴 } ) ∈ β„•0 )
16 absexp ⊒ ( ( - 1 ∈ β„‚ ∧ ( β™― β€˜ { 𝑝 ∈ β„™ ∣ 𝑝 βˆ₯ 𝐴 } ) ∈ β„•0 ) β†’ ( abs β€˜ ( - 1 ↑ ( β™― β€˜ { 𝑝 ∈ β„™ ∣ 𝑝 βˆ₯ 𝐴 } ) ) ) = ( ( abs β€˜ - 1 ) ↑ ( β™― β€˜ { 𝑝 ∈ β„™ ∣ 𝑝 βˆ₯ 𝐴 } ) ) )
17 12 15 16 sylancr ⊒ ( 𝐴 ∈ β„• β†’ ( abs β€˜ ( - 1 ↑ ( β™― β€˜ { 𝑝 ∈ β„™ ∣ 𝑝 βˆ₯ 𝐴 } ) ) ) = ( ( abs β€˜ - 1 ) ↑ ( β™― β€˜ { 𝑝 ∈ β„™ ∣ 𝑝 βˆ₯ 𝐴 } ) ) )
18 ax-1cn ⊒ 1 ∈ β„‚
19 18 absnegi ⊒ ( abs β€˜ - 1 ) = ( abs β€˜ 1 )
20 abs1 ⊒ ( abs β€˜ 1 ) = 1
21 19 20 eqtri ⊒ ( abs β€˜ - 1 ) = 1
22 21 oveq1i ⊒ ( ( abs β€˜ - 1 ) ↑ ( β™― β€˜ { 𝑝 ∈ β„™ ∣ 𝑝 βˆ₯ 𝐴 } ) ) = ( 1 ↑ ( β™― β€˜ { 𝑝 ∈ β„™ ∣ 𝑝 βˆ₯ 𝐴 } ) )
23 15 nn0zd ⊒ ( 𝐴 ∈ β„• β†’ ( β™― β€˜ { 𝑝 ∈ β„™ ∣ 𝑝 βˆ₯ 𝐴 } ) ∈ β„€ )
24 1exp ⊒ ( ( β™― β€˜ { 𝑝 ∈ β„™ ∣ 𝑝 βˆ₯ 𝐴 } ) ∈ β„€ β†’ ( 1 ↑ ( β™― β€˜ { 𝑝 ∈ β„™ ∣ 𝑝 βˆ₯ 𝐴 } ) ) = 1 )
25 23 24 syl ⊒ ( 𝐴 ∈ β„• β†’ ( 1 ↑ ( β™― β€˜ { 𝑝 ∈ β„™ ∣ 𝑝 βˆ₯ 𝐴 } ) ) = 1 )
26 22 25 eqtrid ⊒ ( 𝐴 ∈ β„• β†’ ( ( abs β€˜ - 1 ) ↑ ( β™― β€˜ { 𝑝 ∈ β„™ ∣ 𝑝 βˆ₯ 𝐴 } ) ) = 1 )
27 17 26 eqtrd ⊒ ( 𝐴 ∈ β„• β†’ ( abs β€˜ ( - 1 ↑ ( β™― β€˜ { 𝑝 ∈ β„™ ∣ 𝑝 βˆ₯ 𝐴 } ) ) ) = 1 )
28 27 adantr ⊒ ( ( 𝐴 ∈ β„• ∧ Β¬ βˆƒ 𝑝 ∈ β„™ ( 𝑝 ↑ 2 ) βˆ₯ 𝐴 ) β†’ ( abs β€˜ ( - 1 ↑ ( β™― β€˜ { 𝑝 ∈ β„™ ∣ 𝑝 βˆ₯ 𝐴 } ) ) ) = 1 )
29 11 28 eqtrd ⊒ ( ( 𝐴 ∈ β„• ∧ Β¬ βˆƒ 𝑝 ∈ β„™ ( 𝑝 ↑ 2 ) βˆ₯ 𝐴 ) β†’ ( abs β€˜ ( ΞΌ β€˜ 𝐴 ) ) = 1 )
30 1le1 ⊒ 1 ≀ 1
31 29 30 eqbrtrdi ⊒ ( ( 𝐴 ∈ β„• ∧ Β¬ βˆƒ 𝑝 ∈ β„™ ( 𝑝 ↑ 2 ) βˆ₯ 𝐴 ) β†’ ( abs β€˜ ( ΞΌ β€˜ 𝐴 ) ) ≀ 1 )
32 8 31 pm2.61dan ⊒ ( 𝐴 ∈ β„• β†’ ( abs β€˜ ( ΞΌ β€˜ 𝐴 ) ) ≀ 1 )