IsarMathLib

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

theory Int_ZF_3 imports Int_ZF_2
begin

This theory is a continuation of Int_ZF_2. We consider here the properties of slopes (almost homomorphisms on integers) that allow to define the order relation and multiplicative inverse on real numbers. We also prove theorems that allow to show completeness of the order relation of real numbers we define in Real_ZF.

Positive slopes

This section provides background material for defining the order relation on real numbers.

Positive slopes are functions (of course.)

lemma (in int1) Int_ZF_2_3_L1:

assumes A1: \( f\in \mathcal{S} _+ \)

shows \( f:\mathbb{Z} \rightarrow \mathbb{Z} \) using assms, AlmostHoms_def, PositiveSet_def

A small technical lemma to simplify the proof of the next theorem.

lemma (in int1) Int_ZF_2_3_L1A:

assumes A1: \( f\in \mathcal{S} _+ \) and A2: \( \exists n \in f(\mathbb{Z} _+) \cap \mathbb{Z} _+.\ a\leq n \)

shows \( \exists M\in \mathbb{Z} _+.\ a \leq f(M) \)proof
from A1 have \( f:\mathbb{Z} \rightarrow \mathbb{Z} \), \( \mathbb{Z} _+ \subseteq \mathbb{Z} \) using AlmostHoms_def, PositiveSet_def
with A2 show \( thesis \) using func_imagedef
qed

The next lemma is Lemma 3 in the Arthan's paper.

lemma (in int1) Arthan_Lem_3:

assumes A1: \( f\in \mathcal{S} _+ \) and A2: \( D \in \mathbb{Z} _+ \)

shows \( \exists M\in \mathbb{Z} _+.\ \forall m\in \mathbb{Z} _+.\ (m + 1 )\cdot D \leq f(m\cdot M) \)proof
let \( E = \text{ max}\delta (f) + D \)
let \( A = f(\mathbb{Z} _+) \cap \mathbb{Z} _+ \)
from A1, A2 have I: \( D\leq E \) using Int_ZF_1_5_L3, Int_ZF_2_1_L8, Int_ZF_2_L1A, Int_ZF_2_L15D
from A1, A2 have \( A \subseteq \mathbb{Z} _+ \), \( A \notin Fin(\mathbb{Z} ) \), \( 2 \cdot E \in \mathbb{Z} \) using int_two_three_are_int, Int_ZF_2_1_L8, PositiveSet_def, Int_ZF_1_1_L5
with A1 have \( \exists M\in \mathbb{Z} _+.\ 2 \cdot E \leq f(M) \) using Int_ZF_1_5_L2A, Int_ZF_2_3_L1A
then obtain \( M \) where II: \( M\in \mathbb{Z} _+ \) and III: \( 2 \cdot E \leq f(M) \)
{
fix \( m \)
assume \( m\in \mathbb{Z} _+ \)
then have A4: \( 1 \leq m \) using Int_ZF_1_5_L3
moreover
from II, III have \( (1 + 1 ) \cdot E \leq f(1 \cdot M) \) using PositiveSet_def, Int_ZF_1_1_L4
moreover
have \( \forall k.\ \) \( 1 \leq k \wedge (k + 1 )\cdot E \leq f(k\cdot M) \longrightarrow (k + 1 + 1 )\cdot E \leq f((k + 1 )\cdot M) \)proof
{
fix \( k \)
assume A5: \( 1 \leq k \) and A6: \( (k + 1 )\cdot E \leq f(k\cdot M) \)
with A1, A2, II have T: \( k\in \mathbb{Z} \), \( M\in \mathbb{Z} \), \( k + 1 \in \mathbb{Z} \), \( E\in \mathbb{Z} \), \( (k + 1 )\cdot E \in \mathbb{Z} \), \( 2 \cdot E \in \mathbb{Z} \) using Int_ZF_2_L1A, PositiveSet_def, int_zero_one_are_int, Int_ZF_1_1_L5, Int_ZF_2_1_L8
from A1, A2, A5, II have \( \delta (f,k\cdot M,M) \in \mathbb{Z} \), \( abs(\delta (f,k\cdot M,M)) \leq \text{ max}\delta (f) \), \( 0 \leq D \) using Int_ZF_2_L1A, PositiveSet_def, Int_ZF_1_1_L5, Int_ZF_2_1_L7, Int_ZF_2_L16C
with III, A6 have \( (k + 1 )\cdot E + ( 2 \cdot E - E) \leq f(k\cdot M) + (f(M) + \delta (f,k\cdot M,M)) \) using Int_ZF_1_3_L19A, int_ineq_add_sides
with A1, T have \( (k + 1 + 1 )\cdot E \leq f((k + 1 )\cdot M) \) using Int_ZF_1_1_L1, int_zero_one_are_int, Int_ZF_1_1_L4, Int_ZF_1_2_L11, Int_ZF_2_1_L13
}
then show \( thesis \)
qed
ultimately have \( (m + 1 )\cdot E \leq f(m\cdot M) \) by (rule Induction_on_int )
with A4, I have \( (m + 1 )\cdot D \leq f(m\cdot M) \) using Int_ZF_1_3_L13A
}
then have \( \forall m\in \mathbb{Z} _+.\ (m + 1 )\cdot D \leq f(m\cdot M) \)
with II show \( thesis \)
qed

A special case of Arthan_Lem_3 when \(D=1\).

corollary (in int1) Arthan_L_3_spec:

assumes A1: \( f \in \mathcal{S} _+ \)

shows \( \exists M\in \mathbb{Z} _+.\ \forall n\in \mathbb{Z} _+.\ n + 1 \leq f(n\cdot M) \)proof
have \( \forall n\in \mathbb{Z} _+.\ n + 1 \in \mathbb{Z} \) using PositiveSet_def, int_zero_one_are_int, Int_ZF_1_1_L5
then have \( \forall n\in \mathbb{Z} _+.\ (n + 1 )\cdot 1 = n + 1 \) using Int_ZF_1_1_L4
moreover
from A1 have \( \exists M\in \mathbb{Z} _+.\ \forall n\in \mathbb{Z} _+.\ (n + 1 )\cdot 1 \leq f(n\cdot M) \) using int_one_two_are_pos, Arthan_Lem_3
ultimately show \( thesis \)
qed

We know from Group_ZF_3.thy that finite range functions are almost homomorphisms. Besides reminding that fact for slopes the next lemma shows that finite range functions do not belong to \( \mathcal{S} _+ \). This is important, because the projection of the set of finite range functions defines zero in the real number construction in Real_ZF_x.thy series, while the projection of \( \mathcal{S} _+ \) becomes the set of (strictly) positive reals. We don't want zero to be positive, do we? The next lemma is a part of Lemma 5 in the Arthan's paper \cite{Arthan2004}.

lemma (in int1) Int_ZF_2_3_L1B:

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

shows \( f\in \mathcal{S} \), \( f \notin \mathcal{S} _+ \)proof
from A1 show \( f\in \mathcal{S} \) using Int_ZF_2_1_L1, Group_ZF_3_3_L1
have \( \mathbb{Z} _+ \subseteq \mathbb{Z} \) using PositiveSet_def
with A1 have \( f(\mathbb{Z} _+) \in Fin(\mathbb{Z} ) \) using Finite1_L21
then have \( f(\mathbb{Z} _+) \cap \mathbb{Z} _+ \in Fin(\mathbb{Z} ) \) using Fin_subset_lemma
thus \( f \notin \mathcal{S} _+ \)
qed

We want to show that if \(f\) is a slope and neither \(f\) nor \(-f\) are in \( \mathcal{S} _+ \), then \(f\) is bounded. The next lemma is the first step towards that goal and shows that if slope is not in \( \mathcal{S} _+ \) then \(f(\)\( \mathbb{Z} _+ \)\()\) is bounded above.

lemma (in int1) Int_ZF_2_3_L2:

assumes A1: \( f\in \mathcal{S} \) and A2: \( f \notin \mathcal{S} _+ \)

shows \( \text{IsBoundedAbove}(f(\mathbb{Z} _+), IntegerOrder) \)proof
from A1 have \( f:\mathbb{Z} \rightarrow \mathbb{Z} \) using AlmostHoms_def
then have \( f(\mathbb{Z} _+) \subseteq \mathbb{Z} \) using func1_1_L6
moreover
from A1, A2 have \( f(\mathbb{Z} _+) \cap \mathbb{Z} _+ \in Fin(\mathbb{Z} ) \)
ultimately show \( thesis \) using Int_ZF_2_T1, OrderedGroup_ZF_2_L4
qed

If \(f\) is a slope and \(-f\notin\) \( \mathcal{S} _+ \), then \(f(\)\( \mathbb{Z} _+ \)\()\) is bounded below.

lemma (in int1) Int_ZF_2_3_L3:

assumes A1: \( f\in \mathcal{S} \) and A2: \( - f \notin \mathcal{S} _+ \)

shows \( \text{IsBoundedBelow}(f(\mathbb{Z} _+), IntegerOrder) \)proof
from A1 have T: \( f:\mathbb{Z} \rightarrow \mathbb{Z} \) using AlmostHoms_def
then have \( (-(f(\mathbb{Z} _+))) = ( - f)(\mathbb{Z} _+) \) using Int_ZF_1_T2, group0_2_T2, PositiveSet_def, func1_1_L15C
with A1, A2, T show \( \text{IsBoundedBelow}(f(\mathbb{Z} _+), IntegerOrder) \) using Int_ZF_2_1_L12, Int_ZF_2_3_L2, PositiveSet_def, func1_1_L6, Int_ZF_2_T1, OrderedGroup_ZF_2_L5
qed

A slope that is bounded on \( \mathbb{Z} _+ \) is bounded everywhere.

lemma (in int1) Int_ZF_2_3_L4:

assumes A1: \( f\in \mathcal{S} \) and A2: \( m\in \mathbb{Z} \) and A3: \( \forall n\in \mathbb{Z} _+.\ abs(f(n)) \leq L \)

shows \( abs(f(m)) \leq 2 \cdot \text{ max}\delta (f) + L \)proof
from A1, A3 have \( 0 \leq abs(f(1 )) \), \( abs(f(1 )) \leq L \) using int_zero_one_are_int, Int_ZF_2_1_L2B, int_abs_nonneg, int_one_two_are_pos
then have II: \( 0 \leq L \) by (rule Int_order_transitive )
note A2
moreover
have \( abs(f( 0 )) \leq 2 \cdot \text{ max}\delta (f) + L \)proof
from A1 have \( abs(f( 0 )) \leq \text{ max}\delta (f) \), \( 0 \leq \text{ max}\delta (f) \) and T: \( \text{ max}\delta (f) \in \mathbb{Z} \) using Int_ZF_2_1_L8
with II have \( abs(f( 0 )) \leq \text{ max}\delta (f) + \text{ max}\delta (f) + L \) using Int_ZF_2_L15F
with T show \( thesis \) using Int_ZF_1_1_L4
qed
moreover
from A1, A3, II have \( \forall n\in \mathbb{Z} _+.\ abs(f(n)) \leq 2 \cdot \text{ max}\delta (f) + L \) using Int_ZF_2_1_L8, Int_ZF_1_3_L5A, Int_ZF_2_L15F
moreover
have \( \forall n\in \mathbb{Z} _+.\ abs(f( - n)) \leq 2 \cdot \text{ max}\delta (f) + L \)proof
fix \( n \)
assume \( n\in \mathbb{Z} _+ \)
with A1, A3 have \( 2 \cdot \text{ max}\delta (f) \in \mathbb{Z} \), \( abs(f( - n)) \leq 2 \cdot \text{ max}\delta (f) + abs(f(n)) \), \( abs(f(n)) \leq L \) using int_two_three_are_int, Int_ZF_2_1_L8, Int_ZF_1_1_L5, PositiveSet_def, Int_ZF_2_1_L14
then show \( abs(f( - n)) \leq 2 \cdot \text{ max}\delta (f) + L \) using Int_ZF_2_L15A
qed
ultimately show \( thesis \) by (rule Int_ZF_2_L19B )
qed

A slope whose image of the set of positive integers is bounded is a finite range function.

lemma (in int1) Int_ZF_2_3_L4A:

assumes A1: \( f\in \mathcal{S} \) and A2: \( \text{IsBounded}(f(\mathbb{Z} _+), IntegerOrder) \)

shows \( f \in \text{FinRangeFunctions}(\mathbb{Z} ,\mathbb{Z} ) \)proof
have T1: \( \mathbb{Z} _+ \subseteq \mathbb{Z} \) using PositiveSet_def
from A1 have T2: \( f:\mathbb{Z} \rightarrow \mathbb{Z} \) using AlmostHoms_def
from A2 obtain \( L \) where \( \forall a\in f(\mathbb{Z} _+).\ abs(a) \leq L \) using Int_ZF_1_3_L20A
with T2, T1 have \( \forall n\in \mathbb{Z} _+.\ abs(f(n)) \leq L \) by (rule func1_1_L15B )
with A1 have \( \forall m\in \mathbb{Z} .\ abs(f(m)) \leq 2 \cdot \text{ max}\delta (f) + L \) using Int_ZF_2_3_L4
with T2 have \( f(\mathbb{Z} ) \in Fin(\mathbb{Z} ) \) by (rule Int_ZF_1_3_L20C )
with T2 show \( f \in \text{FinRangeFunctions}(\mathbb{Z} ,\mathbb{Z} ) \) using FinRangeFunctions_def
qed

A slope whose image of the set of positive integers is bounded below is a finite range function or a positive slope.

lemma (in int1) Int_ZF_2_3_L4B:

assumes \( f\in \mathcal{S} \) and \( \text{IsBoundedBelow}(f(\mathbb{Z} _+), IntegerOrder) \)

