\problemdata
{induction}
{S00 ps2}

\begin{problem}
% ordinary induction
% source:  Parmenter p. 173

Prove by induction that $\forall\; n \geq 1$, the quantity $n^3 +
(n+1)^3 + (n+2)^3$ is divisible by~$9$.

\solution
  Let $P(n)$ be the predicate that $n^3 + (n+1)^3 + (n+2)^3$ is
  divisible by $9$, \ie $P(n) = 9 | (n^3 + (n+1)^3 + (n+2)^3)$.  We
  prove that $P(n)$ holds for all $n \geq 1$ by induction on $n$.  In
  fact, the predicate $P(n)$ is also true for $n = 0$.

  \begin{description}\itemsep 0\baselineskip
  \item[Base Case:~~] $P(1)$ \mbox{} \\
    $P(1) = 9 | (1^3 + 2^3 + 3^3) = 9 | 36 = \True$ 

  \item[Inductive Step:~~] For all $n \geq 1$, $P(n) \implies P(n+1)$
    \begin{enumerate}\itemsep 0ex
    \item Fix $n \geq 1$.

    \item From the inductive hypothesis $P(n)$ holds, \ie $9 | (n^3 +
      (n+1)^3 + (n+2)^3)$.

    \item We must show that $P(n+1)$ holds, \ie $9 | ((n+1)^3 +
      (n+2)^3 + (n+3)^3)$.
          
      \begin{enumerate}\itemsep 0ex
      \item $(n+1)^3 + (n+2)^3 + (n+3)^3 = n^3 + (n+1)^3 + (n+2)^3 + 9
        (n^2 + 3n +3)$
        
      \item From the inductive hypothesis, $9 | (n^3 + (n+1)^3 + (n+2)^3)$.
        
      \item Also, it is simple to see that $9 | (9 (n^2 + 3n +3))$.

      \item Since $9$ divided both terms, it divides their sum.

      \item QED
          
      \end{enumerate}

    \item QED (implication and UG)

    \end{enumerate}

  \end{description}

}
\end{problem}