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

Kategorie

inheritable relation

zweistellige Funktion
is instance of

Kategorie

inheritable relation

Relation erweitert auf Quantitäten
is instance of

RestFn

Coordinate term(s)

AdditionFn TagFn DichteFn DivisionFn AusgabeFn ExponentiationFn GraphPfadFn StundeFn DurchschnittFn AbstandFn KappaFn ListeVerkettenFn ListeOrdnungFn LogarithmusFn MaximumFn MaximalerBelasteterPfadFn MassFn MereologischeDifferenzFn MereologischesProduktFn MereologischeSummeFn MinumumFn MinimalerBelasteterPfadFn MinuteFn MonatFn MultiplikationFn PeriodikumAusgabeFn ReziprokerWert RückläufigeZeitAbstandFn RelativeErgänzungFn RelativeZeitFn RundFn SekundFn ReiheBandeFn GeschwindigkeitFn SubtraktionFn ZeitlicheAufbauFn ZeitabstandFn VereinigungFn WoFn %1 ist gleich %2 %n{nicht} grösserAls grösserAlsOderGleich kleinerAls kleinerAlsOderGleich

Type restrictions

Eigenschaft RemainderFn(Eigenschaft, Eigenschaft)

Axioms (10)

wenn "die größte gemeinsamer teiler von " ist gleich number ,
dann für jeden element gilt: wenn element ist ein Mitglied von "()", dann "element betrag number" ist gleich

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

wenn "die größte gemeinsamer teiler von " ist gleich number ,
dann es gibt kein greater der greater ist grösserAls number und für jeden element gilt: wenn element ist ein Mitglied von "()", dann "element betrag greater" ist gleich

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

wenn "das kleinste gemeinsames vielfach von " ist gleich number ,
dann für jeden element gilt: wenn element ist ein Mitglied von "()", dann "number betrag element" ist gleich

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

wenn "das kleinste gemeinsames vielfach von " ist gleich number ,
dann es gibt kein less der less ist kleinerAls number und für jeden element gilt: wenn element ist ein Mitglied von "()", dann "less betrag element" ist gleich

(=>
      (equal
            (LeastCommonMultipleFn @ROW)
            ?NUMBER)
      (not
            (exists
                  (?LESS)
                  (and
                        (lessThan ?LESS ?NUMBER)
                        (forall
                              (?ELEMENT)
                              (=>
                                    (inList
                                          ?ELEMENT
                                          (ListFn @ROW))
                                    (equal
                                          (RemainderFn ?LESS ?ELEMENT)
                                          0)))))))

"number1 betrag number2" ist gleich number nur wenn "(""die grösste Ganzzahl kleiner als oder Gleichgestelltes zu "number1/number2""*number2"+number)" ist gleich number1 .

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

Wenn "number1 betrag number2" ist gleich number , dann "das zeichen von number2" ist gleich "das zeichen von number" .

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

Wenn number ist ein fall von gerade Ganzzahl , dann "number betrag " ist gleich .

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

Wenn number ist ein fall von ungerade Ganzzahl , dann "number betrag " ist gleich .

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

wenn prime ist ein fall von Hauptzahl ,
dann für jeden number gilt: wenn "prime betrag number" ist gleich , dann number ist gleich oder number ist gleich prime

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

Wenn leap ist ein fall von Schaltjahr und leap ist gleich "number Jahr(s)" , dann

"number betrag " ist gleich und "number betrag " ist gleich nicht
"number betrag " ist gleich

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