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