**Description:** 4 is a positive integer. (Contributed by NM, 8-Jan-2006)

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

Assertion | 4nn | $${\u22a2}4\in \mathbb{N}$$ |

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

1 | df-4 | $${\u22a2}4=3+1$$ | |

2 | 3nn | $${\u22a2}3\in \mathbb{N}$$ | |

3 | peano2nn | $${\u22a2}3\in \mathbb{N}\to 3+1\in \mathbb{N}$$ | |

4 | 2 3 | ax-mp | $${\u22a2}3+1\in \mathbb{N}$$ |

5 | 1 4 | eqeltri | $${\u22a2}4\in \mathbb{N}$$ |