shows \( f \in \text{FinRangeFunctions}(\mathbb{Z} ,\mathbb{Z} ) \vee f\in \mathcal{S} _+ \) using assms, Int_ZF_2_3_L2, IsBounded_def, Int_ZF_2_3_L4A

If one slope is not greater then another on positive integers, then they are almost equal or the difference is a positive slope.

lemma (in int1) Int_ZF_2_3_L4C:

assumes A1: \( f\in \mathcal{S} \), \( g\in \mathcal{S} \) and A2: \( \forall n\in \mathbb{Z} _+.\ f(n) \leq g(n) \)

shows \( f\sim g \vee g + ( - f) \in \mathcal{S} _+ \)proof
let \( h = g + ( - f) \)
from A1 have \( ( - f) \in \mathcal{S} \) using Int_ZF_2_1_L12
with A1 have I: \( h \in \mathcal{S} \) using Int_ZF_2_1_L12C
moreover
have \( \text{IsBoundedBelow}(h(\mathbb{Z} _+), IntegerOrder) \)proof
from I have \( h:\mathbb{Z} \rightarrow \mathbb{Z} \) and \( \mathbb{Z} _+\subseteq \mathbb{Z} \) using AlmostHoms_def, PositiveSet_def
moreover
from A1, A2 have \( \forall n\in \mathbb{Z} _+.\ \langle 0 , h(n)\rangle \in IntegerOrder \) using Int_ZF_2_1_L2B, PositiveSet_def, Int_ZF_1_3_L10A, Int_ZF_2_1_L12, Int_ZF_2_1_L12B, Int_ZF_2_1_L12A
ultimately show \( \text{IsBoundedBelow}(h(\mathbb{Z} _+), IntegerOrder) \) by (rule func_ZF_8_L1 )
qed
ultimately have \( h \in \text{FinRangeFunctions}(\mathbb{Z} ,\mathbb{Z} ) \vee h\in \mathcal{S} _+ \) using Int_ZF_2_3_L4B
with A1 show \( f\sim g \vee g + ( - f) \in \mathcal{S} _+ \) using Int_ZF_2_1_L9C
qed

Positive slopes are arbitrarily large for large enough arguments.

lemma (in int1) Int_ZF_2_3_L5:

assumes A1: \( f\in \mathcal{S} _+ \) and A2: \( K\in \mathbb{Z} \)

shows \( \exists N\in \mathbb{Z} _+.\ \forall m.\ N\leq m \longrightarrow K \leq f(m) \)proof
from A1 obtain \( M \) where I: \( M\in \mathbb{Z} _+ \) and II: \( \forall n\in \mathbb{Z} _+.\ n + 1 \leq f(n\cdot M) \) using Arthan_L_3_spec
let \( j = \text{GreaterOf}(IntegerOrder,M,K - (minf(f, 0 .\ .\ (M - 1 )) - \text{ max}\delta (f)) - 1 ) \)
from A1, I have T1: \( minf(f, 0 .\ .\ (M - 1 )) - \text{ max}\delta (f) \in \mathbb{Z} \), \( M\in \mathbb{Z} \) using Int_ZF_2_1_L15, Int_ZF_2_1_L8, Int_ZF_1_1_L5, PositiveSet_def
with A2, I have T2: \( K - (minf(f, 0 .\ .\ (M - 1 )) - \text{ max}\delta (f)) \in \mathbb{Z} \), \( K - (minf(f, 0 .\ .\ (M - 1 )) - \text{ max}\delta (f)) - 1 \in \mathbb{Z} \) using Int_ZF_1_1_L5, int_zero_one_are_int
with T1 have III: \( M \leq j \) and \( K - (minf(f, 0 .\ .\ (M - 1 )) - \text{ max}\delta (f)) - 1 \leq j \) using Int_ZF_1_3_L18
with A2, T1, T2 have IV: \( K \leq j + 1 + (minf(f, 0 .\ .\ (M - 1 )) - \text{ max}\delta (f)) \) using int_zero_one_are_int, Int_ZF_2_L9C
let \( N = \text{GreaterOf}(IntegerOrder,1 ,j\cdot M) \)
from T1, III have T3: \( j \in \mathbb{Z} \), \( j\cdot M \in \mathbb{Z} \) using Int_ZF_2_L1A, Int_ZF_1_1_L5
then have V: \( N \in \mathbb{Z} _+ \) and VI: \( j\cdot M \leq N \) using int_zero_one_are_int, Int_ZF_1_5_L3, Int_ZF_1_3_L18
{
fix \( m \)
let \( n = m\text{ zdiv }M \)
let \( k = m\text{ zmod }M \)
assume \( N\leq m \)
with VI have \( j\cdot M \leq m \) by (rule Int_order_transitive )
with I, III have VII: \( m = n\cdot M + k \), \( j \leq n \) and VIII: \( n \in \mathbb{Z} _+ \), \( k \in 0 .\ .\ (M - 1 ) \) using IntDiv_ZF_1_L5
with II have \( j + 1 \leq n + 1 \), \( n + 1 \leq f(n\cdot M) \) using int_zero_one_are_int, int_ord_transl_inv
then have \( j + 1 \leq f(n\cdot M) \) by (rule Int_order_transitive )
with T1 have \( j + 1 + (minf(f, 0 .\ .\ (M - 1 )) - \text{ max}\delta (f)) \leq \) \( f(n\cdot M) + (minf(f, 0 .\ .\ (M - 1 )) - \text{ max}\delta (f)) \) using int_ord_transl_inv
with IV have \( K \leq f(n\cdot M) + (minf(f, 0 .\ .\ (M - 1 )) - \text{ max}\delta (f)) \) by (rule Int_order_transitive )
moreover
from A1, I, VIII have \( f(n\cdot M) + (minf(f, 0 .\ .\ (M - 1 )) - \text{ max}\delta (f)) \leq f(n\cdot M + k) \) using PositiveSet_def, Int_ZF_2_1_L16
ultimately have \( K \leq f(n\cdot M + k) \) by (rule Int_order_transitive )
with VII have \( K \leq f(m) \)
}
then have \( \forall m.\ N\leq m \longrightarrow K \leq f(m) \)
with V show \( thesis \)
qed

Positive slopes are arbitrarily small for small enough arguments. Kind of dual to Int_ZF_2_3_L5.

lemma (in int1) Int_ZF_2_3_L5A:

assumes A1: \( f\in \mathcal{S} _+ \) and A2: \( K\in \mathbb{Z} \)

shows \( \exists N\in \mathbb{Z} _+.\ \forall m.\ N\leq m \longrightarrow f( - m) \leq K \)proof
from A1 have T1: \( abs(f( 0 )) + \text{ max}\delta (f) \in \mathbb{Z} \) using Int_ZF_2_1_L8
with A2 have \( abs(f( 0 )) + \text{ max}\delta (f) - K \in \mathbb{Z} \) using Int_ZF_1_1_L5
with A1 have \( \exists N\in \mathbb{Z} _+.\ \forall m.\ N\leq m \longrightarrow abs(f( 0 )) + \text{ max}\delta (f) - K \leq f(m) \) using Int_ZF_2_3_L5
then obtain \( N \) where I: \( N\in \mathbb{Z} _+ \) and II: \( \forall m.\ N\leq m \longrightarrow abs(f( 0 )) + \text{ max}\delta (f) - K \leq f(m) \)
{
fix \( m \)
assume A3: \( N\leq m \)
with A1 have \( f( - m) \leq abs(f( 0 )) + \text{ max}\delta (f) - f(m) \) using Int_ZF_2_L1A, Int_ZF_2_1_L14
moreover
from II, T1, A3 have \( abs(f( 0 )) + \text{ max}\delta (f) - f(m) \leq \) \( (abs(f( 0 )) + \text{ max}\delta (f)) - (abs(f( 0 )) + \text{ max}\delta (f) - K) \) using Int_ZF_2_L10, int_ord_transl_inv
with A2, T1 have \( abs(f( 0 )) + \text{ max}\delta (f) - f(m) \leq K \) using Int_ZF_1_2_L3
ultimately have \( f( - m) \leq K \) by (rule Int_order_transitive )
}
then have \( \forall m.\ N\leq m \longrightarrow f( - m) \leq K \)
with I show \( thesis \)
qed

A special case of Int_ZF_2_3_L5 where \(K=1\).

corollary (in int1) Int_ZF_2_3_L6:

assumes \( f\in \mathcal{S} _+ \)

shows \( \exists N\in \mathbb{Z} _+.\ \forall m.\ N\leq m \longrightarrow f(m) \in \mathbb{Z} _+ \) using assms, int_zero_one_are_int, Int_ZF_2_3_L5, Int_ZF_1_5_L3

A special case of Int_ZF_2_3_L5 where \(m=N\).

corollary (in int1) Int_ZF_2_3_L6A:

assumes \( f\in \mathcal{S} _+ \) and \( K\in \mathbb{Z} \)

shows \( \exists N\in \mathbb{Z} _+.\ K \leq f(N) \)proof
from assms have \( \exists N\in \mathbb{Z} _+.\ \forall m.\ N\leq m \longrightarrow K \leq f(m) \) using Int_ZF_2_3_L5
then obtain \( N \) where I: \( N \in \mathbb{Z} _+ \) and II: \( \forall m.\ N\leq m \longrightarrow K \leq f(m) \)
then show \( thesis \) using PositiveSet_def, int_ord_is_refl, refl_def
qed

If values of a slope are not bounded above, then the slope is positive.

lemma (in int1) Int_ZF_2_3_L7:

assumes A1: \( f\in \mathcal{S} \) and A2: \( \forall K\in \mathbb{Z} .\ \exists n\in \mathbb{Z} _+.\ K \leq f(n) \)

shows \( f \in \mathcal{S} _+ \)proof
{
fix \( K \)
assume \( K\in \mathbb{Z} \)
with A2 obtain \( n \) where \( n\in \mathbb{Z} _+ \), \( K \leq f(n) \)
moreover
from A1 have \( \mathbb{Z} _+ \subseteq \mathbb{Z} \), \( f:\mathbb{Z} \rightarrow \mathbb{Z} \) using PositiveSet_def, AlmostHoms_def
ultimately have \( \exists m \in f(\mathbb{Z} _+).\ K \leq m \) using func1_1_L15D
}
then have \( \forall K\in \mathbb{Z} .\ \exists m \in f(\mathbb{Z} _+).\ K \leq m \)
with A1 show \( f \in \mathcal{S} _+ \) using Int_ZF_4_L9, Int_ZF_2_3_L2
qed

For unbounded slope \(f\) either \(f\in\)\( \mathcal{S} _+ \) of \(-f\in\)\( \mathcal{S} _+ \).

theorem (in int1) Int_ZF_2_3_L8:

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

shows \( (f \in \mathcal{S} _+) \text{ Xor } (( - f) \in \mathcal{S} _+) \)proof
have T1: \( \mathbb{Z} _+ \subseteq \mathbb{Z} \) using PositiveSet_def
from A1 have T2: \( f:\mathbb{Z} \rightarrow \mathbb{Z} \) using AlmostHoms_def
then have I: \( f(\mathbb{Z} _+) \subseteq \mathbb{Z} \) using func1_1_L6
from A1, A2 have \( f \in \mathcal{S} _+ \vee ( - f) \in \mathcal{S} _+ \) using Int_ZF_2_3_L2, Int_ZF_2_3_L3, IsBounded_def, Int_ZF_2_3_L4A
moreover
have \( \neg (f \in \mathcal{S} _+ \wedge ( - f) \in \mathcal{S} _+) \)proof
{
assume A3: \( f \in \mathcal{S} _+ \) and A4: \( ( - f) \in \mathcal{S} _+ \)
from A3 obtain \( N1 \) where I: \( N1\in \mathbb{Z} _+ \) and II: \( \forall m.\ N1\leq m \longrightarrow f(m) \in \mathbb{Z} _+ \) using Int_ZF_2_3_L6
from A4 obtain \( N2 \) where III: \( N2\in \mathbb{Z} _+ \) and IV: \( \forall m.\ N2\leq m \longrightarrow ( - f)(m) \in \mathbb{Z} _+ \) using Int_ZF_2_3_L6
let \( N = \text{GreaterOf}(IntegerOrder,N1,N2) \)
from I, III have \( N1 \leq N \), \( N2 \leq N \) using PositiveSet_def, Int_ZF_1_3_L18
with A1, II, IV have \( f(N) \in \mathbb{Z} _+ \), \( ( - f)(N) \in \mathbb{Z} _+ \), \( ( - f)(N) = - (f(N)) \) using Int_ZF_2_L1A, PositiveSet_def, Int_ZF_2_1_L12A
then have \( False \) using Int_ZF_1_5_L8
}
thus \( thesis \)
qed
ultimately show \( (f \in \mathcal{S} _+) \text{ Xor } (( - f) \in \mathcal{S} _+) \) using Xor_def
qed

The sum of positive slopes is a positive slope.

theorem (in int1) sum_of_pos_sls_is_pos_sl:

assumes A1: \( f \in \mathcal{S} _+ \), \( g \in \mathcal{S} _+ \)

