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

Definition df-mod 9989
Description: Define the modulo (remainder) operation. See modqval 9990 for its value. For example,  ( 5  mod  3 )  =  2 and  ( -u 7  mod  2 )  =  1. As with df-fl 9936 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 9988 . 2  class  mod
2 vx . . 3  setvar  x
3 vy . . 3  setvar  y
4 cr 7546 . . 3  class  RR
5 crp 9343 . . 3  class  RR+
62cv 1313 . . . 4  class  x
73cv 1313 . . . . 5  class  y
8 cdiv 8345 . . . . . . 7  class  /
96, 7, 8co 5728 . . . . . 6  class  ( x  /  y )
10 cfl 9934 . . . . . 6  class  |_
119, 10cfv 5081 . . . . 5  class  ( |_
`  ( x  / 
y ) )
12 cmul 7552 . . . . 5  class  x.
137, 11, 12co 5728 . . . 4  class  ( y  x.  ( |_ `  ( x  /  y
) ) )
14 cmin 7856 . . . 4  class  -
156, 13, 14co 5728 . . 3  class  ( x  -  ( y  x.  ( |_ `  (
x  /  y ) ) ) )
162, 3, 4, 5, 15cmpo 5730 . 2  class  ( x  e.  RR ,  y  e.  RR+  |->  ( x  -  ( y  x.  ( |_ `  (
x  /  y ) ) ) ) )
171, 16wceq 1314 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  9990
  Copyright terms: Public domain W3C validator