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 ) )