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∈ℝ∧N∈ℤ∧N≤A∧A<N+1→0≤A↔0≤N

Proof

Step Hyp Ref Expression
1 0z ⊢0∈ℤ
2 flge ⊢A∈ℝ∧0∈ℤ→0≤A↔0≤A
3 1 2 mpan2 ⊢A∈ℝ→0≤A↔0≤A
4 3 ad2antrr ⊢A∈ℝ∧N∈ℤ∧N≤A∧A<N+1→0≤A↔0≤A
5 flbi ⊢A∈ℝ∧N∈ℤ→A=N↔N≤A∧A<N+1
6 5 biimpar ⊢A∈ℝ∧N∈ℤ∧N≤A∧A<N+1→A=N
7 6 breq2d ⊢A∈ℝ∧N∈ℤ∧N≤A∧A<N+1→0≤A↔0≤N
8 4 7 bitrd ⊢A∈ℝ∧N∈ℤ∧N≤A∧A<N+1→0≤A↔0≤N