  We show that $VTC^0$, the basic theory of bounded arithmetic corresponding to
the complexity class $\mathrm{TC}^0$, proves the $IMUL$ axiom expressing the
totality of iterated multiplication satisfying its recursive definition, by
formalizing a suitable version of the $\mathrm{TC}^0$ iterated multiplication
algorithm by Hesse, Allender, and Barrington. As a consequence, $VTC^0$ can
also prove the integer division axiom, and (by our previous results) the
RSUV-translation of induction and minimization for sharply bounded formulas.
Similar consequences hold for the related theories $\Delta^b_1$-$CR$ and
$C^0_2$.
  As a side result, we also prove that there is a well-behaved $\Delta_0$
definition of modular powering in $I\Delta_0+WPHP(\Delta_0)$.
