Detailed syntax breakdown of Definition df-mod
Step | Hyp | Ref
| Expression |
1 | | cmo 13570 |
. 2
class
mod |
2 | | vx |
. . 3
setvar 𝑥 |
3 | | vy |
. . 3
setvar 𝑦 |
4 | | cr 10854 |
. . 3
class
ℝ |
5 | | crp 12712 |
. . 3
class
ℝ+ |
6 | 2 | cv 1540 |
. . . 4
class 𝑥 |
7 | 3 | cv 1540 |
. . . . 5
class 𝑦 |
8 | | cdiv 11615 |
. . . . . . 7
class
/ |
9 | 6, 7, 8 | co 7268 |
. . . . . 6
class (𝑥 / 𝑦) |
10 | | cfl 13491 |
. . . . . 6
class
⌊ |
11 | 9, 10 | cfv 6430 |
. . . . 5
class
(⌊‘(𝑥 /
𝑦)) |
12 | | cmul 10860 |
. . . . 5
class
· |
13 | 7, 11, 12 | co 7268 |
. . . 4
class (𝑦 · (⌊‘(𝑥 / 𝑦))) |
14 | | cmin 11188 |
. . . 4
class
− |
15 | 6, 13, 14 | co 7268 |
. . 3
class (𝑥 − (𝑦 · (⌊‘(𝑥 / 𝑦)))) |
16 | 2, 3, 4, 5, 15 | cmpo 7270 |
. 2
class (𝑥 ∈ ℝ, 𝑦 ∈ ℝ+
↦ (𝑥 − (𝑦 · (⌊‘(𝑥 / 𝑦))))) |
17 | 1, 16 | wceq 1541 |
1
wff mod =
(𝑥 ∈ ℝ, 𝑦 ∈ ℝ+
↦ (𝑥 − (𝑦 · (⌊‘(𝑥 / 𝑦))))) |