# Metamath Proof Explorer

## Theorem fllt

Description: The floor function value is less than the next integer. (Contributed by NM, 24-Feb-2005)

Ref Expression
Assertion fllt ${⊢}\left({A}\in ℝ\wedge {B}\in ℤ\right)\to \left({A}<{B}↔⌊{A}⌋<{B}\right)$

### Proof

Step Hyp Ref Expression
1 flge ${⊢}\left({A}\in ℝ\wedge {B}\in ℤ\right)\to \left({B}\le {A}↔{B}\le ⌊{A}⌋\right)$
2 zre ${⊢}{B}\in ℤ\to {B}\in ℝ$
3 lenlt ${⊢}\left({B}\in ℝ\wedge {A}\in ℝ\right)\to \left({B}\le {A}↔¬{A}<{B}\right)$
4 2 3 sylan ${⊢}\left({B}\in ℤ\wedge {A}\in ℝ\right)\to \left({B}\le {A}↔¬{A}<{B}\right)$
5 4 ancoms ${⊢}\left({A}\in ℝ\wedge {B}\in ℤ\right)\to \left({B}\le {A}↔¬{A}<{B}\right)$
6 reflcl ${⊢}{A}\in ℝ\to ⌊{A}⌋\in ℝ$
7 lenlt ${⊢}\left({B}\in ℝ\wedge ⌊{A}⌋\in ℝ\right)\to \left({B}\le ⌊{A}⌋↔¬⌊{A}⌋<{B}\right)$
8 2 6 7 syl2anr ${⊢}\left({A}\in ℝ\wedge {B}\in ℤ\right)\to \left({B}\le ⌊{A}⌋↔¬⌊{A}⌋<{B}\right)$
9 1 5 8 3bitr3d ${⊢}\left({A}\in ℝ\wedge {B}\in ℤ\right)\to \left(¬{A}<{B}↔¬⌊{A}⌋<{B}\right)$
10 9 con4bid ${⊢}\left({A}\in ℝ\wedge {B}\in ℤ\right)\to \left({A}<{B}↔⌊{A}⌋<{B}\right)$