PID implies UFD

This article gives the statement and possibly, proof, of an implication relation between two integral domain properties. That is, it states that every integral domain satisfying the first integral domain property (i.e., principal ideal domain) must also satisfy the second integral domain property (i.e., unique factorization domain)
View all integral domain property implications | View all integral domain property non-implications |Get help on looking up integral domain property implications/non-implications
Get more facts about principal ideal domain|Get more facts about unique factorization domain

Statement

Any principal ideal domain is a unique factorization domain.

Facts used

1. Principal ideal implies Noetherian
2. Noetherian implies ACCP
3. ACCP implies every element has a factorization into irreducibles
4. PID implies Bezout
5. Bezout implies every irreducible is prime
6. Every irreducible is prime implies any two irreducible factorizations are equal upto ordering and associates

Proof

Facts (1)-(3) guarantee the existence of a factorization into irreducibles for any nonzero non-unit. Facts (4)-(6) guarantee the uniqueness of factorization.