*RemainderFn* | *documentation* (*RemainderFn* ?NUMBER ?DIVISOR) is the remainder of the number ?NUMBER divided by the number ?DIVISOR. The result has the same sign as ?DIVISOR | |

**has axiom** (*<=>* (*equal* (*RemainderFn* ?NUMBER1 ?NUMBER2) ?NUMBER) (*equal* (*AdditionFn* (*MultiplicationFn* (*FloorFn* (*DivisionFn* ?NUMBER1 ?NUMBER2)) ?NUMBER2) ?NUMBER) ?NUMBER1))
| |

**has axiom** (=> (*equal* (*RemainderFn* ?NUMBER1 ?NUMBER2) ?NUMBER) (*equal* (*SignumFn* ?NUMBER2) (*SignumFn* ?NUMBER)))
| |

**has axiom** (=> (*instance* ?PRIME PrimeNumber) (forall (?NUMBER) (=> (*equal* (*RemainderFn* ?PRIME ?NUMBER) 0) (or (*equal* ?NUMBER 1) (*equal* ?NUMBER ?PRIME)))))
| |

**has axiom** (=> (*instance* ?NUMBER EvenInteger) (*equal* (*RemainderFn* ?NUMBER 2) 0))
| |

**has axiom** (=> (*instance* ?NUMBER OddInteger) (*equal* (*RemainderFn* ?NUMBER 2) 1))
| |

**has domain1** Quantity | |

**has domain2** Quantity | |

**has ***range* Quantity | |

**is an ***instance* of BinaryFunction | |

**is an ***instance* of RelationExtendedToQuantities | |

BinaryFunction | **is first ***domain* of *distributes* | |

**is first ***domain* of *identityElement* | |

**is second ***domain* of *distributes* | |

Class | **is third ***domain* of *domain* | |

**is third ***domain* of *domainSubclass* | |

Abstract | **is ***disjoint* from Physical | |