Integer | *documentation* A negative or nonnegative whole number | |

**has axiom** (=> (*instance* ?SEQ SequenceFunction) (*subclass* (*RangeFn* ?SEQ) Integer))
| |

**has axiom** (=> (*and* (*instance* ?INT1 Integer) (*instance* ?INT2 Integer)) (*not* (*and* (*lessThan* ?INT1 ?INT2) (*lessThan* ?INT2 (*SuccessorFn* ?INT1)))))
| |

**has axiom** (=> (*and* (*instance* ?INT1 Integer) (*instance* ?INT2 Integer)) (*not* (*and* (*lessThan* ?INT2 ?INT1) (*lessThan* (*PredecessorFn* ?INT1) ?INT2))))
| |

**has axiom** (=> (*equal* (*CeilingFn* ?NUMBER) ?INT) (*not* (exists (?OTHERINT) (*and* (*instance* ?OTHERINT Integer) (*greaterThanOrEqualTo* ?OTHERINT ?NUMBER) (*lessThan* ?OTHERINT ?INT)))))
| |

**has axiom** (=> (*equal* (*FloorFn* ?NUMBER) ?INT) (*not* (exists (?OTHERINT) (*and* (*instance* ?OTHERINT Integer) (*lessThanOrEqualTo* ?OTHERINT ?NUMBER) (*greaterThan* ?OTHERINT ?INT)))))
| |

**has axiom** (=> (*instance* ?INT Integer) (*equal* ?INT (*SuccessorFn* (*PredecessorFn* ?INT))))
| |

**has axiom** (=> (*instance* ?INT Integer) (*equal* ?INT (*PredecessorFn* (*SuccessorFn* ?INT))))
| |

**has axiom** (=> (*instance* ?INT Integer) (*greaterThan* ?INT (*PredecessorFn* ?INT)))
| |

**has axiom** (=> (*instance* ?INT Integer) (*lessThan* ?INT (*SuccessorFn* ?INT)))
| |

**has axiom** (=> (*instance* ?NUMBER RationalNumber) (exists (?INT1 ?INT2) (*and* (*instance* ?INT1 Integer) (*instance* ?INT2 Integer) (*equal* ?NUMBER (*DivisionFn* ?INT1 ?INT2)))))
| |

**is first ***domain* of *PredecessorFn* | |

**is first ***domain* of *SuccessorFn* | |

**is first ***domain* of *YearFn* | |

**is second ***domain* of *ExponentiationFn* | |

**is second ***domain* of *singleValued* | |

**is partitioned into** NegativeInteger, NonnegativeInteger | |

**is partitioned into** OddInteger, EvenInteger | |

**is a kind of** RationalNumber | |

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