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

Definition df-mod 9651
Description: Define the modulo (remainder) operation. See modqval 9652 for its value. For example,  ( 5  mod  3 )  =  2 and  ( -u 7  mod  2 )  =  1. As with df-fl 9598 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  =  ( x  e.  RR ,  y  e.  RR+  |->  ( x  -  ( y  x.  ( |_ `  (
x  /  y ) ) ) ) )
Distinct variable group:    x, y

Detailed syntax breakdown of Definition df-mod
StepHypRef Expression
1 cmo 9650 . 2  class  mod
2 vx . . 3  setvar  x
3 vy . . 3  setvar  y
4 cr 7286 . . 3  class  RR
5 crp 9059 . . 3  class  RR+
62cv 1286 . . . 4  class  x
73cv 1286 . . . . 5  class  y
8 cdiv 8071 . . . . . . 7  class  /
96, 7, 8co 5607 . . . . . 6  class  ( x  /  y )
10 cfl 9596 . . . . . 6  class  |_
119, 10cfv 4978 . . . . 5  class  ( |_
`  ( x  / 
y ) )
12 cmul 7292 . . . . 5  class  x.
137, 11, 12co 5607 . . . 4  class  ( y  x.  ( |_ `  ( x  /  y
) ) )
14 cmin 7590 . . . 4  class  -
156, 13, 14co 5607 . . 3  class  ( x  -  ( y  x.  ( |_ `  (
x  /  y ) ) ) )
162, 3, 4, 5, 15cmpt2 5609 . 2  class  ( x  e.  RR ,  y  e.  RR+  |->  ( x  -  ( y  x.  ( |_ `  (
x  /  y ) ) ) ) )
171, 16wceq 1287 1  wff  mod  =  ( x  e.  RR ,  y  e.  RR+  |->  ( x  -  ( y  x.  ( |_ `  (
x  /  y ) ) ) ) )
Colors of variables: wff set class
This definition is referenced by:  modqval  9652
  Copyright terms: Public domain W3C validator