shows \( f + g \in \mathcal{S} _+ \)proof
{
fix \( K \)
assume \( K\in \mathbb{Z} \)
with A1 have \( \exists N\in \mathbb{Z} _+.\ \forall m.\ N\leq m \longrightarrow K \leq f(m) \) using Int_ZF_2_3_L5
then obtain \( N \) where I: \( N\in \mathbb{Z} _+ \) and II: \( \forall m.\ N\leq m \longrightarrow K \leq f(m) \)
from A1 have \( \exists M\in \mathbb{Z} _+.\ \forall m.\ M\leq m \longrightarrow 0 \leq g(m) \) using int_zero_one_are_int, Int_ZF_2_3_L5
then obtain \( M \) where III: \( M\in \mathbb{Z} _+ \) and IV: \( \forall m.\ M\leq m \longrightarrow 0 \leq g(m) \)
let \( L = \text{GreaterOf}(IntegerOrder,N,M) \)
from I, III have V: \( L \in \mathbb{Z} _+ \), \( \mathbb{Z} _+ \subseteq \mathbb{Z} \) using GreaterOf_def, PositiveSet_def
moreover
from A1, V have \( (f + g)(L) = f(L) + g(L) \) using Int_ZF_2_1_L12B
moreover
from I, II, III, IV have \( K \leq f(L) + g(L) \) using PositiveSet_def, Int_ZF_1_3_L18, Int_ZF_2_L15F
ultimately have \( L \in \mathbb{Z} _+ \), \( K \leq (f + g)(L) \)
then have \( \exists n \in \mathbb{Z} _+.\ K \leq (f + g)(n) \)
}
with A1 show \( f + g \in \mathcal{S} _+ \) using Int_ZF_2_1_L12C, Int_ZF_2_3_L7
qed

The composition of positive slopes is a positive slope.

theorem (in int1) comp_of_pos_sls_is_pos_sl:

assumes A1: \( f \in \mathcal{S} _+ \), \( g \in \mathcal{S} _+ \)

shows \( f\circ g \in \mathcal{S} _+ \)proof
{
fix \( K \)
assume \( K\in \mathbb{Z} \)
with A1 have \( \exists N\in \mathbb{Z} _+.\ \forall m.\ N\leq m \longrightarrow K \leq f(m) \) using Int_ZF_2_3_L5
then obtain \( N \) where \( N\in \mathbb{Z} _+ \) and I: \( \forall m.\ N\leq m \longrightarrow K \leq f(m) \)
with A1 have \( \exists M\in \mathbb{Z} _+.\ N \leq g(M) \) using PositiveSet_def, Int_ZF_2_3_L6A
then obtain \( M \) where \( M\in \mathbb{Z} _+ \), \( N \leq g(M) \)
with A1, I have \( \exists M\in \mathbb{Z} _+.\ K \leq (f\circ g)(M) \) using PositiveSet_def, Int_ZF_2_1_L10
}
with A1 show \( f\circ g \in \mathcal{S} _+ \) using Int_ZF_2_1_L11, Int_ZF_2_3_L7
qed

A slope equivalent to a positive one is positive.

lemma (in int1) Int_ZF_2_3_L9:

assumes A1: \( f \in \mathcal{S} _+ \) and A2: \( \langle f,g\rangle \in AlEqRel \)

shows \( g \in \mathcal{S} _+ \)proof
from A2 have T: \( g\in \mathcal{S} \) and \( \exists L\in \mathbb{Z} .\ \forall m\in \mathbb{Z} .\ abs(f(m) - g(m)) \leq L \) using Int_ZF_2_1_L9A
then obtain \( L \) where I: \( L\in \mathbb{Z} \) and II: \( \forall m\in \mathbb{Z} .\ abs(f(m) - g(m)) \leq L \)
{
fix \( K \)
assume A3: \( K\in \mathbb{Z} \)
with I have \( K + L \in \mathbb{Z} \) using Int_ZF_1_1_L5
with A1 obtain \( M \) where III: \( M\in \mathbb{Z} _+ \) and IV: \( K + L \leq f(M) \) using Int_ZF_2_3_L6A
with A1, A3, I have \( K \leq f(M) - L \) using PositiveSet_def, Int_ZF_2_1_L2B, Int_ZF_2_L9B
moreover
from A1, T, II, III have \( f(M) - L \leq g(M) \) using PositiveSet_def, Int_ZF_2_1_L2B, Int_triangle_ineq2
ultimately have \( K \leq g(M) \) by (rule Int_order_transitive )
with III have \( \exists n\in \mathbb{Z} _+.\ K \leq g(n) \)
}
with T show \( g \in \mathcal{S} _+ \) using Int_ZF_2_3_L7
qed

The set of positive slopes is saturated with respect to the relation of equivalence of slopes.

lemma (in int1) pos_slopes_saturated:

shows \( \text{IsSaturated}(AlEqRel,\mathcal{S} _+) \)proof
have \( \text{equiv}(\mathcal{S} ,AlEqRel) \), \( AlEqRel \subseteq \mathcal{S} \times \mathcal{S} \) using Int_ZF_2_1_L9B
moreover
have \( \mathcal{S} _+ \subseteq \mathcal{S} \)
moreover
have \( \forall f\in \mathcal{S} _+.\ \forall g\in \mathcal{S} .\ \langle f,g\rangle \in AlEqRel \longrightarrow g \in \mathcal{S} _+ \) using Int_ZF_2_3_L9
ultimately show \( \text{IsSaturated}(AlEqRel,\mathcal{S} _+) \) by (rule EquivClass_3_L3 )
qed

A technical lemma involving a projection of the set of positive slopes and a logical epression with exclusive or.

lemma (in int1) Int_ZF_2_3_L10:

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

shows \( (AlEqRel\{f\} \in R) \text{ Xor } (AlEqRel\{g\} \in R) \)proof
from A1, A2, A3 have \( \text{equiv}(\mathcal{S} ,AlEqRel) \), \( \text{IsSaturated}(AlEqRel,\mathcal{S} _+) \), \( \mathcal{S} _+ \subseteq \mathcal{S} \), \( f\in \mathcal{S} \), \( g\in \mathcal{S} \), \( R = \{AlEqRel\{s\}.\ s\in \mathcal{S} _+\} \), \( (f\in \mathcal{S} _+) \text{ Xor } (g\in \mathcal{S} _+) \) using pos_slopes_saturated, Int_ZF_2_1_L9B
then show \( thesis \) by (rule EquivClass_3_L7 )
qed

Identity function is a positive slope.

lemma (in int1) Int_ZF_2_3_L11:

shows \( id(\mathbb{Z} ) \in \mathcal{S} _+ \)proof
let \( f = id(\mathbb{Z} ) \)
{
fix \( K \)
assume \( K\in \mathbb{Z} \)
then obtain \( n \) where T: \( n\in \mathbb{Z} _+ \) and \( K\leq n \) using Int_ZF_1_5_L9
moreover
from T have \( f(n) = n \) using PositiveSet_def
ultimately have \( n\in \mathbb{Z} _+ \) and \( K\leq f(n) \)
then have \( \exists n\in \mathbb{Z} _+.\ K\leq f(n) \)
}
then show \( f \in \mathcal{S} _+ \) using Int_ZF_2_1_L17, Int_ZF_2_3_L7
qed

The identity function is not almost equal to any bounded function.

lemma (in int1) Int_ZF_2_3_L12:

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

shows \( \neg (id(\mathbb{Z} ) \sim f) \)proof
{
from A1 have \( id(\mathbb{Z} ) \in \mathcal{S} _+ \) using Int_ZF_2_3_L11
moreover
assume \( \langle id(\mathbb{Z} ),f\rangle \in AlEqRel \)
ultimately have \( f \in \mathcal{S} _+ \) by (rule Int_ZF_2_3_L9 )
with A1 have \( False \) using Int_ZF_2_3_L1B
}
then show \( \neg (id(\mathbb{Z} ) \sim f) \)
qed

Inverting slopes

Not every slope is a 1:1 function. However, we can still invert slopes in the sense that if \(f\) is a slope, then we can find a slope \(g\) such that \(f\circ g\) is almost equal to the identity function. The goal of this this section is to establish this fact for positive slopes.

If \(f\) is a positive slope, then for every positive integer \(p\) the set \(\{n\in Z_+: p\leq f(n)\}\) is a nonempty subset of positive integers. Recall that \(f^{-1}(p)\) is the notation for the smallest element of this set.

lemma (in int1) Int_ZF_2_4_L1:

assumes A1: \( f \in \mathcal{S} _+ \) and A2: \( p\in \mathbb{Z} _+ \) and A3: \( A = \{n\in \mathbb{Z} _+.\ p \leq f(n)\} \)

shows \( A \subseteq \mathbb{Z} _+ \), \( A \neq 0 \), \( f^{-1}(p) \in A \), \( \forall m\in A.\ f^{-1}(p) \leq m \)proof
from A3 show I: \( A \subseteq \mathbb{Z} _+ \)
from A1, A2 have \( \exists n\in \mathbb{Z} _+.\ p \leq f(n) \) using PositiveSet_def, Int_ZF_2_3_L6A
with A3 show II: \( A \neq 0 \)
from A3, I, II show \( f^{-1}(p) \in A \), \( \forall m\in A.\ f^{-1}(p) \leq m \) using Int_ZF_1_5_L1C
qed

If \(f\) is a positive slope and \(p\) is a positive integer \(p\), then \(f^{-1}(p)\) (defined as the minimum of the set \(\{n\in Z_+: p\leq f(n)\}\) ) is a (well defined) positive integer.

lemma (in int1) Int_ZF_2_4_L2:

assumes \( f \in \mathcal{S} _+ \) and \( p\in \mathbb{Z} _+ \)

shows \( f^{-1}(p) \in \mathbb{Z} _+ \), \( p \leq f(f^{-1}(p)) \) using assms, Int_ZF_2_4_L1

If \(f\) is a positive slope and \(p\) is a positive integer such that \(n\leq f(p)\), then \(f^{-1}(n) \leq p\).

lemma (in int1) Int_ZF_2_4_L3:

assumes \( f \in \mathcal{S} _+ \) and \( m\in \mathbb{Z} _+ \), \( p\in \mathbb{Z} _+ \) and \( m \leq f(p) \)

shows \( f^{-1}(m) \leq p \) using assms, Int_ZF_2_4_L1

An upper bound \(f(f^{-1}(m) -1)\) for positive slopes.

lemma (in int1) Int_ZF_2_4_L4:

assumes A1: \( f \in \mathcal{S} _+ \) and A2: \( m\in \mathbb{Z} _+ \) and A3: \( f^{-1}(m) - 1 \in \mathbb{Z} _+ \)

shows \( f(f^{-1}(m) - 1 ) \leq m \), \( f(f^{-1}(m) - 1 ) \neq m \)proof
from A1, A2 have T: \( f^{-1}(m) \in \mathbb{Z} \) using Int_ZF_2_4_L2, PositiveSet_def
from A1, A3 have \( f:\mathbb{Z} \rightarrow \mathbb{Z} \) and \( f^{-1}(m) - 1 \in \mathbb{Z} \) using Int_ZF_2_3_L1, PositiveSet_def
with A1, A2 have T1: \( f(f^{-1}(m) - 1 ) \in \mathbb{Z} \), \( m\in \mathbb{Z} \) using apply_funtype, PositiveSet_def
{
assume \( m \leq f(f^{-1}(m) - 1 ) \)
with A1, A2, A3 have \( f^{-1}(m) \leq f^{-1}(m) - 1 \) by (rule Int_ZF_2_4_L3 )
with T have \( False \) using Int_ZF_1_2_L3AA
}
then have I: \( \neg (m \leq f(f^{-1}(m) - 1 )) \)
with T1 show \( f(f^{-1}(m) - 1 ) \leq m \) by (rule Int_ZF_2_L19 )
from T1, I show \( f(f^{-1}(m) - 1 ) \neq m \) by (rule Int_ZF_2_L19 )
qed

The (candidate for) the inverse of a positive slope is nondecreasing.

lemma (in int1) Int_ZF_2_4_L5:

assumes A1: \( f \in \mathcal{S} _+ \) and A2: \( m\in \mathbb{Z} _+ \) and A3: \( m\leq n \)

shows \( f^{-1}(m) \leq f^{-1}(n) \)proof
from A2, A3 have T: \( n \in \mathbb{Z} _+ \) using Int_ZF_1_5_L7
with A1 have \( n \leq f(f^{-1}(n)) \) using Int_ZF_2_4_L2
with A3 have \( m \leq f(f^{-1}(n)) \) by (rule Int_order_transitive )
with A1, A2, T show \( f^{-1}(m) \leq f^{-1}(n) \) using Int_ZF_2_4_L2, Int_ZF_2_4_L3
qed

If \(f^{-1}(m)\) is positive and \(n\) is a positive integer, then, then \(f^{-1}(m+n)-1\) is positive.

lemma (in int1) Int_ZF_2_4_L6:

assumes A1: \( f \in \mathcal{S} _+ \) and A2: \( m\in \mathbb{Z} _+ \), \( n\in \mathbb{Z} _+ \) and A3: \( f^{-1}(m) - 1 \in \mathbb{Z} _+ \)

shows \( f^{-1}(m + n) - 1 \in \mathbb{Z} _+ \)proof
from A1, A2 have \( f^{-1}(m) - 1 \leq f^{-1}(m + n) - 1 \) using PositiveSet_def, Int_ZF_1_5_L7A, Int_ZF_2_4_L2, Int_ZF_2_4_L5, int_zero_one_are_int, Int_ZF_1_1_L4, int_ord_transl_inv
with A3 show \( f^{-1}(m + n) - 1 \in \mathbb{Z} _+ \) using Int_ZF_1_5_L7
qed

If \(f\) is a slope, then \(f(f^{-1}(m+n)-f^{-1}(m) - f^{-1}(n))\) is uniformly bounded above and below. Will it be the messiest IsarMathLib proof ever? Only time will tell.

lemma (in int1) Int_ZF_2_4_L7:

assumes A1: \( f \in \mathcal{S} _+ \) and A2: \( \forall m\in \mathbb{Z} _+.\ f^{-1}(m) - 1 \in \mathbb{Z} _+ \)

