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	$⊢ \mod = (x \in ℝ, y \in ℝ^{+} ⟼ x - y ⌊\frac{x}{y}⌋)$

Detailed syntax breakdown

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

Metamath Proof Explorer

Definition df-mod

Detailed syntax breakdown