This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 )