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