Detailed syntax breakdown of Definition df-dig
Step | Hyp | Ref
| Expression |
1 | | cdig 45642 |
. 2
class
digit |
2 | | vb |
. . 3
setvar 𝑏 |
3 | | cn 11854 |
. . 3
class
ℕ |
4 | | vk |
. . . 4
setvar 𝑘 |
5 | | vr |
. . . 4
setvar 𝑟 |
6 | | cz 12200 |
. . . 4
class
ℤ |
7 | | cc0 10753 |
. . . . 5
class
0 |
8 | | cpnf 10888 |
. . . . 5
class
+∞ |
9 | | cico 12961 |
. . . . 5
class
[,) |
10 | 7, 8, 9 | co 7231 |
. . . 4
class
(0[,)+∞) |
11 | 2 | cv 1542 |
. . . . . . . 8
class 𝑏 |
12 | 4 | cv 1542 |
. . . . . . . . 9
class 𝑘 |
13 | 12 | cneg 11087 |
. . . . . . . 8
class -𝑘 |
14 | | cexp 13659 |
. . . . . . . 8
class
↑ |
15 | 11, 13, 14 | co 7231 |
. . . . . . 7
class (𝑏↑-𝑘) |
16 | 5 | cv 1542 |
. . . . . . 7
class 𝑟 |
17 | | cmul 10758 |
. . . . . . 7
class
· |
18 | 15, 16, 17 | co 7231 |
. . . . . 6
class ((𝑏↑-𝑘) · 𝑟) |
19 | | cfl 13389 |
. . . . . 6
class
⌊ |
20 | 18, 19 | cfv 6397 |
. . . . 5
class
(⌊‘((𝑏↑-𝑘) · 𝑟)) |
21 | | cmo 13466 |
. . . . 5
class
mod |
22 | 20, 11, 21 | co 7231 |
. . . 4
class
((⌊‘((𝑏↑-𝑘) · 𝑟)) mod 𝑏) |
23 | 4, 5, 6, 10, 22 | cmpo 7233 |
. . 3
class (𝑘 ∈ ℤ, 𝑟 ∈ (0[,)+∞) ↦
((⌊‘((𝑏↑-𝑘) · 𝑟)) mod 𝑏)) |
24 | 2, 3, 23 | cmpt 5149 |
. 2
class (𝑏 ∈ ℕ ↦ (𝑘 ∈ ℤ, 𝑟 ∈ (0[,)+∞) ↦
((⌊‘((𝑏↑-𝑘) · 𝑟)) mod 𝑏))) |
25 | 1, 24 | wceq 1543 |
1
wff digit =
(𝑏 ∈ ℕ ↦
(𝑘 ∈ ℤ, 𝑟 ∈ (0[,)+∞) ↦
((⌊‘((𝑏↑-𝑘) · 𝑟)) mod 𝑏))) |