Gnarly equality proof? Or not?

Question

I have this gnarly equality which Mathematica's Reduce says it doesn't have the chops to handle: $\left.k\in \mathbb{Z}\land \left\lceil \frac{k-2}{2}\right\rceil \left(\left\lceil \frac{k-2}{2}\right\rceil -((k-2) \bmod 2)+2\right)+k+1=\left\lceil \frac{k}{2}\right\rceil \left(\left\lceil \frac{k}{2}\right\rceil -(k \bmod 2)+2\right)\right]$,
so I simplified to this: $k\in \mathbb{Z}\land (k \bmod 2)+k=2 \left\lceil \frac{k}{2}\right\rceil$, which Mathematica reduces to: $c_1\in \mathbb{Z}\land k=c_1$.

So, can I say that this proves the equality for $k\geq1$? Or is something subtle going on? Do I need to do more?

Answer 1

Rad, dude. You are correct on all counts. The equality is too gnarly for Mathematica; your reduction is correct; and your interpretation of Mathematica's final answer is good. Way to go.

You can actually go further: Mathematica's answer is good for $k \in \mathbb{Z}$, not just $k \in \mathbb{Z}^{\geq 1}$.

Answer 2

Good job simplifying the equality. Let me just show how to finish it off by hand, without Mathematica's help.

The mod operation can conveniently be defined in terms of the floor function by

$$x \bmod y = x - y \lfloor x/y \rfloor,\quad \text{for all real }x \text{ and real }y \ne 0.$$

Try to understand why this is the right definition. We are subtracting a multiple of $y$ from $x$. Test it out with a few small integers to see what happens. By the way, for the sake of completeness note also that we define $x \bmod 0 = x$ for all $x.$

Substituting the definition of mod into your equation yields

$$k - 2 \lfloor k/2 \rfloor + k = 2\lceil k/2 \rceil,$$

and rearranging we get

$$k = \lfloor k/2 \rfloor + \lceil k/2 \rceil.$$

Rad! This last equation holds for all integer $k$. If you'd like to verify it, check the odd and even cases separately (ie. write $k = 2j$ and $k = 2j + 1$.)