[proofplan] The statement is a generalization of Euclid's lemma from elements to ideals: if the product of two ideals lies inside a prime ideal, then one of the factors already does. The proof is a direct contrapositive argument. Assume $\mathfrak{a} \not\subseteq \mathfrak{p}$ and exhibit an element $a \in \mathfrak{a} \setminus \mathfrak{p}$; we then show every $b \in \mathfrak{b}$ must lie in $\mathfrak{p}$, using the defining property of a prime ideal applied to the element $ab \in \mathfrak{p}$. [/proofplan] [step:Fix an element of $\mathfrak{a}$ outside $\mathfrak{p}$ using the contrapositive assumption] Suppose $\mathfrak{a} \not\subseteq \mathfrak{p}$ (otherwise there is nothing to prove). By negation of inclusion, there exists \begin{align*} a \in \mathfrak{a} \setminus \mathfrak{p}. \end{align*} We will show $\mathfrak{b} \subseteq \mathfrak{p}$, which suffices to conclude the disjunction "$\mathfrak{a} \subseteq \mathfrak{p}$ or $\mathfrak{b} \subseteq \mathfrak{p}$". [guided] The conclusion "$\mathfrak{a} \subseteq \mathfrak{p}$ or $\mathfrak{b} \subseteq \mathfrak{p}$" is a disjunction; one standard way to prove it is: assume the first disjunct fails, derive the second. We choose this route. Assume $\mathfrak{a} \not\subseteq \mathfrak{p}$. The inclusion $\mathfrak{a} \subseteq \mathfrak{p}$ means every element of $\mathfrak{a}$ lies in $\mathfrak{p}$; its negation is that *some* element of $\mathfrak{a}$ does not lie in $\mathfrak{p}$. So we may pick \begin{align*} a \in \mathfrak{a}, \quad a \notin \mathfrak{p}. \end{align*} Our goal is now to show $\mathfrak{b} \subseteq \mathfrak{p}$. This means: for every $b \in \mathfrak{b}$, we must establish $b \in \mathfrak{p}$. Since $b$ is to be arbitrary, let us fix one and argue. [/guided] [/step] [step:Form the product $ab$ and place it inside $\mathfrak{p}$ via the containment hypothesis] Let $b \in \mathfrak{b}$ be arbitrary. The product $ab$ lies in the product ideal $\mathfrak{a}\mathfrak{b}$ by definition: the product ideal $\mathfrak{a}\mathfrak{b}$ is the set of finite sums $\sum_k a_k b_k$ with $a_k \in \mathfrak{a}$, $b_k \in \mathfrak{b}$, and $ab$ is the particular one-term sum $a \cdot b$. By the standing hypothesis $\mathfrak{a}\mathfrak{b} \subseteq \mathfrak{p}$, \begin{align*} ab \in \mathfrak{p}. \end{align*} [guided] We have fixed $a \in \mathfrak{a} \setminus \mathfrak{p}$ from the previous step, and we are considering an arbitrary $b \in \mathfrak{b}$. We want to relate $b$ to $\mathfrak{p}$ via a tool that converts containment of products into containment of factors — this is the defining property of a prime ideal, and the input it requires is an element of the form $xy$ with $x, y \in \mathcal{O}_L$ and $xy \in \mathfrak{p}$. The natural candidate is $ab \in \mathcal{O}_L$ (since $a, b \in \mathcal{O}_L$ and the ring is closed under multiplication). Does $ab$ lie in $\mathfrak{p}$? We construct a chain: \begin{align*} ab \in \mathfrak{a}\mathfrak{b} \subseteq \mathfrak{p}. \end{align*} The first membership uses the definition of the product ideal: $\mathfrak{a}\mathfrak{b}$ is the set of finite sums $\sum_k a_k b_k$ with $a_k \in \mathfrak{a}$, $b_k \in \mathfrak{b}$. Taking the single-term sum with the pair $(a, b)$ shows $ab \in \mathfrak{a}\mathfrak{b}$. The second inclusion $\mathfrak{a}\mathfrak{b} \subseteq \mathfrak{p}$ is our standing hypothesis. Chaining yields $ab \in \mathfrak{p}$, the input required by primality. [/guided] [/step] [step:Apply the primality of $\mathfrak{p}$ to conclude $b \in \mathfrak{p}$] Recall that an ideal $\mathfrak{p} \unlhd \mathcal{O}_L$ is **prime** if $\mathfrak{p} \neq \mathcal{O}_L$ and, for all $x, y \in \mathcal{O}_L$, \begin{align*} xy \in \mathfrak{p} \implies x \in \mathfrak{p} \text{ or } y \in \mathfrak{p}. \end{align*} We apply this with $x = a$, $y = b$: we have $a, b \in \mathcal{O}_L$ and $ab \in \mathfrak{p}$ (from Step 2). Therefore $a \in \mathfrak{p}$ or $b \in \mathfrak{p}$. Since $a \notin \mathfrak{p}$ by our choice in Step 1, we must have $b \in \mathfrak{p}$. [guided] Primality of $\mathfrak{p}$ is the axiom \begin{align*} \forall x, y \in \mathcal{O}_L: \quad xy \in \mathfrak{p} \implies x \in \mathfrak{p} \text{ or } y \in \mathfrak{p}, \end{align*} together with $\mathfrak{p} \neq \mathcal{O}_L$. **Verifying hypotheses.** We apply the implication with $x = a$ and $y = b$: - $a \in \mathcal{O}_L$: since $\mathfrak{a} \subseteq \mathcal{O}_L$ (as $\mathfrak{a}$ is an integral ideal of $\mathcal{O}_L$) and $a \in \mathfrak{a}$. - $b \in \mathcal{O}_L$: analogously, $b \in \mathfrak{b} \subseteq \mathcal{O}_L$. - $ab \in \mathfrak{p}$: established in Step 2. **Conclusion of the implication.** $a \in \mathfrak{p}$ or $b \in \mathfrak{p}$. **Elimination of the first disjunct.** By Step 1, $a \notin \mathfrak{p}$. Hence the disjunction resolves to $b \in \mathfrak{p}$. Notice the role each ingredient plays: primality is used *once*, on the concrete element $ab$ that we manufactured. The witness $a$ from Step 1 is the key lever — without an element of $\mathfrak{a}$ outside $\mathfrak{p}$, the primality axiom would never be able to pick $b$ as the disjunct that must belong to $\mathfrak{p}$. [/guided] [/step] [step:Pass from the arbitrary $b$ to the conclusion $\mathfrak{b} \subseteq \mathfrak{p}$] The element $b \in \mathfrak{b}$ in Step 2 was arbitrary; Step 3 produced $b \in \mathfrak{p}$ from only the hypotheses $b \in \mathfrak{b}$ and $\mathfrak{a}\mathfrak{b} \subseteq \mathfrak{p}$ (together with the fixed $a \in \mathfrak{a} \setminus \mathfrak{p}$ of Step 1). Hence the implication $b \in \mathfrak{b} \implies b \in \mathfrak{p}$ holds for all $b$, i.e. \begin{align*} \mathfrak{b} \subseteq \mathfrak{p}. \end{align*} Combined with the contrapositive setup (Step 1: we assumed $\mathfrak{a} \not\subseteq \mathfrak{p}$), we have shown: \begin{align*} \mathfrak{a} \not\subseteq \mathfrak{p} \implies \mathfrak{b} \subseteq \mathfrak{p}. \end{align*} Equivalently, $\mathfrak{a} \subseteq \mathfrak{p}$ or $\mathfrak{b} \subseteq \mathfrak{p}$, which is the theorem. [guided] The argument we have carried out is: fix any $b \in \mathfrak{b}$; then $b \in \mathfrak{p}$. Since $b$ was a generic element of $\mathfrak{b}$, this proves the set-inclusion $\mathfrak{b} \subseteq \mathfrak{p}$ directly from its definition (every element of $\mathfrak{b}$ lies in $\mathfrak{p}$). We started by assuming $\mathfrak{a} \not\subseteq \mathfrak{p}$ (the contrapositive route). We reached $\mathfrak{b} \subseteq \mathfrak{p}$. The implication \begin{align*} \mathfrak{a} \not\subseteq \mathfrak{p} \implies \mathfrak{b} \subseteq \mathfrak{p} \end{align*} is logically equivalent to the disjunction \begin{align*} \mathfrak{a} \subseteq \mathfrak{p} \text{ or } \mathfrak{b} \subseteq \mathfrak{p} \end{align*} (by the tautology $\neg P \implies Q$ iff $P \lor Q$). This is the theorem statement. **Where primality was the crucial input.** If we drop primality and only ask $\mathfrak{p}$ to be a proper ideal, the statement fails. For instance, $\mathfrak{p} = (4) \subseteq \mathbb{Z}$ (not prime) and $\mathfrak{a} = \mathfrak{b} = (2)$ gives $\mathfrak{a}\mathfrak{b} = (4) \subseteq \mathfrak{p}$, yet neither $\mathfrak{a} = (2)$ nor $\mathfrak{b} = (2)$ is contained in $(4)$. Primality of $\mathfrak{p}$ is exactly the lever that forces the disjunction. **Consequence — prime ideals divide one factor.** Using [Divisibility Equals Containment](/theorems/1587), which identifies $\mathfrak{a} \mid \mathfrak{b}$ with $\mathfrak{b} \subseteq \mathfrak{a}$, the theorem can be restated as: if $\mathfrak{p}$ is prime and $\mathfrak{p} \mid \mathfrak{a}\mathfrak{b}$, then $\mathfrak{p} \mid \mathfrak{a}$ or $\mathfrak{p} \mid \mathfrak{b}$. This is the form in which the result is used to establish uniqueness of factorization (theorem 1589): it is Euclid's lemma for ideals. [/guided] [/step]