ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  df-mod GIF version

Definition df-mod 9238
Description: Define the modulo (remainder) operation. See modqval 9239 for its value. For example, (5 mod 3) = 2 and (-7 mod 2) = 1. As with df-fl 9187 we define this for first and second arguments which are real and positive real, respectively, even though many theorems will need to be more restricted (for example, specify rational arguments). (Contributed by NM, 10-Nov-2008.)
Assertion
Ref Expression
df-mod mod = (𝑥 ∈ ℝ, 𝑦 ∈ ℝ+ ↦ (𝑥 − (𝑦 · (⌊‘(𝑥 / 𝑦)))))
Distinct variable group:   𝑥,𝑦

Detailed syntax breakdown of Definition df-mod
StepHypRef Expression
1 cmo 9237 . 2 class mod
2 vx . . 3 setvar 𝑥
3 vy . . 3 setvar 𝑦
4 cr 6916 . . 3 class
5 crp 8651 . . 3 class +
62cv 1256 . . . 4 class 𝑥
73cv 1256 . . . . 5 class 𝑦
8 cdiv 7695 . . . . . . 7 class /
96, 7, 8co 5537 . . . . . 6 class (𝑥 / 𝑦)
10 cfl 9185 . . . . . 6 class
119, 10cfv 4927 . . . . 5 class (⌊‘(𝑥 / 𝑦))
12 cmul 6922 . . . . 5 class ·
137, 11, 12co 5537 . . . 4 class (𝑦 · (⌊‘(𝑥 / 𝑦)))
14 cmin 7215 . . . 4 class
156, 13, 14co 5537 . . 3 class (𝑥 − (𝑦 · (⌊‘(𝑥 / 𝑦))))
162, 3, 4, 5, 15cmpt2 5539 . 2 class (𝑥 ∈ ℝ, 𝑦 ∈ ℝ+ ↦ (𝑥 − (𝑦 · (⌊‘(𝑥 / 𝑦)))))
171, 16wceq 1257 1 wff mod = (𝑥 ∈ ℝ, 𝑦 ∈ ℝ+ ↦ (𝑥 − (𝑦 · (⌊‘(𝑥 / 𝑦)))))
Colors of variables: wff set class
This definition is referenced by:  modqval  9239
  Copyright terms: Public domain W3C validator