Detailed syntax breakdown of Definition df-mu
Step | Hyp | Ref
| Expression |
1 | | cmu 24621 |
. 2
class
μ |
2 | | vx |
. . 3
setvar 𝑥 |
3 | | cn 10897 |
. . 3
class
ℕ |
4 | | vp |
. . . . . . . 8
setvar 𝑝 |
5 | 4 | cv 1474 |
. . . . . . 7
class 𝑝 |
6 | | c2 10947 |
. . . . . . 7
class
2 |
7 | | cexp 12722 |
. . . . . . 7
class
↑ |
8 | 5, 6, 7 | co 6549 |
. . . . . 6
class (𝑝↑2) |
9 | 2 | cv 1474 |
. . . . . 6
class 𝑥 |
10 | | cdvds 14821 |
. . . . . 6
class
∥ |
11 | 8, 9, 10 | wbr 4583 |
. . . . 5
wff (𝑝↑2) ∥ 𝑥 |
12 | | cprime 15223 |
. . . . 5
class
ℙ |
13 | 11, 4, 12 | wrex 2897 |
. . . 4
wff
∃𝑝 ∈
ℙ (𝑝↑2) ∥
𝑥 |
14 | | cc0 9815 |
. . . 4
class
0 |
15 | | c1 9816 |
. . . . . 6
class
1 |
16 | 15 | cneg 10146 |
. . . . 5
class
-1 |
17 | 5, 9, 10 | wbr 4583 |
. . . . . . 7
wff 𝑝 ∥ 𝑥 |
18 | 17, 4, 12 | crab 2900 |
. . . . . 6
class {𝑝 ∈ ℙ ∣ 𝑝 ∥ 𝑥} |
19 | | chash 12979 |
. . . . . 6
class
# |
20 | 18, 19 | cfv 5804 |
. . . . 5
class
(#‘{𝑝 ∈
ℙ ∣ 𝑝 ∥
𝑥}) |
21 | 16, 20, 7 | co 6549 |
. . . 4
class
(-1↑(#‘{𝑝
∈ ℙ ∣ 𝑝
∥ 𝑥})) |
22 | 13, 14, 21 | cif 4036 |
. . 3
class
if(∃𝑝 ∈
ℙ (𝑝↑2) ∥
𝑥, 0,
(-1↑(#‘{𝑝 ∈
ℙ ∣ 𝑝 ∥
𝑥}))) |
23 | 2, 3, 22 | cmpt 4643 |
. 2
class (𝑥 ∈ ℕ ↦
if(∃𝑝 ∈ ℙ
(𝑝↑2) ∥ 𝑥, 0, (-1↑(#‘{𝑝 ∈ ℙ ∣ 𝑝 ∥ 𝑥})))) |
24 | 1, 23 | wceq 1475 |
1
wff μ =
(𝑥 ∈ ℕ ↦
if(∃𝑝 ∈ ℙ
(𝑝↑2) ∥ 𝑥, 0, (-1↑(#‘{𝑝 ∈ ℙ ∣ 𝑝 ∥ 𝑥})))) |