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.

Ontologie

SUMO / NUMERIC-FUNCTIONS

Class(es)

třída

inheritable relation

binární funkce
is instance of

třída

inheritable relation

relace rozšířená na veličiny
is instance of

remainder fn

Související termín(y)

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

Typy argumentů

veličina RemainderFn(veličina, veličina)

Axiomy (10)

jestliže "greatest common divisor fn()" se rovná number,
potom pro všechny element platí: jestliže element je a member of "()", potom "element mod number" se rovná

(=>
      (equal
            (GreatestCommonDivisorFn @ROW)
            ?NUMBER)
      (forall
            (?ELEMENT)
            (=>
                  (inList
                        ?ELEMENT
                        (ListFn @ROW))
                  (equal
                        (RemainderFn ?ELEMENT ?NUMBER)
                        0))))

jestliže "greatest common divisor fn()" se rovná number,
potom neexistuje greater tak, že greater je větší než number a pro všechny element platí: jestliže element je a member of "()", potom "element mod greater" se rovná

(=>
      (equal
            (GreatestCommonDivisorFn @ROW)
            ?NUMBER)
      (not
            (exists
                  (?GREATER)
                  (and
                        (greaterThan ?GREATER ?NUMBER)
                        (forall
                              (?ELEMENT)
                              (=>
                                    (inList
                                          ?ELEMENT
                                          (ListFn @ROW))
                                    (equal
                                          (RemainderFn ?ELEMENT ?GREATER)
                                          0)))))))

jestliže "least common multiple fn()" se rovná number,
potom pro všechny element platí: jestliže element je a member of "()", potom "number mod element" se rovná

(=>
      (equal
            (LeastCommonMultipleFn @ROW)
            ?NUMBER)
      (forall
            (?ELEMENT)
            (=>
                  (inList
                        ?ELEMENT
                        (ListFn @ROW))
                  (equal
                        (RemainderFn ?NUMBER ?ELEMENT)
                        0))))

jestliže "least common multiple fn()" se rovná number,
potom neexistuje less tak, že less je menší než number a pro všechny element platí: jestliže element je a member of "()", potom "less mod element" se rovná

(=>
      (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" se rovná number tehdy a jen tehdy pokud "(""floor fn(number1/number2)"*number2"+number)" se rovná number1.

(<=>
      (equal
            (RemainderFn ?NUMBER1 ?NUMBER2)
            ?NUMBER)
      (equal
            (AdditionFn
                  (MultiplicationFn
                        (FloorFn
                              (DivisionFn ?NUMBER1 ?NUMBER2))
                        ?NUMBER2)
                  ?NUMBER)
            ?NUMBER1))

Jestliže "number1 mod number2" se rovná number, potom "signum fn(number2)" se rovná "signum fn(number)".

(=>
      (equal
            (RemainderFn ?NUMBER1 ?NUMBER2)
            ?NUMBER)
      (equal
            (SignumFn ?NUMBER2)
            (SignumFn ?NUMBER)))

Jestliže number je instancí třídy sudé celé číslo, potom "number mod " se rovná .

(=>
      (instance ?NUMBER EvenInteger)
      (equal
            (RemainderFn ?NUMBER 2)
            0))

Jestliže number je instancí třídy liché celé číslo, potom "number mod " se rovná .

(=>
      (instance ?NUMBER OddInteger)
      (equal
            (RemainderFn ?NUMBER 2)
            1))

jestliže prime je instancí třídy prvočíslo,
potom pro všechny number platí: jestliže "prime mod number" se rovná , potom number se rovná nebo number se rovná prime

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

Jestliže leap je instancí třídy přestupný rok a leap se rovná "number rok(s)", potom

"number mod " se rovná a "number mod " se nerovná
"number mod " se rovná

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