IsarMathLib

Proofs by humans, for humans, formally verified by Isabelle/ZF proof assistant

theory Real_ZF_1 imports Real_ZF Int_ZF_3 OrderedField_ZF

begin

In this theory file we continue the construction of real numbers started in Real_ZF to a succesful conclusion. We put here those parts of the construction that can not be done in the general settings of abelian groups and require integers.

Definitions and notation

In this section we define notions and notation needed for the rest of the construction.

We define positive slopes as those that take an infinite number of posititive values on the positive integers (see Int_ZF_2 for properties of positive slopes).

definition

$ PositiveSlopes \equiv \{s \in Slopes.\ $ $ s(PositiveIntegers) \cap PositiveIntegers \notin Fin(int)\} $

The order on the set of real numbers is constructed by specifying the set of positive reals. This set is defined as the projection of the set of positive slopes.

definition

$ PositiveReals \equiv \{SlopeEquivalenceRel\{s\}.\ s \in PositiveSlopes\} $

The order relation on real numbers is constructed from the set of positive elements in a standard way (see section "Alternative definitions" in OrderedGroup_ZF.)

definition

$ OrderOnReals \equiv \text{OrderFromPosSet}(RealNumbers,RealAddition,PositiveReals) $

The next locale extends the locale real0 to define notation specific to the construction of real numbers. The notation follows the one defined in Int_ZF_2.thy. If $m$ is an integer, then the real number which is the class of the slope $n\mapsto m\cdot n$ is denoted $ m^R $. For a real number $a$ notation $\lfloor a \rfloor$ means the largest integer $m$ such that the real version of it (that is, $m^R$) is not greater than $a$. For an integer $m$ and a subset of reals $S$ the expression $\Gamma(S,m)$ is defined as $\max \{\lfloor p^R\cdot x\rfloor : x\in S\}$. This is plays a role in the proof of completeness of real numbers. We also reuse some notation defined in the int0 context, like $ \mathbb{Z} _+ $ (the set of positive integers) and abs$(m)$ ( the absolute value of an integer, and some defined in the int1 context, like the addition ( $ + $) and composition ($ \circ $ of slopes.

locale real1 = real0 +

defines $ s \sim r \equiv \langle s,r\rangle \in SlopeEquivalenceRel $

defines $ s + r \equiv SlopeOp1\langle s,r\rangle $

defines $ s \circ r \equiv SlopeOp2\langle s,r\rangle $

defines $ \mathcal{S} \equiv \text{AlmostHoms}(int,IntegerAddition) $

defines $ \mathcal{S} _+ \equiv PositiveSlopes $

defines $ [f] \equiv SlopeEquivalenceRel\{f\} $

defines $ - s \equiv \text{GroupInv}(int,IntegerAddition)\circ s $

defines $ a \leq b \equiv \langle a,b\rangle \in OrderOnReals $

defines $ a \lt b \equiv a\leq b \wedge a\neq b $

defines $ \mathbb{R} _+ \equiv \text{PositiveSet}(\mathbb{R} ,RealAddition,OrderOnReals) $

defines $ m^R \equiv [\{\langle n,IntegerMultiplication\langle m,n\rangle \rangle .\ n \in int\}] $

defines $ \lfloor a\rfloor \equiv \text{Maximum}(IntegerOrder,\{m \in int.\ m^R \leq a\}) $

defines $ \Gamma (S,p) \equiv \text{Maximum}(IntegerOrder,\{\lfloor p^R\cdot x\rfloor .\ x\in S\}) $

defines $ a + b \equiv IntegerAddition\langle a,b\rangle $

defines $ - a \equiv \text{GroupInv}(int,IntegerAddition)(a) $

defines $ a - b \equiv a + ( - b) $

defines $ \mathbb{Z} _+ \equiv \text{PositiveSet}(int,IntegerAddition,IntegerOrder) $

defines $ m \leq n \equiv \langle m,n\rangle \in IntegerOrder $

defines $ a\cdot b \equiv IntegerMultiplication\langle a,b\rangle $

defines $ 0 _Z \equiv \text{ TheNeutralElement}(int,IntegerAddition) $

defines $ 1 _Z \equiv \text{ TheNeutralElement}(int,IntegerMultiplication) $

defines $ 2 _Z \equiv 1 _Z + 1 _Z $

defines $ abs(m) \equiv \text{AbsoluteValue}(int,IntegerAddition,IntegerOrder)(m) $

defines $ \delta (s,m,n) \equiv s(m + n) - s(m) - s(n) $

Multiplication of real numbers

Multiplication of real numbers is defined as a projection of composition of slopes onto the space of equivalence classes of slopes. Thus, the product of the real numbers given as classes of slopes $s$ and $r$ is defined as the class of $s\circ r$. The goal of this section is to show that multiplication defined this way is commutative.

Let's recall a theorem from Int_ZF_2.thy that states that if $f,g$ are slopes, then $f\circ g$ is equivalent to $g\circ f$. Here we conclude from that that the classes of $f\circ g$ and $g\circ f$ are the same.

lemma (in real1) Real_ZF_1_1_L2:

assumes A1: $ f \in \mathcal{S} $, $ g \in \mathcal{S} $

shows $ [f\circ g] = [g\circ f] $proof

from A1 have $ f\circ g \sim g\circ f $ using Slopes_def, Arthan_Th_9, SlopeOp1_def, BoundedIntMaps_def, SlopeEquivalenceRel_def, SlopeOp2_def

then show $ thesis $ using Real_ZF_1_L11, equiv_class_eq

qed

Classes of slopes are real numbers.

lemma (in real1) Real_ZF_1_1_L3:

assumes A1: $ f \in \mathcal{S} $

shows $ [f] \in \mathbb{R} $proof

from A1 have $ [f] \in Slopes//SlopeEquivalenceRel $ using Slopes_def, quotientI

then show $ [f] \in \mathbb{R} $ using RealNumbers_def

qed

Each real number is a class of a slope.

lemma (in real1) Real_ZF_1_1_L3A:

assumes A1: $ a\in \mathbb{R} $

shows $ \exists f\in \mathcal{S} .\ a = [f] $proof

from A1 have $ a \in \mathcal{S} //SlopeEquivalenceRel $ using RealNumbers_def, Slopes_def

then show $ thesis $ using quotient_def

qed

It is useful to have the definition of addition and multiplication in the real1 context notation.

lemma (in real1) Real_ZF_1_1_L4:

assumes A1: $ f \in \mathcal{S} $, $ g \in \mathcal{S} $

shows $ [f] + [g] = [f + g] $, $ [f] \cdot [g] = [f\circ g] $proof

let $ r = SlopeEquivalenceRel $

have $ [f]\cdot [g] = \text{ProjFun2}(\mathcal{S} ,r,SlopeOp2)\langle [f],[g]\rangle $ using RealMultiplication_def, Slopes_def

also

from A1 have $ \ldots = [f\circ g] $ using Real_ZF_1_L11, EquivClass_1_L10, Slopes_def

finally show $ [f] \cdot [g] = [f\circ g] $

have $ [f] + [g] = \text{ProjFun2}(\mathcal{S} ,r,SlopeOp1)\langle [f],[g]\rangle $ using RealAddition_def, Slopes_def

also

from A1 have $ \ldots = [f + g] $ using Real_ZF_1_L11, EquivClass_1_L10, Slopes_def

finally show $ [f] + [g] = [f + g] $

qed

The next lemma is essentially the same as Real_ZF_1_L12, but written in the notation defined in the real1 context. It states that if $f$ is a slope, then $-[f] = [-f]$.

lemma (in real1) Real_ZF_1_1_L4A:

assumes $ f \in \mathcal{S} $

shows $ [ - f] = - [f] $ using assms, Slopes_def, SlopeEquivalenceRel_def, Real_ZF_1_L12

Subtracting real numbers correspods to adding the opposite slope.

lemma (in real1) Real_ZF_1_1_L4B:

assumes A1: $ f \in \mathcal{S} $, $ g \in \mathcal{S} $

shows $ [f] - [g] = [f + ( - g)] $proof

from A1 have $ [f + ( - g)] = [f] + [ - g] $ using Slopes_def, BoundedIntMaps_def, Int_ZF_2_1_L12, Real_ZF_1_1_L4

with A1 show $ [f] - [g] = [f + ( - g)] $ using Real_ZF_1_1_L4A

qed

Multiplication of real numbers is commutative.

theorem (in real1) real_mult_commute:

assumes A1: $ a\in \mathbb{R} $, $ b\in \mathbb{R} $

shows $ a\cdot b = b\cdot a $proof

from A1 have $ \exists f\in \mathcal{S} .\ a = [f] $, $ \exists g\in \mathcal{S} .\ b = [g] $ using Real_ZF_1_1_L3A

then obtain $ f $ $ g $ where $ f \in \mathcal{S} $, $ g \in \mathcal{S} $ and $ a = [f] $, $ b = [g] $

then show $ a\cdot b = b\cdot a $ using Real_ZF_1_1_L4, Real_ZF_1_1_L2

qed

Multiplication is commutative on reals.

lemma real_mult_commutative:

shows $ RealMultiplication \text{ is commutative on } RealNumbers $ using real_mult_commute, IsCommutative_def

The neutral element of multiplication of reals (denoted as $ 1 $ in the real1 context) is the class of identity function on integers. This is really shown in Real_ZF_1_L11, here we only rewrite it in the notation used in the real1 context.

lemma (in real1) real_one_cl_identity:

shows $ [id(int)] = 1 $ using Real_ZF_1_L11

If $f$ is bounded, then its class is the neutral element of additive operation on reals (denoted as $ 0 $ in the real1 context).

lemma (in real1) real_zero_cl_bounded_map:

assumes $ f \in BoundedIntMaps $

shows $ [f] = 0 $ using assms, Real_ZF_1_L11A

Two real numbers are equal iff the slopes that represent them are almost equal. This is proven in Real_ZF_1_L13, here we just rewrite it in the notation used in the real1 context.

lemma (in real1) Real_ZF_1_1_L5:

assumes $ f \in \mathcal{S} $, $ g \in \mathcal{S} $

shows $ [f] = [g] \longleftrightarrow f \sim g $ using assms, Slopes_def, Real_ZF_1_L13

If the pair of function belongs to the slope equivalence relation, then their classes are equal. This is convenient, because we don't need to assume that $f,g$ are slopes (follows from the fact that $f\sim g$).

lemma (in real1) Real_ZF_1_1_L5A:

assumes $ f \sim g $

shows $ [f] = [g] $ using assms, Real_ZF_1_L11, Slopes_def, Real_ZF_1_1_L5

Identity function on integers is a slope. This is proven in Real_ZF_1_L13, here we just rewrite it in the notation used in the real1 context.

lemma (in real1) id_on_int_is_slope:

shows $ id(int) \in \mathcal{S} $ using Real_ZF_1_L14, Slopes_def

A result from Int_ZF_2.thy: the identity function on integers is not almost equal to any bounded function.

lemma (in real1) Real_ZF_1_1_L7:

assumes A1: $ f \in BoundedIntMaps $

shows $ \neg (id(int) \sim f) $ using assms, Slopes_def, SlopeOp1_def, BoundedIntMaps_def, SlopeEquivalenceRel_def, BoundedIntMaps_def, Int_ZF_2_3_L12

Zero is not one.

lemma (in real1) real_zero_not_one:

shows $ 1 \neq 0 $proof

{

assume A1: $ 1 = 0 $

have $ \exists f \in \mathcal{S} .\ 0 = [f] $ using Real_ZF_1_L4, Real_ZF_1_1_L3A

with A1 have $ \exists f \in \mathcal{S} .\ [id(int)] = [f] \wedge [f] = 0 $ using real_one_cl_identity

then have $ False $ using Real_ZF_1_1_L5, Slopes_def, Real_ZF_1_L10, Real_ZF_1_1_L7, id_on_int_is_slope

}

then show $ 1 \neq 0 $

qed

Negative of a real number is a real number. Property of groups.

lemma (in real1) Real_ZF_1_1_L8:

assumes $ a\in \mathbb{R} $

shows $ ( - a) \in \mathbb{R} $ using assms, Real_ZF_1_L2, inverse_in_group

An identity with three real numbers.

lemma (in real1) Real_ZF_1_1_L9:

assumes $ a\in \mathbb{R} $, $ b\in \mathbb{R} $, $ c\in \mathbb{R} $

shows $ a\cdot (b\cdot c) = a\cdot c\cdot b $ using assms, real_mult_commutative, Real_ZF_1_L3, Ring_ZF_2_L4

The order on reals

In this section we show that the order relation defined by prescribing the set of positive reals as the projection of the set of positive slopes makes the ring of real numbers into an ordered ring. We also collect the facts about ordered groups and rings that we use in the construction.

Positive slopes are slopes and positive reals are real.

lemma Real_ZF_1_2_L1:

shows $ PositiveSlopes \subseteq Slopes $, $ PositiveReals \subseteq RealNumbers $proof

have $ PositiveSlopes = $ $ \{s \in Slopes.\ s(PositiveIntegers) \cap PositiveIntegers \notin Fin(int)\} $ using PositiveSlopes_def

then show $ PositiveSlopes \subseteq Slopes $ by (rule subset_with_property )

then have $ \{SlopeEquivalenceRel\{s\}.\ s \in PositiveSlopes \} \subseteq $ $ Slopes//SlopeEquivalenceRel $ using EquivClass_1_L1A

then show $ PositiveReals \subseteq RealNumbers $ using PositiveReals_def, RealNumbers_def

qed

Positive reals are the same as classes of a positive slopes.

lemma (in real1) Real_ZF_1_2_L2:

shows $ a \in PositiveReals \longleftrightarrow (\exists f\in \mathcal{S} _+.\ a = [f]) $proof

assume $ a \in PositiveReals $

then have $ a \in \{([s]).\ s \in \mathcal{S} _+\} $ using PositiveReals_def

then show $ \exists f\in \mathcal{S} _+.\ a = [f] $

next

assume $ \exists f\in \mathcal{S} _+.\ a = [f] $

then have $ a \in \{([s]).\ s \in \mathcal{S} _+\} $

then show $ a \in PositiveReals $ using PositiveReals_def

qed

Let's recall from Int_ZF_2.thy that the sum and composition of positive slopes is a positive slope.

lemma (in real1) Real_ZF_1_2_L3:

assumes $ f\in \mathcal{S} _+ $, $ g\in \mathcal{S} _+ $

shows $ f + g \in \mathcal{S} _+ $, $ f\circ g \in \mathcal{S} _+ $ using assms, Slopes_def, PositiveSlopes_def, PositiveIntegers_def, SlopeOp1_def, sum_of_pos_sls_is_pos_sl, SlopeOp2_def, comp_of_pos_sls_is_pos_sl

Bounded integer maps are not positive slopes.

lemma (in real1) Real_ZF_1_2_L5:

assumes $ f \in BoundedIntMaps $

shows $ f \notin \mathcal{S} _+ $ using assms, BoundedIntMaps_def, Slopes_def, PositiveSlopes_def, PositiveIntegers_def, Int_ZF_2_3_L1B

The set of positive reals is closed under addition and multiplication. Zero (the neutral element of addition) is not a positive number.

lemma (in real1) Real_ZF_1_2_L6:

shows $ PositiveReals \text{ is closed under } RealAddition $, $ PositiveReals \text{ is closed under } RealMultiplication $, $ 0 \notin PositiveReals $proof

{

fix $ a $ $ fix $ $ b $

assume $ a \in PositiveReals $ and $ b \in PositiveReals $

then obtain $ f $ $ g $ where I: $ f \in \mathcal{S} _+ $, $ g \in \mathcal{S} _+ $ and II: $ a = [f] $, $ b = [g] $ using Real_ZF_1_2_L2

then have $ f \in \mathcal{S} $, $ g \in \mathcal{S} $ using Real_ZF_1_2_L1, Slopes_def

with I, II have $ a + b \in PositiveReals \wedge a\cdot b \in PositiveReals $ using Real_ZF_1_1_L4, Real_ZF_1_2_L3, Real_ZF_1_2_L2

}

then show $ PositiveReals \text{ is closed under } RealAddition $, $ PositiveReals \text{ is closed under } RealMultiplication $ using IsOpClosed_def

{

assume $ 0 \in PositiveReals $

then obtain $ f $ where $ f \in \mathcal{S} _+ $ and $ 0 = [f] $ using Real_ZF_1_2_L2

then have $ False $ using Real_ZF_1_2_L1, Slopes_def, Real_ZF_1_L10, Real_ZF_1_2_L5

}

then show $ 0 \notin PositiveReals $

qed

If a class of a slope $f$ is not zero, then either $f$ is a positive slope or $-f$ is a positive slope. The real proof is in Int_ZF_2.thy.

lemma (in real1) Real_ZF_1_2_L7:

assumes A1: $ f \in \mathcal{S} $ and A2: $ [f] \neq 0 $

shows $ (f \in \mathcal{S} _+) \text{ Xor } (( - f) \in \mathcal{S} _+) $ using assms, Slopes_def, SlopeEquivalenceRel_def, BoundedIntMaps_def, PositiveSlopes_def, PositiveIntegers_def, Real_ZF_1_L10, Int_ZF_2_3_L8

The next lemma rephrases Int_ZF_2_3_L10 in the notation used in real1 context.

lemma (in real1) Real_ZF_1_2_L8:

assumes A1: $ f \in \mathcal{S} $, $ g \in \mathcal{S} $ and A2: $ (f \in \mathcal{S} _+) \text{ Xor } (g \in \mathcal{S} _+) $

shows $ ([f] \in PositiveReals) \text{ Xor } ([g] \in PositiveReals) $ using assms, PositiveReals_def, SlopeEquivalenceRel_def, Slopes_def, SlopeOp1_def, BoundedIntMaps_def, PositiveSlopes_def, PositiveIntegers_def, Int_ZF_2_3_L10

The trichotomy law for the (potential) order on reals: if $a\neq 0$, then either $a$ is positive or $-a$ is potitive.

lemma (in real1) Real_ZF_1_2_L9:

assumes A1: $ a\in \mathbb{R} $ and A2: $ a\neq 0 $

shows $ (a \in PositiveReals) \text{ Xor } (( - a) \in PositiveReals) $proof

from A1 obtain $ f $ where I: $ f \in \mathcal{S} $, $ a = [f] $ using Real_ZF_1_1_L3A

with A2 have $ ([f] \in PositiveReals) \text{ Xor } ([ - f] \in PositiveReals) $ using Slopes_def, BoundedIntMaps_def, Int_ZF_2_1_L12, Real_ZF_1_2_L7, Real_ZF_1_2_L8

with I show $ (a \in PositiveReals) \text{ Xor } (( - a) \in PositiveReals) $ using Real_ZF_1_1_L4A

qed

Finally we are ready to prove that real numbers form an ordered ring with no zero divisors.

theorem reals_are_ord_ring:

shows $ \text{IsAnOrdRing}(RealNumbers,RealAddition,RealMultiplication,OrderOnReals) $, $ OrderOnReals \text{ is total on } RealNumbers $, $ \text{PositiveSet}(RealNumbers,RealAddition,OrderOnReals) = PositiveReals $, $ \text{HasNoZeroDivs}(RealNumbers,RealAddition,RealMultiplication) $proof

let $ R = RealNumbers $

let $ A = RealAddition $

let $ M = RealMultiplication $

let $ P = PositiveReals $

let $ r = OrderOnReals $

let $ z = \text{ TheNeutralElement}(R, A) $

have I: $ ring0(R, A, M) $, $ M \text{ is commutative on } R $, $ P \subseteq R $, $ P \text{ is closed under } A $, $ \text{ TheNeutralElement}(R, A) \notin P $, $ \forall a\in R.\ a \neq z \longrightarrow (a \in P) \text{ Xor } ( \text{GroupInv}(R, A)(a) \in P) $, $ P \text{ is closed under } M $, $ r = \text{OrderFromPosSet}(R, A, P) $ using Real_ZF_1_L3, real_mult_commutative, Real_ZF_1_2_L1, Real_ZF_1_2_L6, Real_ZF_1_2_L9, OrderOnReals_def

then show $ \text{IsAnOrdRing}(R, A, M, r) $ by (rule ring_ord_by_positive_set )

from I show $ r \text{ is total on } R $ by (rule ring_ord_by_positive_set )

from I show $ \text{PositiveSet}(R,A,r) = P $ by (rule ring_ord_by_positive_set )

from I show $ \text{HasNoZeroDivs}(R,A,M) $ by (rule ring_ord_by_positive_set )

qed

All theorems proven in the ring1 (about ordered rings), group3 (about ordered groups) and group1 (about groups) contexts are valid as applied to ordered real numbers with addition and (real) order.

lemma Real_ZF_1_2_L10:

shows $ ring1(RealNumbers,RealAddition,RealMultiplication,OrderOnReals) $, $ \text{IsAnOrdGroup}(RealNumbers,RealAddition,OrderOnReals) $, $ group3(RealNumbers,RealAddition,OrderOnReals) $, $ OrderOnReals \text{ is total on } RealNumbers $proof

show $ ring1(RealNumbers,RealAddition,RealMultiplication,OrderOnReals) $ using reals_are_ord_ring, OrdRing_ZF_1_L2

then show $ \text{IsAnOrdGroup}(RealNumbers,RealAddition,OrderOnReals) $, $ group3(RealNumbers,RealAddition,OrderOnReals) $, $ OrderOnReals \text{ is total on } RealNumbers $ using OrdRing_ZF_1_L4

qed

If $a=b$ or $b-a$ is positive, then $a$ is less or equal $b$.

lemma (in real1) Real_ZF_1_2_L11:

assumes A1: $ a\in \mathbb{R} $, $ b\in \mathbb{R} $ and A3: $ a=b \vee b - a \in PositiveReals $

shows $ a\leq b $ using assms, reals_are_ord_ring, Real_ZF_1_2_L10, OrderedGroup_ZF_1_L30

A sufficient condition for two classes to be in the real order.

lemma (in real1) Real_ZF_1_2_L12:

assumes A1: $ f \in \mathcal{S} $, $ g \in \mathcal{S} $ and A2: $ f\sim g \vee (g + ( - f)) \in \mathcal{S} _+ $

shows $ [f] \leq [g] $proof

from A1, A2 have $ [f] = [g] \vee [g] - [f] \in PositiveReals $ using Real_ZF_1_1_L5A, Real_ZF_1_2_L2, Real_ZF_1_1_L4B

with A1 show $ [f] \leq [g] $ using Real_ZF_1_1_L3, Real_ZF_1_2_L11

qed

Taking negative on both sides reverses the inequality, a case with an inverse on one side. Property of ordered groups.

lemma (in real1) Real_ZF_1_2_L13:

assumes A1: $ a\in \mathbb{R} $ and A2: $ ( - a) \leq b $

shows $ ( - b) \leq a $ using assms, Real_ZF_1_2_L10, OrderedGroup_ZF_1_L5AG

Real order is antisymmetric.

lemma (in real1) real_ord_antisym:

assumes A1: $ a\leq b $, $ b\leq a $

shows $ a=b $proof

from A1 have $ group3(RealNumbers,RealAddition,OrderOnReals) $, $ \langle a,b\rangle \in OrderOnReals $, $ \langle b,a\rangle \in OrderOnReals $ using Real_ZF_1_2_L10

then show $ a=b $ by (rule group_order_antisym )

qed

Real order is transitive.

lemma (in real1) real_ord_transitive:

assumes A1: $ a\leq b $, $ b\leq c $

shows $ a\leq c $proof

from A1 have $ group3(RealNumbers,RealAddition,OrderOnReals) $, $ \langle a,b\rangle \in OrderOnReals $, $ \langle b,c\rangle \in OrderOnReals $ using Real_ZF_1_2_L10

then have $ \langle a,c\rangle \in OrderOnReals $ by (rule Group_order_transitive )

then show $ a\leq c $

qed

We can multiply both sides of an inequality by a nonnegative real number.

lemma (in real1) Real_ZF_1_2_L14:

assumes $ a\leq b $ and $ 0 \leq c $

shows $ a\cdot c \leq b\cdot c $, $ c\cdot a \leq c\cdot b $ using assms, Real_ZF_1_2_L10, OrdRing_ZF_1_L9

A special case of Real_ZF_1_2_L14: we can multiply an inequality by a real number.

lemma (in real1) Real_ZF_1_2_L14A:

assumes A1: $ a\leq b $ and A2: $ c\in \mathbb{R} _+ $

shows $ c\cdot a \leq c\cdot b $ using assms, Real_ZF_1_2_L10, OrdRing_ZF_1_L9A

In the real1 context notation $a\leq b$ implies that $a$ and $b$ are real numbers.

lemma (in real1) Real_ZF_1_2_L15:

assumes $ a\leq b $

shows $ a\in \mathbb{R} $, $ b\in \mathbb{R} $ using assms, Real_ZF_1_2_L10, OrderedGroup_ZF_1_L4

$a\leq b$ implies that $0 \leq b -a$.

lemma (in real1) Real_ZF_1_2_L16:

assumes $ a\leq b $

shows $ 0 \leq b - a $ using assms, Real_ZF_1_2_L10, OrderedGroup_ZF_1_L12A

A sum of nonnegative elements is nonnegative.

lemma (in real1) Real_ZF_1_2_L17:

assumes $ 0 \leq a $, $ 0 \leq b $

shows $ 0 \leq a + b $ using assms, Real_ZF_1_2_L10, OrderedGroup_ZF_1_L12

We can add sides of two inequalities

lemma (in real1) Real_ZF_1_2_L18:

assumes $ a\leq b $, $ c\leq d $

shows $ a + c \leq b + d $ using assms, Real_ZF_1_2_L10, OrderedGroup_ZF_1_L5B

The order on real is reflexive.

lemma (in real1) real_ord_refl:

assumes $ a\in \mathbb{R} $

shows $ a\leq a $ using assms, Real_ZF_1_2_L10, OrderedGroup_ZF_1_L3

We can add a real number to both sides of an inequality.

lemma (in real1) add_num_to_ineq:

assumes $ a\leq b $ and $ c\in \mathbb{R} $

shows $ a + c \leq b + c $ using assms, Real_ZF_1_2_L10, IsAnOrdGroup_def

We can put a number on the other side of an inequality, changing its sign.

lemma (in real1) Real_ZF_1_2_L19:

assumes $ a\in \mathbb{R} $, $ b\in \mathbb{R} $ and $ c \leq a + b $

shows $ c - b \leq a $ using assms, Real_ZF_1_2_L10, OrderedGroup_ZF_1_L9C

What happens when one real number is not greater or equal than another?

lemma (in real1) Real_ZF_1_2_L20:

assumes $ a\in \mathbb{R} $, $ b\in \mathbb{R} $ and $ \neg (a\leq b) $

shows $ b \lt a $proof

from assms have I: $ group3(\mathbb{R} ,RealAddition,OrderOnReals) $, $ OrderOnReals \text{ is total on } \mathbb{R} $, $ a\in \mathbb{R} $, $ b\in \mathbb{R} $, $ \neg (\langle a,b\rangle \in OrderOnReals) $ using Real_ZF_1_2_L10

then have $ \langle b,a\rangle \in OrderOnReals $ by (rule OrderedGroup_ZF_1_L8 )

then have $ b \leq a $

moreover

from I have $ a\neq b $ by (rule OrderedGroup_ZF_1_L8 )

ultimately show $ b \lt a $

qed

We can put a number on the other side of an inequality, changing its sign, version with a minus.

lemma (in real1) Real_ZF_1_2_L21:

assumes $ a\in \mathbb{R} $, $ b\in \mathbb{R} $ and $ c \leq a - b $

shows $ c + b \leq a $ using assms, Real_ZF_1_2_L10, OrderedGroup_ZF_1_L5J

The order on reals is a relation on reals.

lemma (in real1) Real_ZF_1_2_L22:

shows $ OrderOnReals \subseteq \mathbb{R} \times \mathbb{R} $ using Real_ZF_1_2_L10, IsAnOrdGroup_def

A set that is bounded above in the sense defined by order on reals is a subset of real numbers.

lemma (in real1) Real_ZF_1_2_L23:

assumes A1: $ \text{IsBoundedAbove}(A,OrderOnReals) $

shows $ A \subseteq \mathbb{R} $ using A1, Real_ZF_1_2_L22, Order_ZF_3_L1A

Properties of the maximum of three real numbers.

lemma (in real1) Real_ZF_1_2_L24:

assumes A1: $ a\in \mathbb{R} $, $ b\in \mathbb{R} $, $ c\in \mathbb{R} $

shows $ \text{Maximum}(OrderOnReals,\{a,b,c\}) \in \{a,b,c\} $, $ \text{Maximum}(OrderOnReals,\{a,b,c\}) \in \mathbb{R} $, $ a \leq \text{Maximum}(OrderOnReals,\{a,b,c\}) $, $ b \leq \text{Maximum}(OrderOnReals,\{a,b,c\}) $, $ c \leq \text{Maximum}(OrderOnReals,\{a,b,c\}) $proof

have $ \text{IsLinOrder}(\mathbb{R} ,OrderOnReals) $ using Real_ZF_1_2_L10, group_ord_total_is_lin

with A1 show $ \text{Maximum}(OrderOnReals,\{a,b,c\}) \in \{a,b,c\} $, $ \text{Maximum}(OrderOnReals,\{a,b,c\}) \in \mathbb{R} $, $ a \leq \text{Maximum}(OrderOnReals,\{a,b,c\}) $, $ b \leq \text{Maximum}(OrderOnReals,\{a,b,c\}) $, $ c \leq \text{Maximum}(OrderOnReals,\{a,b,c\}) $ using Finite_ZF_1_L2A

qed

A form of transitivity for the order on reals.

lemma (in real1) real_strict_ord_transit:

assumes A1: $ a\leq b $ and A2: $ b \lt c $

shows $ a \lt c $proof

from A1, A2 have I: $ group3(\mathbb{R} ,RealAddition,OrderOnReals) $, $ \langle a,b\rangle \in OrderOnReals $, $ \langle b,c\rangle \in OrderOnReals \wedge b\neq c $ using Real_ZF_1_2_L10

then have $ \langle a,c\rangle \in OrderOnReals \wedge a\neq c $ by (rule group_strict_ord_transit )

then show $ a \lt c $

qed

We can multiply a right hand side of an inequality between positive real numbers by a number that is greater than one.

lemma (in real1) Real_ZF_1_2_L25:

assumes $ b \in \mathbb{R} _+ $ and $ a\leq b $ and $ 1 \lt c $

shows $ a \lt b\cdot c $ using assms, reals_are_ord_ring, Real_ZF_1_2_L10, OrdRing_ZF_3_L17

We can move a real number to the other side of a strict inequality, changing its sign.

lemma (in real1) Real_ZF_1_2_L26:

assumes $ a\in \mathbb{R} $, $ b\in \mathbb{R} $ and $ a - b \lt c $

shows $ a \lt c + b $ using assms, Real_ZF_1_2_L10, OrderedGroup_ZF_1_L12B

Real order is translation invariant.

lemma (in real1) real_ord_transl_inv:

assumes $ a\leq b $ and $ c\in \mathbb{R} $

shows $ c + a \leq c + b $ using assms, Real_ZF_1_2_L10, IsAnOrdGroup_def

It is convenient to have the transitivity of the order on integers in the notation specific to real1 context. This may be confusing for the presentation readers: even though $ \leq $ and $ \leq $ are printed in the same way, they are different symbols in the source. In the real1 context the former denotes inequality between integers, and the latter denotes inequality between real numbers (classes of slopes). The next lemma is about transitivity of the order relation on integers.

lemma (in real1) int_order_transitive:

assumes A1: $ a\leq b $, $ b\leq c $

shows $ a\leq c $proof

from A1 have $ \langle a,b\rangle \in IntegerOrder $ and $ \langle b,c\rangle \in IntegerOrder $

then have $ \langle a,c\rangle \in IntegerOrder $ by (rule Int_ZF_2_L5 )

then show $ a\leq c $

qed

A property of nonempty subsets of real numbers that don't have a maximum: for any element we can find one that is (strictly) greater.

lemma (in real1) Real_ZF_1_2_L27:

assumes $ A\subseteq \mathbb{R} $ and $ \neg \text{HasAmaximum}(OrderOnReals,A) $ and $ x\in A $

shows $ \exists y\in A.\ x \lt y $ using assms, Real_ZF_1_2_L10, OrderedGroup_ZF_2_L2B

The next lemma shows what happens when one real number is not greater or equal than another.

lemma (in real1) Real_ZF_1_2_L28:

assumes $ a\in \mathbb{R} $, $ b\in \mathbb{R} $ and $ \neg (a\leq b) $

shows $ b \lt a $proof

from assms have $ group3(\mathbb{R} ,RealAddition,OrderOnReals) $, $ OrderOnReals \text{ is total on } \mathbb{R} $, $ a\in \mathbb{R} $, $ b\in \mathbb{R} $, $ \langle a,b\rangle \notin OrderOnReals $ using Real_ZF_1_2_L10

then have $ \langle b,a\rangle \in OrderOnReals \wedge b\neq a $ by (rule OrderedGroup_ZF_1_L8 )

then show $ b \lt a $

qed

If a real number is less than another, then the second one can not be less or equal that the first.

lemma (in real1) Real_ZF_1_2_L29:

assumes $ a \lt b $

shows $ \neg (b\leq a) $proof

from assms have $ group3(\mathbb{R} ,RealAddition,OrderOnReals) $, $ \langle a,b\rangle \in OrderOnReals $, $ a\neq b $ using Real_ZF_1_2_L10

then have $ \langle b,a\rangle \notin OrderOnReals $ by (rule OrderedGroup_ZF_1_L8AA )

then show $ \neg (b\leq a) $

qed

Inverting reals

In this section we tackle the issue of existence of (multiplicative) inverses of real numbers and show that real numbers form an ordered field. We also restate here some facts specific to ordered fields that we need for the construction. The actual proofs of most of these facts can be found in Field_ZF.thy and OrderedField_ZF.thy

We rewrite the theorem from Int_ZF_2.thy that shows that for every positive slope we can find one that is almost equal and has an inverse.

lemma (in real1) pos_slopes_have_inv:

assumes $ f \in \mathcal{S} _+ $

shows $ \exists g\in \mathcal{S} .\ f\sim g \wedge (\exists h\in \mathcal{S} .\ g\circ h \sim id(int)) $ using assms, PositiveSlopes_def, Slopes_def, PositiveIntegers_def, pos_slope_has_inv, SlopeOp1_def, SlopeOp2_def, BoundedIntMaps_def, SlopeEquivalenceRel_def

The set of real numbers we are constructing is an ordered field.

theorem (in real1) reals_are_ord_field:

shows $ \text{IsAnOrdField}(RealNumbers,RealAddition,RealMultiplication,OrderOnReals) $proof

let $ R = RealNumbers $

let $ A = RealAddition $

let $ M = RealMultiplication $

let $ r = OrderOnReals $

have $ ring1(R,A,M,r) $ and $ 0 \neq 1 $ using reals_are_ord_ring, OrdRing_ZF_1_L2, real_zero_not_one

moreover

have $ M \text{ is commutative on } R $ using real_mult_commutative

moreover

have $ \forall a\in \text{PositiveSet}(R,A,r).\ \exists b\in R.\ a\cdot b = 1 $proof

fix $ a $

assume $ a \in \text{PositiveSet}(R,A,r) $

then obtain $ f $ where I: $ f\in \mathcal{S} _+ $ and II: $ a = [f] $ using reals_are_ord_ring, Real_ZF_1_2_L2

then have $ \exists g\in \mathcal{S} .\ f\sim g \wedge (\exists h\in \mathcal{S} .\ g\circ h \sim id(int)) $ using pos_slopes_have_inv

then obtain $ g $ where III: $ g\in \mathcal{S} $ and IV: $ f\sim g $ and V: $ \exists h\in \mathcal{S} .\ g\circ h \sim id(int) $

from V obtain $ h $ where VII: $ h\in \mathcal{S} $ and VIII: $ g\circ h \sim id(int) $

from I, III, IV have $ [f] = [g] $ using Real_ZF_1_2_L1, Slopes_def, Real_ZF_1_1_L5

with II, III, VII, VIII have $ a\cdot [h] = 1 $ using Real_ZF_1_1_L4, Real_ZF_1_1_L5A, real_one_cl_identity

with VII show $ \exists b\in R.\ a\cdot b = 1 $ using Real_ZF_1_1_L3

qed

ultimately show $ thesis $ using OrdField_ZF_1_L4

qed

Reals form a field.

lemma reals_are_field:

shows $ \text{IsAfield}(RealNumbers,RealAddition,RealMultiplication) $ using reals_are_ord_field, OrdField_ZF_1_L1A

Theorem proven in field0 and field1 contexts are valid as applied to real numbers.

lemma field_cntxts_ok:

shows $ field0(RealNumbers,RealAddition,RealMultiplication) $, $ field1(RealNumbers,RealAddition,RealMultiplication,OrderOnReals) $ using reals_are_field, reals_are_ord_field, field_field0, OrdField_ZF_1_L2

If $a$ is positive, then $a^{-1}$ is also positive.

lemma (in real1) Real_ZF_1_3_L1:

assumes $ a \in \mathbb{R} _+ $

shows $ a^{-1} \in \mathbb{R} _+ $, $ a^{-1} \in \mathbb{R} $ using assms, field_cntxts_ok, OrdField_ZF_1_L8, PositiveSet_def

A technical fact about multiplying strict inequality by the inverse of one of the sides.

lemma (in real1) Real_ZF_1_3_L2:

assumes $ a \in \mathbb{R} _+ $ and $ a^{-1} \lt b $

shows $ 1 \lt b\cdot a $ using assms, field_cntxts_ok, OrdField_ZF_2_L2

If $a$ is smaller than $b$, then $(b-a)^{-1}$ is positive.

lemma (in real1) Real_ZF_1_3_L3:

assumes $ a \lt b $

shows $ (b - a)^{-1} \in \mathbb{R} _+ $ using assms, field_cntxts_ok, OrdField_ZF_1_L9

We can put a positive factor on the other side of a strict inequality, changing it to its inverse.

lemma (in real1) Real_ZF_1_3_L4:

assumes A1: $ a\in \mathbb{R} $, $ b\in \mathbb{R} _+ $ and A2: $ a\cdot b \lt c $

shows $ a \lt c\cdot b^{-1} $ using assms, field_cntxts_ok, OrdField_ZF_2_L6

We can put a positive factor on the other side of a strict inequality, changing it to its inverse, version with the product initially on the right hand side.

lemma (in real1) Real_ZF_1_3_L4A:

assumes A1: $ b\in \mathbb{R} $, $ c\in \mathbb{R} _+ $ and A2: $ a \lt b\cdot c $

shows $ a\cdot c^{-1} \lt b $ using assms, field_cntxts_ok, OrdField_ZF_2_L6A

We can put a positive factor on the other side of an inequality, changing it to its inverse, version with the product initially on the right hand side.

lemma (in real1) Real_ZF_1_3_L4B:

assumes A1: $ b\in \mathbb{R} $, $ c\in \mathbb{R} _+ $ and A2: $ a \leq b\cdot c $

shows $ a\cdot c^{-1} \leq b $ using assms, field_cntxts_ok, OrdField_ZF_2_L5A

We can put a positive factor on the other side of an inequality, changing it to its inverse, version with the product initially on the left hand side.

lemma (in real1) Real_ZF_1_3_L4C:

assumes A1: $ a\in \mathbb{R} $, $ b\in \mathbb{R} _+ $ and A2: $ a\cdot b \leq c $

shows $ a \leq c\cdot b^{-1} $ using assms, field_cntxts_ok, OrdField_ZF_2_L5

A technical lemma about solving a strict inequality with three real numbers and inverse of a difference.

lemma (in real1) Real_ZF_1_3_L5:

assumes $ a \lt b $ and $ (b - a)^{-1} \lt c $

shows $ 1 + a\cdot c \lt b\cdot c $ using assms, field_cntxts_ok, OrdField_ZF_2_L9

We can multiply an inequality by the inverse of a positive number.

lemma (in real1) Real_ZF_1_3_L6:

assumes $ a\leq b $ and $ c\in \mathbb{R} _+ $

shows $ a\cdot c^{-1} \leq b\cdot c^{-1} $ using assms, field_cntxts_ok, OrdField_ZF_2_L3

We can multiply a strict inequality by a positive number or its inverse.

lemma (in real1) Real_ZF_1_3_L7:

assumes $ a \lt b $ and $ c\in \mathbb{R} _+ $

shows $ a\cdot c \lt b\cdot c $, $ c\cdot a \lt c\cdot b $, $ a\cdot c^{-1} \lt b\cdot c^{-1} $ using assms, field_cntxts_ok, OrdField_ZF_2_L4

An identity with three real numbers, inverse and cancelling.

lemma (in real1) Real_ZF_1_3_L8:

assumes $ a\in \mathbb{R} $, $ b\in \mathbb{R} $, $ b\neq 0 $, $ c\in \mathbb{R} $

shows $ a\cdot b\cdot (c\cdot b^{-1}) = a\cdot c $ using assms, field_cntxts_ok, Field_ZF_2_L6

Completeness

This goal of this section is to show that the order on real numbers is complete, that is every subset of reals that is bounded above has a smallest upper bound.

If $m$ is an integer, then $ m^R $ is a real number. Recall that in real1 context $ m^R $ denotes the class of the slope $n\mapsto m\cdot n$.

lemma (in real1) real_int_is_real:

assumes $ m \in int $

shows $ m^R \in \mathbb{R} $ using assms, Int_ZF_2_5_L1, Real_ZF_1_1_L3

The negative of the real embedding of an integer is the embedding of the negative of the integer.

lemma (in real1) Real_ZF_1_4_L1:

assumes $ m \in int $

shows $ ( - m)^R = - (m^R) $ using assms, Int_ZF_2_5_L3, Int_ZF_2_5_L1, Real_ZF_1_1_L4A

The embedding of sum of integers is the sum of embeddings.

lemma (in real1) Real_ZF_1_4_L1A:

assumes $ m \in int $, $ k \in int $

shows $ m^R + k^R = ((m + k)^R) $ using assms, Int_ZF_2_5_L1, SlopeOp1_def, Int_ZF_2_5_L3A, Real_ZF_1_1_L4

The embedding of a difference of integers is the difference of embeddings.

lemma (in real1) Real_ZF_1_4_L1B:

assumes A1: $ m \in int $, $ k \in int $

shows $ m^R - k^R = (m - k)^R $proof

from A1 have $ ( - k) \in int $ using Int_ZF_1_1_L4

with A1 have $ (m - k)^R = m^R + ( - k)^R $ using Real_ZF_1_4_L1A

with A1 show $ m^R - k^R = (m - k)^R $ using Real_ZF_1_4_L1

qed

The embedding of the product of integers is the product of embeddings.

lemma (in real1) Real_ZF_1_4_L1C:

assumes $ m \in int $, $ k \in int $

shows $ m^R \cdot k^R = (m\cdot k)^R $ using assms, Int_ZF_2_5_L1, SlopeOp2_def, Int_ZF_2_5_L3B, Real_ZF_1_1_L4

For any real numbers there is an integer whose real version is greater or equal.

lemma (in real1) Real_ZF_1_4_L2:

assumes A1: $ a\in \mathbb{R} $

shows $ \exists m\in int.\ a \leq m^R $proof

from A1 obtain $ f $ where I: $ f\in \mathcal{S} $ and II: $ a = [f] $ using Real_ZF_1_1_L3A

then have $ \exists m\in int.\ \exists g\in \mathcal{S} .\ $ $ \{\langle n,m\cdot n\rangle .\ n \in int\} \sim g \wedge (f\sim g \vee (g + ( - f)) \in \mathcal{S} _+) $ using Int_ZF_2_5_L2, Slopes_def, SlopeOp1_def, BoundedIntMaps_def, SlopeEquivalenceRel_def, PositiveIntegers_def, PositiveSlopes_def

then obtain $ m $ $ g $ where III: $ m\in int $ and IV: $ g\in \mathcal{S} $ and $ \{\langle n,m\cdot n\rangle .\ n \in int\} \sim g \wedge (f\sim g \vee (g + ( - f)) \in \mathcal{S} _+) $

then have $ m^R = [g] $ and $ f \sim g \vee (g + ( - f)) \in \mathcal{S} _+ $ using Real_ZF_1_1_L5A

with I, II, IV have $ a \leq m^R $ using Real_ZF_1_2_L12

with III show $ \exists m\in int.\ a \leq m^R $

qed

For any real numbers there is an integer whose real version (embedding) is less or equal.

lemma (in real1) Real_ZF_1_4_L3:

assumes A1: $ a\in \mathbb{R} $

shows $ \{m \in int.\ m^R \leq a\} \neq 0 $proof

from A1 have $ ( - a) \in \mathbb{R} $ using Real_ZF_1_1_L8

then obtain $ m $ where I: $ m\in int $ and II: $ ( - a) \leq m^R $ using Real_ZF_1_4_L2

let $ k = \text{GroupInv}(int,IntegerAddition)(m) $

from A1, I, II have $ k \in int $ and $ k^R \leq a $ using Real_ZF_1_2_L13, Real_ZF_1_4_L1, Int_ZF_1_1_L4

then show $ thesis $

qed

Embeddings of two integers are equal only if the integers are equal.

lemma (in real1) Real_ZF_1_4_L4:

assumes A1: $ m \in int $, $ k \in int $ and A2: $ m^R = k^R $

shows $ m=k $proof

let $ r = \{\langle n, IntegerMultiplication \langle m, n\rangle \rangle .\ n \in int\} $

let $ s = \{\langle n, IntegerMultiplication \langle k, n\rangle \rangle .\ n \in int\} $

from A1, A2 have $ r \sim s $ using Int_ZF_2_5_L1, AlmostHoms_def, Real_ZF_1_1_L5

with A1 have $ m \in int $, $ k \in int $, $ \langle r,s\rangle \in \text{QuotientGroupRel}( \text{AlmostHoms}(int, IntegerAddition),$ $ \text{AlHomOp1}(int, IntegerAddition), \text{FinRangeFunctions}(int, int)) $ using SlopeEquivalenceRel_def, Slopes_def, SlopeOp1_def, BoundedIntMaps_def

then show $ m=k $ by (rule Int_ZF_2_5_L6 )

qed

The embedding of integers preserves the order.

lemma (in real1) Real_ZF_1_4_L5:

assumes A1: $ m\leq k $

shows $ m^R \leq k^R $proof

let $ r = \{\langle n, m\cdot n\rangle .\ n \in int\} $

let $ s = \{\langle n, k\cdot n\rangle .\ n \in int\} $

from A1 have $ r \in \mathcal{S} $, $ s \in \mathcal{S} $ using Int_ZF_2_L1A, Int_ZF_2_5_L1

moreover

from A1 have $ r \sim s \vee s + ( - r) \in \mathcal{S} _+ $ using Slopes_def, SlopeOp1_def, BoundedIntMaps_def, SlopeEquivalenceRel_def, PositiveIntegers_def, PositiveSlopes_def, Int_ZF_2_5_L4

ultimately show $ m^R \leq k^R $ using Real_ZF_1_2_L12

qed

The embedding of integers preserves the strict order.

lemma (in real1) Real_ZF_1_4_L5A:

assumes A1: $ m\leq k $, $ m\neq k $

shows $ m^R \lt k^R $proof

from A1 have $ m^R \leq k^R $ using Real_ZF_1_4_L5

moreover

from A1 have T: $ m \in int $, $ k \in int $ using Int_ZF_2_L1A

with A1 have $ m^R \neq k^R $ using Real_ZF_1_4_L4

ultimately show $ m^R \lt k^R $

qed

For any real number there is a positive integer whose real version is (strictly) greater. This is Lemma 14 i) in \cite{Arthan2004}.

lemma (in real1) Arthan_Lemma14i:

assumes A1: $ a\in \mathbb{R} $

shows $ \exists n\in \mathbb{Z} _+.\ a \lt n^R $proof

from A1 obtain $ m $ where I: $ m\in int $ and II: $ a \leq m^R $ using Real_ZF_1_4_L2

let $ n = \text{GreaterOf}(IntegerOrder,1 _Z,m) + 1 _Z $

from I have T: $ n \in \mathbb{Z} _+ $ and $ m \leq n $, $ m\neq n $ using Int_ZF_1_5_L7B

then have III: $ m^R \lt n^R $ using Real_ZF_1_4_L5A

with II have $ a \lt n^R $ by (rule real_strict_ord_transit )

with T show $ thesis $

qed

If one embedding is less or equal than another, then the integers are also less or equal.

lemma (in real1) Real_ZF_1_4_L6:

assumes A1: $ k \in int $, $ m \in int $ and A2: $ m^R \leq k^R $

shows $ m\leq k $proof

{

assume A3: $ \langle m,k\rangle \notin IntegerOrder $

with A1 have $ \langle k,m\rangle \in IntegerOrder $ by (rule Int_ZF_2_L19 )

then have $ k^R \leq m^R $ using Real_ZF_1_4_L5

with A2 have $ m^R = k^R $ by (rule real_ord_antisym )

with A1 have $ k = m $ using Real_ZF_1_4_L4

moreover

from A1, A3 have $ k\neq m $ by (rule Int_ZF_2_L19 )

ultimately have $ False $

}

then show $ m\leq k $

qed

The floor function is well defined and has expected properties.

lemma (in real1) Real_ZF_1_4_L7:

assumes A1: $ a\in \mathbb{R} $

shows $ \text{IsBoundedAbove}(\{m \in int.\ m^R \leq a\},IntegerOrder) $, $ \{m \in int.\ m^R \leq a\} \neq 0 $, $ \lfloor a\rfloor \in int $, $ \lfloor a\rfloor ^R \leq a $proof

let $ A = \{m \in int.\ m^R \leq a\} $

from A1 obtain $ K $ where I: $ K\in int $ and II: $ a \leq (K^R) $ using Real_ZF_1_4_L2

{

fix $ n $

assume $ n \in A $

then have III: $ n \in int $ and IV: $ n^R \leq a $

from IV, II have $ (n^R) \leq (K^R) $ by (rule real_ord_transitive )

with I, III have $ n\leq K $ using Real_ZF_1_4_L6

}

then have $ \forall n\in A.\ \langle n,K\rangle \in IntegerOrder $

then show $ \text{IsBoundedAbove}(A,IntegerOrder) $ by (rule Order_ZF_3_L10 )

moreover

from A1 show $ A \neq 0 $ using Real_ZF_1_4_L3

ultimately have $ \text{Maximum}(IntegerOrder,A) \in A $ by (rule int_bounded_above_has_max )

then show $ \lfloor a\rfloor \in int $, $ \lfloor a\rfloor ^R \leq a $

qed

Every integer whose embedding is less or equal a real number $a$ is less or equal than the floor of $a$.

lemma (in real1) Real_ZF_1_4_L8:

assumes A1: $ m \in int $ and A2: $ m^R \leq a $

shows $ m \leq \lfloor a\rfloor $proof

let $ A = \{m \in int.\ m^R \leq a\} $

from A2 have $ \text{IsBoundedAbove}(A,IntegerOrder) $ and $ A\neq 0 $ using Real_ZF_1_2_L15, Real_ZF_1_4_L7

then have $ \forall x\in A.\ \langle x, \text{Maximum}(IntegerOrder,A)\rangle \in IntegerOrder $ by (rule int_bounded_above_has_max )

with A1, A2 show $ m \leq \lfloor a\rfloor $

qed

Integer zero and one embed as real zero and one.

lemma (in real1) int_0_1_are_real_zero_one:

shows $ 0 _Z^R = 0 $, $ 1 _Z^R = 1 $ using Int_ZF_2_5_L7, BoundedIntMaps_def, real_one_cl_identity, real_zero_cl_bounded_map

Integer two embeds as the real two.

lemma (in real1) int_two_is_real_two:

shows $ 2 _Z^R = 2 $proof

have $ 2 _Z^R = 1 _Z^R + 1 _Z^R $ using int_zero_one_are_int, Real_ZF_1_4_L1A

also

have $ \ldots = 2 $ using int_0_1_are_real_zero_one

finally show $ 2 _Z^R = 2 $

qed

A positive integer embeds as a positive (hence nonnegative) real.

lemma (in real1) int_pos_is_real_pos:

assumes A1: $ p\in \mathbb{Z} _+ $

shows $ p^R \in \mathbb{R} $, $ 0 \leq p^R $, $ p^R \in \mathbb{R} _+ $proof

from A1 have I: $ p \in int $, $ 0 _Z \leq p $, $ 0 _Z \neq p $ using PositiveSet_def

then have $ p^R \in \mathbb{R} $, $ 0 _Z^R \leq p^R $ using real_int_is_real, Real_ZF_1_4_L5

then show $ p^R \in \mathbb{R} $, $ 0 \leq p^R $ using int_0_1_are_real_zero_one

moreover

have $ 0 \neq p^R $proof

{

assume $ 0 = p^R $

with I have $ False $ using int_0_1_are_real_zero_one, int_zero_one_are_int, Real_ZF_1_4_L4

}

then show $ 0 \neq p^R $

qed

ultimately show $ p^R \in \mathbb{R} _+ $ using PositiveSet_def

qed

The ordered field of reals we are constructing is archimedean, i.e., if $x,y$ are its elements with $y$ positive, then there is a positive integer $M$ such that $x$ is smaller than $M^R y$. This is Lemma 14 ii) in \cite{Arthan2004}.

