# Proof involving Floor function

Prove: $\forall l \in \mathbb{Z}: \forall r \in \mathbb{R}: 0 \le r \lt 1 \Rightarrow\lfloor l+r\rfloor = l$

My attempt:

Let: $l \in \mathbb{Z}, r \in \mathbb{R}.$

Assume: $0 \le r \lt 1.$

$\lfloor l + r \rfloor \le \lfloor l \rfloor + \lfloor r \rfloor = \lfloor l \rfloor + 0$, since $0 \le r \lt 1$.

$\lfloor l \rfloor + 0 = l$, since $l \in \mathbb{Z}$

Is that correct? This is for a beginners' proofs course.

• An approach you could take is to show that $l \leq (l +r) < l+1$ – Nicholas Nov 13 '15 at 8:32
• Your approach is totally right. – SchrodingersCat Nov 13 '15 at 8:41
• you've not proved $l\le\lfloor l+r\rfloor$ – JMP Nov 13 '15 at 8:42
• @JonMarkPerry if I change the <= sign to an = sign, would the proof be correct? i.e. $\lfloor l + r \rfloor = \lfloor l \rfloor + \lfloor r \rfloor = ...$ – player87 Nov 13 '15 at 17:31
• @MarnixKlooster Assumptions 1: $$\forall x \in R: \lfloor x \rfloor \in Z \wedge \lfloor x \rfloor \le x \wedge [\forall z \in Z: z \le x \Rightarrow z \le \lfloor x \rfloor]$$ Assmpt. 2: $$\forall x \in R: \forall y \in Z: [y \le x \wedge [\forall z \in Z: z \le x \Rightarrow z \le y]] \Rightarrow y = \lfloor x \rfloor$$ – player87 Nov 14 '15 at 17:16

Correctness depends on the properties of $\;\lfloor \cdots \rfloor\;$ that you are allowed to use. Since you gave none, let me use the following definition: for every real $\;x, y\;$, $$\tag{0} \lfloor x \rfloor = y \;\;\equiv\;\; 0 \le x - y \lt 1 \;\land\; y \in \mathbb Z$$

