Proofs with floor and ceiling: $\lceil -x \rceil = -\lfloor x \rfloor$ 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.
 A: 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$.
A: Concerning your final answer I would proceed as follows.
Some preliminary definitions first.


*

*$y = \left\lfloor y \right\rfloor  + \left\{ y \right\}$
which is a definition of the fractional part $0 \leqslant \left\{ y \right\} < 1$,

*$\left\lceil y \right\rceil  = \left\lceil {\left\lfloor y
   \right\rfloor  + \left\{ y \right\}} \right\rceil  = \left\lfloor y
   \right\rfloor  + \left\lceil {\left\{ y \right\}} \right\rceil  =
   \left\lfloor y \right\rfloor  + 1 - \left[ {0 = \left\{ y \right\}}
   \right]$
which is the relation between ceil and floor functions,

*and where the square brackets indicates the Iverson bracket $$
   \left[ \text{P} \right] = \left\{ {\begin{array}{*{20}c}    0 &
   {\text{P} = \text{FALSE}}  \\    \text{1} & {\text{P} = \text{TRUE}} 
   \\  \end{array} } \right. $$


Then
$$
\begin{gathered}
  \left\lfloor { - y} \right\rfloor  = \left\lfloor { - \left\lfloor y \right\rfloor  - \left\{ y \right\}} \right\rfloor  =  - \left\lfloor y \right\rfloor  + \left\lfloor { - \left\{ y \right\}} \right\rfloor  =  \hfill \\
   =  - \left\lfloor y \right\rfloor  - 1 + \left[ {0 = \left\{ y \right\}} \right] =  \hfill \\
   =  - \left( {\left\lfloor y \right\rfloor  + 1 - \left[ {0 = \left\{ y \right\}} \right]} \right) =  - \left\lceil y \right\rceil  \hfill \\ 
\end{gathered} 
$$
and replacing $y$ with $-x$, you get the complementary
$$
\left\lfloor x \right\rfloor  =  - \left\lceil { - x} \right\rceil 
$$
Of course you could proceed like that right from the beginning.
A: Let $y = \lceil - x \rceil$.  So $y \ge -x$ so $-y \le x$.  $\forall z\in \mathbb Z, z \ge -x \implies z \ge y$ so $\forall -z \in \mathbb Z -z \le x \implies -z \le -y$.  So by definition $-y = \lfloor x \rfloor$.
Although, to tell the truth, I'm not sure we can accept your conditions as definitions unless we can also prove i) such a $y$ exists and ii) such a $y$ is unique.
A: Let $F = \lfloor x \rfloor$. Then $F$ is an integer, $F \le x$,  and 
$\forall m \in \mathbb{Z},\; m\le x \implies m \le F$.
Then $F+1 \le x \implies F+1 \le F$. It follows that
$$ F \le x \lt F+1$$
$$ -F - 1 \lt -x \le -F $$
Let $-C = \lceil -x \rceil$. Then $-C$ is an integer,  $-x \le -C$, and
$\forall m \in \mathbb{Z}, \; -x \lt m \implies -C \le m)$.
By reasoning similar to that used above, it follows that
$$-C -1 < -x \le -C$$
Then $-C-1 < -F$ and $-F-1 < -C$. Hence $-1 < F-C < 1$. Since $F$ and $C$ are integers,it follows that $F=C$; that is
$$\lceil -x \rceil = -\lfloor x \rfloor$$
