SUMO   View all facts   Glossary   Help
Entity > Abstract > Class > Relation > Function > BinaryFunction > RemainderFn
Next BinaryFunctionSecondFn    UpBinaryFunction, RelationExtendedToQuantities    Previous BinaryFunctionRelativeComplementFn   

RemainderFn
subjectfact 
RemainderFndocumentation (RemainderFn ?NUMBER ?DIVISOR) is the remainder of the number ?NUMBER divided by the number ?DIVISOR. The result has the same sign as ?DIVISOR2001-11-30 13:35:11.0
has axiom
(<=>
(equal (RemainderFn ?NUMBER1 ?NUMBER2) ?NUMBER)
(equal (AdditionFn (MultiplicationFn (FloorFn (DivisionFn ?NUMBER1 ?NUMBER2)) ?NUMBER2) ?NUMBER) ?NUMBER1))
2001-11-30 13:35:11.0
has axiom
(=>
(equal (RemainderFn ?NUMBER1 ?NUMBER2) ?NUMBER)
(equal (SignumFn ?NUMBER2) (SignumFn ?NUMBER)))
2001-11-30 13:35:11.0
has axiom
(=>
(instance ?PRIME PrimeNumber)
(forall (?NUMBER)
(=>
(equal (RemainderFn ?PRIME ?NUMBER) 0)
(or
(equal ?NUMBER 1)
(equal ?NUMBER ?PRIME)))))
2001-11-30 13:35:11.0
has axiom
(=>
(instance ?NUMBER EvenInteger)
(equal (RemainderFn ?NUMBER 2) 0))
2001-11-30 13:35:11.0
has axiom
(=>
(instance ?NUMBER OddInteger)
(equal (RemainderFn ?NUMBER 2) 1))
2001-11-30 13:35:11.0
has domain1 Quantity2001-11-30 13:35:11.0
has domain2 Quantity2001-11-30 13:35:11.0
has range Quantity2001-11-30 13:35:11.0
is an instance of BinaryFunction2001-11-30 13:35:11.0
is an instance of RelationExtendedToQuantities2001-11-30 13:35:11.0
BinaryFunctionis first domain of distributes2001-11-30 13:33:43.0
is first domain of identityElement2001-11-30 13:33:43.0
is second domain of distributes2001-11-30 13:33:43.0
Classis third domain of domain2001-11-30 13:33:51.0
is third domain of domainSubclass2001-11-30 13:33:51.0
Abstractis disjoint from Physical2001-11-30 13:33:32.0

Next BinaryFunctionSecondFn    UpBinaryFunction, RelationExtendedToQuantities    Previous BinaryFunctionRelativeComplementFn