\import{order/order.tex}
\import{relation.tex}
\import{set/suc.tex}
\import{ordinal.tex}


\section{The real numbers}

\begin{signature}
    $\reals$ is a set.
\end{signature}

\begin{signature}
    $x + y$ is a set.
\end{signature}

\begin{signature}
    $x \rmul y$ is a set.
\end{signature}



\subsection{Creation of natural numbers}

\subsubsection{Defenition and axioms}

\begin{abbreviation}\label{inductive_set}
    $A$ is an inductive set iff $\emptyset\in A$ and for all $a\in A$ we have $\suc{a}\in A$.
\end{abbreviation}

\begin{abbreviation}\label{zero_is_emptyset}
    $\zero = \emptyset$.
\end{abbreviation}

\begin{axiom}\label{reals_axiom_zero_in_reals}
    $\zero \in \reals$.
\end{axiom}

\begin{axiom}\label{one_in_reals}
    $1 \in \reals$.
\end{axiom}

\begin{axiom}\label{zero_neq_one}
    $\zero \neq 1$.
\end{axiom}

\begin{axiom}\label{one_is_suc_zero}
    $\suc{\zero} = 1$.
\end{axiom}

\begin{axiom}\label{naturals_subseteq_reals}
    $\naturals \subseteq \reals$.
\end{axiom}

\begin{axiom}\label{naturals_inductive_set}
    $\naturals$ is an inductive set.
\end{axiom}

\begin{axiom}\label{naturals_smallest_inductive_set}
    Let $A$ be an inductive set.
    Then $\naturals\subseteq A$.
\end{axiom}

\begin{abbreviation}\label{is_a_natural_number}
    $n$ is a natural number iff $n \in \naturals$.
\end{abbreviation}

\begin{axiom}\label{naturals_addition_axiom_1}
    For all $n \in \naturals$ $n + \zero = \zero + n = n$.
\end{axiom}

\begin{axiom}\label{naturals_addition_axiom_2}
    For all $n, m \in \naturals$ $n + \suc{m} = \suc{n} + m = \suc{n+m}$.
\end{axiom}

\begin{axiom}\label{naturals_mul_axiom_1}
    For all $n \in \naturals$ we have $n \rmul \zero = \zero = \zero \rmul n$.
\end{axiom}

\begin{axiom}\label{naturals_mul_axiom_2}
    For all $n,m \in \naturals$ we have $\suc{n} \rmul m = (n \rmul m) + m$.
\end{axiom}

\begin{axiom}\label{addition_on_naturals}
    If $x$ is a natural number and $y$ is a natural number then $x+y$ is a natural number.
\end{axiom}

\begin{axiom}\label{naturals_rmul_is_closed_in_n}
    For all $n,m \in \naturals$ we have $(n \rmul m) \in \naturals$.
\end{axiom}

\begin{axiom}\label{naturals_add_is_closed_in_n}
    For all $n,m \in \naturals$ we have $(n + m) \in \naturals$.
\end{axiom}

\subsubsection{Natural numbers as ordinals}


\begin{lemma}\label{nat_is_successor_ordinal}
    Let $n\in\naturals$.
    Suppose $n\neq \emptyset$.
    Then $n$ is a successor ordinal.
\end{lemma}
\begin{proof}
    Let $M = \{ m\in \naturals \mid\text{$m = \emptyset$ or $m$ is a successor ordinal}\}$.
    $M$ is an inductive set by \cref{suc_ordinal,naturals_inductive_set,successor_ordinal,emptyset_is_ordinal}.
    Now $M\subseteq \naturals\subseteq M$
        by \cref{subseteq,naturals_smallest_inductive_set}.
    Thus $M = \naturals$.
    Follows by \cref{subseteq}.
\end{proof}

\begin{lemma}\label{nat_is_transitiveset}
    $\naturals$ is \in-transitive.
\end{lemma}
\begin{proof}
    Let $M = \{ m\in\naturals \mid \text{for all $n\in m$ we have $n\in\naturals$} \}$.
    $\emptyset\in M$.
    For all $n\in M$ we have $\suc{n}\in M$
        by \cref{naturals_inductive_set,suc}.
    Thus $M$ is an inductive set.
    Now $M\subseteq \naturals\subseteq M$
        by \cref{subseteq,naturals_smallest_inductive_set}.
    Hence $\naturals = M$.
