Definition df-mod 9983

Description: Define the modulo (remainder) operation. See modqval 9984 for its value. For example, (5 mod 3) = 2 and (-7 mod 2) = 1. As with df-fl 9930 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

Step	Hyp	Ref	Expression
1		cmo 9982	. 2 class mod
2		vx	. . 3 setvar 𝑥
3		vy	. . 3 setvar 𝑦
4		cr 7540	. . 3 class ℝ
5		crp 9337	. . 3 class ℝ+
6	2	cv 1311	. . . 4 class 𝑥
7	3	cv 1311	. . . . 5 class 𝑦
8		cdiv 8339	. . . . . . 7 class /
9	6, 7, 8	co 5726	. . . . . 6 class (𝑥 / 𝑦)
10		cfl 9928	. . . . . 6 class ⌊
11	9, 10	cfv 5079	. . . . 5 class (⌊‘(𝑥 / 𝑦))
12		cmul 7546	. . . . 5 class ·
13	7, 11, 12	co 5726	. . . 4 class (𝑦 · (⌊‘(𝑥 / 𝑦)))
14		cmin 7850	. . . 4 class −
15	6, 13, 14	co 5726	. . 3 class (𝑥 − (𝑦 · (⌊‘(𝑥 / 𝑦))))
16	2, 3, 4, 5, 15	cmpo 5728	. 2 class (𝑥 ∈ ℝ, 𝑦 ∈ ℝ+ ↦ (𝑥 − (𝑦 · (⌊‘(𝑥 / 𝑦)))))
17	1, 16	wceq 1312	1 wff mod = (𝑥 ∈ ℝ, 𝑦 ∈ ℝ+ ↦ (𝑥 − (𝑦 · (⌊‘(𝑥 / 𝑦)))))

This definition is referenced by:  modqval  9984