lemma (in real1) Arthan_Lemma14ii:

assumes A1: $ x\in \mathbb{R} $, $ y \in \mathbb{R} _+ $

shows $ \exists M\in \mathbb{Z} _+.\ x \lt M^R\cdot y $proof

from A1 have $ \exists C\in \mathbb{Z} _+.\ x \lt C^R $ and $ \exists D\in \mathbb{Z} _+.\ y^{-1} \lt D^R $ using Real_ZF_1_3_L1, Arthan_Lemma14i

then obtain $ C $ $ D $ where I: $ C\in \mathbb{Z} _+ $ and II: $ x \lt C^R $ and III: $ D\in \mathbb{Z} _+ $ and IV: $ y^{-1} \lt D^R $

let $ M = C\cdot D $

from I, III have T: $ M \in \mathbb{Z} _+ $, $ C^R \in \mathbb{R} $, $ D^R \in \mathbb{R} $ using pos_int_closed_mul_unfold, PositiveSet_def, real_int_is_real

with A1, I, III have $ C^R\cdot (D^R\cdot y) = M^R\cdot y $ using PositiveSet_def, Real_ZF_1_L6A, Real_ZF_1_4_L1C

moreover

from A1, I, II, IV have $ x \lt C^R\cdot (D^R\cdot y) $ using int_pos_is_real_pos, Real_ZF_1_3_L2, Real_ZF_1_2_L25

