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)

varga

inheritable relation

dvi-aadhaary prakaarya
is instance of

varga

inheritable relation

matraaon kaa sanbandha vistaara
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

parimaaNa RemainderFn(parimaaNa, parimaaNa)

Axioms (10)

agar "the greatest common divisor of " is equal to number,
to sab-kuch element ke lie hai, ki: agar element is a member of "()", to "element mod number" is equal to

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

agar "the greatest common divisor of " is equal to number,
to yah kuch greater nahin, ki greater is greater than number aur sab-kuch element ke lie hai, ki: agar element is a member of "()", to "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)))))))

agar "the least common multiple of " is equal to number,
to sab-kuch element ke lie hai, ki: agar element is a member of "()", to "number mod element" is equal to

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

agar "the least common multiple of " is equal to number,
to yah kuch less nahin, ki less is less than number aur sab-kuch element ke lie hai, ki: agar element is a member of "()", to "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 agar hai "(""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))

Agar "number1 mod number2" is equal to number, to "the sign of number2" is equal to "the sign of number".

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

Agar number is an instance of sama pUrNaanka, to "number mod " is equal to .

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

Agar number is an instance of visham pUrNaanka, to "number mod " is equal to .

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

agar prime is an instance of abhaajya anka,
to sab-kuch number ke lie hai, ki: agar "prime mod number" is equal to , to number is equal to yaa number is equal to prime

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

Agar leap is an instance of adhivarsha aur leap is equal to "number varsha(s)", to

"number mod " is equal to aur "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)))