Theorem btwnzge0

Description: A real bounded between an integer and its successor is nonnegative iff the integer is nonnegative. Second half of Lemma 13-4.1 of Gleason p. 217. (For the first half see rebtwnz .) (Contributed by NM, 12-Mar-2005)

	Ref	Expression
Assertion	btwnzge0	|- ( ( ( A e. RR /\ N e. ZZ ) /\ ( N <_ A /\ A < ( N + 1 ) ) ) -> ( 0 <_ A <-> 0 <_ N ) )

Proof

Step	Hyp	Ref	Expression
1		0z	|- 0 e. ZZ
2		flge	|- ( ( A e. RR /\ 0 e. ZZ ) -> ( 0 <_ A <-> 0 <_ ( |_ ` A ) ) )
3	1 2	mpan2	|- ( A e. RR -> ( 0 <_ A <-> 0 <_ ( |_ ` A ) ) )
4	3	ad2antrr	|- ( ( ( A e. RR /\ N e. ZZ ) /\ ( N <_ A /\ A < ( N + 1 ) ) ) -> ( 0 <_ A <-> 0 <_ ( |_ ` A ) ) )
5		flbi	|- ( ( A e. RR /\ N e. ZZ ) -> ( ( |_ ` A ) = N <-> ( N <_ A /\ A < ( N + 1 ) ) ) )
6	5	biimpar	|- ( ( ( A e. RR /\ N e. ZZ ) /\ ( N <_ A /\ A < ( N + 1 ) ) ) -> ( |_ ` A ) = N )
7	6	breq2d	|- ( ( ( A e. RR /\ N e. ZZ ) /\ ( N <_ A /\ A < ( N + 1 ) ) ) -> ( 0 <_ ( |_ ` A ) <-> 0 <_ N ) )
8	4 7	bitrd	|- ( ( ( A e. RR /\ N e. ZZ ) /\ ( N <_ A /\ A < ( N + 1 ) ) ) -> ( 0 <_ A <-> 0 <_ N ) )