\import{order/order.tex}
\import{relation.tex}
\import{set/suc.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}

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

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

\begin{abbreviation}\label{less_on_reals}
    $x < y$ iff it is wrong that $y \leq 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}


%Structure TODO:
% Take as may axioms as needed  - Tarski Axioms of reals
%Implement Naturals -> Integer -> rationals -> reals 


\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{definition}\label{naturals}
    $\naturals = \{ x \in \reals \mid \exists y \in \reals. \suc{y} = x \lor x = \zero \}$.
\end{definition}

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

%\begin{inductive}\label{naturals_subset_reals}
%    Define $\naturals \subseteq \reals$ inductively as follows.
%    \begin{enumerate}
%        \item $\zero \in \naturals$.
%        \item If $n\in \naturals$, then $\suc{n} \in \naturals$.   %Naproche translate this to for all n \in R \suc{n} \in R we want something like the definition before. 
%    \end{enumerate}
%\end{inductive}

\begin{axiom}\label{suc_eq_plus_one}
    For all $n \in \naturals$ we have $\suc{n} = n + 1$.
\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$.
\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}


\subsubsection{Properties and Facts natural numbers}

\begin{proposition}\label{naturals_kommu}
    For all $n,m \in \naturals$ we have $n + m = m + n$.
\end{proposition}
\begin{proof}
    \begin{byCase}
        \caseOf{$n = \emptyset$.} Trivial.
        \caseOf{$m = \emptyset$.} Trivial.
        \caseOf{$n \neq \emptyset \land m \neq \emptyset$.} Omitted.
    \end{byCase}
\end{proof}
    


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


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


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

%\begin{lemma}\label{oeder_on_naturals}
%    $\lt[\reals] \inter (\naturals \times \naturals)$ is an order on $\naturals$.
%\end{lemma}






\subsection{The Intergers}




\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_assoc}
    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{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_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{proposition}\label{reals_disstro2}
    For all $x,y,z \in \reals$ $(y + z) \rmul x = (y \rmul x) + (z \rmul x)$.
\end{proposition}
\begin{proof}
    Omitted.
\end{proof}

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


%\begin{signature}\label{invers_is_set}
%    $\addInv{y}$ is a set.
%\end{signature}

%\begin{definition}\label{add_inverse}
%    $\addInv{y} = \{ x \mid \exists k \in \reals. k + y = \zero \land x \in k\}$.
%\end{definition}
    

%\begin{definition}\label{add_inverse_natural_language}
%    $x$ is additiv inverse of $y$ iff $x = \addInv{y}$. 
%\end{definition}

%\begin{lemma}\label{rminus}
%    $x \rminus \addInv{x} = \zero$.
%\end{lemma}



\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}

\section{The integers}

%\begin{definition}
%    $\integers = \{z \in \reals \mid z = \zero or \} $.
%\end{definition}