SUMO   View all facts   Glossary   Help

Entity > Abstract > Class > Relation > Function > BinaryFunction > RemainderFn

RemainderFn
subject			fact

RemainderFn	documentation (RemainderFn ?NUMBER ?DIVISOR) is the remainder of the number ?NUMBER divided by the number ?DIVISOR. The result has the same sign as ?DIVISOR
	has axiom (<=> (equal (RemainderFn ?NUMBER1 ?NUMBER2) ?NUMBER) (equal (AdditionFn (MultiplicationFn (FloorFn (DivisionFn ?NUMBER1 ?NUMBER2)) ?NUMBER2) ?NUMBER) ?NUMBER1))
	has axiom (=> (equal (RemainderFn ?NUMBER1 ?NUMBER2) ?NUMBER) (equal (SignumFn ?NUMBER2) (SignumFn ?NUMBER)))
	has axiom (=> (instance ?PRIME PrimeNumber) (forall (?NUMBER) (=> (equal (RemainderFn ?PRIME ?NUMBER) 0) (or (equal ?NUMBER 1) (equal ?NUMBER ?PRIME)))))
	has axiom (=> (instance ?NUMBER EvenInteger) (equal (RemainderFn ?NUMBER 2) 0))
	has axiom (=> (instance ?NUMBER OddInteger) (equal (RemainderFn ?NUMBER 2) 1))
	has domain1 Quantity
	has domain2 Quantity
	has range Quantity
	is an instance of BinaryFunction
	is an instance of RelationExtendedToQuantities
BinaryFunction	is first domain of distributes
	is first domain of identityElement
	is second domain of distributes
Class	is third domain of domain
	is third domain of domainSubclass
Abstract	is disjoint from Physical

Next BinaryFunction: SecondFn    Up: BinaryFunction, RelationExtendedToQuantities    Previous BinaryFunction: RelativeComplementFn