IsarMathLib

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

theory Int_ZF_2 imports func_ZF_1 Int_ZF_1 IntDiv_ZF_IML Group_ZF_3
begin

In this theory file we consider the properties of integers that are needed for the real numbers construction in Real_ZF series.

Slopes

In this section we study basic properties of slopes - the integer almost homomorphisms. The general definition of an almost homomorphism \(f\) on a group \(G\) written in additive notation requires the set \(\{f(m+n) - f(m) - f(n): m,n\in G\}\) to be finite. In this section we establish a definition that is equivalent for integers: that for all integer \(m,n\) we have \(|f(m+n) - f(m) - f(n)| \leq L\) for some \(L\).

First we extend the standard notation for integers with notation related to slopes. We define slopes as almost homomorphisms on the additive group of integers. The set of slopes is denoted \( \mathcal{S} \). We also define "positive" slopes as those that take infinite number of positive values on positive integers. We write \( \delta (s,m,n) \) to denote the homomorphism difference of \(s\) at \(m,n\) (i.e the expression \(s(m+n) - s(m) - s(n)\)). We denote \( \text{ max}\delta (s) \) the maximum absolute value of homomorphism difference of \(s\) as \(m,n\) range over integers. If \(s\) is a slope, then the set of homomorphism differences is finite and this maximum exists. In Group_ZF_3 we define the equivalence relation on almost homomorphisms using the notion of a quotient group relation and use "\( \approx \)" to denote it. As here this symbol seems to be hogged by the standard Isabelle, we will use "\( \sim \)" instead "\( \approx \)". We show in this section that \(s\sim r\) iff for some \(L\) we have \(|s(m)-r(m)| \leq L\) for all integer \(m\). The "\( + \)" denotes the first operation on almost homomorphisms. For slopes this is addition of functions defined in the natural way. The "\( \circ \)" symbol denotes the second operation on almost homomorphisms (see Group_ZF_3 for definition), defined for the group of integers. In short "\( \circ \)" is the composition of slopes. The "\( ^{-1} \)" symbol acts as an infix operator that assigns the value \(\min\{n\in Z_+: p\leq f(n)\}\) to a pair (of sets) \(f\) and \(p\). In application \(f\) represents a function defined on \(Z_+\) and \(p\) is a positive integer. We choose this notation because we use it to construct the right inverse in the ring of classes of slopes and show that this ring is in fact a field. To study the homomorphism difference of the function defined by \(p\mapsto f^{-1}(p)\) we introduce the symbol \( \varepsilon \) defined as \(\varepsilon(f,\langle m,n \rangle ) = f^{-1}(m+n)-f^{-1}(m)-f^{-1}(n)\). Of course the intention is to use the fact that \(\varepsilon(f,\langle m,n \rangle )\) is the homomorphism difference of the function \(g\) defined as \(g(m) = f^{-1}(m)\). We also define \(\gamma (s,m,n)\) as the expression \(\delta(f,m,-n)+s(0)-\delta (f,n,-n)\). This is useful because of the identity \(f(m-n) = \gamma (m,n) + f(m)-f(n)\) that allows to obtain bounds on the value of a slope at the difference of of two integers. For every integer \(m\) we introduce notation \(m^S\) defined by \(m^E(n)=m\cdot n\). The mapping \(q\mapsto q^S\) embeds integers into \( \mathcal{S} \) preserving the order, (that is, maps positive integers into \( \mathcal{S} _+ \)).

locale int1 = int0 +

defines \( \mathcal{S} \equiv \text{AlmostHoms}(\mathbb{Z} ,IntegerAddition) \)

defines \( \mathcal{S} _+ \equiv \{s\in \mathcal{S} .\ s(\mathbb{Z} _+) \cap \mathbb{Z} _+ \notin Fin(\mathbb{Z} )\} \)

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

defines \( \text{ max}\delta (s) \equiv \text{Maximum}(IntegerOrder,\{abs(\delta (s,m,n)).\ \langle m,n\rangle \in \mathbb{Z} \times \mathbb{Z} \}) \)

defines \( AlEqRel \equiv \text{QuotientGroupRel}(\mathcal{S} , \text{AlHomOp1}(\mathbb{Z} ,IntegerAddition), \text{FinRangeFunctions}(\mathbb{Z} ,\mathbb{Z} )) \)

defines \( s \sim r \equiv \langle s,r\rangle \in AlEqRel \)

defines \( s + r \equiv \text{AlHomOp1}(\mathbb{Z} ,IntegerAddition)\langle s,r\rangle \)

defines \( s \circ r \equiv \text{AlHomOp2}(\mathbb{Z} ,IntegerAddition)\langle s,r\rangle \)

defines \( - s \equiv \text{GroupInv}(\mathbb{Z} ,IntegerAddition)\circ s \)

defines \( f^{-1}(p) \equiv \text{Minimum}(IntegerOrder,\{n\in \mathbb{Z} _+.\ p \leq f(n)\}) \)

defines \( \varepsilon (f,p) \equiv f^{-1}(\text{fst}(p) + \text{snd}(p)) - f^{-1}(\text{fst}(p)) - f^{-1}(\text{snd}(p)) \)

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

defines \( m^S \equiv \{\langle n,m\cdot n\rangle .\ n\in \mathbb{Z} \} \)

We can use theorems proven in the group1 context.

lemma (in int1) Int_ZF_2_1_L1:

shows \( group1(\mathbb{Z} ,IntegerAddition) \) using Int_ZF_1_T2, group1_axioms.intro, group1_def

Type information related to the homomorphism difference expression.

lemma (in int1) Int_ZF_2_1_L2:

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

shows \( m + n \in \mathbb{Z} \), \( f(m + n) \in \mathbb{Z} \), \( f(m) \in \mathbb{Z} \), \( f(n) \in \mathbb{Z} \), \( f(m) + f(n) \in \mathbb{Z} \), \( \text{HomDiff}(\mathbb{Z} ,IntegerAddition,f,\langle m,n\rangle ) \in \mathbb{Z} \) using assms, Int_ZF_2_1_L1, Group_ZF_3_2_L4A

Type information related to the homomorphism difference expression.

lemma (in int1) Int_ZF_2_1_L2A:

assumes \( f:\mathbb{Z} \rightarrow \mathbb{Z} \) and \( n\in \mathbb{Z} \), \( m\in \mathbb{Z} \)

shows \( m + n \in \mathbb{Z} \), \( f(m + n) \in \mathbb{Z} \), \( f(m) \in \mathbb{Z} \), \( f(n) \in \mathbb{Z} \), \( f(m) + f(n) \in \mathbb{Z} \), \( \text{HomDiff}(\mathbb{Z} ,IntegerAddition,f,\langle m,n\rangle ) \in \mathbb{Z} \) using assms, Int_ZF_2_1_L1, Group_ZF_3_2_L4

Slopes map integers into integers.

lemma (in int1) Int_ZF_2_1_L2B:

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

shows \( f(m) \in \mathbb{Z} \)proof
from A1 have \( f:\mathbb{Z} \rightarrow \mathbb{Z} \) using AlmostHoms_def
with A2 show \( f(m) \in \mathbb{Z} \) using apply_funtype
qed

The homomorphism difference in multiplicative notation is defined as the expression \(s(m\cdot n)\cdot(s(m)\cdot s(n))^{-1}\). The next lemma shows that in the additive notation used for integers the homomorphism difference is \(f(m+n) - f(m) - f(n)\) which we denote as \( \delta (f,m,n) \).

lemma (in int1) Int_ZF_2_1_L3:

assumes \( f:\mathbb{Z} \rightarrow \mathbb{Z} \) and \( m\in \mathbb{Z} \), \( n\in \mathbb{Z} \)

shows \( \text{HomDiff}(\mathbb{Z} ,IntegerAddition,f,\langle m,n\rangle ) = \delta (f,m,n) \) using assms, Int_ZF_2_1_L2A, Int_ZF_1_T2, group0_4_L4A, HomDiff_def

The next formula restates the definition of the homomorphism difference to express the value an almost homomorphism on a sum.

lemma (in int1) Int_ZF_2_1_L3A:

assumes A1: \( f\in \mathcal{S} \) and A2: \( m\in \mathbb{Z} \), \( n\in \mathbb{Z} \)

shows \( f(m + n) = f(m) + (f(n) + \delta (f,m,n)) \)proof
from A1, A2 have T: \( f(m)\in \mathbb{Z} \), \( f(n) \in \mathbb{Z} \), \( \delta (f,m,n) \in \mathbb{Z} \) and \( \text{HomDiff}(\mathbb{Z} ,IntegerAddition,f,\langle m,n\rangle ) = \delta (f,m,n) \) using Int_ZF_2_1_L2, AlmostHoms_def, Int_ZF_2_1_L3
with A1, A2 show \( f(m + n) = f(m) + (f(n) + \delta (f,m,n)) \) using Int_ZF_2_1_L3, Int_ZF_1_L3, Int_ZF_2_1_L1, Group_ZF_3_4_L1
qed

The homomorphism difference of any integer function is integer.

lemma (in int1) Int_ZF_2_1_L3B:

assumes \( f:\mathbb{Z} \rightarrow \mathbb{Z} \) and \( m\in \mathbb{Z} \), \( n\in \mathbb{Z} \)

shows \( \delta (f,m,n) \in \mathbb{Z} \) using assms, Int_ZF_2_1_L2A, Int_ZF_2_1_L3

The value of an integer function at a sum expressed in terms of \( \delta \).

lemma (in int1) Int_ZF_2_1_L3C:

assumes A1: \( f:\mathbb{Z} \rightarrow \mathbb{Z} \) and A2: \( m\in \mathbb{Z} \), \( n\in \mathbb{Z} \)

shows \( f(m + n) = \delta (f,m,n) + f(n) + f(m) \)proof
from A1, A2 have T: \( \delta (f,m,n) \in \mathbb{Z} \), \( f(m + n) \in \mathbb{Z} \), \( f(m) \in \mathbb{Z} \), \( f(n) \in \mathbb{Z} \) using Int_ZF_1_1_L5, apply_funtype
then show \( f(m + n) = \delta (f,m,n) + f(n) + f(m) \) using Int_ZF_1_2_L15
qed

The next lemma presents two ways the set of homomorphism differences can be written.

lemma (in int1) Int_ZF_2_1_L4:

assumes A1: \( f:\mathbb{Z} \rightarrow \mathbb{Z} \)

shows \( \{abs( \text{HomDiff}(\mathbb{Z} ,IntegerAddition,f,x)).\ x \in \mathbb{Z} \times \mathbb{Z} \} =\) \( \{abs(\delta (f,m,n)).\ \langle m,n\rangle \in \mathbb{Z} \times \mathbb{Z} \} \)proof
from A1 have \( \forall m\in \mathbb{Z} .\ \forall n\in \mathbb{Z} .\ \) \( abs( \text{HomDiff}(\mathbb{Z} ,IntegerAddition,f,\langle m,n\rangle )) = abs(\delta (f,m,n)) \) using Int_ZF_2_1_L3
then show \( thesis \) by (rule ZF1_1_L4A )
qed

If \(f\) maps integers into integers and for all \(m,n\in Z\) we have \(|f(m+n) - f(m) - f(n)| \leq L\) for some \(L\), then \(f\) is a slope.

lemma (in int1) Int_ZF_2_1_L5:

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

shows \( f\in \mathcal{S} \)proof
let \( Abs = \text{AbsoluteValue}(\mathbb{Z} ,IntegerAddition,IntegerOrder) \)
have \( group3(\mathbb{Z} ,IntegerAddition,IntegerOrder) \), \( IntegerOrder \text{ is total on } \mathbb{Z} \) using Int_ZF_2_T1
moreover
from A1, A2 have \( \forall x\in \mathbb{Z} \times \mathbb{Z} .\ \text{HomDiff}(\mathbb{Z} ,IntegerAddition,f,x) \in \mathbb{Z} \wedge \) \( \langle Abs( \text{HomDiff}(\mathbb{Z} ,IntegerAddition,f,x)),L \rangle \in IntegerOrder \) using Int_ZF_2_1_L2A, Int_ZF_2_1_L3
ultimately have \( \text{IsBounded}(\{ \text{HomDiff}(\mathbb{Z} ,IntegerAddition,f,x).\ x\in \mathbb{Z} \times \mathbb{Z} \},IntegerOrder) \) by (rule OrderedGroup_ZF_3_L9A )
with A1 show \( f \in \mathcal{S} \) using Int_bounded_iff_fin, AlmostHoms_def
qed

The absolute value of homomorphism difference of a slope \(s\) does not exceed \( \text{ max}\delta (s) \).

lemma (in int1) Int_ZF_2_1_L7:

assumes A1: \( s\in \mathcal{S} \) and A2: \( 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) \)proof
from A1, A2 show T: \( \delta (s,m,n) \in \mathbb{Z} \) using Int_ZF_2_1_L2, Int_ZF_1_1_L5
let \( A = \{abs( \text{HomDiff}(\mathbb{Z} ,IntegerAddition,s,x)).\ x\in \mathbb{Z} \times \mathbb{Z} \} \)
let \( B = \{abs(\delta (s,m,n)).\ \langle m,n\rangle \in \mathbb{Z} \times \mathbb{Z} \} \)
let \( d = abs(\delta (s,m,n)) \)
have \( \text{IsLinOrder}(\mathbb{Z} ,IntegerOrder) \) using Int_ZF_2_T1
moreover
have \( A \in Fin(\mathbb{Z} ) \)proof
have \( \forall k\in \mathbb{Z} .\ abs(k) \in \mathbb{Z} \) using Int_ZF_2_L14
moreover
from A1 have \( \{ \text{HomDiff}(\mathbb{Z} ,IntegerAddition,s,x).\ x \in \mathbb{Z} \times \mathbb{Z} \} \in Fin(\mathbb{Z} ) \) using AlmostHoms_def
ultimately show \( A \in Fin(\mathbb{Z} ) \) by (rule Finite1_L6C )
qed
moreover
have \( A\neq 0 \)
ultimately have \( \forall k\in A.\ \langle k, \text{Maximum}(IntegerOrder,A)\rangle \in IntegerOrder \) by (rule Finite_ZF_1_T2 )
moreover
from A1, A2 have \( d\in A \) using AlmostHoms_def, Int_ZF_2_1_L4
ultimately have \( d \leq \text{Maximum}(IntegerOrder,A) \)
with A1 show \( d \leq \text{ max}\delta (s) \), \( \text{ max}\delta (s) \in \mathbb{Z} \) using AlmostHoms_def, Int_ZF_2_1_L4, Int_ZF_2_L1A
with T show \( ( - \text{ max}\delta (s)) \leq \delta (s,m,n) \) using Int_ZF_1_3_L19
qed

