This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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