Detailed syntax breakdown of Definition df-bits
Step | Hyp | Ref
| Expression |
1 | | cbits 15978 |
. 2
class
bits |
2 | | vn |
. . 3
setvar 𝑛 |
3 | | cz 12176 |
. . 3
class
ℤ |
4 | | c2 11885 |
. . . . . 6
class
2 |
5 | 2 | cv 1542 |
. . . . . . . 8
class 𝑛 |
6 | | vm |
. . . . . . . . . 10
setvar 𝑚 |
7 | 6 | cv 1542 |
. . . . . . . . 9
class 𝑚 |
8 | | cexp 13635 |
. . . . . . . . 9
class
↑ |
9 | 4, 7, 8 | co 7213 |
. . . . . . . 8
class
(2↑𝑚) |
10 | | cdiv 11489 |
. . . . . . . 8
class
/ |
11 | 5, 9, 10 | co 7213 |
. . . . . . 7
class (𝑛 / (2↑𝑚)) |
12 | | cfl 13365 |
. . . . . . 7
class
⌊ |
13 | 11, 12 | cfv 6380 |
. . . . . 6
class
(⌊‘(𝑛 /
(2↑𝑚))) |
14 | | cdvds 15815 |
. . . . . 6
class
∥ |
15 | 4, 13, 14 | wbr 5053 |
. . . . 5
wff 2 ∥
(⌊‘(𝑛 /
(2↑𝑚))) |
16 | 15 | wn 3 |
. . . 4
wff ¬ 2
∥ (⌊‘(𝑛 /
(2↑𝑚))) |
17 | | cn0 12090 |
. . . 4
class
ℕ0 |
18 | 16, 6, 17 | crab 3065 |
. . 3
class {𝑚 ∈ ℕ0
∣ ¬ 2 ∥ (⌊‘(𝑛 / (2↑𝑚)))} |
19 | 2, 3, 18 | cmpt 5135 |
. 2
class (𝑛 ∈ ℤ ↦ {𝑚 ∈ ℕ0
∣ ¬ 2 ∥ (⌊‘(𝑛 / (2↑𝑚)))}) |
20 | 1, 19 | wceq 1543 |
1
wff bits =
(𝑛 ∈ ℤ ↦
{𝑚 ∈
ℕ0 ∣ ¬ 2 ∥ (⌊‘(𝑛 / (2↑𝑚)))}) |