If $n$ is a positive integer, prove that
$$\left\lfloor\frac{8n+13}{25}\right\rfloor-\left\lfloor\frac{n-12-\left\lfloor\frac{n-17}{25}\right\rfloor}{3}\right\rfloor$$
is independent of $n$.
Taking
$$f(n)=\left\lfloor\frac{8n+13}{25}\right\rfloor-\left\lfloor\frac{n-12-\left\lfloor\frac{n-17}{25}\right\rfloor}{3}\right\rfloor$$
I could prove that
$$f(n+25)=f(n)$$
But, I have no idea how to show
$$f(n+k)=f(n)\\\forall k\in \{1,2,\dots 24\}$$
Of course, we can check these finite number of cases by force. But is there any other elegant method to handle this?
Best Answer
Using $\color{darkorange}{\rm UF}$ = universal property of floor, i.e. $\ k\le \lfloor r\rfloor\!\!\iff\! k\le r;\ $ $\ \color{#90f}{k \le -\lfloor r\rfloor\!\!\iff\! k\!-\!1< -r},\ $ the proof reduces to trivial algebra, i.e. apply $\,\lfloor(r\!-\!12)/3\rfloor^{\phantom{|^|}}\!\!\! = \lfloor r/3\rfloor - 4\,$ followed by below.
$\begin{align} {\bf Theorem}\ \quad \lfloor \color{#0a0}{\tfrac{1}{25}(8n+3)}\rfloor &= \lfloor \tfrac{1}{3}(n - \lfloor(n-17)/25\rfloor)\rfloor,\ \ {\rm for}\ \ n\in\Bbb Z\\[.4em] {\bf Proof}\ \ {\rm for}\ \ k\in\Bbb Z\!:\ \ \qquad k&\ \le\, \tfrac{1}{3}(n - \lfloor(n-17)/25\rfloor)\\[.2em] \iff\ 3k-n&\,\le\,\ \ \ \ \ \ \ -\lfloor(n-17)/25\rfloor\\[.3em] \iff\ 3k-n &\,\le\, (-n+41)/25,\ \ {\rm by\ Lemma\ below}\\[.3em] \smash[t]{\overset{\times\ 25}\iff}\ \ \ \ \ \ \ \ 75k &\,\le\,\ 24n+41\\[.3em] \smash[t]{\overset{\div\,3}\iff}\ \ \ \ \ \ \ \,25k &\,\le\ \ \ 8n+ 13,\ \ {\rm by}\ \ 25k\in\Bbb Z\\[.2em] \iff\qquad\ \ \ k &\,\le \color{#0a0}{\tfrac{1}{25}(8n+3)} \end{align}$
Lemma $\ \ \ \ \color{#90f}{j \,\le\, -\lfloor a/b\rfloor}\iff j\!\color{darkorange}{-\!1}\le (-a\!\color{darkorange}{-\!1})/b,\ \ {\rm for}\,\ \color{#c00}{b>0}\,$ (wlog), $\,a,b\in\Bbb Z$
Pf: $ \overset{\rm\color{darkorange}{UF}}\iff\! \color{#90f}{j\!-\!1 < {-}a/b}\!\!\underset{\color{#c00}{\times\ b}}\iff\! b(j\!\color{darkorange}{-\!1})\!\,\le -a\!\color{darkorange}{-\!1}\ $ [by $\ m<n\!\iff m\le n\!\color{darkorange}{-\!1}$]