ultimately have $ x \lt M^R\cdot y $

with T show $ thesis $

qed

Taking the floor function preserves the order.

lemma (in real1) Real_ZF_1_4_L9:

assumes A1: $ a\leq b $

shows $ \lfloor a\rfloor \leq \lfloor b\rfloor $proof

from A1 have T: $ a\in \mathbb{R} $ using Real_ZF_1_2_L15

with A1 have $ \lfloor a\rfloor ^R \leq a $ and $ a\leq b $ using Real_ZF_1_4_L7

then have $ \lfloor a\rfloor ^R \leq b $ by (rule real_ord_transitive )

moreover

from T have $ \lfloor a\rfloor \in int $ using Real_ZF_1_4_L7

ultimately show $ \lfloor a\rfloor \leq \lfloor b\rfloor $ using Real_ZF_1_4_L8

qed

If $S$ is bounded above and $p$ is a positive intereger, then $\Gamma(S,p)$ is well defined.

lemma (in real1) Real_ZF_1_4_L10:

assumes A1: $ \text{IsBoundedAbove}(S,OrderOnReals) $, $ S\neq 0 $ and A2: $ p\in \mathbb{Z} _+ $

shows $ \text{IsBoundedAbove}(\{\lfloor p^R\cdot x\rfloor .\ x\in S\},IntegerOrder) $, $ \Gamma (S,p) \in \{\lfloor p^R\cdot x\rfloor .\ x\in S\} $, $ \Gamma (S,p) \in int $proof

let $ A = \{\lfloor p^R\cdot x\rfloor .\ x\in S\} $

from A1 obtain $ X $ where I: $ \forall x\in S.\ x\leq X $ using IsBoundedAbove_def

