**Description:** -1 is an integer. (Contributed by David A. Wheeler, 5-Dec-2018)

Ref | Expression | ||
---|---|---|---|

Assertion | neg1z | $${\u22a2}-1\in \mathbb{Z}$$ |

Step | Hyp | Ref | Expression |
---|---|---|---|

1 | 1nn | $${\u22a2}1\in \mathbb{N}$$ | |

2 | nnnegz | $${\u22a2}1\in \mathbb{N}\to -1\in \mathbb{Z}$$ | |

3 | 1 2 | ax-mp | $${\u22a2}-1\in \mathbb{Z}$$ |