A useful estimate for the value of a slope at \(0\), plus some type information for slopes.

lemma (in int1) Int_ZF_2_1_L8:

assumes A1: \( 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} \)proof
from A1 have \( s( 0 ) \in \mathbb{Z} \) using int_zero_one_are_int, Int_ZF_2_1_L2B
then have I: \( 0 \leq abs(s( 0 )) \) and \( abs(\delta (s, 0 , 0 )) = abs(s( 0 )) \) using int_abs_nonneg, int_zero_one_are_int, Int_ZF_1_1_L4, Int_ZF_2_L17
moreover
from A1 have \( abs(\delta (s, 0 , 0 )) \leq \text{ max}\delta (s) \) using int_zero_one_are_int, Int_ZF_2_1_L7
ultimately show II: \( abs(s( 0 )) \leq \text{ max}\delta (s) \)
with I show \( 0 \leq \text{ max}\delta (s) \) by (rule Int_order_transitive )
with II show \( \text{ max}\delta (s) \in \mathbb{Z} \), \( abs(s( 0 )) \in \mathbb{Z} \), \( abs(s( 0 )) + \text{ max}\delta (s) \in \mathbb{Z} \) using Int_ZF_2_L1A, Int_ZF_1_1_L5
qed

Int Group_ZF_3.thy we show that finite range functions valued in an abelian group form a normal subgroup of almost homomorphisms. This allows to define the equivalence relation between almost homomorphisms as the relation resulting from dividing by that normal subgroup. Then we show in Group_ZF_3_4_L12 that if the difference of \(f\) and \(g\) has finite range (actually \(f(n)\cdot g(n)^{-1}\) as we use multiplicative notation in Group_ZF_3.thy), then \(f\) and \(g\) are equivalent. The next lemma translates that fact into the notation used in int1 context.

lemma (in int1) Int_ZF_2_1_L9:

assumes A1: \( s\in \mathcal{S} \), \( r\in \mathcal{S} \) and A2: \( \forall m\in \mathbb{Z} .\ abs(s(m) - r(m)) \leq L \)

shows \( s \sim r \)proof
from A1, A2 have \( \forall m\in \mathbb{Z} .\ s(m) - r(m) \in \mathbb{Z} \wedge abs(s(m) - r(m)) \leq L \) using Int_ZF_2_1_L2B, Int_ZF_1_1_L5
then have \( \text{IsBounded}(\{s(n) - r(n).\ n\in \mathbb{Z} \}, IntegerOrder) \) by (rule Int_ZF_1_3_L20 )
with A1 show \( s \sim r \) using Int_bounded_iff_fin, Int_ZF_2_1_L1, Group_ZF_3_4_L12
qed

A neccessary condition for two slopes to be almost equal. For slopes the definition postulates the set \(\{f(m)-g(m): m\in Z\}\) to be finite. This lemma shows that this implies that \(|f(m)-g(m)|\) is bounded (by some integer) as \(m\) varies over integers. We also mention here that in this context \( s \sim r \) implies that both \(s\) and \(r\) are slopes.

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} \) using assms, Int_ZF_2_1_L1, Group_ZF_3_4_L11, Int_ZF_1_3_L20AA, QuotientGroupRel_def

Let's recall that the relation of almost equality is an equivalence relation on the set of slopes.

lemma (in int1) Int_ZF_2_1_L9B:

shows \( AlEqRel \subseteq \mathcal{S} \times \mathcal{S} \), \( \text{equiv}(\mathcal{S} ,AlEqRel) \) using Int_ZF_2_1_L1, Group_ZF_3_3_L3

Another version of sufficient condition for two slopes to be almost equal: if the difference of two slopes is a finite range function, then they are almost equal.

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 \) using assms, Int_ZF_2_1_L1, Group_ZF_3_2_L13, Group_ZF_3_4_L12A

If two slopes are almost equal, then the difference has finite range. This is the inverse of Int_ZF_2_1_L9C.

lemma (in int1) Int_ZF_2_1_L9D:

assumes A1: \( s \sim r \)

shows \( s + ( - r) \in \text{FinRangeFunctions}(\mathbb{Z} ,\mathbb{Z} ) \)proof
let \( G = \mathbb{Z} \)
let \( f = IntegerAddition \)
from A1 have \( \text{AlHomOp1}(G, f)\langle s, \text{GroupInv}( \text{AlmostHoms}(G, f), \text{AlHomOp1}(G, f))(r)\rangle \) \( \in \text{FinRangeFunctions}(G, G) \) using Int_ZF_2_1_L1, Group_ZF_3_4_L12B
with A1 show \( s + ( - r) \in \text{FinRangeFunctions}(\mathbb{Z} ,\mathbb{Z} ) \) using Int_ZF_2_1_L9A, Int_ZF_2_1_L1, Group_ZF_3_2_L13
qed

What is the value of a composition of slopes?

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} \) using assms, Int_ZF_2_1_L1, Group_ZF_3_4_L2

Composition of slopes is a slope.

lemma (in int1) Int_ZF_2_1_L11:

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

shows \( s\circ r \in \mathcal{S} \) using assms, Int_ZF_2_1_L1, Group_ZF_3_4_T1

Negative of a slope is a slope.

lemma (in int1) Int_ZF_2_1_L12:

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

shows \( - s \in \mathcal{S} \) using assms, Int_ZF_1_T2, Int_ZF_2_1_L1, Group_ZF_3_2_L13

What is the value of a negative of a slope?

lemma (in int1) Int_ZF_2_1_L12A:

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

shows \( ( - s)(m) = - (s(m)) \) using assms, Int_ZF_2_1_L1, Group_ZF_3_2_L5

What are the values of a sum of slopes?

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) \) using assms, Int_ZF_2_1_L1, Group_ZF_3_2_L12

Sum of slopes is a slope.

lemma (in int1) Int_ZF_2_1_L12C:

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

shows \( s + r \in \mathcal{S} \) using assms, Int_ZF_2_1_L1, Group_ZF_3_2_L16

A simple but useful identity.

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) \) using assms, Int_ZF_1_1_L5, Int_ZF_2_1_L2B, Int_ZF_1_2_L9, Int_ZF_1_2_L7

Some estimates for the absolute value of a slope at the opposite integer.

lemma (in int1) Int_ZF_2_1_L14:

assumes A1: \( s\in \mathcal{S} \) and A2: \( 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) \)proof
from A1, A2 have T: \( ( - m) \in \mathbb{Z} \), \( abs(s(m)) \in \mathbb{Z} \), \( s( 0 ) \in \mathbb{Z} \), \( abs(s( 0 )) \in \mathbb{Z} \), \( \delta (s,m, - m) \in \mathbb{Z} \), \( s(m) \in \mathbb{Z} \), \( s( - m) \in \mathbb{Z} \), \( ( - (s(m))) \in \mathbb{Z} \), \( s( 0 ) - \delta (s,m, - m) \in \mathbb{Z} \) using Int_ZF_1_1_L4, Int_ZF_2_1_L2B, Int_ZF_2_L14, Int_ZF_2_1_L2, Int_ZF_1_1_L5, int_zero_one_are_int
with A2 show I: \( s( - m) = s( 0 ) - \delta (s,m, - m) - s(m) \) using Int_ZF_1_1_L4, Int_ZF_1_2_L15
from T have \( abs(s( 0 ) - \delta (s,m, - m)) \leq abs(s( 0 )) + abs(\delta (s,m, - m)) \) using Int_triangle_ineq1
moreover
from A1, A2, T have \( abs(s( 0 )) + abs(\delta (s,m, - m)) \leq 2 \cdot \text{ max}\delta (s) \) using Int_ZF_2_1_L7, Int_ZF_2_1_L8, Int_ZF_1_3_L21
ultimately have \( abs(s( 0 ) - \delta (s,m, - m)) \leq 2 \cdot \text{ max}\delta (s) \) by (rule Int_order_transitive )
moreover
from I have \( s(m) + s( - m) = s(m) + (s( 0 ) - \delta (s,m, - m) - s(m)) \)
with T have \( abs(s(m) + s( - m)) = abs(s( 0 ) - \delta (s,m, - m)) \) using Int_ZF_1_2_L3
ultimately show \( abs(s(m) + s( - m)) \leq 2 \cdot \text{ max}\delta (s) \)
from I have \( abs(s( - m)) = abs(s( 0 ) - \delta (s,m, - m) - s(m)) \)
with T have \( abs(s( - m)) \leq abs(s( 0 )) + abs(\delta (s,m, - m)) + abs(s(m)) \) using int_triangle_ineq3
moreover
from A1, A2, T have \( abs(s( 0 )) + abs(\delta (s,m, - m)) + abs(s(m)) \leq 2 \cdot \text{ max}\delta (s) + abs(s(m)) \) using Int_ZF_2_1_L7, Int_ZF_2_1_L8, Int_ZF_1_3_L21, int_ord_transl_inv
ultimately show \( abs(s( - m)) \leq 2 \cdot \text{ max}\delta (s) + abs(s(m)) \) by (rule Int_order_transitive )
from T have \( s( 0 ) - \delta (s,m, - m) \leq abs(s( 0 )) + abs(\delta (s,m, - m)) \) using Int_ZF_2_L15E
moreover
from A1, A2, T have \( abs(s( 0 )) + abs(\delta (s,m, - m)) \leq abs(s( 0 )) + \text{ max}\delta (s) \) using Int_ZF_2_1_L7, int_ord_transl_inv
ultimately have \( s( 0 ) - \delta (s,m, - m) \leq abs(s( 0 )) + \text{ max}\delta (s) \) by (rule Int_order_transitive )
with T have \( s( 0 ) - \delta (s,m, - m) - s(m) \leq abs(s( 0 )) + \text{ max}\delta (s) - s(m) \) using int_ord_transl_inv
with I show \( s( - m) \leq abs(s( 0 )) + \text{ max}\delta (s) - s(m) \)
qed

An identity that expresses the value of an integer function at the opposite integer in terms of the value of that function at the integer, zero, and the homomorphism difference. We have a similar identity in Int_ZF_2_1_L14, but over there we assume that \(f\) is a slope.

lemma (in int1) Int_ZF_2_1_L14A:

assumes A1: \( f:\mathbb{Z} \rightarrow \mathbb{Z} \) and A2: \( m\in \mathbb{Z} \)

shows \( f( - m) = ( - \delta (f,m, - m)) + f( 0 ) - f(m) \)proof
from A1, A2 have T: \( f( - m) \in \mathbb{Z} \), \( \delta (f,m, - m) \in \mathbb{Z} \), \( f( 0 ) \in \mathbb{Z} \), \( f(m) \in \mathbb{Z} \) using Int_ZF_1_1_L4, Int_ZF_1_1_L5, int_zero_one_are_int, apply_funtype
with A2 show \( f( - m) = ( - \delta (f,m, - m)) + f( 0 ) - f(m) \) using Int_ZF_1_1_L4, Int_ZF_1_2_L15
qed

The next lemma allows to use the expression \( maxf(f, 0 .\ .\ M-1) \). Recall that \( maxf(f,A) \) is the maximum of (function) \(f\) on (the set) \(A\).

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) \) using assms, AlmostHoms_def, Int_ZF_1_5_L6, Int_ZF_1_4_L2

A lower estimate for the value of a slope at \(nM+k\).

lemma (in int1) Int_ZF_2_1_L16:

assumes A1: \( s\in \mathcal{S} \) and A2: \( m\in \mathbb{Z} \) and A3: \( M \in \mathbb{Z} _+ \) and A4: \( 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) \)proof
from A3 have \( 0 .\ .\ (M - 1 ) \subseteq \mathbb{Z} \) using Int_ZF_1_5_L6
with A1, A2, A3, A4 have T: \( m\cdot M \in \mathbb{Z} \), \( k \in \mathbb{Z} \), \( s(m\cdot M) \in \mathbb{Z} \) using PositiveSet_def, Int_ZF_1_1_L5, Int_ZF_2_1_L2B
with A1, A3, A4 have \( s(m\cdot M) + (minf(s, 0 .\ .\ (M - 1 )) - \text{ max}\delta (s)) \leq s(m\cdot M) + (s(k) + \delta (s,m\cdot M,k)) \) using Int_ZF_2_1_L15, Int_ZF_2_1_L7, int_ineq_add_sides, int_ord_transl_inv
with A1, T show \( thesis \) using Int_ZF_2_1_L3A
qed

Identity is a slope.

lemma (in int1) Int_ZF_2_1_L17:

shows \( id(\mathbb{Z} ) \in \mathcal{S} \) using Int_ZF_2_1_L1, Group_ZF_3_4_L15

Simple identities about (absolute value of) homomorphism differences.

lemma (in int1) Int_ZF_2_1_L18:

assumes A1: \( f:\mathbb{Z} \rightarrow \mathbb{Z} \) and A2: \( m\in \mathbb{Z} \), \( n\in \mathbb{Z} \)

shows \( abs(f(n) + f(m) - f(m + n)) = abs(\delta (f,m,n)) \), \( abs(f(m) + f(n) - f(m + n)) = abs(\delta (f,m,n)) \), \( ( - (f(m))) - f(n) + f(m + n) = \delta (f,m,n) \), \( ( - (f(n))) - f(m) + f(m + n) = \delta (f,m,n) \), \( abs(( - f(m + n)) + f(m) + f(n)) = abs(\delta (f,m,n)) \)proof
from A1, A2 have T: \( f(m + n) \in \mathbb{Z} \), \( f(m) \in \mathbb{Z} \), \( f(n) \in \mathbb{Z} \), \( f(m + n) - f(m) - f(n) \in \mathbb{Z} \), \( ( - (f(m))) \in \mathbb{Z} \), \( ( - f(m + n)) + f(m) + f(n) \in \mathbb{Z} \) using apply_funtype, Int_ZF_1_1_L4, Int_ZF_1_1_L5
then have \( abs( - (f(m + n) - f(m) - f(n))) = abs(f(m + n) - f(m) - f(n)) \) using Int_ZF_2_L17
moreover
from T have \( ( - (f(m + n) - f(m) - f(n))) = f(n) + f(m) - f(m + n) \) using Int_ZF_1_2_L9A
ultimately show \( abs(f(n) + f(m) - f(m + n)) = abs(\delta (f,m,n)) \)
moreover
from T have \( f(n) + f(m) = f(m) + f(n) \) using Int_ZF_1_1_L5
ultimately show \( abs(f(m) + f(n) - f(m + n)) = abs(\delta (f,m,n)) \)
from T show \( ( - (f(m))) - f(n) + f(m + n) = \delta (f,m,n) \), \( ( - (f(n))) - f(m) + f(m + n) = \delta (f,m,n) \) using Int_ZF_1_2_L9
from T have \( abs(( - f(m + n)) + f(m) + f(n)) =\) \( abs( - (( - f(m + n)) + f(m) + f(n))) \) using Int_ZF_2_L17
also
from T have \( abs( - (( - f(m + n)) + f(m) + f(n))) = abs(\delta (f,m,n)) \) using Int_ZF_1_2_L9
finally show \( abs(( - f(m + n)) + f(m) + f(n)) = abs(\delta (f,m,n)) \)
qed

