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

Definition df-mod 10126
Description: Define the modulo (remainder) operation. See modqval 10127 for its value. For example, (5 mod 3) = 2 and (-7 mod 2) = 1. As with df-fl 10073 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 10125 . 2 class mod
2 vx . . 3 setvar 𝑥
3 vy . . 3 setvar 𝑦
4 cr 7642 . . 3 class
5 crp 9469 . . 3 class +
62cv 1331 . . . 4 class 𝑥
73cv 1331 . . . . 5 class 𝑦
8 cdiv 8455 . . . . . . 7 class /
96, 7, 8co 5781 . . . . . 6 class (𝑥 / 𝑦)
10 cfl 10071 . . . . . 6 class
119, 10cfv 5130 . . . . 5 class (⌊‘(𝑥 / 𝑦))
12 cmul 7648 . . . . 5 class ·
137, 11, 12co 5781 . . . 4 class (𝑦 · (⌊‘(𝑥 / 𝑦)))
14 cmin 7956 . . . 4 class
156, 13, 14co 5781 . . 3 class (𝑥 − (𝑦 · (⌊‘(𝑥 / 𝑦))))
162, 3, 4, 5, 15cmpo 5783 . 2 class (𝑥 ∈ ℝ, 𝑦 ∈ ℝ+ ↦ (𝑥 − (𝑦 · (⌊‘(𝑥 / 𝑦)))))
171, 16wceq 1332 1 wff mod = (𝑥 ∈ ℝ, 𝑦 ∈ ℝ+ ↦ (𝑥 − (𝑦 · (⌊‘(𝑥 / 𝑦)))))
Colors of variables: wff set class
This definition is referenced by:  modqval  10127
  Copyright terms: Public domain W3C validator