\documentclass{article}
\usepackage[english]{babel}
\usepackage{../lib/tex/naproche}
\usepackage{amssymb}

\begin{document}

\newcommand{\Prod}[3]{#1_{#2} \cdots #1_{#3}}
\newcommand{\Seq}[2]{\{#1,\dots,#2\}}
\newcommand{\FinSet}[3]{\{#1_{#2},\dots,#1_{#3}\}}
\newcommand{\Primes}{\mathbb{P}}
\newcommand{\pow}{{\cal P}}
\newcommand{\range}{\operatorname{ran}}
\newcommand{\inv}[1]{#1^{-1}}
\newcommand{\sset}[2]{\{#1\}_{#2}}

\title{Formalizing Sets and Numbers, and some of Wiedijk's
"100 Theorems" in \Naproche{}}

\author{Peter Koepke, Mateusz Marcol and Patrick Schäfer\\
\emph{Mathematical Institute, University of Bonn, Germany}
}

\maketitle

\section*{Preliminary Remarks}

{\em The source file of this document is a \LaTeX{} file which on one hand can be mathematically
typeset into a readable pdf document, and which on the other hand can
be input into the \Naproche{} natural language proof checker. \Naproche{} is part of the
Isabelle prover IDE; installing the current version of Isabelle will also
install \Naproche{}. Opening and editing a \verb+ftl.tex+ file like this one 
in Isabelle will automatically start the inbuilt \Naproche{} proof checking.

Apart from its mathematical content, the source file of about 3000
lines is testing the limits of the present \Naproche{}
system, its external automatic theorem provers (mostly E in our case),
and the underlying hardware. The file has been checked successfully 
in about half an hour on mid-range consumer
laptops. Checking, however, may fail, because ATP proof searches
are restricted by wallclock timeouts and depend significantly on system speed and state.
It may be necessary to increase the standard timeout of 3 seconds to X = 10, 20, or
more seconds by inserting \verb+[timelimit X]+ commands, which we have done
frequently. In stubborn cases, one has to insert further proof steps.}

\tableofcontents

\newpage

\section{Introduction}

The \Naproche{} system (for \emph{Natural Proof Checking})
checks the logical correctness of texts
written in an input language ForTheL (for \emph{Formula Theory Language})
which ideally reads like common mathematical language. Proofs and proof 
structures should resemble the
style of undergraduate textbooks. 
\Naproche{} is a \emph{natural proof assistant} intended to
approximate and support ordinary mathematical practices.
The inbuilt ontology of \Naproche{} corresponds to classical foundations
of mathematics in first-order logic and set theory.

\Naproche{} is included in the Isabelle prover environment: installing Isabelle
also installs \Naproche{}; opening files with a \verb+.ftl+ or \verb+.ftl.tex+
extension in Isabelle/jEdit automatically activates proof-checking by \Naproche{},
with feedback through the standard output buffer, highlighting, and
pop-up windows. The \Naproche{} installation contains a small library of
formalization examples. The current document is one of the examples, available
in \verb+.ftl.tex+ format for proof-checking and \LaTeX{} typesetting, and
as a typeset \verb+.pdf+ file.

This document serves several purposes: to demonstrate the 
\Naproche{} concept  within a longer formalization;
to propose a logical and set-theoretical foundation for
number systems in a build-up of mathematical notions
with sets and classes, maps, relations and numbers;
to prove several theorems from the well-known list of 100 theorems
that F. Wiedijk has proposed as formalization benchmarks \cite{Wiedijk}.
 
In our approach the ordered field $\mathbb{R}$ of real numbers
is postulated axiomatically. We then construe the structures of integer and
rational numbers as substructures of $\mathbb{R}$:
\[ \mathbb{R} \supseteq \mathbb{Q} \supseteq \mathbb{Z}
\supseteq \mathbb{N}. \]
This corresponds to the 
geometric intuition of a continuous line of numbers with
distinguished elements $0$ and $1$, from which integer and rational numbers can
be constructed. Technically, this has the advantage 
that real addition and multiplication
can be {\em restricted} to those substructures, instead of {\em extending} operations
to larger superstructures.

We list the ten "Wiedijk Theorems" contained in this document and
the authors of the respective formalizations. Most formalizations build on
earlier versions, also by other authors, some are inherited from 
\Naproche's predecessor system
SAD (for \emph{System for Automated Deduction}) by A. Paskevich 
and others \cite{SAD}. 
\begin{itemize}
\item \#1: The Irrationality of the Square Root of 2\\
Naproche formalization: Peter Koepke, Mateusz Marcol and Patrick Schäfer
\item \#11: The Infinitude of Primes\\
Peter Koepke
\item \#25: The Schröder-Bernstein Theorem\\
Peter Koepke, Marcel Schütz
\item \#52: Number of Subsets of a Set\\
Patrick Schäfer
\item \#60: Bezout's Identity\\
Mateusz Marcol, Patrick Schäfer
\item \#63: Cantor's Theorem\\
Peter Koepke
\item \#66: Sum of a Geometric Series\\
Peter Koepke
\item \#66: Sum of an Arithmetic Series\\
Peter Koepke
\item \#69: Greatest Common Divisor Algorithm\\
Mateusz Marcol, Patrick Schäfer
\item \#74: The Principle of Mathematical Induction\\
Peter Koepke
\end{itemize}
We shall continue to extend and improve the formalizations and upload
new versions for inclusion into future releases of Isabelle.

We view the present state of \Naproche{} and this paper as proof of 
concept for interactive theorem
proving with natural language formalizations. 
To extend \Naproche{} to a powerful comprehensive
system like Mizar or Isabelle should in principle be possible, 
given sufficient time and manpower.
We think, however, that it is more promising to equip established
system with a natural language interface by adapting 
\Naproche's translation techniques
from natural mathematical language texts into formal logics.

\section{Basic Notions}

Some notions and their elementary properties are already
built into \Naproche{} and its input language 
ForTheL. There are
mathematical {\em objects}, and {\em sets} and 
{\em classes} that contain mathematical
objects. Sets are classes which are objects themselves and
can thus be used in further mathematical constructions. 
{\em Functions}
and {\em maps} map objects to objects, where 
functions are those
maps which are themselves objects.

Modelling mathematical notions by objects corresponds
to the intuition that numbers, points, etc. should
not have internal set-theoretical
structurings, in contrast to purely set-theoretical
foundations of mathematics. This is also advantageous
for automated proving since it prevents proof searches to
dig into mathematically irrelevant internal structurings.

We begin by fixing some mathematical language. 
We import singular/plural forms of words that will be used in
our formalizations (\path{examples/vocabulary.ftl.tex}).
In the long run this should be replaced by
employing a proper English vocabulary. We also
import some alternative formulations for
useful mathematical phrases (\path{examples/macros.ftl.tex}).

\begin{forthel}
\begin{lemma} Let $x$ be a set. Then $x=x$. \end{lemma}
  [readtex \path{vocabulary.ftl.tex}]

  [readtex \path{macros.ftl.tex}]
\end{forthel}


On the basis of inbuilt assumptions we prove some 
lemmas that illustrate the \Naproche{} ontology. 
Later we shall postulate further axioms known from the
set theories of Kelley-Morse or Zermelo-Fraenkel.

The notions of set and class capture the naive intuition
of set expressed by Georg Cantor:
%
\begin{quotation}
\noindent A set is a collection of definite, distinguishable objects 
of perception or thought conceived as a whole. 
The objects are called elements or members of the set.
\end{quotation}
%
This is reflected formally in the following two lemmas, stating
that classes are built and determined by their
elements which are mathematical objects.

\begin{forthel}

\begin{proposition}
Let $X$ be a class. Let $x$ be an element of $X$.
Then $x$ is an object.
\end{proposition}

\begin{lemma}[Extensionality Axiom]
    Let $X, Y$ be classes.
    Assume that every element of $X$ is an element of $Y$ and every element of
    $Y$ is an element of $X$.
    Then $X = Y$.
\end{lemma}

\end{forthel}

Maps are also built into \Naproche{}, equipped with
domains and an application operator $\_ ( \_ )$.

\begin{forthel}
  \begin{lemma}
    Let $F$ be a map.
    Then $\dom(F)$ is a class.
  \end{lemma}

  \begin{lemma}
    Let $F$ be a map and $x$ be an element of $\dom(F)$.
    Then $F(x)$ is an object.
  \end{lemma}

  \begin{lemma}[Map Extensionality]
    Let $F, G$ be maps.
    Assume $\dom(F) = \dom(G)$ and for all elements $x$ of $\dom(F)$ we have
    $F(x) = G(x)$.
    Then $F = G$.
  \end{lemma}
\end{forthel}

Sets are those classes that are themselves objects.

\begin{forthel}
  \begin{lemma}
    Let $X$ be a set.
    Then $X$ is a class that is an object.
  \end{lemma}

  \begin{lemma}
    Let $X$ be a class that is an object.
    Then $X$ is a set.
  \end{lemma}
\end{forthel}
%
Similarly, functions are maps that are objects.
\begin{forthel}
  \begin{lemma}
    Let $F$ be a function.
    Then $F$ is a map that is an object.
  \end{lemma}

  \begin{lemma}
    Let $F$ be a map that is an object.
    Then $F$ is a function.
  \end{lemma}
\end{forthel}

\section{Classes}

Classes are usually defined by
abstraction terms $\{ ... \mid ... \}$. We indicate the
beginnings of a theory of classes which could be extended
much further.

\begin{forthel}
Let $S, T, U$ denote classes.

\begin{definition}
$\emptyset$ is the class that has no elements.
\end{definition}

Let the empty class stand for $\emptyset$.

\begin{definition}
${\cal V}$ is the class of all mathematical objects.
\end{definition}

Let the universe stand for ${\cal V}$.



\begin{definition}
$S$ is nonempty iff $S$ has an element.
\end{definition}

  \begin{definition}
    A subclass of $S$ is a class $T$ such that every $x \in T$ belongs to $S$.
  \end{definition}

  Let $T \subseteq S$ stand for $T$ is a subclass of $S$.

  \begin{definition}
    The union of $S$ and $T$ is $\class{x | x \in S \vee x \in T}$.
  \end{definition}

  Let $S \cup T$ stand for the union of $S$ and $T$.

  \begin{definition}
    The intersection of $S$ and $T$ is 
      $\class{x | x \in S \wedge x \in T}$.
  \end{definition}

  Let $S \cap T$ stand for the intersection of $S$ and $T$.

  \begin{definition}
    The set difference of $S$ and $T$ is $\class{x \in S | x \notin T}$.
  \end{definition}

  Let $S \setminus T$ stand for the set difference of $S$ and $T$.
\end{forthel}
These class operations satisfy algebraic properties of Boolean algebras
like the following distributive law:
\begin{forthel}

\begin{proposition}
Let $B,C,D$ be classes. Then
$B \cup (C \cap D) = (B \cup C) \cap (B \cup D)$.
\end{proposition}
\end{forthel}
%
We conclude with a few more definitions.
%
\begin{forthel}
  \begin{definition}
    $S$ is disjoint from $T$ iff there is no element of $S$ that is an element
    of $T$.
  \end{definition}

  \begin{definition}
    A family of sets is a class $A$ such that every element of 
$A$ is a set.
  \end{definition}

\begin{definition}
Let $A$ be a family of sets. The union of $A$
is $ \{x | x \in y$ for some $y \in A\}$.
\end{definition}

Let $\bigcup A$ stand for the union of $A$.


\begin{lemma}
Let $A,B,C$ be sets such that $C \subseteq A$ and $C \subseteq B$.
If $A \setminus C = B \setminus C$ then $A = B$.
\end{lemma}


\end{forthel}
%
\section{Maps}
%
\begin{forthel}

Let $F$ stand for maps.

\begin{definition}
A value of $F$ is an object $y$ such
that $F(x) = y$ for some $x \in \dom(F)$.
\end{definition}


  \begin{definition}
    Assume $S$ is a subclass of the domain of $F$.
    $F[S] = \class{F(x) | x \in S}$.
  \end{definition}

\begin{definition}
Let $F$ be a map. $\range(F) = F[\dom(F)]$.
\end{definition}


  Let the image of $F$ stand for $F[\dom(F)]$.

\begin{definition}
    A map from $S$ to $T$ is a map $F$ such that $\dom(F) = S$ 
and $F[S]  \subseteq T$.
  \end{definition}

Let $F : S \rightarrow T$ stand for $F$ is a map from $S$ to $T$.
%
\end{forthel}
%
There are canonical operations on maps.
%
\begin{forthel}
\begin{signature}
Let $F,G$ be maps such that $\range(G) \subseteq \dom(F)$.
$F \circ G$ is a map $H$ such that $\dom(H) = \dom(G)$ and
$H(x) = F(G(x))$ for all $x \in \dom(H)$.
\end{signature}

\begin{lemma}
Let $F,G,H$ be maps such that $\range(H) \subseteq \dom(G)$ and
$\range(G) \subseteq \dom(F)$.
Then $(F \circ G) \circ H = F \circ (G \circ H)$.
\end{lemma}
\begin{proof}
$\dom((F \circ G) \circ H) = \dom(H)$.
$\dom(G \circ H) = \dom(H)$. Let $U = G \circ H$.
$$\dom(F \circ (G \circ H)) = 
\dom(F \circ U) = \dom(U) = \dom(G \circ H) = \dom(H).$$

For every $x \in \dom(H)$ we have  
$$((F \circ G) \circ H)(x) = F(G(H(x))) =
(F \circ (G \circ H))(x).$$
\end{proof}

\begin{signature}
$Id$ is the map such that $\dom(Id) = {\cal V}$
and $Id(x) = x$ for all $x \in {\cal V}$.
\end{signature}

\begin{lemma}
$Id : {\cal V} \rightarrow {\cal V}$.
\end{lemma}

\begin{lemma}
Let $F$ be a map. Then $Id \circ F = F$.
\end{lemma}
\begin{proof} Consider $G = Id \circ F$.
$\dom(Id \circ F) = \dom(F)$.
$((Id \circ F))(x) = F(x)$ for all $x \in \dom(F)$.
\end{proof}

\begin{signature}
Let $F$ be a map and $A$ be a class.
$F\upharpoonright A$ is the map $G$ such that
$\dom(G) = \dom(F) \cap A$ and $G(x)=F(x)$
for all $x \in \dom(G)$.
\end{signature}

\begin{lemma}
Let $F$ be a map. Then $F \circ (Id \upharpoonright \dom(F)) = F$.
\end{lemma}
\begin{proof} Consider $I = Id \upharpoonright \dom(F)$.
$\dom(F \circ (Id \upharpoonright \dom(F))) = 
\dom(F \circ I) = \dom(I) = \dom(F)$.
$(F \circ (Id \upharpoonright \dom(F)))(x) = F(x)$ 
for all $x \in \dom(F)$.
\end{proof}

\end{forthel}
We distinguish several important kinds of maps.
%
\begin{forthel}
\begin{definition}
A surjection from $S$
onto $T$ is a map $f$ from $S$ to $T$ such that $f[S] = T$.
\end{definition}

\begin{definition}
Let $f$ be a map. $f$ is injective iff $f(x) \neq f(y)$ for all
distinct elements $x,y$ of $\dom(f)$.
\end{definition}

\begin{lemma}
$Id$ is an injective surjection from ${\cal V}$ onto ${\cal V}$.
\end{lemma}

\begin{lemma}
Let $F,G$ be injective maps such that $\range(F) \subseteq \dom(G)$.
Then $G \circ F$ is injective.
\end{lemma}

\begin{lemma} Let $S,T,U$ be classes. Let 
$F$ be a surjection from $S$ onto $T$ and $G$ be
a surjection from $T$ onto $U$. Then
$G \circ F$ is a surjection from $S$ onto $U$.
\end{lemma}

\begin{signature}
Let $F$ be an injective map.
$\inv{F}$ is the map $G$ such that $\dom(G) = \range(F)$
and for all $v \in \dom(G)$ $G(v) \in \dom(F)$ and $F(G(v))=v$.
\end{signature}

\begin{lemma}
Let $F$ be an injective map. Then 
$\inv{F} : \range(F) \rightarrow \dom(F)$.
\end{lemma}


\begin{definition}
A bijection between $S$ and $T$ is an injective surjection from
$S$ onto $T$.
\end{definition}

\begin{lemma} Let $S, T$ be classes.
Let $F$ be a bijection between $S$ and $T$.
Then $\inv{F}$ is a bijection between $T$ and $S$.
\end{lemma}
\end{forthel}
%
\section{Equinumerosity}
%
Bijective maps and functions are the basis for cardinality
theory.
%
\begin{forthel}
\begin{definition}
Let $S, T$ be classes.
$S$ and $T$ are equinumerous iff there exists a bijection between $S$ and
$T$.
\end{definition}

Let $S \sim T$ stand for $S$ and $T$ are equinumerous.
\end{forthel}
%
We show that equinumerosity is an equivalence relation on classes and
in particular on sets.
%
\begin{forthel}

\begin{lemma}
$S \sim S$.
\end{lemma}
\begin{proof}
$Id \upharpoonright S : S \rightarrow S$.
$Id \upharpoonright S$ is injective.
$Id \upharpoonright S$ is a surjection from $S$ onto $S$.
\end{proof}

\begin{lemma}
Assume that $S \sim T$. Then $T \sim S$.
\end{lemma}

\begin{lemma}
Assume that $S \sim T \sim U$. Then $S \sim U$.
\end{lemma}

\begin{lemma}
Let $A,B,C,D$ be classes such that $A$ and $B$ are disjoint and 
$C$ and $D$ are disjoint. Assume that $A \sim C$ and $B \sim D$.
Then $A \cup B \sim C \cup D$.
\end{lemma}
\begin{proof}
Take a bijection $F$ between $A$ and $C$.
Take a bijection $G$ between $B$ and $D$.

Define \[ H(x) =
          \begin{cases}
            F(x) & : x \in A \\
            G(x) & : x \in B
          \end{cases} \]
        for $x \in A \cup B$.

$H$ is a map from $A \cup B$ to $C \cup D$.
$H$ is a bijection between $A \cup B$ and $C \cup D$.
\end{proof}

\end{forthel}

\section{Set-Theoretic Axioms}

Many classes defined in mathematics are considered to be
mathematical objects that can be used freely in further constructions.
We defined sets to be classes that are objects. However, we cannot
identify {\em all} classes with sets due to the famous 
Russell's paradox \cite{Russell}.
The proof is based on the important {\em diagonal argument}.

\begin{forthel}

\begin{theorem}[Russell]
There is a class that is not a set.
\end{theorem}
\begin{proof}
Define $$R = \{x |\text{$x$ is a set and $x \notin x$}\}.$$
$R$ is not a set.
Indeed if $R$ is a set then $$R \in R \iff R \notin R.$$
\end{proof}
\end{forthel}

As a reaction to Russell's theorem, Ernst Zermelo, Abraham
Fraenkel and others have formulated axioms which 
postulate explicitly that certain classes are sets. We
present the standard axioms without
the axioms of infinity, choice and foundation. The infinity
axiom will be introduced later by requiring that the 
(infinite) class
of natural numbers is a set. The axioms of choice 
and foundation are not needed for our presentation.
Note that the axiomatic strength introduced here corresponds
to Kelley-Morse set theory, since classes can be formed using
formulas with class quantifiers.
We begin by restating
the axiom of extensionality.

\begin{forthel}
\begin{lemma}[Extensionality Axiom]
    Let $X, Y$ be classes.
    Assume that every element of $X$ is an element of $Y$ and every element of
    $Y$ is an element of $X$.
    Then $X = Y$.
\end{lemma}

\begin{axiom}[Set Existence Axiom]
The empty class is a set.
\end{axiom}

\begin{axiom}[Pairing Axiom]
Let $a,b$ be objects. Let $P = \{a,b\}$. Then $P$  is a set.
\end{axiom}

\begin{axiom}[Union Axiom]
Let $F$ be a set that is a family of sets. Then
$\bigcup F$ is a set.
\end{axiom}

\begin{axiom}[Separation Axiom]
    Assume that $X$ is a set and $T$ is a subclass of $X$.
    Then $T$ is a set.
\end{axiom}

\begin{definition}
A subset of $S$ is a set $X$ such that $X \subseteq S$.
\end{definition}

\begin{definition}
      Let $X$ be a set.
      The powerset of $X$ is the collection of subsets of $X$.
\end{definition}

Let $\pow(X)$ denote the powerset of $X$.

\begin{axiom}[Powerset Axiom]
  The powerset of any set is a set.
\end{axiom}

\begin{axiom}[Replacement Axiom]
Let $F$ be a function.    
Let $X$ be a subset of the domain of $F$.
Then $F[X]$ is a set.
\end{axiom}
\end{forthel}

The treatment of functions and maps is similar to that
of sets and classes, and we can postulate function-theoretic
axioms like:

\begin{forthel}
  \begin{axiom}
    Assume that $f$ is a map and $\dom(f)$ is a set.
    Then $f$ is a function.
  \end{axiom}
\end{forthel}

\section{Ordered Pairs and Products}

Since we prefer objects over sets if possible, we do not work
with Kuratowski-style set-theoretical ordered pairs, but
introduce them as objects. 
\begin{forthel}
  \begin{lemma}
    Let $x, y$ be objects.
    Then $(x,y)$ is an object.
  \end{lemma}
\end{forthel}
%
The universal property of ordered pairs is postulated as
and axiom.
%
\begin{forthel}
  \begin{axiom}
    For any objects $a, b, c, d$ if $(a,b) = (c,d)$ then $a = c$ and $b = d$.
  \end{axiom}
\end{forthel}
This allows to work with cartesian products. One could show
from the Zermelo-Fraenkel axioms that $X \times Y$ is a set
whenever $X$ and $Y$ are sets. But it is easier to postulate
that as an axiom.
% 
\begin{forthel}
  \begin{definition}
    $S \times T = \class{(x,y) | \text{$x \in S$ and $y \in T$}}$.
  \end{definition}

  \begin{axiom}
    Let $X, Y$ be sets.
    Then $X \times Y$ is a set.
  \end{axiom}

  \begin{lemma}
    Let $x, y$ be objects.
    If $(x,y)$ is an element of $S \times T$ then $x$ is an element of $S$ and
    $y$ is an element of $T$.
  \end{lemma}

\end{forthel}



\section{Cantor's Theorem (\#63)}

Despite its technical simplicity, Cantor's Theorem is the origin of
infinitary and uncountable set theory. The diagonal argument of
its proof has become a powerful and standard proof principle mainly
in foundational theories.

\begin{forthel}
    \begin{theorem*}[Cantor]
      Let $M$ be a set. Then there is 
      no surjection from $M$ onto the powerset of $M$.
    \end{theorem*}
    \begin{proof}
      Assume the contrary.
      Take a surjection $f$ from $M$ onto the powerset of $M$.
      Define \[ N = \class{x \in M | \text{$x$ is not an element of $f(x)$}}. \]
      Take an element $z$ of $M$ such that $f(z) = N$.
      Then \[ z \in N \iff z \notin f(z) = N. \]
      Contradiction.
    \end{proof}
\end{forthel}



\section{The Knaster-Tarski Fixed Point Theorem}

The Knaster-Tarski theorem is an important result in lattice theory \cite{Tarski, Knaster}.
We prove the theorem for 
the $\subseteq$-relation on sets, in order to apply it
in the subsequent section.

 \begin{forthel}
    \begin{definition}
      Let $h$ be a map.
      A fixed point of $h$ is an element $u$ of $\dom(h)$ such that $h(u) = u$.
    \end{definition}

    \begin{definition}
      A map between families of sets is a map from some family of 
sets to some
      family of sets.
    \end{definition}

    \begin{definition*}
Let $h$ be a map between families of sets.
      $h$ preserves subsets iff for all $u, v \in \dom(h)$
      we have \[ u \subseteq v \implies h(u) \subseteq h(v). \]
    \end{definition*}


    \begin{theorem*}[Knaster-Tarski]\label{KT}
      Let $x$ be a set.
      Let $h$ be a map from $\pow(x)$ to $\pow(x)$ that preserves subsets.
      Then $h$ has a fixed point.
    \end{theorem*}
    \begin{proof}
      Define $A = \class{y | \text{$y \subseteq x$ and
      $y \subseteq h(y)$}}$.
[timelimit 10]
      Then $A$ is a subset of $\pow(x)$ and
      $\bigcup A \in \pow(x)$.
[timelimit 3] 

(1) $\bigcup A \subseteq h(\bigcup A)$.

Proof.        Let $u \in \bigcup A$.
        Take $y \in A$ such that $u \in y$.
        Then $u \in h(y) \subseteq h(\bigcup A)$.
      qed.

(2) $h(\bigcup A) \subseteq \bigcup A$.

Proof.      $h(\bigcup A) \subseteq x$.
$h(\bigcup A) \subseteq h(h(\bigcup A))$.
$h(\bigcup A) \in A$.
Thus $h(\bigcup A) \subseteq \bigcup A$.
qed.

Then $\bigcup A$ is a fixed point of $h$ (by 1, 2).
    \end{proof}

\end{forthel}

\section{The Schröder-Bernstein Theorem (\#25)}

The Schröder-Bernstein theorem, also called the
Cantor-Schröder-Bernstein theorem, is important for developing
the theory of infinite cardinals without the axiom of choice.
We base the proof on the Tarski-Knaster theorem, following
 \cite[p. 530]{Schroeder2012}.

 \begin{forthel}

   \begin{theorem*}[Cantor-Schröder-Bernstein]\label{CSB}
      Let $x,y$ be sets.
      $x$ and $y$ are equinumerous iff there exists a injective map from $x$ to
      $y$ and there exists an injective map from $y$ to $x$.
    \end{theorem*}
    \begin{proof}
      Case $x$ and $y$ are equinumerous.
        Take a bijection $f$ between $x$ and $y$.
        Then $\inv{f}$ is a bijection between $y$ and $x$.
        Hence $f$ is an injective map from $x$ to $y$ and $\inv{f}$ is an
        injective map from $y$ to $x$.
      End.

      Case there exists an injective map from $x$ to $y$ and there exists an
      injective map from $y$ to $x$.
        Take an injective map $f$ from $x$ to $y$.
        Take an injective map $g$ from $y$ to $x$.
        We have $y \setminus f[a] \subseteq y$ for any $a \in \pow(x)$.

        (1) Define $h(a) = x \setminus g[y \setminus f[a]]$ for $a \in \pow(x)$.

        $h$ is a map from $\pow(x)$ to $\pow(x)$.
        Indeed $h(a)$ is a subset of $x$ for each subset $a$ of $x$.

        Let us show that $h$ preserves subsets.
          Let $u, v$ be subsets of $x$. $u,v \in \pow(x)$.
          Assume $u \subseteq v$.
          Then $f[u] \subseteq f[v]$.
          Hence $y \setminus f[v] \subseteq y \setminus f[u]$.
          Thus $g[y \setminus f[v]] \subseteq g[y \setminus f[u]]$.
          Indeed $y \setminus f[v]$ and $y \setminus f[u]$ are subsets of $y$.
          Therefore $x \setminus g[y \setminus f[u]] \subseteq
          x \setminus g[y \setminus f[v]]$.
          Consequently $h(u) \subseteq h(v)$. 
        End.

        Hence we can take a fixed point $c$ of $h$ (by \nameref{KT}).

        (2) Define $F(u) = f(u)$ for $u \in c$.

        We have $c = h(c)$ iff $x \setminus c = g[y \setminus f[c]]$.
        $\inv{g}$ is a bijection between $\range(g)$ and $y$.
        Thus $x \setminus c = g[y \setminus f[c]] \subseteq \range(g)$.
        Therefore $x \setminus c$ is a subset of $\dom(\inv{g})$.

        (3) Define $G(u) = \inv{g}(u)$ for $u \in x \setminus c$.

        $F$ is a bijection between $c$ and $\range(F)$.
        $G$ is a bijection between $x \setminus c$ and $\range(G)$.

        Define \[ H(u) =
          \begin{cases}
            F(u) & : u \in c \\
            G(u) & : u \notin c
          \end{cases} \]
        for $u \in x$.

        Let us show that $H$ is a map from $x$ to $y$.
          $\dom(H)$ is a set.
          Hence $H$ is a map.

          Let us show that every value of $H$ is an element of $y$.
            Let $v$ be a value of $H$.
            Take $u \in x$ such that $H(u) = v$.
            If $u \in c$ then $v = H(u) = F(u) = f(u) \in y$.
            If $u \notin c$ then $v = H(u) = G(u) = \inv{g}(u) \in y$.
          End.
        End.

        (4) $H$ is a surjection from $x$  onto $y$.
        Indeed we can show that every element of $y$ is a value of $H$.
          Let $v \in y$.

          Case $v \in f[c]$.
            Take $u \in c$ such that $f(u) = v$.
            Then $F(u) = v$.
          End.

          Case $v \notin f[c]$.
            Then $v \in y \setminus f[c]$.
            Hence $g(v) \in g[y \setminus f[c]]$.
            Thus $g(v) \in x \setminus h(c)$.
            We have $g(v) \in x \setminus c$.
            Therefore we can take $u \in x \setminus c$ such that $G(u) = v$.
            Then $v = H(u)$.
          End.
        End.

        (5) $H$ is injective.
        Indeed we can show that for all $u, v \in x$ if $u \neq v$ then
        $H(u) \neq H(v)$.
          Let $u,v \in x$.
          Assume $u \neq v$.

          Case $u,v \in c$.
            Then $H(u) = F(u)$ and $H(v) = F(v)$.
            We have $F(u) \neq F(v)$.
            Hence $H(u) \neq H(v)$.
          End.

          Case $u,v \notin c$.
            Then $H(u) = G(u)$ and $H(v) = G(v)$.
            We have $G(u) \neq G(v)$.
            Hence $H(u) \neq H(v)$.
          End.

          Case $u \in c$ and $v \notin c$.
            Then $H(u) = F(u)$ and $H(v) = G(v)$.
            Hence $v \in g[y \setminus f[c]]$.
            We have $G(v) \in y \setminus F[c]$.
            Thus $G(v) \neq F(u)$.
          End.

          Case $u \notin c$ and $v \in c$.
            Then $H(u) = G(u)$ and $H(v) = F(v)$.
            Hence $u \in g[y \setminus f[c]]$.
            We have $G(u) \in y \setminus f[c]$.
            Thus $G(u) \neq F(v)$.
          End.
        End.

        Consequently $H$ is a bijection between $x$ and $y$ (by 4, 5).
        Therefore $x$ and $y$ are equinumerous.
      End.
    \end{proof}
  \end{forthel}

\section{The Real Field}

We introduce the real numbers with their  
arithmetical operations and postulate that
they satisfy standard field axioms. This is a partial
axiomatisation.
Only after the introduction
of further axioms that specify the nested number systems
\[ \mathbb{R} \supseteq \mathbb{Q} \supseteq \mathbb{Z}
\supseteq \mathbb{N}. \]
and the relations between the numbersystems will it be clear 
that the reals introduced along this paper are isomorphic to
the standard reals as completion of the rational numbers.

\begin{forthel}

\begin{signature}
A real number is a mathematical object.
\end{signature}

\begin{definition}
$\mathbb{R}$ is the collection of real numbers.
\end{definition}

\begin{axiom}
$\mathbb{R}$ is a set.
\end{axiom}
\end{forthel}
%
Note that this axiom does not yet imply the existence of infinite sets,
since under the axioms in this section $\mathbb{R}$ could still be some finite 
field. The following are standard axioms for commutative fields, where the
additive and multiplicative inverses are given by functions 
$x \mapsto -x$ and $x \mapsto 1/x$. 
%
\begin{forthel}
Let $x,y,z,w$ denote real numbers.

\begin{signature}
$x + y$ is a real number.
\end{signature}
Let the sum of $x$ and $y$ denote $x + y$.

\begin{signature}
$x \cdot y$ is a real number.
\end{signature}
Let the product of $x$ and $y$ denote $x \cdot y$.

\begin{axiom}
$x + y = y + x$.
\end{axiom}

\begin{axiom}
$(x + y) + z = x + (y + z)$.
\end{axiom}

\begin{signature}
$0$ is a real number such that
for every real number $x$ $x + 0 = x$.
\end{signature}

\begin{signature}
$-x$ is a real number such that $x + (-x) = 0$.
\end{signature}

\begin{axiom}
$x \cdot y = y \cdot x$.
\end{axiom}

\begin{axiom}
$((x \cdot y)) \cdot z = x \cdot (y \cdot z)$.
\end{axiom}

\begin{signature}
$1$ is a real number such that $1 \neq 0$ and
for every real number $x$ $1 \cdot x = x$.
\end{signature}

\begin{signature}
Assume $x \neq 0$. $1/x$ is a real number
such that $x \cdot (1/x) = 1$.
\end{signature}

Let $x$ is nonzero stand for $x \neq 0$.

\begin{axiom}
$x \cdot (y + z) = (x \cdot y) + (x \cdot z)$.
\end{axiom}
\end{forthel}
We continue by proving some consequencen of the axioms.
The selection of lemmas follows the
{\em Foundations of Real Analysis} by Walter Rudin \cite{Rudin}.
Note that in rare cases we need to use double brackets 
$((\dots))$ because
of some parser bug.
\begin{forthel}
\begin{proposition}
$((y \cdot x)) + (z \cdot x) = (y + z) \cdot x$.
\end{proposition}

\begin{proposition}
Let $x + y = x + z$. Then $y = z$.
\end{proposition}
\begin{proof}
$y = -x + (x+y) = -x + (x+z) = z$.
\end{proof}

\begin{proposition}
If $x + y = x$ then $y = 0$.
\end{proposition}

\begin{proposition}
If $x + y = 0$ then $y = -x$.
\end{proposition}

\begin{proposition}
$-(-x) = x$.
\end{proposition}


\begin{proposition}
Let $x$ be nonzero and $x \cdot y = x \cdot z$.
Then $y = z$.
\end{proposition}
\begin{proof}
$ y = ((1/x) \cdot x) \cdot y = (1/x) \cdot (x \cdot y) =
(1/x) \cdot (x \cdot z) = ((1/x) \cdot x) \cdot z = z.$
\end{proof}

\begin{proposition}
If $x$ is nonzero and $x \cdot y = x$ then $y = 1$.
\end{proposition}

\begin{proposition}
If $x$ is nonzero and $x \cdot y = 1$ then $y = 1/x$.
\end{proposition}

\begin{proposition}
If $x$ is nonzero then $1/(1/x) = x$.
\end{proposition}

\begin{proposition}
$0 \cdot x = 0$.
\end{proposition}

\begin{proposition}
If $x$ is nonzero and $y \neq 0$ then $x \cdot y \neq 0$.
\end{proposition}

\begin{proposition}
$(-x) \cdot y = -(x \cdot y)$.
\end{proposition}
\begin{proof}
$((x \cdot y)) + (-x \cdot y) = (x + (-x)) \cdot y
= 0 \cdot y = 0$.
\end{proof}

\begin{proposition}
$-x = -1 \cdot x$.
\end{proposition}

\begin{proposition}
$(-x) \cdot (-y) = x \cdot y$.
\end{proposition}
\begin{proof}
$(-x)\cdot (-y) = -(x\cdot(-y)) = -((-y)\cdot x) =
-(-(y\cdot x)) = y\cdot x = x\cdot y$.
\end{proof}
\end{forthel}
%
\begin{forthel}
Let $x - y$ stand for $x + (-y)$.
Let $\frac{x}{y}$ stand for $x \cdot (1/y)$.
\end{forthel}
%
We prove some lemmas for later use.
%
\begin{forthel}
\begin{lemma} Let $z \neq 0$. Then
$x = \frac{z \cdot x}{z}$.
\end{lemma}

\begin{lemma}
$(1 - x) \cdot y = y - (x \cdot y)$.
\end{lemma}
\begin{proof}
$(1 - x) \cdot y = y + ((-x) \cdot y) = y - (x \cdot y)$.
\end{proof}

\begin{lemma} Let $w \neq 0$. Then
$\frac{x - y}{w} + \frac{y - z}{w} = \frac{x - z}{w}$.
\end{lemma}
\begin{proof}
$(x - y) + (y - z) = ((x - y) + y) - z = x - z$.
\end{proof}

\begin{lemma}
$-(x + y) = -x - y$.
\end{lemma}
\begin{proof}
$(x + y) + (-x - y) = (x - x) + (y - y) = 0.$
\end{proof}

\end{forthel}

\section{Some Numbers}

We introduce the standard notations for small natural numbers.
Under the axioms so far, we could still have that$0 = 3$ because
we could be working in a field of characteristic $3$.

\begin{forthel}

\begin{definition}
$2 = 1 + 1$.
\end{definition}

\begin{definition}
$3 = 2 + 1$.
\end{definition}

\begin{definition}
$4 = 3 + 1$.
\end{definition}

\begin{definition}
$5 = 4 + 1$.
\end{definition}

\begin{definition}
$6 = 5 + 1$.
\end{definition}

\begin{definition}
$7 = 6 + 1$.
\end{definition}

\begin{definition}
$8 = 7 + 1$.
\end{definition}

\begin{definition}
$9 = 8 + 1$.
\end{definition}

\begin{definition}
$10 = 9 + 1$.
\end{definition}

\begin{lemma}
$0,1,2,3,4,5,6,7,8,9,10$ are real numbers.
\end{lemma}

\end{forthel}
%
With these numbers we can prove some small "decimal arithmetic":
\begin{forthel}
%
\begin{lemma}
$2 + 5 = 7$.
\end{lemma}

\begin{lemma}
$2 \cdot 5 = 10$.
\end{lemma}

\begin{lemma}
$5 \cdot 5 = (2 \cdot 10) + 5$.
\end{lemma}

\begin{lemma} Assume that $6 \neq 0$. Then
$\frac{1}{2} + \frac{1}{3} = \frac{5}{6}$.
\end{lemma}
\begin{proof}
$\frac{1}{2} + \frac{1}{3} = \frac{3}{6} + \frac{2}{6} = \frac{5}{6}$.
\end{proof}
\end{forthel}
The assumption $6 \neq 0$ makes
the fractions well-defined. Note that $6 \neq 0$ implies
that $2,3 \neq 0$.


\section{The Real Ordered Field}

We first introduce the weak order $\leq$ on $\mathbb{R}$ 
instead of
the strong orders $<$. Although these orders are easily
interdefinable, the choice can noticably influence automatic
proof searches. $\leq$ is a linear order:

\begin{forthel}

\begin{signature}
$x \leq y$ is an atom.
\end{signature}

Let $x \nleq y$ stand for not $x \leq y$.

Let $x \geq y$ stand for $y \leq x$.

\begin{axiom}
$x \leq x$.
\end{axiom}

\begin{axiom}
If $x \leq y$ and $x \geq y$ then $x=y$.
\end{axiom}

\begin{axiom}
If $x \leq y$ and $y \leq z$ then $x \leq z$.
\end{axiom}

\begin{axiom}
$x \leq y$ or $x \geq y$.
\end{axiom}

\end{forthel}
The order makes $\mathbb{R}$ an ordered field:
\begin{forthel}
\begin{axiom}
If $y \leq z$ then $x + y \leq x + z$ and $y + x \leq z + x$.
\end{axiom}

\begin{axiom}[1 17 ii]
If $x \geq 0$ and $y \leq z$ then $x \cdot y \leq x \cdot z$.
\end{axiom}
\end{forthel}
We define the strict order as an abbreviation.
\begin{forthel}
Let $x < y$ stand for $x \leq y$ and $x \neq y$.
Let $x \nless y$ stand for not $x < y$.
Let $x > y$ stand for $y < x$.

\begin{definition}
$x$ is positive iff $x > 0$.
\end{definition}

\begin{definition}
$x$ is negative iff $x < 0$.
\end{definition}

\begin{definition}
$x$ is nonnegative iff $x \geq 0$.
\end{definition}

\begin{lemma}
$x \leq y$ iff $y \nless x$.
\end{lemma}
\end{forthel}
We prove some lemmas, following Rudin \cite{Rudin}.
\begin{forthel}

\begin{lemma}0=0.\end{lemma}

\begin{proposition}
$x > 0$ iff $-x < 0$.
\end{proposition}

[timelimit 10] %%%
\begin{proposition}
If $x \neq 0$ then $x \cdot x > 0$.
\end{proposition}
[timelimit 3]

\begin{proposition}
$1 > 0$.
\end{proposition}

\begin{proposition}
$x \leq y$ iff $-x \geq -y$.
\end{proposition}
\begin{proof}
$x \leq y$ iff $x - y \leq 0$.  
$x - y \leq 0$ iff $-y = -x + (x - y) \leq -x$.
\end{proof}

\begin{proposition}
If $x < 0$ and $y < z$ then
$x \cdot y > x \cdot z$.
\end{proposition}
\begin{proof}
Let $x < 0$ and $y < z$.
$-x > 0$.
$(-x)\cdot y < (-x)\cdot z$.
$-(x\cdot y) < -(x\cdot z)$.
\end{proof}

\begin{proposition}
$-1 < 0$.
\end{proposition}

\begin{proposition}
$x - 1 < x$.
\end{proposition}

\begin{proposition}
$x < y < x + 1$ iff $0 < y - x < 1$.
\end{proposition}
\begin{proof}
$x < y$ iff $0 = x - x < y - x$.
$y < x + 1$ iff $y - x < (x + 1) - x = 1$.
\end{proof}

\begin{proposition}
If $0 < y$ then $0 < 1/y$.
\end{proposition}

\begin{lemma} 0=0. \end{lemma}

\begin{lemma}[syz]
If not $x \leq y$ then $x \geq y$.
\end{lemma}

\begin{proposition}
Assume $0 < x \leq y$.
Then $1/y \leq 1/x$.
\end{proposition}
\begin{proof}[by contradiction]
Assume the contrary. 
Then not $1/y \leq 1/x$. Let $u = 1/y$ and $v = 1/x$.
Then $1/y \geq 1/x$.
Then $1/x < 1/y$.
Then
\[ 1 = x \cdot (1/x) = (1/x) \cdot x \leq (1/x) \cdot y =
y \cdot (1/x) < y \cdot (1/y) = 1. \]
Hence $1 < 1$. Contradiction.
\end{proof}

\end{forthel}


\section{Upper and lower bounds}

The real numbers are {\em complete}, which is often expressed
via Dedekind cuts or Cauchy sequences. Here
we use suprema and infima instead. We make the 
necessary definitions. 

\begin{forthel}

Let $E$ denote a subset of $\mathbb{R}$.

\begin{definition}
An upper bound of $E$ is a
real number $b$ such that for all elements $x$ of $E$ $x \leq b$.
\end{definition}

\begin{definition}
$E$ is bounded above iff
$E$ has an upper bound.
\end{definition}

\begin{definition}
A lower bound of $E$ is a
real number $b$ such that for all elements $x$ of $E$ $x \geq b$.
\end{definition}

\begin{definition}
$E$ is bounded below iff
$E$ has a lower bound.
\end{definition}

\begin{definition}
A supremum of $E$ is a real number $a$ such that
$a$ is an upper bound of $E$ and for all $x$ if $x < a$ then $x$
is not an upper bound of $E$.
\end{definition}

\begin{definition}
Let $E$ be bounded below.
An infimum of $E$ is a real number $a$ such that
$a$ is a lower bound of $E$ and for all $x$ if $x > a$ then $x$ is
not a lower bound of $E$.
\end{definition}
\end{forthel}
%
The crucial completeness axiom now reads:
%
\begin{forthel}
\begin{axiom}
Assume that $E$ is nonempty and bounded above.
Then $E$ has a supremum.
\end{axiom}
\end{forthel}
%
By symmetry, the existence of suprema implies the existence 
of infima.
%
\begin{forthel}
\begin{definition}
$E^- = \{-x \in \mathbb{R} \mid x \in E\}$.
\end{definition}

\begin{lemma}
$E^-$ is a subset of $\mathbb{R}$.
\end{lemma}
[timelimit 5]
\begin{lemma}
$x$ is an upper bound of $E$ iff $-x$ is a lower bound of $E^-$.
\end{lemma}
[timelimit 3]

\begin{theorem} Assume that $E$ is a nonempty subset of $\mathbb{R}$
such that $E$ is bounded below.
Then $E$ has an infimum.\end{theorem}
\begin{proof}
Take a lower bound $a$ of $E$.
$-a$ is an upper bound of $E^-$.
Take a supremum $b$ of $E^-$.

(1) $-b$ is an infimum of $E$.

Proof.
$-b$ is a lower bound of $E$. 
Let $c$ be a lower bound of $E$.
Then $-c$ is an upper bound of $E^-$.
Hence $b \leq -c$ and $c \leq -b$. 
qed.
\end{proof}
\end{forthel}


\section{The rational numbers}

We introduce the rational numbers
as a subfield of $\mathbb{R}$.

\begin{forthel}
\begin{signature}
A rational number is a real number.
\end{signature}

Let $p,q,r$ denote rational numbers.

\begin{definition}
$\mathbb{Q}$ is the collection of rational numbers.
\end{definition}

\begin{theorem}
$\mathbb{Q}$ is a subset of $\mathbb{R}$.
\end{theorem}
\end{forthel}
%
In particular, $\mathbb{Q}$ is a set.
We now stipulate that $\mathbb{Q}$ is closed under the
field operations of $\mathbb{R}$.
%
\begin{forthel}
\begin{axiom}
$0,1$ are rational numbers.
\end{axiom}

Let $p,q$ denote rational numbers.

\begin{axiom}
$p + q$, $p \cdot q$ are rational numbers.
\end{axiom}

\begin{axiom}
$-p$ is a rational number.
\end{axiom}

\begin{axiom}
Assume that $p \neq 0$. Then
$1/p$ is a rational number.
\end{axiom}
\end{forthel}
%
The reals are "generated" from 
the rationals by suprema (or infima). We postulate:
%
\begin{forthel}
\begin{axiom} Let $x$ be a real number.
Then there exists a subset $A$ of $\mathbb{Q}$
such that $A$ is bounded above and
$x$ is the supremum of $A$.
\end{axiom}

\begin{theorem}
$\mathbb{R} = \{x \in \mathbb{R} \mid$ there exists $
A \subseteq \mathbb{Q}$ such that $
A$ is bounded above and $x$ is the supremum of $A\}$.
\end{theorem}
\end{forthel}


\section{Integers}

$\mathbb{Z}$ is introduced as a subring of $\mathbb{Q}$:

\begin{forthel}

\begin{signature}
An integer is a rational number.
\end{signature}

\begin{definition}
$\mathbb{Z}$ is the collection of integers.
\end{definition}

\begin{lemma}
$\mathbb{Z} \subseteq \mathbb{Q} \subseteq \mathbb{R}$.
\end{lemma}

\begin{lemma}
$\mathbb{Z}$ is a set.
\end{lemma}
\end{forthel}
%
$\mathbb{Z}$ is closed under $+$, $\cdot$ and $-$.
%
\begin{forthel}
\begin{axiom}
$0,1$ are integers.
\end{axiom}

Let $a,b$ denote integers.

\begin{axiom}
$a + b$, $a \cdot b$ are integers.
\end{axiom}

\begin{axiom}
$-a$ is an integer.
\end{axiom}
\end{forthel}
%
The axioms up to now are consistent with the unintended
equality $\mathbb{Z} = \mathbb{Q} = \mathbb{R}$. The following
two axioms are crucial to obtain the standard number systems.
$\mathbb{Z}$ is a {\em discrete} ring:
%
\begin{forthel}
\begin{axiom}
There is no integer $a$ such that $0 < a < 1$.
\end{axiom}
\end{forthel}
%
But the discrete ring generates the rationals by fractions:
%
\begin{forthel}
\begin{axiom} Let $p$ be a rational number. Then
there exist integers $m, n$ such that
$n \neq 0$ and $p = \frac{m}{n}$.
\end{axiom}
[timelimit 5]
\begin{lemma}
$$\mathbb{Q} = 
\{\frac{m}{n} \mid m,n \in \mathbb{Z} \wedge n \neq 0\}.$$
\end{lemma}
\begin{proof}
$\frac{m}{n} \in \mathbb{Q}$ where $m,n$ are integers and
$n \neq 0$.
\end{proof}
[timelimit 3]
\end{forthel}
%
Although $\mathbb{Z}$ is a small, indeed countable subring
of $\mathbb{R}$, it is somehow "large" in $\mathbb{R}$.
%
\begin{forthel}

\begin{theorem}[Archimedes1]
$\mathbb{Z}$ is not bounded above.
\end{theorem}
\begin{proof}
Assume the contrary.
$\mathbb{Z}$ is nonempty. Indeed $0$ is an integer.
Take a supremum
$b$ of $\mathbb{Z}$.
Let us show that $b - 1$ is an upper bound of $\mathbb{Z}$.
Let $x \in \mathbb{Z}$. $x + 1 \in \mathbb{Z}$.
$x + 1 \leq b$.
$x = (x + 1) - 1 \leq b - 1$.
End.
\end{proof}

\begin{theorem}
$\mathbb{Z}$ is not bounded below.
\end{theorem}
\begin{proof}
Assume the contrary.
Take a real number $x$ that is a lower bound of $\mathbb{Z}$.
Then $-x$ is an upper bound of $\mathbb{Z}$.
Contradiction.
\end{proof}

\begin{theorem}[Archimedes2]
Let $x$ be a real number.
Then there is an integer $a$
such that $x < a$.\end{theorem}
\begin{proof}[by contradiction]
Assume the contrary.
Then $x$ is an upper bound of $\mathbb{Z}$.
Contradiction.
\end{proof}

\end{forthel}

\section{The natural numbers}

Finally we have descended to the natural numbers.

\begin{forthel}

\begin{definition}
A natural number is a nonnegative integer.
\end{definition}

\begin{definition}
$\mathbb{N}$ is the collection
of natural numbers.
\end{definition}

\begin{lemma}
$\mathbb{N} \subseteq \mathbb{Z} \subseteq 
\mathbb{Q} \subseteq \mathbb{R}$.
\end{lemma}
\end{forthel}
%
In particular we obtain the following theorem which
in other set theoretic approaches is equivalent to 
the Axiom of Infinity.
%
\begin{forthel}
\begin{theorem}[Axiom of Infinity]
$\mathbb{N}$ is a set.
\end{theorem}
\end{forthel}
%
The numbersystems $\mathbb{N}$, $\mathbb{Q}$ and $\mathbb{R}$
are strictly ascending with respect to $\subseteq$.
%
\begin{forthel}
Let $x \subsetneq y$ stand for $x \subseteq y$ and $x \neq y$.

\begin{theorem}
$\mathbb{N} \subsetneq \mathbb{Z} \subsetneq 
\mathbb{Q}$.
\end{theorem}
\begin{proof}
$-1 \notin \mathbb{N}$. $-1 \in \mathbb{Z}$.
$\frac{1}{2} \notin \mathbb{Z}$. 
$\frac{1}{2} \in \mathbb{Q}$.
\end{proof}

\begin{lemma}
$\mathbb{Z} = \mathbb{N}^- \cup \mathbb{N}$.
\end{lemma}

\begin{lemma}
$\mathbb{N}^- \cap \mathbb{N} = \{0\}$.
\end{lemma}
\end{forthel}
We shall later prove that $\mathbb{Q} \subsetneq \mathbb{R}$ 
using the irrationality of $\sqrt{2}$. 
The following closure
properties show that $\mathbb{N}$ is something like
a half-ring.
\begin{forthel}

Let $l,m,n$ stand for natural numbers.

\begin{lemma}
$0$ is a natural number.
\end{lemma}

\begin{lemma}
$1$ is a natural number.
\end{lemma}

\begin{lemma}
$l + m$ is a natural number.
\end{lemma}

\begin{lemma}
$l \cdot m$ is a natural number.
\end{lemma}
\end{forthel}
Although we do not have additive inverses available in 
$\mathbb{N}$, we still have some cancellation properties
known from rings.
\begin{forthel}
\begin{lemma}
If $l + m = l + n$ or $m + l = n + l$ then $m = n$.
\end{lemma}

\begin{lemma}
Assume that $l$ is nonzero.
If $l \cdot m = l \cdot n$ or $m \cdot l = n \cdot l$ then $m = n$.
\end{lemma}
\end{forthel}
%
Together with the principle of mathematical induction the next
lemma expresses that $\mathbb{N}$ is an inductive type that
is generated by $0$ and the successor operation $+1$. 
%
\begin{forthel}
\begin{lemma} Let $n$ be a natural number. Then
$n = 0$ or $n = m + 1$ for some natural number $m$.
\end{lemma}
\begin{proof}
Case $n = 0$. Trivial.

Case $n \neq 0$. Let $m = n - 1$. $m$ is a natural number and
$n = m + 1$. End.
\end{proof}

\begin{lemma}
For every natural number $n$ $n = 0$ or $1 \leq n$.
\end{lemma}

\begin{lemma}
If $m + n = 0$ then $m = 0$ and $n = 0$.
\end{lemma}
\end{forthel}
%
On $\mathbb{N}$, $\leq$ is definable using addition.
%
\begin{forthel}
\begin{lemma}
If $m \geq n$ then $m-n$ is a natural number.
\end{lemma}

\begin{lemma}
Assume $m \leq n$. Then
there exists a natural number $l$ such that $m + l = n$.
\end{lemma}
\begin{proof}
$n - m$ is a natural number. $m + (n-m) = (n - m) + m = n$.
\end{proof}

\begin{lemma}
Assume there exists a natural number $l$ such 
that $m + l = n$. Then $m \leq n$.
\end{lemma}

\begin{lemma}
Let $m \neq 0$. Then $n \leq n \cdot m$.
\end{lemma}
\begin{proof}
We have $1 \leq m$. $n = n \cdot 1 \leq n \cdot m$.
\end{proof}

\begin{lemma}
Let $a,\alpha,b,\beta$ be real numbers such that $a \leq \alpha$ and $b \leq \beta$.
Then $a + b \leq \alpha + \beta$.
\end{lemma}
\begin{proof}
$a \leq \alpha$ and $a + b \leq \alpha + b$ and $\alpha + b \leq \alpha + \beta$.
\end{proof}

\begin{lemma}
Let $a,b$ be integers such that $a < b$.
Then $a + 1 \leq b$.
\end{lemma}
\begin{proof}
Assume contrary. Let $c = a+1$. $c>b$.
Then $a < b < a + 1$. Thus $a - a = 0 < b - a < (a + 1) - a = 1$. Then $b - a$ is an integer
and $0 < b - a < 1$. Contradiction.
\end{proof}

\begin{lemma}
Let $a,b$ be integers such that $a > b$.
Then $a - 1 \geq b$.
\end{lemma}
\begin{proof}
$a > b$. Then $-a < -b$. $-a + 1 \leq -b$. $-(-a + 1) \geq -(-b)$. $a - 1 \geq b$.
\end{proof}
\end{forthel}

\section{The Principle of Mathematical Induction (\#74)}

We prove the second-order Peano axiom for all subsets of $\mathbb{N}$.
This implies the principle of {\em complete induction}: to prove a 
property $P(n)$ for all natural numbers $n$, prove $P(0)$ and
the implication $P(n) \rightarrow P(n+1)$. 
%
\begin{forthel}

\begin{theorem}[Induction Theorem]
Assume $A \subseteq \mathbb{N}$
and $0 \in A$ and for all $n \in A$ $n + 1 \in A$.
Then $A = \mathbb{N}$.
\end{theorem}

\begin{proof}
Let us show that every element of $\mathbb{N}$ is an element of $A$.
	Let $n \in \mathbb{N}$.
	Assume the contrary.
	Define $F = \{  j \in \mathbb{N} \mid j \notin A\}$.
	$F$ is nonempty. $F$ is bounded below.
  Take an infimum $a$ of $F$.
	Let us show that $a+1$ is a lower bound of $F$.
		Let $x \in F$. $x - 1 \in \mathbb{Z}$.

		Case $x - 1 < 0$. Then $0 < x < 1$. Contradiction. End.

		Case $x - 1 = 0$. Then $x = 1$ and $1 \notin A$. Contradiction. End.

		Case $x - 1 > 0$. Then $x - 1 \in \mathbb{N}$.
      $x - 1 \notin A$. Indeed $(x - 1) + 1 = x \notin A$. $x - 1 \in F$.
			$a \leq x - 1$.
			$a + 1 \leq (x - 1) + 1 = x$.
		End.
	End.

	Then $a+1 > a$.
	Contradiction.
End.
\end{proof}
\end{forthel}
%
\Naproche provides a general mechanism for the organisation of
inductive proofs. There is a reserved binary relation
symbol $\prec$ which can be viewed as a universal inductive relation.
The keyphrase {\em proof by induction} turns a universal
claim $\forall x \ P(x)$ into the thesis
$$\forall x (\forall y (y \prec x \rightarrow \ P(y)) \rightarrow P(x))$$
expressing that $P$ is inherited from $\prec$-predecessors.  
Therefore we can describe $\prec$ by:
%
\begin{forthel}
Let $m$ is inductively smaller than $n$ stand for $m \prec n$.
\end{forthel}
%
The Induction Theorem justifies to embed the ordering of the natural numbers
into $\prec$.
%
\begin{forthel}
\begin{axiom}
If $n < m$ then $n$ is inductively smaller than $m$.
\end{axiom}
\end{forthel}
We can now give a generic proof of mathematical induction which
is typical of \Naproche's approach.
\begin{forthel}
\begin{signature}
$P(n)$ is an atom.
\end{signature}

\begin{theorem}
Assume that $P(0)$ and for all natural numbers
$n$ if $P(n)$ then  $P(n+1)$.
Then $P(n)$ for all natural numbers $n$.
\end{theorem}
\begin{proof}[by induction]
Let $n$ be a natural number.

Case $n = 0$. Trivial.

Case $n \neq 0$. Then take a natural number $m$ such that
$n = m + 1$. $m$ is inductively smaller than $n$ and $P(m)$. 
Hence $P(n)$.
Qed.
\end{proof}
\end{forthel}

Induction also implies that the relation $<$ is 
well-founded on $\mathbb{N}$: every nonempty subset
of $\mathbb{N}$ has a minimal element:

\begin{forthel}
\begin{theorem}
Let $X$ be a nonempty subset of $\mathbb{N}$.
Then there is an element $n$ of $X$ such that
$n$ is the infimum of $X$.
\end{theorem}
\begin{proof}
Assume the contrary. Then
for all elements $n$ of $X$ there
is $x \in X$ such that not $n \leq x$.

(1) For all natural numbers $n$ $n \notin X$.

Proof by induction.
Let $n$ be a natural number.
Assume that $n \in X$.
Take $x \in X$ such that not $n \leq x$.
Then $x < n$. $x$ is inductively smaller than $n$.
Hence $x \notin X$. Contradiction.
Qed.

Hence $X = \emptyset$. Contradiction.

\end{proof}
\end{forthel}


\section{Sum of an Arithmetic Series (\#68)}

\newcommand{\sumarith}[3]{\sum_{i = 1}^{#3}(#1 + #2 \cdot i)}

\begin{forthel}
Let $a,d$ denote real numbers.
Let $n$ denote a natural number.

\begin{signature}
$\sumarith{a}{d}{n}$ is a real number.
\end{signature}

\begin{axiom}
$\sumarith{a}{d}{1} = a + d$.
\end{axiom}

\begin{axiom}[1]
$\sumarith{a}{d}{n+1} = \sumarith{a}{d}{n} + (a + (d \cdot (n + 1)))$.
\end{axiom}

\begin{lemma}
Let $b$ be a nonzero real number.
$\frac{a}{b} \cdot d = a \cdot \frac{d}{b}$.
\end{lemma}

\begin{theorem} For all nonzero natural numbers $n$
$$\sumarith{a}{d}{n} = n \cdot ( a + \frac{(n + 1) \cdot d}{2}).$$
\end{theorem}
\begin{proof}[by induction on $n$]
Let $n$ be a nonzero natural number.

Case $n = 1$.
Trivial.

Take a natural number $m$ such that $m + 1 = n$. $m$ is inductively smaller than $n$.

$$\sumarith{a}{d}{m} = m \cdot ( a + \frac{(m + 1) \cdot d}{2}).$$

Then
$$\sumarith{a}{d}{n} = 
(m \cdot ( a + \frac{(m + 1) \cdot d}{2})) + (a + (d \cdot (m + 1)))$$
(by 1).


[timelimit 10]
Hence

$\sumarith{a}{d}{n} =$

$((m \cdot a) + (m \cdot \frac{n \cdot d}{2})) + (a + (d \cdot n)) =$

$(((m \cdot a) + (m \cdot \frac{n \cdot d}{2})) + a) + (d \cdot n) =$

$(((m \cdot a) + a) +  (m \cdot \frac{n \cdot d}{2})) + (d \cdot n) =$

$(((m \cdot a) + (1 \cdot a)) +  (m \cdot \frac{n \cdot d}{2})) + (d \cdot n) =$

$((n \cdot a) +  (m \cdot \frac{n \cdot d}{2})) + (d \cdot n)$.

$((n \cdot a) +  (m \cdot \frac{n \cdot d}{2})) + (d \cdot n) =$

$(n \cdot a) +  ((m \cdot \frac{n \cdot d}{2}) + (d \cdot n))=$

$(n \cdot a) +  ((m \cdot \frac{n \cdot d}{2}) + (1 \cdot (d \cdot n)))=$

$(n \cdot a) +  ((m \cdot \frac{n \cdot d}{2}) + (\frac{2}{2} \cdot (d \cdot n)))$.

Then $(n \cdot a) +  ((m \cdot \frac{n \cdot d}{2}) + (\frac{2}{2} \cdot (d \cdot n))) =$

$(n \cdot a) +  ((m \cdot \frac{n \cdot d}{2}) + (2 \cdot \frac{n \cdot d}{2})) =$

$(n \cdot a) +  ((m +2) \cdot \frac{n \cdot d}{2})$.

Then $(n \cdot a) + ((m +2) \cdot \frac{n \cdot d}{2}) =$
$(n \cdot a) +  ((n+1) \cdot \frac{n \cdot d}{2}) =$

$(n \cdot a) +  \frac{(n+1) \cdot (n \cdot d)}{2} =$
$(n \cdot a) +  \frac{((n+1) \cdot n) \cdot d}{2} =$

$(n \cdot a) +  \frac{(n \cdot (n+1)) \cdot d}{2} =$
$(n \cdot a) +  \frac{n \cdot ((n+1) \cdot d)}{2} =$

$(n \cdot a) +  (n \cdot \frac{((n+1) \cdot d)}{2}) =$
$n \cdot ( a + \frac{(n + 1) \cdot d}{2})$.
[timelimit 3]
\end{proof}
\end{forthel}


\section{Exponentiation}

\begin{forthel}
Let $x,y$ denote real numbers.
Let $i$ denote natural numbers.

\begin{signature} $x^{i}$ is a real number.
\end{signature}

\begin{axiom} $x^{0} = 1$. \end{axiom}

\begin{axiom} $x^{i+1} = x^{i} \cdot x$.
\end{axiom}

\begin{lemma}
$x^{1} = x$.
\end{lemma}

\begin{lemma}
$x^{2} = x \cdot x$.
\end{lemma}

\begin{lemma}
$x \cdot x^{i} = x^{i+1}$.
\end{lemma}

\begin{lemma}
Let $m$ be a natural number.
For all natural numbers $n$ $m^{n}$ is a natural number.
\end{lemma}
\begin{proof}[by induction on $n$]
Let $n$ be a natural number.

Case $n = 0$. $m^{0} = 1 \in \mathbb{N}$. End.

Case $n \neq 0$. Take a natural number $k$ such that $k = n - 1$. $k$ is inductively smaller than $n$.
$m^{k}$ is a natural number. $m \cdot m^{k} = m^{k + 1} = m^{n}$. Thus $m^{n}$ is a natural number. End.
\end{proof}

\begin{lemma}
Let $m$ be a nonzero natural number.
For all natural numbers $n$ $1 \leq m^{n}$.
\end{lemma}
\begin{proof}[by induction on $n$]
Let $n$ be a natural number.

Case $n = 0$. $m^{0} = 1$. $1 \leq 1$. End.

Case $n \neq 0$. Take a natural number $k$ such that $k = n - 1$. $k$ is inductively smaller than $n$.
$1 \leq m^{k}$ and $1 \leq m$. Thus $1 \leq m \cdot m^{k} = m^{k + 1} = m^{n}$. End.
\end{proof}

\end{forthel}
%
We prove two standard binomial formulas. The formulation is
somewhat clumsy, since we are missing proper arithmetic
parsing and rewriting.
%
\begin{forthel}
[timelimit 10]
\begin{lemma}
$(x + y)^{2} = (x^{2} + (2 \cdot (x \cdot y))) + y^{2}$.
\end{lemma}
\begin{proof}
$(x + y) \cdot (x + y) =
(x^{2} + (x \cdot y)) + ((y \cdot x) + y^{2}) = 
(x^{2} + ((x \cdot y) + (y \cdot x))) + y^{2}$.
\end{proof}

\begin{lemma}
$(x - y)^{2} = (x^{2} - (2 \cdot (x \cdot y))) + y^{2}$.
\end{lemma}
\begin{proof}
$(x - y)^{2} = (x^{2} + (2 \cdot (x \cdot (-y)))) + (-y)^{2}$.
\end{proof}
[timelimit 3]
\end{forthel}


\section{Sum of a Geometric Series (\#66)}

\newcommand{\sumgeom}[2]{\sum_{0 \leq i < #2} {#1}^i}


We treat the partial sums $\sumgeom{x}{n}$ of a geometric
series as a function in $x$ and $n$ which satisfies some
recursive axioms:

\begin{forthel}

Let $x$ denote a real number.
Let $n$ denote a natural number.

\begin{signature}
$\sumgeom{x}{n}$ is a real number.
\end{signature}

\begin{axiom}
$\sumgeom{x}{0} = 0$.
\end{axiom}

\begin{axiom} Let $x$ be a real number and $n$ be
a natural number. Then 
$\sumgeom{x}{n+1} = (\sumgeom{x}{n}) + x^{n}$.
\end{axiom}


\begin{theorem} Let $x \neq 1$. Then
$$\sumgeom{x}{n} = \frac{1 - x^{n}}{1 - x}$$
for all natural numbers $n$.
\end{theorem}
\begin{proof}[by induction on $n$]

$1 - x \neq 0$.

Let $n$ be a natural number.

Case $n = 0$. Trivial.

Case $n \neq 0$.
Take a natural number $m$ such that $m + 1 = n$. 
$m$ is inductively smaller than $m+1$ and
$\sumgeom{x}{m} = \frac{1 - x^{m}}{1 - x}$.

Let $a = x^{m}$ and $b = x^{n}$ and $c=1-x$.
Then $a,b,c$ are real numbers and
$\sumgeom{x}{n} =
\frac{1 - x^{m}}{1 - x} + x^{m} = 
\frac{1 - x^{m}}{1 - x} + \frac{x^{m} \cdot (1-x)}{1 - x} =
\frac{1 - x^{m}}{1 - x} + \frac{(x^{m} \cdot 1) + (x^{m} \cdot (-x))}{1 - x} = 
\frac{1 - x^{m}}{1 - x} + \frac{x^{m} + ((-x) \cdot x^{m})}{1 - x} =
\frac{1 - x^{m}}{1 - x} + \frac{x^{m} + (-(x \cdot x^{m}))}{1 - x} =
\frac{1 - x^{m}}{1 - x} + \frac{x^{m} - x^{n}}{1 - x} = 
\frac{1 - a}{c} + \frac{a - b}{c} =
\frac{(1 - a) + (a - b)}{c} = 
\frac{((1 - a) + a) - b}{c} = 
\frac{(1 + (-a + a)) - b}{c} =
\frac{1 - b}{c} = 
\frac{1 - x^{n}}{1 - x}$. End.

\end{proof}
\end{forthel}


\section{Divisibility and Prime Numbers}


We prove some divisibility properties that will be useful
further on.

\begin{forthel}

Let $m,n$ denote integers.

\begin{definition}
$n$ divides $m$ iff for some integer $l$ $m = n \cdot l$.
\end{definition}

Let $x | y$ denote $x$ divides $y$.
Let a divisor of $x$ denote an integer that divides $x$.

\begin{lemma}
Assume $l | m | n$.
Then $l | n$.
\end{lemma}
\begin{proof}
Take integers $u,v$ such that 
$m = l \cdot u$ and $n = m \cdot v$.
Then $n = l \cdot (u \cdot v)$.
\end{proof}

\begin{lemma}
Let $l | m$ and $l | m + n$.
Then $l | n$.
\end{lemma}
\begin{proof}
Assume that $l$ is nonzero.
Take an integers $p,q$ such that $m = l \cdot p$ and $m + n = l \cdot q$.
Take $r = q - p$.
We have 
$(l \cdot p) + (l \cdot r) = l \cdot q = m + n = (l \cdot p) + n$.
Hence $n = l \cdot r$.
\end{proof}

\begin{lemma}
Let $n,m$ be natural numbers such that $n$ is nonzero and $n$ divides $m$.
Then $\frac{m}{n}$ is a natural number.
\end{lemma}

\begin{lemma}
Let $m,n$ be natural numbers such that $n | m$.
Then there exists a natural number $l$ such that $n \cdot l = m$.
\end{lemma}
\begin{proof}
Case $n = 0$. Then $m = 0$. $0$ is a natural number and $n \cdot 0 = m$. End.

Case $n \neq 0$.
Take an integer $l$ such that $n \cdot l = m$.
Assume $l$ is not a natural number.
$n > 0$ and $l < 0$. Thus $n \cdot l < 0$. End.
\end{proof}

\begin{lemma}
Let $m,n$ be natural numbers.
If $n | m | n$ then $m=n$.
\end{lemma}
\begin{proof}
Assume $n | m | n$.
If $n = 0$ then $m = 0$. Assume $n \neq 0$.
Take natural numbers $p,q$ such that $n \cdot p = m$ and $m \cdot q = n$.
Then $n = m \cdot q = (n \cdot p) \cdot q = n \cdot (p \cdot q) = (p \cdot q) \cdot n$. $1 = p \cdot q$. Therefore $p=q=1$.
\end{proof}

\begin{lemma}
Let $m$ be a natural number such that $m \neq 0$.
Let $k$ be a divisor of $m$.
Then $k \leq m$.
\end{lemma}
\begin{proof}
Assume contrary.
Then there is a natural number $l$ such that
$l > 0$ and $m = l \cdot k$.
\end{proof}

\begin{proposition}
Let $k,l$ be natural number such that $k < l$ and $k > 0$.
Then $l$ is not a divisor of $k$.
\end{proposition}

\end{forthel}
%
Prime numbers are the mathematically most interesting
class of natural numbers.
%
\begin{forthel}
Let $x$ is nontrivial stand for $x \neq 0$ and $x \neq 1$.

\begin{definition}
$n$ is prime iff $n$ is a nontrivial natural number and
for every natural number $m$ that divides $n$ $m = 1$ or $m = n$.
\end{definition}
\end{forthel}
%
Remarkably, the following theorem is proved automatically by
just calling the method of induction, without further details.  
%
\begin{forthel}
[timelimit 10]
\begin{theorem}
Every nontrivial natural number $m$ has a prime divisor.
\end{theorem}
\begin{proof}[by induction on $m$]
\end{proof}
[timelimit 3]
\end{forthel}

\section{The Greatest Common Divisor}

\begin{forthel}

Let $m,n$ denote integers.


\begin{signature}
The greatest common divisor of $m$ and $n$ is a natural number.
\end{signature}

\begin{axiom}
The greatest common divisor of $m$ and $n$ is a divisor of $m$ and a divisor of $n$.
\end{axiom}

\begin{axiom}
Let $d$ be a divisor of $m$ and a divisor of $n$.
Then $d$ is a divisor of the greatest common divisor of $m$ and $n$.
\end{axiom}


\begin{lemma}
Let $z$ be an integer.
$z$ is the greatest common divisor of $z$ and $0$ or $-z$ is the greatest common divisor of $z$ and $0$.
\end{lemma}
\begin{proof}
Let $d$ be the greatest common divisor of $z$ and $0$.

Case $z$ is a natural number. $z$ is a common divisor of $z$ and $0$. 
  Then $d$ divides $z$. $z$ divides $d$. Thus $z = d$. End.
  
Case $z$ is not a natural number. Then $-z$ is a natural number and $-z$ is the greatest common divisor of $-z$ and $0$.
  $-z$ is a common divisor of $z$ and $0$. Then $-z$ divides $d$ and $d$ divides $-z$. $d = -z$.
End.
\end{proof}


\begin{lemma}
Let $n,m$ be integers. The greatest common divisor of $n$ and $m$ is equal to
the greatest common divisor of $m$ and $n$.
\end{lemma}
\begin{proof}
Let $d$ be the greatest common divisor of $n$ and $m$.
Let $\delta$ be the greatest common divisor of $m$ and $n$.
$d$ is a common divisor of $m$ and $n$. Thus $d$ divides $\delta$. 
$\delta$ is a common divisor of $n$ and $m$. Thus $\delta$ divides $d$. $\delta = d$.
\end{proof}

\begin{lemma}
Let $n$ be a natural number.
$n$ is the greatest common divisor of $n$ and $n$.
\end{lemma}
\begin{proof}
$n$ is a common divisor of $n$ and $n$. Let $d$ be the greatest common divisor of $n$ and $n$.
Then $d$ divides $n$. $n$ divides $d$. $d = n$.
\end{proof}

\end{forthel}



\section{Greatest Common Divisor Algorithm (\#69)}

\begin{forthel}

\begin{proposition}
Let $m,n$ be natural numbers such that $m > n$.
Let $d$ be a divisor of $m$ and a divisor of $n$ such that $d > 0$.
Then $d$ is a divisor of $m-n$.
\end{proposition}
\begin{proof}
Take natural numbers $u,v$ such that $m = d \cdot u$ and $n = d \cdot v$.
Then $u \cdot d > v \cdot d$. Therefore $(u \cdot d) \cdot 1/d > (v \cdot d) \cdot 1/d$ 
and $u \cdot (d \cdot 1/d) > v \cdot (d \cdot 1/d)$.
Thus $u > v$.
Then $m - n =
(d \cdot u) - (d \cdot v) =
d \cdot (u - v)$.
\end{proof}

\begin{proposition}
Let $m,n$ be natural numbers such that $m > n$.
Let $d$ be a divisor of $m-n$ and a divisor of $n$ such that $d > 0$.
Then $d$ is a divisor of $m$.
\end{proposition}
\begin{proof}
Let $k$ be $m-n$. $k$ is a natural number.
Take natural numbers $u,v$ such that $k = d \cdot u$ and $n = d \cdot v$.
Then $m = k + n =
(d \cdot u) + (d \cdot v) = 
d \cdot (u + v)$.
\end{proof}

\begin{lemma}
Let $m,n$ be natural numbers such that $m > n$. Then
the greatest common divisor of $m$ and $n$ 
is the greatest common divisor of $m-n$ and $n$.
\end{lemma}
\begin{proof}
Case n=0. Trivial.

Case n > 0.
Let $l$ be the greatest common divisor of $m$ and $n$ 
and $k$ be the greatest common divisor of $m-n$ and $n$.
$0$ not divides $n$. Then $l > 0$ and $k > 0$. 
$l$ is a divisor of $m-n$ and $k$ is a divisor of $m$.
Hence $l$ is a divisor of $k$ and $k$ is a divisor of $l$. Therefore $k=l$. End.
\end{proof}


\begin{proposition}
Let $m,n$ be natural numbers such that $m < n$. Then
the greatest common divisor of $m$ and $n$ 
is the greatest common divisor of $n-m$ and $m$.
\end{proposition}



\begin{signature}
$\gcd(m,n)$ is a natural number.
\end{signature}

\begin{axiom}
$\gcd(m,n) = \gcd(n,m)$.
\end{axiom}

\begin{axiom}
If $m=0$ and $n$ is a natural number then $\gcd(m,n)=n$.
\end{axiom}
\begin{axiom}
If $m > n$ then $\gcd(m,n) = \gcd(m-n,n)$.
\end{axiom}
\begin{axiom}
If $m < n$ then $\gcd(m,n) = \gcd(m,n-m)$.
\end{axiom}
\begin{axiom}
If $m = n$ then $\gcd(m,n) = \gcd(m-n,n)$.
\end{axiom}


\begin{proposition}
For all natural numbers $m,n$ the greatest common divisor of $m$ and $n$ is $\gcd(m,n)$.
\end{proposition}
\begin{proof}[by induction on $m+n$]
Let $m,n$ be natural numbers.
Then $m+n$ is a natural number.

Case $m + n =0$. Trivial.

Case $m + n > 0$.
If $m=0$ or $n=0$ then $\gcd(m,n)$ is 
the greatest common divisor of $m$ and $n$.
Assume $m>0$ and $n>0$.[timelimit 20]
If $m \leq n$ then $m + (n-m)$ is inductively smaller than $m + n$ and
$\gcd(m,n) = \gcd(m,n-m)$ and
the greatest common divisor of $m$ and $n$ is 
the greatest common divisor of $m$ and $n-m$
and the greatest common divisor of $m$ and $n$ is $\gcd(m,n)$. [timelimit 3]
If $m > n$ then $(m-n) + n$ is inductively smaller than $m + n$ and
$\gcd(m,n) = \gcd(m-n,n)$ and 
the greatest common divisor of $m$ and $n$ is 
the greatest common divisor of $m-n$ and $n$. End.
\end{proof}
\end{forthel}


\section{Bezout's Identity (\#60)}

\begin{forthel}

\begin{lemma}
Let $s,t$ be real numbers such that $s < t$.
Then there exists a real number $r$ such that $s < r < t$.
\end{lemma}
\begin{proof}
$\frac{s+t}{2}$ is a real number. $s + s < s + t$ and $\frac{s + s}{2} < \frac{s + t}{2}$.
$s = \frac{2}{2} \cdot s = \frac{2 \cdot s}{2} = \frac{s + s}{2} < \frac{s + t}{2}$.
$s + t < t + t$ and $\frac{s + t}{2} < \frac{t + t}{2}$.
[timelimit 10]
$\frac{s+t}{2} < \frac{t+t}{2} = \frac{2 \cdot t}{2} = \frac{2}{2} \cdot t = t$.
[timelimit 3]
$s < \frac{s+t}{2} < t$.
\end{proof}



Let $m,n$ denote integers.


\begin{proposition}
Let $a$ be nonzero natural number.
For every natural number $m$ there exist
a natural number $k$ such that $0 \leq m - (k \cdot a) < a$.
\end{proposition}
\begin{proof}[by induction on $m$]
Let $m$ be a natural number.

Case $m = 0$.
$0 \leq 0 - (0 \cdot a) < a$. End.

Case $m > 0$. Let $\mu = m-1$.
$\mu$ is a natural number and $\mu$ is inductively smaller than $m$.
Take a natural number $k$ such that $0 \leq \mu - (k \cdot a) < a$.
Then $\mu < m$ and $0 \leq \mu - (k \cdot a) <  a$.

Let us show that $m - (k \cdot a) = a$ or $m - (k \cdot a) < a$.
Assume contrary.
Let $b = m - (k \cdot a)$ and $c = (m-1) - (k \cdot a)$.
$(m-1) - (k \cdot a) < a$.
If not $b = a$ and not $b < a$ then $b > a$.
Then $m - (k \cdot a) > a$.
$(m - (k \cdot a)) - 1 > a - 1$.
$(-1) + (m - (k\cdot a)) > a - 1$.
$((-1) + m) - (k \cdot a) > a - 1$.
$(m-1) - (k \cdot a) > a - 1$.
$c > a-1$.
Then $c \geq a$.
Contradiction.
End.

Case $m - (k \cdot a) = a$. 
$k$ is a natural number.
$0 = 
a + (-a) = 
(m + (-(k \cdot a))) + (-a) =
m + (-(k \cdot a) + (-a)) = 
m + (-(k \cdot a) + ((-1) \cdot a)) = 
m + (((-k) \cdot a) + ((-1) \cdot a)) =
m + (((-k)+(-1)) \cdot a) = 
m + ((-k-1) \cdot a) =
m - (-(-k-1) \cdot a)$. 
$0 \leq m - (-(-k-1) \cdot a) < a$. 
$-(-k-1)$ is a natural number. 
Indeed $k$ is a natural number and $0 > ((-k) + (-1)) = (-k-1)$.
Then there exist a natural number $l$ such that
$0 \leq m - (-(-k-1) \cdot a) < a$.
End.

Case $m - (k \cdot a) < a$. Let $\nu = -(k \cdot a)$.
$0 \leq \mu + \nu < m + \nu$. 
$0 \leq m - (k \cdot a)$.
Then $k$ is a natural number such that
$0 \leq  m - (k \cdot a) < a$. End.
End. 
\end{proof}

\begin{lemma}
Let $a$ be nonzero natural number and $m$ be an integer.
Then there exists an integer $k$ such that $0 \leq m - (k \cdot a) < a$.
\end{lemma}
\begin{proof}
Case $m$ is a natural number. Then there exists a natural number $k$ such that $0 \leq m - (k \cdot a) < a$. End.

Case $m$ is not a natural number. Let $\mu = -m$. Then $\mu$ is a natural number.
Take a natural number $k$ such that $0 \leq \mu - (k \cdot a) < a$. Let $\kappa = -k$. 
$\kappa$ is an integer and $0 \leq m - (\kappa \cdot a) < a$. End.
\end{proof}



\begin{theorem}[Bezout]
Let $a,b$ be integers and $\delta$ be the greatest common divisor of $a$ and $b$.
Then there exist integer $x$ and integer $y$ such that 
$\delta = (a \cdot x) + (b \cdot y)$. 
\end{theorem}
\begin{proof}
Case $a = 0$. The greatest common divisor of $b$ and $a$ is equal to $\delta$.
  Then $\delta = b$ or $\delta = -b$. 1 and -1 are integers. 
  If $\delta = b$ then $\delta = (a \cdot 1) + (b \cdot 1)$. If $\delta = -b$ then $\delta = (a \cdot 1) + (b \cdot -1)$. End. 

Case $b = 0$. Then $\delta = a$ or $\delta = -a$. 1 and -1 are integers. 
  If $\delta = a$ then $\delta = (a \cdot 1) + (b \cdot 1)$. If $\delta = -a$ then $\delta = (a \cdot -1) + (b \cdot 1)$. End. 

Case $a \neq  0$ and $b \neq 0$.
  $0$ not divides $a$. Thus $\delta \neq 0$.
  Define $S = \{ (a \cdot e) + (b \cdot f) \mid e,f$ are integers and 
  $(a \cdot e) + (b \cdot f) > 0\}$.
  $a > 0$ or $-a > 0$.
  $((a \cdot 1) + (b \cdot 0)) > 0$ or $(a \cdot -1) + (b \cdot 0) > 0$. 
  [timelimit 10] $((a \cdot 1) + (b \cdot 0)) \in S$ or $(a \cdot -1) + (b \cdot 0) \in S$. [timelimit 3]
  $S$ is nonempty.

  Let us show that $S \subseteq \mathbb{N}$.
    Indeed we can show that for all $s \in S$ $s \in \mathbb{N}$.
    Let $s \in S$.
    Take integers $e,f$ such that $s = (a \cdot e) + (b \cdot f)$. 
    $a \cdot e \in \mathbb{Z}$ and $b \cdot f \in \mathbb{Z}$. Thus $s$ is an integer.
    $s > 0$. 
  End.
    

  $S$ has an infimum.
  Take $d \in S$ such that $d$ is the infimum of $S$.
  Take integers $e,f$ such that $d = (a \cdot e) + (b \cdot f)$.

  Let us show that $d$ divides $a$.
    $d$ is a nonzero natural number and $a$ is an integers.
    Take an integer $k$ such that $0 \leq a - (k \cdot d) < d$. Let $r = a - (k \cdot d)$.
    $r = a - (k \cdot d) = a - (k \cdot ((a \cdot e) + (b \cdot f))) 
    = a - ((k \cdot (a \cdot e)) + (k \cdot (b \cdot f)))
    = a + (-(k \cdot (a \cdot e)) - (k \cdot (b \cdot f)))$.
    Let $\phi = (-k \cdot e)$ and $\psi = (-k \cdot f)$.
    $-(k \cdot (a \cdot e)) = -(a \cdot (k \cdot e)) = a \cdot (-k \cdot e) = a \cdot \phi$.
    $- (k \cdot (b \cdot f)) = -(b \cdot (k \cdot f)) = b \cdot (-k \cdot f) = b \cdot \psi$.
    $r = (a + (a \cdot \phi)) + (b \cdot \psi)$. [timelimit 10]
    $(a + (a \cdot \phi)) + (b \cdot \psi)= (a \cdot (1 + \phi)) + (b \cdot \psi)$. [timelimit 3]
    $(1 + \phi)$ and $\psi$ are integers. Thus $r \in S$ or $r = 0$. $0 \leq r < d$ and $d$ is the infimum of $S$.
    Thus $r = 0$. $k \cdot d = a$. Therefore $d$ divides $a$.
  End.

  Let us show that $d$ divides $b$.
    $d$ is a nonzero natural number and $b$ is an integers.
    [timelimit 10] Take an integer $k$ such that $0 \leq b - (k \cdot d) < d$. [timelimit 3] Let $r = b - (k \cdot d)$.
    $r = b - (k \cdot d) = b - (k \cdot ((a \cdot e) + (b \cdot f))) 
    = b - ((k \cdot (a \cdot e)) + (k \cdot (b \cdot f)))
    = b + (-(k \cdot (a \cdot e)) - (k \cdot (b \cdot f)))$.
    Let $\phi = (-k \cdot e)$ and $\psi = (-k \cdot f)$.
    $-(k \cdot (a \cdot e)) = -(a \cdot (k \cdot e)) = a \cdot (-k \cdot e) = a \cdot \phi$.
    $- (k \cdot (b \cdot f)) = -(b \cdot (k \cdot f)) = b \cdot (-k \cdot f) = b \cdot \psi$.
    $r = (b + (a \cdot \phi)) + (b \cdot \psi)$. [timelimit 10]
    $(b + (a \cdot \phi)) + (b \cdot \psi) = (a \cdot \phi) + (b + (b \cdot \psi)) = (a \cdot \phi) + (b \cdot (1 + \psi))$. [timelimit 3]
    $\phi$ and $(1+\psi)$ are integers. Thus $r \in S$ or $r = 0$. $0 \leq r < d$ and $d$ is the infimum of $S$.
    Thus $r = 0$. $k \cdot d = b$. Therefore $d$ divides $b$.
  End.


  $d$ is a common divisor of $a$ and $b$ and a natural number.

  Let us show that $d$ is the greatest common divisor of $a$ and $b$.
    Let $c$ be the greatest common divisor of $a$ and $b$. Take integers $u,v$ such that $a = c \cdot u$ and $b = c \cdot v$.
    $d = (a \cdot e) + (b \cdot f)
    = ((c \cdot u) \cdot e) + ((c \cdot v) \cdot f)
    = (c \cdot (u \cdot e)) + (c \cdot (v \cdot f))
    = c \cdot ((u \cdot e) + (v \cdot f))$.
    $((u \cdot e) + (v \cdot f))$ is an integer. $c$ is a divisor of $d$ and $d$ is a divisor of $c$. Thus $d = c$.
  End.
  
  Therefore $d = \delta$ and
  there exist integers $i,j$ such that $\delta = (a \cdot i) + (b \cdot j)$.
End.
\end{proof}

\end{forthel}


\section{Irrationality of Roots of Prime Numbers (\#1)}

\begin{forthel}

\begin{lemma}
The greatest common divisor of $n$ and $m$ is 0 iff $n = 0$ and $m = 0$.
\end{lemma}
\begin{proof}
Let us show that the greatest common divisor of 0 and 0 is 0.
  Assume contrary. Let $d$ be the greatest common divisor of 0 and 0. 
  0 is a divisor of 0 and 0 is not a divisor of $d$. Contradiction. End.

Let us show that if the greatest common divisor of $n$ and $m$ is 0 then $n = 0$ and $m = 0$.
  If $n \neq 0$ then 0 is not a divisor of $n$.
  If $m \neq 0$ then 0 is not a divisor of $m$.
End.
\end{proof}

  Let a prime number stand for a prime natural number.

    Let $p$ denote a prime number.
    Let $n,m$ denote natural numbers.
    Let $q$ denote a rational number.

    \begin{definition}
      $n$ and $m$ are coprime iff $n$ and $m$ have no common prime divisor.
    \end{definition}

    \begin{lemma}
      If $q$ is positive then there exist coprime natural numbers $m,n$ such that $m \cdot q = n$.
    \end{lemma}
\begin{proof}
Let $q$ be positive. 

Let us show that there exists a natural number $a$ and nonzero natural number $b$ such that $q = \frac{a}{b}$.
  Take an integer $a$ and a nonzero integer $b$ such that $q = \frac{a}{b}$.
  
  Case $a = 0$ or $a,b$ are natural numbers. Trivial.
  
  Case ($a < 0$ and $b > 0$) or ($a > 0$ and $b < 0$). Then $\frac{a}{b} < 0$ and $q \geq 0$. Contradiction. End.
  
  Case $a < 0$ and $b < 0$. Then $-a,-b \in \mathbb{N}$ and $q = \frac{-a}{-b}$. End.
End.
Take a natural number $a$ and a nontrivial natural number $b$ such that $q = \frac{a}{b}$.\\

Take the greatest common divisor $d$ of $a$ and $b$. $b$ is nontrivial. Thus 0 not divides $b$ and $d$ is a nonzero natural number. 
Take $n = \frac{a}{d}$ and $m = \frac{b}{d}$. $n,m$ are natural numbers.\\

Let us show that $n,m$ are coprime. 

  Assume contrary. The greatest common divisor of $n$ and $m$ is not 1. Take the greatest common divisor $\delta$ of $n$ and $m$.
  Take $p = d \cdot \delta$, $\nu = \frac{n}{\delta}$ and $\mu = \frac{m}{\delta}$. $p,\nu,\mu$ are natural numbers.
  $\nu \cdot p = \frac{n}{\delta} \cdot (\delta \cdot d) = n \cdot d = \frac{a}{d} \cdot d = a$ and
  $\mu \cdot p = \frac{m}{\delta} \cdot (\delta \cdot d) = m \cdot d = \frac{b}{d} \cdot d = b$. 
  Thus $p$ divides $a$ and $p$ divides $b$. $\delta \neq 1$.
  Therefore$p$ not divides $d$ and $d$ is not the greatest common divisor of $a$ and $b$. Contradiction.
End.\\

$q = \frac{n}{m}$ and $m \cdot q = n$.
\end{proof}

    \begin{lemma}
      If $p$ divides $n^{2}$ then $p$ divides $n$. 
    \end{lemma}
    \begin{proof}
      Assume $p$ divides $n^{2}$ and $p$ not divides $n$. Thus the greatest common divisor of $p$ and $n$ is 1.
      Take integers $s,t$ such that $(p \cdot s) + (n \cdot t) = 1$.
      $n = n \cdot 1 = n \cdot ((p \cdot s) + (n \cdot t)) = (n \cdot (p \cdot s)) + (n \cdot (n \cdot t))$.
      $n \cdot (p \cdot s), n \cdot (n \cdot t)$ are integers.
      $p$ divides $n \cdot (p \cdot s)$. $p$ divides $n \cdot (n \cdot t)$.
      Thus $p$ divides $(n \cdot (p \cdot s)) + (n \cdot (n \cdot t))$ and $p$ divides $n$. Contradiction.
    \end{proof}


    \begin{theorem}[Pythagoras]
      $q^{2} = p$ for no positive rational number $q$.
    \end{theorem}
    \begin{proof}[by contradiction]
      Assume the contrary.
      Take a positive rational number $q$ such that $p = q^{2}$.
      Take coprime natural numbers $m,n$ such that $m \cdot q = n$.
      Then $p \cdot m^{2} = n^{2}$.
      Therefore $p$ divides $n$.
      Take a natural number $k$ such that $n = k \cdot p$.
      Then $p \cdot m^{2} = p \cdot (k \cdot n)$.
      Therefore $m^{2} = k \cdot n$.
      Therefore $m^{2}$ is equal to $p \cdot k^{2}$.
      Hence $p$ divides $m$.
      Contradiction.
    \end{proof}
  \end{forthel}

  \section{Finite and Infinite Sets}
  
  \begin{forthel}
  Let $m,n,k$ denote natural numbers.
  
  \begin{definition}
  $\Seq{m}{n}$ is the class of
  natural numbers $i$ such that $m \leq i \leq n$.
  \end{definition}
  
  \begin{lemma}
  $\Seq{m}{n}$ is a set.
  \end{lemma}
  
  \begin{lemma} 
  Assume that $m \leq n \leq k$.
  Then $\Seq{m}{n} \cup \Seq{n+1}{k} = \Seq{m}{k}$.
  \end{lemma}
  \begin{proof}
  $\Seq{m}{k} \subseteq \Seq{m}{n} \cup \Seq{n+1}{k}$.
  Proof.
  Let $x \in \Seq{m}{k}$. $x$ is an integer. 
  $x \leq n$ or $n+1 \leq x$. Proof. Assume the contrary. Then $n < x < n+1$. $0 < x - n < 1$. End.
  $x \in \Seq{m}{n}$ or $x \in \Seq{n+1}{k}$. End.
  \end{proof}
  
  
  \begin{lemma} Assume that $m \leq n \leq k$.
  Then $\Seq{m}{n}$ and $\Seq{n+1}{k}$ are disjoint.
  \end{lemma}
  
  \begin{lemma} Let $x \in \Seq{1}{n+1} \setminus \Seq{1}{n}$.
  Then $x = n+1$.
  \end{lemma}
  \begin{proof}
  $x$ is an integer.
  $x \leq n+1$. Not $x \leq n$.
  Assume that $x \neq n+1$.
  $n < x < n+1$.
  $0 < x - n < 1$.
  \end{proof}
  
  Let $S$ denote a class.
  
  \begin{definition}
  $S$ is finite iff $S$ and $\Seq{1}{n}$ are equinumerous for some 
  natural number $n$.
  \end{definition}
  
  \begin{lemma}
  Let $S$ be finite. Then $S$ is a set.
  \end{lemma}
  \begin{proof}
  Take a natural number $n$ such that $S$ and $\Seq{1}{n}$ are equinumerous.
  Take a bijection $f$ between $\Seq{1}{n}$ and $S$.
  Then $\Seq{1}{n}$ is a set and $S = f[\Seq{1}{n}]$.
  \end{proof}
  \end{forthel}
  %
  We show that the number $n$ in the definition is uniquely
  determined.
  %
  \begin{forthel}
  
  \begin{lemma}
  For all natural numbers $n$
  for all natural numbers $m$
  for all injective maps $f$ from 
  $\Seq{1}{m}$ to $\Seq{1}{n}$ we have $m \leq n$.
  \end{lemma}
  \begin{proof}[by induction on $n$]
  Let $n$ be a natural number.
  Let $m$ be a natural number.
  Let $f$ be an injective map from $\Seq{1}{m}$ to $\Seq{1}{n}$.
  
  Case $n=0$. $\Seq{1}{n} = \emptyset$. Then $\Seq{1}{m} = \emptyset$ and 
  $0 = m \leq n$. Qed.
  
  Case $n \neq 0$.
  Take a natural number $n1$ such that $n = n1 + 1$.
  
  Case $m = 0$. Then $m \leq n$. Trivial.
  
  Case $m \neq 0$.
  Take a natural number $m1$ such that $m = m1 + 1$.
  
  Case $f[\Seq{1}{m1}] \subseteq \Seq{1}{n1}$.

  Let 
$$g = f \upharpoonright \Seq{1}{m1}.$$
  Let $C = \Seq{1}{m1}$. Let $D = \Seq{1}{n1}$.
  $f \upharpoonright \Seq{1}{m1}$ is an injective map.
  $\dom(f \upharpoonright \Seq{1}{m1}) = \Seq{1}{m1}$.
  $f[\Seq{1}{m1}] \subseteq \Seq{1}{n1}$.
  $g$ is a map
  from $C$ to $D$.

  (1) $f \upharpoonright \Seq{1}{m1}$ is an injective map
  from $\Seq{1}{m1}$ to $\Seq{1}{n1}$.

  $n1$ is inductively smaller than $n$.
[timelimit 10] %%%
  $m1 \leq n1$ and $m \leq n$. Qed.
[timelimit 3] %%%

  Case not $f[\Seq{1}{m1}] \subseteq \Seq{1}{n1}$.

  Take $w \in f[\Seq{1}{m1}]$ such that $w \notin \Seq{1}{n1}$.
  $w \in f[\Seq{1}{m1}] \subseteq f[\Seq{1}{m}] \subseteq \Seq{1}{n}$.
  $w \in \Seq{1}{n1+1} \setminus \Seq{1}{n1}$.
  $w = n$.
  Take $i \in \Seq{1}{m1}$ such that $f(i) = w$.
  Define
  \[h(j) =
    \begin{cases}
    f(j)  & : j \neq i \\
    f(m) & : j = i
    \end{cases} \]
  for $j \in \Seq{1}{m1}$.
  $h$ is a map. $\dom(h) = \Seq{1}{m1}$. 
  
  (2) $h$ is injective.

  Proof.
  Let $j,k$ be distinct elements of $\Seq{1}{m1}$.
  Let us show that $h(j) \neq h(k)$.
  
  Case $j = i$.
  Then $k \neq i$. $k \neq m$. [timelimit 10]
  $h(j) = f(m) \neq f(k) = h(k)$. [timelimit 3]
  Qed.
  
  Case $k = i$.
  Then $j \neq i$. $j \neq m$. [timelimit 10]
  $h(j) = f(j) \neq f(m) = h(k)$. [timelimit 3]
  Qed.
  Then $j \neq i$ and $k \neq i$. [timelimit 10]
  $h(j) = f(j) \neq f(k) = h(k)$. [timelimit 3]
  Qed.
  Qed.
  
(3)  $h[\Seq{1}{m1}] \subseteq \Seq{1}{n1}$.
  
Proof.
  Let $j \in \Seq{1}{m1}$.
  $h(j) \in \Seq{1}{n}$.
  Proof.
  [timelimit 30]
  $h(j) = f(j) \in \Seq{1}{n}$ or $h(j) = f(m) \in \Seq{1}{n}$.
  [timelimit 3]
  Qed.
  
  Let us show that  $h(j) \in \Seq{1}{n1}$.

  Proof.
[timelimit 10]
    Case $j = i$.

    $h(j) = f(m) \neq f(i) = w = n$. Indeed $m \neq i$.

%    $h(j) = f(m)$. $f(m) \neq f(i)$. Indeed $m \neq i$. $f(i) = w$. $w  = n$.
End.
[timelimit 3]

    Then $j \neq i$.
    $h(j) = f(j) \neq f(i) = n$.
  Qed.
  Qed.
    
(4) $h$ is an injective map from $\Seq{1}{m1}$ to $\Seq{1}{n1}$. 
  
  $n1$ is inductively smaller than $n$.
Then $m1 \leq n1$ and $m \leq n$.
  Qed.
  Qed.
  Qed.
  \end{proof}
  
  
  \begin{lemma}
  Let $n,m$ be natural numbers and
  $\Seq{1}{m} \sim \Seq{1}{n}$. Then $m = n$.
  \end{lemma}
  \begin{proof}
  There is an injective map from 
  $\Seq{1}{m}$ to $\Seq{1}{n}$ and
  there is an injective map from 
  $\Seq{1}{n}$ to $\Seq{1}{m}$. Then $m \leq n \leq m$.
  \end{proof}
  
  \begin{signature}
  Let $x$ be a finite set. $|x|$ is the natural number $n$
  such that $x$ and $\Seq{1}{n}$ are equinumerous.
  \end{signature}
  
  \begin{lemma} Let $x$ be a finite set.
  Let $x$ and $\Seq{1}{n}$ be equinumerous. Then
  $|x| = n$.
  \end{lemma}
  \begin{proof}
  $x \sim \Seq{1}{|x|}$ and $x \sim \Seq{1}{n}$. Thus $\Seq{1}{|x|} \sim \Seq{1}{n}$.
  \end{proof}
  
  \begin{lemma}
  $|\Seq{1}{n}| = n$.
  \end{lemma}
  
  \begin{lemma}
  Let $n,m,i$ be natural numbers.
  Then $\Seq{m}{n} \sim \Seq{m+i}{n+i}$.
  \end{lemma}
  \begin{proof}
  Define \[ H(k) = k + i \]
          for $k \in \Seq{m}{n}$.
  $H$ is a map from $\Seq{m}{n}$ to $\Seq{m+i}{n+i}$.
  $H$ is injective.
  $H$ is a surjection from $\Seq{m}{n}$ onto $\Seq{m+i}{n+i}$.
  Proof.
  Let $u \in \Seq{m+i}{n+i}$. $m + i \leq u \leq n + i$.
  $m  = (m + i) - i \leq u - i \leq (n + i) - i = n$.
[timelimit 10]
  Hence $u - i \in \Seq{m}{n}$.
[timelimit 3] $H(u-i) = u$ and 
  $u \in H[\Seq{m}{n}]$.
  Qed.
  \end{proof}
  
  \begin{lemma}
  Let $x,y$ be disjoint finite sets.
  Then $x \cup y$ is a finite set and $|x \cup y| = |x| + |y|$.
  \end{lemma}
  \begin{proof}
  Let $m = |x|$ and $n = |y|$.
  $x \sim \Seq{1}{m}$.
  Consider $u = \Seq{1}{n}$ and $v = \Seq{m}{m+n}$. 
  $y \sim \Seq{1}{n} \sim \Seq{1+m}{n+m}$.
  $y \sim \Seq{m+1}{m+n}$.[timelimit 30]
  $x \cup y \sim \Seq{1}{m} \cup \Seq{m+1}{m+n} = \Seq{1}{|x|+|y|}$. [timelimit 3]
  $x \cup y \sim \Seq{1}{|x|+|y|}$.
  \end{proof}
  
  
  \begin{definition}
  $S$ is infinite iff $S$ is not finite.
  \end{definition}
  
  \begin{definition}
  $S$ is denumerable iff $S$ and $\mathbb{N}$ are equinumerous.
  \end{definition}
  \end{forthel}


  \section{Number of Subsets of a Set (\#52)}
  
  \begin{forthel}
  
  \begin{lemma}
  Let $X$ be a finite set.
  $|X| = 0$ iff $X = \emptyset$.
  \end{lemma}
  \begin{proof}
  Let us show that if $|X| = 0$ then $X = \emptyset$.
    Assume $|X| = 0$ and there exists an $x \in X$.
    Take $x \in X$ and bijection $g$ between $X$ and $\Seq{1}{0}$. Then $g(x) \in \Seq{1}{0} = \emptyset$. Contradiction. End.
  
  If $X = \emptyset$ then $|X| = 0$. 
  \end{proof}
  
  
  \begin{definition}
  Let $Y$ be a nonempty set and $y \in Y$. 
  $\sset{y}{Y}$ is $\{\nu \in Y \mid \nu=y \}$.
  \end{definition}
  
  \begin{theorem}
  For all finite sets $X$ and all natural numbers $n$ if $|X| = n$ then
  $\pow(X)$ is finite and $|\pow(X)| = 2^{n}$.
  \end{theorem}
  \begin{proof}[by induction on $n$]
  Let $X$ be a finite set and $n$ be a natural number. Assume $|X| = n$.
  
  Case $n = 0$. $\Seq{1}{0} = \emptyset$. Thus $X = \emptyset$. 
    For all $x \in \pow(\emptyset)$ $x = \emptyset$. 
    Define $h(x) = 1$ for $x \in \pow(\emptyset)$. 
    $h$ is a bijection between $\pow(\emptyset)$ and $\Seq{1}{1}$.
    Hence $|\pow(X)| = 1$ and $2^{0} = 1$. End.\\
  
  Case $n \neq 0$. Take a natural number $m$ such that $m = n - 1$. $m$ is inductively smaller than $n$.
    There exists a bijection between $X$ and $\Seq{1}{n}$ and $1 \in \Seq{1}{n}$. Thus $X$ is nonempty.
    Take a bijection $g$ between $X$ and $\Seq{1}{n}$. Take $\xi \in X$ such that $g(\xi) = n$.
  
    Define $M = \{x \mid x \in \pow(X)$ and $\xi \in x\}$. Define $N = \{x \mid x \in \pow(X)$ and $\xi \notin x\}$.
    $M \cup N = \pow(X)$. $M,N$ are disjoint.
  
    Take $Y = X \setminus \sset{\xi}{X}$. $Y \subseteq X$.
    Let us show that $Y$ is finite and $|Y| = m$.
      Take $f = g \upharpoonright Y$.
      $g$ is injective. Thus $f$ is injective.
  
      Let us show that $f[Y] \subseteq \Seq{1}{m}$.
        $f[Y] \subseteq \Seq{1}{n}$ and $f(\gamma) = n$ for no $\gamma \in Y$.
        Thus $f[Y] \subseteq \Seq{1}{m}$. End.
  
      (2) $f$ is a surjection from $Y$ onto $\Seq{1}{m}$.
      Indeed we can show that every element of $\Seq{1}{m}$ is a value of $f$.
        Let $y \in \Seq{1}{m}$. $\Seq{1}{m} \subseteq \Seq{1}{n}$. $g$ is a surjection from $X$ onto $\Seq{1}{n}$.
        Take $x \in X$ such that $g(x) = y$. $y \neq n$ and $x \neq \xi$. $x \in Y$ and $f(x) = g(x) = y$. End.
    QED.
  
  
    Let us show that $M$ and $N$ are finite and $|\pow(Y)| = |M| = |N|$.
      We can show that there exists a bijection between $M$ and $N$.
        Define $f(x) = x \setminus \sset{\xi}{X}$ for $x \in M$.
    
        We can show that $f$ is injective.
          Let $x,y \in M$. Assume $f(x) = f(y)$. $\sset{\xi}{X} \subseteq x$ and $\sset{\xi}{X} \subseteq y$.
          $x \setminus \sset{\xi}{X} = y \setminus \sset{\xi}{X}$. Thus $x = y$. End.
    
        We can show that $f[M] \subseteq N$.
          Let $x \in M$ and $y = f(x)$. $y = x \setminus \sset{\xi}{X}$. $y \subseteq X$ and $\xi \notin y$. Thus $y \in N$. End.
  
        (2) $f$ is a surjection from $M$ onto $N$.
        Indeed we can show that every element of $N$ is a value of $f$.
          Let $y \in N$ and $x = y \cup \sset{\xi}{X}$. $x \subseteq X$ and $\xi \in x$. $x \in M$. 
          $f(x) = (y \cup \sset{\xi}{X}) \setminus \sset{\xi}{X} = y \setminus \sset{\xi}{X} = y$. End.
      End. 
  
      We can show that $\pow(Y) \subseteq N$.
        Let $y \in \pow(Y)$. $y \subseteq X$ and $\xi \notin y$. $y \in N$. End.
        
      We can show that $N \subseteq \pow(Y)$.
        Let $y \in N$. $\xi \notin y$. $y \subseteq Y$. $y \in \pow(Y)$. End.
        
  
      $\pow(Y) = N$. $\pow(Y)$ is finite. $N$ is finite and $M$ is finite.
      Thus $|\pow(Y)| = |N| = |M|$.
    QED.
  
    $|\pow(Y)| = 2^{m}$. Hence $|M| = |N| = 2^{m}$. $|M| + |N| = |M \cup N| = |\pow(X)|$. Let $w = 2^{m}$.
    $|M| + |N| = 2^{m} + 2^{m} = (1 \cdot 2^{m}) + (1 \cdot 2^{m}) = (1 + 1) \cdot 2^{m} =  2 \cdot 2^{m} = 2^{m+1} = 2^{n}$.
    Therefore $\pow(X)$ is finite and $|\pow(X)| = 2^{n}$.
  End.
  \end{proof}
  
  \end{forthel}
  
  

\section{Finite Products}

\begin{forthel}

\begin{definition}
A sequence of length $n$ is a
function $F$ such that $\dom(F) = \Seq{1}{n}$.
\end{definition}

Let $F_{i}$ stand for $F(i)$.

\begin{definition}
Let $F$ be a sequence of length $n$.
$\FinSet{F}{1}{n} = \{ F_{i} | i \in \dom(F)\}$.
\end{definition}





\begin{signature}
Let $F$ be a sequence of length $n$
such that $\FinSet{F}{1}{n} \subseteq \mathbb{N}$.
$\Prod{F}{1}{n}$ is a natural number.
\end{signature}

\begin{axiom}[Factorproperty]
Let $F$ be a sequence of length $n$
such that $F(i)$ is a nonzero natural number for every $i \in \dom(F)$.
Then $\Prod{F}{1}{n}$ is nonzero and
$F(i)$ divides $\Prod{F}{1}{n}$ for every $i \in \dom(F)$.
\end{axiom}

\end{forthel}

\section{The Infinitude of Primes (\#11)}

\begin{forthel}

\begin{signature}
$\Primes$ is the collection of prime natural numbers.
\end{signature}

\begin{theorem}[Euclid]
$\Primes$ is infinite.
\end{theorem}
\begin{proof}[by contradiction]
Assume that $\Primes$ is finite.
Take a natural number $r$ such that $\Seq{1}{r}$ and $\Primes$ are equinumerous.
Take a bijection $p$ between $\Seq{1}{r}$ and $\Primes$.
$p$ is a sequence of length $r$ and 
$\Primes = \FinSet{p}{1}{r}$.

(1) $p_{i}$ is a nonzero natural number for every
$i \in  \dom(p)$.

Consider $n = \Prod{p}{1}{r}+1$. [timelimit 10]
$\Prod{p}{1}{r}$ is nonzero and $n$ is nontrivial. [timelimit 3]
Take a prime divisor $q$ of $n$.

(2) $q \notin \FinSet{p}{1}{r}$.

Proof by contradiction.
Take a natural number $i$ such that $1 \leq i \leq r$
and $q=p_{i}$.
$q$ is a divisor of $n$.
$i \in \dom(p)$. 
$p_{i}$ is a divisor of $\Prod{p}{1}{r}$
(by Factorproperty, 1).
Thus $q$ divides $1$. [timelimit 10]
Contradiction. qed.
[timelimit 3]
\end{proof}
\end{forthel}

\begin{thebibliography}{plain}

\bibitem{Isabelle} The Isabelle Proof Assistant. \url{https://isabelle.in.tum.de/}

\bibitem{Knaster}
B. Knaster. Un théorème sur les fonctions d'ensembles. With A. Tarski. 
\textit{Ann. Soc. Polon. Math.} 6: 133–134, 1928.

\bibitem{Naproche} The Naproche Natural Proof Checker. \url{https://naproche.github.io/}

\bibitem{SAD} The SAD Proof Checker. \url{http://nevidal.org/sad.en.html}

\bibitem{Rudin} Walter Rudin. \textit{Principles of Mathematical
Analysis}. McGraw Hill, 1953.

\bibitem{Russell} Bertrand Russell,
{\em The Principles of Mathematics}, Cambridge 1903, {\S}100

\bibitem{Schroeder2012} Bernd S. W. Schröder,
\textit{The fixed point property for ordered sets};
Springer, \textit{Arabian Journal of Mathematics}, vol. 1, p. 529--547

\bibitem{Tarski}
Alfred Tarski. A lattice-theoretical fixpoint theorem and its applications. 
\textit{Pacific Journal of Mathematics}. 5:2: 285–309, 1955.

\bibitem{Wiedijk} Freek Wiedijk. Formalizing 100 Theorems. \url{https://www.cs.ru.nl/~freek/100/}

\end{thebibliography}

\end{document}