shows \( \exists U\in \mathbb{Z} .\ \forall m\in \mathbb{Z} _+.\ \forall n\in \mathbb{Z} _+.\ f(f^{-1}(m + n) - f^{-1}(m) - f^{-1}(n)) \leq U \), \( \exists N\in \mathbb{Z} .\ \forall m\in \mathbb{Z} _+.\ \forall n\in \mathbb{Z} _+.\ N \leq f(f^{-1}(m + n) - f^{-1}(m) - f^{-1}(n)) \)proof
from A1 have \( \exists L\in \mathbb{Z} .\ \forall r\in \mathbb{Z} .\ f(r) \leq f(r - 1 ) + L \) using Int_ZF_2_1_L28
then obtain \( L \) where I: \( L\in \mathbb{Z} \) and II: \( \forall r\in \mathbb{Z} .\ f(r) \leq f(r - 1 ) + L \)
from A1 have \( \exists M\in \mathbb{Z} .\ \forall r\in \mathbb{Z} .\ \forall p\in \mathbb{Z} .\ \forall q\in \mathbb{Z} .\ f(r - p - q) \leq f(r) - f(p) - f(q) + M \), \( \exists K\in \mathbb{Z} .\ \forall r\in \mathbb{Z} .\ \forall p\in \mathbb{Z} .\ \forall q\in \mathbb{Z} .\ f(r) - f(p) - f(q) + K \leq f(r - p - q) \) using Int_ZF_2_1_L30
then obtain \( M \) \( K \) where III: \( M\in \mathbb{Z} \) and IV: \( \forall r\in \mathbb{Z} .\ \forall p\in \mathbb{Z} .\ \forall q\in \mathbb{Z} .\ f(r - p - q) \leq f(r) - f(p) - f(q) + M \) and V: \( K\in \mathbb{Z} \) and VI: \( \forall r\in \mathbb{Z} .\ \forall p\in \mathbb{Z} .\ \forall q\in \mathbb{Z} .\ f(r) - f(p) - f(q) + K \leq f(r - p - q) \)
from I, III, V have \( L + M \in \mathbb{Z} \), \( ( - L) - L + K \in \mathbb{Z} \) using Int_ZF_1_1_L4, Int_ZF_1_1_L5
moreover {
fix \( m \) \( n \)
assume A3: \( m\in \mathbb{Z} _+ \), \( n\in \mathbb{Z} _+ \)
have \( f(f^{-1}(m + n) - f^{-1}(m) - f^{-1}(n)) \leq L + M \wedge \) \( ( - L) - L + K \leq f(f^{-1}(m + n) - f^{-1}(m) - f^{-1}(n)) \)proof
let \( r = f^{-1}(m + n) \)
let \( p = f^{-1}(m) \)
let \( q = f^{-1}(n) \)
from A1, A3 have T1: \( p \in \mathbb{Z} _+ \), \( q \in \mathbb{Z} _+ \), \( r \in \mathbb{Z} _+ \) using Int_ZF_2_4_L2, pos_int_closed_add_unfolded
with A3 have T2: \( m \in \mathbb{Z} \), \( n \in \mathbb{Z} \), \( p \in \mathbb{Z} \), \( q \in \mathbb{Z} \), \( r \in \mathbb{Z} \) using PositiveSet_def
from A2, A3 have T3: \( r - 1 \in \mathbb{Z} _+ \), \( p - 1 \in \mathbb{Z} _+ \), \( q - 1 \in \mathbb{Z} _+ \) using pos_int_closed_add_unfolded
from A1, A3 have VII: \( m + n \leq f(r) \), \( m \leq f(p) \), \( n \leq f(q) \) using Int_ZF_2_4_L2, pos_int_closed_add_unfolded
from A1, A3, T3 have VIII: \( f(r - 1 ) \leq m + n \), \( f(p - 1 ) \leq m \), \( f(q - 1 ) \leq n \) using pos_int_closed_add_unfolded, Int_ZF_2_4_L4
have \( f(r - p - q) \leq L + M \)proof
from IV, T2 have \( f(r - p - q) \leq f(r) - f(p) - f(q) + M \)
moreover
from I, II, T2, VIII have \( f(r) \leq f(r - 1 ) + L \), \( f(r - 1 ) + L \leq m + n + L \) using int_ord_transl_inv
then have \( f(r) \leq m + n + L \) by (rule Int_order_transitive )
with VII have \( f(r) - f(p) \leq m + n + L - m \) using int_ineq_add_sides
with I, T2, VII have \( f(r) - f(p) - f(q) \leq n + L - n \) using Int_ZF_1_2_L9, int_ineq_add_sides
with I, III, T2 have \( f(r) - f(p) - f(q) + M \leq L + M \) using Int_ZF_1_2_L3, int_ord_transl_inv
ultimately show \( f(r - p - q) \leq L + M \) by (rule Int_order_transitive )
qed
moreover
have \( ( - L) - L + K \leq f(r - p - q) \)proof
from I, II, T2, VIII have \( f(p) \leq f(p - 1 ) + L \), \( f(p - 1 ) + L \leq m + L \) using int_ord_transl_inv
then have \( f(p) \leq m + L \) by (rule Int_order_transitive )
with VII have \( m + n - (m + L) \leq f(r) - f(p) \) using int_ineq_add_sides
with I, T2 have \( n - L \leq f(r) - f(p) \) using Int_ZF_1_2_L9
moreover
from I, II, T2, VIII have \( f(q) \leq f(q - 1 ) + L \), \( f(q - 1 ) + L \leq n + L \) using int_ord_transl_inv
then have \( f(q) \leq n + L \) by (rule Int_order_transitive )
ultimately have \( n - L - (n + L) \leq f(r) - f(p) - f(q) \) using int_ineq_add_sides
with I, V, T2 have \( ( - L) - L + K \leq f(r) - f(p) - f(q) + K \) using Int_ZF_1_2_L3, int_ord_transl_inv
moreover
from VI, T2 have \( f(r) - f(p) - f(q) + K \leq f(r - p - q) \)
ultimately show \( ( - L) - L + K \leq f(r - p - q) \) by (rule Int_order_transitive )
qed
ultimately show \( f(r - p - q) \leq L + M \wedge \) \( ( - L) - L + K \leq f(f^{-1}(m + n) - f^{-1}(m) - f^{-1}(n)) \)
qed
} ultimately show \( \exists U\in \mathbb{Z} .\ \forall m\in \mathbb{Z} _+.\ \forall n\in \mathbb{Z} _+.\ f(f^{-1}(m + n) - f^{-1}(m) - f^{-1}(n)) \leq U \), \( \exists N\in \mathbb{Z} .\ \forall m\in \mathbb{Z} _+.\ \forall n\in \mathbb{Z} _+.\ N \leq f(f^{-1}(m + n) - f^{-1}(m) - f^{-1}(n)) \)
qed

The expression \(f^{-1}(m+n)-f^{-1}(m) - f^{-1}(n)\) is uniformly bounded for all pairs \(\langle m,n \rangle \in\) \( \mathbb{Z} _+\times \mathbb{Z} _+ \). Recall that in the int1 context \( \varepsilon (f,x) \) is defined so that \(\varepsilon(f,\langle m,n \rangle ) = f^{-1}(m+n)-f^{-1}(m) - f^{-1}(n)\).

lemma (in int1) Int_ZF_2_4_L8:

assumes A1: \( f \in \mathcal{S} _+ \) and A2: \( \forall m\in \mathbb{Z} _+.\ f^{-1}(m) - 1 \in \mathbb{Z} _+ \)

shows \( \exists M.\ \forall x\in \mathbb{Z} _+\times \mathbb{Z} _+.\ abs(\varepsilon (f,x)) \leq M \)proof
from A1, A2 have \( \exists U\in \mathbb{Z} .\ \forall m\in \mathbb{Z} _+.\ \forall n\in \mathbb{Z} _+.\ f(f^{-1}(m + n) - f^{-1}(m) - f^{-1}(n)) \leq U \), \( \exists N\in \mathbb{Z} .\ \forall m\in \mathbb{Z} _+.\ \forall n\in \mathbb{Z} _+.\ N \leq f(f^{-1}(m + n) - f^{-1}(m) - f^{-1}(n)) \) using Int_ZF_2_4_L7
then obtain \( U \) \( N \) where I: \( \forall m\in \mathbb{Z} _+.\ \forall n\in \mathbb{Z} _+.\ f(f^{-1}(m + n) - f^{-1}(m) - f^{-1}(n)) \leq U \), \( \forall m\in \mathbb{Z} _+.\ \forall n\in \mathbb{Z} _+.\ N \leq f(f^{-1}(m + n) - f^{-1}(m) - f^{-1}(n)) \)
have \( \mathbb{Z} _+\times \mathbb{Z} _+ \neq 0 \) using int_one_two_are_pos
moreover
from A1 have \( f: \mathbb{Z} \rightarrow \mathbb{Z} \) using AlmostHoms_def
moreover
from A1 have \( \forall a\in \mathbb{Z} .\ \exists b\in \mathbb{Z} _+.\ \forall x.\ b\leq x \longrightarrow a \leq f(x) \) using Int_ZF_2_3_L5
moreover
from A1 have \( \forall a\in \mathbb{Z} .\ \exists b\in \mathbb{Z} _+.\ \forall y.\ b\leq y \longrightarrow f( - y) \leq a \) using Int_ZF_2_3_L5A
moreover
have \( \forall x\in \mathbb{Z} _+\times \mathbb{Z} _+.\ \varepsilon (f,x) \in \mathbb{Z} \wedge f(\varepsilon (f,x)) \leq U \wedge N \leq f(\varepsilon (f,x)) \)proof
{
fix \( x \)
assume A3: \( x \in \mathbb{Z} _+\times \mathbb{Z} _+ \)
let \( m = \text{fst}(x) \)
let \( n = \text{snd}(x) \)
from A3 have T: \( m \in \mathbb{Z} _+ \), \( n \in \mathbb{Z} _+ \), \( m + n \in \mathbb{Z} _+ \) using pos_int_closed_add_unfolded
with A1 have \( f^{-1}(m + n) \in \mathbb{Z} \), \( f^{-1}(m) \in \mathbb{Z} \), \( f^{-1}(n) \in \mathbb{Z} \) using Int_ZF_2_4_L2, PositiveSet_def
with I, T have \( \varepsilon (f,x) \in \mathbb{Z} \wedge f(\varepsilon (f,x)) \leq U \wedge N \leq f(\varepsilon (f,x)) \) using Int_ZF_1_1_L5
}
thus \( thesis \)
qed
ultimately show \( \exists M.\ \forall x\in \mathbb{Z} _+\times \mathbb{Z} _+.\ abs(\varepsilon (f,x)) \leq M \) by (rule Int_ZF_1_6_L4 )
qed

The (candidate for) inverse of a positive slope is a (well defined) function on \( \mathbb{Z} _+ \).

lemma (in int1) Int_ZF_2_4_L9:

assumes A1: \( f \in \mathcal{S} _+ \) and A2: \( g = \{\langle p,f^{-1}(p)\rangle .\ p\in \mathbb{Z} _+\} \)

shows \( g : \mathbb{Z} _+\rightarrow \mathbb{Z} _+ \), \( g : \mathbb{Z} _+\rightarrow \mathbb{Z} \)proof
from A1 have \( \forall p\in \mathbb{Z} _+.\ f^{-1}(p) \in \mathbb{Z} _+ \), \( \forall p\in \mathbb{Z} _+.\ f^{-1}(p) \in \mathbb{Z} \) using Int_ZF_2_4_L2, PositiveSet_def
with A2 show \( g : \mathbb{Z} _+\rightarrow \mathbb{Z} _+ \) and \( g : \mathbb{Z} _+\rightarrow \mathbb{Z} \) using ZF_fun_from_total
qed

What are the values of the (candidate for) the inverse of a positive slope?

lemma (in int1) Int_ZF_2_4_L10:

assumes A1: \( f \in \mathcal{S} _+ \) and A2: \( g = \{\langle p,f^{-1}(p)\rangle .\ p\in \mathbb{Z} _+\} \) and A3: \( p\in \mathbb{Z} _+ \)

shows \( g(p) = f^{-1}(p) \)proof
from A1, A2 have \( g : \mathbb{Z} _+\rightarrow \mathbb{Z} _+ \) using Int_ZF_2_4_L9
with A2, A3 show \( g(p) = f^{-1}(p) \) using ZF_fun_from_tot_val
qed

The (candidate for) the inverse of a positive slope is a slope.

lemma (in int1) Int_ZF_2_4_L11:

assumes A1: \( f \in \mathcal{S} _+ \) and A2: \( \forall m\in \mathbb{Z} _+.\ f^{-1}(m) - 1 \in \mathbb{Z} _+ \) and A3: \( g = \{\langle p,f^{-1}(p)\rangle .\ p\in \mathbb{Z} _+\} \)

shows \( \text{OddExtension}(\mathbb{Z} ,IntegerAddition,IntegerOrder,g) \in \mathcal{S} \)proof
from A1, A2 have \( \exists L.\ \forall x\in \mathbb{Z} _+\times \mathbb{Z} _+.\ abs(\varepsilon (f,x)) \leq L \) using Int_ZF_2_4_L8
then obtain \( L \) where I: \( \forall x\in \mathbb{Z} _+\times \mathbb{Z} _+.\ abs(\varepsilon (f,x)) \leq L \)
from A1, A3 have \( g : \mathbb{Z} _+\rightarrow \mathbb{Z} \) using Int_ZF_2_4_L9
moreover
have \( \forall m\in \mathbb{Z} _+.\ \forall n\in \mathbb{Z} _+.\ abs(\delta (g,m,n)) \leq L \)proof
{
fix \( m \) \( n \)
assume A4: \( m\in \mathbb{Z} _+ \), \( n\in \mathbb{Z} _+ \)
then have \( \langle m,n\rangle \in \mathbb{Z} _+\times \mathbb{Z} _+ \)
with I have \( abs(\varepsilon (f,\langle m,n\rangle )) \leq L \)
moreover
have \( \varepsilon (f,\langle m,n\rangle ) = f^{-1}(m + n) - f^{-1}(m) - f^{-1}(n) \)
moreover
from A1, A3, A4 have \( f^{-1}(m + n) = g(m + n) \), \( f^{-1}(m) = g(m) \), \( f^{-1}(n) = g(n) \) using pos_int_closed_add_unfolded, Int_ZF_2_4_L10
ultimately have \( abs(\delta (g,m,n)) \leq L \)
}
thus \( \forall m\in \mathbb{Z} _+.\ \forall n\in \mathbb{Z} _+.\ abs(\delta (g,m,n)) \leq L \)
qed
ultimately show \( thesis \) by (rule Int_ZF_2_1_L24 )
qed