{

fix $ m $

assume $ m \in A $

then obtain $ x $ where $ x\in S $ and II: $ m = \lfloor p^R\cdot x\rfloor $

with I have $ x\leq X $

moreover

from A2 have $ 0 \leq p^R $ using int_pos_is_real_pos

ultimately have $ p^R\cdot x \leq p^R\cdot X $ using Real_ZF_1_2_L14

with II have $ m \leq \lfloor p^R\cdot X\rfloor $ using Real_ZF_1_4_L9

}

then have $ \forall m\in A.\ \langle m,\lfloor p^R\cdot X\rfloor \rangle \in IntegerOrder $

then show II: $ \text{IsBoundedAbove}(A,IntegerOrder) $ by (rule Order_ZF_3_L10 )

moreover

from A1 have III: $ A \neq 0 $

ultimately have $ \text{Maximum}(IntegerOrder,A) \in A $ by (rule int_bounded_above_has_max )

moreover

from II, III have $ \text{Maximum}(IntegerOrder,A) \in int $ by (rule int_bounded_above_has_max )

ultimately show $ \Gamma (S,p) \in \{\lfloor p^R\cdot x\rfloor .\ x\in S\} $ and $ \Gamma (S,p) \in int $

qed

If $p$ is a positive integer, then for all $s\in S$ the floor of $p\cdot x$ is not greater that $\Gamma(S,p)$.

lemma (in real1) Real_ZF_1_4_L11:

assumes A1: $ \text{IsBoundedAbove}(S,OrderOnReals) $ and A2: $ x\in S $ and A3: $ p\in \mathbb{Z} _+ $

shows $ \lfloor p^R\cdot x\rfloor \leq \Gamma (S,p) $proof

let $ A = \{\lfloor p^R\cdot x\rfloor .\ x\in S\} $

from A2 have $ S\neq 0 $

with A1, A3 have $ \text{IsBoundedAbove}(A,IntegerOrder) $, $ A \neq 0 $ using Real_ZF_1_4_L10

then have $ \forall x\in A.\ \langle x, \text{Maximum}(IntegerOrder,A)\rangle \in IntegerOrder $ by (rule int_bounded_above_has_max )

with A2 show $ \lfloor p^R\cdot x\rfloor \leq \Gamma (S,p) $

qed

The candidate for supremum is an integer mapping with values given by $\Gamma$.

lemma (in real1) Real_ZF_1_4_L12:

assumes A1: $ \text{IsBoundedAbove}(S,OrderOnReals) $, $ S\neq 0 $ and A2: $ g = \{\langle p,\Gamma (S,p)\rangle .\ p\in \mathbb{Z} _+\} $

shows $ g : \mathbb{Z} _+\rightarrow int $, $ \forall n\in \mathbb{Z} _+.\ g(n) = \Gamma (S,n) $proof

from A1 have $ \forall n\in \mathbb{Z} _+.\ \Gamma (S,n) \in int $ using Real_ZF_1_4_L10

with A2 show I: $ g : \mathbb{Z} _+\rightarrow int $ using ZF_fun_from_total

{

fix $ n $

assume $ n\in \mathbb{Z} _+ $

with A2, I have $ g(n) = \Gamma (S,n) $ using ZF_fun_from_tot_val

}

then show $ \forall n\in \mathbb{Z} _+.\ g(n) = \Gamma (S,n) $

qed

Every integer is equal to the floor of its embedding.

lemma (in real1) Real_ZF_1_4_L14:

assumes A1: $ m \in int $

shows $ \lfloor m^R\rfloor = m $proof

let $ A = \{n \in int.\ n^R \leq m^R \} $

have $ \text{antisym}(IntegerOrder) $ using Int_ZF_2_L4

moreover

from A1 have $ m \in A $ using real_int_is_real, real_ord_refl

moreover

from A1 have $ \forall n \in A.\ \langle n,m\rangle \in IntegerOrder $ using Real_ZF_1_4_L6

ultimately show $ \lfloor m^R\rfloor = m $ using Order_ZF_4_L14

qed

Floor of (real) zero is (integer) zero.

lemma (in real1) floor_01_is_zero_one:

shows $ \lfloor 0 \rfloor = 0 _Z $, $ \lfloor 1 \rfloor = 1 _Z $proof

have $ \lfloor ( 0 _Z)^R\rfloor = 0 _Z $ and $ \lfloor (1 _Z)^R\rfloor = 1 _Z $ using int_zero_one_are_int, Real_ZF_1_4_L14

then show $ \lfloor 0 \rfloor = 0 _Z $ and $ \lfloor 1 \rfloor = 1 _Z $ using int_0_1_are_real_zero_one

qed

Floor of (real) two is (integer) two.

lemma (in real1) floor_2_is_two:

shows $ \lfloor 2 \rfloor = 2 _Z $proof

have $ \lfloor ( 2 _Z)^R\rfloor = 2 _Z $ using int_two_three_are_int, Real_ZF_1_4_L14

then show $ \lfloor 2 \rfloor = 2 _Z $ using int_two_is_real_two

qed

Floor of a product of embeddings of integers is equal to the product of integers.

lemma (in real1) Real_ZF_1_4_L14A:

assumes A1: $ m \in int $, $ k \in int $

shows $ \lfloor m^R\cdot k^R\rfloor = m\cdot k $proof

from A1 have T: $ m\cdot k \in int $ using Int_ZF_1_1_L5

from A1 have $ \lfloor m^R\cdot k^R\rfloor = \lfloor (m\cdot k)^R\rfloor $ using Real_ZF_1_4_L1C

with T show $ \lfloor m^R\cdot k^R\rfloor = m\cdot k $ using Real_ZF_1_4_L14

qed

Floor of the sum of a number and the embedding of an integer is the floor of the number plus the integer.

lemma (in real1) Real_ZF_1_4_L15:

assumes A1: $ x\in \mathbb{R} $ and A2: $ p \in int $

shows $ \lfloor x + p^R\rfloor = \lfloor x\rfloor + p $proof

let $ A = \{n \in int.\ n^R \leq x + p^R\} $

have $ \text{antisym}(IntegerOrder) $ using Int_ZF_2_L4

moreover

have $ \lfloor x\rfloor + p \in A $proof

from A1, A2 have $ \lfloor x\rfloor ^R \leq x $ and $ p^R \in \mathbb{R} $ using Real_ZF_1_4_L7, real_int_is_real

then have $ \lfloor x\rfloor ^R + p^R \leq x + p^R $ using add_num_to_ineq

moreover

from A1, A2 have $ (\lfloor x\rfloor + p)^R = \lfloor x\rfloor ^R + p^R $ using Real_ZF_1_4_L7, Real_ZF_1_4_L1A

ultimately have $ (\lfloor x\rfloor + p)^R \leq x + p^R $

moreover

from A1, A2 have $ \lfloor x\rfloor + p \in int $ using Real_ZF_1_4_L7, Int_ZF_1_1_L5

ultimately show $ \lfloor x\rfloor + p \in A $

qed

moreover

have $ \forall n\in A.\ n \leq \lfloor x\rfloor + p $proof

fix $ n $

assume $ n\in A $

then have I: $ n \in int $ and $ n^R \leq x + p^R $

with A1, A2 have $ n^R - p^R \leq x $ using real_int_is_real, Real_ZF_1_2_L19

with A2, I have $ \lfloor (n - p)^R\rfloor \leq \lfloor x\rfloor $ using Real_ZF_1_4_L1B, Real_ZF_1_4_L9

moreover

from A2, I have $ n - p \in int $ using Int_ZF_1_1_L5

then have $ \lfloor (n - p)^R\rfloor = n - p $ using Real_ZF_1_4_L14

ultimately have $ n - p \leq \lfloor x\rfloor $

with A2, I show $ n \leq \lfloor x\rfloor + p $ using Int_ZF_2_L9C

qed

ultimately show $ \lfloor x + p^R\rfloor = \lfloor x\rfloor + p $ using Order_ZF_4_L14

qed

Floor of the difference of a number and the embedding of an integer is the floor of the number minus the integer.

lemma (in real1) Real_ZF_1_4_L16:

assumes A1: $ x\in \mathbb{R} $ and A2: $ p \in int $

shows $ \lfloor x - p^R\rfloor = \lfloor x\rfloor - p $proof

from A2 have $ \lfloor x - p^R\rfloor = \lfloor x + ( - p)^R\rfloor $ using Real_ZF_1_4_L1

with A1, A2 show $ \lfloor x - p^R\rfloor = \lfloor x\rfloor - p $ using Int_ZF_1_1_L4, Real_ZF_1_4_L15

qed

The floor of sum of embeddings is the sum of the integers.

lemma (in real1) Real_ZF_1_4_L17:

assumes $ m \in int $, $ n \in int $

shows $ \lfloor (m^R) + n^R\rfloor = m + n $ using assms, real_int_is_real, Real_ZF_1_4_L15, Real_ZF_1_4_L14

A lemma about adding one to floor.

lemma (in real1) Real_ZF_1_4_L17A:

assumes A1: $ a\in \mathbb{R} $

shows $ 1 + \lfloor a\rfloor ^R = (1 _Z + \lfloor a\rfloor )^R $proof

have $ 1 + \lfloor a\rfloor ^R = 1 _Z^R + \lfloor a\rfloor ^R $ using int_0_1_are_real_zero_one

with A1 show $ 1 + \lfloor a\rfloor ^R = (1 _Z + \lfloor a\rfloor )^R $ using int_zero_one_are_int, Real_ZF_1_4_L7, Real_ZF_1_4_L1A

qed

The difference between the a number and the embedding of its floor is (strictly) less than one.

lemma (in real1) Real_ZF_1_4_L17B:

assumes A1: $ a\in \mathbb{R} $

shows $ a - \lfloor a\rfloor ^R \lt 1 $, $ a \lt (1 _Z + \lfloor a\rfloor )^R $proof

from A1 have T1: $ \lfloor a\rfloor \in int $, $ \lfloor a\rfloor ^R \in \mathbb{R} $ and T2: $ 1 \in \mathbb{R} $, $ a - \lfloor a\rfloor ^R \in \mathbb{R} $ using Real_ZF_1_4_L7, real_int_is_real, Real_ZF_1_L6, Real_ZF_1_L4

{

assume $ 1 \leq a - \lfloor a\rfloor ^R $

with A1, T1 have $ \lfloor 1 _Z^R + \lfloor a\rfloor ^R\rfloor \leq \lfloor a\rfloor $ using Real_ZF_1_2_L21, Real_ZF_1_4_L9, int_0_1_are_real_zero_one

with T1 have $ False $ using int_zero_one_are_int, Real_ZF_1_4_L17, Int_ZF_1_2_L3AA

}

then have I: $ \neg (1 \leq a - \lfloor a\rfloor ^R) $

with T2 show II: $ a - \lfloor a\rfloor ^R \lt 1 $ by (rule Real_ZF_1_2_L20 )

with A1, T1, I, II have $ a \lt 1 + \lfloor a\rfloor ^R $ using Real_ZF_1_2_L26

with A1 show $ a \lt (1 _Z + \lfloor a\rfloor )^R $ using Real_ZF_1_4_L17A

qed

The next lemma corresponds to Lemma 14 iii) in \cite{Arthan2004}. It says that we can find a rational number between any two different real numbers.

lemma (in real1) Arthan_Lemma14iii:

assumes A1: $ x \lt y $

shows $ \exists M\in int.\ \exists N\in \mathbb{Z} _+.\ x\cdot N^R \lt M^R \wedge M^R \lt y\cdot N^R $proof

from A1 have $ (y - x)^{-1} \in \mathbb{R} _+ $ using Real_ZF_1_3_L3

then have $ \exists N\in \mathbb{Z} _+.\ (y - x)^{-1} \lt N^R $ using Arthan_Lemma14i, PositiveSet_def

then obtain $ N $ where I: $ N\in \mathbb{Z} _+ $ and II: $ (y - x)^{-1} \lt N^R $

let $ M = 1 _Z + \lfloor x\cdot N^R\rfloor $

from A1, I have T1: $ x\in \mathbb{R} $, $ N^R \in \mathbb{R} $, $ N^R \in \mathbb{R} _+ $, $ x\cdot N^R \in \mathbb{R} $ using Real_ZF_1_2_L15, PositiveSet_def, real_int_is_real, Real_ZF_1_L6, int_pos_is_real_pos

then have T2: $ M \in int $ using int_zero_one_are_int, Real_ZF_1_4_L7, Int_ZF_1_1_L5

from T1 have III: $ x\cdot N^R \lt M^R $ using Real_ZF_1_4_L17B

from T1 have $ (1 + \lfloor x\cdot N^R\rfloor ^R) \leq (1 + x\cdot N^R) $ using Real_ZF_1_4_L7, Real_ZF_1_L4, real_ord_transl_inv

with T1 have $ M^R \leq (1 + x\cdot N^R) $ using Real_ZF_1_4_L17A

moreover

from A1, II have $ (1 + x\cdot N^R) \lt y\cdot N^R $ using Real_ZF_1_3_L5

ultimately have $ M^R \lt y\cdot N^R $ by (rule real_strict_ord_transit )

with I, T2, III show $ thesis $

qed

Some estimates for the homomorphism difference of the floor function.

lemma (in real1) Real_ZF_1_4_L18:

assumes A1: $ x\in \mathbb{R} $, $ y\in \mathbb{R} $

shows $ abs(\lfloor x + y\rfloor - \lfloor x\rfloor - \lfloor y\rfloor ) \leq 2 _Z $proof

from A1 have T: $ \lfloor x\rfloor ^R \in \mathbb{R} $, $ \lfloor y\rfloor ^R \in \mathbb{R} $, $ x + y - (\lfloor x\rfloor ^R) \in \mathbb{R} $ using Real_ZF_1_4_L7, real_int_is_real, Real_ZF_1_L6

from A1 have $ 0 \leq x - (\lfloor x\rfloor ^R) + (y - (\lfloor y\rfloor ^R)) $, $ x - (\lfloor x\rfloor ^R) + (y - (\lfloor y\rfloor ^R)) \leq 2 $ using Real_ZF_1_4_L7, Real_ZF_1_2_L16, Real_ZF_1_2_L17, Real_ZF_1_4_L17B, Real_ZF_1_2_L18

moreover

from A1, T have $ x - (\lfloor x\rfloor ^R) + (y - (\lfloor y\rfloor ^R)) = x + y - (\lfloor x\rfloor ^R) - (\lfloor y\rfloor ^R) $ using Real_ZF_1_L7A

ultimately have $ 0 \leq x + y - (\lfloor x\rfloor ^R) - (\lfloor y\rfloor ^R) $, $ x + y - (\lfloor x\rfloor ^R) - (\lfloor y\rfloor ^R) \leq 2 $

then have $ \lfloor 0 \rfloor \leq \lfloor x + y - (\lfloor x\rfloor ^R) - (\lfloor y\rfloor ^R)\rfloor $, $ \lfloor x + y - (\lfloor x\rfloor ^R) - (\lfloor y\rfloor ^R)\rfloor \leq \lfloor 2 \rfloor $ using Real_ZF_1_4_L9

then have $ 0 _Z \leq \lfloor x + y - (\lfloor x\rfloor ^R) - (\lfloor y\rfloor ^R)\rfloor $, $ \lfloor x + y - (\lfloor x\rfloor ^R) - (\lfloor y\rfloor ^R)\rfloor \leq 2 _Z $ using floor_01_is_zero_one, floor_2_is_two

moreover

from A1 have $ \lfloor x + y - (\lfloor x\rfloor ^R) - (\lfloor y\rfloor ^R)\rfloor = \lfloor x + y\rfloor - \lfloor x\rfloor - \lfloor y\rfloor $ using Real_ZF_1_L6, Real_ZF_1_4_L7, real_int_is_real, Real_ZF_1_4_L16

ultimately have $ 0 _Z \leq \lfloor x + y\rfloor - \lfloor x\rfloor - \lfloor y\rfloor $, $ \lfloor x + y\rfloor - \lfloor x\rfloor - \lfloor y\rfloor \leq 2 _Z $

then show $ abs(\lfloor x + y\rfloor - \lfloor x\rfloor - \lfloor y\rfloor ) \leq 2 _Z $ using Int_ZF_2_L16

qed

Suppose $S\neq \emptyset$ is bounded above and $\Gamma(S,m) =\lfloor m^R\cdot x\rfloor$ for some positive integer $m$ and $x\in S$. Then if $y\in S, x\leq y$ we also have $\Gamma(S,m) =\lfloor m^R\cdot y\rfloor$.

lemma (in real1) Real_ZF_1_4_L20:

assumes A1: $ \text{IsBoundedAbove}(S,OrderOnReals) $, $ S\neq 0 $ and A2: $ n\in \mathbb{Z} _+ $, $ x\in S $ and A3: $ \Gamma (S,n) = \lfloor n^R\cdot x\rfloor $ and A4: $ y\in S $, $ x\leq y $

shows $ \Gamma (S,n) = \lfloor n^R\cdot y\rfloor $proof

from A2, A4 have $ \lfloor n^R\cdot x\rfloor \leq \lfloor (n^R)\cdot y\rfloor $ using int_pos_is_real_pos, Real_ZF_1_2_L14, Real_ZF_1_4_L9

with A3 have $ \langle \Gamma (S,n),\lfloor (n^R)\cdot y\rfloor \rangle \in IntegerOrder $

moreover

from A1, A2, A4 have $ \langle \lfloor n^R\cdot y\rfloor ,\Gamma (S,n)\rangle \in IntegerOrder $ using Real_ZF_1_4_L11

ultimately show $ \Gamma (S,n) = \lfloor n^R\cdot y\rfloor $ by (rule Int_ZF_2_L3 )

qed

The homomorphism difference of $n\mapsto \Gamma(S,n)$ is bounded by $2$ on positive integers.

lemma (in real1) Real_ZF_1_4_L21:

assumes A1: $ \text{IsBoundedAbove}(S,OrderOnReals) $, $ S\neq 0 $ and A2: $ m\in \mathbb{Z} _+ $, $ n\in \mathbb{Z} _+ $

shows $ abs(\Gamma (S,m + n) - \Gamma (S,m) - \Gamma (S,n)) \leq 2 _Z $proof

from A2 have T: $ m + n \in \mathbb{Z} _+ $ using pos_int_closed_add_unfolded

with A1, A2 have $ \Gamma (S,m) \in \{\lfloor m^R\cdot x\rfloor .\ x\in S\} $ and $ \Gamma (S,n) \in \{\lfloor n^R\cdot x\rfloor .\ x\in S\} $ and $ \Gamma (S,m + n) \in \{\lfloor (m + n)^R\cdot x\rfloor .\ x\in S\} $ using Real_ZF_1_4_L10

then obtain $ a $ $ b $ $ c $ where I: $ a\in S $, $ b\in S $, $ c\in S $ and II: $ \Gamma (S,m) = \lfloor m^R\cdot a\rfloor $, $ \Gamma (S,n) = \lfloor n^R\cdot b\rfloor $, $ \Gamma (S,m + n) = \lfloor (m + n)^R\cdot c\rfloor $

