Detailed syntax breakdown of Definition df-mu
Step | Hyp | Ref
| Expression |
1 | | cmu 26240 |
. 2
class
μ |
2 | | vx |
. . 3
setvar 𝑥 |
3 | | cn 11971 |
. . 3
class
ℕ |
4 | | vp |
. . . . . . . 8
setvar 𝑝 |
5 | 4 | cv 1541 |
. . . . . . 7
class 𝑝 |
6 | | c2 12026 |
. . . . . . 7
class
2 |
7 | | cexp 13778 |
. . . . . . 7
class
↑ |
8 | 5, 6, 7 | co 7269 |
. . . . . 6
class (𝑝↑2) |
9 | 2 | cv 1541 |
. . . . . 6
class 𝑥 |
10 | | cdvds 15959 |
. . . . . 6
class
∥ |
11 | 8, 9, 10 | wbr 5079 |
. . . . 5
wff (𝑝↑2) ∥ 𝑥 |
12 | | cprime 16372 |
. . . . 5
class
ℙ |
13 | 11, 4, 12 | wrex 3067 |
. . . 4
wff
∃𝑝 ∈
ℙ (𝑝↑2) ∥
𝑥 |
14 | | cc0 10870 |
. . . 4
class
0 |
15 | | c1 10871 |
. . . . . 6
class
1 |
16 | 15 | cneg 11204 |
. . . . 5
class
-1 |
17 | 5, 9, 10 | wbr 5079 |
. . . . . . 7
wff 𝑝 ∥ 𝑥 |
18 | 17, 4, 12 | crab 3070 |
. . . . . 6
class {𝑝 ∈ ℙ ∣ 𝑝 ∥ 𝑥} |
19 | | chash 14040 |
. . . . . 6
class
♯ |
20 | 18, 19 | cfv 6431 |
. . . . 5
class
(♯‘{𝑝
∈ ℙ ∣ 𝑝
∥ 𝑥}) |
21 | 16, 20, 7 | co 7269 |
. . . 4
class
(-1↑(♯‘{𝑝 ∈ ℙ ∣ 𝑝 ∥ 𝑥})) |
22 | 13, 14, 21 | cif 4465 |
. . 3
class
if(∃𝑝 ∈
ℙ (𝑝↑2) ∥
𝑥, 0,
(-1↑(♯‘{𝑝
∈ ℙ ∣ 𝑝
∥ 𝑥}))) |
23 | 2, 3, 22 | cmpt 5162 |
. 2
class (𝑥 ∈ ℕ ↦
if(∃𝑝 ∈ ℙ
(𝑝↑2) ∥ 𝑥, 0,
(-1↑(♯‘{𝑝
∈ ℙ ∣ 𝑝
∥ 𝑥})))) |
24 | 1, 23 | wceq 1542 |
1
wff μ =
(𝑥 ∈ ℕ ↦
if(∃𝑝 ∈ ℙ
(𝑝↑2) ∥ 𝑥, 0,
(-1↑(♯‘{𝑝
∈ ℙ ∣ 𝑝
∥ 𝑥})))) |