MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  df-mu Structured version   Visualization version   GIF version

Definition df-mu 25605
Description: Define the Möbius function, which is zero for non-squarefree numbers and is -1 or 1 for squarefree numbers according as to the number of prime divisors of the number is even or odd, see definition in [ApostolNT] p. 24. (Contributed by Mario Carneiro, 22-Sep-2014.)
Assertion
Ref Expression
df-mu μ = (𝑥 ∈ ℕ ↦ if(∃𝑝 ∈ ℙ (𝑝↑2) ∥ 𝑥, 0, (-1↑(♯‘{𝑝 ∈ ℙ ∣ 𝑝𝑥}))))
Distinct variable group:   𝑥,𝑝

Detailed syntax breakdown of Definition df-mu
StepHypRef Expression
1 cmu 25599 . 2 class μ
2 vx . . 3 setvar 𝑥
3 cn 11626 . . 3 class
4 vp . . . . . . . 8 setvar 𝑝
54cv 1527 . . . . . . 7 class 𝑝
6 c2 11680 . . . . . . 7 class 2
7 cexp 13417 . . . . . . 7 class
85, 6, 7co 7145 . . . . . 6 class (𝑝↑2)
92cv 1527 . . . . . 6 class 𝑥
10 cdvds 15595 . . . . . 6 class
118, 9, 10wbr 5057 . . . . 5 wff (𝑝↑2) ∥ 𝑥
12 cprime 16003 . . . . 5 class
1311, 4, 12wrex 3136 . . . 4 wff 𝑝 ∈ ℙ (𝑝↑2) ∥ 𝑥
14 cc0 10525 . . . 4 class 0
15 c1 10526 . . . . . 6 class 1
1615cneg 10859 . . . . 5 class -1
175, 9, 10wbr 5057 . . . . . . 7 wff 𝑝𝑥
1817, 4, 12crab 3139 . . . . . 6 class {𝑝 ∈ ℙ ∣ 𝑝𝑥}
19 chash 13678 . . . . . 6 class
2018, 19cfv 6348 . . . . 5 class (♯‘{𝑝 ∈ ℙ ∣ 𝑝𝑥})
2116, 20, 7co 7145 . . . 4 class (-1↑(♯‘{𝑝 ∈ ℙ ∣ 𝑝𝑥}))
2213, 14, 21cif 4463 . . 3 class if(∃𝑝 ∈ ℙ (𝑝↑2) ∥ 𝑥, 0, (-1↑(♯‘{𝑝 ∈ ℙ ∣ 𝑝𝑥})))
232, 3, 22cmpt 5137 . 2 class (𝑥 ∈ ℕ ↦ if(∃𝑝 ∈ ℙ (𝑝↑2) ∥ 𝑥, 0, (-1↑(♯‘{𝑝 ∈ ℙ ∣ 𝑝𝑥}))))
241, 23wceq 1528 1 wff μ = (𝑥 ∈ ℕ ↦ if(∃𝑝 ∈ ℙ (𝑝↑2) ∥ 𝑥, 0, (-1↑(♯‘{𝑝 ∈ ℙ ∣ 𝑝𝑥}))))
Colors of variables: wff setvar class
This definition is referenced by:  muval  25636  muf  25644
  Copyright terms: Public domain W3C validator