From acbde8031d18ff5ccbdb2842f57cbe1c628de0d0 Mon Sep 17 00:00:00 2001
From: Simon-Kor <52245124+Simon-Kor@users.noreply.github.com>
Date: Tue, 25 Jun 2024 00:01:31 +0200
Subject: Sorted the structure of numbers.tex

---
 library/numbers.tex | 231 ++++++++++++++++++++++++++++++++++++++--------------
 1 file changed, 168 insertions(+), 63 deletions(-)

(limited to 'library')

diff --git a/library/numbers.tex b/library/numbers.tex
index 2451730..1837ae8 100644
--- a/library/numbers.tex
+++ b/library/numbers.tex
@@ -1,49 +1,52 @@
-\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.
+    $x + y$ is a set.
 \end{signature}
 
 \begin{signature}
     $x \rmul y$ is a set.
 \end{signature}
 
+\subsection{Basic axioms of the reals}
+
+\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{reals_axiom_order}
-    $\lt[\reals]$ is an order on $\reals$.
+\begin{axiom}\label{zero_neq_one}
+    $\zero \neq 1$.
 \end{axiom}
 
-\begin{axiom}\label{reals_axiom_strictorder}
-    $\lt[\reals]$ is a strict order.
-\end{axiom}
+\begin{definition}\label{reals_definition_order_def}
+    $x < y$ iff there exist $z \in \reals$ such that $x + (z \rmul z) = y$.
+\end{definition}
+
+%\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 $(x,y) \in \lt[\reals]$.
+    $x \leq y$ iff it is wrong that $y < x$.
 \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$.
+    $x > y$ iff $y \leq x$.
 \end{abbreviation}
 
 \begin{abbreviation}\label{greatereq_on_reals}
@@ -55,100 +58,165 @@
     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)$.
+    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 \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$.
+    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 \add \zero = x$. 
+    For all $x \in \reals$ $x + \zero = x$. 
 \end{axiom}
 
 \begin{axiom}\label{reals_axiom_one}
-    For all $x \in \reals$ $1 \neq \zero$ and $x \rmul 1 = x$.
+    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 \add y = \zero$.
+    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 \add z) = (x \rmul y) \add (x \rmul z)$.
+    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 \add z) \rmul x = (y \rmul x) \add (z \rmul x)$.
+    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 \add y = x \add z$ then $y = z$.
+    For all $x,y,z \in \reals$ if $x + y = x + 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{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{abbreviation}\label{is_positiv}
+    $x$ is positiv iff $x > \zero$.
+\end{abbreviation}
+
+\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}
-    For all $x,y,z \in \reals$ such that $\zero < x$ 
-    if $y < z$ 
-    then $(y \rmul x) < (z \rmul x)$.
+    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}
-    For all $x,y,z \in \reals$ such that $\zero < x$ 
-    if $y < z$ 
-    then $(x \rmul y) < (x \rmul z)$.
+    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}
-    For all $x,y,z \in \reals$ such that $x < \zero$ 
-    if $y < z$ 
-    then $(x \rmul z) < (x \rmul y)$.
+    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{o4rder_reals_lemma}
-    For all $x,y \in \reals$ if $x > y$ then $x \geq y$.
+\begin{lemma}\label{order_reals_lemma00}
+    For all $x,y \in \reals$ such that $x > y$ we have $x \geq y$.
 \end{lemma}
 
+
 \begin{lemma}\label{order_reals_lemma5}
-    For all $x,y \in \reals$ if $x < y$ then $x \leq y$.
+    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$ if $x \leq y \leq x$ then $x=y$.
+    For all $x,y \in \reals$ such that $x \leq y \leq x$ we have $x=y$.
 \end{lemma}
-
-\begin{axiom}\label{reals_axiom_minus}
-    For all $x \in \reals$ $x \rmiuns x = \zero$.
-\end{axiom}
+\begin{proof}
+    Omitted.
+\end{proof}
 
 \begin{lemma}\label{reals_minus}
-    Assume $x,y \in \reals$. If $x \rmiuns y = \zero$ then $x=y$.
+    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$.
@@ -162,6 +230,9 @@
     %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$.
@@ -181,8 +252,42 @@
 \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}
 
+
+
+
+\section{The natural numbers}
+
+
+\begin{abbreviation}\label{def_suc}
+    $\successor{n} = n + 1$.
+\end{abbreviation}
+
+\begin{inductive}\label{naturals_definition_as_subset_of_reals}
+    Define $\nat \subseteq \reals$ inductively as follows.
+    \begin{enumerate}
+        \item $\zero \in \nat$.
+        \item If $n\in \nat$, then $\successor{n} \in \nat$. 
+    \end{enumerate}
+\end{inductive}
+
+\begin{lemma}\label{reals_order_suc}
+    $n < \successor{n}$.
+\end{lemma}
+
+%\begin{proposition}\label{safe}
+%    Contradiction.
+%\end{proposition}
+
+\section{The integers}
+
+%\begin{definition}
+%    $\integers = \{z \in \reals \mid z = \zero or \} $.
+%\end{definition}
\ No newline at end of file
-- 
cgit v1.2.3