Select language: english | cesky | deutsch | italiano | simplified chinese | traditional chinese | hindi Concept: English word: Home

# remainder fn (RemainderFn)

(RemainderFn number divisor) is the remainder of the number number divided by the number divisor. The result has the same sign as divisor.

## Ontology

SUMO / NUMERIC-FUNCTIONS

## Class(es)

 class

inheritable relation

binary function
 class

inheritable relation

relation extended to quantities

remainder fn

## Coordinate term(s)

addition fn  day fn  density fn  division fn  edition fn  exponentiation fn  graph path fn  hour fn  intersection fn  interval fn  kappa fn  list concatenate fn  list order fn  log fn  max fn  maximal weighted path fn  measure fn  mereological difference fn  mereological product fn  mereological sum fn  min fn  minimal weighted path fn  minute fn  month fn  multiplication fn  periodical issue fn  reciprocal fn  recurrent time interval fn  relative complement fn  relative time fn  round fn  second fn  series volume fn  speed fn  subtraction fn  temporal composition fn  time interval fn  union fn  where fn  equal  greater than  greater than or equal to  less than  less than or equal to

## Type restrictions

quantity RemainderFn(quantity, quantity)

## Axioms (10)

• if "the greatest common divisor of " is equal to number,
• then for all element holds: if element is a member of "()", then "element mod number" is equal to
• .
```(=>
(equal
(GreatestCommonDivisorFn @ROW)
?NUMBER)
(forall
(?ELEMENT)
(=>
(inList
?ELEMENT
(ListFn @ROW))
(equal
(RemainderFn ?ELEMENT ?NUMBER)
0))))```

• if "the greatest common divisor of " is equal to number,
• then there doesn't exist greater so that greater is greater than number and for all element holds: if element is a member of "()", then "element mod greater" is equal to
• .
```(=>
(equal
(GreatestCommonDivisorFn @ROW)
?NUMBER)
(not
(exists
(?GREATER)
(and
(greaterThan ?GREATER ?NUMBER)
(forall
(?ELEMENT)
(=>
(inList
?ELEMENT
(ListFn @ROW))
(equal
(RemainderFn ?ELEMENT ?GREATER)
0)))))))```

• if "the least common multiple of " is equal to number,
• then for all element holds: if element is a member of "()", then "number mod element" is equal to
• .
```(=>
(equal
(LeastCommonMultipleFn @ROW)
?NUMBER)
(forall
(?ELEMENT)
(=>
(inList
?ELEMENT
(ListFn @ROW))
(equal
(RemainderFn ?NUMBER ?ELEMENT)
0))))```

• if "the least common multiple of " is equal to number,
• then there doesn't exist less so that less is less than number and for all element holds: if element is a member of "()", then "less mod element" is equal to
• .
```(=>
(equal
(LeastCommonMultipleFn @ROW)
?NUMBER)
(not
(exists
(?LESS)
(and
(lessThan ?LESS ?NUMBER)
(forall
(?ELEMENT)
(=>
(inList
?ELEMENT
(ListFn @ROW))
(equal
(RemainderFn ?LESS ?ELEMENT)
0)))))))```

"number1 mod number2" is equal to number if and only if "(""the largest integer less than or equal to "number1/number2""*number2"+number)" is equal to number1.
```(<=>
(equal
(RemainderFn ?NUMBER1 ?NUMBER2)
?NUMBER)
(equal
(MultiplicationFn
(FloorFn
(DivisionFn ?NUMBER1 ?NUMBER2))
?NUMBER2)
?NUMBER)
?NUMBER1))```

If "number1 mod number2" is equal to number, then "the sign of number2" is equal to "the sign of number".
```(=>
(equal
(RemainderFn ?NUMBER1 ?NUMBER2)
?NUMBER)
(equal
(SignumFn ?NUMBER2)
(SignumFn ?NUMBER)))```

If number is an instance of even integer, then "number mod " is equal to .
```(=>
(instance ?NUMBER EvenInteger)
(equal
(RemainderFn ?NUMBER 2)
0))```

If number is an instance of odd integer, then "number mod " is equal to .
```(=>
(instance ?NUMBER OddInteger)
(equal
(RemainderFn ?NUMBER 2)
1))```

```(=>
(forall
(?NUMBER)
(=>
(equal
(RemainderFn ?PRIME ?NUMBER)
0)
(or
(equal ?NUMBER 1)
(equal ?NUMBER ?PRIME)))))```

If leap is an instance of leap year and leap is equal to "number year(s)", then
```(=>
(and
(instance ?LEAP LeapYear)
(equal
?LEAP
(MeasureFn ?NUMBER Year)))
(or
(and
(equal
(RemainderFn ?NUMBER 4)
0)
(not
(equal
(RemainderFn ?NUMBER 100)
0)))
(equal
(RemainderFn ?NUMBER 400)
0)))```