\documentclass{article}

\usepackage[english]{babel}

\usepackage{amsmath}
% for symbols such as /implies
\usepackage{amssymb}
% for symbols such as /subsetneq
\usepackage{amsthm}
% for commands such as \newtheorem

\theoremstyle{definition}
\newtheorem{theorem}{Theorem}
\newtheorem{lemma}[theorem]{Lemma}
\newtheorem{corollary}[theorem]{Corollary}
\newtheorem{definition}{Definition}
\newtheorem{example}{Example}
\newtheorem{axiom}{Axiom}

\begin{document}

\section{Real Numbers}

This page serves as an introduction to the real numbers in an axiomatic way. We assume only basic knowledge of predicate logic, sets, binary operations, and order relations. We shall construct the real numbers more carefully from ZF set theory later.

\begin{definition}
  The real numbers $\mathbb{R}$ is a set with binary operations $+,\cdot$ and a total order relation $<$ satisfying the 14 axioms that follow.
\end{definition}

\begin{axiom}[Associativity of Addition]
  $$
    \forall a,b,c\in\mathbb{R} \quad (a+b)+c = a+(b+c)
  $$
\end{axiom}

\begin{axiom}[Identity of Addition]
  $$
    \exists e\in\mathbb{R} \ \forall a\in\mathbb{R} \quad a+e=e+a=a
  $$
  Such an element $e$ is called an \emph{additive identity}.
\end{axiom}

\begin{theorem}[Uniqueness of Additive Identity]
  The additive identity $e\in\mathbb{R}$ from Axiom 2 is unique. We denote the additive identity by 0.
  \begin{proof}
    Suppose $e_1,e_2\in\mathbb{R}$ are additive identities. Then, by Axiom 2
    $$
      e_1 = e_1 + e_2
    $$
    since $e_2$ is an additive identity. Likewise, by Axiom 2
    $$
      e_1 + e_2 = e_2
    $$
    since $e_1$ is an additive identity. It follows that $e_1=e_2$.
  \end{proof}
\end{theorem}

\begin{axiom}[Inverse of Addition]
  $$
    \forall a\in\mathbb{R} \ \exists b\in\mathbb{R} \quad a+b=b+a=0
  $$
  Such an element $b$ is called an \emph{additive inverse} of $a$.
\end{axiom}

\begin{theorem}[Uniqueness of Additive Inverse]
  For each $a\in\mathbb{R}$, the additive inverse from Axiom 2 is unique. We denote the additive inverse of $a$ by $-a$.
  \begin{proof}
    Let $a\in\mathbb{R}$. Suppose $b,c\in\mathbb{R}$ are additive inverses of $a$. Then, by Axiom 2
    $$
      b = b + 0.
    $$
    By Axiom 3
    $$
      b + 0 = b + (a + c)
    $$
    since $c$ is an additive inverse of $a$. By Axiom 1
    $$
      b + (a + c) = (b + a) + c.
    $$
    By Axiom 3
    $$
      (b + a) + c = 0 + c
    $$
    since $b$ is an additive inverse of $a$. By Axiom 2
    $$
      0 + c = c.
    $$
    It follows that $b=c$.
  \end{proof}
\end{theorem}

\begin{axiom}[Commutativity of Addition]
  $$
    \forall a,b\in\mathbb{R} \quad a+b=b+a
  $$
\end{axiom}

\begin{axiom}[Associativity of Multiplication]
  $$
    \forall a,b,c\in\mathbb{R} \quad (a\cdot b)\cdot c = a\cdot (b\cdot c)
  $$
\end{axiom}

\begin{axiom}[Identity of Multiplication]
  $$
    \exists e\in\mathbb{R} \quad (e \neq 0) \land (\forall a\in\mathbb{R} \quad a\cdot e = e\cdot a = a)
  $$
  Such an element $e$ is called a \emph{multiplicative identity}.
\end{axiom}

\begin{theorem}[Uniqueness of Multiplicative Identity]
  The multiplicative identity $e\in\mathbb{R}$ from Axiom 6 is unique. We denote the multiplicative identity by 1.
  \begin{proof}
    Suppose $e_1,e_2\in\mathbb{R}$ are multiplicative identities. Then, by Axiom 6
    $$
      e_1 = e_1 \cdot e_2
    $$
    since $e_2$ is a multiplicative identity. Likewise, by Axiom 6
    $$
      e_1 \cdot e_2 = e_2
    $$
    since $e_1$ is a multiplicative identity. It follows that $e_1 = e_2$.
  \end{proof}
\end{theorem}

\begin{axiom}[Inverse of Multiplication]
  $$
    \forall a\in\mathbb{R}\setminus\{0\} \ \exists b\in\mathbb{R} \quad ab = ba = 1
  $$
  Such an element $b$ is called a \emph{multiplicative inverse} of $a$.
\end{axiom}

