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 e. ZZ -> ( 0 < Z <-> 1 <_ Z ) )

Proof

Step Hyp Ref Expression
1 0z
 |-  0 e. ZZ
2 zltp1le
 |-  ( ( 0 e. ZZ /\ Z e. ZZ ) -> ( 0 < Z <-> ( 0 + 1 ) <_ Z ) )
3 1 2 mpan
 |-  ( Z e. ZZ -> ( 0 < Z <-> ( 0 + 1 ) <_ Z ) )
4 0p1e1
 |-  ( 0 + 1 ) = 1
5 4 a1i
 |-  ( Z e. ZZ -> ( 0 + 1 ) = 1 )
6 5 breq1d
 |-  ( Z e. ZZ -> ( ( 0 + 1 ) <_ Z <-> 1 <_ Z ) )
7 3 6 bitrd
 |-  ( Z e. ZZ -> ( 0 < Z <-> 1 <_ Z ) )