Every nontrivial finite abelian group is an internal direct product of indecomposable subgroups

Given: The objects and hypotheses in the statement.

A nontrivial finite abelian group is indecomposable if it is not an internal direct product of two nontrivial subgroups in the sense of def-internal-direct-product-of-subgroups. It is decomposable if such a product exists. The trivial group is assigned neither label. (Indecomposable and decomposable nontrivial finite abelian groups).

Let $P$ be a property of naturals such that for every $n \in \mathbb{N}$, if $P(m)$ holds for all $m < n$ then $P(n)$. Then $P(n)$ holds for all $n \in \mathbb{N}$. (At $n = 0$ the hypothesis is vacuous, so $P(0)$ is forced.) (Strong (complete) induction).

Let $N_0,\ldots,N_{r-1}\trianglelefteq G$. The following are equivalent: the $N_i$ form an internal direct product of $G$; every $g\in G$ has a unique expression $g=n_0\cdots n_{r-1}$ with $n_i\in N_i$; and the multiplication map $\mu:\prod_{i<r}N_i\to G$ is an isomorphism. These statements include the empty family and the one-factor case. (Internal direct products are external direct products, equivalently every element has a unique factorisation).

Let $G$ be a finite group and $H\le G$. Then $|G|=[G:H]\,|H|.$ Consequently, under the canonical embedding $\iota:\mathbb N\to\mathbb Z$, $|H|$ divides $|G|$. (Lagrange's theorem: $|G|=[G:H]|H|$ for every subgroup $H$ of a finite group $G$).