Some identities about the homomorphism difference of odd functions.

lemma (in int1) Int_ZF_2_1_L19:

assumes A1: \( f:\mathbb{Z} \rightarrow \mathbb{Z} \) and A2: \( \forall x\in \mathbb{Z} .\ ( - f( - x)) = f(x) \) and A3: \( m\in \mathbb{Z} \), \( n\in \mathbb{Z} \)

shows \( abs(\delta (f, - m,m + n)) = abs(\delta (f,m,n)) \), \( abs(\delta (f, - n,m + n)) = abs(\delta (f,m,n)) \), \( \delta (f,n, - (m + n)) = \delta (f,m,n) \), \( \delta (f,m, - (m + n)) = \delta (f,m,n) \), \( abs(\delta (f, - m, - n)) = abs(\delta (f,m,n)) \)proof
from A1, A2, A3 show \( abs(\delta (f, - m,m + n)) = abs(\delta (f,m,n)) \), \( abs(\delta (f, - n,m + n)) = abs(\delta (f,m,n)) \) using Int_ZF_1_2_L3, Int_ZF_2_1_L18
from A3 have T: \( m + n \in \mathbb{Z} \) using Int_ZF_1_1_L5
from A1, A2 have I: \( \forall x\in \mathbb{Z} .\ f( - x) = ( - f(x)) \) using Int_ZF_1_5_L13
with A1, A2, A3, T show \( \delta (f,n, - (m + n)) = \delta (f,m,n) \), \( \delta (f,m, - (m + n)) = \delta (f,m,n) \) using Int_ZF_1_2_L3, Int_ZF_2_1_L18
from A3 have \( abs(\delta (f, - m, - n)) = abs(f( - (m + n)) - f( - m) - f( - n)) \) using Int_ZF_1_1_L5
also
from A1, A2, A3, T, I have \( \ldots = abs(\delta (f,m,n)) \) using Int_ZF_2_1_L18
finally show \( abs(\delta (f, - m, - n)) = abs(\delta (f,m,n)) \)
qed

Recall that \(f\) is a slope iff \(f(m+n)-f(m)-f(n)\) is bounded as \(m,n\) ranges over integers. The next lemma is the first step in showing that we only need to check this condition as \(m,n\) ranges over positive intergers. Namely we show that if the condition holds for positive integers, then it holds if one integer is positive and the second one is nonnegative.

lemma (in int1) Int_ZF_2_1_L20:

assumes A1: \( f:\mathbb{Z} \rightarrow \mathbb{Z} \) and A2: \( \forall a\in \mathbb{Z} _+.\ \forall b\in \mathbb{Z} _+.\ abs(\delta (f,a,b)) \leq L \) and A3: \( m\in \mathbb{Z} ^+ \), \( n\in \mathbb{Z} _+ \)

shows \( 0 \leq L \), \( abs(\delta (f,m,n)) \leq L + abs(f( 0 )) \)proof
from A1, A2 have \( \delta (f,1 ,1 ) \in \mathbb{Z} \) and \( abs(\delta (f,1 ,1 )) \leq L \) using int_one_two_are_pos, PositiveSet_def, Int_ZF_2_1_L3B
then show I: \( 0 \leq L \) using Int_ZF_1_3_L19
from A1, A3 have T: \( n \in \mathbb{Z} \), \( f(n) \in \mathbb{Z} \), \( f( 0 ) \in \mathbb{Z} \), \( \delta (f,m,n) \in \mathbb{Z} \), \( abs(\delta (f,m,n)) \in \mathbb{Z} \) using PositiveSet_def, int_zero_one_are_int, apply_funtype, Nonnegative_def, Int_ZF_2_1_L3B, Int_ZF_2_L14
from A3 have \( m= 0 \vee m\in \mathbb{Z} _+ \) using Int_ZF_1_5_L3A
moreover {
assume \( m = 0 \)
with T, I have \( abs(\delta (f,m,n)) \leq L + abs(f( 0 )) \) using Int_ZF_1_1_L4, Int_ZF_1_2_L3, Int_ZF_2_L17, int_ord_is_refl, refl_def, Int_ZF_2_L15F
} moreover {
assume \( m\in \mathbb{Z} _+ \)
with A2, A3, T have \( abs(\delta (f,m,n)) \leq L + abs(f( 0 )) \) using int_abs_nonneg, Int_ZF_2_L15F
} ultimately show \( abs(\delta (f,m,n)) \leq L + abs(f( 0 )) \)
qed

If the slope condition holds for all pairs of integers such that one integer is positive and the second one is nonnegative, then it holds when both integers are nonnegative.

lemma (in int1) Int_ZF_2_1_L21:

assumes A1: \( f:\mathbb{Z} \rightarrow \mathbb{Z} \) and A2: \( \forall a\in \mathbb{Z} ^+.\ \forall b\in \mathbb{Z} _+.\ abs(\delta (f,a,b)) \leq L \) and A3: \( n\in \mathbb{Z} ^+ \), \( m\in \mathbb{Z} ^+ \)

shows \( abs(\delta (f,m,n)) \leq L + abs(f( 0 )) \)proof
from A1, A2 have \( \delta (f,1 ,1 ) \in \mathbb{Z} \) and \( abs(\delta (f,1 ,1 )) \leq L \) using int_one_two_are_pos, PositiveSet_def, Nonnegative_def, Int_ZF_2_1_L3B
then have I: \( 0 \leq L \) using Int_ZF_1_3_L19
from A1, A3 have T: \( m \in \mathbb{Z} \), \( f(m) \in \mathbb{Z} \), \( f( 0 ) \in \mathbb{Z} \), \( ( - f( 0 )) \in \mathbb{Z} \), \( \delta (f,m,n) \in \mathbb{Z} \), \( abs(\delta (f,m,n)) \in \mathbb{Z} \) using int_zero_one_are_int, apply_funtype, Nonnegative_def, Int_ZF_2_1_L3B, Int_ZF_2_L14, Int_ZF_1_1_L4
from A3 have \( n= 0 \vee n\in \mathbb{Z} _+ \) using Int_ZF_1_5_L3A
moreover {
assume \( n= 0 \)
with T have \( \delta (f,m,n) = - f( 0 ) \) using Int_ZF_1_1_L4
with T have \( abs(\delta (f,m,n)) = abs(f( 0 )) \) using Int_ZF_2_L17
with T have \( abs(\delta (f,m,n)) \leq abs(f( 0 )) \) using int_ord_is_refl, refl_def
with T, I have \( abs(\delta (f,m,n)) \leq L + abs(f( 0 )) \) using Int_ZF_2_L15F
} moreover {
assume \( n\in \mathbb{Z} _+ \)
with A2, A3, T have \( abs(\delta (f,m,n)) \leq L + abs(f( 0 )) \) using int_abs_nonneg, Int_ZF_2_L15F
} ultimately show \( abs(\delta (f,m,n)) \leq L + abs(f( 0 )) \)
qed

If the homomorphism difference is bounded on \( \mathbb{Z} _+\times \mathbb{Z} _+ \), then it is bounded on \( \mathbb{Z} ^+\times \mathbb{Z} ^+ \).

lemma (in int1) Int_ZF_2_1_L22:

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

shows \( \exists M.\ \forall m\in \mathbb{Z} ^+.\ \forall n\in \mathbb{Z} ^+.\ abs(\delta (f,m,n)) \leq M \)proof
from A1, A2 have \( \forall m\in \mathbb{Z} ^+.\ \forall n\in \mathbb{Z} ^+.\ abs(\delta (f,m,n)) \leq L + abs(f( 0 )) + abs(f( 0 )) \) using Int_ZF_2_1_L20, Int_ZF_2_1_L21
then show \( thesis \)
qed

For odd functions we can do better than in Int_ZF_2_1_L22: if the homomorphism difference of \(f\) is bounded on \( \mathbb{Z} ^+\times \mathbb{Z} ^+ \), then it is bounded on \( \mathbb{Z} \times \mathbb{Z} \), hence \(f\) is a slope. Loong prof by splitting the \( \mathbb{Z} \times \mathbb{Z} \) into six subsets.

lemma (in int1) Int_ZF_2_1_L23:

assumes A1: \( f:\mathbb{Z} \rightarrow \mathbb{Z} \) and A2: \( \forall a\in \mathbb{Z} _+.\ \forall b\in \mathbb{Z} _+.\ abs(\delta (f,a,b)) \leq L \) and A3: \( \forall x\in \mathbb{Z} .\ ( - f( - x)) = f(x) \)

shows \( f\in \mathcal{S} \)proof
from A1, A2 have \( \exists M.\ \forall a\in \mathbb{Z} ^+.\ \forall b\in \mathbb{Z} ^+.\ abs(\delta (f,a,b)) \leq M \) by (rule Int_ZF_2_1_L22 )
then obtain \( M \) where I: \( \forall m\in \mathbb{Z} ^+.\ \forall n\in \mathbb{Z} ^+.\ abs(\delta (f,m,n)) \leq M \)
{
fix \( a \) \( b \)
assume A4: \( a\in \mathbb{Z} \), \( b\in \mathbb{Z} \)
then have \( 0 \leq a \wedge 0 \leq b \vee a\leq 0 \wedge b\leq 0 \vee \) \( a\leq 0 \wedge 0 \leq b \wedge 0 \leq a + b \vee a\leq 0 \wedge 0 \leq b \wedge a + b \leq 0 \vee \) \( 0 \leq a \wedge b\leq 0 \wedge 0 \leq a + b \vee 0 \leq a \wedge b\leq 0 \wedge a + b \leq 0 \) using int_plane_split_in6
moreover {
assume \( 0 \leq a \wedge 0 \leq b \)
then have \( a\in \mathbb{Z} ^+ \), \( b\in \mathbb{Z} ^+ \) using Int_ZF_2_L16
with I have \( abs(\delta (f,a,b)) \leq M \)
} moreover {
assume \( a\leq 0 \wedge b\leq 0 \)
with I have \( abs(\delta (f, - a, - b)) \leq M \) using Int_ZF_2_L10A, Int_ZF_2_L16
with A1, A3, A4 have \( abs(\delta (f,a,b)) \leq M \) using Int_ZF_2_1_L19
} moreover {
assume \( a\leq 0 \wedge 0 \leq b \wedge 0 \leq a + b \)
with I have \( abs(\delta (f, - a,a + b)) \leq M \) using Int_ZF_2_L10A, Int_ZF_2_L16
with A1, A3, A4 have \( abs(\delta (f,a,b)) \leq M \) using Int_ZF_2_1_L19
} moreover {
assume \( a\leq 0 \wedge 0 \leq b \wedge a + b \leq 0 \)
with I have \( abs(\delta (f,b, - (a + b))) \leq M \) using Int_ZF_2_L10A, Int_ZF_2_L16
with A1, A3, A4 have \( abs(\delta (f,a,b)) \leq M \) using Int_ZF_2_1_L19
} moreover {
assume \( 0 \leq a \wedge b\leq 0 \wedge 0 \leq a + b \)
with I have \( abs(\delta (f, - b,a + b)) \leq M \) using Int_ZF_2_L10A, Int_ZF_2_L16
with A1, A3, A4 have \( abs(\delta (f,a,b)) \leq M \) using Int_ZF_2_1_L19
} moreover {
assume \( 0 \leq a \wedge b\leq 0 \wedge a + b \leq 0 \)
with I have \( abs(\delta (f,a, - (a + b))) \leq M \) using Int_ZF_2_L10A, Int_ZF_2_L16
with A1, A3, A4 have \( abs(\delta (f,a,b)) \leq M \) using Int_ZF_2_1_L19
} ultimately have \( abs(\delta (f,a,b)) \leq M \)
}
then have \( \forall m\in \mathbb{Z} .\ \forall n\in \mathbb{Z} .\ abs(\delta (f,m,n)) \leq M \)
with A1 show \( f\in \mathcal{S} \) by (rule Int_ZF_2_1_L5 )
qed

If the homomorphism difference of a function defined on positive integers is bounded, then the odd extension of this function is a slope.

lemma (in int1) Int_ZF_2_1_L24:

assumes A1: \( f:\mathbb{Z} _+\rightarrow \mathbb{Z} \) and A2: \( \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} \)proof
let \( g = \text{OddExtension}(\mathbb{Z} ,IntegerAddition,IntegerOrder,f) \)
from A1 have \( g : \mathbb{Z} \rightarrow \mathbb{Z} \) using Int_ZF_1_5_L10
moreover
have \( \forall a\in \mathbb{Z} _+.\ \forall b\in \mathbb{Z} _+.\ abs(\delta (g,a,b)) \leq L \)proof
{
fix \( a \) \( b \)
assume A3: \( a\in \mathbb{Z} _+ \), \( b\in \mathbb{Z} _+ \)
with A1 have \( abs(\delta (f,a,b)) = abs(\delta (g,a,b)) \) using pos_int_closed_add_unfolded, Int_ZF_1_5_L11
moreover
from A2, A3 have \( abs(\delta (f,a,b)) \leq L \)
ultimately have \( abs(\delta (g,a,b)) \leq L \)
}
then show \( thesis \)
qed
moreover
from A1 have \( \forall x\in \mathbb{Z} .\ ( - g( - x)) = g(x) \) using int_oddext_is_odd_alt
ultimately show \( g \in \mathcal{S} \) by (rule Int_ZF_2_1_L23 )
qed

Type information related to \(\gamma\).

lemma (in int1) Int_ZF_2_1_L25:

assumes A1: \( f:\mathbb{Z} \rightarrow \mathbb{Z} \) and A2: \( m\in \mathbb{Z} \), \( n\in \mathbb{Z} \)

