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

Definition df-mod 9405
Description: Define the modulo (remainder) operation. See modqval 9406 for its value. For example,  ( 5  mod  3 )  =  2 and  ( -u 7  mod  2 )  =  1. As with df-fl 9352 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 9404 . 2  class  mod
2 vx . . 3  setvar  x
3 vy . . 3  setvar  y
4 cr 7042 . . 3  class  RR
5 crp 8815 . . 3  class  RR+
62cv 1284 . . . 4  class  x
73cv 1284 . . . . 5  class  y
8 cdiv 7827 . . . . . . 7  class  /
96, 7, 8co 5543 . . . . . 6  class  ( x  /  y )
10 cfl 9350 . . . . . 6  class  |_
119, 10cfv 4932 . . . . 5  class  ( |_
`  ( x  / 
y ) )
12 cmul 7048 . . . . 5  class  x.
137, 11, 12co 5543 . . . 4  class  ( y  x.  ( |_ `  ( x  /  y
) ) )
14 cmin 7346 . . . 4  class  -
156, 13, 14co 5543 . . 3  class  ( x  -  ( y  x.  ( |_ `  (
x  /  y ) ) ) )
162, 3, 4, 5, 15cmpt2 5545 . 2  class  ( x  e.  RR ,  y  e.  RR+  |->  ( x  -  ( y  x.  ( |_ `  (
x  /  y ) ) ) ) )
171, 16wceq 1285 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  9406
  Copyright terms: Public domain W3C validator