Detailed syntax breakdown of Definition df-vma
Step | Hyp | Ref
| Expression |
1 | | cvma 26001 |
. 2
class
Λ |
2 | | vx |
. . 3
setvar 𝑥 |
3 | | cn 11855 |
. . 3
class
ℕ |
4 | | vs |
. . . 4
setvar 𝑠 |
5 | | vp |
. . . . . . 7
setvar 𝑝 |
6 | 5 | cv 1542 |
. . . . . 6
class 𝑝 |
7 | 2 | cv 1542 |
. . . . . 6
class 𝑥 |
8 | | cdvds 15843 |
. . . . . 6
class
∥ |
9 | 6, 7, 8 | wbr 5068 |
. . . . 5
wff 𝑝 ∥ 𝑥 |
10 | | cprime 16256 |
. . . . 5
class
ℙ |
11 | 9, 5, 10 | crab 3066 |
. . . 4
class {𝑝 ∈ ℙ ∣ 𝑝 ∥ 𝑥} |
12 | 4 | cv 1542 |
. . . . . . 7
class 𝑠 |
13 | | chash 13924 |
. . . . . . 7
class
♯ |
14 | 12, 13 | cfv 6398 |
. . . . . 6
class
(♯‘𝑠) |
15 | | c1 10755 |
. . . . . 6
class
1 |
16 | 14, 15 | wceq 1543 |
. . . . 5
wff
(♯‘𝑠) =
1 |
17 | 12 | cuni 4834 |
. . . . . 6
class ∪ 𝑠 |
18 | | clog 25470 |
. . . . . 6
class
log |
19 | 17, 18 | cfv 6398 |
. . . . 5
class
(log‘∪ 𝑠) |
20 | | cc0 10754 |
. . . . 5
class
0 |
21 | 16, 19, 20 | cif 4454 |
. . . 4
class
if((♯‘𝑠)
= 1, (log‘∪ 𝑠), 0) |
22 | 4, 11, 21 | csb 3826 |
. . 3
class
⦋{𝑝
∈ ℙ ∣ 𝑝
∥ 𝑥} / 𝑠⦌if((♯‘𝑠) = 1, (log‘∪ 𝑠),
0) |
23 | 2, 3, 22 | cmpt 5150 |
. 2
class (𝑥 ∈ ℕ ↦
⦋{𝑝 ∈
ℙ ∣ 𝑝 ∥
𝑥} / 𝑠⦌if((♯‘𝑠) = 1, (log‘∪ 𝑠),
0)) |
24 | 1, 23 | wceq 1543 |
1
wff Λ =
(𝑥 ∈ ℕ ↦
⦋{𝑝 ∈
ℙ ∣ 𝑝 ∥
𝑥} / 𝑠⦌if((♯‘𝑠) = 1, (log‘∪ 𝑠),
0)) |