shows \( \delta (f,m, - n) \in \mathbb{Z} \), \( \delta (f,n, - n) \in \mathbb{Z} \), \( ( - \delta (f,n, - n)) \in \mathbb{Z} \), \( f( 0 ) \in \mathbb{Z} \), \( \gamma (f,m,n) \in \mathbb{Z} \)proof
from A1, A2 show T1: \( \delta (f,m, - n) \in \mathbb{Z} \), \( f( 0 ) \in \mathbb{Z} \) using Int_ZF_1_1_L4, Int_ZF_2_1_L3B, int_zero_one_are_int, apply_funtype
from A2 have \( ( - n) \in \mathbb{Z} \) using Int_ZF_1_1_L4
with A1, A2 show \( \delta (f,n, - n) \in \mathbb{Z} \) using Int_ZF_2_1_L3B
then show \( ( - \delta (f,n, - n)) \in \mathbb{Z} \) using Int_ZF_1_1_L4
with T1 show \( \gamma (f,m,n) \in \mathbb{Z} \) using Int_ZF_1_1_L5
qed

A couple of formulae involving \(f(m-n)\) and \(\gamma(f,m,n)\).

lemma (in int1) Int_ZF_2_1_L26:

assumes A1: \( f:\mathbb{Z} \rightarrow \mathbb{Z} \) and A2: \( m\in \mathbb{Z} \), \( n\in \mathbb{Z} \)

shows \( f(m - n) = \gamma (f,m,n) + f(m) - f(n) \), \( f(m - n) = \gamma (f,m,n) + (f(m) - f(n)) \), \( f(m - n) + (f(n) - \gamma (f,m,n)) = f(m) \)proof
from A1, A2 have T: \( ( - n) \in \mathbb{Z} \), \( \delta (f,m, - n) \in \mathbb{Z} \), \( f( 0 ) \in \mathbb{Z} \), \( f(m) \in \mathbb{Z} \), \( f(n) \in \mathbb{Z} \), \( ( - f(n)) \in \mathbb{Z} \), \( ( - \delta (f,n, - n)) \in \mathbb{Z} \), \( ( - \delta (f,n, - n)) + f( 0 ) \in \mathbb{Z} \), \( \gamma (f,m,n) \in \mathbb{Z} \) using Int_ZF_1_1_L4, Int_ZF_2_1_L25, apply_funtype, Int_ZF_1_1_L5
with A1, A2 have \( f(m - n) = \) \( \delta (f,m, - n) + (( - \delta (f,n, - n)) + f( 0 ) - f(n)) + f(m) \) using Int_ZF_2_1_L3C, Int_ZF_2_1_L14A
with T have \( f(m - n) =\) \( \delta (f,m, - n) + (( - \delta (f,n, - n)) + f( 0 )) + f(m) - f(n) \) using Int_ZF_1_2_L16
moreover
from T have \( \delta (f,m, - n) + (( - \delta (f,n, - n)) + f( 0 )) = \gamma (f,m,n) \) using Int_ZF_1_1_L7
ultimately show I: \( f(m - n) = \gamma (f,m,n) + f(m) - f(n) \)
then have \( f(m - n) + (f(n) - \gamma (f,m,n)) = \) \( (\gamma (f,m,n) + f(m) - f(n)) + (f(n) - \gamma (f,m,n)) \)
moreover
from T have \( \ldots = f(m) \) using Int_ZF_1_2_L18
ultimately show \( f(m - n) + (f(n) - \gamma (f,m,n)) = f(m) \)
from T have \( \gamma (f,m,n) \in \mathbb{Z} \), \( f(m) \in \mathbb{Z} \), \( ( - f(n)) \in \mathbb{Z} \)
then have \( \gamma (f,m,n) + f(m) + ( - f(n)) = \gamma (f,m,n) + (f(m) + ( - f(n))) \) by (rule Int_ZF_1_1_L7 )
with I show \( f(m - n) = \gamma (f,m,n) + (f(m) - f(n)) \)
qed

A formula expressing the difference between \(f(m-n-k)\) and \(f(m)-f(n)-f(k)\) in terms of \(\gamma\).

lemma (in int1) Int_ZF_2_1_L26A:

assumes A1: \( f:\mathbb{Z} \rightarrow \mathbb{Z} \) and A2: \( m\in \mathbb{Z} \), \( n\in \mathbb{Z} \), \( k\in \mathbb{Z} \)

shows \( f(m - n - k) - (f(m) - f(n) - f(k)) = \gamma (f,m - n,k) + \gamma (f,m,n) \)proof
from A1, A2 have T: \( m - n \in \mathbb{Z} \), \( \gamma (f,m - n,k) \in \mathbb{Z} \), \( f(m) - f(n) - f(k) \in \mathbb{Z} \) and T1: \( \gamma (f,m,n) \in \mathbb{Z} \), \( f(m) - f(n) \in \mathbb{Z} \), \( ( - f(k)) \in \mathbb{Z} \) using Int_ZF_1_1_L4, Int_ZF_1_1_L5, Int_ZF_2_1_L25, apply_funtype
from A1, A2 have \( f(m - n) - f(k) = \gamma (f,m,n) + (f(m) - f(n)) + ( - f(k)) \) using Int_ZF_2_1_L26
also
from T1 have \( \ldots = \gamma (f,m,n) + (f(m) - f(n) + ( - f(k))) \) by (rule Int_ZF_1_1_L7 )
finally have \( f(m - n) - f(k) = \gamma (f,m,n) + (f(m) - f(n) - f(k)) \)
moreover
from A1, A2, T have \( f(m - n - k) = \gamma (f,m - n,k) + (f(m - n) - f(k)) \) using Int_ZF_2_1_L26
ultimately have \( f(m - n - k) - (f(m) - f(n) - f(k)) = \) \( \gamma (f,m - n,k) + ( \gamma (f,m,n) + (f(m) - f(n) - f(k))) \) \( - (f(m) - f(n) - f(k)) \)
with T, T1 show \( thesis \) using Int_ZF_1_2_L17
qed

If \(s\) is a slope, then \(\gamma (s,m,n)\) is uniformly bounded.

lemma (in int1) Int_ZF_2_1_L27:

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

shows \( \exists L\in \mathbb{Z} .\ \forall m\in \mathbb{Z} .\ \forall n\in \mathbb{Z} .\ abs(\gamma (s,m,n)) \leq L \)proof
let \( L = \text{ max}\delta (s) + \text{ max}\delta (s) + abs(s( 0 )) \)
from A1 have T: \( \text{ max}\delta (s) \in \mathbb{Z} \), \( abs(s( 0 )) \in \mathbb{Z} \), \( L \in \mathbb{Z} \) using Int_ZF_2_1_L8, int_zero_one_are_int, Int_ZF_2_1_L2B, Int_ZF_2_L14, Int_ZF_1_1_L5
moreover {
fix \( m \) \( fix \) \( n \)
assume A2: \( m\in \mathbb{Z} \), \( n\in \mathbb{Z} \)
with A1 have T: \( ( - n) \in \mathbb{Z} \), \( \delta (s,m, - n) \in \mathbb{Z} \), \( \delta (s,n, - n) \in \mathbb{Z} \), \( ( - \delta (s,n, - n)) \in \mathbb{Z} \), \( s( 0 ) \in \mathbb{Z} \), \( abs(s( 0 )) \in \mathbb{Z} \) using Int_ZF_1_1_L4, AlmostHoms_def, Int_ZF_2_1_L25, Int_ZF_2_L14
with T have \( abs(\delta (s,m, - n) - \delta (s,n, - n) + s( 0 )) \leq \) \( abs(\delta (s,m, - n)) + abs( - \delta (s,n, - n)) + abs(s( 0 )) \) using Int_triangle_ineq3
moreover
from A1, A2, T have \( abs(\delta (s,m, - n)) + abs( - \delta (s,n, - n)) + abs(s( 0 )) \leq L \) using Int_ZF_2_1_L7, int_ineq_add_sides, int_ord_transl_inv, Int_ZF_2_L17
ultimately have \( abs(\delta (s,m, - n) - \delta (s,n, - n) + s( 0 )) \leq L \) by (rule Int_order_transitive )
then have \( abs(\gamma (s,m,n)) \leq L \)
} ultimately show \( \exists L\in \mathbb{Z} .\ \forall m\in \mathbb{Z} .\ \forall n\in \mathbb{Z} .\ abs(\gamma (s,m,n)) \leq L \)
qed

If \(s\) is a slope, then \(s(m) \leq s(m-1) + M\), where \(L\) does not depend on \(m\).

lemma (in int1) Int_ZF_2_1_L28:

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

shows \( \exists M\in \mathbb{Z} .\ \forall m\in \mathbb{Z} .\ s(m) \leq s(m - 1 ) + M \)proof
from A1 have \( \exists L\in \mathbb{Z} .\ \forall m\in \mathbb{Z} .\ \forall n\in \mathbb{Z} .\ abs(\gamma (s,m,n)) \leq L \) using Int_ZF_2_1_L27
then obtain \( L \) where T: \( L\in \mathbb{Z} \) and \( \forall m\in \mathbb{Z} .\ \forall n\in \mathbb{Z} .\ abs(\gamma (s,m,n)) \leq L \) using Int_ZF_2_1_L27
then have I: \( \forall m\in \mathbb{Z} .\ abs(\gamma (s,m,1 )) \leq L \) using int_zero_one_are_int
let \( M = s(1 ) + L \)
from A1, T have \( M \in \mathbb{Z} \) using int_zero_one_are_int, Int_ZF_2_1_L2B, Int_ZF_1_1_L5
moreover {
fix \( m \)
assume A2: \( m\in \mathbb{Z} \)
with A1 have T1: \( s:\mathbb{Z} \rightarrow \mathbb{Z} \), \( m\in \mathbb{Z} \), \( 1 \in \mathbb{Z} \) and T2: \( \gamma (s,m,1 ) \in \mathbb{Z} \), \( s(1 ) \in \mathbb{Z} \) using int_zero_one_are_int, AlmostHoms_def, Int_ZF_2_1_L25
from A2, T1 have T3: \( s(m - 1 ) \in \mathbb{Z} \) using Int_ZF_1_1_L5, apply_funtype
from I, A2, T2 have \( ( - \gamma (s,m,1 )) \leq abs(\gamma (s,m,1 )) \), \( abs(\gamma (s,m,1 )) \leq L \) using Int_ZF_2_L19C
then have \( ( - \gamma (s,m,1 )) \leq L \) by (rule Int_order_transitive )
with T2, T3 have \( s(m - 1 ) + (s(1 ) - \gamma (s,m,1 )) \leq s(m - 1 ) + M \) using int_ord_transl_inv
moreover
from T1 have \( s(m - 1 ) + (s(1 ) - \gamma (s,m,1 )) = s(m) \) by (rule Int_ZF_2_1_L26 )
ultimately have \( s(m) \leq s(m - 1 ) + M \)
} ultimately show \( \exists M\in \mathbb{Z} .\ \forall m\in \mathbb{Z} .\ s(m) \leq s(m - 1 ) + M \)
qed

If \(s\) is a slope, then the difference between \(s(m-n-k)\) and \(s(m)-s(n)-s(k)\) is uniformly bounded.

lemma (in int1) Int_ZF_2_1_L29:

assumes A1: \( 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} .\ abs(s(m - n - k) - (s(m) - s(n) - s(k))) \leq M \)proof
from A1 have \( \exists L\in \mathbb{Z} .\ \forall m\in \mathbb{Z} .\ \forall n\in \mathbb{Z} .\ abs(\gamma (s,m,n)) \leq L \) using Int_ZF_2_1_L27
then obtain \( L \) where I: \( L\in \mathbb{Z} \) and II: \( \forall m\in \mathbb{Z} .\ \forall n\in \mathbb{Z} .\ abs(\gamma (s,m,n)) \leq L \)
from I have \( L + L \in \mathbb{Z} \) using Int_ZF_1_1_L5
moreover {
fix \( m \) \( n \) \( k \)
assume A2: \( m\in \mathbb{Z} \), \( n\in \mathbb{Z} \), \( k\in \mathbb{Z} \)
with A1 have T: \( m - n \in \mathbb{Z} \), \( \gamma (s,m - n,k) \in \mathbb{Z} \), \( \gamma (s,m,n) \in \mathbb{Z} \) using Int_ZF_1_1_L5, AlmostHoms_def, Int_ZF_2_1_L25
then have I: \( abs(\gamma (s,m - n,k) + \gamma (s,m,n)) \leq abs(\gamma (s,m - n,k)) + abs(\gamma (s,m,n)) \) using Int_triangle_ineq
from II, A2, T have \( abs(\gamma (s,m - n,k)) \leq L \), \( abs(\gamma (s,m,n)) \leq L \)
then have \( abs(\gamma (s,m - n,k)) + abs(\gamma (s,m,n)) \leq L + L \) using int_ineq_add_sides
with I have \( abs(\gamma (s,m - n,k) + \gamma (s,m,n)) \leq L + L \) by (rule Int_order_transitive )
moreover
from A1, A2 have \( s(m - n - k) - (s(m) - s(n) - s(k)) = \gamma (s,m - n,k) + \gamma (s,m,n) \) using AlmostHoms_def, Int_ZF_2_1_L26A
ultimately have \( abs(s(m - n - k) - (s(m) - s(n) - s(k))) \leq L + L \)
} ultimately show \( thesis \)
qed

If \(s\) is a slope, then we can find integers \(M,K\) such that \(s(m-n-k) \leq s(m)-s(n)-s(k) + M\) and \(s(m)-s(n)-s(k) + K \leq s(m-n-k)\), for all integer \(m,n,k\).

lemma (in int1) Int_ZF_2_1_L30:

assumes A1: \( 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) \)proof
from A1 have \( \exists M\in \mathbb{Z} .\ \forall m\in \mathbb{Z} .\ \forall n\in \mathbb{Z} .\ \forall k\in \mathbb{Z} .\ abs(s(m - n - k) - (s(m) - s(n) - s(k))) \leq M \) using Int_ZF_2_1_L29
then obtain \( M \) where I: \( M\in \mathbb{Z} \) and II: \( \forall m\in \mathbb{Z} .\ \forall n\in \mathbb{Z} .\ \forall k\in \mathbb{Z} .\ abs(s(m - n - k) - (s(m) - s(n) - s(k))) \leq M \)
from I have III: \( ( - M) \in \mathbb{Z} \) using Int_ZF_1_1_L4
{
fix \( m \) \( n \) \( k \)
assume A2: \( m\in \mathbb{Z} \), \( n\in \mathbb{Z} \), \( k\in \mathbb{Z} \)
with A1 have \( s(m - n - k) \in \mathbb{Z} \) and \( s(m) - s(n) - s(k) \in \mathbb{Z} \) using Int_ZF_1_1_L5, Int_ZF_2_1_L2B
moreover
from II, A2 have \( abs(s(m - n - k) - (s(m) - s(n) - s(k))) \leq M \)
ultimately have \( s(m - n - k) \leq s(m) - s(n) - s(k) + M \wedge \) \( s(m) - s(n) - s(k) - M \leq s(m - n - k) \) using Int_triangle_ineq2
}
then have \( \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 \), \( \forall m\in \mathbb{Z} .\ \forall n\in \mathbb{Z} .\ \forall k\in \mathbb{Z} .\ s(m) - s(n) - s(k) - M \leq s(m - n - k) \)
with I, III show \( \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) \)
qed

