Definition df-mod

Description: Define the modulo (remainder) operation. See modval for its value. For example, ( 5 mod 3 ) = 2 and ( -u 7 mod 2 ) = 1 ( ex-mod ). (Contributed by NM, 10-Nov-2008)

	Ref	Expression
Assertion	df-mod	$$⊢\mathrm{mod}=\left(x\in ℝ,y\in {ℝ}^{+}⟼x-y⌊\frac{x}{y}⌋\right)$$

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cmo	$$class\mathrm{mod}$$
1		vx	$$setvarx$$
2		cr	$$classℝ$$
3		vy	$$setvary$$
4		crp	$$class{ℝ}^{+}$$
5	1	cv	$$setvarx$$
6		cmin	$$class-$$
7	3	cv	$$setvary$$
8		cmul	$$class\times$$
9		cfl	$$class⌊.⌋$$
10		cdiv	$$class÷$$
11	5 7 10	co	$$class\left(\frac{x}{y}\right)$$
12	11 9	cfv	$$class⌊\frac{x}{y}⌋$$
13	7 12 8	co	$$classy⌊\frac{x}{y}⌋$$
14	5 13 6	co	$$class\left(x-y⌊\frac{x}{y}⌋\right)$$
15	1 3 2 4 14	cmpo	$$class\left(x\in ℝ,y\in {ℝ}^{+}⟼x-y⌊\frac{x}{y}⌋\right)$$
16	0 15	wceq	$$wff\mathrm{mod}=\left(x\in ℝ,y\in {ℝ}^{+}⟼x-y⌊\frac{x}{y}⌋\right)$$