let $ d = \text{Maximum}(OrderOnReals,\{a,b,c\}) $

from A1, I have $ a\in \mathbb{R} $, $ b\in \mathbb{R} $, $ c\in \mathbb{R} $ using Real_ZF_1_2_L23

then have IV: $ d \in \{a,b,c\} $, $ d \in \mathbb{R} $, $ a \leq d $, $ b \leq d $, $ c \leq d $ using Real_ZF_1_2_L24

with I have V: $ d \in S $

from A1, T, I, II, IV, V have $ \Gamma (S,m + n) = \lfloor (m + n)^R\cdot d\rfloor $ using Real_ZF_1_4_L20

also

from A2 have $ \ldots = \lfloor ((m^R) + (n^R))\cdot d\rfloor $ using Real_ZF_1_4_L1A, PositiveSet_def

also

from A2, IV have $ \ldots = \lfloor (m^R)\cdot d + (n^R)\cdot d\rfloor $ using PositiveSet_def, real_int_is_real, Real_ZF_1_L7

finally have $ \Gamma (S,m + n) = \lfloor (m^R)\cdot d + (n^R)\cdot d\rfloor $

moreover

from A1, A2, I, II, IV, V have $ \Gamma (S,m) = \lfloor m^R\cdot d\rfloor $ using Real_ZF_1_4_L20

moreover

from A1, A2, I, II, IV, V have $ \Gamma (S,n) = \lfloor n^R\cdot d\rfloor $ using Real_ZF_1_4_L20

moreover

from A1, T, I, II, IV, V have $ \Gamma (S,m + n) = \lfloor (m + n)^R\cdot d\rfloor $ using Real_ZF_1_4_L20

ultimately have $ abs(\Gamma (S,m + n) - \Gamma (S,m) - \Gamma (S,n)) =$ $ abs(\lfloor (m^R)\cdot d + (n^R)\cdot d\rfloor - \lfloor m^R\cdot d\rfloor - \lfloor n^R\cdot d\rfloor ) $

with A2, IV show $ abs(\Gamma (S,m + n) - \Gamma (S,m) - \Gamma (S,n)) \leq 2 _Z $ using PositiveSet_def, real_int_is_real, Real_ZF_1_L6, Real_ZF_1_4_L18

qed

The next lemma provides sufficient condition for an odd function to be an almost homomorphism. It says for odd functions we only need to check that the homomorphism difference (denoted $ \delta $ in the real1 context) is bounded on positive integers. This is really proven in Int_ZF_2.thy, but we restate it here for convenience. Recall from Group_ZF_3.thy that OddExtension of a function defined on the set of positive elements (of an ordered group) is the only odd function that is equal to the given one when restricted to positive elements.

lemma (in real1) Real_ZF_1_4_L21A:

assumes A1: $ f:\mathbb{Z} _+\rightarrow int $, $ \forall a\in \mathbb{Z} _+.\ \forall b\in \mathbb{Z} _+.\ abs(\delta (f,a,b)) \leq L $

shows $ \text{OddExtension}(int,IntegerAddition,IntegerOrder,f) \in \mathcal{S} $ using A1, Int_ZF_2_1_L24

The candidate for (a representant of) the supremum of a nonempty bounded above set is a slope.

lemma (in real1) Real_ZF_1_4_L22:

assumes A1: $ \text{IsBoundedAbove}(S,OrderOnReals) $, $ S\neq 0 $ and A2: $ g = \{\langle p,\Gamma (S,p)\rangle .\ p\in \mathbb{Z} _+\} $

shows $ \text{OddExtension}(int,IntegerAddition,IntegerOrder,g) \in \mathcal{S} $proof

from A1, A2 have $ g: \mathbb{Z} _+\rightarrow int $ by (rule Real_ZF_1_4_L12 )

moreover

have $ \forall m\in \mathbb{Z} _+.\ \forall n\in \mathbb{Z} _+.\ abs(\delta (g,m,n)) \leq 2 _Z $proof

{

fix $ m $ $ n $

assume A3: $ m\in \mathbb{Z} _+ $, $ n\in \mathbb{Z} _+ $

then have $ m + n \in \mathbb{Z} _+ $, $ m\in \mathbb{Z} _+ $, $ n\in \mathbb{Z} _+ $ using pos_int_closed_add_unfolded

moreover

from A1, A2 have $ \forall n\in \mathbb{Z} _+.\ g(n) = \Gamma (S,n) $ by (rule Real_ZF_1_4_L12 )

ultimately have $ \delta (g,m,n) = \Gamma (S,m + n) - \Gamma (S,m) - \Gamma (S,n) $

moreover

from A1, A3 have $ abs(\Gamma (S,m + n) - \Gamma (S,m) - \Gamma (S,n)) \leq 2 _Z $ by (rule Real_ZF_1_4_L21 )

ultimately have $ abs(\delta (g,m,n)) \leq 2 _Z $

}

then show $ \forall m\in \mathbb{Z} _+.\ \forall n\in \mathbb{Z} _+.\ abs(\delta (g,m,n)) \leq 2 _Z $

qed

ultimately show $ thesis $ by (rule Real_ZF_1_4_L21A )

qed

A technical lemma used in the proof that all elements of $S$ are less or equal than the candidate for supremum of $S$.

lemma (in real1) Real_ZF_1_4_L23:

assumes A1: $ f \in \mathcal{S} $ and A2: $ N \in int $, $ M \in int $ and A3: $ \forall n\in \mathbb{Z} _+.\ M\cdot n \leq f(N\cdot n) $

shows $ M^R \leq [f]\cdot (N^R) $proof

let $ M_S = \{\langle n, M\cdot n\rangle .\ n \in int\} $

let $ N_S = \{\langle n, N\cdot n\rangle .\ n \in int\} $

from A1, A2 have T: $ M_S \in \mathcal{S} $, $ N_S \in \mathcal{S} $, $ f\circ N_S \in \mathcal{S} $ using Int_ZF_2_5_L1, Int_ZF_2_1_L11, SlopeOp2_def

moreover

from A1, A2, A3 have $ M_S \sim f\circ N_S \vee f\circ N_S + ( - M_S) \in \mathcal{S} _+ $ using Int_ZF_2_5_L8, SlopeOp2_def, SlopeOp1_def, Slopes_def, BoundedIntMaps_def, SlopeEquivalenceRel_def, PositiveIntegers_def, PositiveSlopes_def

ultimately have $ [M_S] \leq [f\circ N_S] $ using Real_ZF_1_2_L12

with A1, T show $ M^R \leq [f]\cdot (N^R) $ using Real_ZF_1_1_L4

qed

A technical lemma aimed used in the proof the candidate for supremum of $S$ is less or equal than any upper bound for $S$.

lemma (in real1) Real_ZF_1_4_L23A:

assumes A1: $ f \in \mathcal{S} $ and A2: $ N \in int $, $ M \in int $ and A3: $ \forall n\in \mathbb{Z} _+.\ f(N\cdot n) \leq M\cdot n $

shows $ [f]\cdot (N^R) \leq M^R $proof

let $ M_S = \{\langle n, M\cdot n\rangle .\ n \in int\} $

let $ N_S = \{\langle n, N\cdot n\rangle .\ n \in int\} $

from A1, A2 have T: $ M_S \in \mathcal{S} $, $ N_S \in \mathcal{S} $, $ f\circ N_S \in \mathcal{S} $ using Int_ZF_2_5_L1, Int_ZF_2_1_L11, SlopeOp2_def

moreover

from A1, A2, A3 have $ f\circ N_S \sim M_S \vee M_S + ( - (f\circ N_S)) \in \mathcal{S} _+ $ using Int_ZF_2_5_L9, SlopeOp2_def, SlopeOp1_def, Slopes_def, BoundedIntMaps_def, SlopeEquivalenceRel_def, PositiveIntegers_def, PositiveSlopes_def

ultimately have $ [f\circ N_S] \leq [M_S] $ using Real_ZF_1_2_L12

with A1, T show $ [f]\cdot (N^R)\leq M^R $ using Real_ZF_1_1_L4

qed

The essential condition to claim that the candidate for supremum of $S$ is greater or equal than all elements of $S$.

lemma (in real1) Real_ZF_1_4_L24:

assumes A1: $ \text{IsBoundedAbove}(S,OrderOnReals) $ and A2: $ x \lt y $, $ y\in S $ and A4: $ N \in \mathbb{Z} _+ $, $ M \in int $ and A5: $ M^R \lt y\cdot N^R $ and A6: $ p \in \mathbb{Z} _+ $

shows $ p\cdot M \leq \Gamma (S,p\cdot N) $proof

from A2, A4, A6 have T1: $ N^R \in \mathbb{R} _+ $, $ y\in \mathbb{R} $, $ p^R \in \mathbb{R} _+ $, $ p\cdot N \in \mathbb{Z} _+ $, $ (p\cdot N)^R \in \mathbb{R} _+ $ using int_pos_is_real_pos, Real_ZF_1_2_L15, pos_int_closed_mul_unfold

with A4, A6 have T2: $ p \in int $, $ p^R \in \mathbb{R} $, $ N^R \in \mathbb{R} $, $ N^R \neq 0 $, $ M^R \in \mathbb{R} $ using real_int_is_real, PositiveSet_def

from T1, A5 have $ \lfloor (p\cdot N)^R\cdot (M^R\cdot (N^R)^{-1})\rfloor \leq \lfloor (p\cdot N)^R\cdot y\rfloor $ using Real_ZF_1_3_L4A, Real_ZF_1_3_L7, Real_ZF_1_4_L9

moreover

from A1, A2, T1 have $ \lfloor (p\cdot N)^R\cdot y\rfloor \leq \Gamma (S,p\cdot N) $ using Real_ZF_1_4_L11

ultimately have I: $ \lfloor (p\cdot N)^R\cdot (M^R\cdot (N^R)^{-1})\rfloor \leq \Gamma (S,p\cdot N) $ by (rule int_order_transitive )

from A4, A6 have $ (p\cdot N)^R\cdot (M^R\cdot (N^R)^{-1}) = p^R\cdot N^R\cdot (M^R\cdot (N^R)^{-1}) $ using PositiveSet_def, Real_ZF_1_4_L1C

with A4, T2 have $ \lfloor (p\cdot N)^R\cdot (M^R\cdot (N^R)^{-1})\rfloor = p\cdot M $ using Real_ZF_1_3_L8, Real_ZF_1_4_L14A

with I show $ p\cdot M \leq \Gamma (S,p\cdot N) $

qed

An obvious fact about odd extension of a function $p\mapsto \Gamma(s,p)$ that is used a couple of times in proofs.

lemma (in real1) Real_ZF_1_4_L24A:

assumes A1: $ \text{IsBoundedAbove}(S,OrderOnReals) $, $ S\neq 0 $ and A2: $ p \in \mathbb{Z} _+ $ and A3: $ h = \text{OddExtension}(int,IntegerAddition,IntegerOrder,\{\langle p,\Gamma (S,p)\rangle .\ p\in \mathbb{Z} _+\}) $

shows $ h(p) = \Gamma (S,p) $proof

let $ g = \{\langle p,\Gamma (S,p)\rangle .\ p\in \mathbb{Z} _+\} $

from A1 have I: $ g : \mathbb{Z} _+\rightarrow int $ using Real_ZF_1_4_L12

with A2, A3 show $ h(p) = \Gamma (S,p) $ using Int_ZF_1_5_L11, ZF_fun_from_tot_val

qed

The candidate for the supremum of $S$ is not smaller than any element of $S$.

lemma (in real1) Real_ZF_1_4_L25:

assumes A1: $ \text{IsBoundedAbove}(S,OrderOnReals) $ and A2: $ \neg \text{HasAmaximum}(OrderOnReals,S) $ and A3: $ x\in S $ and A4: $ h = \text{OddExtension}(int,IntegerAddition,IntegerOrder,\{\langle p,\Gamma (S,p)\rangle .\ p\in \mathbb{Z} _+\}) $

shows $ x \leq [h] $proof

from A1, A2, A3 have $ S \subseteq \mathbb{R} $, $ \neg \text{HasAmaximum}(OrderOnReals,S) $, $ x\in S $ using Real_ZF_1_2_L23

then have $ \exists y\in S.\ x \lt y $ by (rule Real_ZF_1_2_L27 )

then obtain $ y $ where I: $ y\in S $ and II: $ x \lt y $

from II have $ \exists M\in int.\ \exists N\in \mathbb{Z} _+.\ x\cdot N^R \lt M^R \wedge M^R \lt y\cdot N^R $ using Arthan_Lemma14iii

then obtain $ M $ $ N $ where III: $ M \in int $, $ N\in \mathbb{Z} _+ $ and IV: $ x\cdot N^R \lt M^R $, $ M^R \lt y\cdot N^R $

from II, III, IV have V: $ x \leq M^R\cdot (N^R)^{-1} $ using int_pos_is_real_pos, Real_ZF_1_2_L15, Real_ZF_1_3_L4

from A3 have VI: $ S\neq 0 $

with A1, A4 have T1: $ h \in \mathcal{S} $ using Real_ZF_1_4_L22

moreover

from III have $ N \in int $, $ M \in int $ using PositiveSet_def

moreover

have $ \forall n\in \mathbb{Z} _+.\ M\cdot n \leq h(N\cdot n) $proof

let $ g = \{\langle p,\Gamma (S,p)\rangle .\ p\in \mathbb{Z} _+\} $

fix $ n $

assume A5: $ n\in \mathbb{Z} _+ $

with III have T2: $ N\cdot n \in \mathbb{Z} _+ $ using pos_int_closed_mul_unfold

from III, A5 have $ N\cdot n = n\cdot N $ and $ n\cdot M = M\cdot n $ using PositiveSet_def, Int_ZF_1_1_L5

moreover

from A1, I, II, III, IV, A5 have $ \text{IsBoundedAbove}(S,OrderOnReals) $, $ x \lt y $, $ y\in S $, $ N \in \mathbb{Z} _+ $, $ M \in int $, $ M^R \lt y\cdot N^R $, $ n \in \mathbb{Z} _+ $

then have $ n\cdot M \leq \Gamma (S,n\cdot N) $ by (rule Real_ZF_1_4_L24 )

moreover

from A1, A4, VI, T2 have $ h(N\cdot n) = \Gamma (S,N\cdot n) $ using Real_ZF_1_4_L24A

ultimately show $ M\cdot n \leq h(N\cdot n) $

qed

ultimately have $ M^R \leq [h]\cdot N^R $ using Real_ZF_1_4_L23

with III, T1 have $ M^R\cdot (N^R)^{-1} \leq [h] $ using int_pos_is_real_pos, Real_ZF_1_1_L3, Real_ZF_1_3_L4B

with V show $ x \leq [h] $ by (rule real_ord_transitive )

qed

The essential condition to claim that the candidate for supremum of $S$ is less or equal than any upper bound of $S$.

lemma (in real1) Real_ZF_1_4_L26:

assumes A1: $ \text{IsBoundedAbove}(S,OrderOnReals) $ and A2: $ x\leq y $, $ x\in S $ and A4: $ N \in \mathbb{Z} _+ $, $ M \in int $ and A5: $ y\cdot N^R \lt M^R $ and A6: $ p \in \mathbb{Z} _+ $

shows $ \lfloor (N\cdot p)^R\cdot x\rfloor \leq M\cdot p $proof

from A2, A4, A6 have T: $ p\cdot N \in \mathbb{Z} _+ $, $ p \in int $, $ N \in int $, $ p^R \in \mathbb{R} _+ $, $ p^R \in \mathbb{R} $, $ N^R \in \mathbb{R} $, $ x \in \mathbb{R} $, $ y \in \mathbb{R} $ using pos_int_closed_mul_unfold, PositiveSet_def, real_int_is_real, Real_ZF_1_2_L15, int_pos_is_real_pos

with A2 have $ (p\cdot N)^R\cdot x \leq (p\cdot N)^R\cdot y $ using int_pos_is_real_pos, Real_ZF_1_2_L14A

moreover

from A4, T have I: $ (p\cdot N)^R = p^R\cdot N^R $, $ (p\cdot M)^R = p^R\cdot M^R $ using Real_ZF_1_4_L1C

ultimately have $ (p\cdot N)^R\cdot x \leq p^R\cdot N^R\cdot y $

moreover

from A5, T, I have $ p^R\cdot (y\cdot N^R) \lt (p\cdot M)^R $ using Real_ZF_1_3_L7

with T have $ p^R\cdot N^R\cdot y \lt (p\cdot M)^R $ using Real_ZF_1_1_L9

ultimately have $ (p\cdot N)^R\cdot x \lt (p\cdot M)^R $ by (rule real_strict_ord_transit )

then have $ \lfloor (p\cdot N)^R\cdot x\rfloor \leq \lfloor (p\cdot M)^R\rfloor $ using Real_ZF_1_4_L9

moreover

from A4, T have $ p\cdot M \in int $ using Int_ZF_1_1_L5

then have $ \lfloor (p\cdot M)^R\rfloor = p\cdot M $ using Real_ZF_1_4_L14

moreover

from A4, A6 have $ p\cdot N = N\cdot p $ and $ p\cdot M = M\cdot p $ using PositiveSet_def, Int_ZF_1_1_L5

ultimately show $ \lfloor (N\cdot p)^R\cdot x\rfloor \leq M\cdot p $

qed

A piece of the proof of the fact that the candidate for the supremum of $S$ is not greater than any upper bound of $S$, done separately for clarity (of mind).

lemma (in real1) Real_ZF_1_4_L27:

assumes $ \text{IsBoundedAbove}(S,OrderOnReals) $, $ S\neq 0 $ and $ h = \text{OddExtension}(int,IntegerAddition,IntegerOrder,\{\langle p,\Gamma (S,p)\rangle .\ p\in \mathbb{Z} _+\}) $ and $ p \in \mathbb{Z} _+ $

shows $ \exists x\in S.\ h(p) = \lfloor p^R\cdot x\rfloor $ using assms, Real_ZF_1_4_L10, Real_ZF_1_4_L24A

The candidate for the supremum of $S$ is not greater than any upper bound of $S$.

lemma (in real1) Real_ZF_1_4_L28:

assumes A1: $ \text{IsBoundedAbove}(S,OrderOnReals) $, $ S\neq 0 $ and A2: $ \forall x\in S.\ x\leq y $ and A3: $ h = \text{OddExtension}(int,IntegerAddition,IntegerOrder,\{\langle p,\Gamma (S,p)\rangle .\ p\in \mathbb{Z} _+\}) $

shows $ [h] \leq y $proof

from A1 obtain $ a $ where $ a\in S $

with A1, A2, A3 have T: $ y\in \mathbb{R} $, $ h \in \mathcal{S} $, $ [h] \in \mathbb{R} $ using Real_ZF_1_2_L15, Real_ZF_1_4_L22, Real_ZF_1_1_L3