By definition functions \(f,g\) are almost equal if \(f-g\)* is bounded. In the next lemma we show it is sufficient to check the boundedness on positive integers.

lemma (in int1) Int_ZF_2_1_L31:

assumes A1: \( s\in \mathcal{S} \), \( r\in \mathcal{S} \) and A2: \( \forall m\in \mathbb{Z} _+.\ abs(s(m) - r(m)) \leq L \)

shows \( s \sim r \)proof
let \( a = abs(s( 0 ) - r( 0 )) \)
let \( c = 2 \cdot \text{ max}\delta (s) + 2 \cdot \text{ max}\delta (r) + L \)
let \( M = \text{Maximum}(IntegerOrder,\{a,L,c\}) \)
from A2 have \( abs(s(1 ) - r(1 )) \leq L \) using int_one_two_are_pos
then have T: \( L\in \mathbb{Z} \) using Int_ZF_2_L1A
moreover
from A1 have \( a \in \mathbb{Z} \) using int_zero_one_are_int, Int_ZF_2_1_L2B, Int_ZF_1_1_L5, Int_ZF_2_L14
moreover
from A1, T have \( c \in \mathbb{Z} \) using Int_ZF_2_1_L8, int_two_three_are_int, Int_ZF_1_1_L5
ultimately have I: \( a \leq M \) and II: \( L \leq M \) and III: \( c \leq M \) using Int_ZF_1_4_L1A
{
fix \( m \)
assume A5: \( m\in \mathbb{Z} \)
with A1 have T: \( s(m) \in \mathbb{Z} \), \( r(m) \in \mathbb{Z} \), \( s(m) - r(m) \in \mathbb{Z} \), \( s( - m) \in \mathbb{Z} \), \( r( - m) \in \mathbb{Z} \) using Int_ZF_2_1_L2B, Int_ZF_1_1_L4, Int_ZF_1_1_L5
from A5 have \( m= 0 \vee m\in \mathbb{Z} _+ \vee ( - m) \in \mathbb{Z} _+ \) using int_decomp_cases
moreover {
assume \( m= 0 \)
with I have \( abs(s(m) - r(m)) \leq M \)
} moreover {
assume \( m\in \mathbb{Z} _+ \)
with A2, II have \( abs(s(m) - r(m)) \leq L \) and \( L\leq M \)
then have \( abs(s(m) - r(m)) \leq M \) by (rule Int_order_transitive )
} moreover {
assume A6: \( ( - m) \in \mathbb{Z} _+ \)
from T have \( abs(s(m) - r(m)) \leq \) \( abs(s(m) + s( - m)) + abs(r(m) + r( - m)) + abs(s( - m) - r( - m)) \) using Int_ZF_1_3_L22A
moreover
from A1, A2, III, A5, A6 have \( abs(s(m) + s( - m)) + abs(r(m) + r( - m)) + abs(s( - m) - r( - m)) \leq c \), \( c \leq M \) using Int_ZF_2_1_L14, int_ineq_add_sides
then have \( abs(s(m) + s( - m)) + abs(r(m) + r( - m)) + abs(s( - m) - r( - m)) \leq M \) by (rule Int_order_transitive )
ultimately have \( abs(s(m) - r(m)) \leq M \) by (rule Int_order_transitive )
} ultimately have \( abs(s(m) - r(m)) \leq M \)
}
then have \( \forall m\in \mathbb{Z} .\ abs(s(m) - r(m)) \leq M \)
with A1 show \( s \sim r \) by (rule Int_ZF_2_1_L9 )
qed

A sufficient condition for an odd slope to be almost equal to identity: If for all positive integers the value of the slope at \(m\) is between \(m\) and \(m\) plus some constant independent of \(m\), then the slope is almost identity.

lemma (in int1) Int_ZF_2_1_L32:

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

shows \( s \sim id(\mathbb{Z} ) \)proof
let \( r = id(\mathbb{Z} ) \)
from A1 have \( s\in \mathcal{S} \), \( r \in \mathcal{S} \) using Int_ZF_2_1_L17
moreover
from A1, A2 have \( \forall m\in \mathbb{Z} _+.\ abs(s(m) - r(m)) \leq M \) using Int_ZF_1_3_L23, PositiveSet_def, id_conv
ultimately show \( s \sim id(\mathbb{Z} ) \) by (rule Int_ZF_2_1_L31 )
qed

A lemma about adding a constant to slopes. This is actually proven in Group_ZF_3_5_L1, in Group_ZF_3.thy here we just refer to that lemma to show it in notation used for integers. Unfortunately we have to use raw set notation in the proof.

lemma (in int1) Int_ZF_2_1_L33:

assumes A1: \( s\in \mathcal{S} \) and A2: \( c\in \mathbb{Z} \) and A3: \( 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 \)proof
let \( G = \mathbb{Z} \)
let \( f = IntegerAddition \)
let \( AH = \text{AlmostHoms}(G, f) \)
from assms have I: \( group1(G, f) \), \( s \in \text{AlmostHoms}(G, f) \), \( c \in G \), \( r = \{\langle x, f\langle s(x), c\rangle \rangle .\ x \in G\} \) using Int_ZF_2_1_L1
then have \( \forall x\in G.\ r(x) = f\langle s(x),c\rangle \) by (rule Group_ZF_3_5_L1 )
moreover
from I have \( r \in \text{AlmostHoms}(G, f) \) by (rule Group_ZF_3_5_L1 )
moreover
from I have \( \langle s, r\rangle \in \text{QuotientGroupRel}( \text{AlmostHoms}(G, f), \text{AlHomOp1}(G, f), \text{FinRangeFunctions}(G, G)) \) by (rule Group_ZF_3_5_L1 )
ultimately show \( \forall m\in \mathbb{Z} .\ r(m) = s(m) + c \), \( r\in \mathcal{S} \), \( s \sim r \)
qed

Composing slopes

Composition of slopes is not commutative. However, as we show in this section if \(f\) and \(g\) are slopes then the range of \(f\circ g - g\circ f\) is bounded. This allows to show that the multiplication of real numbers is commutative.

Two useful estimates.

lemma (in int1) Int_ZF_2_2_L1:

assumes A1: \( f:\mathbb{Z} \rightarrow \mathbb{Z} \) and A2: \( p\in \mathbb{Z} \), \( q\in \mathbb{Z} \)

shows \( abs(f((p + 1 )\cdot q) - (p + 1 )\cdot f(q)) \leq abs(\delta (f,p\cdot q,q)) + abs(f(p\cdot q) - p\cdot f(q)) \), \( abs(f((p - 1 )\cdot q) - (p - 1 )\cdot f(q)) \leq abs(\delta (f,(p - 1 )\cdot q,q)) + abs(f(p\cdot q) - p\cdot f(q)) \)proof
let \( R = \mathbb{Z} \)
let \( A = IntegerAddition \)
let \( M = IntegerMultiplication \)
let \( I = \text{GroupInv}(R, A) \)
let \( a = f((p + 1 )\cdot q) \)
let \( b = p \)
let \( c = f(q) \)
let \( d = f(p\cdot q) \)
from A1, A2 have T1: \( ring0(R, A, M) \), \( a \in R \), \( b \in R \), \( c \in R \), \( d \in R \) using Int_ZF_1_1_L2, int_zero_one_are_int, Int_ZF_1_1_L5, apply_funtype
then have \( A\langle a,I(M\langle A\langle b, \text{ TheNeutralElement}(R, M)\rangle ,c\rangle )\rangle =\) \( A\langle A\langle A\langle a,I(d)\rangle ,I(c)\rangle ,A\langle d, I(M\langle b, c\rangle )\rangle \rangle \) by (rule Ring_ZF_2_L2 )
with A2 have \( f((p + 1 )\cdot q) - (p + 1 )\cdot f(q) = \delta (f,p\cdot q,q) + (f(p\cdot q) - p\cdot f(q)) \) using int_zero_one_are_int, Int_ZF_1_1_L1, Int_ZF_1_1_L4
moreover
from A1, A2, T1 have \( \delta (f,p\cdot q,q) \in \mathbb{Z} \), \( f(p\cdot q) - p\cdot f(q) \in \mathbb{Z} \) using Int_ZF_1_1_L5, apply_funtype
ultimately show \( abs(f((p + 1 )\cdot q) - (p + 1 )\cdot f(q)) \leq abs(\delta (f,p\cdot q,q)) + abs(f(p\cdot q) - p\cdot f(q)) \) using Int_triangle_ineq
from A1, A2 have T1: \( f((p - 1 )\cdot q) \in \mathbb{Z} \), \( p\in \mathbb{Z} \), \( f(q) \in \mathbb{Z} \), \( f(p\cdot q) \in \mathbb{Z} \) using int_zero_one_are_int, Int_ZF_1_1_L5, apply_funtype
then have \( f((p - 1 )\cdot q) - (p - 1 )\cdot f(q) = (f(p\cdot q) - p\cdot f(q)) - (f(p\cdot q) - f((p - 1 )\cdot q) - f(q)) \) by (rule Int_ZF_1_2_L6 )
with A2 have \( f((p - 1 )\cdot q) - (p - 1 )\cdot f(q) = (f(p\cdot q) - p\cdot f(q)) - \delta (f,(p - 1 )\cdot q,q) \) using Int_ZF_1_2_L7
moreover
from A1, A2 have \( f(p\cdot q) - p\cdot f(q) \in \mathbb{Z} \), \( \delta (f,(p - 1 )\cdot q,q) \in \mathbb{Z} \) using Int_ZF_1_1_L5, int_zero_one_are_int, apply_funtype
ultimately show \( abs(f((p - 1 )\cdot q) - (p - 1 )\cdot f(q)) \leq abs(\delta (f,(p - 1 )\cdot q,q)) + abs(f(p\cdot q) - p\cdot f(q)) \) using Int_triangle_ineq1
qed

If \(f\) is a slope, then \(|f(p\cdot q)-p\cdot f(q)|\leq (|p|+1)\cdot\)\( \text{ max}\delta (f) \). The proof is by induction on \(p\) and the next lemma is the induction step for the case when \(0\leq p\).

lemma (in int1) Int_ZF_2_2_L2:

assumes A1: \( f\in \mathcal{S} \) and A2: \( 0 \leq p \), \( q\in \mathbb{Z} \) and A3: \( abs(f(p\cdot q) - p\cdot f(q)) \leq (abs(p) + 1 )\cdot \text{ max}\delta (f) \)

shows \( abs(f((p + 1 )\cdot q) - (p + 1 )\cdot f(q)) \leq (abs(p + 1 ) + 1 )\cdot \text{ max}\delta (f) \)proof
from A2 have \( q\in \mathbb{Z} \), \( p\cdot q \in \mathbb{Z} \) using Int_ZF_2_L1A, Int_ZF_1_1_L5
with A1 have I: \( abs(\delta (f,p\cdot q,q)) \leq \text{ max}\delta (f) \) by (rule Int_ZF_2_1_L7 )
moreover
note A3
moreover
from A1, A2 have \( abs(f((p + 1 )\cdot q) - (p + 1 )\cdot f(q)) \leq abs(\delta (f,p\cdot q,q)) + abs(f(p\cdot q) - p\cdot f(q)) \) using AlmostHoms_def, Int_ZF_2_L1A, Int_ZF_2_2_L1
ultimately have \( abs(f((p + 1 )\cdot q) - (p + 1 )\cdot f(q)) \leq \text{ max}\delta (f) + (abs(p) + 1 )\cdot \text{ max}\delta (f) \) by (rule Int_ZF_2_L15 )
moreover
from I, A2 have \( \text{ max}\delta (f) + (abs(p) + 1 )\cdot \text{ max}\delta (f) = (abs(p + 1 ) + 1 )\cdot \text{ max}\delta (f) \) using Int_ZF_2_L1A, Int_ZF_1_2_L2
ultimately show \( abs(f((p + 1 )\cdot q) - (p + 1 )\cdot f(q)) \leq (abs(p + 1 ) + 1 )\cdot \text{ max}\delta (f) \)
qed

If \(f\) is a slope, then \(|f(p\cdot q)-p\cdot f(q)|\leq (|p|+1)\cdot\)\( \text{ max}\delta \). The proof is by induction on \(p\) and the next lemma is the induction step for the case when \(p\leq 0\).

lemma (in int1) Int_ZF_2_2_L3:

assumes A1: \( f\in \mathcal{S} \) and A2: \( p\leq 0 \), \( q\in \mathbb{Z} \) and A3: \( abs(f(p\cdot q) - p\cdot f(q)) \leq (abs(p) + 1 )\cdot \text{ max}\delta (f) \)

shows \( abs(f((p - 1 )\cdot q) - (p - 1 )\cdot f(q)) \leq (abs(p - 1 ) + 1 )\cdot \text{ max}\delta (f) \)proof
from A2 have \( q\in \mathbb{Z} \), \( (p - 1 )\cdot q \in \mathbb{Z} \) using Int_ZF_2_L1A, int_zero_one_are_int, Int_ZF_1_1_L5
with A1 have I: \( abs(\delta (f,(p - 1 )\cdot q,q)) \leq \text{ max}\delta (f) \) by (rule Int_ZF_2_1_L7 )
moreover
note A3
moreover
from A1, A2 have \( abs(f((p - 1 )\cdot q) - (p - 1 )\cdot f(q)) \leq abs(\delta (f,(p - 1 )\cdot q,q)) + abs(f(p\cdot q) - p\cdot f(q)) \) using AlmostHoms_def, Int_ZF_2_L1A, Int_ZF_2_2_L1
ultimately have \( abs(f((p - 1 )\cdot q) - (p - 1 )\cdot f(q)) \leq \text{ max}\delta (f) + (abs(p) + 1 )\cdot \text{ max}\delta (f) \) by (rule Int_ZF_2_L15 )
with I, A2 show \( thesis \) using Int_ZF_2_L1A, Int_ZF_1_2_L5
qed

