Zvolte jazyk: english | cesky | deutsch | italiano | simplified chinese | traditional chinese | hindi Koncept: Anglické slovo: Hlavní stránka

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
 třída

inheritable relation

relace rozšířená na veličiny

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)

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

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

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

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

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