[Math] Proofs with floor and ceiling: $\lceil -x \rceil = -\lfloor x \rfloor$

ceiling-and-floor-functionslogicpredicate-logicproof-writing

I am trying to prove that $\lceil -x \rceil = -\lfloor x \rfloor$ using the following definitions:

$y = \lceil x \rceil$ means $y \in \mathbb{Z} \land y \ge x \land (\forall z \in \mathbb{Z}\; z\ge x \implies z \ge y)$

$y = \lfloor x \rfloor$ means $y \in \mathbb{Z} \land y \le x \land (\forall z \in \mathbb{Z}\;z\le x \implies z \le y)$

Since $\lceil -x \rceil = -\lfloor x \rfloor$ then $-\lceil -x \rceil = \lfloor x \rfloor$

I can substitute the $-x$ into the above definition for $\lceil x \rceil$

This gets me

$y = \lceil -x \rceil$ means $y \in \mathbb{Z} \land y \ge -x \land (\forall z \in \mathbb{Z}\; z\ge -x \implies z \ge y)$

How would I incorporate the $-$ on the outside of $-\lceil -x \rceil$ into the above statement, to show that it is equal to $\lfloor x \rfloor$?

I have looked at other questions discussing this proof, but they do not have anything to do with the two predicate definitions I wrote above.

Best Answer

To go directly from your definitions:

$y=-\lfloor x\rfloor$ means $-y=\lfloor x\rfloor$ and therefore we can again directly insert to get: $$-y \in \mathbb{Z} \land -y \le x \land (\forall z \in \mathbb{Z}\;z\le x \implies z \le -y)$$

Now obviously $-y\in\mathbb Z$ iff $y\in\mathbb Z$. Also $-y \le x$iff $y\ge -x$. Furthermore, $z\le x$ iff $-z\ge -x$, and $z\le -y$ iff $-z\ge y$. So we get: $$y \in \mathbb{Z} \land y \ge -x \land (\forall z \in \mathbb{Z}\;-z\ge -x \implies -z \ge y)$$ Finally, we observe that for any proposition $P(z)$, $\forall z\in\mathbb Z\;P(-z)$ is equivalent to $\forall z\in\mathbb Z\;P(z)$. Using this with $P(z)=(-z\ge -x \implies -z \ge y)$, we finally arrive at $$y \in \mathbb{Z} \land y \ge -x \land (\forall z \in \mathbb{Z}\;z\ge -x \implies z \ge y)$$ But that is exactly the expression you correctly derived as meaning $y=\lceil -x\rceil$.

So we have $y=-\lfloor x\rfloor \iff y=\lceil -x\rceil$ and thus $-\lfloor x\rfloor=\lceil -x\rceil$.