Let and form the Rees algebra . It is generated over by , so the Hilbert basis theorem makes it Noetherian. The Rees module is finite over it, generated by finitely many generators of the module in degree zero. Hence its graded submodule
has finitely many homogeneous generators, all in degrees at most some .
For , each degree- generator contributes a multiple from . This is contained in , because multiplication by puts its coefficient both in and in . Thus . The reverse inclusion follows directly by multiplication: it stays in and in . Consequently
This is the Artin-Rees lemma, proved through finite graded generation rather than an assumption that the intersection filtration initially has that form.
The height of a prime ideal is the supremum of the lengths of strict chains of prime ideals ending at :
The last equality follows from the prime ideal correspondence for localization. Here is a length-growth proof of the Krull height theorem that makes the bound explicit.
We first establish a prime-chain lower bound for local length. For a Noetherian local ring admitting a prime chain of length , put . Then
for some . For , use . For , quotient by the first prime ideal of the chain; this only decreases and reduces us to a local integral domain with
Take and put . It has a prime chain of length , so induction bounds below by a positive multiple of .
The Artin-Rees lemma applied to gives, for a fixed integer ,
Because is a non-zero-divisor, the first term in the exact sequence
has length at least . Hence
Iterate this inequality about times, while its arguments remain at least . This gives the desired positive multiple of . The particular Artin-Rees lemma inclusion used here follows directly from finite generation: the Rees algebra is Noetherian, by the Hilbert basis theorem, and its graded submodule has finitely many homogeneous generators. A bound on their degrees gives .
Now localize at the given minimal prime ideal . Write , , and . The only prime ideal of containing is , so . Since is finitely generated, some . Thus has finite module length, say . The ideal is generated by at most elements.
For , products of these generators give a surjection from copies of onto . Summing the lengths gives the generator bound for primary-ideal length
Since , we have , and therefore
The prime-chain lower bound for local length now excludes any chain of length greater than . Consequently
For , minimality over the zero ideal says that is a minimal prime ideal, so its height is zero. This also handles that boundary case.