|
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
¤ Dauer der Verarbeitung: 0.15 Sekunden
(vorverarbeitet)
¤
|
schauen Sie vor die Tür
Fenster
Die Firma ist wie angegeben erreichbar.
Die farbliche Syntaxdarstellung ist noch experimentell.
|