\end{proof}

\begin{lemma}\label{natural_number_is_ordinal}
    Every natural number is an ordinal.
\end{lemma}
\begin{proof}
    Follows by \cref{suc_ordinal,suc_neq_emptyset,naturals_inductive_set,nat_is_successor_ordinal,successor_ordinal,suc_ordinal_implies_ordinal}.
\end{proof}

\begin{lemma}\label{omega_is_an_ordinal}
    $\naturals$ is an ordinal.
\end{lemma}
\begin{proof}
    Follows by \cref{natural_number_is_ordinal,transitive_set_of_ordinals_is_ordinal,nat_is_transitiveset}.
\end{proof}

\begin{lemma}\label{omega_is_a_limit_ordinal}
    $\naturals$ is a limit ordinal.
\end{lemma}
\begin{proof}
    $\emptyset\precedes \naturals$.
    If $n\in \naturals$, then $\suc{n}\in\naturals$.
\end{proof}


\subsubsection{Properties and Facts natural numbers}

\begin{theorem}\label{induction_principle}
    Let $P$ be a set.
    Suppose $P \subseteq \naturals$.
    Suppose $\zero \in P$.
    Suppose $\forall n \in P. \suc{n} \in P$.
    Then $P = \naturals$.
\end{theorem}
\begin{proof}
    Trivial.
\end{proof}

\begin{proposition}\label{existence_of_suc}
    Let $n \in \naturals$.
    Suppose $n \neq \zero$.
    Then there exist $n' \in \naturals$ such that $\suc{n'} = n$.
\end{proposition}
\begin{proof}
    Follows by \cref{transitiveset,nat_is_transitiveset,suc_intro_self,successor_ordinal,nat_is_successor_ordinal}.
\end{proof}

\begin{proposition}\label{suc_eq_plus_one}
    Let $n \in \naturals$.
    Then $\suc{n} = n + 1$.
\end{proposition}
\begin{proof}
    Let $P = \{ n \in \naturals \mid n + 1 = 1 + n  \}$.
    $\zero \in P$.
    It suffices to show that if $m \in P$ then $\suc{m} \in P$.
\end{proof}

\begin{proposition}\label{naturals_1_kommu}
    Let $n \in \naturals$.
    Then $1 + n = n + 1$.
\end{proposition}
\begin{proof}
    Follows by \cref{suc_eq_plus_one,naturals_addition_axiom_2,naturals_addition_axiom_1,naturals_inductive_set,one_is_suc_zero}.
\end{proof}

\begin{proposition}\label{naturals_add_kommu}
    For all $n \in \naturals$ we have for all $m\in \naturals$ we have $n + m = m + n$.
\end{proposition}
\begin{proof}
    Fix $n \in \naturals$.
    Let $P = \{ m \in \naturals \mid m + n = n + m \}$.
    It suffices to show that $P = \naturals$.
    $P \subseteq \naturals$.
    $\zero \in P$.
    It suffices to show that if $m \in P$ then $\suc{m} \in P$.
\end{proof}

\begin{proposition}\label{naturals_add_assoc}
    Suppose $n,m,k \in \naturals$.
    Then $n + (m + k) = (n + m) + k$.
\end{proposition}
\begin{proof}
    Let $P = \{ k \in \naturals \mid \text{for all $n',m' \in \naturals$ we have $n' + (m' + k) = (n' + m') + k$}\}$.
    $P \subseteq \naturals$.
    $\zero \in P$.
    It suffices to show that for all $k \in P$ we have $\suc{k} \in P$.
    Fix $k \in P$.
    It suffices to show that for all $n' \in \naturals$ we have for all $m' \in \naturals$ we have $n' + (m' + \suc{k}) = (n' + m') + \suc{k}$.
    Fix $n' \in \naturals$.
    Fix $m' \in \naturals$.
    \begin{align*}
        (n' + m') + \suc{k}    \\
        &= \suc{(n' + m') + k}   \\
        &= \suc{n' + (m' + k)} \\
        &= n' + \suc{(m' + k)} \\
        &= n' + (m' + \suc{k})
    \end{align*}
