Proof of prime_ideals_in_int_ring