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 ( ( ( 𝐴 ∈ ℝ ∧ 𝑁 ∈ ℤ ) ∧ ( 𝑁 ≤ 𝐴 ∧ 𝐴 < ( 𝑁 + 1 ) ) ) → ( 0 ≤ 𝐴 ↔ 0 ≤ 𝑁 ) )

Proof

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