{

assume $ \neg ([h] \leq y) $

with T have $ y \lt [h] $ using Real_ZF_1_2_L28

then have $ \exists M\in int.\ \exists N\in \mathbb{Z} _+.\ y\cdot N^R \lt M^R \wedge M^R \lt [h]\cdot N^R $ using Arthan_Lemma14iii

then obtain $ M $ $ N $ where I: $ M\in int $, $ N\in \mathbb{Z} _+ $ and II: $ y\cdot N^R \lt M^R $, $ M^R \lt [h]\cdot N^R $

from I have III: $ N^R \in \mathbb{R} _+ $ using int_pos_is_real_pos

have $ \forall p\in \mathbb{Z} _+.\ h(N\cdot p) \leq M\cdot p $proof

fix $ p $

assume A4: $ p\in \mathbb{Z} _+ $

with A1, A3, I have $ \exists x\in S.\ h(N\cdot p) = \lfloor (N\cdot p)^R\cdot x\rfloor $ using pos_int_closed_mul_unfold, Real_ZF_1_4_L27

with A1, A2, I, II, A4 show $ h(N\cdot p) \leq M\cdot p $ using Real_ZF_1_4_L26

qed

with T, I have $ [h]\cdot N^R \leq M^R $ using PositiveSet_def, Real_ZF_1_4_L23A

with T, III have $ [h] \leq M^R\cdot (N^R)^{-1} $ using Real_ZF_1_3_L4C

moreover

from T, II, III have $ M^R\cdot (N^R)^{-1} \lt [h] $ using Real_ZF_1_3_L4A

ultimately have $ False $ using Real_ZF_1_2_L29

}

then show $ [h] \leq y $

qed

Now we can prove that every nonempty subset of reals that is bounded above has a supremum. Proof by considering two cases: when the set has a maximum and when it does not.

lemma (in real1) real_order_complete:

assumes A1: $ \text{IsBoundedAbove}(S,OrderOnReals) $, $ S\neq 0 $

shows $ \text{HasAminimum}(OrderOnReals,\bigcap a\in S.\ OrderOnReals\{a\}) $proof

{

assume $ \text{HasAmaximum}(OrderOnReals,S) $

with A1 have $ \text{HasAminimum}(OrderOnReals,\bigcap a\in S.\ OrderOnReals\{a\}) $ using Real_ZF_1_2_L10, IsAnOrdGroup_def, IsPartOrder_def, Order_ZF_5_L6

}

moreover {

assume A2: $ \neg \text{HasAmaximum}(OrderOnReals,S) $

let $ h = \text{OddExtension}(int,IntegerAddition,IntegerOrder,\{\langle p,\Gamma (S,p)\rangle .\ p\in \mathbb{Z} _+\}) $

let $ r = OrderOnReals $

from A1 have $ \text{antisym}(OrderOnReals) $, $ S\neq 0 $ using Real_ZF_1_2_L10, IsAnOrdGroup_def, IsPartOrder_def

moreover

from A1, A2 have $ \forall x\in S.\ \langle x,[h]\rangle \in r $ using Real_ZF_1_4_L25

moreover

from A1 have $ \forall y.\ (\forall x\in S.\ \langle x,y\rangle \in r) \longrightarrow \langle [h],y\rangle \in r $ using Real_ZF_1_4_L28

ultimately have $ \text{HasAminimum}(OrderOnReals,\bigcap a\in S.\ OrderOnReals\{a\}) $ by (rule Order_ZF_5_L5 )

} ultimately show $ thesis $

qed

Finally, we are ready to formulate the main result: that the construction of real numbers from the additive group of integers results in a complete ordered field. This theorem completes the construction. It was fun.

theorem eudoxus_reals_are_reals:

shows $ \text{IsAmodelOfReals}(RealNumbers,RealAddition,RealMultiplication,OrderOnReals) $ using reals_are_ord_field, real_order_complete, IsComplete_def, IsAmodelOfReals_def

end

Definition of Slopes: $ Slopes \equiv \text{AlmostHoms}(int,IntegerAddition) $

theorem (in int1) Arthan_Th_9:

assumes $ f\in \mathcal{S} $, $ g\in \mathcal{S} $

shows $ f\circ g \sim g\circ f $

Definition of SlopeOp1: $ SlopeOp1 \equiv \text{AlHomOp1}(int,IntegerAddition) $

Definition of BoundedIntMaps: $ BoundedIntMaps \equiv \text{FinRangeFunctions}(int,int) $

Definition of SlopeEquivalenceRel: $ SlopeEquivalenceRel \equiv \text{QuotientGroupRel}(Slopes,SlopeOp1,BoundedIntMaps) $

Definition of SlopeOp2: $ SlopeOp2 \equiv \text{AlHomOp2}(int,IntegerAddition) $

lemma Real_ZF_1_L11: shows $ \text{Congruent2}(SlopeEquivalenceRel,SlopeOp1) $, $ \text{Congruent2}(SlopeEquivalenceRel,SlopeOp2) $, $ SlopeEquivalenceRel \subseteq Slopes \times Slopes $, $ \text{equiv}(Slopes, SlopeEquivalenceRel) $, $ SlopeEquivalenceRel\{id(int)\} = $ $ \text{ TheNeutralElement}(RealNumbers,RealMultiplication) $, $ BoundedIntMaps \subseteq Slopes $

Definition of RealNumbers: $ RealNumbers \equiv Slopes//SlopeEquivalenceRel $

Definition of RealMultiplication: $ RealMultiplication \equiv \text{ProjFun2}(Slopes,SlopeEquivalenceRel,SlopeOp2) $

lemma EquivClass_1_L10:

assumes $ \text{equiv}(A,r) $ and $ \text{Congruent2}(r,f) $ and $ x\in A $, $ y\in A $

shows $ \text{ProjFun2}(A,r,f)\langle r\{x\},r\{y\}\rangle = r\{f\langle x,y\rangle \} $

Definition of RealAddition: $ RealAddition \equiv \text{ProjFun2}(Slopes,SlopeEquivalenceRel,SlopeOp1) $

lemma (in real0) Real_ZF_1_L12:

assumes $ s \in Slopes $ and $ r = \text{QuotientGroupRel}(Slopes,SlopeOp1,BoundedIntMaps) $

shows $ r\{ \text{GroupInv}(int,IntegerAddition)\circ s\} = - (r\{s\}) $

lemma (in int1) Int_ZF_2_1_L12:

assumes $ s\in \mathcal{S} $

shows $ - s \in \mathcal{S} $

lemma (in real1) Real_ZF_1_1_L4:

assumes $ f \in \mathcal{S} $, $ g \in \mathcal{S} $

shows $ [f] + [g] = [f + g] $, $ [f] \cdot [g] = [f\circ g] $

lemma (in real1) Real_ZF_1_1_L4A:

assumes $ f \in \mathcal{S} $

shows $ [ - f] = - [f] $

lemma (in real1) Real_ZF_1_1_L3A:

assumes $ a\in \mathbb{R} $

shows $ \exists f\in \mathcal{S} .\ a = [f] $

lemma (in real1) Real_ZF_1_1_L2:

assumes $ f \in \mathcal{S} $, $ g \in \mathcal{S} $

shows $ [f\circ g] = [g\circ f] $

theorem (in real1) real_mult_commute:

assumes $ a\in \mathbb{R} $, $ b\in \mathbb{R} $

shows $ a\cdot b = b\cdot a $

Definition of IsCommutative: $ f \text{ is commutative on } G \equiv \forall x\in G.\ \forall y\in G.\ f\langle x,y\rangle = f\langle y,x\rangle $

lemma (in real0) Real_ZF_1_L11A:

assumes $ s \in BoundedIntMaps $

shows $ SlopeEquivalenceRel\{s\} = 0 $

lemma Real_ZF_1_L13:

assumes $ s \in Slopes $, $ p \in Slopes $ and $ r = SlopeEquivalenceRel $

shows $ r\{s\} = r\{p\} \longleftrightarrow \langle s,p\rangle \in r $

lemma (in real1) Real_ZF_1_1_L5:

assumes $ f \in \mathcal{S} $, $ g \in \mathcal{S} $

shows $ [f] = [g] \longleftrightarrow f \sim g $

lemma Real_ZF_1_L14: shows $ id(int) \in Slopes $

lemma (in int1) Int_ZF_2_3_L12:

assumes $ f \in \text{FinRangeFunctions}(\mathbb{Z} ,\mathbb{Z} ) $

shows $ \neg (id(\mathbb{Z} ) \sim f) $

lemma (in real0) Real_ZF_1_L4: shows $ 0 \in \mathbb{R} $, $ 1 \in \mathbb{R} $

lemma (in real1) real_one_cl_identity: shows $ [id(int)] = 1 $

lemma (in real0) Real_ZF_1_L10:

assumes $ s \in Slopes $

shows $ SlopeEquivalenceRel\{s\} = 0 \longleftrightarrow s \in BoundedIntMaps $

lemma (in real1) Real_ZF_1_1_L7:

assumes $ f \in BoundedIntMaps $

shows $ \neg (id(int) \sim f) $

lemma (in real1) id_on_int_is_slope: shows $ id(int) \in \mathcal{S} $

lemma Real_ZF_1_L2: shows $ group0(RealNumbers,RealAddition) $, $ RealAddition \text{ is commutative on } RealNumbers $, $ group1(RealNumbers,RealAddition) $

lemma (in group0) inverse_in_group:

assumes $ x\in G $

shows $ x^{-1}\in G $

lemma real_mult_commutative: shows $ RealMultiplication \text{ is commutative on } RealNumbers $

lemma (in real0) Real_ZF_1_L3: shows $ ring0(\mathbb{R} ,RealAddition,RealMultiplication) $

lemma (in ring0) Ring_ZF_2_L4:

assumes $ M \text{ is commutative on } R $ and $ a\in R $, $ b\in R $, $ c\in R $

shows $ a\cdot (b\cdot c) = a\cdot c\cdot b $ and $ a\cdot b\cdot c = a\cdot c\cdot b $

Definition of PositiveSlopes: $ PositiveSlopes \equiv \{s \in Slopes.\ $ $ s(PositiveIntegers) \cap PositiveIntegers \notin Fin(int)\} $

lemma subset_with_property:

assumes $ Y = \{x\in X.\ b(x)\} $

shows $ Y \subseteq X $

lemma EquivClass_1_L1A:

assumes $ A\subseteq X $

shows $ \{r\{x\}.\ x\in A\} \subseteq X//r $

Definition of PositiveReals: $ PositiveReals \equiv \{SlopeEquivalenceRel\{s\}.\ s \in PositiveSlopes\} $

Definition of PositiveIntegers: $ PositiveIntegers \equiv \text{PositiveSet}(int,IntegerAddition,IntegerOrder) $

theorem (in int1) sum_of_pos_sls_is_pos_sl:

assumes $ f \in \mathcal{S} _+ $, $ g \in \mathcal{S} _+ $

shows $ f + g \in \mathcal{S} _+ $

theorem (in int1) comp_of_pos_sls_is_pos_sl:

assumes $ f \in \mathcal{S} _+ $, $ g \in \mathcal{S} _+ $

shows $ f\circ g \in \mathcal{S} _+ $

lemma (in int1) Int_ZF_2_3_L1B:

assumes $ f \in \text{FinRangeFunctions}(\mathbb{Z} ,\mathbb{Z} ) $

shows $ f\in \mathcal{S} $, $ f \notin \mathcal{S} _+ $

lemma (in real1) Real_ZF_1_2_L2: shows $ a \in PositiveReals \longleftrightarrow (\exists f\in \mathcal{S} _+.\ a = [f]) $

lemma Real_ZF_1_2_L1: shows $ PositiveSlopes \subseteq Slopes $, $ PositiveReals \subseteq RealNumbers $

lemma (in real1) Real_ZF_1_2_L3:

assumes $ f\in \mathcal{S} _+ $, $ g\in \mathcal{S} _+ $

shows $ f + g \in \mathcal{S} _+ $, $ f\circ g \in \mathcal{S} _+ $

Definition of IsOpClosed: $ A \text{ is closed under } f \equiv \forall x\in A.\ \forall y\in A.\ f\langle x,y\rangle \in A $

lemma (in real1) Real_ZF_1_2_L5:

assumes $ f \in BoundedIntMaps $

shows $ f \notin \mathcal{S} _+ $

theorem (in int1) Int_ZF_2_3_L8:

assumes $ f\in \mathcal{S} $ and $ f \notin \text{FinRangeFunctions}(\mathbb{Z} ,\mathbb{Z} ) $

shows $ (f \in \mathcal{S} _+) \text{ Xor } (( - f) \in \mathcal{S} _+) $

lemma (in int1) Int_ZF_2_3_L10:

assumes $ f\in \mathcal{S} $, $ g\in \mathcal{S} $ and $ R = \{AlEqRel\{s\}.\ s\in \mathcal{S} _+\} $ and $ (f\in \mathcal{S} _+) \text{ Xor } (g\in \mathcal{S} _+) $

shows $ (AlEqRel\{f\} \in R) \text{ Xor } (AlEqRel\{g\} \in R) $

lemma (in real1) Real_ZF_1_2_L7:

assumes $ f \in \mathcal{S} $ and $ [f] \neq 0 $

shows $ (f \in \mathcal{S} _+) \text{ Xor } (( - f) \in \mathcal{S} _+) $

lemma (in real1) Real_ZF_1_2_L8:

assumes $ f \in \mathcal{S} $, $ g \in \mathcal{S} $ and $ (f \in \mathcal{S} _+) \text{ Xor } (g \in \mathcal{S} _+) $

shows $ ([f] \in PositiveReals) \text{ Xor } ([g] \in PositiveReals) $

lemma (in real1) Real_ZF_1_2_L6: shows $ PositiveReals \text{ is closed under } RealAddition $, $ PositiveReals \text{ is closed under } RealMultiplication $, $ 0 \notin PositiveReals $

lemma (in real1) Real_ZF_1_2_L9:

assumes $ a\in \mathbb{R} $ and $ a\neq 0 $

shows $ (a \in PositiveReals) \text{ Xor } (( - a) \in PositiveReals) $

Definition of OrderOnReals: $ OrderOnReals \equiv \text{OrderFromPosSet}(RealNumbers,RealAddition,PositiveReals) $

theorem (in ring0) ring_ord_by_positive_set:

assumes $ M \text{ is commutative on } R $ and $ P\subseteq R $, $ P \text{ is closed under } A $, $ 0 \notin P $ and $ \forall a\in R.\ a\neq 0 \longrightarrow (a\in P) \text{ Xor } (( - a) \in P) $ and $ P \text{ is closed under } M $ and $ r = \text{OrderFromPosSet}(R,A,P) $

shows $ \text{IsAnOrdGroup}(R,A,r) $, $ \text{IsAnOrdRing}(R,A,M,r) $, $ r \text{ is total on } R $, $ \text{PositiveSet}(R,A,r) = P $, $ \text{Nonnegative}(R,A,r) = P \cup \{ 0 \} $, $ \text{HasNoZeroDivs}(R,A,M) $

theorem reals_are_ord_ring: shows $ \text{IsAnOrdRing}(RealNumbers,RealAddition,RealMultiplication,OrderOnReals) $, $ OrderOnReals \text{ is total on } RealNumbers $, $ \text{PositiveSet}(RealNumbers,RealAddition,OrderOnReals) = PositiveReals $, $ \text{HasNoZeroDivs}(RealNumbers,RealAddition,RealMultiplication) $

lemma OrdRing_ZF_1_L2:

assumes $ \text{IsAnOrdRing}(R,A,M,r) $

shows $ ring1(R,A,M,r) $

lemma (in ring1) OrdRing_ZF_1_L4: shows $ \text{IsAnOrdGroup}(R,A,r) $, $ r \text{ is total on } R $, $ A \text{ is commutative on } R $, $ group3(R,A,r) $

lemma Real_ZF_1_2_L10: shows $ ring1(RealNumbers,RealAddition,RealMultiplication,OrderOnReals) $, $ \text{IsAnOrdGroup}(RealNumbers,RealAddition,OrderOnReals) $, $ group3(RealNumbers,RealAddition,OrderOnReals) $, $ OrderOnReals \text{ is total on } RealNumbers $

lemma (in group3) OrderedGroup_ZF_1_L30:

assumes $ a\in G $, $ b\in G $ and $ a=b \vee b\cdot a^{-1} \in G_+ $

shows $ a\leq b $

lemma (in real1) Real_ZF_1_1_L5A:

assumes $ f \sim g $

shows $ [f] = [g] $

lemma (in real1) Real_ZF_1_1_L4B:

assumes $ f \in \mathcal{S} $, $ g \in \mathcal{S} $

shows $ [f] - [g] = [f + ( - g)] $

lemma (in real1) Real_ZF_1_1_L3:

assumes $ f \in \mathcal{S} $

shows $ [f] \in \mathbb{R} $

lemma (in real1) Real_ZF_1_2_L11:

assumes $ a\in \mathbb{R} $, $ b\in \mathbb{R} $ and $ a=b \vee b - a \in PositiveReals $

shows $ a\leq b $

lemma (in group3) OrderedGroup_ZF_1_L5AG:

assumes $ a \in G $ and $ a^{-1}\leq b $

shows $ b^{-1} \leq a $

lemma (in group3) group_order_antisym:

assumes $ a\leq b $, $ b\leq a $

shows $ a=b $

lemma (in group3) Group_order_transitive:

assumes $ a\leq b $, $ b\leq c $

shows $ a\leq c $

lemma (in ring1) OrdRing_ZF_1_L9:

assumes $ a\leq b $ and $ 0 \leq c $

shows $ a\cdot c \leq b\cdot c $, $ c\cdot a \leq c\cdot b $

lemma (in ring1) OrdRing_ZF_1_L9A:

assumes $ a\leq b $ and $ c\in R_+ $

shows $ a\cdot c \leq b\cdot c $, $ c\cdot a \leq c\cdot b $

lemma (in group3) OrderedGroup_ZF_1_L4:

assumes $ a\leq b $

shows $ a\in G $, $ b\in G $

lemma (in group3) OrderedGroup_ZF_1_L12A:

assumes $ a\leq b $

shows $ 1 \leq b\cdot a^{-1} $

lemma (in group3) OrderedGroup_ZF_1_L12:

assumes $ 1 \leq a $, $ 1 \leq b $

shows $ 1 \leq a\cdot b $

lemma (in group3) OrderedGroup_ZF_1_L5B:

assumes $ a\leq b $ and $ c\leq d $

shows $ a\cdot c \leq b\cdot d $

lemma (in group3) OrderedGroup_ZF_1_L3:

assumes $ g\in G $

shows $ g\leq g $

Definition of IsAnOrdGroup: $ \text{IsAnOrdGroup}(G,P,r) \equiv $ $ ( \text{IsAgroup}(G,P) \wedge r\subseteq G\times G \wedge \text{IsPartOrder}(G,r) \wedge (\forall g\in G.\ \forall a b.\ $ $ \langle a,b\rangle \in r \longrightarrow \langle P\langle a,g\rangle ,P\langle b,g\rangle \rangle \in r \wedge \langle P\langle g,a\rangle ,P\langle g,b\rangle \rangle \in r ) ) $

