SSL infinite_primes.pvs   Interaktion und
PortierbarkeitPVS

infinite_primes: THEORY
BEGIN
    IMPORTING ints@divides_lems, 
              reals@product_fseq_posnat,
              prime_factorization
    Primes: set[nat] = {n: nat | prime?(n)}

    n: VAR posnat
    prime_divides: LEMMA  NOT prime?(n) AND n > 1 IMPLIES
                                 (EXISTS (p: nat): prime?(p) AND divides(p,n))

    ii: VAR nat
    divides_product: LEMMA FORALL (fs: fseq[posnat]),
                                       (ii: below(length(fs))): 
                                 divides(seq(fs)(ii), product(fs))

    primes_infinite: THEOREM NOT is_finite(Primes)
 
END infinite_primes