\newcommand{\calc}{\begin{align} \quad &} \newcommand{\op}{\\ #1 \quad & \quad \unicode{x201c}} \newcommand{\hints}{\mbox{#1} \\ \quad & \quad \phantom{\unicode{x201c}} } \newcommand{\hint}{\mbox{#1} \unicode{x201d} \\ \quad & } \newcommand{\then}{\Rightarrow} \newcommand{\when}{\Leftarrow} \newcommand{\endcalc}{\end{align}} \newcommand{\ref}{\text{(#1)}}Now, for any real $\;l,r\;$, let's see if we can use this definition to simplify $\;\lfloor l + r \rfloor = l\;$: $$\calc \tag 1 \lfloor l + r \rfloor = l \op=\hint{definition \ref 0 with \;x,y := l+r, l\;} 0 \le l+r - l \lt 1 \;\land\; l \in \mathbb Z \op=\hint{arithmetic: simplify} \tag 2 0 \le r \lt 1 \;\land\; l \in \mathbb Z \endcalc$$ This immediately proves the original statement, which says that $\ref 2$ implies $\ref 1$.

Update. In the comments you now specified that, instead, your basic properties/assumptions are the following, for real $\;x\;$ and for $\;n \in \mathbb Z\;$: \begin{align} \tag{A1a} & \lfloor x \rfloor \in \mathbb Z \\ \tag{A1b} & \lfloor x \rfloor \le x \\ \tag{A1c} & n \le x \;\then\; n \le \lfloor x \rfloor \\ \tag{A2} & n \le x \land \langle \forall z : z \in \mathbb Z : z \le x \then z \le n \rangle \;\then\; n = \lfloor x \rfloor \end{align} (Apologies for switching to a slightly different notation, which I am more used to, and which I feel focuses on the essentials. See EWD1300 for more details.)

Now one way to prove the original statement, is to again start with the main part that we're to prove: $$\calc \lfloor l + r \rfloor = l \op\when\hints{using \ref{A2} using \;l \in \mathbb Z\;} \hint{-- this seems the only assumption directly applicable} l \le l + r \;\land\; \langle \forall z : z \in \mathbb Z : z \le l + r \then z \le l \rangle \op=\hint{LHS: simplify by subtracting \;l\;; RHS: substitute \;z := z + l\;} 0 \le r \;\land\; \langle \forall z : z \in \mathbb Z : z + l \le l + r \then z + l \le l \rangle \op=\hint{RHS: simplify by subtracting \;l\;; contraposition} 0 \le r \;\land\; \langle \forall z : z \in \mathbb Z : z \gt 0 \then z \gt r \rangle \op=\hint{RHS: ordering} 0 \le r \;\land\; r < 1 \endcalc$$ Note that we did not need to use any part of assumption 1.

Now you should try to take the proof from your question, together with Jon Mark Perry's suggestion, and write it in the above format: this forces you to add an explicit justification for each step.

However, be warned that the property $\;\lfloor x + y \rfloor \;\le\; \lfloor x \rfloor + \lfloor y \rfloor\;$ does not hold in general for all real $\;x,y\;$: e.g., $\;\lfloor \tfrac 1 2 + \tfrac 1 2 \rfloor \;=\; 1 \;>\; 0 \;=\; \lfloor \tfrac 1 2 \rfloor + \lfloor \tfrac 1 2 \rfloor\;$. Instead property $\ref 5$ below does hold.

Also, note that you would only be allowed to use the following properties, if you can prove them from $\ref{A1a}$, $\ref{A1b}$, $\ref{A1c}$, and $\ref{A2}$, for real $\;x,y\;$ and $\;n \in \mathbb Z\;$: \begin{align} \tag{3} & \lfloor n \rfloor \;=\; n \\ \tag{4} & x \le y \;\then\; \lfloor x \rfloor \le \lfloor y \rfloor \\ \tag{5} & \lfloor x \rfloor + \lfloor y \rfloor \;\le\; \lfloor x + y \rfloor \\ \tag{6} & 0 \le x \lt 1 \;\then\; \lfloor x \rfloor = 0 \\ \end{align}

• Assmpt. 1: $$\forall x \in R: \lfloor x \rfloor \in Z \wedge \lfloor x \rfloor \le x \wedge [\forall z \in Z: z \le x \Rightarrow z \le \lfloor x \rfloor]$$ Assmpt. 2: $$\forall x \in R: \forall y \in Z: [y \le x \wedge [\forall z \in Z: z \le x \Rightarrow z \le y]] \Rightarrow y = \lfloor x \rfloor$$ I basically showed that l+r = x and l = y = z. Then I "brought in" the assumption into the proof and showed that y = l = $\lfloor$ x $\rfloor$ = $\lfloor$ l + r $\rfloor$. Does that sound right? – player87 Nov 14 '15 at 17:13

Let $x=l+r$. Since $r \ge 0$ we have $l \le l+r=x$ and, since $r<1$ we have $x=l+r<l+r+(1-r)=l+1$.

Now use the fact that: $$\forall l \in \mathbb{Z} \qquad \lfloor x \rfloor=l \iff l\le x\lt l+1$$ that can be easily proved by the definition:

$$\lfloor x \rfloor= \mbox{Max}\{n\in \mathbb{Z}, n\le x \}$$

• If the OP wants to use the fact that you gave, then I'd suggest to use it directly, by writing down your proof as follows:$\newcommand{\Xop}{\\ #1 \quad & \quad \unicode{x201c}} \newcommand{\Xhi}{\mbox{#1} \unicode{x201d} \\ \quad & }$ for every $\;l \in \mathbb Z\;$ and real $\;r\;$,\begin{align} \quad &\lfloor l + r \rfloor = l\Xop=\Xhi{using your fact, and the assumption that \;l \in \mathbb Z\;}l \le l+r \lt l+1\Xop=\Xhi{arithmetic: simplify by subtracting \;l\;}0 \le r \lt 1\end{align} – MarnixKlooster ReinstateMonica Nov 14 '15 at 14:01