\import{nat.tex}
\import{order/order.tex}
\import{relation.tex}

\section{The real numbers}

%TODO:
%\inv{} für inverse benutzen. Per Signatur einfüheren und dann axiomatisch absicher
%\cdot für multiklikation verwenden. 
%< für die relation benutzen.
% sup und inf einfügen

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

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

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

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

\begin{axiom}\label{reals_axiom_order}
    $\lt[\reals]$ is an order on $\reals$.
\end{axiom}

\begin{axiom}\label{reals_axiom_strictorder}
    $\lt[\reals]$ is a strict order.
\end{axiom}

\begin{abbreviation}\label{less_on_reals}
    $x < y$ iff $(x,y) \in \lt[\reals]$.
\end{abbreviation}

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

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

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

\begin{axiom}\label{reals_axiom_dense}
    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{reals_axiom_order_def}
    $x < y$ iff there exist $z \in \reals$ such that $\zero < z$ and $x \add z = y$.
\end{axiom}

\begin{lemma}\label{reals_one_bigger_than_zero}
    $\zero < 1$.
\end{lemma}


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

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

\begin{axiom}\label{reals_axiom_zero_in_reals}
    $\zero \in \reals$.
\end{axiom}
  
\begin{axiom}\label{reals_axiom_zero}
    For all $x \in \reals$ $x \add \zero = x$. 
\end{axiom}

\begin{axiom}\label{reals_axiom_one}
    For all $x \in \reals$ $1 \neq \zero$ and $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 \add 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 \add z) = (x \rmul y) \add (x \rmul z)$.
\end{axiom}

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

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

\begin{axiom}\label{reals_axiom_dedekind_complete}
    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{lemma}\label{order_reals_lemma1}
    For all $x,y,z \in \reals$ such that $\zero < x$ 
    if $y < z$ 
    then $(y \rmul x) < (z \rmul x)$.
\end{lemma}

\begin{lemma}\label{order_reals_lemma2}
    For all $x,y,z \in \reals$ such that $\zero < x$ 
    if $y < z$ 
    then $(x \rmul y) < (x \rmul z)$.
\end{lemma}


\begin{lemma}\label{order_reals_lemma3}
    For all $x,y,z \in \reals$ such that $x < \zero$ 
    if $y < z$ 
    then $(x \rmul z) < (x \rmul y)$.
\end{lemma}

\begin{lemma}\label{o4rder_reals_lemma}
    For all $x,y \in \reals$ if $x > y$ then $x \geq y$.
\end{lemma}

\begin{lemma}\label{order_reals_lemma5}
    For all $x,y \in \reals$ if $x < y$ then $x \leq y$.
\end{lemma}

\begin{lemma}\label{order_reals_lemma6}
    For all $x,y \in \reals$ if $x \leq y \leq x$ then $x=y$.
\end{lemma}

\begin{axiom}\label{reals_axiom_minus}
    For all $x \in \reals$ $x \rmiuns x = \zero$.
\end{axiom}

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

\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{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{definition}\label{infimum_reals}
    $x$ is the supremum of $X$ iff $x$ is a greatest lower bound of $X$.
\end{definition}