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, and . 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
Distinct variable group:   ,

Detailed syntax breakdown of Definition df-mod
StepHypRef Expression
1 cmo 9988 . 2
2 vx . . 3
3 vy . . 3
4 cr 7546 . . 3
5 crp 9343 . . 3
62cv 1313 . . . 4
73cv 1313 . . . . 5
8 cdiv 8345 . . . . . . 7
96, 7, 8co 5728 . . . . . 6
10 cfl 9934 . . . . . 6
119, 10cfv 5081 . . . . 5
12 cmul 7552 . . . . 5
137, 11, 12co 5728 . . . 4
14 cmin 7856 . . . 4
156, 13, 14co 5728 . . 3
162, 3, 4, 5, 15cmpo 5730 . 2
171, 16wceq 1314 1
 Colors of variables: wff set class This definition is referenced by:  modqval  9990
 Copyright terms: Public domain W3C validator