If $x>y$, then $\lfloor x\rfloor\ge \lfloor y\rfloor$, formal proof

Question

For x ∈ ℝ, define by: ⌊x⌋ ∈ ℤ ∧ ⌊x⌋ ≤ x ∧ (∀z ∈ ℤ, z ≤ x ⇒ z ≤ ⌊x⌋).

Claim 1.1: ∀x ∈ ℝ, ∀y ∈ ℝ, x > y ⇒ ⌊x⌋ ≥ ⌊y⌋.

Assume, x, y ∈ ℝ # Domain assumption

Assume x  > y               # Antecedent assumption

    Then x ≥ ⌊x⌋            # By definition

    Then x ≥ z              # By definition

    Then ⌊x⌋≥ z             # Also by definition

    Let z = ⌊y⌋             # By assumption & definition since ∀z ∈ ℤ, y ∈ ℝ and ℤ ∈ ℝ

    Then ⌊x⌋ ≥ ⌊y⌋          # Substitution

Then x  > y  ⇒ ⌊x⌋ ≥ ⌊y⌋    # Introduce implication

Then ∀x ∈ ℝ, ∀y ∈ ℝ, x > y ⇒ ⌊x⌋ ≥ ⌊y⌋ # Introduce universal

Answer 1

You should justify that x ≥ ⌊y⌋ before saying that "Then ⌊x⌋ ≥ ⌊y⌋". And it is quite obvious that x ≥ ⌊y⌋ since by definition, x>y>⌊y⌋.

Answer 2

I get the general idea of your proof, but some steps aren't very clear. For example, when do you use the fact that $x > y$? Here's my version.

---

Given any $r \in \mathbb R$, we make use of the following assumptions about the floor function:

$\lfloor r \rfloor \in \mathbb Z \tag 1$ $r \geq \lfloor r \rfloor \tag 2$ $\forall z \in \mathbb Z \tag 3,~ r \geq z \implies \lfloor r \rfloor \geq z$

We want to prove that for all $x,y \in \mathbb R$, if $x > y$, then $\lfloor x \rfloor \geq \lfloor y \rfloor$.

• To this end, choose any $x,y \in \mathbb R$ such that $x > y$.
• Now since $y \in \mathbb R$, we may take $r = y$ so that by $(2)$, we know that $y \geq \lfloor y \rfloor$.
• But since $x > y$ implies that $x \geq y$, it follows by the transitivity of $\geq$ that $x \geq \lfloor y \rfloor$.
• But since $y \in \mathbb R$, we may take $r = y$ so that by $(1)$, we know that $\lfloor y \rfloor \in \mathbb Z$.
• Hence, by taking $r = x$ and $z = \lfloor y \rfloor$, we may combine the last two bullets with $(3)$ to conclude that $\lfloor x \rfloor \geq \lfloor y \rfloor$, as desired. $~~\blacksquare$

Answer 3

$x\geq y$ combined with $\lfloor y\rfloor\leq y$ gives $\lfloor y\rfloor\leq x$.

Here $\lfloor y\rfloor\in\mathbb Z$ so we conclude that $\lfloor y\rfloor\leq \lfloor x\rfloor$.

Proved is now: $$x\geq y\Rightarrow \lfloor x\rfloor\geq \lfloor y\rfloor$$