**Description:** The number 7 is positive. (Contributed by NM, 27-May-1999)

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

Assertion | 7pos | ⊢ 0 < 7 |

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

1 | 6re | ⊢ 6 ∈ ℝ | |

2 | 1re | ⊢ 1 ∈ ℝ | |

3 | 6pos | ⊢ 0 < 6 | |

4 | 0lt1 | ⊢ 0 < 1 | |

5 | 1 2 3 4 | addgt0ii | ⊢ 0 < ( 6 + 1 ) |

6 | df-7 | ⊢ 7 = ( 6 + 1 ) | |

7 | 5 6 | breqtrri | ⊢ 0 < 7 |