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

Definition df-mod 10340
Description: Define the modulo (remainder) operation. See modqval 10341 for its value. For example,  ( 5  mod  3 )  =  2 and  ( -u 7  mod  2 )  =  1. As with df-fl 10287 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 10339 . 2  class  mod
2 vx . . 3  setvar  x
3 vy . . 3  setvar  y
4 cr 7827 . . 3  class  RR
5 crp 9670 . . 3  class  RR+
62cv 1362 . . . 4  class  x
73cv 1362 . . . . 5  class  y
8 cdiv 8646 . . . . . . 7  class  /
96, 7, 8co 5890 . . . . . 6  class  ( x  /  y )
10 cfl 10285 . . . . . 6  class  |_
119, 10cfv 5230 . . . . 5  class  ( |_
`  ( x  / 
y ) )
12 cmul 7833 . . . . 5  class  x.
137, 11, 12co 5890 . . . 4  class  ( y  x.  ( |_ `  ( x  /  y
) ) )
14 cmin 8145 . . . 4  class  -
156, 13, 14co 5890 . . 3  class  ( x  -  ( y  x.  ( |_ `  (
x  /  y ) ) ) )
162, 3, 4, 5, 15cmpo 5892 . 2  class  ( x  e.  RR ,  y  e.  RR+  |->  ( x  -  ( y  x.  ( |_ `  (
x  /  y ) ) ) ) )
171, 16wceq 1363 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  10341
  Copyright terms: Public domain W3C validator