Every positive slope that is at least \(2\) on positive integers almost has an inverse.

lemma (in int1) Int_ZF_2_4_L12:

assumes A1: \( f \in \mathcal{S} _+ \) and A2: \( \forall m\in \mathbb{Z} _+.\ f^{-1}(m) - 1 \in \mathbb{Z} _+ \)

shows \( \exists h\in \mathcal{S} .\ f\circ h \sim id(\mathbb{Z} ) \)proof
let \( g = \{\langle p,f^{-1}(p)\rangle .\ p\in \mathbb{Z} _+\} \)
let \( h = \text{OddExtension}(\mathbb{Z} ,IntegerAddition,IntegerOrder,g) \)
from A1 have \( \exists M\in \mathbb{Z} .\ \forall n\in \mathbb{Z} .\ f(n) \leq f(n - 1 ) + M \) using Int_ZF_2_1_L28
then obtain \( M \) where I: \( M\in \mathbb{Z} \) and II: \( \forall n\in \mathbb{Z} .\ f(n) \leq f(n - 1 ) + M \)
from A1, A2 have T: \( h \in \mathcal{S} \) using Int_ZF_2_4_L11
moreover
have \( f\circ h \sim id(\mathbb{Z} ) \)proof
from A1, T have \( f\circ h \in \mathcal{S} \) using Int_ZF_2_1_L11
moreover
note I
moreover {
fix \( m \)
assume A3: \( m\in \mathbb{Z} _+ \)
with A1 have \( f^{-1}(m) \in \mathbb{Z} \) using Int_ZF_2_4_L2, PositiveSet_def
with II have \( f(f^{-1}(m)) \leq f(f^{-1}(m) - 1 ) + M \)
moreover
from A1, A2, I, A3 have \( f(f^{-1}(m) - 1 ) + M \leq m + M \) using Int_ZF_2_4_L4, int_ord_transl_inv
ultimately have \( f(f^{-1}(m)) \leq m + M \) by (rule Int_order_transitive )
moreover
from A1, A3 have \( m \leq f(f^{-1}(m)) \) using Int_ZF_2_4_L2
moreover
from A1, A2, T, A3 have \( f(f^{-1}(m)) = (f\circ h)(m) \) using Int_ZF_2_4_L9, Int_ZF_1_5_L11, Int_ZF_2_4_L10, PositiveSet_def, Int_ZF_2_1_L10
ultimately have \( m \leq (f\circ h)(m) \wedge (f\circ h)(m) \leq m + M \)
} ultimately show \( f\circ h \sim id(\mathbb{Z} ) \) using Int_ZF_2_1_L32
qed
ultimately show \( \exists h\in \mathcal{S} .\ f\circ h \sim id(\mathbb{Z} ) \)
qed

Int_ZF_2_4_L12 is almost what we need, except that it has an assumption that the values of the slope that we get the inverse for are not smaller than \(2\) on positive integers. The Arthan's proof of Theorem 11 has a mistake where he says "note that for all but finitely many \(m,n\in N\) \(p=g(m)\) and \(q=g(n)\) are both positive". Of course there may be infinitely many pairs \(\langle m,n \rangle\) such that \(p,q\) are not both positive. This is however easy to workaround: we just modify the slope by adding a constant so that the slope is large enough on positive integers and then look for the inverse.

theorem (in int1) pos_slope_has_inv:

assumes A1: \( 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} )) \)proof
from A1 have \( f: \mathbb{Z} \rightarrow \mathbb{Z} \), \( 1 \in \mathbb{Z} \), \( 2 \in \mathbb{Z} \) using AlmostHoms_def, int_zero_one_are_int, int_two_three_are_int
moreover
from A1 have \( \forall a\in \mathbb{Z} .\ \exists b\in \mathbb{Z} _+.\ \forall x.\ b\leq x \longrightarrow a \leq f(x) \) using Int_ZF_2_3_L5
ultimately have \( \exists c\in \mathbb{Z} .\ 2 \leq \text{Minimum}(IntegerOrder,\{n\in \mathbb{Z} _+.\ 1 \leq f(n) + c\}) \) by (rule Int_ZF_1_6_L7 )
then obtain \( c \) where I: \( c\in \mathbb{Z} \) and II: \( 2 \leq \text{Minimum}(IntegerOrder,\{n\in \mathbb{Z} _+.\ 1 \leq f(n) + c\}) \)
let \( g = \{\langle m,f(m) + c\rangle .\ m\in \mathbb{Z} \} \)
from A1, I have III: \( g\in \mathcal{S} \) and IV: \( f\sim g \) using Int_ZF_2_1_L33
from IV have \( \langle f,g\rangle \in AlEqRel \)
with A1 have T: \( g \in \mathcal{S} _+ \) by (rule Int_ZF_2_3_L9 )
moreover
have \( \forall m\in \mathbb{Z} _+.\ g^{-1}(m) - 1 \in \mathbb{Z} _+ \)proof
fix \( m \)
assume A2: \( m\in \mathbb{Z} _+ \)
from A1, I, II have V: \( 2 \leq g^{-1}(1 ) \) using Int_ZF_2_1_L33, PositiveSet_def
moreover
from A2, T have \( g^{-1}(1 ) \leq g^{-1}(m) \) using Int_ZF_1_5_L3, int_one_two_are_pos, Int_ZF_2_4_L5
ultimately have \( 2 \leq g^{-1}(m) \) by (rule Int_order_transitive )
then have \( 2 - 1 \leq g^{-1}(m) - 1 \) using int_zero_one_are_int, Int_ZF_1_1_L4, int_ord_transl_inv
then show \( g^{-1}(m) - 1 \in \mathbb{Z} _+ \) using int_zero_one_are_int, Int_ZF_1_2_L3, Int_ZF_1_5_L3
qed
ultimately have \( \exists h\in \mathcal{S} .\ g\circ h \sim id(\mathbb{Z} ) \) by (rule Int_ZF_2_4_L12 )
with III, IV show \( thesis \)
qed

Completeness

In this section we consider properties of slopes that are needed for the proof of completeness of real numbers constructred in Real_ZF_1.thy. In particular we consider properties of embedding of integers into the set of slopes by the mapping \(m \mapsto m^S\) , where \(m^S\) is defined by \(m^S(n) = m\cdot n\).

If m is an integer, then \(m^S\) is a slope whose value is \(m\cdot n\) for every integer.

lemma (in int1) Int_ZF_2_5_L1:

assumes A1: \( m \in \mathbb{Z} \)

shows \( \forall n \in \mathbb{Z} .\ (m^S)(n) = m\cdot n \), \( m^S \in \mathcal{S} \)proof
from A1 have I: \( m^S:\mathbb{Z} \rightarrow \mathbb{Z} \) using Int_ZF_1_1_L5, ZF_fun_from_total
then show II: \( \forall n \in \mathbb{Z} .\ (m^S)(n) = m\cdot n \) using ZF_fun_from_tot_val
{
fix \( n \) \( k \)
assume A2: \( n\in \mathbb{Z} \), \( k\in \mathbb{Z} \)
with A1 have T: \( m\cdot n \in \mathbb{Z} \), \( m\cdot k \in \mathbb{Z} \) using Int_ZF_1_1_L5
from A1, A2, II, T have \( \delta (m^S,n,k) = m\cdot k - m\cdot k \) using Int_ZF_1_1_L5, Int_ZF_1_1_L1, Int_ZF_1_2_L3
also
from T have \( \ldots = 0 \) using Int_ZF_1_1_L4
finally have \( \delta (m^S,n,k) = 0 \)
then have \( abs(\delta (m^S,n,k)) \leq 0 \) using Int_ZF_2_L18, int_zero_one_are_int, int_ord_is_refl, refl_def
}
then have \( \forall n\in \mathbb{Z} .\ \forall k\in \mathbb{Z} .\ abs(\delta (m^S,n,k)) \leq 0 \)
with I show \( m^S \in \mathcal{S} \) by (rule Int_ZF_2_1_L5 )
qed

For any slope \(f\) there is an integer \(m\) such that there is some slope \(g\) that is almost equal to \(m^S\) and dominates \(f\) in the sense that \(f\leq g\) on positive integers (which implies that either \(g\) is almost equal to \(f\) or \(g-f\) is a positive slope. This will be used in Real_ZF_1.thy to show that for any real number there is an integer that (whose real embedding) is greater or equal.

lemma (in int1) Int_ZF_2_5_L2:

assumes A1: \( 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} _+)) \)proof
from A1 have \( \exists m k.\ m\in \mathbb{Z} \wedge k\in \mathbb{Z} \wedge (\forall p\in \mathbb{Z} .\ abs(f(p)) \leq m\cdot abs(p) + k) \) using Arthan_Lem_8
then obtain \( m \) \( k \) where I: \( m\in \mathbb{Z} \) and II: \( k\in \mathbb{Z} \) and III: \( \forall p\in \mathbb{Z} .\ abs(f(p)) \leq m\cdot abs(p) + k \)
let \( g = \{\langle n,m^S(n) + k\rangle .\ n\in \mathbb{Z} \} \)
from I have IV: \( m^S \in \mathcal{S} \) using Int_ZF_2_5_L1
with II have V: \( g\in \mathcal{S} \) and VI: \( m^S\sim g \) using Int_ZF_2_1_L33
{
fix \( n \)
assume A2: \( n\in \mathbb{Z} _+ \)
with A1 have \( f(n) \in \mathbb{Z} \) using Int_ZF_2_1_L2B, PositiveSet_def
then have \( f(n) \leq abs(f(n)) \) using Int_ZF_2_L19C
moreover
from III, A2 have \( abs(f(n)) \leq m\cdot abs(n) + k \) using PositiveSet_def
with A2 have \( abs(f(n)) \leq m\cdot n + k \) using Int_ZF_1_5_L4A
ultimately have \( f(n) \leq m\cdot n + k \) by (rule Int_order_transitive )
moreover
from II, IV, A2 have \( g(n) = (m^S)(n) + k \) using Int_ZF_2_1_L33, PositiveSet_def
with I, A2 have \( g(n) = m\cdot n + k \) using Int_ZF_2_5_L1, PositiveSet_def
ultimately have \( f(n) \leq g(n) \)
}
then have \( \forall n\in \mathbb{Z} _+.\ f(n) \leq g(n) \)
with A1, V have \( f\sim g \vee g + ( - f) \in \mathcal{S} _+ \) using Int_ZF_2_3_L4C
with I, V, VI show \( thesis \)
qed

The negative of an integer embeds in slopes as a negative of the orgiginal embedding.

lemma (in int1) Int_ZF_2_5_L3:

assumes A1: \( m \in \mathbb{Z} \)

shows \( ( - m)^S = - (m^S) \)proof
from A1 have \( ( - m)^S: \mathbb{Z} \rightarrow \mathbb{Z} \) and \( ( - (m^S)): \mathbb{Z} \rightarrow \mathbb{Z} \) using Int_ZF_1_1_L4, Int_ZF_2_5_L1, AlmostHoms_def, Int_ZF_2_1_L12
moreover
have \( \forall n\in \mathbb{Z} .\ (( - m)^S)(n) = ( - (m^S))(n) \)proof
fix \( n \)
assume A2: \( n\in \mathbb{Z} \)
with A1 have \( (( - m)^S)(n) = ( - m)\cdot n \), \( ( - (m^S))(n) = - (m\cdot n) \) using Int_ZF_1_1_L4, Int_ZF_2_5_L1, Int_ZF_2_1_L12A
with A1, A2 show \( (( - m)^S)(n) = ( - (m^S))(n) \) using Int_ZF_1_1_L5
qed
ultimately show \( ( - m)^S = - (m^S) \) using fun_extension_iff
qed

The sum of embeddings is the embeding of the sum.

lemma (in int1) Int_ZF_2_5_L3A:

assumes A1: \( m\in \mathbb{Z} \), \( k\in \mathbb{Z} \)

shows \( (m^S) + (k^S) = ((m + k)^S) \)proof
from A1 have T1: \( m + k \in \mathbb{Z} \) using Int_ZF_1_1_L5
with A1 have T2: \( (m^S) \in \mathcal{S} \), \( (k^S) \in \mathcal{S} \), \( (m + k)^S \in \mathcal{S} \), \( (m^S) + (k^S) \in \mathcal{S} \) using Int_ZF_2_5_L1, Int_ZF_2_1_L12C
then have \( (m^S) + (k^S) : \mathbb{Z} \rightarrow \mathbb{Z} \), \( (m + k)^S : \mathbb{Z} \rightarrow \mathbb{Z} \) using AlmostHoms_def
moreover
have \( \forall n\in \mathbb{Z} .\ ((m^S) + (k^S))(n) = ((m + k)^S)(n) \)proof
fix \( n \)
assume A2: \( n\in \mathbb{Z} \)
with A1, T1, T2 have \( ((m^S) + (k^S))(n) = (m + k)\cdot n \) using Int_ZF_2_1_L12B, Int_ZF_2_5_L1, Int_ZF_1_1_L1
also
from T1, A2 have \( \ldots = ((m + k)^S)(n) \) using Int_ZF_2_5_L1
finally show \( ((m^S) + (k^S))(n) = ((m + k)^S)(n) \)
qed
ultimately show \( (m^S) + (k^S) = ((m + k)^S) \) using fun_extension_iff
qed

