Grace/Cumulus/NumberTheory/Infinitude.g17

Open in Workbench Download source

Imports

Prime · Cardinal.Finite

Declarations

• primes.subset_naturals theorem derivation
• primes.order_unbounded theorem derivation
• primes.infinite theorem derivation

Source

1-- Infinitude of the prime natural numbers2-- Part of Cumulus, the Grace17 mathematics library.3-- Copyright (c) 2026 Grant Passmore.4-- Released under the Apache License 2.0. See LICENSE in the repository root.5-- Authors: Grant Passmore67module Grace.Cumulus.NumberTheory.Infinitude8import Prime9import Cardinal.Finite1011theorem primes.subset_naturals12  shows (primes ⊆ ℕ)13proof14  intros p hp15  obtain ⟨hpNatural, hpPrime⟩ := primes.membership.forward with hp16  exact hpNatural1718theorem primes.order_unbounded (n : Nat)19  shows ∃ p ∈ primes, n < p20proof21  obtain ⟨p, hpPrime, hnLessP⟩ := Euclid.larger_prime at n with assumption22  witness p23  constructor24  . apply primes.contains at p25    exact hpPrime26  . exact hnLessP2728-- The set-level corollary lives apart from the elementary number theory, so29-- prime development and computation need not load the cardinality and30-- function library to state and prove Euclid's theorem.31theorem primes.infinite32  shows ¬Finite(primes)33proof34  exact infinite.of_unbounded_naturals with primes.subset_naturals, primes.order_unbounded35