Description: A positive integer is not less than one. (Contributed by NM, 18-Jan-2004) (Revised by Mario Carneiro, 27-May-2016)
Ref | Expression | ||
---|---|---|---|
Assertion | nnnlt1 | |- ( A e. NN -> -. A < 1 ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | nnge1 | |- ( A e. NN -> 1 <_ A ) |
|
2 | 1re | |- 1 e. RR |
|
3 | nnre | |- ( A e. NN -> A e. RR ) |
|
4 | lenlt | |- ( ( 1 e. RR /\ A e. RR ) -> ( 1 <_ A <-> -. A < 1 ) ) |
|
5 | 2 3 4 | sylancr | |- ( A e. NN -> ( 1 <_ A <-> -. A < 1 ) ) |
6 | 1 5 | mpbid | |- ( A e. NN -> -. A < 1 ) |