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 ∈ ℕ → μ ⁡ A ≤ 1

Proof

Step Hyp Ref Expression
1 muval ⊢ A ∈ ℕ → μ ⁡ A = if ∃ p ∈ ℙ p 2 ∥ A 0 − 1 p ∈ ℙ | p ∥ A
2 iftrue ⊢ ∃ p ∈ ℙ p 2 ∥ A → if ∃ p ∈ ℙ p 2 ∥ A 0 − 1 p ∈ ℙ | p ∥ A = 0
3 1 2 sylan9eq ⊢ A ∈ ℕ ∧ ∃ p ∈ ℙ p 2 ∥ A → μ ⁡ A = 0
4 3 fveq2d ⊢ A ∈ ℕ ∧ ∃ p ∈ ℙ p 2 ∥ A → μ ⁡ A = 0
5 abs0 ⊢ 0 = 0
6 0le1 ⊢ 0 ≤ 1
7 5 6 eqbrtri ⊢ 0 ≤ 1
8 4 7 eqbrtrdi ⊢ A ∈ ℕ ∧ ∃ p ∈ ℙ p 2 ∥ A → μ ⁡ A ≤ 1
9 iffalse ⊢ ¬ ∃ p ∈ ℙ p 2 ∥ A → if ∃ p ∈ ℙ p 2 ∥ A 0 − 1 p ∈ ℙ | p ∥ A = − 1 p ∈ ℙ | p ∥ A
10 1 9 sylan9eq ⊢ A ∈ ℕ ∧ ¬ ∃ p ∈ ℙ p 2 ∥ A → μ ⁡ A = − 1 p ∈ ℙ | p ∥ A
11 10 fveq2d ⊢ A ∈ ℕ ∧ ¬ ∃ p ∈ ℙ p 2 ∥ A → μ ⁡ A = − 1 p ∈ ℙ | p ∥ A
12 neg1cn ⊢ − 1 ∈ ℂ
13 prmdvdsfi ⊢ A ∈ ℕ → p ∈ ℙ | p ∥ A ∈ Fin
14 hashcl ⊢ p ∈ ℙ | p ∥ A ∈ Fin → p ∈ ℙ | p ∥ A ∈ ℕ 0
15 13 14 syl ⊢ A ∈ ℕ → p ∈ ℙ | p ∥ A ∈ ℕ 0
16 absexp ⊢ − 1 ∈ ℂ ∧ p ∈ ℙ | p ∥ A ∈ ℕ 0 → − 1 p ∈ ℙ | p ∥ A = − 1 p ∈ ℙ | p ∥ A
17 12 15 16 sylancr ⊢ A ∈ ℕ → − 1 p ∈ ℙ | p ∥ A = − 1 p ∈ ℙ | p ∥ A
18 ax-1cn ⊢ 1 ∈ ℂ
19 18 absnegi ⊢ − 1 = 1
20 abs1 ⊢ 1 = 1
21 19 20 eqtri ⊢ − 1 = 1
22 21 oveq1i ⊢ − 1 p ∈ ℙ | p ∥ A = 1 p ∈ ℙ | p ∥ A
23 15 nn0zd ⊢ A ∈ ℕ → p ∈ ℙ | p ∥ A ∈ ℤ
24 1exp ⊢ p ∈ ℙ | p ∥ A ∈ ℤ → 1 p ∈ ℙ | p ∥ A = 1
25 23 24 syl ⊢ A ∈ ℕ → 1 p ∈ ℙ | p ∥ A = 1
26 22 25 eqtrid ⊢ A ∈ ℕ → − 1 p ∈ ℙ | p ∥ A = 1
27 17 26 eqtrd ⊢ A ∈ ℕ → − 1 p ∈ ℙ | p ∥ A = 1
28 27 adantr ⊢ A ∈ ℕ ∧ ¬ ∃ p ∈ ℙ p 2 ∥ A → − 1 p ∈ ℙ | p ∥ A = 1
29 11 28 eqtrd ⊢ A ∈ ℕ ∧ ¬ ∃ p ∈ ℙ p 2 ∥ A → μ ⁡ A = 1
30 1le1 ⊢ 1 ≤ 1
31 29 30 eqbrtrdi ⊢ A ∈ ℕ ∧ ¬ ∃ p ∈ ℙ p 2 ∥ A → μ ⁡ A ≤ 1
32 8 31 pm2.61dan ⊢ A ∈ ℕ → μ ⁡ A ≤ 1