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

Definition df-mod 10354
Description: Define the modulo (remainder) operation. See modqval 10355 for its value. For example, (5 mod 3) = 2 and (-7 mod 2) = 1. As with df-fl 10301 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 10353 . 2 class mod
2 vx . . 3 setvar 𝑥
3 vy . . 3 setvar 𝑦
4 cr 7840 . . 3 class
5 crp 9683 . . 3 class +
62cv 1363 . . . 4 class 𝑥
73cv 1363 . . . . 5 class 𝑦
8 cdiv 8659 . . . . . . 7 class /
96, 7, 8co 5896 . . . . . 6 class (𝑥 / 𝑦)
10 cfl 10299 . . . . . 6 class
119, 10cfv 5235 . . . . 5 class (⌊‘(𝑥 / 𝑦))
12 cmul 7846 . . . . 5 class ·
137, 11, 12co 5896 . . . 4 class (𝑦 · (⌊‘(𝑥 / 𝑦)))
14 cmin 8158 . . . 4 class
156, 13, 14co 5896 . . 3 class (𝑥 − (𝑦 · (⌊‘(𝑥 / 𝑦))))
162, 3, 4, 5, 15cmpo 5898 . 2 class (𝑥 ∈ ℝ, 𝑦 ∈ ℝ+ ↦ (𝑥 − (𝑦 · (⌊‘(𝑥 / 𝑦)))))
171, 16wceq 1364 1 wff mod = (𝑥 ∈ ℝ, 𝑦 ∈ ℝ+ ↦ (𝑥 − (𝑦 · (⌊‘(𝑥 / 𝑦)))))
Colors of variables: wff set class
This definition is referenced by:  modqval  10355
  Copyright terms: Public domain W3C validator