Theorem znnnlt1

Description: An integer is not a positive integer iff it is less than one. (Contributed by NM, 13-Jul-2005)

	Ref	Expression
Assertion	znnnlt1	|- ( N e. ZZ -> ( -. N e. NN <-> N < 1 ) )

Proof

Step	Hyp	Ref	Expression
1		elnnz1	|- ( N e. NN <-> ( N e. ZZ /\ 1 <_ N ) )
2	1	baib	|- ( N e. ZZ -> ( N e. NN <-> 1 <_ N ) )
3	2	notbid	|- ( N e. ZZ -> ( -. N e. NN <-> -. 1 <_ N ) )
4		zre	|- ( N e. ZZ -> N e. RR )
5		1re	|- 1 e. RR
6		ltnle	|- ( ( N e. RR /\ 1 e. RR ) -> ( N < 1 <-> -. 1 <_ N ) )
7	4 5 6	sylancl	|- ( N e. ZZ -> ( N < 1 <-> -. 1 <_ N ) )
8	3 7	bitr4d	|- ( N e. ZZ -> ( -. N e. NN <-> N < 1 ) )