# Properties of Floor Function

## Theorem

### Floor is between Number and One Less

$x - 1 < \left\lfloor{x}\right\rfloor \le x$

where $\left\lfloor{x}\right\rfloor$ is the floor of $x$.

### Floor of Number plus Integer

$\forall n \in \Z: \floor x + n = \floor {x + n}$

### Real Number minus Floor

$x - \floor x \in \hointr 0 1$

### Real Number is between Floor Functions

$\forall x \in \R: \floor x \le x < \floor {x + 1}$

### Real Number is Floor plus Difference

There exists an integer $n \in \Z$ such that for some $t \in \hointr 0 1$:
$x = n + t$
$n = \floor x$

### Floor Function is Idempotent

$\floor {\floor x} = \floor x$

## Range of Values of Floor Function

### Number less than Integer iff Floor less than Integer

$\left \lfloor{x}\right \rfloor < n \iff x < n$

### Number not less than Integer iff Floor not less than Integer

$x \ge n \iff \left \lfloor{x}\right \rfloor \ge n$

### Integer equals Floor iff between Number and One Less

$\floor x = n \iff x - 1 < n \le x$

### Integer equals Floor iff Number between Integer and One More

$\left \lfloor{x}\right \rfloor = n \iff n \le x < n + 1$