\end{proof}

\begin{proposition}\label{naturals_rmul_one_left}
    For all $n \in \naturals$ we have $1 \rmul n = n$.
\end{proposition}
\begin{proof}
    Fix $n \in \naturals$.
    \begin{align*}
        1 \rmul n  \\
        &= \suc{\zero} \rmul n \\
        &= (\zero \rmul n) + n \\
        &= (\zero) + n \\
        &= n
    \end{align*}
\end{proof}

\begin{proposition}\label{naturals_add_remove_brakets}
    Suppose $n,m,k \in \naturals$.
    Then $(n + m) + k = n + m + k = n + (m + k)$.    
\end{proposition}

\begin{proposition}\label{naturals_add_remove_brakets2}
    Suppose $n,m,k,l \in \naturals$.
    Then $(n + m) + (k + l)= n + m + k + l = n + (m + k) + l = (((n + m) + k) + l)$.    
\end{proposition}

\begin{proposition}\label{natural_disstro}
    Suppose $n,m,k \in \naturals$.
    Then $n \rmul (m + k) = (n \rmul m) + (n \rmul k)$.
\end{proposition}
\begin{proof}
    Let $P = \{n \in \naturals \mid \text{for all $m,k \in \naturals$ we have $n \rmul (m + k) = (n \rmul m) + (n \rmul k)$}\}$.
    $\zero \in P$.
    $P \subseteq \naturals$.
    It suffices to show that for all $n \in P$ we have $\suc{n} \in P$.
    Fix $n \in P$.

    It suffices to show that for all $m'$ such that $m' \in \naturals$ we have for all $k' \in \naturals$ we have $\suc{n} \rmul (m' + k') = (\suc{n} \rmul m') + (\suc{n} \rmul k')$.
    Fix $m' \in \naturals$.
    Fix $k' \in \naturals$.
    $n \in \naturals$.
    \begin{align*}
        \suc{n} \rmul (m' + k') \\
        &= (n \rmul (m' + k')) + (m' + k') \\% \explanation{by \cref{naturals_mul_axiom_2}}\\
        &= ((n \rmul m') + (n \rmul k')) + (m' + k') \\%\explanation{by assumption}\\
        &= ((n \rmul m') + (n \rmul k')) + m' + k'   \\%\explanation{by \cref{naturals_add_remove_brakets,naturals_add_kommu}}\\
        &= (((n \rmul m') + (n \rmul k')) + m') + k' \\%\explanation{by \cref{naturals_add_kommu,naturals_add_remove_brakets,naturals_add_assoc}}\\
        &= (m' + ((n \rmul m') + (n \rmul k'))) + k' \\%\explanation{by \cref{naturals_add_kommu}}\\
        &= ((m' + (n \rmul m')) + (n \rmul k')) + k' \\%\explanation{by \cref{naturals_add_assoc}}\\
        &= (((n \rmul m') + m') + (n \rmul k')) + k' \\%\explanation{by \cref{naturals_add_kommu}}\\
        &= ((n \rmul m') + m') + ((n \rmul k') + k') \\%\explanation{by \cref{naturals_add_assoc}}\\
        &= (\suc{n} \rmul m') + (\suc{n} \rmul k')   %\explanation{by \cref{naturals_mul_axiom_2}}
    \end{align*}
\end{proof}

\begin{proposition}\label{naturals_rmul_one_kommu}
    For all $n \in \naturals$ we have $n \rmul 1 = n$.
\end{proposition}
\begin{proof}
    Let $P = \{ n \in \naturals \mid n \rmul 1 = n\}$.
    $1 \in P$.
    It suffices to show that for all $n' \in P$ we have $\suc{n'} \in P$.
    Fix $n' \in P$.
    It suffices to show that $\suc{n'} \rmul 1 = \suc{n'}$.
    \begin{align*}
        \suc{n'} \rmul 1 \\
        &=  n' \rmul 1 + 1 \\
        &=  n' + 1 \\
        &= \suc{n'}
    \end{align*}
\end{proof}

\begin{proposition}\label{naturals_rmul_kommu}
    Let $n, m \in \naturals$.
    Then $n \rmul m = m \rmul n$.
\end{proposition}
\begin{proof}
    Let $P = \{n \in \naturals \mid \forall m \in \naturals. n \rmul m = m \rmul n\}$.
    $\zero \in P$.
    $P \subseteq \naturals$.
    It suffices to show that for all $n \in P$ we have $\suc{n} \in P$.
    Fix $n \in P$.
    It suffices to show that for all $m \in \naturals$ we have $\suc{n} \rmul m = m \rmul \suc{n}$.
    Fix $m \in \naturals$.
    $n \rmul m = m \rmul n$.
    \begin{align*}
        \suc{n} \rmul m \\
        &= (n \rmul m) + m \\
        &= (m \rmul n) + m \\
        &= m + (m \rmul n) \\
        &= (m \rmul 1) + (m \rmul n) \\
        &= m \rmul (1 + n) \\
        &= m \rmul \suc{n} \\
    \end{align*}
\end{proof}

\begin{proposition}\label{naturals_rmul_assoc}
    Suppose $n,m,k \in \naturals$.
    Then $n \rmul (m \rmul k) = (n \rmul m) \rmul k$.
\end{proposition}
\begin{proof}
    Let $P = \{ n \in \naturals \mid \text{for all $m,k \in \naturals$ we have $n \rmul (m \rmul k) = (n \rmul m) \rmul k$ }\}$.
    $\zero \in P$.
    It suffices to show that for all $n' \in P$ we have $ \suc{n'} \in P$.
    Fix $n' \in P$.
    It suffices to show that for all $m' \in \naturals$ we have for all $k' \in \naturals$ we have $\suc{n'} \rmul (m' \rmul k') = (\suc{n'} \rmul m') \rmul k'$.
    Fix $m' \in \naturals$.
    Fix $k' \in \naturals$.
    \begin{align*}
        \suc{n'} \rmul (m' \rmul k')                \\
        &=(n' \rmul (m' \rmul k')) + (m' \rmul k')  \\
        &=((n' \rmul m') \rmul k') + (m' \rmul k')  \\
        &=(k' \rmul (n' \rmul m')) + (k' \rmul m')  \\
        &=k' \rmul ((n' \rmul m') + m')             \\
        &=k' \rmul (\suc{n'} \rmul m')              \\
        &=(\suc{n'} \rmul m') \rmul k'              
    \end{align*}
\end{proof}

\begin{lemma}\label{naturals_is_equal_to_two_times_naturals}
    $\{x+y \mid x \in \naturals, y \in \naturals \} = \naturals$.
\end{lemma}


\subsection{Axioms of the reals Part One}
We seen before that we can proof the common behavior of the naturals.
Since we now want to get furhter in a more efficient way, we introduce the basis axioms of the reals.
Such that we can introduce the integers and raitionals as smooth as possible.

\begin{axiom}\label{reals_rmul}
    For all $n,m \in \reals$ we have $(n \rmul m) \in \reals$.
\end{axiom}

\begin{axiom}\label{reals_add}
    For all $n,m \in \reals$ we have $(n + m) \in \reals$.
\end{axiom}



\begin{axiom}\label{reals_axiom_kommu}
    For all $x,y \in \reals$ $x + y = y + x$ and $x \rmul y = y \rmul x$.
\end{axiom}
  
\begin{axiom}\label{reals_axiom_zero}
    For all $x \in \reals$ $x + \zero = x$. 
\end{axiom}

\begin{axiom}\label{reals_axiom_one}
    For all $x \in \reals$ we have $x \rmul 1 = x$.
\end{axiom}

\begin{axiom}\label{reals_axiom_add_invers}
    For all $x \in \reals$ there exist $y \in \reals$ such that $x + y = \zero$.
\end{axiom}

\begin{axiom}\label{reals_axiom_mul_invers}
    For all $x \in \reals$ such that $x \neq \zero$ there exist $y \in \reals$ such that $x \rmul y = 1$.
\end{axiom}

\begin{axiom}\label{reals_axiom_disstro1}
    For all $x,y,z \in \reals$ $x \rmul (y + z) = (x \rmul y) + (x \rmul z)$.
\end{axiom}

\begin{axiom}\label{reals_disstro2}
    For all $x,y,z \in \reals$ $(y + z) \rmul x = (y \rmul x) + (z \rmul x)$.
\end{axiom}

\begin{axiom}\label{reals_reducion_on_addition}
    For all $x,y,z \in \reals$ if $x + y = x + z$ then $y = z$.
\end{axiom}

\begin{abbreviation}\label{rless}
    $x < y$ iff $x \rless y$.
\end{abbreviation}

\begin{abbreviation}\label{less_on_reals}
    $x \leq y$ iff it is wrong that $y < x$.
\end{abbreviation}

\begin{abbreviation}\label{greater_on_reals}
    $x > y$ iff $y \leq x$.
\end{abbreviation}

\begin{abbreviation}\label{greatereq_on_reals}
    $x \geq y$ iff it is wrong that $x < y$.
\end{abbreviation}

\begin{abbreviation}\label{is_positiv}
    $x$ is positiv iff $x > \zero$.
\end{abbreviation}





\begin{axiom}\label{tarski1}
    For all $x,y \in \reals$ we have if $x < y$ then $\lnot y < x$.
\end{axiom}

\begin{axiom}\label{tarski2}
    For all $x,y \in \reals$ if $x < y$ then 
    there exist $z \in \reals$ such that $x < z$ and $z < y$.
\end{axiom}

\begin{axiom}\label{tarski3}
    For all $X,Y,x,y$ such that $X,Y \subseteq \reals$ and $x \in X$ and $y \in Y$ and $x < y$ we have there exist $z \in \reals$
    such that $x < z < y$.
\end{axiom}

\begin{axiom}\label{tarski4}
    For all $x,y,z \in \reals$ $(x + y) + z = x + (y + z)$ and $(x \rmul y) \rmul z = x \rmul (y \rmul z)$.
\end{axiom}

\begin{axiom}\label{tarski5}
    For all $x,y \in \reals$ we have there exist $z \in \reals$ such that $x + z = y$.
\end{axiom}


\begin{axiom}\label{tarski8}
    $\zero < 1$.
\end{axiom}

\begin{axiom}\label{labelordersossss}
    For all $x,y \in \reals$ such that $x < y$ we have for all $z \in \reals$ $x + z < y + z$.
\end{axiom}

\begin{axiom}\label{nocheinschoeneslabel}
    For all $x,y \in \reals$ such that $\zero < x,y$ we have $\zero < (x \rmul y)$. 
\end{axiom}


\subsection{The Intergers}


\begin{axiom}\label{neg}
    For all $n \in \reals$ we have $\neg{n} \in \reals$ and $n + \neg{n} = \zero$.
\end{axiom}

\begin{axiom}\label{neg_of_zero}
    $\neg{\zero} = \zero$.
\end{axiom}

\begin{definition}\label{minus}
    $n - m = n + \neg{m}$.
\end{definition}

\begin{lemma}\label{minus_in_reals}
    Suppose $n,m \in \reals$.
    Then $n - m \in \reals$.
\end{lemma}
\begin{proof}
    \begin{byCase}
        \caseOf{$m = \zero$.} Trivial.
        \caseOf{$m \neq \zero$.} Trivial.
    \end{byCase}
\end{proof}

\begin{proposition}\label{negation_of_negation_is_id}
    For all $r \in \reals$ we have $\neg{\neg{r}} = r$.
\end{proposition}
\begin{proof}
    Fix $r \in \reals$.
    $r + \neg{r} = \zero$.
    $\neg{r} + \neg{\neg{r}} = \zero$.
    Follows by \cref{reals_reducion_on_addition,neg,reals_axiom_kommu}.
\end{proof}

\begin{definition}\label{integers}
    $\integers = \{ z \in \reals \mid \exists n \in \naturals. z \in \naturals \lor  n + z = \zero\}$.
\end{definition}

\begin{lemma}\label{n_subset_z}
    $\naturals \subseteq \integers$.
\end{lemma}

\begin{lemma}\label{neg_of_naturals_in_integers}
    For all $n \in \naturals$ we have $\neg{n} \in \integers$.
\end{lemma}

\begin{lemma}\label{integers_eq_naturals_and_negativ_naturals}
    $\integers = \{ z \in \reals \mid \exists n \in \naturals. n = z \lor \neg{n} = z\}$.
\end{lemma}
\begin{proof}
    Omitted.
\end{proof}

\begin{abbreviation}\label{positiv_real_number}
    $r$ is a positiv real number iff $r > \zero$ and $r \in \reals$.
\end{abbreviation}



\begin{proposition}\label{integers_negativ_times_negativ_is_positiv}
    Suppose $n,m \in \integers$.
    Suppose $n < \zero$ and $m < \zero$.
    Then $n \rmul m > \zero$.
\end{proposition}
\begin{proof}
    Omitted.
    %$n \neq \zero$ and $m \neq \zero$.
    %For all $k \in \naturals$ we have $k = \zero \lor k > \zero$.
    %There exists $n' \in \reals$ such that $n' + n = \zero$.
    %There exists $m' \in \reals$ such that $m' + m = \zero$.
\end{proof}

%TODO: negativ * negativ = positiv.


\subsection{The Rationals}

\begin{axiom}\label{invers_reals}
    For all $q \in \reals$ we have $\inv{q} \rmul q = 1$.
\end{axiom}

\begin{abbreviation}\label{rfrac}
    $\rfrac{x}{y} = x \rmul \inv{y}$.
\end{abbreviation}

\begin{abbreviation}\label{naturalsplus}
    $\naturalsPlus = \naturals \setminus \{\zero\}$.
\end{abbreviation}

\begin{definition}\label{rationals} %TODO: Vielleicht ist hier die definition das alle inversen von den ganzenzahlen und die ganzenzahlen selbst die rationalen zahlen erzeugen
    $\rationals = \{ q \in \reals \mid \exists z \in \integers. \exists n \in \naturalsPlus. q = \rfrac{z}{n} \}$.
\end{definition}

\begin{abbreviation}\label{nominator}
    $z$ is nominator of $q$ iff there exists $n \in \naturalsPlus$ such that $q = \rfrac{z}{n}$.
\end{abbreviation}

\begin{abbreviation}\label{denominator}
    $n$ is denominator of $q$ iff there exists $z \in \integers$ such that $q = \rfrac{z}{n}$.
\end{abbreviation}

%\begin{proposition}\label{q_is_less_then_p_if_denominator_is_bigger_and_nominator_is_equal}
%    Suppose $p,q \in \rationals$.
%    Suppose $z \in \naturals$.
%    Suppose $p$ is positiv.
%    Suppose $q$ is positiv.
%    Suppose $z$ is nominator of $p$.
%    Suppose $z$ is nominator of $p$.
%    Suppose $p'$ is denominator of $p$.
%    Suppose $q'$ is denominator of $q$.
%    Then $p \leq q$ iff $p' \geq q'$.
%\end{proposition}


%\begin{theorem}\label{one_divided_by_n_is_in_zero_to_one}
%    For all $n \in \naturalsPlus$ we have $\zero < \rfrac{1}{n} \leq 1$.
%\end{theorem}

% TODO:  Was man noch so beweisen könnte: bruch kürzung, kehrbruch eigenschaften, bruch in bruch vereinfachung, 


\subsection{Order on the reals}



\begin{lemma}\label{plus_one_order}
    For all $r\in \reals$ we have $ r < r + 1$.
\end{lemma}
\begin{proof}
    Omitted.
\end{proof}

\begin{lemma}\label{negation_and_order}
    Suppose $r \in \reals$.
    $r \leq \zero$ iff $\zero \leq \neg{r}$.
\end{lemma}
\begin{proof}
    Omitted.
\end{proof}


\begin{lemma}\label{reals_add_of_positiv}
    Let $x,y \in \reals$.
    Suppose $x$ is positiv and $y$ is positiv.
    Then $x + y$ is positiv.
\end{lemma}
\begin{proof}
    Omitted.
\end{proof}

\begin{lemma}\label{reals_mul_of_positiv}
    Let $x,y \in \reals$.
    Suppose $x$ is positiv and $y$ is positiv.
    Then $x \rmul y$ is positiv.
\end{lemma}
\begin{proof}
    Omitted.
\end{proof}



\begin{lemma}\label{order_reals_lemma0}
    For all $x \in \reals$ we have not $x < x$.
\end{lemma}
\begin{proof}
    Omitted.
\end{proof}


\begin{lemma}\label{order_reals_lemma1}
    Let $x,y,z \in \reals$.
    Suppose $\zero < x$. 
    Suppose $y < z$. 
    Then $(y \rmul x) < (z \rmul x)$.
\end{lemma}
\begin{proof}
    Omitted.
    %There exist $k \in \reals$ such that $y + k = z$ and $k > \zero$ by \cref{reals_definition_order_def}.
    %\begin{align*}
    %    (z \rmul x) \\
    %    &= ((y + k) \rmul x) \\
    %    &= ((y \rmul x) + (k \rmul x)) \explanation{by \cref{reals_disstro2}}
    %\end{align*} 
    %Then $(k \rmul x) > \zero$. 
    %Therefore $(z \rmul x) > (y \rmul x)$.
\end{proof}

\begin{lemma}\label{order_reals_lemma2}
    Let $x,y,z \in \reals$.
    Suppose $\zero < x$. 
    Suppose $y < z$. 
    Then $(x \rmul y) < (x \rmul z)$.
\end{lemma}
\begin{proof}
    Omitted.
\end{proof}


\begin{lemma}\label{order_reals_lemma3}
    Let $x,y,z \in \reals$.
    Suppose $\zero < x$. 
    Suppose $y < z$. 
    Then $(x \rmul z) < (x \rmul y)$.
\end{lemma}
\begin{proof}
    Omitted.
\end{proof}

\begin{lemma}\label{order_reals_lemma00}
    For all $x,y \in \reals$ such that $x > y$ we have $x \geq y$.
\end{lemma}
\begin{proof}
    Omitted.
\end{proof}

\begin{lemma}\label{order_reals_lemma5}
    For all $x,y \in \reals$ such that $x < y$ we have $x \leq y$.
\end{lemma}
\begin{proof}
    Omitted.
\end{proof}

\begin{lemma}\label{order_reals_lemma6}
    For all $x,y \in \reals$ such that $x \leq y \leq x$ we have $x=y$.
\end{lemma}
\begin{proof}
    Omitted.
\end{proof}

\begin{lemma}\label{reals_minus}
    Assume $x,y \in \reals$. If $x \rminus y = \zero$ then $x=y$.
\end{lemma}
\begin{proof}
    Omitted.
\end{proof}

\begin{definition}\label{upper_bound}
    $x$ is an upper bound of $X$ iff for all $y \in X$ we have $x > y$.
\end{definition}

\begin{definition}\label{least_upper_bound}
    $x$ is a least upper bound of $X$ iff $x$ is an upper bound of $X$ and for all $y$ such that $y$ is an upper bound of $X$ we have $x \leq y$.
\end{definition}

\begin{lemma}\label{supremum_unique}
    %Let $x,y \in \reals$ and let $X$ be a subset of $\reals$.
    If $x$ is a least upper bound of $X$ and $y$ is a least upper bound of $X$ then $x = y$.
\end{lemma}
\begin{proof}
    Omitted.
\end{proof}

\begin{definition}\label{supremum_reals}
    $x$ is the supremum of $X$ iff $x$ is a least upper bound of $X$.
\end{definition}




\begin{definition}\label{lower_bound}
    $x$ is an lower bound of $X$ iff for all $y \in X$ we have $x < y$.
\end{definition}

\begin{definition}\label{greatest_lower_bound}
    $x$ is a greatest lower bound of $X$ iff $x$ is an lower bound of $X$ and for all $y$ such that $y$ is an lower bound of $X$ we have $x \geq y$.
\end{definition}

\begin{lemma}\label{infimum_unique}
    If $x$ is a greatest lower bound of $X$ and $y$ is a greatest lower bound of $X$ then $x = y$.
\end{lemma}
\begin{proof}
    Omitted.
\end{proof}

\begin{definition}\label{infimum_reals}
    $x$ is the supremum of $X$ iff $x$ is a greatest lower bound of $X$.
\end{definition}












%\begin{proposition}\label{safe}
%    Contradiction.
%\end{proposition}