lemma (in group3) OrderedGroup_ZF_1_L9C:

assumes $ a\in G $, $ b\in G $ and $ c\leq a\cdot b $

shows $ c\cdot b^{-1} \leq a $, $ a^{-1}\cdot c \leq b $

lemma (in group3) OrderedGroup_ZF_1_L8:

assumes $ r \text{ is total on } G $ and $ a\in G $, $ b\in G $ and $ \neg (a\leq b) $

shows $ b \leq a $, $ a^{-1} \leq b^{-1} $, $ a\neq b $, $ b \lt a $

lemma (in group3) OrderedGroup_ZF_1_L5J:

assumes $ a\in G $, $ b\in G $ and $ c \leq a\cdot b^{-1} $

shows $ c\cdot b \leq a $

lemma (in real1) Real_ZF_1_2_L22: shows $ OrderOnReals \subseteq \mathbb{R} \times \mathbb{R} $

lemma Order_ZF_3_L1A:

assumes $ r \subseteq X\times X $ and $ \text{IsBoundedAbove}(A,r) $

shows $ A\subseteq X $

lemma (in group3) group_ord_total_is_lin:

assumes $ r \text{ is total on } G $

shows $ \text{IsLinOrder}(G,r) $

corollary Finite_ZF_1_L2A:

assumes $ \text{IsLinOrder}(X,r) $ and $ a\in X $, $ b\in X $, $ c\in X $

shows $ \text{Maximum}(r,\{a,b,c\}) \in \{a,b,c\} $, $ \text{Minimum}(r,\{a,b,c\}) \in \{a,b,c\} $, $ \text{Maximum}(r,\{a,b,c\}) \in X $, $ \text{Minimum}(r,\{a,b,c\}) \in X $, $ \langle a, \text{Maximum}(r,\{a,b,c\})\rangle \in r $, $ \langle b, \text{Maximum}(r,\{a,b,c\})\rangle \in r $, $ \langle c, \text{Maximum}(r,\{a,b,c\})\rangle \in r $

lemma (in group3) group_strict_ord_transit:

assumes $ a\leq b $ and $ b \lt c $

shows $ a \lt c $

lemma (in ring1) OrdRing_ZF_3_L17:

assumes $ \text{HasNoZeroDivs}(R,A,M) $ and $ b\in R_+ $ and $ a\leq b $ and $ 1 \lt c $

shows $ a \lt b\cdot c $

lemma (in group3) OrderedGroup_ZF_1_L12B:

assumes $ a\in G $, $ b\in G $ and $ a\cdot b^{-1} \lt c $

shows $ a \lt c\cdot b $

lemma Int_ZF_2_L5:

assumes $ \langle m,n\rangle \in IntegerOrder $, $ \langle n,k\rangle \in IntegerOrder $

shows $ \langle m,k\rangle \in IntegerOrder $

lemma (in group3) OrderedGroup_ZF_2_L2B:

assumes $ r \text{ is total on } G $ and $ A\subseteq G $ and $ \neg \text{HasAmaximum}(r,A) $ and $ x\in A $

shows $ \exists y\in A.\ x \lt y $

lemma (in group3) OrderedGroup_ZF_1_L8AA:

assumes $ a\leq b $ and $ a\neq b $

shows $ \neg (b\leq a) $

theorem (in int1) pos_slope_has_inv:

assumes $ f \in \mathcal{S} _+ $

shows $ \exists g\in \mathcal{S} .\ f\sim g \wedge (\exists h\in \mathcal{S} .\ g\circ h \sim id(\mathbb{Z} )) $

lemma (in real1) real_zero_not_one: shows $ 1 \neq 0 $

lemma (in real1) pos_slopes_have_inv:

assumes $ f \in \mathcal{S} _+ $

shows $ \exists g\in \mathcal{S} .\ f\sim g \wedge (\exists h\in \mathcal{S} .\ g\circ h \sim id(int)) $

lemma (in ring1) OrdField_ZF_1_L4:

assumes $ 0 \neq 1 $ and $ M \text{ is commutative on } R $ and $ \forall a\in R_+.\ \exists b\in R.\ a\cdot b = 1 $

shows $ \text{IsAnOrdField}(R,A,M,r) $

theorem (in real1) reals_are_ord_field: shows $ \text{IsAnOrdField}(RealNumbers,RealAddition,RealMultiplication,OrderOnReals) $

lemma OrdField_ZF_1_L1A:

assumes $ \text{IsAnOrdField}(K,A,M,r) $

shows $ \text{IsAfield}(K,A,M) $

lemma reals_are_field: shows $ \text{IsAfield}(RealNumbers,RealAddition,RealMultiplication) $

lemma field_field0:

assumes $ \text{IsAfield}(K,A,M) $

shows $ field0(K,A,M) $

lemma OrdField_ZF_1_L2:

assumes $ \text{IsAnOrdField}(K,A,M,r) $

shows $ field1(K,A,M,r) $

lemma field_cntxts_ok: shows $ field0(RealNumbers,RealAddition,RealMultiplication) $, $ field1(RealNumbers,RealAddition,RealMultiplication,OrderOnReals) $

lemma (in field1) OrdField_ZF_1_L8:

assumes $ a \in R_+ $

shows $ a^{-1} \in R_+ $, $ a\cdot (a^{-1}) = 1 $, $ (a^{-1})\cdot a = 1 $

Definition of PositiveSet: $ \text{PositiveSet}(L,A,r) \equiv $ $ \{x\in L.\ \langle \text{ TheNeutralElement}(L,A),x\rangle \in r \wedge \text{ TheNeutralElement}(L,A)\neq x\} $

lemma (in field1) OrdField_ZF_2_L2:

assumes $ a\in R_+ $ and $ a^{-1} \lt b $

shows $ 1 \lt b\cdot a $

lemma (in field1) OrdField_ZF_1_L9:

assumes $ a \lt b $

shows $ (b - a)^{-1} \in R_+ $

lemma (in field1) OrdField_ZF_2_L6:

assumes $ a\in R $, $ b\in R_+ $ and $ a\cdot b \lt c $

shows $ a \lt c\cdot b^{-1} $

lemma (in field1) OrdField_ZF_2_L6A:

assumes $ b\in R $, $ c\in R_+ $ and $ a \lt b\cdot c $

shows $ a\cdot c^{-1} \lt b $

lemma (in field1) OrdField_ZF_2_L5A:

assumes $ b\in R $, $ c\in R_+ $ and $ a \leq b\cdot c $

shows $ a\cdot c^{-1} \leq b $

lemma (in field1) OrdField_ZF_2_L5:

assumes $ a\in R $, $ b\in R_+ $ and $ a\cdot b \leq c $

shows $ a \leq c\cdot b^{-1} $

lemma (in field1) OrdField_ZF_2_L9:

assumes $ a \lt b $ and $ (b - a)^{-1} \lt c $

shows $ 1 + a\cdot c \lt b\cdot c $

lemma (in field1) OrdField_ZF_2_L3:

assumes $ a\leq b $ and $ c\in R_+ $

shows $ a\cdot (c^{-1}) \leq b\cdot (c^{-1}) $

lemma (in field1) OrdField_ZF_2_L4:

assumes $ a \lt b $ and $ c\in R_+ $

shows $ a\cdot c \lt b\cdot c $, $ c\cdot a \lt c\cdot b $, $ a\cdot c^{-1} \lt b\cdot c^{-1} $

lemma (in field0) Field_ZF_2_L6:

assumes $ a\in K $, $ b\in K $, $ b\neq 0 $, $ c\in K $

shows $ a\cdot b\cdot (c\cdot b^{-1}) = a\cdot c $

lemma (in int1) Int_ZF_2_5_L1:

assumes $ m \in \mathbb{Z} $

shows $ \forall n \in \mathbb{Z} .\ (m^S)(n) = m\cdot n $, $ m^S \in \mathcal{S} $

lemma (in int1) Int_ZF_2_5_L3:

assumes $ m \in \mathbb{Z} $

shows $ ( - m)^S = - (m^S) $

lemma (in int1) Int_ZF_2_5_L3A:

assumes $ m\in \mathbb{Z} $, $ k\in \mathbb{Z} $

shows $ (m^S) + (k^S) = ((m + k)^S) $

lemma (in int0) Int_ZF_1_1_L4:

assumes $ a \in \mathbb{Z} $

shows $ a + 0 = a $, $ 0 + a = a $, $ a\cdot 1 = a $, $ 1 \cdot a = a $, $ 0 \cdot a = 0 $, $ a\cdot 0 = 0 $, $ ( - a) \in \mathbb{Z} $, $ ( - ( - a)) = a $, $ a - a = 0 $, $ a - 0 = a $, $ 2 \cdot a = a + a $

lemma (in real1) Real_ZF_1_4_L1A:

assumes $ m \in int $, $ k \in int $

shows $ m^R + k^R = ((m + k)^R) $

lemma (in real1) Real_ZF_1_4_L1:

assumes $ m \in int $

shows $ ( - m)^R = - (m^R) $

lemma (in int1) Int_ZF_2_5_L3B:

assumes $ m\in \mathbb{Z} $, $ k\in \mathbb{Z} $

shows $ (m^S) \circ (k^S) = ((m\cdot k)^S) $

lemma (in int1) Int_ZF_2_5_L2:

assumes $ f \in \mathcal{S} $

shows $ \exists m\in \mathbb{Z} .\ \exists g\in \mathcal{S} .\ (m^S\sim g \wedge (f\sim g \vee g + ( - f) \in \mathcal{S} _+)) $

lemma (in real1) Real_ZF_1_2_L12:

assumes $ f \in \mathcal{S} $, $ g \in \mathcal{S} $ and $ f\sim g \vee (g + ( - f)) \in \mathcal{S} _+ $

shows $ [f] \leq [g] $

lemma (in real1) Real_ZF_1_1_L8:

assumes $ a\in \mathbb{R} $

shows $ ( - a) \in \mathbb{R} $

lemma (in real1) Real_ZF_1_4_L2:

assumes $ a\in \mathbb{R} $

shows $ \exists m\in int.\ a \leq m^R $

lemma (in real1) Real_ZF_1_2_L13:

assumes $ a\in \mathbb{R} $ and $ ( - a) \leq b $

shows $ ( - b) \leq a $

Definition of AlmostHoms: $ \text{AlmostHoms}(G,f) \equiv $ $ \{s \in G\rightarrow G.\ \{ \text{HomDiff}(G,f,s,x).\ x \in G\times G \} \in Fin(G)\} $

lemma (in int1) Int_ZF_2_5_L6:

assumes $ m\in \mathbb{Z} $, $ k\in \mathbb{Z} $ and $ (m^S) \sim (k^S) $

shows $ m=k $

lemma (in int0) Int_ZF_2_L1A:

assumes $ m \leq n $

shows $ m $\leq n $, $ m\in \mathbb{Z} $, $ n\in \mathbb{Z} $

lemma (in int1) Int_ZF_2_5_L4:

assumes $ m\leq n $

shows $ (m^S) \sim (n^S) \vee (n^S) + ( - (m^S)) \in \mathcal{S} _+ $

lemma (in real1) Real_ZF_1_4_L5:

assumes $ m\leq k $

shows $ m^R \leq k^R $

lemma (in real1) Real_ZF_1_4_L4:

assumes $ m \in int $, $ k \in int $ and $ m^R = k^R $

shows $ m=k $

lemma (in int0) Int_ZF_1_5_L7B:

assumes $ a\in \mathbb{Z} $

shows $ a \leq \text{GreaterOf}(IntegerOrder,1 ,a) $, $ \text{GreaterOf}(IntegerOrder,1 ,a) \in \mathbb{Z} _+ $, $ \text{GreaterOf}(IntegerOrder,1 ,a) + 1 \in \mathbb{Z} _+ $, $ a \leq \text{GreaterOf}(IntegerOrder,1 ,a) + 1 $, $ a \neq \text{GreaterOf}(IntegerOrder,1 ,a) + 1 $

lemma (in real1) Real_ZF_1_4_L5A:

assumes $ m\leq k $, $ m\neq k $

shows $ m^R \lt k^R $

lemma (in real1) real_strict_ord_transit:

assumes $ a\leq b $ and $ b \lt c $

shows $ a \lt c $

lemma (in int0) Int_ZF_2_L19:

assumes $ m\in \mathbb{Z} $, $ n\in \mathbb{Z} $ and $ \neg (n\leq m) $

shows $ m\leq n $, $ ( - n) \leq ( - m) $, $ m\neq n $

lemma (in real1) real_ord_antisym:

assumes $ a\leq b $, $ b\leq a $

shows $ a=b $

lemma (in real1) real_ord_transitive:

assumes $ a\leq b $, $ b\leq c $

shows $ a\leq c $

lemma (in real1) Real_ZF_1_4_L6:

assumes $ k \in int $, $ m \in int $ and $ m^R \leq k^R $

shows $ m\leq k $

lemma Order_ZF_3_L10:

assumes $ \forall a\in A.\ \langle a,u\rangle \in r $

shows $ \text{IsBoundedAbove}(A,r) $

lemma (in real1) Real_ZF_1_4_L3:

assumes $ a\in \mathbb{R} $

shows $ \{m \in int.\ m^R \leq a\} \neq 0 $

theorem (in int0) int_bounded_above_has_max:

assumes $ \text{IsBoundedAbove}(A,IntegerOrder) $ and $ A\neq 0 $

shows $ \text{HasAmaximum}(IntegerOrder,A) $, $ \text{Maximum}(IntegerOrder,A) \in A $, $ \text{Maximum}(IntegerOrder,A) \in \mathbb{Z} $, $ \forall x\in A.\ x \leq \text{Maximum}(IntegerOrder,A) $

lemma (in real1) Real_ZF_1_2_L15:

assumes $ a\leq b $

shows $ a\in \mathbb{R} $, $ b\in \mathbb{R} $

lemma (in real1) Real_ZF_1_4_L7:

assumes $ a\in \mathbb{R} $

shows $ \text{IsBoundedAbove}(\{m \in int.\ m^R \leq a\},IntegerOrder) $, $ \{m \in int.\ m^R \leq a\} \neq 0 $, $ \lfloor a\rfloor \in int $, $ \lfloor a\rfloor ^R \leq a $

lemma (in int1) Int_ZF_2_5_L7: shows $ 1 ^S = id(\mathbb{Z} ) $, $ 0 ^S \in \text{FinRangeFunctions}(\mathbb{Z} ,\mathbb{Z} ) $

lemma (in real1) real_zero_cl_bounded_map:

assumes $ f \in BoundedIntMaps $

shows $ [f] = 0 $

lemma (in int0) int_zero_one_are_int: shows $ 0 \in \mathbb{Z} $, $ 1 \in \mathbb{Z} $

lemma (in real1) int_0_1_are_real_zero_one: shows $ 0 _Z^R = 0 $, $ 1 _Z^R = 1 $

lemma (in real1) real_int_is_real:

assumes $ m \in int $

shows $ m^R \in \mathbb{R} $

lemma (in real1) Real_ZF_1_3_L1:

assumes $ a \in \mathbb{R} _+ $

shows $ a^{-1} \in \mathbb{R} _+ $, $ a^{-1} \in \mathbb{R} $

lemma (in real1) Arthan_Lemma14i:

assumes $ a\in \mathbb{R} $

shows $ \exists n\in \mathbb{Z} _+.\ a \lt n^R $

lemma (in int0) pos_int_closed_mul_unfold:

assumes $ a\in \mathbb{Z} _+ $, $ b\in \mathbb{Z} _+ $

shows $ a\cdot b \in \mathbb{Z} _+ $

lemma (in real0) Real_ZF_1_L6A:

assumes $ a\in \mathbb{R} $, $ b\in \mathbb{R} $, $ c\in \mathbb{R} $

shows $ a\cdot (b\cdot c) = (a\cdot b)\cdot c $

lemma (in real1) Real_ZF_1_4_L1C:

assumes $ m \in int $, $ k \in int $

shows $ m^R \cdot k^R = (m\cdot k)^R $

lemma (in real1) int_pos_is_real_pos:

assumes $ p\in \mathbb{Z} _+ $

shows $ p^R \in \mathbb{R} $, $ 0 \leq p^R $, $ p^R \in \mathbb{R} _+ $

lemma (in real1) Real_ZF_1_3_L2:

assumes $ a \in \mathbb{R} _+ $ and $ a^{-1} \lt b $

shows $ 1 \lt b\cdot a $

lemma (in real1) Real_ZF_1_2_L25:

assumes $ b \in \mathbb{R} _+ $ and $ a\leq b $ and $ 1 \lt c $

shows $ a \lt b\cdot c $

lemma (in real1) Real_ZF_1_4_L8:

assumes $ m \in int $ and $ m^R \leq a $

shows $ m \leq \lfloor a\rfloor $

Definition of IsBoundedAbove: $ \text{IsBoundedAbove}(A,r) \equiv ( A=0 \vee (\exists u.\ \forall x\in A.\ \langle x,u\rangle \in r)) $

lemma (in real1) Real_ZF_1_2_L14:

assumes $ a\leq b $ and $ 0 \leq c $

shows $ a\cdot c \leq b\cdot c $, $ c\cdot a \leq c\cdot b $

lemma (in real1) Real_ZF_1_4_L9:

assumes $ a\leq b $

shows $ \lfloor a\rfloor \leq \lfloor b\rfloor $

lemma (in real1) Real_ZF_1_4_L10:

assumes $ \text{IsBoundedAbove}(S,OrderOnReals) $, $ S\neq 0 $ and $ p\in \mathbb{Z} _+ $

shows $ \text{IsBoundedAbove}(\{\lfloor p^R\cdot x\rfloor .\ x\in S\},IntegerOrder) $, $ \Gamma (S,p) \in \{\lfloor p^R\cdot x\rfloor .\ x\in S\} $, $ \Gamma (S,p) \in int $

lemma ZF_fun_from_total:

assumes $ \forall x\in X.\ b(x) \in Y $

shows $ \{\langle x,b(x)\rangle .\ x\in X\} : X\rightarrow Y $

lemma ZF_fun_from_tot_val:

assumes $ f:X\rightarrow Y $, $ x\in X $ and $ f = \{\langle x,b(x)\rangle .\ x\in X\} $

shows $ f(x) = b(x) $ and $ b(x)\in Y $

lemma (in int0) Int_ZF_2_L4: shows $ \text{antisym}(IntegerOrder) $

lemma (in real1) real_ord_refl:

assumes $ a\in \mathbb{R} $

shows $ a\leq a $

lemma Order_ZF_4_L14:

assumes $ \text{antisym}(r) $ and $ M \in A $ and $ \forall a\in A.\ \langle a,M\rangle \in r $

shows $ \text{Maximum}(r,A) = M $

lemma (in real1) Real_ZF_1_4_L14:

assumes $ m \in int $

shows $ \lfloor m^R\rfloor = m $

lemma (in int0) int_two_three_are_int: shows $ 2 \in \mathbb{Z} $, $ 3 \in \mathbb{Z} $

lemma (in real1) int_two_is_real_two: shows $ 2 _Z^R = 2 $

lemma (in int0) Int_ZF_1_1_L5:

assumes $ a\in \mathbb{Z} $, $ b\in \mathbb{Z} $

shows $ a + b \in \mathbb{Z} $, $ a - b \in \mathbb{Z} $, $ a\cdot b \in \mathbb{Z} $, $ a + b = b + a $, $ a\cdot b = b\cdot a $, $ ( - b) - a = ( - a) - b $, $ ( - (a + b)) = ( - a) - b $, $ ( - (a - b)) = (( - a) + b) $, $ ( - a)\cdot b = - (a\cdot b) $, $ a\cdot ( - b) = - (a\cdot b) $, $ ( - a)\cdot ( - b) = a\cdot b $

lemma (in real1) add_num_to_ineq:

assumes $ a\leq b $ and $ c\in \mathbb{R} $

shows $ a + c \leq b + c $

lemma (in real1) Real_ZF_1_2_L19:

assumes $ a\in \mathbb{R} $, $ b\in \mathbb{R} $ and $ c \leq a + b $

shows $ c - b \leq a $

lemma (in real1) Real_ZF_1_4_L1B:

assumes $ m \in int $, $ k \in int $

shows $ m^R - k^R = (m - k)^R $

lemma (in int0) Int_ZF_2_L9C:

assumes $ i\in \mathbb{Z} $, $ m\in \mathbb{Z} $ and $ i - m \leq k $

shows $ i \leq k + m $

lemma (in real1) Real_ZF_1_4_L15:

assumes $ x\in \mathbb{R} $ and $ p \in int $

shows $ \lfloor x + p^R\rfloor = \lfloor x\rfloor + p $

lemma (in real0) Real_ZF_1_L6:

assumes $ a\in \mathbb{R} $, $ b\in \mathbb{R} $

shows $ a + b \in \mathbb{R} $, $ a - b \in \mathbb{R} $, $ a\cdot b \in \mathbb{R} $, $ a + b = b + a $, $ ( - a)\cdot b = - (a\cdot b) $, $ a\cdot ( - b) = - (a\cdot b) $

lemma (in real1) Real_ZF_1_2_L21:

assumes $ a\in \mathbb{R} $, $ b\in \mathbb{R} $ and $ c \leq a - b $

shows $ c + b \leq a $

lemma (in real1) Real_ZF_1_4_L17:

assumes $ m \in int $, $ n \in int $

shows $ \lfloor (m^R) + n^R\rfloor = m + n $

lemma (in int0) Int_ZF_1_2_L3AA:

assumes $ a\in \mathbb{Z} $

shows $ a - 1 \leq a $, $ a - 1 \neq a $, $ \neg (a\leq a - 1 ) $, $ \neg (a + 1 \leq a) $, $ \neg (1 + a \leq a) $

lemma (in real1) Real_ZF_1_2_L20:

assumes $ a\in \mathbb{R} $, $ b\in \mathbb{R} $ and $ \neg (a\leq b) $

shows $ b \lt a $

lemma (in real1) Real_ZF_1_2_L26:

assumes $ a\in \mathbb{R} $, $ b\in \mathbb{R} $ and $ a - b \lt c $

shows $ a \lt c + b $

lemma (in real1) Real_ZF_1_4_L17A:

assumes $ a\in \mathbb{R} $

shows $ 1 + \lfloor a\rfloor ^R = (1 _Z + \lfloor a\rfloor )^R $

lemma (in real1) Real_ZF_1_3_L3:

assumes $ a \lt b $

shows $ (b - a)^{-1} \in \mathbb{R} _+ $

lemma (in real1) Real_ZF_1_4_L17B:

assumes $ a\in \mathbb{R} $

shows $ a - \lfloor a\rfloor ^R \lt 1 $, $ a \lt (1 _Z + \lfloor a\rfloor )^R $

lemma (in real1) real_ord_transl_inv:

assumes $ a\leq b $ and $ c\in \mathbb{R} $

shows $ c + a \leq c + b $

lemma (in real1) Real_ZF_1_3_L5:

assumes $ a \lt b $ and $ (b - a)^{-1} \lt c $

shows $ 1 + a\cdot c \lt b\cdot c $

lemma (in real1) Real_ZF_1_2_L16:

assumes $ a\leq b $

shows $ 0 \leq b - a $

lemma (in real1) Real_ZF_1_2_L17:

assumes $ 0 \leq a $, $ 0 \leq b $

shows $ 0 \leq a + b $

lemma (in real1) Real_ZF_1_2_L18:

assumes $ a\leq b $, $ c\leq d $

shows $ a + c \leq b + d $

lemma (in real0) Real_ZF_1_L7A:

assumes $ a\in \mathbb{R} $, $ b\in \mathbb{R} $, $ c\in \mathbb{R} $, $ d\in \mathbb{R} $

shows $ a - b + (c - d) = a + c - b - d $

lemma (in real1) floor_01_is_zero_one: shows $ \lfloor 0 \rfloor = 0 _Z $, $ \lfloor 1 \rfloor = 1 _Z $

lemma (in real1) floor_2_is_two: shows $ \lfloor 2 \rfloor = 2 _Z $

lemma (in real1) Real_ZF_1_4_L16:

assumes $ x\in \mathbb{R} $ and $ p \in int $

shows $ \lfloor x - p^R\rfloor = \lfloor x\rfloor - p $

lemma (in int0) Int_ZF_2_L16:

assumes $ 0 \leq m $

shows $ m\in \mathbb{Z} ^+ $ and $ abs(m) = m $

lemma (in real1) Real_ZF_1_4_L11:

assumes $ \text{IsBoundedAbove}(S,OrderOnReals) $ and $ x\in S $ and $ p\in \mathbb{Z} _+ $

shows $ \lfloor p^R\cdot x\rfloor \leq \Gamma (S,p) $

lemma (in int0) Int_ZF_2_L3:

assumes $ m \leq n $, $ n \leq m $

shows $ m=n $

lemma (in int0) pos_int_closed_add_unfolded:

assumes $ a\in \mathbb{Z} _+ $, $ b\in \mathbb{Z} _+ $

shows $ a + b \in \mathbb{Z} _+ $

lemma (in real1) Real_ZF_1_2_L23:

assumes $ \text{IsBoundedAbove}(A,OrderOnReals) $

shows $ A \subseteq \mathbb{R} $

lemma (in real1) Real_ZF_1_2_L24:

assumes $ a\in \mathbb{R} $, $ b\in \mathbb{R} $, $ c\in \mathbb{R} $

lemma (in real1) Real_ZF_1_4_L20:

assumes $ \text{IsBoundedAbove}(S,OrderOnReals) $, $ S\neq 0 $ and $ n\in \mathbb{Z} _+ $, $ x\in S $ and $ \Gamma (S,n) = \lfloor n^R\cdot x\rfloor $ and $ y\in S $, $ x\leq y $

shows $ \Gamma (S,n) = \lfloor n^R\cdot y\rfloor $

lemma (in real0) Real_ZF_1_L7:

assumes $ a\in \mathbb{R} $, $ b\in \mathbb{R} $, $ c\in \mathbb{R} $

shows $ a\cdot (b + c) = a\cdot b + a\cdot c $, $ (b + c)\cdot a = b\cdot a + c\cdot a $, $ a\cdot (b - c) = a\cdot b - a\cdot c $, $ (b - c)\cdot a = b\cdot a - c\cdot a $

lemma (in real1) Real_ZF_1_4_L18:

assumes $ x\in \mathbb{R} $, $ y\in \mathbb{R} $

shows $ abs(\lfloor x + y\rfloor - \lfloor x\rfloor - \lfloor y\rfloor ) \leq 2 _Z $

lemma (in int1) Int_ZF_2_1_L24:

assumes $ f:\mathbb{Z} _+\rightarrow \mathbb{Z} $ and $ \forall a\in \mathbb{Z} _+.\ \forall b\in \mathbb{Z} _+.\ abs(\delta (f,a,b)) \leq L $

shows $ \text{OddExtension}(\mathbb{Z} ,IntegerAddition,IntegerOrder,f) \in \mathcal{S} $

lemma (in real1) Real_ZF_1_4_L12:

assumes $ \text{IsBoundedAbove}(S,OrderOnReals) $, $ S\neq 0 $ and $ g = \{\langle p,\Gamma (S,p)\rangle .\ p\in \mathbb{Z} _+\} $

shows $ g : \mathbb{Z} _+\rightarrow int $, $ \forall n\in \mathbb{Z} _+.\ g(n) = \Gamma (S,n) $

lemma (in real1) Real_ZF_1_4_L21:

assumes $ \text{IsBoundedAbove}(S,OrderOnReals) $, $ S\neq 0 $ and $ m\in \mathbb{Z} _+ $, $ n\in \mathbb{Z} _+ $

shows $ abs(\Gamma (S,m + n) - \Gamma (S,m) - \Gamma (S,n)) \leq 2 _Z $

lemma (in real1) Real_ZF_1_4_L21A:

assumes $ f:\mathbb{Z} _+\rightarrow int $, $ \forall a\in \mathbb{Z} _+.\ \forall b\in \mathbb{Z} _+.\ abs(\delta (f,a,b)) \leq L $

shows $ \text{OddExtension}(int,IntegerAddition,IntegerOrder,f) \in \mathcal{S} $

lemma (in int1) Int_ZF_2_1_L11:

assumes $ s\in \mathcal{S} $, $ r\in \mathcal{S} $

shows $ s\circ r \in \mathcal{S} $

lemma (in int1) Int_ZF_2_5_L8:

assumes $ f \in \mathcal{S} $ and $ N \in \mathbb{Z} $, $ M \in \mathbb{Z} $ and $ \forall n\in \mathbb{Z} _+.\ M\cdot n \leq f(N\cdot n) $

shows $ M^S \sim f\circ (N^S) \vee (f\circ (N^S)) + ( - (M^S)) \in \mathcal{S} _+ $

lemma (in int1) Int_ZF_2_5_L9:

assumes $ f \in \mathcal{S} $ and $ N \in \mathbb{Z} $, $ M \in \mathbb{Z} $ and $ \forall n\in \mathbb{Z} _+.\ f(N\cdot n) \leq M\cdot n $

shows $ f\circ (N^S) \sim (M^S) \vee (M^S) + ( - (f\circ (N^S))) \in \mathcal{S} _+ $

lemma (in real1) Real_ZF_1_3_L4A:

assumes $ b\in \mathbb{R} $, $ c\in \mathbb{R} _+ $ and $ a \lt b\cdot c $

shows $ a\cdot c^{-1} \lt b $

lemma (in real1) Real_ZF_1_3_L7:

assumes $ a \lt b $ and $ c\in \mathbb{R} _+ $

shows $ a\cdot c \lt b\cdot c $, $ c\cdot a \lt c\cdot b $, $ a\cdot c^{-1} \lt b\cdot c^{-1} $

lemma (in real1) int_order_transitive:

assumes $ a\leq b $, $ b\leq c $

shows $ a\leq c $

lemma (in real1) Real_ZF_1_3_L8:

assumes $ a\in \mathbb{R} $, $ b\in \mathbb{R} $, $ b\neq 0 $, $ c\in \mathbb{R} $

shows $ a\cdot b\cdot (c\cdot b^{-1}) = a\cdot c $

lemma (in real1) Real_ZF_1_4_L14A:

assumes $ m \in int $, $ k \in int $

shows $ \lfloor m^R\cdot k^R\rfloor = m\cdot k $

lemma (in int0) Int_ZF_1_5_L11:

assumes $ f : \mathbb{Z} _+\rightarrow \mathbb{Z} $ and $ a \in \mathbb{Z} _+ $ and $ g = \text{OddExtension}(\mathbb{Z} ,IntegerAddition,IntegerOrder,f) $

shows $ g(a) = f(a) $

lemma (in real1) Real_ZF_1_2_L27:

assumes $ A\subseteq \mathbb{R} $ and $ \neg \text{HasAmaximum}(OrderOnReals,A) $ and $ x\in A $

shows $ \exists y\in A.\ x \lt y $

lemma (in real1) Arthan_Lemma14iii:

assumes $ x \lt y $

shows $ \exists M\in int.\ \exists N\in \mathbb{Z} _+.\ x\cdot N^R \lt M^R \wedge M^R \lt y\cdot N^R $

lemma (in real1) Real_ZF_1_3_L4:

assumes $ a\in \mathbb{R} $, $ b\in \mathbb{R} _+ $ and $ a\cdot b \lt c $

shows $ a \lt c\cdot b^{-1} $

lemma (in real1) Real_ZF_1_4_L22:

assumes $ \text{IsBoundedAbove}(S,OrderOnReals) $, $ S\neq 0 $ and $ g = \{\langle p,\Gamma (S,p)\rangle .\ p\in \mathbb{Z} _+\} $

shows $ \text{OddExtension}(int,IntegerAddition,IntegerOrder,g) \in \mathcal{S} $

lemma (in real1) Real_ZF_1_4_L24:

assumes $ \text{IsBoundedAbove}(S,OrderOnReals) $ and $ x \lt y $, $ y\in S $ and $ N \in \mathbb{Z} _+ $, $ M \in int $ and $ M^R \lt y\cdot N^R $ and $ p \in \mathbb{Z} _+ $

shows $ p\cdot M \leq \Gamma (S,p\cdot N) $

lemma (in real1) Real_ZF_1_4_L24A:

assumes $ \text{IsBoundedAbove}(S,OrderOnReals) $, $ S\neq 0 $ and $ p \in \mathbb{Z} _+ $ and $ h = \text{OddExtension}(int,IntegerAddition,IntegerOrder,\{\langle p,\Gamma (S,p)\rangle .\ p\in \mathbb{Z} _+\}) $

shows $ h(p) = \Gamma (S,p) $

lemma (in real1) Real_ZF_1_4_L23:

assumes $ f \in \mathcal{S} $ and $ N \in int $, $ M \in int $ and $ \forall n\in \mathbb{Z} _+.\ M\cdot n \leq f(N\cdot n) $

shows $ M^R \leq [f]\cdot (N^R) $

lemma (in real1) Real_ZF_1_3_L4B:

assumes $ b\in \mathbb{R} $, $ c\in \mathbb{R} _+ $ and $ a \leq b\cdot c $

shows $ a\cdot c^{-1} \leq b $

lemma (in real1) Real_ZF_1_2_L14A:

assumes $ a\leq b $ and $ c\in \mathbb{R} _+ $

shows $ c\cdot a \leq c\cdot b $

lemma (in real1) Real_ZF_1_1_L9:

assumes $ a\in \mathbb{R} $, $ b\in \mathbb{R} $, $ c\in \mathbb{R} $

shows $ a\cdot (b\cdot c) = a\cdot c\cdot b $

lemma (in real1) Real_ZF_1_2_L28:

assumes $ a\in \mathbb{R} $, $ b\in \mathbb{R} $ and $ \neg (a\leq b) $

shows $ b \lt a $

lemma (in real1) Real_ZF_1_4_L27:

shows $ \exists x\in S.\ h(p) = \lfloor p^R\cdot x\rfloor $

lemma (in real1) Real_ZF_1_4_L26:

assumes $ \text{IsBoundedAbove}(S,OrderOnReals) $ and $ x\leq y $, $ x\in S $ and $ N \in \mathbb{Z} _+ $, $ M \in int $ and $ y\cdot N^R \lt M^R $ and $ p \in \mathbb{Z} _+ $

shows $ \lfloor (N\cdot p)^R\cdot x\rfloor \leq M\cdot p $

lemma (in real1) Real_ZF_1_4_L23A:

assumes $ f \in \mathcal{S} $ and $ N \in int $, $ M \in int $ and $ \forall n\in \mathbb{Z} _+.\ f(N\cdot n) \leq M\cdot n $

shows $ [f]\cdot (N^R) \leq M^R $

lemma (in real1) Real_ZF_1_3_L4C:

assumes $ a\in \mathbb{R} $, $ b\in \mathbb{R} _+ $ and $ a\cdot b \leq c $

shows $ a \leq c\cdot b^{-1} $

lemma (in real1) Real_ZF_1_2_L29:

assumes $ a \lt b $

shows $ \neg (b\leq a) $

Definition of IsPartOrder: $ \text{IsPartOrder}(X,r) \equiv \text{refl}(X,r) \wedge \text{antisym}(r) \wedge \text{trans}(r) $

lemma Order_ZF_5_L6:

assumes $ \text{antisym}(r) $ and $ A\neq 0 $ and $ \text{HasAmaximum}(r,A) $

shows $ \text{HasAminimum}(r,\bigcap a\in A.\ r\{a\}) $, $ \text{Maximum}(r,A) = \text{Supremum}(r,A) $

lemma (in real1) Real_ZF_1_4_L25:

assumes $ \text{IsBoundedAbove}(S,OrderOnReals) $ and $ \neg \text{HasAmaximum}(OrderOnReals,S) $ and $ x\in S $ and $ h = \text{OddExtension}(int,IntegerAddition,IntegerOrder,\{\langle p,\Gamma (S,p)\rangle .\ p\in \mathbb{Z} _+\}) $

shows $ x \leq [h] $

lemma (in real1) Real_ZF_1_4_L28:

assumes $ \text{IsBoundedAbove}(S,OrderOnReals) $, $ S\neq 0 $ and $ \forall x\in S.\ x\leq y $ and $ h = \text{OddExtension}(int,IntegerAddition,IntegerOrder,\{\langle p,\Gamma (S,p)\rangle .\ p\in \mathbb{Z} _+\}) $

shows $ [h] \leq y $

lemma Order_ZF_5_L5:

assumes $ \text{antisym}(r) $ and $ A\neq 0 $ and $ \forall x\in A.\ \langle x,z\rangle \in r $ and $ \forall y.\ (\forall x\in A.\ \langle x,y\rangle \in r) \longrightarrow \langle z,y\rangle \in r $

shows $ \text{HasAminimum}(r,\bigcap a\in A.\ r\{a\}) $, $ z = \text{Supremum}(r,A) $

lemma (in real1) real_order_complete:

assumes $ \text{IsBoundedAbove}(S,OrderOnReals) $, $ S\neq 0 $

shows $ \text{HasAminimum}(OrderOnReals,\bigcap a\in S.\ OrderOnReals\{a\}) $

Definition of IsComplete: $ r \text{ is complete } \equiv $ $ \forall A.\ \text{IsBoundedAbove}(A,r) \wedge A\neq 0 \longrightarrow \text{HasAminimum}(r,\bigcap a\in A.\ r\{a\}) $

Definition of IsAmodelOfReals: $ \text{IsAmodelOfReals}(K,A,M,r) \equiv \text{IsAnOrdField}(K,A,M,r) \wedge (r \text{ is complete }) $