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

Definition df-mod 9405
 Description: Define the modulo (remainder) operation. See modqval 9406 for its value. For example, (5 mod 3) = 2 and (-7 mod 2) = 1. As with df-fl 9352 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 9404 . 2 class mod
2 vx . . 3 setvar 𝑥
3 vy . . 3 setvar 𝑦
4 cr 7042 . . 3 class
5 crp 8815 . . 3 class +
62cv 1284 . . . 4 class 𝑥
73cv 1284 . . . . 5 class 𝑦
8 cdiv 7827 . . . . . . 7 class /
96, 7, 8co 5543 . . . . . 6 class (𝑥 / 𝑦)
10 cfl 9350 . . . . . 6 class
119, 10cfv 4932 . . . . 5 class (⌊‘(𝑥 / 𝑦))
12 cmul 7048 . . . . 5 class ·
137, 11, 12co 5543 . . . 4 class (𝑦 · (⌊‘(𝑥 / 𝑦)))
14 cmin 7346 . . . 4 class
156, 13, 14co 5543 . . 3 class (𝑥 − (𝑦 · (⌊‘(𝑥 / 𝑦))))
162, 3, 4, 5, 15cmpt2 5545 . 2 class (𝑥 ∈ ℝ, 𝑦 ∈ ℝ+ ↦ (𝑥 − (𝑦 · (⌊‘(𝑥 / 𝑦)))))
171, 16wceq 1285 1 wff mod = (𝑥 ∈ ℝ, 𝑦 ∈ ℝ+ ↦ (𝑥 − (𝑦 · (⌊‘(𝑥 / 𝑦)))))
 Colors of variables: wff set class This definition is referenced by:  modqval  9406
 Copyright terms: Public domain W3C validator