theory
Primtal
imports
Main
"HOL-Computational_Algebra.Primes"
begin
abbreviation \primes \ {p :: nat. prime p}\
theorem \\ (finite primes)\
proof
assume \finite primes\
then have \\b. \x \ primes. x \ b\
using finite_nat_set_iff_bounded_le by blast
then obtain b :: nat where \\x. prime x \ x \ b\
by auto
moreover have \\n. \p :: nat. prime p \ n < p \ p \ fact n + 1\
proof
fix n
have n1: \fact n + 1 \ 1\
by (metis add.commute add_diff_cancel_left' cancel_comm_monoid_add_class.diff_cancel fact_nonzero of_nat_eq_1_iff of_nat_fact semiring_1_class.of_nat_simps(2))
from prime_factor_nat[OF n1] obtain p :: nat
where \prime p\ and \p dvd fact n + 1\
by auto
then have \p \ fact n + 1\
by (intro dvd_imp_le, auto)
have \n < p\
proof (rule ccontr)
assume \\ n < p\
then have \p \ n\ by simp
from \prime p\ have \p \ 1\
by (cases p, auto)
with \p \ n\ have \p dvd fact n\
by (intro dvd_fact)
with \p dvd fact n + 1\ have \p dvd fact n + 1 - fact n\
by (rule dvd_diff_nat)
then have \p dvd 1\ by simp
then have \p \ 1\ by auto
moreover from \prime p\ have \p > 1\
using prime_nat_iff by blast
ultimately show False by auto
qed
with \prime p\ and \p \ fact n + 1\
show \\p :: nat. prime p \ n < p \ p \ fact n + 1\
by blast
qed
then have \\p. prime p \ p > b\
by auto
ultimately show False
by auto
qed
end