Metamath Proof Explorer

Theorem zgt0ge1

Description: An integer greater than 0 is greater than or equal to 1 . (Contributed by AV, 14-Oct-2018)

Ref Expression
Assertion zgt0ge1 ⊢ Z ∈ ℤ → 0 < Z ↔ 1 ≤ Z

Proof

Step Hyp Ref Expression
1 0z ⊢ 0 ∈ ℤ
2 zltp1le ⊢ 0 ∈ ℤ ∧ Z ∈ ℤ → 0 < Z ↔ 0 + 1 ≤ Z
3 1 2 mpan ⊢ Z ∈ ℤ → 0 < Z ↔ 0 + 1 ≤ Z
4 0p1e1 ⊢ 0 + 1 = 1
5 4 a1i ⊢ Z ∈ ℤ → 0 + 1 = 1
6 5 breq1d ⊢ Z ∈ ℤ → 0 + 1 ≤ Z ↔ 1 ≤ Z
7 3 6 bitrd ⊢ Z ∈ ℤ → 0 < Z ↔ 1 ≤ Z