If \(f\) is a slope, then \(|f(p\cdot q)-p\cdot f(q)|\leq (|p|+1)\cdot\)\( \text{ max}\delta \)\((f)\). Proof by cases on \(0 \leq p\).

lemma (in int1) Int_ZF_2_2_L4:

assumes A1: \( f\in \mathcal{S} \) and A2: \( p\in \mathbb{Z} \), \( q\in \mathbb{Z} \)

shows \( abs(f(p\cdot q) - p\cdot f(q)) \leq (abs(p) + 1 )\cdot \text{ max}\delta (f) \)proof
{
assume \( 0 \leq p \)
moreover
from A1, A2 have \( abs(f( 0 \cdot q) - 0 \cdot f(q)) \leq (abs( 0 ) + 1 )\cdot \text{ max}\delta (f) \) using int_zero_one_are_int, Int_ZF_2_1_L2B, Int_ZF_1_1_L4, Int_ZF_2_1_L8, Int_ZF_2_L18
moreover
from A1, A2 have \( \forall p.\ 0 \leq p \wedge abs(f(p\cdot q) - p\cdot f(q)) \leq (abs(p) + 1 )\cdot \text{ max}\delta (f) \longrightarrow \) \( abs(f((p + 1 )\cdot q) - (p + 1 )\cdot f(q)) \leq (abs(p + 1 ) + 1 )\cdot \text{ max}\delta (f) \) using Int_ZF_2_2_L2
ultimately have \( abs(f(p\cdot q) - p\cdot f(q)) \leq (abs(p) + 1 )\cdot \text{ max}\delta (f) \) by (rule Induction_on_int )
}
moreover {
assume \( \neg ( 0 \leq p) \)
with A2 have \( p\leq 0 \) using Int_ZF_2_L19A
moreover
from A1, A2 have \( abs(f( 0 \cdot q) - 0 \cdot f(q)) \leq (abs( 0 ) + 1 )\cdot \text{ max}\delta (f) \) using int_zero_one_are_int, Int_ZF_2_1_L2B, Int_ZF_1_1_L4, Int_ZF_2_1_L8, Int_ZF_2_L18
moreover
from A1, A2 have \( \forall p.\ p\leq 0 \wedge abs(f(p\cdot q) - p\cdot f(q)) \leq (abs(p) + 1 )\cdot \text{ max}\delta (f) \longrightarrow \) \( abs(f((p - 1 )\cdot q) - (p - 1 )\cdot f(q)) \leq (abs(p - 1 ) + 1 )\cdot \text{ max}\delta (f) \) using Int_ZF_2_2_L3
ultimately have \( abs(f(p\cdot q) - p\cdot f(q)) \leq (abs(p) + 1 )\cdot \text{ max}\delta (f) \) by (rule Back_induct_on_int )
} ultimately show \( thesis \)
qed

The next elegant result is Lemma 7 in the Arthan's paper \cite{Arthan2004}.

lemma (in int1) Arthan_Lem_7:

assumes A1: \( f\in \mathcal{S} \) and A2: \( p\in \mathbb{Z} \), \( q\in \mathbb{Z} \)

shows \( abs(q\cdot f(p) - p\cdot f(q)) \leq (abs(p) + abs(q) + 2 )\cdot \text{ max}\delta (f) \)proof
from A1, A2 have T: \( q\cdot f(p) - f(p\cdot q) \in \mathbb{Z} \), \( f(p\cdot q) - p\cdot f(q) \in \mathbb{Z} \), \( f(q\cdot p) \in \mathbb{Z} \), \( f(p\cdot q) \in \mathbb{Z} \), \( q\cdot f(p) \in \mathbb{Z} \), \( p\cdot f(q) \in \mathbb{Z} \), \( \text{ max}\delta (f) \in \mathbb{Z} \), \( abs(q) \in \mathbb{Z} \), \( abs(p) \in \mathbb{Z} \) using Int_ZF_1_1_L5, Int_ZF_2_1_L2B, Int_ZF_2_1_L7, Int_ZF_2_L14
moreover
have \( abs(q\cdot f(p) - f(p\cdot q)) \leq (abs(q) + 1 )\cdot \text{ max}\delta (f) \)proof
from A1, A2 have \( abs(f(q\cdot p) - q\cdot f(p)) \leq (abs(q) + 1 )\cdot \text{ max}\delta (f) \) using Int_ZF_2_2_L4
with T, A2 show \( thesis \) using Int_ZF_2_L20, Int_ZF_1_1_L5
qed
moreover
from A1, A2 have \( abs(f(p\cdot q) - p\cdot f(q)) \leq (abs(p) + 1 )\cdot \text{ max}\delta (f) \) using Int_ZF_2_2_L4
ultimately have \( abs(q\cdot f(p) - f(p\cdot q) + (f(p\cdot q) - p\cdot f(q))) \leq (abs(q) + 1 )\cdot \text{ max}\delta (f) + (abs(p) + 1 )\cdot \text{ max}\delta (f) \) using Int_ZF_2_L21
with T show \( thesis \) using Int_ZF_1_2_L9, int_zero_one_are_int, Int_ZF_1_2_L10
qed

This is Lemma 8 in the Arthan's paper.

lemma (in int1) Arthan_Lem_8:

assumes A1: \( 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) \)proof
let \( A = \text{ max}\delta (f) + abs(f(1 )) \)
let \( B = 3 \cdot \text{ max}\delta (f) \)
from A1 have \( A\in \mathbb{Z} \), \( B\in \mathbb{Z} \) using int_zero_one_are_int, Int_ZF_1_1_L5, Int_ZF_2_1_L2B, Int_ZF_2_1_L7, Int_ZF_2_L14
moreover
have \( \forall p\in \mathbb{Z} .\ abs(f(p)) \leq A\cdot abs(p) + B \)proof
fix \( p \)
assume A2: \( p\in \mathbb{Z} \)
with A1 have T: \( f(p) \in \mathbb{Z} \), \( abs(p) \in \mathbb{Z} \), \( f(1 ) \in \mathbb{Z} \), \( p\cdot f(1 ) \in \mathbb{Z} \), \( 3 \in \mathbb{Z} \), \( \text{ max}\delta (f) \in \mathbb{Z} \) using Int_ZF_2_1_L2B, Int_ZF_2_L14, int_zero_one_are_int, Int_ZF_1_1_L5, Int_ZF_2_1_L7
from A1, A2 have \( abs(1 \cdot f(p) - p\cdot f(1 )) \leq (abs(p) + abs(1 ) + 2 )\cdot \text{ max}\delta (f) \) using int_zero_one_are_int, Arthan_Lem_7
with T have \( abs(f(p)) \leq abs(p\cdot f(1 )) + (abs(p) + 3 )\cdot \text{ max}\delta (f) \) using Int_ZF_2_L16A, Int_ZF_1_1_L4, Int_ZF_1_2_L11, Int_triangle_ineq2
with A2, T show \( abs(f(p)) \leq A\cdot abs(p) + B \) using Int_ZF_1_3_L14
qed
ultimately show \( thesis \)
qed

If \(f\) and \(g\) are slopes, then \(f\circ g\) is equivalent (almost equal) to \(g\circ f\). This is Theorem 9 in Arthan's paper \cite{Arthan2004}.

theorem (in int1) Arthan_Th_9:

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

shows \( f\circ g \sim g\circ f \)proof
from A1 have \( \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) \), \( \exists C D.\ C\in \mathbb{Z} \wedge D\in \mathbb{Z} \wedge (\forall p\in \mathbb{Z} .\ abs(g(p)) \leq C\cdot abs(p) + D) \) using Arthan_Lem_8
then obtain \( A \) \( B \) \( C \) \( D \) where D1: \( A\in \mathbb{Z} \), \( B\in \mathbb{Z} \), \( C\in \mathbb{Z} \), \( D\in \mathbb{Z} \) and D2: \( \forall p\in \mathbb{Z} .\ abs(f(p)) \leq A\cdot abs(p) + B \), \( \forall p\in \mathbb{Z} .\ abs(g(p)) \leq C\cdot abs(p) + D \)
let \( E = \text{ max}\delta (g)\cdot (A + 1 ) + \text{ max}\delta (f)\cdot (C + 1 ) \)
let \( F = (B\cdot \text{ max}\delta (g) + 2 \cdot \text{ max}\delta (g)) + (D\cdot \text{ max}\delta (f) + 2 \cdot \text{ max}\delta (f)) \)
{
fix \( p \)
assume A2: \( p\in \mathbb{Z} \)
with A1 have T1: \( g(p) \in \mathbb{Z} \), \( f(p) \in \mathbb{Z} \), \( abs(p) \in \mathbb{Z} \), \( 2 \in \mathbb{Z} \), \( f(g(p)) \in \mathbb{Z} \), \( g(f(p)) \in \mathbb{Z} \), \( f(g(p)) - g(f(p)) \in \mathbb{Z} \), \( p\cdot f(g(p)) \in \mathbb{Z} \), \( p\cdot g(f(p)) \in \mathbb{Z} \), \( abs(f(g(p)) - g(f(p))) \in \mathbb{Z} \) using Int_ZF_2_1_L2B, Int_ZF_2_1_L10, Int_ZF_1_1_L5, Int_ZF_2_L14, int_two_three_are_int
with A1, A2 have \( abs((f(g(p)) - g(f(p)))\cdot p) \leq \) \( (abs(p) + abs(f(p)) + 2 )\cdot \text{ max}\delta (g) + (abs(p) + abs(g(p)) + 2 )\cdot \text{ max}\delta (f) \) using Arthan_Lem_7, Int_ZF_1_2_L10A, Int_ZF_1_2_L12
moreover
have \( (abs(p) + abs(f(p)) + 2 )\cdot \text{ max}\delta (g) + (abs(p) + abs(g(p)) + 2 )\cdot \text{ max}\delta (f) \leq \) \( ((\text{ max}\delta (g)\cdot (A + 1 ) + \text{ max}\delta (f)\cdot (C + 1 )))\cdot abs(p) + \) \( ((B\cdot \text{ max}\delta (g) + 2 \cdot \text{ max}\delta (g)) + (D\cdot \text{ max}\delta (f) + 2 \cdot \text{ max}\delta (f))) \)proof
from D2, A2, T1 have \( abs(p) + abs(f(p)) + 2 \leq abs(p) + (A\cdot abs(p) + B) + 2 \), \( abs(p) + abs(g(p)) + 2 \leq abs(p) + (C\cdot abs(p) + D) + 2 \) using Int_ZF_2_L15C
with A1 have \( (abs(p) + abs(f(p)) + 2 )\cdot \text{ max}\delta (g) \leq (abs(p) + (A\cdot abs(p) + B) + 2 )\cdot \text{ max}\delta (g) \), \( (abs(p) + abs(g(p)) + 2 )\cdot \text{ max}\delta (f) \leq (abs(p) + (C\cdot abs(p) + D) + 2 )\cdot \text{ max}\delta (f) \) using Int_ZF_2_1_L8, Int_ZF_1_3_L13
moreover
from A1, D1, T1 have \( (abs(p) + (A\cdot abs(p) + B) + 2 )\cdot \text{ max}\delta (g) = \) \( \text{ max}\delta (g)\cdot (A + 1 )\cdot abs(p) + (B\cdot \text{ max}\delta (g) + 2 \cdot \text{ max}\delta (g)) \), \( (abs(p) + (C\cdot abs(p) + D) + 2 )\cdot \text{ max}\delta (f) = \) \( \text{ max}\delta (f)\cdot (C + 1 )\cdot abs(p) + (D\cdot \text{ max}\delta (f) + 2 \cdot \text{ max}\delta (f)) \) using Int_ZF_2_1_L8, Int_ZF_1_2_L13
ultimately have \( (abs(p) + abs(f(p)) + 2 )\cdot \text{ max}\delta (g) + (abs(p) + abs(g(p)) + 2 )\cdot \text{ max}\delta (f) \leq \) \( (\text{ max}\delta (g)\cdot (A + 1 )\cdot abs(p) + (B\cdot \text{ max}\delta (g) + 2 \cdot \text{ max}\delta (g))) + \) \( (\text{ max}\delta (f)\cdot (C + 1 )\cdot abs(p) + (D\cdot \text{ max}\delta (f) + 2 \cdot \text{ max}\delta (f))) \) using int_ineq_add_sides
moreover
from A1, A2, D1 have \( abs(p) \in \mathbb{Z} \), \( \text{ max}\delta (g)\cdot (A + 1 ) \in \mathbb{Z} \), \( B\cdot \text{ max}\delta (g) + 2 \cdot \text{ max}\delta (g) \in \mathbb{Z} \), \( \text{ max}\delta (f)\cdot (C + 1 ) \in \mathbb{Z} \), \( D\cdot \text{ max}\delta (f) + 2 \cdot \text{ max}\delta (f) \in \mathbb{Z} \) using Int_ZF_2_L14, Int_ZF_2_1_L8, int_zero_one_are_int, Int_ZF_1_1_L5, int_two_three_are_int
ultimately show \( thesis \) using Int_ZF_1_2_L14
qed
ultimately have \( abs((f(g(p)) - g(f(p)))\cdot p) \leq E\cdot abs(p) + F \) by (rule Int_order_transitive )
with A2, T1 have \( abs(f(g(p)) - g(f(p)))\cdot abs(p) \leq E\cdot abs(p) + F \), \( abs(f(g(p)) - g(f(p))) \in \mathbb{Z} \) using Int_ZF_1_3_L5
}
then have \( \forall p\in \mathbb{Z} .\ abs(f(g(p)) - g(f(p))) \in \mathbb{Z} \), \( \forall p\in \mathbb{Z} .\ abs(f(g(p)) - g(f(p)))\cdot abs(p) \leq E\cdot abs(p) + F \)
moreover
from A1, D1 have \( E \in \mathbb{Z} \), \( F \in \mathbb{Z} \) using int_zero_one_are_int, int_two_three_are_int, Int_ZF_2_1_L8, Int_ZF_1_1_L5
ultimately have \( \exists L.\ \forall p\in \mathbb{Z} .\ abs(f(g(p)) - g(f(p))) \leq L \) by (rule Int_ZF_1_7_L1 )
with A1 obtain \( L \) where \( \forall p\in \mathbb{Z} .\ abs((f\circ g)(p) - (g\circ f)(p)) \leq L \) using Int_ZF_2_1_L10
moreover
from A1 have \( f\circ g \in \mathcal{S} \), \( g\circ f \in \mathcal{S} \) using Int_ZF_2_1_L11
ultimately show \( f\circ g \sim g\circ f \) using Int_ZF_2_1_L9
qed
end
theorem Int_ZF_1_T2: shows \( \text{IsAgroup}(int,IntegerAddition) \), \( IntegerAddition \text{ is commutative on } int \), \( group0(int,IntegerAddition) \)
lemma (in int1) Int_ZF_2_1_L1: shows \( group1(\mathbb{Z} ,IntegerAddition) \)
corollary (in group1) Group_ZF_3_2_L4A:

assumes \( s \in AH \) and \( m\in G \), \( n\in G \)

shows \( m\cdot n \in G \), \( s(m\cdot n) \in G \), \( s(m) \in G \), \( s(n) \in G \), \( \delta (s,\langle m,n\rangle ) \in G \), \( s(m)\cdot s(n) \in G \)
lemma (in group1) Group_ZF_3_2_L4:

assumes \( s:G\rightarrow G \) and \( m\in G \), \( n\in G \)

shows \( m\cdot n \in G \), \( s(m\cdot n) \in G \), \( s(m) \in G \), \( s(n) \in G \), \( \delta (s,\langle m,n\rangle ) \in G \), \( s(m)\cdot s(n) \in G \)
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_1_L2A:

assumes \( f:\mathbb{Z} \rightarrow \mathbb{Z} \) and \( n\in \mathbb{Z} \), \( m\in \mathbb{Z} \)

shows \( m + n \in \mathbb{Z} \), \( f(m + n) \in \mathbb{Z} \), \( f(m) \in \mathbb{Z} \), \( f(n) \in \mathbb{Z} \), \( f(m) + f(n) \in \mathbb{Z} \), \( \text{HomDiff}(\mathbb{Z} ,IntegerAddition,f,\langle m,n\rangle ) \in \mathbb{Z} \)
lemma (in group0) group0_4_L4A:

assumes \( P \text{ is commutative on } G \) and \( a\in G \), \( b\in G \), \( c\in G \)

shows \( a\cdot b\cdot c = c\cdot a\cdot b \), \( a^{-1}\cdot (b^{-1}\cdot c^{-1})^{-1} = (a\cdot (b\cdot c)^{-1})^{-1} \), \( a\cdot (b\cdot c)^{-1} = a\cdot b^{-1}\cdot c^{-1} \), \( a\cdot (b\cdot c^{-1})^{-1} = a\cdot b^{-1}\cdot c \), \( a\cdot b^{-1}\cdot c^{-1} = a\cdot c^{-1}\cdot b^{-1} \)
Definition of HomDiff: \( \text{HomDiff}(G,f,s,x) \equiv \) \( f\langle s(f\langle \text{fst}(x),\text{snd}(x)\rangle ) , \) \( ( \text{GroupInv}(G,f)(f\langle s(\text{fst}(x)),s(\text{snd}(x))\rangle ))\rangle \)
lemma (in int1) Int_ZF_2_1_L2:

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

shows \( m + n \in \mathbb{Z} \), \( f(m + n) \in \mathbb{Z} \), \( f(m) \in \mathbb{Z} \), \( f(n) \in \mathbb{Z} \), \( f(m) + f(n) \in \mathbb{Z} \), \( \text{HomDiff}(\mathbb{Z} ,IntegerAddition,f,\langle m,n\rangle ) \in \mathbb{Z} \)
lemma (in int1) Int_ZF_2_1_L3:

assumes \( f:\mathbb{Z} \rightarrow \mathbb{Z} \) and \( m\in \mathbb{Z} \), \( n\in \mathbb{Z} \)

shows \( \text{HomDiff}(\mathbb{Z} ,IntegerAddition,f,\langle m,n\rangle ) = \delta (f,m,n) \)
lemma (in int0) Int_ZF_1_L3:

assumes \( x\in \mathbb{Z} \), \( y\in \mathbb{Z} \), \( z\in \mathbb{Z} \)

shows \( x + y + z = x + (y + z) \), \( x\cdot y\cdot z = x\cdot (y\cdot z) \)
lemma (in group1) Group_ZF_3_4_L1:

assumes \( s\in AH \) and \( m\in G \), \( n\in G \)

shows \( s(m\cdot n) = s(m)\cdot s(n)\cdot \delta (s,\langle m,n\rangle ) \)
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_2_L15:

assumes \( a\in \mathbb{Z} \), \( b\in \mathbb{Z} \), \( c\in \mathbb{Z} \), \( d\in \mathbb{Z} \) and \( a = b - c - d \)

shows \( d = b - a - c \), \( d = ( - a) + b - c \), \( b = a + d + c \)
lemma ZF1_1_L4A:

assumes \( \forall x\in X.\ \forall y\in Y.\ a(\langle x,y\rangle ) = b(x,y) \)

shows \( \{a(p).\ p \in X\times Y\} = \{b(x,y).\ \langle x,y\rangle \in X\times 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_3_L9A:

assumes \( r \text{ is total on } G \) and \( \forall x\in X.\ b(x)\in G \wedge \vert b(x)\vert \leq L \)

shows \( \text{IsBounded}(\{b(x).\ x\in X\},r) \)
theorem (in int0) Int_bounded_iff_fin: shows \( \text{IsBounded}(A,IntegerOrder)\longleftrightarrow A\in Fin(\mathbb{Z} ) \)
lemma (in int0) Int_ZF_2_L14:

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

shows \( abs(m) \in \mathbb{Z} \)
lemma Finite1_L6C:

assumes \( \forall y\in Y.\ b(y) \in Z \) and \( \{a(x).\ x\in X\} \in Fin(Y) \)

shows \( \{b(a(x)).\ x\in X\} \in Fin(Z) \)
theorem Finite_ZF_1_T2:

assumes \( \text{IsLinOrder}(X,r) \) and \( A \in Fin(X) \) and \( A\neq 0 \)

shows \( \text{Maximum}(r,A) \in A \), \( \text{Minimum}(r,A) \in A \), \( \forall x\in A.\ \langle x, \text{Maximum}(r,A)\rangle \in r \), \( \forall x\in A.\ \langle \text{Minimum}(r,A),x\rangle \in r \)
lemma (in int1) Int_ZF_2_1_L4:

assumes \( f:\mathbb{Z} \rightarrow \mathbb{Z} \)

shows \( \{abs( \text{HomDiff}(\mathbb{Z} ,IntegerAddition,f,x)).\ x \in \mathbb{Z} \times \mathbb{Z} \} =\) \( \{abs(\delta (f,m,n)).\ \langle m,n\rangle \in \mathbb{Z} \times \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_1_3_L19:

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

shows \( ( - n) \leq m \), \( m \leq n \), \( m \in ( - n).\ .\ n \), \( 0 \leq n \)
lemma (in int0) int_zero_one_are_int: shows \( 0 \in \mathbb{Z} \), \( 1 \in \mathbb{Z} \)
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_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_ZF_2_L17:

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

shows \( abs( - m) = abs(m) \)
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_order_transitive:

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

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

assumes \( \forall x\in X.\ b(x) \in \mathbb{Z} \wedge abs(b(x)) \leq L \)

shows \( \text{IsBounded}(\{b(x).\ x\in X\},IntegerOrder) \)
lemma (in group1) Group_ZF_3_4_L12:

assumes \( s\in AH \), \( r\in AH \) and \( \{s(n)\cdot (r(n))^{-1}.\ n\in G\} \in Fin(G) \)

shows \( s\cong r \)
lemma (in group1) Group_ZF_3_4_L11:

assumes \( s\cong r \)

shows \( \{s(n)\cdot (r(n))^{-1}.\ n\in G\} \in Fin(G) \)
lemma (in int0) Int_ZF_1_3_L20AA:

assumes \( \{b(x).\ x\in \mathbb{Z} \} \in Fin(\mathbb{Z} ) \)

shows \( \exists L\in \mathbb{Z} .\ \forall x\in \mathbb{Z} .\ abs(b(x)) \leq L \)
Definition of QuotientGroupRel: \( \text{QuotientGroupRel}(G,P,H) \equiv \) \( \{\langle a,b\rangle \in G\times G.\ P\langle a, \text{GroupInv}(G,P)(b)\rangle \in H\} \)
lemma (in group1) Group_ZF_3_3_L3: shows \( \text{QuotientGroupRel}(AH,Op1,FR) \subseteq AH \times AH \) and \( \text{equiv}(AH, \text{QuotientGroupRel}(AH,Op1,FR)) \)
lemma (in group1) Group_ZF_3_2_L13:

assumes \( s\in AH \)

shows \( \text{GroupInv}(AH,Op1)(s) = \text{GroupInv}(G,P)\circ s \), \( \text{GroupInv}(AH,Op1)(s) \in AH \), \( \text{GroupInv}(G,P)\circ s \in AH \)
lemma (in group1) Group_ZF_3_4_L12A:

assumes \( s\in AH \), \( r\in AH \) and \( s\bullet ( \text{GroupInv}(AH,Op1)(r)) \in FR \)

shows \( s\cong r \), \( r\cong s \)
lemma (in group1) Group_ZF_3_4_L12B:

assumes \( s\cong r \)

shows \( s\bullet ( \text{GroupInv}(AH,Op1)(r)) \in FR \)
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 group1) Group_ZF_3_4_L2:

assumes \( s\in AH \), \( r\in AH \) and \( m\in G \)

shows \( (s\circ r)(m) = s(r(m)) \), \( s(r(m)) \in G \)
theorem (in group1) Group_ZF_3_4_T1:

assumes \( s\in AH \), \( r\in AH \)

shows \( \text{Composition}(G)\langle s,r\rangle \in AH \), \( s\circ r \in AH \)
lemma (in group1) Group_ZF_3_2_L5:

assumes \( s \in AH \) and \( n\in G \)

shows \( (\sim s)(n) = (s(n))^{-1} \)
lemma (in group1) Group_ZF_3_2_L12:

assumes \( s\in AH \), \( r\in AH \) and \( n\in G \)

shows \( (s\bullet r)(n) = s(n)\cdot r(n) \)
corollary (in group1) Group_ZF_3_2_L16:

assumes \( s \in AH \), \( r \in AH \)

shows \( s\bullet r \in AH \), \( s\bullet (\sim r) \in AH \)
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 int0) Int_ZF_1_2_L7:

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

shows \( a\cdot b = (a - 1 )\cdot b + b \), \( a\cdot (b + 1 ) = a\cdot b + a \), \( (b + 1 )\cdot a = b\cdot a + a \), \( (b + 1 )\cdot a = a + b\cdot a \)
lemma (in int0) Int_triangle_ineq1:

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

shows \( abs(m - n) \leq abs(n) + abs(m) \), \( abs(m - n) \leq abs(m) + abs(n) \)
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_1_3_L21:

assumes \( a\leq c \), \( b\leq c \)

shows \( a + b \leq 2 \cdot c \)
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_triangle_ineq3:

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

shows \( abs(a - b - c) \leq abs(a) + abs(b) + abs(c) \)
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 int0) Int_ZF_2_L15E:

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

shows \( m + n \leq abs(m) + abs(n) \), \( m - n \leq abs(m) + abs(n) \), \( ( - m) + n \leq abs(m) + abs(n) \), \( ( - m) - n \leq abs(m) + abs(n) \)
lemma (in int0) Int_ZF_1_5_L6:

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

shows \( 0 \leq n - 1 \), \( 0 \in 0 .\ .\ (n - 1 ) \), \( 0 .\ .\ (n - 1 ) \subseteq \mathbb{Z} \)
lemma (in int0) Int_ZF_1_4_L2:

assumes \( f:\mathbb{Z} \rightarrow \mathbb{Z} \) and \( a\leq b \)

shows \( maxf(f,a.\ .\ b) \in \mathbb{Z} \), \( \forall c \in a.\ .\ b.\ f(c) \leq maxf(f,a.\ .\ b) \), \( \exists c \in a.\ .\ b.\ f(c) = maxf(f,a.\ .\ b) \), \( minf(f,a.\ .\ b) \in \mathbb{Z} \), \( \forall c \in a.\ .\ b.\ minf(f,a.\ .\ b) \leq f(c) \), \( \exists c \in a.\ .\ b.\ f(c) = minf(f,a.\ .\ b) \)
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 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_ineq_add_sides:

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

shows \( a + c \leq b + d \), \( a - d \leq b - c \)
lemma (in int1) Int_ZF_2_1_L3A:

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

shows \( f(m + n) = f(m) + (f(n) + \delta (f,m,n)) \)
lemma (in group1) Group_ZF_3_4_L15: shows \( id(G) \in AH \)
lemma (in int0) Int_ZF_1_2_L9A:

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

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

assumes \( f:\mathbb{Z} \rightarrow \mathbb{Z} \) and \( m\in \mathbb{Z} \), \( n\in \mathbb{Z} \)

shows \( abs(f(n) + f(m) - f(m + n)) = abs(\delta (f,m,n)) \), \( abs(f(m) + f(n) - f(m + n)) = abs(\delta (f,m,n)) \), \( ( - (f(m))) - f(n) + f(m + n) = \delta (f,m,n) \), \( ( - (f(n))) - f(m) + f(m + n) = \delta (f,m,n) \), \( abs(( - f(m + n)) + f(m) + f(n)) = abs(\delta (f,m,n)) \)
lemma (in int0) Int_ZF_1_5_L13:

assumes \( f: \mathbb{Z} \rightarrow \mathbb{Z} \)

shows \( (\forall a\in \mathbb{Z} .\ f( - a) = ( - f(a))) \longleftrightarrow (\forall a\in \mathbb{Z} .\ ( - (f( - a))) = f(a)) \)
lemma (in int0) int_one_two_are_pos: shows \( 1 \in \mathbb{Z} _+ \), \( 2 \in \mathbb{Z} _+ \)
lemma (in int1) Int_ZF_2_1_L3B:

assumes \( f:\mathbb{Z} \rightarrow \mathbb{Z} \) and \( m\in \mathbb{Z} \), \( n\in \mathbb{Z} \)

shows \( \delta (f,m,n) \in \mathbb{Z} \)
Definition of Nonnegative: \( \text{Nonnegative}(L,A,r) \equiv \{x\in L.\ \langle \text{ TheNeutralElement}(L,A),x\rangle \in r\} \)
lemma (in int0) Int_ZF_1_5_L3A: shows \( \mathbb{Z} ^+ = \mathbb{Z} _+ \cup \{ 0 \} \)
lemma (in int0) int_ord_is_refl: shows \( \text{refl}(\mathbb{Z} ,IntegerOrder) \)
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 int1) Int_ZF_2_1_L20:

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 \) and \( m\in \mathbb{Z} ^+ \), \( n\in \mathbb{Z} _+ \)

