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