Detailed syntax breakdown of Definition df-dig
Step | Hyp | Ref
| Expression |
1 | | cdig 42389 |
. 2
class
digit |
2 | | vb |
. . 3
setvar 𝑏 |
3 | | cn 11020 |
. . 3
class
ℕ |
4 | | vk |
. . . 4
setvar 𝑘 |
5 | | vr |
. . . 4
setvar 𝑟 |
6 | | cz 11377 |
. . . 4
class
ℤ |
7 | | cc0 9936 |
. . . . 5
class
0 |
8 | | cpnf 10071 |
. . . . 5
class
+∞ |
9 | | cico 12177 |
. . . . 5
class
[,) |
10 | 7, 8, 9 | co 6650 |
. . . 4
class
(0[,)+∞) |
11 | 2 | cv 1482 |
. . . . . . . 8
class 𝑏 |
12 | 4 | cv 1482 |
. . . . . . . . 9
class 𝑘 |
13 | 12 | cneg 10267 |
. . . . . . . 8
class -𝑘 |
14 | | cexp 12860 |
. . . . . . . 8
class
↑ |
15 | 11, 13, 14 | co 6650 |
. . . . . . 7
class (𝑏↑-𝑘) |
16 | 5 | cv 1482 |
. . . . . . 7
class 𝑟 |
17 | | cmul 9941 |
. . . . . . 7
class
· |
18 | 15, 16, 17 | co 6650 |
. . . . . 6
class ((𝑏↑-𝑘) · 𝑟) |
19 | | cfl 12591 |
. . . . . 6
class
⌊ |
20 | 18, 19 | cfv 5888 |
. . . . 5
class
(⌊‘((𝑏↑-𝑘) · 𝑟)) |
21 | | cmo 12668 |
. . . . 5
class
mod |
22 | 20, 11, 21 | co 6650 |
. . . 4
class
((⌊‘((𝑏↑-𝑘) · 𝑟)) mod 𝑏) |
23 | 4, 5, 6, 10, 22 | cmpt2 6652 |
. . 3
class (𝑘 ∈ ℤ, 𝑟 ∈ (0[,)+∞) ↦
((⌊‘((𝑏↑-𝑘) · 𝑟)) mod 𝑏)) |
24 | 2, 3, 23 | cmpt 4729 |
. 2
class (𝑏 ∈ ℕ ↦ (𝑘 ∈ ℤ, 𝑟 ∈ (0[,)+∞) ↦
((⌊‘((𝑏↑-𝑘) · 𝑟)) mod 𝑏))) |
25 | 1, 24 | wceq 1483 |
1
wff digit =
(𝑏 ∈ ℕ ↦
(𝑘 ∈ ℤ, 𝑟 ∈ (0[,)+∞) ↦
((⌊‘((𝑏↑-𝑘) · 𝑟)) mod 𝑏))) |