The composition of embeddings is the embeding of the product.

lemma (in int1) Int_ZF_2_5_L3B:

assumes A1: \( m\in \mathbb{Z} \), \( k\in \mathbb{Z} \)

shows \( (m^S) \circ (k^S) = ((m\cdot k)^S) \)proof
from A1 have T1: \( m\cdot k \in \mathbb{Z} \) using Int_ZF_1_1_L5
with A1 have T2: \( (m^S) \in \mathcal{S} \), \( (k^S) \in \mathcal{S} \), \( (m\cdot k)^S \in \mathcal{S} \), \( (m^S) \circ (k^S) \in \mathcal{S} \) using Int_ZF_2_5_L1, Int_ZF_2_1_L11
then have \( (m^S) \circ (k^S) : \mathbb{Z} \rightarrow \mathbb{Z} \), \( (m\cdot k)^S : \mathbb{Z} \rightarrow \mathbb{Z} \) using AlmostHoms_def
moreover
have \( \forall n\in \mathbb{Z} .\ ((m^S) \circ (k^S))(n) = ((m\cdot k)^S)(n) \)proof
fix \( n \)
assume A2: \( n\in \mathbb{Z} \)
with A1, T2 have \( ((m^S) \circ (k^S))(n) = (m^S)(k\cdot n) \) using Int_ZF_2_1_L10, Int_ZF_2_5_L1
moreover
from A1, A2 have \( k\cdot n \in \mathbb{Z} \) using Int_ZF_1_1_L5
with A1, A2 have \( (m^S)(k\cdot n) = m\cdot k\cdot n \) using Int_ZF_2_5_L1, Int_ZF_1_1_L7
ultimately have \( ((m^S) \circ (k^S))(n) = m\cdot k\cdot n \)
also
from T1, A2 have \( m\cdot k\cdot n = ((m\cdot k)^S)(n) \) using Int_ZF_2_5_L1
finally show \( ((m^S) \circ (k^S))(n) = ((m\cdot k)^S)(n) \)
qed
ultimately show \( (m^S) \circ (k^S) = ((m\cdot k)^S) \) using fun_extension_iff
qed

Embedding integers in slopes preserves order.

lemma (in int1) Int_ZF_2_5_L4:

assumes A1: \( m\leq n \)

shows \( (m^S) \sim (n^S) \vee (n^S) + ( - (m^S)) \in \mathcal{S} _+ \)proof
from A1 have \( m^S \in \mathcal{S} \) and \( n^S \in \mathcal{S} \) using Int_ZF_2_L1A, Int_ZF_2_5_L1
moreover
from A1 have \( \forall k\in \mathbb{Z} _+.\ (m^S)(k) \leq (n^S)(k) \) using Int_ZF_1_3_L13B, Int_ZF_2_L1A, PositiveSet_def, Int_ZF_2_5_L1
ultimately show \( thesis \) using Int_ZF_2_3_L4C
qed

We aim at showing that \(m\mapsto m^S\) is an injection modulo the relation of almost equality. To do that we first show that if \(m^S\) has finite range, then \(m=0\).

lemma (in int1) Int_ZF_2_5_L5:

assumes \( m\in \mathbb{Z} \) and \( m^S \in \text{FinRangeFunctions}(\mathbb{Z} ,\mathbb{Z} ) \)

shows \( m= 0 \) using assms, FinRangeFunctions_def, Int_ZF_2_5_L1, AlmostHoms_def, func_imagedef, Int_ZF_1_6_L8

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

lemma (in int1) Int_ZF_2_5_L6:

assumes A1: \( m\in \mathbb{Z} \), \( k\in \mathbb{Z} \) and A2: \( (m^S) \sim (k^S) \)

shows \( m=k \)proof
from A1 have T: \( m - k \in \mathbb{Z} \) using Int_ZF_1_1_L5
from A1 have \( ( - (k^S)) = (( - k)^S) \) using Int_ZF_2_5_L3
then have \( m^S + ( - (k^S)) = (m^S) + (( - k)^S) \)
with A1 have \( m^S + ( - (k^S)) = ((m - k)^S) \) using Int_ZF_1_1_L4, Int_ZF_2_5_L3A
moreover
from A1, A2 have \( m^S + ( - (k^S)) \in \text{FinRangeFunctions}(\mathbb{Z} ,\mathbb{Z} ) \) using Int_ZF_2_5_L1, Int_ZF_2_1_L9D
ultimately have \( (m - k)^S \in \text{FinRangeFunctions}(\mathbb{Z} ,\mathbb{Z} ) \)
with T have \( m - k = 0 \) using Int_ZF_2_5_L5
with A1 show \( m=k \) by (rule Int_ZF_1_L15 )
qed

Embedding of \(1\) is the identity slope and embedding of zero is a finite range function.

lemma (in int1) Int_ZF_2_5_L7:

shows \( 1 ^S = id(\mathbb{Z} ) \), \( 0 ^S \in \text{FinRangeFunctions}(\mathbb{Z} ,\mathbb{Z} ) \)proof
have \( id(\mathbb{Z} ) = \{\langle x,x\rangle .\ x\in \mathbb{Z} \} \) using id_def
then show \( 1 ^S = id(\mathbb{Z} ) \) using Int_ZF_1_1_L4
have \( \{ 0 ^S(n).\ n\in \mathbb{Z} \} = \{ 0 \cdot n.\ n\in \mathbb{Z} \} \) using int_zero_one_are_int, Int_ZF_2_5_L1
also
have \( \ldots = \{ 0 \} \) using Int_ZF_1_1_L4, int_not_empty
finally have \( \{ 0 ^S(n).\ n\in \mathbb{Z} \} = \{ 0 \} \)
then have \( \{ 0 ^S(n).\ n\in \mathbb{Z} \} \in Fin(\mathbb{Z} ) \) using int_zero_one_are_int, Finite1_L16
moreover
have \( 0 ^S: \mathbb{Z} \rightarrow \mathbb{Z} \) using int_zero_one_are_int, Int_ZF_2_5_L1, AlmostHoms_def
ultimately show \( 0 ^S \in \text{FinRangeFunctions}(\mathbb{Z} ,\mathbb{Z} ) \) using Finite1_L19
qed

A somewhat technical condition for a embedding of an integer to be "less or equal" (in the sense apriopriate for slopes) than the composition of a slope and another integer (embedding).

lemma (in int1) Int_ZF_2_5_L8:

assumes A1: \( f \in \mathcal{S} \) and A2: \( N \in \mathbb{Z} \), \( M \in \mathbb{Z} \) and A3: \( \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} _+ \)proof
from A1, A2 have \( M^S \in \mathcal{S} \), \( f\circ (N^S) \in \mathcal{S} \) using Int_ZF_2_5_L1, Int_ZF_2_1_L11
moreover
from A1, A2, A3 have \( \forall n\in \mathbb{Z} _+.\ (M^S)(n) \leq (f\circ (N^S))(n) \) using Int_ZF_2_5_L1, PositiveSet_def, Int_ZF_2_1_L10
ultimately show \( thesis \) using Int_ZF_2_3_L4C
qed

Another technical condition for the composition of a slope and an integer (embedding) to be "less or equal" (in the sense apriopriate for slopes) than embedding of another integer.

lemma (in int1) Int_ZF_2_5_L9:

assumes A1: \( f \in \mathcal{S} \) and A2: \( N \in \mathbb{Z} \), \( M \in \mathbb{Z} \) and A3: \( \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} _+ \)proof
from A1, A2 have \( f\circ (N^S) \in \mathcal{S} \), \( M^S \in \mathcal{S} \) using Int_ZF_2_5_L1, Int_ZF_2_1_L11
moreover
from A1, A2, A3 have \( \forall n\in \mathbb{Z} _+.\ (f\circ (N^S))(n) \leq (M^S)(n) \) using Int_ZF_2_5_L1, PositiveSet_def, Int_ZF_2_1_L10
ultimately show \( thesis \) using Int_ZF_2_3_L4C
qed
end
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)\} \)
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 func_imagedef:

assumes \( f:X\rightarrow Y \) and \( A\subseteq X \)

shows \( f(A) = \{f(x).\ x \in A\} \)
lemma (in int0) Int_ZF_1_5_L3: shows \( m\in \mathbb{Z} _+ \longleftrightarrow 1 \leq m \)
lemma (in int1) Int_ZF_2_1_L8:

assumes \( s\in \mathcal{S} \)

shows \( abs(s( 0 )) \leq \text{ max}\delta (s) \), \( 0 \leq \text{ max}\delta (s) \), \( abs(s( 0 )) \in \mathbb{Z} \), \( \text{ max}\delta (s) \in \mathbb{Z} \), \( abs(s( 0 )) + \text{ max}\delta (s) \in \mathbb{Z} \)
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 int0) Int_ZF_2_L15D:

assumes \( 0 \leq n \), \( m\in \mathbb{Z} \)

shows \( m \leq n + m \)
lemma (in int0) int_two_three_are_int: shows \( 2 \in \mathbb{Z} \), \( 3 \in \mathbb{Z} \)
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 int0) Int_ZF_1_5_L2A:

assumes \( A \subseteq \mathbb{Z} _+ \) and \( A \notin Fin(\mathbb{Z} ) \) and \( D\in \mathbb{Z} \)

shows \( \exists n\in A.\ D\leq n \)
lemma (in int1) Int_ZF_2_3_L1A:

assumes \( f\in \mathcal{S} _+ \) and \( \exists n \in f(\mathbb{Z} _+) \cap \mathbb{Z} _+.\ a\leq n \)

shows \( \exists M\in \mathbb{Z} _+.\ a \leq f(M) \)
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 int0) int_zero_one_are_int: shows \( 0 \in \mathbb{Z} \), \( 1 \in \mathbb{Z} \)
lemma (in int1) Int_ZF_2_1_L7:

assumes \( s\in \mathcal{S} \) and \( n\in \mathbb{Z} \), \( m\in \mathbb{Z} \)

shows \( abs(\delta (s,m,n)) \leq \text{ max}\delta (s) \), \( \delta (s,m,n) \in \mathbb{Z} \), \( \text{ max}\delta (s) \in \mathbb{Z} \), \( ( - \text{ max}\delta (s)) \leq \delta (s,m,n) \)
lemma (in int0) Int_ZF_2_L16C:

assumes \( 1 \leq a \)

shows \( 0 \leq a \), \( a\neq 0 \), \( 2 \leq a + 1 \), \( 1 \leq a + 1 \), \( 0 \leq a + 1 \)
lemma (in int0) Int_ZF_1_3_L19A:

assumes \( m\in \mathbb{Z} \) and \( abs(m) \leq n \) and \( 0 \leq k \)

shows \( ( - (n + k)) \leq m \)
lemma (in int0) int_ineq_add_sides:

assumes \( a\leq b \) and \( c\leq d \)

shows \( a + c \leq b + d \), \( a - d \leq b - c \)
lemma (in int0) Int_ZF_1_1_L1:

assumes \( a\in \mathbb{Z} \), \( b\in \mathbb{Z} \), \( c\in \mathbb{Z} \)

shows \( a\cdot (b + c) = a\cdot b + a\cdot c \), \( (b + c)\cdot a = b\cdot a + c\cdot a \)
lemma (in int0) Int_ZF_1_2_L11:

assumes \( a\in \mathbb{Z} \)

shows \( a + 1 + 2 = a + 3 \), \( a = 2 \cdot a - a \)
lemma (in int1) Int_ZF_2_1_L13:

assumes \( s\in \mathcal{S} \) and \( n\in \mathbb{Z} \), \( m\in \mathbb{Z} \)

shows \( s(n\cdot m) + (s(m) + \delta (s,n\cdot m,m)) = s((n + 1 )\cdot m) \)
theorem (in int0) Induction_on_int:

assumes \( i\leq k \) and \( Q(i) \) and \( \forall m.\ i\leq m \wedge Q(m) \longrightarrow Q(m + 1 ) \)

shows \( Q(k) \)
lemma (in int0) Int_ZF_1_3_L13A:

assumes \( 1 \leq a \) and \( b\leq c \) and \( (a + 1 )\cdot c \leq d \)

shows \( (a + 1 )\cdot b \leq d \)
lemma (in int0) int_one_two_are_pos: shows \( 1 \in \mathbb{Z} _+ \), \( 2 \in \mathbb{Z} _+ \)
lemma (in int1) Arthan_Lem_3:

assumes \( f\in \mathcal{S} _+ \) and \( D \in \mathbb{Z} _+ \)

shows \( \exists M\in \mathbb{Z} _+.\ \forall m\in \mathbb{Z} _+.\ (m + 1 )\cdot D \leq f(m\cdot M) \)
lemma (in int1) Int_ZF_2_1_L1: shows \( group1(\mathbb{Z} ,IntegerAddition) \)
lemma (in group1) Group_ZF_3_3_L1: shows \( FR \subseteq AH \)
lemma Finite1_L21:

assumes \( f \in \text{FinRangeFunctions}(X,Y) \) and \( A\subseteq X \)

shows \( f(A) \in Fin(Y) \)
lemma func1_1_L6:

assumes \( f:X\rightarrow Y \)

shows \( f(B) \subseteq \text{range}(f) \) and \( f(B) \subseteq Y \)
theorem (in int0) Int_ZF_2_T1: shows \( \text{IsAnOrdGroup}(\mathbb{Z} ,IntegerAddition,IntegerOrder) \), \( IntegerOrder \text{ is total on } \mathbb{Z} \), \( group3(\mathbb{Z} ,IntegerAddition,IntegerOrder) \), \( \text{IsLinOrder}(\mathbb{Z} ,IntegerOrder) \)
lemma (in group3) OrderedGroup_ZF_2_L4:

assumes \( r \text{ is total on } G \) and \( A\subseteq G \) and \( A \cap G_+ \in Fin(G) \)