shows \( 0 \leq L \), \( abs(\delta (f,m,n)) \leq L + abs(f( 0 )) \)
lemma (in int1) Int_ZF_2_1_L21:

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 \) and \( n\in \mathbb{Z} ^+ \), \( m\in \mathbb{Z} ^+ \)

shows \( abs(\delta (f,m,n)) \leq L + abs(f( 0 )) \)
lemma (in int1) Int_ZF_2_1_L22:

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 \( \exists M.\ \forall m\in \mathbb{Z} ^+.\ \forall n\in \mathbb{Z} ^+.\ abs(\delta (f,m,n)) \leq M \)
lemma (in int0) int_plane_split_in6:

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

shows \( 0 \leq a \wedge 0 \leq b \vee a\leq 0 \wedge b\leq 0 \vee \) \( a\leq 0 \wedge 0 \leq b \wedge 0 \leq a + b \vee a\leq 0 \wedge 0 \leq b \wedge a + b \leq 0 \vee \) \( 0 \leq a \wedge b\leq 0 \wedge 0 \leq a + b \vee 0 \leq a \wedge b\leq 0 \wedge a + b \leq 0 \)
lemma (in int0) Int_ZF_2_L16:

assumes \( 0 \leq m \)

shows \( m\in \mathbb{Z} ^+ \) and \( abs(m) = m \)
lemma (in int0) Int_ZF_2_L10A:

assumes \( k \leq 0 \)

shows \( 0 \leq ( - k) \)
lemma (in int1) Int_ZF_2_1_L19:

assumes \( f:\mathbb{Z} \rightarrow \mathbb{Z} \) and \( \forall x\in \mathbb{Z} .\ ( - f( - x)) = f(x) \) and \( m\in \mathbb{Z} \), \( n\in \mathbb{Z} \)

shows \( abs(\delta (f, - m,m + n)) = abs(\delta (f,m,n)) \), \( abs(\delta (f, - n,m + n)) = abs(\delta (f,m,n)) \), \( \delta (f,n, - (m + n)) = \delta (f,m,n) \), \( \delta (f,m, - (m + n)) = \delta (f,m,n) \), \( abs(\delta (f, - m, - n)) = abs(\delta (f,m,n)) \)
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 int0) Int_ZF_1_5_L10:

assumes \( f : \mathbb{Z} _+\rightarrow \mathbb{Z} \)

shows \( \text{OddExtension}(\mathbb{Z} ,IntegerAddition,IntegerOrder,f) : \mathbb{Z} \rightarrow \mathbb{Z} \)
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 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 int0) int_oddext_is_odd_alt:

assumes \( f : \mathbb{Z} _+\rightarrow \mathbb{Z} \) and \( a\in \mathbb{Z} \) and \( g = \text{OddExtension}(\mathbb{Z} ,IntegerAddition,IntegerOrder,f) \)

shows \( ( - g( - a)) = g(a) \)
lemma (in int1) Int_ZF_2_1_L23:

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 \) and \( \forall x\in \mathbb{Z} .\ ( - f( - x)) = f(x) \)

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

assumes \( f:\mathbb{Z} \rightarrow \mathbb{Z} \) and \( m\in \mathbb{Z} \), \( n\in \mathbb{Z} \)

shows \( \delta (f,m, - n) \in \mathbb{Z} \), \( \delta (f,n, - n) \in \mathbb{Z} \), \( ( - \delta (f,n, - n)) \in \mathbb{Z} \), \( f( 0 ) \in \mathbb{Z} \), \( \gamma (f,m,n) \in \mathbb{Z} \)
lemma (in int1) Int_ZF_2_1_L3C:

assumes \( f:\mathbb{Z} \rightarrow \mathbb{Z} \) and \( m\in \mathbb{Z} \), \( n\in \mathbb{Z} \)

shows \( f(m + n) = \delta (f,m,n) + f(n) + f(m) \)
lemma (in int1) Int_ZF_2_1_L14A:

assumes \( f:\mathbb{Z} \rightarrow \mathbb{Z} \) and \( m\in \mathbb{Z} \)

shows \( f( - m) = ( - \delta (f,m, - m)) + f( 0 ) - f(m) \)
lemma (in int0) Int_ZF_1_2_L16:

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

shows \( a + (b - c) + d = a + b + d - c \)
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_2_L18:

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

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

assumes \( f:\mathbb{Z} \rightarrow \mathbb{Z} \) and \( m\in \mathbb{Z} \), \( n\in \mathbb{Z} \)

shows \( f(m - n) = \gamma (f,m,n) + f(m) - f(n) \), \( f(m - n) = \gamma (f,m,n) + (f(m) - f(n)) \), \( f(m - n) + (f(n) - \gamma (f,m,n)) = f(m) \)
lemma (in int0) Int_ZF_1_2_L17:

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

shows \( a + b - c + (c - b) = a \), \( a + (b + c) - c = a + b \)
lemma (in int0) Int_triangle_ineq3:

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

shows \( abs(m + n + k) \leq abs(m) + abs(n) + abs(k) \)
lemma (in int1) Int_ZF_2_1_L27:

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

shows \( \exists L\in \mathbb{Z} .\ \forall m\in \mathbb{Z} .\ \forall n\in \mathbb{Z} .\ abs(\gamma (s,m,n)) \leq L \)
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_triangle_ineq:

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

shows \( abs(m + n)\leq abs(m) + abs(n) \)
lemma (in int1) Int_ZF_2_1_L26A:

assumes \( f:\mathbb{Z} \rightarrow \mathbb{Z} \) and \( m\in \mathbb{Z} \), \( n\in \mathbb{Z} \), \( k\in \mathbb{Z} \)

shows \( f(m - n - k) - (f(m) - f(n) - f(k)) = \gamma (f,m - n,k) + \gamma (f,m,n) \)
lemma (in int1) Int_ZF_2_1_L29:

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} .\ abs(s(m - n - k) - (s(m) - s(n) - s(k))) \leq 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 int0) int_two_three_are_int: shows \( 2 \in \mathbb{Z} \), \( 3 \in \mathbb{Z} \)
lemma (in int0) Int_ZF_1_4_L1A:

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

shows \( \text{Maximum}(IntegerOrder,\{a,b,c\}) \in \mathbb{Z} \), \( a \leq \text{Maximum}(IntegerOrder,\{a,b,c\}) \), \( b \leq \text{Maximum}(IntegerOrder,\{a,b,c\}) \), \( c \leq \text{Maximum}(IntegerOrder,\{a,b,c\}) \)
lemma (in int0) int_decomp_cases:

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

shows \( m= 0 \vee m\in \mathbb{Z} _+ \vee ( - m) \in \mathbb{Z} _+ \)
lemma (in int0) Int_ZF_1_3_L22A:

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

shows \( abs(a - c) \leq abs(a + b) + abs(c + d) + abs(b - d) \)
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 int1) Int_ZF_2_1_L9:

assumes \( s\in \mathcal{S} \), \( r\in \mathcal{S} \) and \( \forall m\in \mathbb{Z} .\ abs(s(m) - r(m)) \leq L \)

shows \( s \sim r \)
lemma (in int1) Int_ZF_2_1_L17: shows \( id(\mathbb{Z} ) \in \mathcal{S} \)
lemma (in int0) Int_ZF_1_3_L23:

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

shows \( abs(b - a) \leq c \)
lemma (in int1) Int_ZF_2_1_L31:

assumes \( s\in \mathcal{S} \), \( r\in \mathcal{S} \) and \( \forall m\in \mathbb{Z} _+.\ abs(s(m) - r(m)) \leq L \)

shows \( s \sim r \)
lemma (in group1) Group_ZF_3_5_L1:

assumes \( s \in AH \) and \( c\in G \) and \( r = \{\langle x,s(x)\cdot c\rangle .\ x\in G\} \)

shows \( \forall x\in G.\ r(x) = s(x)\cdot c \), \( r \in AH \), \( s \cong r \)
lemma (in int0) Int_ZF_1_1_L2: shows \( \text{IsAring}(\mathbb{Z} ,IntegerAddition,IntegerMultiplication) \), \( IntegerMultiplication \text{ is commutative on } \mathbb{Z} \), \( ring0(\mathbb{Z} ,IntegerAddition,IntegerMultiplication) \)
lemma (in ring0) Ring_ZF_2_L2:

assumes \( a\in R \), \( b\in R \), \( c\in R \), \( d\in R \)

shows \( a - (b + 1 )\cdot c = (a - d - c) + (d - b\cdot c) \), \( a + b + (c + d) = a + b + c + d \), \( a + b + (c + d) = a + (b + c) + d \)
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_L6:

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

shows \( a - (b - 1 )\cdot c = (d - b\cdot c) - (d - a - c) \)
lemma (in int1) Int_ZF_2_2_L1:

assumes \( f:\mathbb{Z} \rightarrow \mathbb{Z} \) and \( p\in \mathbb{Z} \), \( q\in \mathbb{Z} \)

shows \( abs(f((p + 1 )\cdot q) - (p + 1 )\cdot f(q)) \leq abs(\delta (f,p\cdot q,q)) + abs(f(p\cdot q) - p\cdot f(q)) \), \( abs(f((p - 1 )\cdot q) - (p - 1 )\cdot f(q)) \leq abs(\delta (f,(p - 1 )\cdot q,q)) + abs(f(p\cdot q) - p\cdot f(q)) \)
lemma (in int0) Int_ZF_2_L15:

assumes \( b\leq b_1 \), \( c\leq c_1 \) and \( a\leq b + c \)

shows \( a\leq b_1 + c_1 \)
lemma (in int0) Int_ZF_1_2_L2:

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

shows \( a + (abs(b) + 1 )\cdot a = (abs(b + 1 ) + 1 )\cdot a \)
lemma (in int0) Int_ZF_1_2_L5:

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

shows \( a + (abs(b) + 1 )\cdot a = (abs(b - 1 ) + 1 )\cdot a \)
lemma (in int0) Int_ZF_2_L18: shows \( abs( 0 ) = 0 \)
lemma (in int1) Int_ZF_2_2_L2:

assumes \( f\in \mathcal{S} \) and \( 0 \leq p \), \( q\in \mathbb{Z} \) and \( abs(f(p\cdot q) - p\cdot f(q)) \leq (abs(p) + 1 )\cdot \text{ max}\delta (f) \)

shows \( abs(f((p + 1 )\cdot q) - (p + 1 )\cdot f(q)) \leq (abs(p + 1 ) + 1 )\cdot \text{ max}\delta (f) \)
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_2_L19A:

assumes \( m\in \mathbb{Z} \) and \( \neg ( 0 \leq m) \)

shows \( m\leq 0 \), \( 0 \leq ( - m) \), \( m\neq 0 \)
lemma (in int1) Int_ZF_2_2_L3:

assumes \( f\in \mathcal{S} \) and \( p\leq 0 \), \( q\in \mathbb{Z} \) and \( abs(f(p\cdot q) - p\cdot f(q)) \leq (abs(p) + 1 )\cdot \text{ max}\delta (f) \)

shows \( abs(f((p - 1 )\cdot q) - (p - 1 )\cdot f(q)) \leq (abs(p - 1 ) + 1 )\cdot \text{ max}\delta (f) \)
theorem (in int0) Back_induct_on_int:

assumes \( k\leq i \) and \( P(i) \) and \( \forall n.\ n\leq i \wedge P(n) \longrightarrow P(n - 1 ) \)

shows \( P(k) \)
lemma (in int1) Int_ZF_2_2_L4:

assumes \( f\in \mathcal{S} \) and \( p\in \mathbb{Z} \), \( q\in \mathbb{Z} \)

shows \( abs(f(p\cdot q) - p\cdot f(q)) \leq (abs(p) + 1 )\cdot \text{ max}\delta (f) \)
lemma (in int0) Int_ZF_2_L20:

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

shows \( abs(m - n) = abs(n - m) \)
lemma (in int0) Int_ZF_2_L21:

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

shows \( abs(m + n) \leq k + l \), \( abs(m - n) \leq k + l \)
lemma (in int0) Int_ZF_1_2_L10:

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

shows \( (a + 1 )\cdot b + (c + 1 )\cdot b = (c + a + 2 )\cdot b \)
lemma (in int1) Arthan_Lem_7:

assumes \( f\in \mathcal{S} \) and \( p\in \mathbb{Z} \), \( q\in \mathbb{Z} \)

shows \( abs(q\cdot f(p) - p\cdot f(q)) \leq (abs(p) + abs(q) + 2 )\cdot \text{ max}\delta (f) \)
lemma (in int0) Int_ZF_2_L16A: shows \( 0 \leq 1 \) and \( abs(1 ) = 1 \)
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 int0) Int_ZF_1_3_L14:

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

shows \( abs(a\cdot b) + (abs(a) + c)\cdot d = (d + abs(b))\cdot abs(a) + c\cdot d \)
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_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 int0) Int_ZF_1_2_L10A:

assumes \( a\in \mathbb{Z} \), \( b\in \mathbb{Z} \), \( c\in \mathbb{Z} \), \( e\in \mathbb{Z} \) and \( abs(a\cdot b - c) \leq d \), \( abs(b\cdot a - e) \leq f \)

shows \( abs(c - e) \leq f + d \)
lemma (in int0) Int_ZF_1_2_L12:

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

shows \( (b - c)\cdot a = a\cdot b - a\cdot c \)
lemma (in int0) Int_ZF_2_L15C:

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

shows \( m + k + n \leq m + L + n \)
lemma (in int0) Int_ZF_1_3_L13:

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 int0) Int_ZF_1_2_L13:

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

shows \( (x + (a\cdot x + b) + c)\cdot d = d\cdot (a + 1 )\cdot x + (b\cdot d + c\cdot d) \)
lemma (in int0) Int_ZF_1_2_L14:

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

shows \( (a\cdot x + b) + (c\cdot x + d) = (a + c)\cdot x + (b + d) \)
lemma (in int0) Int_ZF_1_3_L5:

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

shows \( abs(a\cdot b) = abs(a)\cdot abs(b) \)
lemma (in int0) Int_ZF_1_7_L1:

assumes \( \forall q\in \mathbb{Z} .\ F(q) \in \mathbb{Z} \) and \( \forall q\in \mathbb{Z} .\ F(q)\cdot abs(q) \leq A\cdot abs(q) + B \) and \( A\in \mathbb{Z} \), \( B\in \mathbb{Z} \)

shows \( \exists L.\ \forall p\in \mathbb{Z} .\ F(p) \leq L \)
lemma (in int1) Int_ZF_2_1_L11:

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

shows \( s\circ r \in \mathcal{S} \)