\documentclass{article}

\usepackage[utf8]{inputenc}
\usepackage[british]{babel}
\usepackage{xr}
\usepackage[foundations, arithmetic]{../lib/tex/naproche}

\externaldocument{arithmetic/arithmetic}

\newcommand{\N}{\mathrm{N}}
\newcommand{\Int}{\mathbb{Z}}
\newcommand{\Ps}{\mathrm{P}}

\title{Furstenberg's proof of the infinitude of primes}
\author{\Naproche formalization: \vspace{0.5em} \\
Andrei Paskevich (2007), \\
Marcel Schütz (2021 - 2022)}
\date{}


\begin{document}
  \maketitle

  \noindent This is a formalization of Furstenberg's topological proof of the
  infinitude of primes \cite[p. 353]{Furstenberg1955}.
  On mid-range hardware \Naproche needs approximately 5 Minutes to verify this
  formalization plus approximately 40 minutes to verify the library files it
  depends on.

  \begin{forthel}
    %[prove off][check off]

    [readtex \path{arithmetic/sections/10_primes.ftl.tex}]

    [readtex \path{arithmetic/sections/11_cardinality.ftl.tex}]

    %[prove on][check on]
  \end{forthel}

  The central idea of Furstenberg's proof is to define a certain topology on
  $\Nat$ from the properties of which we can deduce that the set of
  primes is infinite.\footnote{Actually, Furstenberg's proof makes use of a
  topology on $\Int$. But this topology can as well be restricted to
  $\Nat$ without substantially changing the proof.}

  \begin{forthel}
    Let $n, m, k$ denote natural numbers.
    Let $p, q$ denote nonzero natural numbers.

    \begin{definition}
      Let $A$ be a subset of $\Nat$.
      $A^{\complement} = \Nat \setminus A$.
    \end{definition}

    Let the complement of $A$ stand for $A^{\complement}$.

    \begin{lemma}
      The complement of any subset of $\Nat$ is a subset of $\Nat$.
    \end{lemma}
  \end{forthel}

  Towards a suitable topology on $\Nat$ let us define \textit{arithmetic
  sequences} $\N_{n, q}$ on $\Nat$.

  \begin{forthel}
    \begin{definition}
      $\N_{n, q} = \{ m \in \Nat \mid m \equiv n \pmod{q} \}$.
    \end{definition}
  \end{forthel}

  This allows us to define the \textit{evenly spaced natural number
  topology} on $\Nat$, whose open sets are defined as follows.

  \begin{forthel}
    \begin{definition}
      Let $U$ be a subset of $\Nat$.
      $U$ is open iff for any $n \in U$ there exists a $q$ such that
      $\N_{n, q} \subseteq U$.
    \end{definition}

    \begin{definition}
      A system of open sets is a system of sets $S$ such that every element of
      $S$ is an open subset of $\Nat$.
    \end{definition}
  \end{forthel}

  We can show that the open sets indeed form a topology on $\Nat$.

  \begin{forthel}
    \begin{lemma}
      $\Nat$ and $\emptyset$ are open.
    \end{lemma}

    \begin{lemma}
      Let $U,V$ be open subsets of $\Nat$.
      Then $U \cap V$ is open.
    \end{lemma}
    \begin{proof}
      Let $n \in U \cap V$.
      Take a $q$ such that $\N_{n, q} \subseteq U$.
      Take a $p$ such that $\N_{n, p} \subseteq V$.
      Then $p \cdot q \neq 0$.

      Let us show that $\N_{n, p \cdot q} \subseteq U \cap V$.
        Let $m \in \N_{n, p \cdot q}$.
        We have $m \equiv n \pmod{p \cdot q}$.
        Hence $m \equiv n \pmod{p}$ and $m \equiv n \pmod{q}$.
        Thus $m \in \N_{n, p}$ and $m \in \N_{n, q}$.
        Therefore $m \in U$ and $m \in V$.
        Consequently $m \in U \cap V$.
      End.
    \end{proof}

    \begin{lemma}
      Let $S$ be a system of open sets.
      Then $\bigcup S$ is open.
    \end{lemma}
    \begin{proof}
      Let $n \in \bigcup S$.
      Take a set $M$ such that $n \in M \in S$.
      Consider a $q$ such that $\N_{n, q} \subseteq M$.
      Then $\N_{n, q} \subseteq \bigcup S$.
    \end{proof}
  \end{forthel}

  Now that we have a topology of open sets on $\Nat$, we can continue
  with a characterization of closed sets whose key property is that they are
  closed under finite unions.

  \begin{forthel}
    \begin{definition}
      Let $A$ be a subset of $\Nat$.
      $A$ is closed iff $A^{\complement}$ is open.
    \end{definition}

    \begin{definition}
      A system of closed sets is a system of sets $S$ such that every element of
      $S$ is a closed subset of $\Nat$.
    \end{definition}

    \begin{lemma}
      Every system of closed sets is a set.
    \end{lemma}
    \begin{proof}
      Let $S$ be a system of closed sets.
      Then $S \subseteq \pow(\Nat)$.
      $\pow(\Nat)$ is a set.
      Hence $S$ is a set.
    \end{proof}

    \begin{lemma}
      Let $S$ be a finite system of closed sets.
      Then $\bigcup S$ is closed.
    \end{lemma}
    \begin{proof}
      Define $C = \{ X \mid X$ is a closed subset of $\Nat \}$.

      Let us show that $A \cup B \in C$ for any $A, B \in C$.
        Let $A, B \in C$.
        Then $A, B$ are closed subsets of $\Nat$.
        % The LHS of the following equation must be put in parentheses due to a
        % bug in Naproche's parser.
        We have $((A \cup B)^{\complement}) = A^{\complement} \cap B^{\complement}$.
        $A^{\complement}$ and $B^{\complement}$ are open.
        Hence $A^{\complement} \cap B^{\complement}$ is open.
        Thus $A \cup B$ is a closed subset of $\Nat$.
      End.

      Therefore $C$ is closed under finite unions.
      Consequently $\bigcup S \in C$.
      Indeed $S$ is a subset of $C$.
    \end{proof}
  \end{forthel}

  An important step towards Furstenberg's proof is to show that arithmetic
  sequences are closed.

  \begin{forthel}
    \begin{lemma}
      $\N_{n, q}$ is closed.
    \end{lemma}
    \begin{proof}
      Let $m \in (\N_{n, q})^{\complement}$.

      Let us show that $\N_{m, q} \subseteq (\N_{n, q})^{\complement}$.
        Let $k \in \N_{m, q}$.
        Assume $k \notin (\N_{n, q})^{\complement}$.
        Then $k \equiv m \pmod{q}$ and $n \equiv k \pmod{q}$.
        Hence $m \equiv n \pmod{q}$.
        Therefore $m \in \N_{n, q}$.
        Contradiction.
      End.
    \end{proof}
  \end{forthel}

  Identifying each prime number $p$ with the arithmetic sequence $\N_{0, p}$
  yields a bijection between the set $\Prime$ of all prime numbers and the set
  $\Ps$ of all such sequences $\N_{0, p}$.
  Thus to show that there are infinitely many primes it suffices to show that
  $\Ps$ is infinite.

  \begin{forthel}
    \begin{definition}
      $\Ps = \{ \N_{0, p} \mid p \in \Prime \}$.
    \end{definition}

    \begin{lemma}
      $\Ps$ is a system of closed sets.
    \end{lemma}
    \begin{proof}
      $\N_{0, p}$ is a closed subset of $\Nat$ for every $p \in \Prime$.
    \end{proof}

    \begin{lemma}
      $\Ps$ is a set that is equinumerous to $\Prime$.
    \end{lemma}
    \begin{proof}
      (1) $\Ps$ is a set.
      Indeed $\Ps \subseteq \pow(\Nat)$.

      (2) $\Ps$ is equinumerous to $\Prime$. \\
      Proof.
        Define $f(p) = \N_{0,p}$ for $p \in \Prime$.

        Let us show that $f$ is injective.
          Let $p, q \in \Prime$.
          Assume $f(p) = f(q)$.
          Then $\N_{0, p} = \N_{0, q}$.
          We have $\N_{0, p} = \{ m \in \Nat \mid m \equiv 0 \pmod{p} \}$ and
          $\N_{0, q} = \{ m \in \Nat \mid m \equiv 0 \pmod{q} \}$.
          Hence for all $m \in \Nat$ we have $m \equiv 0 \pmod{p}$ iff
          $m \equiv 0 \pmod{q}$.
          Thus for all $m \in \Nat$ we have $m \mod p = 0 \mod p$ iff
          $m \mod q = 0 \mod q$.
          We have $0 \mod p = 0 = 0 \mod q$.
          Hence for all $m \in \Nat$ we have $m \mod p = 0$ iff $m \mod q = 0$.
          Thus for all $m \in \Nat$ we have $p \mid m$ iff $q \mid m$.
          Therefore $p = q$.
        End.

        $f$ is surjective onto $\Ps$.
        Thus $f$ is a bijection between $\Prime$ and $\Ps$.
      Qed.
    \end{proof}

    \begin{theorem}[Furstenberg]
      $\Prime$ is infinite.
    \end{theorem}
    \begin{proof}
      $\bigcup \Ps$ is a subset of $\Nat$.

      Let us show that for any $n \in \Nat$ we have $n \in \bigcup \Ps$ iff $n$
      has a prime divisor.
        Let $n \in \Nat$.

        If $n$ has a prime divisor then $n$ belongs to $\bigcup \Ps$. \\
        Proof.
          Assume $n$ has a prime divisor.
          Take a prime divisor $p$ of $n$.
          We have $\N_{0, p} \in \Ps$.
          Hence $n \in \N_{0, p}$.
        Qed.

        If $n$ belongs to $\bigcup \Ps$ then $n$ has a prime divisor. \\
        Proof.
          Assume that $n$ belongs to $\bigcup \Ps$.
          Take a prime number $r$ such that $n \in \N_{0, r}$.
          Hence $n \equiv 0 \pmod{r}$.
          Thus $n \mod r = 0 \mod r = 0$.
          Therefore $r$ is a prime divisor of $n$.
        Qed.
      End.

      Hence For all $n \in \Nat$ we have $n \in (\bigcup \Ps)^{\complement}$ iff
      $n$ has no prime divisor.
      $1$ has no prime divisor and any natural number having no prime
      divisor is equal to $1$.
      Therefore $(\bigcup \Ps)^{\complement} = \set{1}$.
      Indeed $((\bigcup \Ps)^{\complement}) \subseteq \set{1}$ and $\set{1}
      \subseteq (\bigcup \Ps)^{\complement}$. %!

      $\Ps$ is infinite. \\
      Proof by contradiction.
        Assume that $\Ps$ is finite.
        Then $\bigcup \Ps$ is closed and $(\bigcup \Ps)^{\complement}$ is open.
        Take a $p$ such that $\N_{1, p} \subseteq (\bigcup \Ps)^{\complement}$.
        $1 + p$ is an element of $\N_{1, p}$.
        Indeed $1 + p \equiv 1 \pmod{p}$
        (by \ref{ARITHMETIC_08_5984712287846400}).
        $1 + p$ is not equal to $1$.
        Hence $1 + p \notin (\bigcup \Ps)^{\complement}$.
        Contradiction.
      Qed.
    \end{proof}
  \end{forthel}

  \begin{thebibliography}{1}
    \bibitem{Furstenberg1955} Harry Furstenberg (1955),
      \textit{On the Infinitude of Primes};
      The American Mathematical Monthly, vol. 62, no. 5
  \end{thebibliography}
\end{document}