shows \( \text{IsBoundedAbove}(A,r) \)
theorem Int_ZF_1_T2: shows \( \text{IsAgroup}(int,IntegerAddition) \), \( IntegerAddition \text{ is commutative on } int \), \( group0(int,IntegerAddition) \)
theorem group0_2_T2:

assumes \( \text{IsAgroup}(G,f) \)

shows \( \text{GroupInv}(G,f) : G\rightarrow G \)
lemma func1_1_L15C:

assumes \( f:X\rightarrow Y \) and \( g:Y\rightarrow Z \) and \( A\subseteq X \)

shows \( g(f(A)) = \{g(f(x)).\ x\in A\} \), \( g(f(A)) = (g\circ f)(A) \)
lemma (in int1) Int_ZF_2_1_L12:

assumes \( s\in \mathcal{S} \)

shows \( - s \in \mathcal{S} \)
lemma (in int1) Int_ZF_2_3_L2:

assumes \( f\in \mathcal{S} \) and \( f \notin \mathcal{S} _+ \)

shows \( \text{IsBoundedAbove}(f(\mathbb{Z} _+), IntegerOrder) \)
lemma (in group3) OrderedGroup_ZF_2_L5:

assumes \( A\subseteq G \) and \( \text{IsBoundedAbove}(-A,r) \)

shows \( \text{IsBoundedBelow}(A,r) \)
lemma (in int1) Int_ZF_2_1_L2B:

assumes \( f\in \mathcal{S} \) and \( m\in \mathbb{Z} \)

shows \( f(m) \in \mathbb{Z} \)
lemma (in int0) int_abs_nonneg:

assumes \( m\in \mathbb{Z} \)

shows \( abs(m) \in \mathbb{Z} ^+ \), \( 0 \leq abs(m) \)
lemma (in int0) Int_order_transitive:

assumes \( m\leq n \), \( n\leq k \)

shows \( m\leq k \)
lemma (in int0) Int_ZF_2_L15F:

assumes \( m\leq k \) and \( 0 \leq n \)

shows \( m \leq k + n \), \( m \leq n + k \)
lemma (in int0) Int_ZF_1_3_L5A:

assumes \( 0 \leq a \)

shows \( 0 \leq 2 \cdot a \)
lemma (in int1) Int_ZF_2_1_L14:

assumes \( s\in \mathcal{S} \) and \( m\in \mathbb{Z} \)

shows \( s( - m) = s( 0 ) - \delta (s,m, - m) - s(m) \), \( abs(s(m) + s( - m)) \leq 2 \cdot \text{ max}\delta (s) \), \( abs(s( - m)) \leq 2 \cdot \text{ max}\delta (s) + abs(s(m)) \), \( s( - m) \leq abs(s( 0 )) + \text{ max}\delta (s) - s(m) \)
lemma (in int0) Int_ZF_2_L15A:

assumes \( b\in \mathbb{Z} \) and \( a\leq b + c \) and \( c\leq c_1 \)

shows \( a\leq b + c_1 \)
lemma (in int0) Int_ZF_2_L19B:

assumes \( m\in \mathbb{Z} \) and \( Q( 0 ) \) and \( \forall n\in \mathbb{Z} _+.\ Q(n) \) and \( \forall n\in \mathbb{Z} _+.\ Q( - n) \)

shows \( Q(m) \)
lemma (in int0) Int_ZF_1_3_L20A:

assumes \( \text{IsBounded}(A,IntegerOrder) \)

shows \( \exists L.\ \forall a\in A.\ abs(a) \leq L \)
lemma func1_1_L15B:

assumes \( f:X\rightarrow Y \) and \( A\subseteq X \) and \( \forall y\in f(A).\ P(y) \)

shows \( \forall x\in A.\ P(f(x)) \)
lemma (in int1) Int_ZF_2_3_L4:

assumes \( f\in \mathcal{S} \) and \( m\in \mathbb{Z} \) and \( \forall n\in \mathbb{Z} _+.\ abs(f(n)) \leq L \)

shows \( abs(f(m)) \leq 2 \cdot \text{ max}\delta (f) + L \)
corollary (in int0) Int_ZF_1_3_L20C:

assumes \( f:\mathbb{Z} \rightarrow \mathbb{Z} \) and \( \forall m\in \mathbb{Z} .\ abs(f(m)) \leq L \)

shows \( f(\mathbb{Z} ) \in Fin(\mathbb{Z} ) \)
Definition of FinRangeFunctions: \( \text{FinRangeFunctions}(X,Y) \equiv \{f:X\rightarrow Y.\ f(X) \in Fin(Y)\} \)
Definition of IsBounded: \( \text{IsBounded}(A,r) \equiv ( \text{IsBoundedAbove}(A,r) \wedge \text{IsBoundedBelow}(A,r)) \)
lemma (in int1) Int_ZF_2_3_L4A:

assumes \( f\in \mathcal{S} \) and \( \text{IsBounded}(f(\mathbb{Z} _+), IntegerOrder) \)

shows \( f \in \text{FinRangeFunctions}(\mathbb{Z} ,\mathbb{Z} ) \)
lemma (in int1) Int_ZF_2_1_L12C:

assumes \( s\in \mathcal{S} \), \( r\in \mathcal{S} \)

shows \( s + r \in \mathcal{S} \)
lemma (in int0) Int_ZF_1_3_L10A:

assumes \( a\leq b \)

shows \( 0 \leq b - a \)
lemma (in int1) Int_ZF_2_1_L12B:

assumes \( s\in \mathcal{S} \), \( r\in \mathcal{S} \) and \( m\in \mathbb{Z} \)

shows \( (s + r)(m) = s(m) + r(m) \)
lemma (in int1) Int_ZF_2_1_L12A:

assumes \( s\in \mathcal{S} \) and \( m\in \mathbb{Z} \)

shows \( ( - s)(m) = - (s(m)) \)
lemma func_ZF_8_L1:

assumes \( f:X\rightarrow Y \) and \( A\subseteq X \) and \( \forall x\in A.\ \langle L,f(x)\rangle \in r \)

shows \( \text{IsBoundedBelow}(f(A),r) \)
lemma (in int1) Int_ZF_2_3_L4B:

assumes \( f\in \mathcal{S} \) and \( \text{IsBoundedBelow}(f(\mathbb{Z} _+), IntegerOrder) \)

shows \( f \in \text{FinRangeFunctions}(\mathbb{Z} ,\mathbb{Z} ) \vee f\in \mathcal{S} _+ \)
lemma (in int1) Int_ZF_2_1_L9C:

assumes \( s\in \mathcal{S} \), \( r\in \mathcal{S} \) and \( s + ( - r) \in \text{FinRangeFunctions}(\mathbb{Z} ,\mathbb{Z} ) \)

shows \( s \sim r \), \( r \sim s \)
corollary (in int1) Arthan_L_3_spec:

assumes \( f \in \mathcal{S} _+ \)

shows \( \exists M\in \mathbb{Z} _+.\ \forall n\in \mathbb{Z} _+.\ n + 1 \leq f(n\cdot M) \)
lemma (in int1) Int_ZF_2_1_L15:

assumes \( s\in \mathcal{S} \) and \( M \in \mathbb{Z} _+ \)

shows \( maxf(s, 0 .\ .\ (M - 1 )) \in \mathbb{Z} \), \( \forall n \in 0 .\ .\ (M - 1 ).\ s(n) \leq maxf(s, 0 .\ .\ (M - 1 )) \), \( minf(s, 0 .\ .\ (M - 1 )) \in \mathbb{Z} \), \( \forall n \in 0 .\ .\ (M - 1 ).\ minf(s, 0 .\ .\ (M - 1 )) \leq s(n) \)
lemma (in int0) Int_ZF_1_3_L18:

assumes \( m\in \mathbb{Z} \), \( n\in \mathbb{Z} \)

shows \( m \leq \text{GreaterOf}(IntegerOrder,m,n) \), \( n \leq \text{GreaterOf}(IntegerOrder,m,n) \), \( \text{SmallerOf}(IntegerOrder,m,n) \leq m \), \( \text{SmallerOf}(IntegerOrder,m,n) \leq n \)
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 int0) IntDiv_ZF_1_L5:

assumes \( n \in \mathbb{Z} _+ \) and \( n \leq k \) and \( k\cdot n \leq m \)

shows \( m = n\cdot (m\text{ zdiv }n) + (m\text{ zmod }n) \), \( m = (m\text{ zdiv }n)\cdot n + (m\text{ zmod }n) \), \( (m\text{ zmod }n) \in 0 .\ .\ (n - 1 ) \), \( k \leq (m\text{ zdiv }n) \), \( m\text{ zdiv }n \in \mathbb{Z} _+ \)
lemma (in int0) int_ord_transl_inv:

assumes \( k \in \mathbb{Z} \) and \( m \leq n \)

shows \( m + k \leq n + k \), \( k + m\leq k + n \)
lemma (in int1) Int_ZF_2_1_L16:

assumes \( s\in \mathcal{S} \) and \( m\in \mathbb{Z} \) and \( M \in \mathbb{Z} _+ \) and \( k \in 0 .\ .\ (M - 1 ) \)

shows \( s(m\cdot M) + (minf(s, 0 .\ .\ (M - 1 )) - \text{ max}\delta (s)) \leq s(m\cdot M + k) \)
lemma (in int1) Int_ZF_2_3_L5:

assumes \( f\in \mathcal{S} _+ \) and \( K\in \mathbb{Z} \)

shows \( \exists N\in \mathbb{Z} _+.\ \forall m.\ N\leq m \longrightarrow K \leq f(m) \)
lemma (in int0) Int_ZF_2_L10:

assumes \( k \leq i \)

shows \( ( - i) \leq ( - k) \), \( \ \$\!-\!i \leq \ \$\!-\!k \)
lemma (in int0) Int_ZF_1_2_L3:

assumes \( a\in \mathbb{Z} \), \( b\in \mathbb{Z} \)

shows \( a + b - a = b \), \( a + (b - a) = b \), \( a + b - b = a \), \( a - b + b = a \), \( ( - a) + (a + b) = b \), \( a + (b - a) = b \), \( ( - b) + (a + b) = a \), \( a - (b + a) = - b \), \( a - (a + b) = - b \), \( a - (a - b) = b \), \( a - b - a = - b \), \( a - b - (a + b) = ( - b) - b \)
lemma (in int0) int_ord_is_refl: shows \( \text{refl}(\mathbb{Z} ,IntegerOrder) \)
lemma func1_1_L15D:

assumes \( f:X\rightarrow Y \), \( x\in A \), \( A\subseteq X \)

shows \( f(x) \in f(A) \)
lemma (in int0) Int_ZF_4_L9:

assumes \( \forall m\in \mathbb{Z} .\ \exists k\in A.\ m\leq k \)

shows \( \neg \text{IsBoundedAbove}(A,IntegerOrder) \), \( A \notin Fin(\mathbb{Z} ) \)
lemma (in int1) Int_ZF_2_3_L3:

assumes \( f\in \mathcal{S} \) and \( - f \notin \mathcal{S} _+ \)

shows \( \text{IsBoundedBelow}(f(\mathbb{Z} _+), IntegerOrder) \)
corollary (in int1) Int_ZF_2_3_L6:

assumes \( f\in \mathcal{S} _+ \)

shows \( \exists N\in \mathbb{Z} _+.\ \forall m.\ N\leq m \longrightarrow f(m) \in \mathbb{Z} _+ \)
lemma (in int0) Int_ZF_1_5_L8:

assumes \( a \in \mathbb{Z} _+ \)

shows \( ( - a) \notin \mathbb{Z} _+ \)
Definition of Xor: \( p \text{ Xor } q \equiv (p\vee q) \wedge \neg (p \wedge q) \)
Definition of GreaterOf: \( \text{GreaterOf}(r,a,b) \equiv (\text{if }\langle a,b\rangle \in r\text{ then }b\text{ else }a) \)
lemma (in int1) Int_ZF_2_3_L7:

assumes \( f\in \mathcal{S} \) and \( \forall K\in \mathbb{Z} .\ \exists n\in \mathbb{Z} _+.\ K \leq f(n) \)

shows \( f \in \mathcal{S} _+ \)
corollary (in int1) Int_ZF_2_3_L6A:

assumes \( f\in \mathcal{S} _+ \) and \( K\in \mathbb{Z} \)

shows \( \exists N\in \mathbb{Z} _+.\ K \leq f(N) \)
lemma (in int1) Int_ZF_2_1_L10:

assumes \( s\in \mathcal{S} \), \( r\in \mathcal{S} \) and \( m\in \mathbb{Z} \)

shows \( (s\circ r)(m) = s(r(m)) \), \( s(r(m)) \in \mathbb{Z} \)
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_1_L9A:

assumes \( s \sim r \)

shows \( \exists L\in \mathbb{Z} .\ \forall m\in \mathbb{Z} .\ abs(s(m) - r(m)) \leq L \), \( s\in \mathcal{S} \), \( r\in \mathcal{S} \)
lemma (in int0) Int_ZF_2_L9B:

assumes \( i\in \mathbb{Z} \), \( m\in \mathbb{Z} \), \( k\in \mathbb{Z} \)

shows \( i + m \leq k \longleftrightarrow i \leq k - m \)
lemma (in int0) Int_triangle_ineq2:

assumes \( m\in \mathbb{Z} \), \( n\in \mathbb{Z} \) and \( abs(m - n) \leq k \)

shows \( abs(m) \leq abs(n) + k \), \( m - k \leq n \), \( m \leq n + k \), \( n - k \leq m \)
lemma (in int1) Int_ZF_2_1_L9B: shows \( AlEqRel \subseteq \mathcal{S} \times \mathcal{S} \), \( \text{equiv}(\mathcal{S} ,AlEqRel) \)
lemma (in int1) Int_ZF_2_3_L9:

assumes \( f \in \mathcal{S} _+ \) and \( \langle f,g\rangle \in AlEqRel \)

shows \( g \in \mathcal{S} _+ \)
lemma EquivClass_3_L3:

assumes \( \text{equiv}(X,r) \) and \( r \subseteq X\times X \) and \( A\subseteq X \) and \( \forall x\in A.\ \forall y\in X.\ \langle x,y\rangle \in r \longrightarrow y\in A \)

shows \( \text{IsSaturated}(r,A) \)
lemma (in int1) pos_slopes_saturated: shows \( \text{IsSaturated}(AlEqRel,\mathcal{S} _+) \)
lemma EquivClass_3_L7:

assumes \( \text{equiv}(X,r) \) and \( \text{IsSaturated}(r,A) \) and \( A\subseteq X \) and \( x\in X \), \( y\in X \) and \( B = \{r\{x\}.\ x\in A\} \) and \( (x\in A) \text{ Xor } (y\in A) \)

shows \( (r\{x\} \in B) \text{ Xor } (r\{y\} \in B) \)
lemma (in int0) Int_ZF_1_5_L9:

assumes \( a\in \mathbb{Z} \)

shows \( \exists b\in \mathbb{Z} _+.\ a\leq b \)
lemma (in int1) Int_ZF_2_1_L17: shows \( id(\mathbb{Z} ) \in \mathcal{S} \)
lemma (in int1) Int_ZF_2_3_L11: shows \( id(\mathbb{Z} ) \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 int0) Int_ZF_1_5_L1C:

assumes \( A \subseteq \mathbb{Z} _+ \) and \( A \neq 0 \)

shows \( \text{HasAminimum}(IntegerOrder,A) \), \( \text{Minimum}(IntegerOrder,A) \in A \), \( \forall x\in A.\ \text{Minimum}(IntegerOrder,A) \leq x \)
lemma (in int1) Int_ZF_2_4_L1:

assumes \( f \in \mathcal{S} _+ \) and \( p\in \mathbb{Z} _+ \) and \( A = \{n\in \mathbb{Z} _+.\ p \leq f(n)\} \)

shows \( A \subseteq \mathbb{Z} _+ \), \( A \neq 0 \), \( f^{-1}(p) \in A \), \( \forall m\in A.\ f^{-1}(p) \leq m \)
lemma (in int1) Int_ZF_2_4_L2:

assumes \( f \in \mathcal{S} _+ \) and \( p\in \mathbb{Z} _+ \)

shows \( f^{-1}(p) \in \mathbb{Z} _+ \), \( p \leq f(f^{-1}(p)) \)
lemma (in int1) Int_ZF_2_3_L1:

assumes \( f\in \mathcal{S} _+ \)

shows \( f:\mathbb{Z} \rightarrow \mathbb{Z} \)
lemma (in int1) Int_ZF_2_4_L3:

assumes \( f \in \mathcal{S} _+ \) and \( m\in \mathbb{Z} _+ \), \( p\in \mathbb{Z} _+ \) and \( m \leq f(p) \)

shows \( f^{-1}(m) \leq p \)
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 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 int0) Int_ZF_1_5_L7:

assumes \( a \in \mathbb{Z} _+ \) and \( a\leq b \)

shows \( b \in \mathbb{Z} _+ \)
lemma (in int0) Int_ZF_1_5_L7A:

assumes \( a\in \mathbb{Z} \), \( b \in \mathbb{Z} _+ \)

shows \( a \leq a + b \), \( a \neq a + b \), \( a + b \in \mathbb{Z} \)
lemma (in int1) Int_ZF_2_4_L5:

assumes \( f \in \mathcal{S} _+ \) and \( m\in \mathbb{Z} _+ \) and \( m\leq n \)

shows \( f^{-1}(m) \leq f^{-1}(n) \)
lemma (in int1) Int_ZF_2_1_L28:

assumes \( s\in \mathcal{S} \)

shows \( \exists M\in \mathbb{Z} .\ \forall m\in \mathbb{Z} .\ s(m) \leq s(m - 1 ) + M \)
lemma (in int1) Int_ZF_2_1_L30:

assumes \( s\in \mathcal{S} \)

shows \( \exists M\in \mathbb{Z} .\ \forall m\in \mathbb{Z} .\ \forall n\in \mathbb{Z} .\ \forall k\in \mathbb{Z} .\ s(m - n - k) \leq s(m) - s(n) - s(k) + M \), \( \exists K\in \mathbb{Z} .\ \forall m\in \mathbb{Z} .\ \forall n\in \mathbb{Z} .\ \forall k\in \mathbb{Z} .\ s(m) - s(n) - s(k) + K \leq s(m - n - k) \)
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 int1) Int_ZF_2_4_L4:

assumes \( f \in \mathcal{S} _+ \) and \( m\in \mathbb{Z} _+ \) and \( f^{-1}(m) - 1 \in \mathbb{Z} _+ \)

shows \( f(f^{-1}(m) - 1 ) \leq m \), \( f(f^{-1}(m) - 1 ) \neq m \)
lemma (in int0) Int_ZF_1_2_L9:

assumes \( a\in \mathbb{Z} \), \( b\in \mathbb{Z} \), \( c\in \mathbb{Z} \)

shows \( (a - b) + (b - c) = a - c \), \( (a - b) - (a - c) = c - b \), \( a + (b + (c - a - b)) = c \), \( ( - a) - b + c = c - a - b \), \( ( - b) - a + c = c - a - b \), \( ( - (( - a) + b + c)) = a - b - c \), \( a + b + c - a = b + c \), \( a + b - (a + c) = b - c \)
lemma (in int1) Int_ZF_2_4_L7:

assumes \( f \in \mathcal{S} _+ \) and \( \forall m\in \mathbb{Z} _+.\ f^{-1}(m) - 1 \in \mathbb{Z} _+ \)

shows \( \exists U\in \mathbb{Z} .\ \forall m\in \mathbb{Z} _+.\ \forall n\in \mathbb{Z} _+.\ f(f^{-1}(m + n) - f^{-1}(m) - f^{-1}(n)) \leq U \), \( \exists N\in \mathbb{Z} .\ \forall m\in \mathbb{Z} _+.\ \forall n\in \mathbb{Z} _+.\ N \leq f(f^{-1}(m + n) - f^{-1}(m) - f^{-1}(n)) \)
lemma (in int1) Int_ZF_2_3_L5A:

assumes \( f\in \mathcal{S} _+ \) and \( K\in \mathbb{Z} \)

shows \( \exists N\in \mathbb{Z} _+.\ \forall m.\ N\leq m \longrightarrow f( - m) \leq K \)
lemma (in int0) Int_ZF_1_6_L4:

assumes \( X\neq 0 \) and \( f: \mathbb{Z} \rightarrow \mathbb{Z} \) and \( \forall a\in \mathbb{Z} .\ \exists b\in \mathbb{Z} _+.\ \forall x.\ b\leq x \longrightarrow a \leq f(x) \) and \( \forall a\in \mathbb{Z} .\ \exists b\in \mathbb{Z} _+.\ \forall y.\ b\leq y \longrightarrow f( - y) \leq a \) and \( \forall x\in X.\ b(x) \in \mathbb{Z} \wedge f(b(x)) \leq U \wedge L \leq f(b(x)) \)

shows \( \exists M.\ \forall x\in X.\ abs(b(x)) \leq M \)
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 (in int1) Int_ZF_2_4_L9:

assumes \( f \in \mathcal{S} _+ \) and \( g = \{\langle p,f^{-1}(p)\rangle .\ p\in \mathbb{Z} _+\} \)

shows \( g : \mathbb{Z} _+\rightarrow \mathbb{Z} _+ \), \( g : \mathbb{Z} _+\rightarrow \mathbb{Z} \)
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 int1) Int_ZF_2_4_L8:

assumes \( f \in \mathcal{S} _+ \) and \( \forall m\in \mathbb{Z} _+.\ f^{-1}(m) - 1 \in \mathbb{Z} _+ \)

shows \( \exists M.\ \forall x\in \mathbb{Z} _+\times \mathbb{Z} _+.\ abs(\varepsilon (f,x)) \leq M \)
lemma (in int1) Int_ZF_2_4_L10:

assumes \( f \in \mathcal{S} _+ \) and \( g = \{\langle p,f^{-1}(p)\rangle .\ p\in \mathbb{Z} _+\} \) and \( p\in \mathbb{Z} _+ \)

shows \( g(p) = f^{-1}(p) \)
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 int1) Int_ZF_2_4_L11:

assumes \( f \in \mathcal{S} _+ \) and \( \forall m\in \mathbb{Z} _+.\ f^{-1}(m) - 1 \in \mathbb{Z} _+ \) and \( g = \{\langle p,f^{-1}(p)\rangle .\ p\in \mathbb{Z} _+\} \)

shows \( \text{OddExtension}(\mathbb{Z} ,IntegerAddition,IntegerOrder,g) \in \mathcal{S} \)
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 int1) Int_ZF_2_1_L32:

assumes \( s\in \mathcal{S} \), \( M\in \mathbb{Z} \) and \( \forall m\in \mathbb{Z} _+.\ m \leq s(m) \wedge s(m) \leq m + M \)

shows \( s \sim id(\mathbb{Z} ) \)
lemma (in int0) Int_ZF_1_6_L7:

assumes \( f: \mathbb{Z} \rightarrow \mathbb{Z} \) and \( K\in \mathbb{Z} \), \( N\in \mathbb{Z} \) and \( \forall a\in \mathbb{Z} .\ \exists b\in \mathbb{Z} _+.\ \forall x.\ b\leq x \longrightarrow a \leq f(x) \)

shows \( \exists C\in \mathbb{Z} .\ N \leq \text{Minimum}(IntegerOrder,\{n\in \mathbb{Z} _+.\ K \leq f(n) + C\}) \)
lemma (in int1) Int_ZF_2_1_L33:

assumes \( s\in \mathcal{S} \) and \( c\in \mathbb{Z} \) and \( r = \{\langle m,s(m) + c\rangle .\ m\in \mathbb{Z} \} \)

shows \( \forall m\in \mathbb{Z} .\ r(m) = s(m) + c \), \( r\in \mathcal{S} \), \( s \sim r \)
lemma (in int1) Int_ZF_2_4_L12:

assumes \( f \in \mathcal{S} _+ \) and \( \forall m\in \mathbb{Z} _+.\ f^{-1}(m) - 1 \in \mathbb{Z} _+ \)

shows \( \exists h\in \mathcal{S} .\ f\circ h \sim id(\mathbb{Z} ) \)
lemma (in int0) Int_ZF_2_L18: shows \( abs( 0 ) = 0 \)
lemma (in int1) Int_ZF_2_1_L5:

assumes \( f:\mathbb{Z} \rightarrow \mathbb{Z} \) and \( \forall m\in \mathbb{Z} .\ \forall n\in \mathbb{Z} .\ abs(\delta (f,m,n)) \leq L \)

shows \( f\in \mathcal{S} \)
lemma (in int1) Arthan_Lem_8:

assumes \( f\in \mathcal{S} \)

shows \( \exists A B.\ A\in \mathbb{Z} \wedge B\in \mathbb{Z} \wedge (\forall p\in \mathbb{Z} .\ abs(f(p)) \leq A\cdot abs(p) + B) \)
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 int0) Int_ZF_2_L19C:

assumes \( m\in \mathbb{Z} \)

shows \( m \leq abs(m) \), \( ( - m) \leq abs(m) \)
lemma (in int0) Int_ZF_1_5_L4A:

assumes \( a\in \mathbb{Z} _+ \)

shows \( abs(a) = a \)
lemma (in int1) Int_ZF_2_3_L4C:

assumes \( f\in \mathcal{S} \), \( g\in \mathcal{S} \) and \( \forall n\in \mathbb{Z} _+.\ f(n) \leq g(n) \)

shows \( f\sim g \vee g + ( - f) \in \mathcal{S} _+ \)
lemma (in int0) Int_ZF_1_1_L7:

assumes \( a\in \mathbb{Z} \), \( b\in \mathbb{Z} \), \( c\in \mathbb{Z} \)

shows \( a + b + c = a + (b + c) \), \( a\cdot b\cdot c = a\cdot (b\cdot c) \)
lemma (in int0) Int_ZF_1_3_L13B:

assumes \( a\leq b \) and \( c\in \mathbb{Z} _+ \)

shows \( a\cdot c \leq b\cdot c \), \( c\cdot a \leq c\cdot b \)
lemma (in int0) Int_ZF_1_6_L8:

assumes \( a\in \mathbb{Z} \) and \( \{a\cdot x.\ x\in \mathbb{Z} \} \in Fin(\mathbb{Z} ) \)

shows \( a = 0 \)
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 int1) Int_ZF_2_1_L9D:

assumes \( s \sim r \)

shows \( s + ( - r) \in \text{FinRangeFunctions}(\mathbb{Z} ,\mathbb{Z} ) \)
lemma (in int1) Int_ZF_2_5_L5:

assumes \( m\in \mathbb{Z} \) and \( m^S \in \text{FinRangeFunctions}(\mathbb{Z} ,\mathbb{Z} ) \)

shows \( m= 0 \)
lemma (in int0) Int_ZF_1_L15:

assumes \( m\in \mathbb{Z} \), \( n\in \mathbb{Z} \) and \( m - n = 0 \)

shows \( m=n \)
lemma (in int0) int_not_empty: shows \( \mathbb{Z} \neq 0 \)
lemma Finite1_L16:

assumes \( x\in X \)

shows \( \{x\} \in Fin(X) \)
lemma Finite1_L19:

assumes \( f:X\rightarrow Y \) and \( \{f(x).\ x\in X\} \in Fin(Y) \)

shows \( f \in \text{FinRangeFunctions}(X,Y) \)