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
is instance of

class

inheritable relation

relation extended to quantities
is instance of

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
            (AdditionFn
                  (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))

if prime is an instance of prime number,
then for all number holds: if "prime mod number" is equal to , then number is equal to or number is equal to prime

(=>
      (instance ?PRIME PrimeNumber)
      (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

"number mod " is equal to and "number mod " is not equal to
"number mod " is equal to

(=>
      (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)))