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 ( 𝑍 ∈ ℤ → ( 0 < 𝑍 ↔ 1 ≤ 𝑍 ) )

Proof

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