Detailed syntax breakdown of Definition df-bits
| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | cbits 16457 | . 2
class
bits | 
| 2 |  | vn | . . 3
setvar 𝑛 | 
| 3 |  | cz 12615 | . . 3
class
ℤ | 
| 4 |  | c2 12322 | . . . . . 6
class
2 | 
| 5 | 2 | cv 1538 | . . . . . . . 8
class 𝑛 | 
| 6 |  | vm | . . . . . . . . . 10
setvar 𝑚 | 
| 7 | 6 | cv 1538 | . . . . . . . . 9
class 𝑚 | 
| 8 |  | cexp 14103 | . . . . . . . . 9
class
↑ | 
| 9 | 4, 7, 8 | co 7432 | . . . . . . . 8
class
(2↑𝑚) | 
| 10 |  | cdiv 11921 | . . . . . . . 8
class 
/ | 
| 11 | 5, 9, 10 | co 7432 | . . . . . . 7
class (𝑛 / (2↑𝑚)) | 
| 12 |  | cfl 13831 | . . . . . . 7
class
⌊ | 
| 13 | 11, 12 | cfv 6560 | . . . . . 6
class
(⌊‘(𝑛 /
(2↑𝑚))) | 
| 14 |  | cdvds 16291 | . . . . . 6
class 
∥ | 
| 15 | 4, 13, 14 | wbr 5142 | . . . . 5
wff 2 ∥
(⌊‘(𝑛 /
(2↑𝑚))) | 
| 16 | 15 | wn 3 | . . . 4
wff  ¬ 2
∥ (⌊‘(𝑛 /
(2↑𝑚))) | 
| 17 |  | cn0 12528 | . . . 4
class
ℕ0 | 
| 18 | 16, 6, 17 | crab 3435 | . . 3
class {𝑚 ∈ ℕ0
∣ ¬ 2 ∥ (⌊‘(𝑛 / (2↑𝑚)))} | 
| 19 | 2, 3, 18 | cmpt 5224 | . 2
class (𝑛 ∈ ℤ ↦ {𝑚 ∈ ℕ0
∣ ¬ 2 ∥ (⌊‘(𝑛 / (2↑𝑚)))}) | 
| 20 | 1, 19 | wceq 1539 | 1
wff bits =
(𝑛 ∈ ℤ ↦
{𝑚 ∈
ℕ0 ∣ ¬ 2 ∥ (⌊‘(𝑛 / (2↑𝑚)))}) |