When extending Euclid's lemma to an arbitrary product, why must 2 be in the induction base case? The statement I'm trying to prove:
Let $p$ be prime, $n \in N$, and $a_1, a_2, \ldots, a_n \in Z$. If $p \mid (\prod^n_{i=1}a_i)$ then $p \mid a_i$ for some $i$.
So if $p$ divides a product of integers, it must divide one of the integers in the product.
Proof. I prove by induction.
Base Case The base case is given - when $n=1$, $p \mid a_1 \implies p \mid a_1$, trivially.
Induction Step Suppose the theorem holds for $n=m$. Suppose $p \mid (\prod^{m+1}_{i=1}a_i)$. Then
$$
p \mid (\prod^{m}_{i=1}a_i) \cdot a_{m+1}
$$
By Euclid's lemma $p \mid (\prod^{m}_{i=1}a_i)$ or $p \mid a_{m+1}$. In the first case, $p \mid a_i$ for some $i$ by hypothesis. In the second, $p \mid a_i$ for $i = m+1$. So in either case $p \mid a_i$ for $1 \leq i \leq m+1$. So if the lemma holds for $n=m$ it holds for $n=m+1$ and thus holds for all $k \in N$. QED
Standard proof of this statement. Here's what I don't understand - every other proof shows $n=2$ in the base case. Why? Can't we show 2 in the inductive step?
 A: When you say $p \mid (\prod_{i=1}^m a_i)$ or  $p\mid a_{m+1}$, my question is: how do you know?
It would be nice to have proven if $p\mid a_1a_2$ then $p\mid a_1$ or $p\mid a_2$. I.e. you actually need the base case of $n=2$ to be true as you use both this fact and the inductive hypothesis in the inductive step.
A: Call the statement $P_n$. The standard proof uses $\rm\color{#c00}{strong}$ induction with base case $\,n=2\,$ and it uses the strong inductive step $\,\color{#c00}{P_2}\ \&\ P_n\Rightarrow P_{n+1}$.
Your proof effectively transforms the strong induction into a normal induction by moving the proof of $P_2$ into a Lemma (call it $\rm\color{#0a0}{EL}$ = Euclid's Lemma). So  your transformed proof has base case $\,n=1\,$ and the normal inductive step $\, P_n\Rightarrow P_{n+1}$ by $\rm\color{#0a0}{EL}$.
Obviously the same method works to transform into a normal induction any complete induction that uses a fixed number of $\rm\color{#c00}{initial\  cases}$ in its strong induction step.
Remark $ $ The proof is a special case of the inductive $n$-ary extension of a hom, i.e.
$$f(a_2 * a_1) = f(a_2)\sqcup f(a_1)\ \Rightarrow\ f(a_n* \cdots* a_1) = f(a_n)\sqcup \cdots \sqcup f(a_1)\qquad$$
OP is case $\,f(n) = [\![\:\! p\mid n\:\!]\!]\,$ where the brackets denote boolean truth value, and where $\sqcup $ is $\vee$, i.e. logical or. Above, for simplicity of notation, I assume the operations are associative (else e.g. right-associate everything).
