Detailed syntax breakdown of Definition df-mu
Step | Hyp | Ref
| Expression |
1 | | cmu 25931 |
. 2
class
μ |
2 | | vx |
. . 3
setvar 𝑥 |
3 | | cn 11795 |
. . 3
class
ℕ |
4 | | vp |
. . . . . . . 8
setvar 𝑝 |
5 | 4 | cv 1542 |
. . . . . . 7
class 𝑝 |
6 | | c2 11850 |
. . . . . . 7
class
2 |
7 | | cexp 13600 |
. . . . . . 7
class
↑ |
8 | 5, 6, 7 | co 7191 |
. . . . . 6
class (𝑝↑2) |
9 | 2 | cv 1542 |
. . . . . 6
class 𝑥 |
10 | | cdvds 15778 |
. . . . . 6
class
∥ |
11 | 8, 9, 10 | wbr 5039 |
. . . . 5
wff (𝑝↑2) ∥ 𝑥 |
12 | | cprime 16191 |
. . . . 5
class
ℙ |
13 | 11, 4, 12 | wrex 3052 |
. . . 4
wff
∃𝑝 ∈
ℙ (𝑝↑2) ∥
𝑥 |
14 | | cc0 10694 |
. . . 4
class
0 |
15 | | c1 10695 |
. . . . . 6
class
1 |
16 | 15 | cneg 11028 |
. . . . 5
class
-1 |
17 | 5, 9, 10 | wbr 5039 |
. . . . . . 7
wff 𝑝 ∥ 𝑥 |
18 | 17, 4, 12 | crab 3055 |
. . . . . 6
class {𝑝 ∈ ℙ ∣ 𝑝 ∥ 𝑥} |
19 | | chash 13861 |
. . . . . 6
class
♯ |
20 | 18, 19 | cfv 6358 |
. . . . 5
class
(♯‘{𝑝
∈ ℙ ∣ 𝑝
∥ 𝑥}) |
21 | 16, 20, 7 | co 7191 |
. . . 4
class
(-1↑(♯‘{𝑝 ∈ ℙ ∣ 𝑝 ∥ 𝑥})) |
22 | 13, 14, 21 | cif 4425 |
. . 3
class
if(∃𝑝 ∈
ℙ (𝑝↑2) ∥
𝑥, 0,
(-1↑(♯‘{𝑝
∈ ℙ ∣ 𝑝
∥ 𝑥}))) |
23 | 2, 3, 22 | cmpt 5120 |
. 2
class (𝑥 ∈ ℕ ↦
if(∃𝑝 ∈ ℙ
(𝑝↑2) ∥ 𝑥, 0,
(-1↑(♯‘{𝑝
∈ ℙ ∣ 𝑝
∥ 𝑥})))) |
24 | 1, 23 | wceq 1543 |
1
wff μ =
(𝑥 ∈ ℕ ↦
if(∃𝑝 ∈ ℙ
(𝑝↑2) ∥ 𝑥, 0,
(-1↑(♯‘{𝑝
∈ ℙ ∣ 𝑝
∥ 𝑥})))) |