\begin{theorem}[Uniqueness of Multiplicative Inverse]
  For each $a\in\mathbb{R}\setminus\{0\}$, the multiplicative inverse from Axiom 7 is unique. We denote the multiplicative inverse of $a$ by $a^{-1}$.
  \begin{proof}
    Let $a\in\mathbb{R}\setminus\{0\}$. Suppose $b,c\in\mathbb{R}$ are multiplicative inverses of $a$. Then, by Axiom 6
    $$
      b = b \cdot 1.
    $$
    By Axiom 7
    $$
      b \cdot 1 = b \cdot (a \cdot c)
    $$
    since $c$ is a multiplicative inverse of $a$. By Axiom 5
    $$
      b \cdot (a \cdot c) = (b \cdot a) \cdot c.
    $$
    By Axiom 7
    $$
      (b \cdot a) \cdot c = 1 \cdot c
    $$
    since $b$ is a multiplicative inverse of $a$. By Axiom 6
    $$
      1 \cdot c = c.
    $$
    It follows that $b=c$.
  \end{proof}
\end{theorem}

\begin{axiom}[Commutativity of Multiplication]
  $$
    \forall a,b\in\mathbb{R} \quad a \cdot b = b \cdot a
  $$
\end{axiom}

\begin{axiom}[Distributivity]
  $$
    \forall a,b,c\in\mathbb{R} \quad a \cdot (b + c) = a \cdot b + a \cdot c
  $$
\end{axiom}

\begin{axiom}[Trichotomy of Order]
  $$
    \forall a,b\in\mathbb{R} \quad ((a < b) \veebar (a = b) \veebar (b < a)) \land \lnot ((a < b) \land (a = b) \land (b < a))
  $$
\end{axiom}
Axiom 10 states that there is a true statement among $a < b$, $a = b$, $b < a$, and when any is true the others are false. The symbol $\veebar$ represents the xor operation from predicate logic.

\begin{axiom}[Transitivity of Order]
  $$
    \forall a,b,c\in\mathbb{R} \quad (a < b) \land (b < c) \implies (a < c)
  $$
\end{axiom}

\begin{axiom}[Addition and Order]
  $$
    \forall a,b,c\in\mathbb{R} \quad a < b \implies a + c < b + c
  $$
\end{axiom}

\begin{axiom}[Multiplication and Order]
  $$
    \forall a,b,c\in\mathbb{R} \quad (c > 0) \land (a < b) \implies a \cdot c < b \cdot c
  $$
\end{axiom}

\begin{definition}
  We define the relation $\leq$ on $\mathbb{R}$ by 
  $$
    \forall a,b\in\mathbb{R} \quad a\leq b \iff (a < b) \lor (a = b).
  $$
\end{definition}

\begin{theorem}
  The relation $\leq$ on $\mathbb{R}$ is a partial order relation.
  \begin{proof}
    Since $<$ and $=$ are reflexive and transitive, so is $\leq$. Supose $a,b\in\mathbb{R}$ with $a\leq b$ and $b\leq a$. By Axiom 10, we cannot have $a = b$ and either of $a < b$ or $b < a$ simultaneously, so it must be the case that $a = b$. Then $\leq$ is antisymmetric.
  \end{proof}
\end{theorem}

\begin{definition}
  A subset $A\subseteq\mathbb{R}$ is \emph{bounded above} if
  $$
    \exists b\in\mathbb{R} \ \forall a\in A \quad a \leq b.
  $$
  Such a real number $b$ is called an \emph{upper bound} of $A$.
\end{definition}

\begin{definition}
  An upper bound $c\in\mathbb{R}$ of a subset $A\subseteq\mathbb{R}$ is a \emph{supremum}, or \emph{least upper bound}, of $A$ if for all upper bounds $b\in\mathbb{R}$ of $A$, $c \leq b$.
\end{definition}

\begin{theorem}[Uniqueness of Supremum]
  If $c\in\mathbb{R}$ is a supremum of $A \subseteq\mathbb{R}$, then it is unique. We denote $c$ by $\sup A$.
  \begin{proof}
    Suppose $c_1,c_2\in\mathbb{R}$ are supremums of $A \subseteq\mathbb{R}$.
    Then $c_1$ is an upper bound of $A$. Since $c_2$ is a supremum of $A$
    $$
      c_2 \leq c_1.
    $$
    Likewise, $c_2$ is an upper bound of $A$. Since $c_1$ is a supremum of $A$
    $$
      c_1 \leq c_2.
    $$
    Since $\leq$ is antisymmetric, it follows that $c_1 = c_2$.
  \end{proof}
\end{theorem}

\begin{axiom}[Completeness]
  $$
    \forall A\subseteq\mathbb{R} \quad (A \neq \emptyset) \land (\exists b\in\mathbb{R} \ \forall a\in A \quad a \leq b) \implies \exists c\in\mathbb{R} \quad c = \sup A
  $$
\end{axiom}
    
\end{document}