IsarMathLib

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

theory Int_ZF_IML imports OrderedGroup_ZF_1 Finite_ZF_1 ZF.Int Nat_ZF_IML
begin

This theory file is an interface between the old-style Isabelle (ZF logic) material on integers and the IsarMathLib project. Here we redefine the meta-level operations on integers (addition and multiplication) to convert them to ZF-functions and show that integers form a commutative group with respect to addition and commutative monoid with respect to multiplication. Similarly, we redefine the order on integers as a relation, that is a subset of \(Z\times Z\). We show that a subset of intergers is bounded iff it is finite. As we are forced to use standard Isabelle notation with all these dollar signs, sharps etc. to denote "type coercions" (?) the notation is often ugly and difficult to read.

Addition and multiplication as ZF-functions.

In this section we provide definitions of addition and multiplication as subsets of \((Z\times Z)\times Z\). We use the (higher order) relation defined in the standard Int theory to define a subset of \(Z\times Z\) that constitutes the ZF order relation corresponding to it. We define the set of positive integers using the notion of positive set from the OrderedGroup_ZF theory.

Definition of addition of integers as a binary operation on int. Recall that in standard Isabelle/ZF int is the set of integers and the sum of integers is denoted by prependig \(+\) with a dollar sign.

definition

\( IntegerAddition \equiv \{ \langle x,c\rangle \in (int\times int)\times int.\ \text{fst}(x) \ \$ + \text{snd}(x) = c\} \)

Definition of multiplication of integers as a binary operation on int. In standard Isabelle/ZF product of integers is denoted by prepending the dollar sign to \( * \).

definition

\( IntegerMultiplication \equiv \) \( \{ \langle x,c\rangle \in (int\times int)\times int.\ \text{fst}(x) \ \$ * \text{snd}(x) = c\} \)

Definition of natural order on integers as a relation on int. In the standard Isabelle/ZF the inequality relation on integers is denoted \( \leq \) prepended with the dollar sign.

definition

\( IntegerOrder \equiv \{p \in int\times int.\ \text{fst}(p) \ \$ \leq \text{snd}(p)\} \)

This defines the set of positive integers.

definition

\( PositiveIntegers \equiv \text{PositiveSet}(int,IntegerAddition,IntegerOrder) \)

IntegerAddition and IntegerMultiplication are functions on \( int \times int \).

lemma Int_ZF_1_L1:

shows \( IntegerAddition : int\times int \rightarrow int \), \( IntegerMultiplication : int\times int \rightarrow int \)proof
have \( \{\langle x,c\rangle \in (int\times int)\times int.\ \text{fst}(x) \ \$ + \text{snd}(x) = c\} \in int\times int\rightarrow int \), \( \{\langle x,c\rangle \in (int\times int)\times int.\ \text{fst}(x) \ \$ * \text{snd}(x) = c\} \in int\times int\rightarrow int \) using func1_1_L11A
then show \( IntegerAddition : int\times int \rightarrow int \), \( IntegerMultiplication : int\times int \rightarrow int \) using IntegerAddition_def, IntegerMultiplication_def
qed

The next context (locale) defines notation used for integers. We define \( 0 \) to denote the neutral element of addition, \( 1 \) as the unit of the multiplicative monoid. We introduce notation \( m\leq n \) for integers and write m..n to denote the integer interval with endpoints in \(m\) and \(n\). \( abs(m) \) means the absolute value of \(m\). This is a function defined in OrderedGroup that assigns \(x\) to itself if \(x\) is positive and assigns the opposite of \(x\) if \(x\leq 0\). Unforunately we cannot use the \(|\cdot|\) notation as in the OrderedGroup theory as this notation has been hogged by the standard Isabelle's Int theory. The notation \( -A \) where \(A\) is a subset of integers means the set \(\{-m: m\in A\}\). The symbol \( maxf(f,M) \) denotes tha maximum of function \(f\) over the set \(A\). We also introduce a similar notation for the minimum.

locale int0

defines \( \mathbb{Z} \equiv int \)

defines \( a + b \equiv IntegerAddition\langle a,b\rangle \)

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

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

defines \( a\cdot b \equiv IntegerMultiplication\langle a,b\rangle \)

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

defines \( 0 \equiv \text{ TheNeutralElement}(\mathbb{Z} ,IntegerAddition) \)

defines \( 1 \equiv \text{ TheNeutralElement}(\mathbb{Z} ,IntegerMultiplication) \)

defines \( 2 \equiv 1 + 1 \)

defines \( 3 \equiv 2 + 1 \)

defines \( \mathbb{Z} ^+ \equiv \text{Nonnegative}(\mathbb{Z} ,IntegerAddition,IntegerOrder) \)

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

defines \( abs(m) \equiv \text{AbsoluteValue}(\mathbb{Z} ,IntegerAddition,IntegerOrder)(m) \)

defines \( m \leq n \equiv \langle m,n\rangle \in IntegerOrder \)

defines \( m.\ .\ n \equiv \text{Interval}(IntegerOrder,m,n) \)

defines \( maxf(f,A) \equiv \text{Maximum}(IntegerOrder,f(A)) \)

defines \( minf(f,A) \equiv \text{Minimum}(IntegerOrder,f(A)) \)

IntegerAddition adds integers and IntegerMultiplication multiplies integers. This states that the ZF functions IntegerAddition and IntegerMultiplication give the same results as the higher-order equivalents defined in the standard Int theory.

lemma (in int0) Int_ZF_1_L2:

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

shows \( a + b = a \ \$ + b \), \( a\cdot b = a \ \$ * b \)proof
let \( x = \langle a,b\rangle \)
let \( c = a \ \$ + b \)
let \( d = a \ \$ * b \)
from A1 have \( \langle x,c\rangle \in \{\langle x,c\rangle \in (\mathbb{Z} \times \mathbb{Z} )\times \mathbb{Z} .\ \text{fst}(x) \ \$ + \text{snd}(x) = c\} \), \( \langle x,d\rangle \in \{\langle x,d\rangle \in (\mathbb{Z} \times \mathbb{Z} )\times \mathbb{Z} .\ \text{fst}(x) \ \$ * \text{snd}(x) = d\} \)
then show \( a + b = a \ \$ + b \), \( a\cdot b = a \ \$ * b \) using IntegerAddition_def, IntegerMultiplication_def, Int_ZF_1_L1, apply_iff
qed

Integer addition and multiplication are associative.

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) \) using assms, Int_ZF_1_L2, zadd_assoc, zmult_assoc

Integer addition and multiplication are commutative.

lemma (in int0) Int_ZF_1_L4:

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

shows \( x + y = y + x \), \( x\cdot y = y\cdot x \) using assms, Int_ZF_1_L2, zadd_commute, zmult_commute

Zero is neutral for addition and one for multiplication.

lemma (in int0) Int_ZF_1_L5:

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

shows \( (\ \$ # 0) + x = x \wedge x + (\ \$ # 0) = x \), \( (\ \$ # 1)\cdot x = x \wedge x\cdot (\ \$ # 1) = x \)proof
from A1 show \( (\ \$ # 0) + x = x \wedge x + (\ \$ # 0) = x \) using Int_ZF_1_L2, zadd_int0, Int_ZF_1_L4
from A1 have \( (\ \$ # 1)\cdot x = x \) using Int_ZF_1_L2, zmult_int1
with A1 show \( (\ \$ # 1)\cdot x = x \wedge x\cdot (\ \$ # 1) = x \) using Int_ZF_1_L4
qed

Zero is neutral for addition and one for multiplication.

lemma (in int0) Int_ZF_1_L6:

shows \( (\ \$ # 0)\in \mathbb{Z} \wedge \) \( (\forall x\in \mathbb{Z} .\ (\ \$ # 0) + x = x \wedge x + (\ \$ # 0) = x) \), \( (\ \$ # 1)\in \mathbb{Z} \wedge \) \( (\forall x\in \mathbb{Z} .\ (\ \$ # 1)\cdot x = x \wedge x\cdot (\ \$ # 1) = x) \) using Int_ZF_1_L5

Integers with addition and integers with multiplication form monoids.

theorem (in int0) Int_ZF_1_T1:

shows \( \text{IsAmonoid}(\mathbb{Z} ,IntegerAddition) \), \( \text{IsAmonoid}(\mathbb{Z} ,IntegerMultiplication) \)proof
have \( \exists e\in \mathbb{Z} .\ \forall x\in \mathbb{Z} .\ e + x = x \wedge x + e = x \), \( \exists e\in \mathbb{Z} .\ \forall x\in \mathbb{Z} .\ e\cdot x = x \wedge x\cdot e = x \) using Int_ZF_1_L6
then show \( \text{IsAmonoid}(\mathbb{Z} ,IntegerAddition) \), \( \text{IsAmonoid}(\mathbb{Z} ,IntegerMultiplication) \) using IsAmonoid_def, IsAssociative_def, Int_ZF_1_L1, Int_ZF_1_L3
qed

Zero is the neutral element of the integers with addition and one is the neutral element of the integers with multiplication.

lemma (in int0) Int_ZF_1_L8:

shows \( (\ \$ # 0) = 0 \), \( (\ \$ # 1) = 1 \)proof
have \( monoid0(\mathbb{Z} ,IntegerAddition) \) using Int_ZF_1_T1, monoid0_def
moreover
have \( (\ \$ # 0)\in \mathbb{Z} \wedge \) \( (\forall x\in \mathbb{Z} .\ IntegerAddition\langle \ \$ # 0,x\rangle = x \wedge \) \( IntegerAddition\langle x ,\ \$ # 0\rangle = x) \) using Int_ZF_1_L6
ultimately have \( (\ \$ # 0) = \text{ TheNeutralElement}(\mathbb{Z} ,IntegerAddition) \) by (rule group0_1_L4 )
then show \( (\ \$ # 0) = 0 \)
have \( monoid0(int,IntegerMultiplication) \) using Int_ZF_1_T1, monoid0_def
moreover
have \( (\ \$ # 1) \in int \wedge \) \( (\forall x\in int.\ IntegerMultiplication\langle \ \$ # 1, x\rangle = x \wedge \) \( IntegerMultiplication\langle x ,\ \$ # 1\rangle = x) \) using Int_ZF_1_L6
ultimately have \( (\ \$ # 1) = \text{ TheNeutralElement}(int,IntegerMultiplication) \) by (rule group0_1_L4 )
then show \( (\ \$ # 1) = 1 \)
qed

\(0\) and \(1\), as defined in int0 context, are integers.

lemma (in int0) Int_ZF_1_L8A:

shows \( 0 \in \mathbb{Z} \), \( 1 \in \mathbb{Z} \)proof
have \( (\ \$ # 0) \in \mathbb{Z} \), \( (\ \$ # 1) \in \mathbb{Z} \)
then show \( 0 \in \mathbb{Z} \), \( 1 \in \mathbb{Z} \) using Int_ZF_1_L8
qed

Zero is not one.

lemma (in int0) int_zero_not_one:

shows \( 0 \neq 1 \)proof
have \( (\ \$ # 0) \neq (\ \$ # 1) \)
then show \( 0 \neq 1 \) using Int_ZF_1_L8
qed

The set of integers is not empty, of course.

lemma (in int0) int_not_empty:

shows \( \mathbb{Z} \neq 0 \) using Int_ZF_1_L8A

The set of integers has more than just zero in it.

lemma (in int0) int_not_trivial:

shows \( \mathbb{Z} \neq \{ 0 \} \) using Int_ZF_1_L8A, int_zero_not_one

Each integer has an inverse (in the addition sense).

lemma (in int0) Int_ZF_1_L9:

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

shows \( \exists b\in \mathbb{Z} .\ g + b = 0 \)proof
from A1 have \( g + \ \$ -g = 0 \) using Int_ZF_1_L2, Int_ZF_1_L8
thus \( thesis \)
qed

Integers with addition form an abelian group. This also shows that we can apply all theorems proven in the proof contexts (locales) that require the assumpion that some pair of sets form a group like locale group0.

theorem Int_ZF_1_T2:

shows \( \text{IsAgroup}(int,IntegerAddition) \), \( IntegerAddition \text{ is commutative on } int \), \( group0(int,IntegerAddition) \) using Int_ZF_1_T1, Int_ZF_1_L9, IsAgroup_def, group0_def, Int_ZF_1_L4, IsCommutative_def

What is the additive group inverse in the group of integers?

lemma (in int0) Int_ZF_1_L9A:

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

shows \( \ \$ -m = - m \)proof
from A1 have \( m\in int \), \( \ \$ -m \in int \), \( IntegerAddition\langle m,\ \$ -m\rangle = \) \( \text{ TheNeutralElement}(int,IntegerAddition) \) using zminus_type, Int_ZF_1_L2, Int_ZF_1_L8
then have \( \ \$ -m = \text{GroupInv}(int,IntegerAddition)(m) \) using Int_ZF_1_T2, group0_2_L9
then show \( thesis \)
qed

Subtracting integers corresponds to adding the negative.

lemma (in int0) Int_ZF_1_L10:

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

shows \( m - n = m \ \$ + \ \$ -n \) using assms, Int_ZF_1_T2, inverse_in_group, Int_ZF_1_L9A, Int_ZF_1_L2

Negative of zero is zero.

lemma (in int0) Int_ZF_1_L11:

shows \( ( - 0 ) = 0 \) using Int_ZF_1_T2, group_inv_of_one

A trivial calculation lemma that allows to subtract and add one.

lemma Int_ZF_1_L12:

assumes \( m\in int \)

shows \( m \ \$ - \ \$ #1 \ \$ + \ \$ #1 = m \) using assms, eq_zdiff_iff

A trivial calculation lemma that allows to subtract and add one, version with ZF-operation.

lemma (in int0) Int_ZF_1_L13:

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

shows \( (m \ \$ - \ \$ #1) + 1 = m \) using assms, Int_ZF_1_L8A, Int_ZF_1_L2, Int_ZF_1_L8, Int_ZF_1_L12

Adding or subtracing one changes integers.

lemma (in int0) Int_ZF_1_L14:

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

shows \( m + 1 \neq m \), \( m - 1 \neq m \)proof
{
assume \( m + 1 = m \)
with A1 have \( group0(\mathbb{Z} ,IntegerAddition) \), \( m\in \mathbb{Z} \), \( 1 \in \mathbb{Z} \), \( IntegerAddition\langle m,1 \rangle = m \) using Int_ZF_1_T2, Int_ZF_1_L8A
then have \( 1 = \text{ TheNeutralElement}(\mathbb{Z} ,IntegerAddition) \) by (rule group0_2_L7 )
then have \( False \) using int_zero_not_one
}
then show I: \( m + 1 \neq m \)
{
from A1 have \( m - 1 + 1 = m \) using Int_ZF_1_L8A, Int_ZF_1_T2, inv_cancel_two
moreover
assume \( m - 1 = m \)
ultimately have \( m + 1 = m \)
with I have \( False \)
}
then show \( m - 1 \neq m \)
qed

If the difference is zero, the integers are equal.

lemma (in int0) Int_ZF_1_L15:

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

shows \( m=n \)proof
let \( G = \mathbb{Z} \)
let \( f = IntegerAddition \)
from A1, A2 have \( group0(G, f) \), \( m \in G \), \( n \in G \), \( f\langle m, \text{GroupInv}(G, f)(n)\rangle = \text{ TheNeutralElement}(G, f) \) using Int_ZF_1_T2
then show \( m=n \) by (rule group0_2_L11A )
qed

Integers as an ordered group

In this section we define order on integers as a relation, that is a subset of \(Z\times Z\) and show that integers form an ordered group.

The next lemma interprets the order definition one way.

lemma (in int0) Int_ZF_2_L1:

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

shows \( m \leq n \)proof
from A1, A2 have \( \langle m,n\rangle \in \{x\in \mathbb{Z} \times \mathbb{Z} .\ \text{fst}(x) \ \$ \leq \text{snd}(x)\} \)
then show \( thesis \) using IntegerOrder_def
qed

The next lemma interprets the definition the other way.

lemma (in int0) Int_ZF_2_L1A:

assumes A1: \( m \leq n \)

shows \( m \ \$ \leq n \), \( m\in \mathbb{Z} \), \( n\in \mathbb{Z} \)proof
from A1 have \( \langle m,n\rangle \in \{p\in \mathbb{Z} \times \mathbb{Z} .\ \text{fst}(p) \ \$ \leq \text{snd}(p)\} \) using IntegerOrder_def
thus \( m \ \$ \leq n \), \( m\in \mathbb{Z} \), \( n\in \mathbb{Z} \)
qed

Integer order is a relation on integers.

lemma Int_ZF_2_L1B:

shows \( IntegerOrder \subseteq int\times int \)proof
fix \( x \)
assume \( x\in IntegerOrder \)
then have \( x \in \{p\in int\times int.\ \text{fst}(p) \ \$ \leq \text{snd}(p)\} \) using IntegerOrder_def
then show \( x\in int\times int \)
qed

The way we define the notion of being bounded below, its sufficient for the relation to be on integers for all bounded below sets to be subsets of integers.

lemma (in int0) Int_ZF_2_L1C:

assumes A1: \( \text{IsBoundedBelow}(A,IntegerOrder) \)

shows \( A\subseteq \mathbb{Z} \)proof
from A1 have \( IntegerOrder \subseteq \mathbb{Z} \times \mathbb{Z} \), \( \text{IsBoundedBelow}(A,IntegerOrder) \) using Int_ZF_2_L1B
then show \( A\subseteq \mathbb{Z} \) by (rule Order_ZF_3_L1B )
qed

The order on integers is reflexive.

lemma (in int0) int_ord_is_refl:

shows \( \text{refl}(\mathbb{Z} ,IntegerOrder) \) using Int_ZF_2_L1, zle_refl, refl_def

The essential condition to show antisymmetry of the order on integers.

lemma (in int0) Int_ZF_2_L3:

assumes A1: \( m \leq n \), \( n \leq m \)

shows \( m=n \)proof
from A1 have \( m \ \$ \leq n \), \( n \ \$ \leq m \), \( m\in \mathbb{Z} \), \( n\in \mathbb{Z} \) using Int_ZF_2_L1A
then show \( m=n \) using zle_anti_sym
qed

The order on integers is antisymmetric.

lemma (in int0) Int_ZF_2_L4:

shows \( \text{antisym}(IntegerOrder) \)proof
have \( \forall m n.\ m \leq n \wedge n \leq m \longrightarrow m=n \) using Int_ZF_2_L3
then show \( thesis \) using imp_conj, antisym_def
qed

The essential condition to show that the order on integers is transitive.

lemma Int_ZF_2_L5:

assumes A1: \( \langle m,n\rangle \in IntegerOrder \), \( \langle n,k\rangle \in IntegerOrder \)

shows \( \langle m,k\rangle \in IntegerOrder \)proof
from A1 have T1: \( m \ \$ \leq n \), \( n \ \$ \leq k \) and T2: \( m\in int \), \( k\in int \) using Int_ZF_2_L1A
from T1 have \( m \ \$ \leq k \) by (rule zle_trans )
with T2 show \( thesis \) using Int_ZF_2_L1
qed

The order on integers is transitive. This version is stated in the int0 context using notation for integers.

lemma (in int0) Int_order_transitive:

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

shows \( m\leq k \)proof
from A1 have \( \langle m,n\rangle \in IntegerOrder \), \( \langle n,k\rangle \in IntegerOrder \)
then have \( \langle m,k\rangle \in IntegerOrder \) by (rule Int_ZF_2_L5 )
then show \( m\leq k \)
qed

The order on integers is transitive.

lemma Int_ZF_2_L6:

shows \( \text{trans}(IntegerOrder) \)proof
have \( \forall m n k.\ \) \( \langle m, n\rangle \in IntegerOrder \wedge \langle n, k\rangle \in IntegerOrder \longrightarrow \) \( \langle m, k\rangle \in IntegerOrder \) using Int_ZF_2_L5
then show \( thesis \) by (rule Fol1_L2 )
qed

The order on integers is a partial order.

lemma Int_ZF_2_L7:

shows \( \text{IsPartOrder}(int,IntegerOrder) \) using int_ord_is_refl, Int_ZF_2_L4, Int_ZF_2_L6, IsPartOrder_def

The essential condition to show that the order on integers is preserved by translations.

lemma (in int0) int_ord_transl_inv:

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

shows \( m + k \leq n + k \), \( k + m\leq k + n \)proof
from A2 have \( m \ \$ \leq n \) and \( m\in \mathbb{Z} \), \( n\in \mathbb{Z} \) using Int_ZF_2_L1A
with A1 show \( m + k \leq n + k \), \( k + m\leq k + n \) using zadd_right_cancel_zle, zadd_left_cancel_zle, Int_ZF_1_L2, Int_ZF_1_L1, apply_funtype, Int_ZF_1_L2, Int_ZF_2_L1, Int_ZF_1_L2
qed

Integers form a linearly ordered group. We can apply all theorems proven in group3 context to integers.

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) \)proof
have \( \forall k\in \mathbb{Z} .\ \forall m n.\ m \leq n \longrightarrow \) \( m + k \leq n + k \wedge k + m\leq k + n \) using int_ord_transl_inv
then show T1: \( \text{IsAnOrdGroup}(\mathbb{Z} ,IntegerAddition,IntegerOrder) \) using Int_ZF_1_T2, Int_ZF_2_L1B, Int_ZF_2_L7, IsAnOrdGroup_def
then show \( group3(\mathbb{Z} ,IntegerAddition,IntegerOrder) \) using group3_def
have \( \forall n\in \mathbb{Z} .\ \forall m\in \mathbb{Z} .\ n\leq m \vee m\leq n \) using zle_linear, Int_ZF_2_L1
then show \( IntegerOrder \text{ is total on } \mathbb{Z} \) using IsTotal_def
with T1 show \( \text{IsLinOrder}(\mathbb{Z} ,IntegerOrder) \) using IsAnOrdGroup_def, IsPartOrder_def, IsLinOrder_def
qed

If a pair \((i,m)\) belongs to the order relation on integers and \(i\neq m\), then \(i

lemma (in int0) Int_ZF_2_L9:

assumes A1: \( i \leq m \) and A2: \( i\neq m \)

shows \( i \ \$ \lt m \)proof
from A1 have \( i \ \$ \leq m \), \( i\in \mathbb{Z} \), \( m\in \mathbb{Z} \) using Int_ZF_2_L1A
with A2 show \( i \ \$ \lt m \) using zle_def
qed

This shows how Isabelle's \( \ \$ \lt \) operator translates to IsarMathLib notation.

lemma (in int0) Int_ZF_2_L9AA:

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

shows \( m\leq n \), \( m \neq n \) using assms, zle_def, Int_ZF_2_L1

A small technical lemma about putting one on the other side of an inequality.

lemma (in int0) Int_ZF_2_L9A:

assumes A1: \( k\in \mathbb{Z} \) and A2: \( m \leq k \ \$ - (\ \$ # 1) \)

shows \( m + 1 \leq k \)proof
from A2 have \( m + 1 \leq (k \ \$ - (\ \$ # 1)) + 1 \) using Int_ZF_1_L8A, int_ord_transl_inv
with A1 show \( m + 1 \leq k \) using Int_ZF_1_L13
qed

We can put any integer on the other side of an inequality reversing its sign.

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 \) using assms, Int_ZF_2_T1, OrderedGroup_ZF_1_L9A

A special case of Int_ZF_2_L9B with weaker assumptions.

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 \) using assms, Int_ZF_2_T1, OrderedGroup_ZF_1_L9B

Taking (higher order) minus on both sides of inequality reverses it.

lemma (in int0) Int_ZF_2_L10:

assumes \( k \leq i \)

shows \( ( - i) \leq ( - k) \), \( \ \$ -i \leq \ \$ -k \) using assms, Int_ZF_2_L1A, Int_ZF_1_L9A, Int_ZF_2_T1, OrderedGroup_ZF_1_L5

Taking minus on both sides of inequality reverses it, version with a negative on one side.

lemma (in int0) Int_ZF_2_L10AA:

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

shows \( n\leq ( - m) \) using assms, Int_ZF_2_T1, OrderedGroup_ZF_1_L5AD

We can cancel the same element on on both sides of an inequality, a version with minus on both sides.

lemma (in int0) Int_ZF_2_L10AB:

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

shows \( k\leq n \) using assms, Int_ZF_2_T1, OrderedGroup_ZF_1_L5AF

If an integer is nonpositive, then its opposite is nonnegative.

lemma (in int0) Int_ZF_2_L10A:

assumes \( k \leq 0 \)

shows \( 0 \leq ( - k) \) using assms, Int_ZF_2_T1, OrderedGroup_ZF_1_L5A

If the opposite of an integers is nonnegative, then the integer is nonpositive.

lemma (in int0) Int_ZF_2_L10B:

assumes \( k\in \mathbb{Z} \) and \( 0 \leq ( - k) \)

shows \( k\leq 0 \) using assms, Int_ZF_2_T1, OrderedGroup_ZF_1_L5AA

Adding one to an integer corresponds to taking a successor for a natural number.

lemma (in int0) Int_ZF_2_L11:

shows \( i \ \$ + \ \$ # n \ \$ + (\ \$ # 1) = i \ \$ + \ \$ # succ(n) \)proof
have \( \ \$ # succ(n) = \ \$ #1 \ \$ + \ \$ # n \) using int_succ_int_1
then have \( i \ \$ + \ \$ # succ(n) = i \ \$ + (\ \$ # n \ \$ + \ \$ #1) \) using zadd_commute
then show \( thesis \) using zadd_assoc
qed

Adding a natural number increases integers.

lemma (in int0) Int_ZF_2_L12:

assumes A1: \( i\in \mathbb{Z} \) and A2: \( n\in nat \)

shows \( i \leq i \ \$ + \ \$ #n \)proof
{
assume \( n = 0 \)
with A1 have \( i \leq i \ \$ + \ \$ #n \) using zadd_int0, int_ord_is_refl, refl_def
}
moreover {
assume \( n\neq 0 \)
with A2 obtain \( k \) where \( k\in nat \), \( n = succ(k) \) using Nat_ZF_1_L3
with A1 have \( i \leq i \ \$ + \ \$ #n \) using zless_succ_zadd, zless_imp_zle, Int_ZF_2_L1
} ultimately show \( thesis \)
qed

Adding one increases integers.

lemma (in int0) Int_ZF_2_L12A:

assumes A1: \( j\leq k \)

shows \( j \leq k \ \$ + \ \$ #1 \), \( j \leq k + 1 \)proof
from A1 have T1: \( j\in \mathbb{Z} \), \( k\in \mathbb{Z} \), \( j \ \$ \leq k \) using Int_ZF_2_L1A
moreover
from T1 have \( k \ \$ \leq k \ \$ + \ \$ #1 \) using Int_ZF_2_L12, Int_ZF_2_L1A
ultimately have \( j \ \$ \leq k \ \$ + \ \$ #1 \) using zle_trans
with T1 show \( j \leq k \ \$ + \ \$ #1 \) using Int_ZF_2_L1
with T1 have \( j\leq k + \ \$ #1 \) using Int_ZF_1_L2
then show \( j \leq k + 1 \) using Int_ZF_1_L8
qed

Adding one increases integers, yet one more version.

lemma (in int0) Int_ZF_2_L12B:

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

shows \( m \leq m + 1 \) using assms, int_ord_is_refl, refl_def, Int_ZF_2_L12A

If \(k+1 = m+n\), where \(n\) is a non-zero natural number, then \(m\leq k\).

lemma (in int0) Int_ZF_2_L13:

assumes A1: \( k\in \mathbb{Z} \), \( m\in \mathbb{Z} \) and A2: \( n\in nat \) and A3: \( k \ \$ + (\ \$ # 1) = m \ \$ + \ \$ # succ(n) \)

shows \( m \leq k \)proof
from A1 have \( k\in \mathbb{Z} \), \( m \ \$ + \ \$ # n \in \mathbb{Z} \)
moreover
from assms have \( k \ \$ + \ \$ # 1 = m \ \$ + \ \$ # n \ \$ + \ \$ #1 \) using Int_ZF_2_L11
ultimately have \( k = m \ \$ + \ \$ # n \) using zadd_right_cancel
with A1, A2 show \( thesis \) using Int_ZF_2_L12
qed

The absolute value of an integer is an integer.

lemma (in int0) Int_ZF_2_L14:

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

shows \( abs(m) \in \mathbb{Z} \)proof
have \( \text{AbsoluteValue}(\mathbb{Z} ,IntegerAddition,IntegerOrder) : \mathbb{Z} \rightarrow \mathbb{Z} \) using Int_ZF_2_T1, OrderedGroup_ZF_3_L1
with A1 show \( thesis \) using apply_funtype
qed

If two integers are nonnegative, then the opposite of one is less or equal than the other and the sum is also nonnegative.

lemma (in int0) Int_ZF_2_L14A:

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

shows \( ( - m) \leq n \), \( 0 \leq m + n \) using assms, Int_ZF_2_T1, OrderedGroup_ZF_1_L5AC, OrderedGroup_ZF_1_L12

We can increase components in an estimate.

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 \)proof
from assms have \( group3(\mathbb{Z} ,IntegerAddition,IntegerOrder) \), \( \langle a,IntegerAddition\langle b,c\rangle \rangle \in IntegerOrder \), \( \langle b,b_1\rangle \in IntegerOrder \), \( \langle c,c_1\rangle \in IntegerOrder \) using Int_ZF_2_T1
then have \( \langle a,IntegerAddition\langle b_1,c_1\rangle \rangle \in IntegerOrder \) by (rule OrderedGroup_ZF_1_L5E )
thus \( thesis \)
qed

We can add or subtract the sides of two inequalities.

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 \) using assms, Int_ZF_2_T1, OrderedGroup_ZF_1_L5B, OrderedGroup_ZF_1_L5I

We can increase the second component in an estimate.

lemma (in int0) Int_ZF_2_L15A:

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

shows \( a\leq b + c_1 \)proof
from assms have \( group3(\mathbb{Z} ,IntegerAddition,IntegerOrder) \), \( b \in \mathbb{Z} \), \( \langle a,IntegerAddition\langle b,c\rangle \rangle \in IntegerOrder \), \( \langle c,c_1\rangle \in IntegerOrder \) using Int_ZF_2_T1
then have \( \langle a,IntegerAddition\langle b,c_1\rangle \rangle \in IntegerOrder \) by (rule OrderedGroup_ZF_1_L5D )
thus \( thesis \)
qed

If we increase the second component in a sum of three integers, the whole sum inceases.

lemma (in int0) Int_ZF_2_L15C:

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

shows \( m + k + n \leq m + L + n \)proof
let \( P = IntegerAddition \)
from assms have \( group3(int,P,IntegerOrder) \), \( m \in int \), \( n \in int \), \( \langle k,L\rangle \in IntegerOrder \) using Int_ZF_2_T1
then have \( \langle P\langle P\langle m,k\rangle ,n\rangle , P\langle P\langle m,L\rangle ,n\rangle \rangle \in IntegerOrder \) by (rule OrderedGroup_ZF_1_L10 )
then show \( m + k + n \leq m + L + n \)
qed

We don't decrease an integer by adding a nonnegative one.

lemma (in int0) Int_ZF_2_L15D:

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

shows \( m \leq n + m \) using assms, Int_ZF_2_T1, OrderedGroup_ZF_1_L5F

Some inequalities about the sum of two integers and its absolute value.

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) \) using assms, Int_ZF_2_T1, OrderedGroup_ZF_3_L6A

We can add a nonnegative integer to the right hand side of an inequality.

lemma (in int0) Int_ZF_2_L15F:

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

shows \( m \leq k + n \), \( m \leq n + k \) using assms, Int_ZF_2_T1, OrderedGroup_ZF_1_L5G

Triangle inequality for integers.

lemma (in int0) Int_triangle_ineq:

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

shows \( abs(m + n)\leq abs(m) + abs(n) \) using assms, Int_ZF_1_T2, Int_ZF_2_T1, OrdGroup_triangle_ineq

Taking absolute value does not change nonnegative integers.

lemma (in int0) Int_ZF_2_L16:

assumes \( 0 \leq m \)

shows \( m\in \mathbb{Z} ^+ \) and \( abs(m) = m \) using assms, Int_ZF_2_T1, OrderedGroup_ZF_1_L2, OrderedGroup_ZF_3_L2

\(0\leq 1\), so \(|1| = 1\).

lemma (in int0) Int_ZF_2_L16A:

shows \( 0 \leq 1 \) and \( abs(1 ) = 1 \)proof
have \( (\ \$ # 0) \in \mathbb{Z} \), \( (\ \$ # 1)\in \mathbb{Z} \)
then have \( 0 \leq 0 \) and T1: \( 1 \in \mathbb{Z} \) using Int_ZF_1_L8, int_ord_is_refl, refl_def
then have \( 0 \leq 0 + 1 \) using Int_ZF_2_L12A
with T1 show \( 0 \leq 1 \) using Int_ZF_1_T2, group0_2_L2
then show \( abs(1 ) = 1 \) using Int_ZF_2_L16
qed

\(1\leq 2\).

lemma (in int0) Int_ZF_2_L16B:

shows \( 1 \leq 2 \)proof
have \( (\ \$ # 1)\in \mathbb{Z} \)
then show \( 1 \leq 2 \) using Int_ZF_1_L8, int_ord_is_refl, refl_def, Int_ZF_2_L12A
qed

Integers greater or equal one are greater or equal zero.

lemma (in int0) Int_ZF_2_L16C:

assumes A1: \( 1 \leq a \)

shows \( 0 \leq a \), \( a\neq 0 \), \( 2 \leq a + 1 \), \( 1 \leq a + 1 \), \( 0 \leq a + 1 \)proof
from A1 have \( 0 \leq 1 \) and \( 1 \leq a \) using Int_ZF_2_L16A
then show \( 0 \leq a \) by (rule Int_order_transitive )
have I: \( 0 \leq 1 \) using Int_ZF_2_L16A
have \( 1 \leq 2 \) using Int_ZF_2_L16B
moreover
from A1 show \( 2 \leq a + 1 \) using Int_ZF_1_L8A, int_ord_transl_inv
ultimately show \( 1 \leq a + 1 \) by (rule Int_order_transitive )
with I show \( 0 \leq a + 1 \) by (rule Int_order_transitive )
from A1 show \( a\neq 0 \) using Int_ZF_2_L16A, Int_ZF_2_L3, int_zero_not_one
qed

Absolute value is the same for an integer and its opposite.

lemma (in int0) Int_ZF_2_L17:

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

shows \( abs( - m) = abs(m) \) using assms, Int_ZF_2_T1, OrderedGroup_ZF_3_L7A

The absolute value of zero is zero.

lemma (in int0) Int_ZF_2_L18:

shows \( abs( 0 ) = 0 \) using Int_ZF_2_T1, OrderedGroup_ZF_3_L2A

A different version of the triangle inequality.

lemma (in int0) Int_triangle_ineq1:

assumes A1: \( 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) \)proof
have \( \ \$ -n \in \mathbb{Z} \)
with A1 have \( abs(m - n) \leq abs(m) + abs( - n) \) using Int_ZF_1_L9A, Int_triangle_ineq
with A1 show \( abs(m - n) \leq abs(n) + abs(m) \), \( abs(m - n) \leq abs(m) + abs(n) \) using Int_ZF_2_L17, Int_ZF_2_L14, Int_ZF_1_T2, IsCommutative_def
qed

Another version of the triangle inequality.

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 \) using assms, Int_ZF_1_T2, Int_ZF_2_T1, OrderedGroup_ZF_3_L7D, OrderedGroup_ZF_3_L7E

Triangle inequality with three integers. We could use OrdGroup_triangle_ineq3, but since simp cannot translate the notation directly, it is simpler to reprove it for integers.

lemma (in int0) Int_triangle_ineq3:

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

shows \( abs(m + n + k) \leq abs(m) + abs(n) + abs(k) \)proof
from A1 have T: \( m + n \in \mathbb{Z} \), \( abs(k) \in \mathbb{Z} \) using Int_ZF_1_T2, group_op_closed, Int_ZF_2_L14
with A1 have \( abs(m + n + k) \leq abs(m + n) + abs(k) \) using Int_triangle_ineq
moreover
from A1, T have \( abs(m + n) + abs(k) \leq abs(m) + abs(n) + abs(k) \) using Int_triangle_ineq, int_ord_transl_inv
ultimately show \( thesis \) by (rule Int_order_transitive )
qed

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

lemma (in int0) Int_ZF_2_L19:

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

shows \( m\leq n \), \( ( - n) \leq ( - m) \), \( m\neq n \)proof
from A1, A2 show \( m\leq n \) using Int_ZF_2_T1, IsTotal_def
then show \( ( - n) \leq ( - m) \) using Int_ZF_2_L10
from A1 have \( n \leq n \) using int_ord_is_refl, refl_def
with A2 show \( m\neq n \)
qed

If one integer is greater or equal and not equal to another, then it is not smaller or equal.

lemma (in int0) Int_ZF_2_L19AA:

assumes A1: \( m\leq n \) and A2: \( m\neq n \)

shows \( \neg (n\leq m) \)proof
from A1, A2 have \( group3(\mathbb{Z} , IntegerAddition, IntegerOrder) \), \( \langle m,n\rangle \in IntegerOrder \), \( m\neq n \) using Int_ZF_2_T1
then have \( \langle n,m\rangle \notin IntegerOrder \) by (rule OrderedGroup_ZF_1_L8AA )
thus \( \neg (n\leq m) \)
qed

The next lemma allows to prove theorems for the case of positive and negative integers separately.

lemma (in int0) Int_ZF_2_L19A:

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

shows \( m\leq 0 \), \( 0 \leq ( - m) \), \( m\neq 0 \)proof
from A1 have T: \( 0 \in \mathbb{Z} \) using Int_ZF_1_T2, group0_2_L2
with A1, A2 show \( m\leq 0 \) using Int_ZF_2_L19
from A1, T, A2 show \( m\neq 0 \) by (rule Int_ZF_2_L19 )
from A1, T, A2 have \( ( - 0 )\leq ( - m) \) by (rule Int_ZF_2_L19 )
then show \( 0 \leq ( - m) \) using Int_ZF_1_T2, group_inv_of_one
qed

We can prove a theorem about integers by proving that it holds for \(m=0\), \(m\in\)\( \mathbb{Z} _+ \) and \(-m\in\)\( \mathbb{Z} _+ \).

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) \)proof
let \( G = \mathbb{Z} \)
let \( P = IntegerAddition \)
let \( r = IntegerOrder \)
let \( b = m \)
from assms have \( group3(G, P, r) \), \( r \text{ is total on } G \), \( b \in G \), \( Q(\text{ TheNeutralElement}(G, P)) \), \( \forall a\in \text{PositiveSet}(G, P, r).\ Q(a) \), \( \forall a\in \text{PositiveSet}(G, P, r).\ Q( \text{GroupInv}(G, P)(a)) \) using Int_ZF_2_T1
then show \( Q(b) \) by (rule OrderedGroup_ZF_1_L18 )
qed

An integer is not greater than its absolute value.

lemma (in int0) Int_ZF_2_L19C:

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

shows \( m \leq abs(m) \), \( ( - m) \leq abs(m) \) using assms, Int_ZF_2_T1, OrderedGroup_ZF_3_L5, OrderedGroup_ZF_3_L6

\(|m-n| = |n-m|\).

lemma (in int0) Int_ZF_2_L20:

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

shows \( abs(m - n) = abs(n - m) \) using assms, Int_ZF_2_T1, OrderedGroup_ZF_3_L7B

We can add the sides of inequalities with absolute values.

lemma (in int0) Int_ZF_2_L21:

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

shows \( abs(m + n) \leq k + l \), \( abs(m - n) \leq k + l \) using assms, Int_ZF_1_T2, Int_ZF_2_T1, OrderedGroup_ZF_3_L7C, OrderedGroup_ZF_3_L7CA

Absolute value is nonnegative.

lemma (in int0) int_abs_nonneg:

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

shows \( abs(m) \in \mathbb{Z} ^+ \), \( 0 \leq abs(m) \)proof
have \( \text{AbsoluteValue}(\mathbb{Z} ,IntegerAddition,IntegerOrder) : \mathbb{Z} \rightarrow \mathbb{Z} ^+ \) using Int_ZF_2_T1, OrderedGroup_ZF_3_L3C
with A1 show \( abs(m) \in \mathbb{Z} ^+ \) using apply_funtype
then show \( 0 \leq abs(m) \) using Int_ZF_2_T1, OrderedGroup_ZF_1_L2
qed

If an nonnegative integer is less or equal than another, then so is its absolute value.

lemma (in int0) Int_ZF_2_L23:

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

shows \( abs(m) \leq k \) using assms, Int_ZF_2_L16

Induction on integers.

In this section we show some induction lemmas for integers. The basic tools are the induction on natural numbers and the fact that integers can be written as a sum of a smaller integer and a natural number.

An integer can be written a a sum of a smaller integer and a natural number.

lemma (in int0) Int_ZF_3_L2:

assumes A1: \( i \leq m \)

shows \( \exists n\in nat.\ m = i \ \$ + \ \$ # n \)proof
let \( n = 0 \)
{
assume A2: \( i=m \)
from A1, A2 have \( n \in nat \), \( m = i \ \$ + \ \$ # n \) using Int_ZF_2_L1A, zadd_int0_right
hence \( \exists n\in nat.\ m = i \ \$ + \ \$ # n \)
}
moreover {
assume A3: \( i\neq m \)
with A1 have \( i \ \$ \lt m \), \( i\in \mathbb{Z} \), \( m\in \mathbb{Z} \) using Int_ZF_2_L9, Int_ZF_2_L1A
then obtain \( k \) where D1: \( k\in nat \), \( m = i \ \$ + \ \$ # succ(k) \) using zless_imp_succ_zadd_lemma
let \( n = succ(k) \)
from D1 have \( n\in nat \), \( m = i \ \$ + \ \$ # n \)
hence \( \exists n\in nat.\ m = i \ \$ + \ \$ # n \)
} ultimately show \( thesis \)
qed

Induction for integers, the induction step.

lemma (in int0) Int_ZF_3_L6:

assumes A1: \( i\in \mathbb{Z} \) and A2: \( \forall m.\ i\leq m \wedge Q(m) \longrightarrow Q(m \ \$ + (\ \$ # 1)) \)

shows \( \forall k\in nat.\ Q(i \ \$ + (\ \$ # k)) \longrightarrow Q(i \ \$ + (\ \$ # succ(k))) \)proof
fix \( k \)
assume A3: \( k\in nat \)
show \( Q(i \ \$ + \ \$ # k) \longrightarrow Q(i \ \$ + \ \$ # succ(k)) \)proof
assume A4: \( Q(i \ \$ + \ \$ # k) \)
from A1, A3 have \( i\leq i \ \$ + (\ \$ # k) \) using Int_ZF_2_L12
with A4, A2 have \( Q(i \ \$ + (\ \$ # k) \ \$ + (\ \$ # 1)) \)
then show \( Q(i \ \$ + (\ \$ # succ(k))) \) using Int_ZF_2_L11
qed
qed

Induction on integers, version with higher-order increment function.

lemma (in int0) Int_ZF_3_L7:

assumes A1: \( i\leq k \) and A2: \( Q(i) \) and A3: \( \forall m.\ i\leq m \wedge Q(m) \longrightarrow Q(m \ \$ + (\ \$ # 1)) \)

shows \( Q(k) \)proof
from A1 obtain \( n \) where D1: \( n\in nat \) and D2: \( k = i \ \$ + \ \$ # n \) using Int_ZF_3_L2
from A1 have T1: \( i\in \mathbb{Z} \) using Int_ZF_2_L1A
note \( n\in nat \)
moreover
from A1, A2 have \( Q(i \ \$ + \ \$ #0) \) using Int_ZF_2_L1A, zadd_int0
moreover
from T1, A3 have \( \forall k\in nat.\ Q(i \ \$ + (\ \$ # k)) \longrightarrow Q(i \ \$ + (\ \$ # succ(k))) \) by (rule Int_ZF_3_L6 )
ultimately have \( Q(i \ \$ + (\ \$ # n)) \) by (rule ind_on_nat )
with D2 show \( Q(k) \)
qed

Induction on integer, implication between two forms of the induction step.

lemma (in int0) Int_ZF_3_L7A:

assumes A1: \( \forall m.\ i\leq m \wedge Q(m) \longrightarrow Q(m + 1 ) \)

shows \( \forall m.\ i\leq m \wedge Q(m) \longrightarrow Q(m \ \$ + (\ \$ # 1)) \)proof
{
fix \( m \)
assume \( i\leq m \wedge Q(m) \)
with A1 have T1: \( m\in \mathbb{Z} \), \( Q(m + 1 ) \) using Int_ZF_2_L1A
then have \( m + 1 = m + (\ \$ # 1) \) using Int_ZF_1_L8
with T1 have \( Q(m \ \$ + (\ \$ # 1)) \) using Int_ZF_1_L2
}
then show \( thesis \)
qed

Induction on integers, version with ZF increment function.

theorem (in int0) Induction_on_int:

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

shows \( Q(k) \)proof
from A3 have \( \forall m.\ i\leq m \wedge Q(m) \longrightarrow Q(m \ \$ + (\ \$ # 1)) \) by (rule Int_ZF_3_L7A )
with A1, A2 show \( thesis \) by (rule Int_ZF_3_L7 )
qed

Another form of induction on integers. This rewrites the basic theorem Int_ZF_3_L7 substituting \(P(-k)\) for \(Q(k)\).

lemma (in int0) Int_ZF_3_L7B:

assumes A1: \( i\leq k \) and A2: \( P(\ \$ -i) \) and A3: \( \forall m.\ i\leq m \wedge P(\ \$ -m) \longrightarrow P(\ \$ -(m \ \$ + (\ \$ # 1))) \)

shows \( P(\ \$ -k) \)proof
from A1, A2, A3 show \( P(\ \$ -k) \) by (rule Int_ZF_3_L7 )
qed

Another induction on integers. This rewrites Int\_ZF\_3\_L7 substituting \(-k\) for \(k\) and \(-i\) for \(i\).

lemma (in int0) Int_ZF_3_L8:

assumes A1: \( k\leq i \) and A2: \( P(i) \) and A3: \( \forall m.\ \ \$ -i\leq m \wedge P(\ \$ -m) \longrightarrow P(\ \$ -(m \ \$ + (\ \$ # 1))) \)

shows \( P(k) \)proof
from A1 have T1: \( \ \$ -i\leq \ \$ -k \) using Int_ZF_2_L10
from A1, A2 have T2: \( P(\ \$ - \ \$ - i) \) using Int_ZF_2_L1A, zminus_zminus
from T1, T2, A3 have \( P(\ \$ -(\ \$ -k)) \) by (rule Int_ZF_3_L7 )
with A1 show \( P(k) \) using Int_ZF_2_L1A, zminus_zminus
qed

An implication between two forms of induction steps.

lemma (in int0) Int_ZF_3_L9:

assumes A1: \( i\in \mathbb{Z} \) and A2: \( \forall n.\ n\leq i \wedge P(n) \longrightarrow P(n \ \$ + \ \$ -(\ \$ #1)) \)

shows \( \forall m.\ \ \$ -i\leq m \wedge P(\ \$ -m) \longrightarrow P(\ \$ -(m \ \$ + (\ \$ # 1))) \)proof
fix \( m \)
show \( \ \$ -i\leq m \wedge P(\ \$ -m) \longrightarrow P(\ \$ -(m \ \$ + (\ \$ # 1))) \)proof
assume A3: \( \ \$ - i \leq m \wedge P(\ \$ - m) \)
then have \( \ \$ - i \leq m \)
then have \( \ \$ -m \leq \ \$ - (\ \$ - i) \) by (rule Int_ZF_2_L10 )
with A1, A2, A3 show \( P(\ \$ -(m \ \$ + (\ \$ # 1))) \) using zminus_zminus, zminus_zadd_distrib
qed
qed

Backwards induction on integers, version with higher-order decrement function.

lemma (in int0) Int_ZF_3_L9A:

assumes A1: \( k\leq i \) and A2: \( P(i) \) and A3: \( \forall n.\ n\leq i \wedge P(n) \longrightarrow P(n \ \$ + \ \$ -(\ \$ #1)) \)

shows \( P(k) \)proof
from A1 have T1: \( i\in \mathbb{Z} \) using Int_ZF_2_L1A
from T1, A3 have T2: \( \forall m.\ \ \$ -i\leq m \wedge P(\ \$ -m) \longrightarrow P(\ \$ -(m \ \$ + (\ \$ # 1))) \) by (rule Int_ZF_3_L9 )
from A1, A2, T2 show \( P(k) \) by (rule Int_ZF_3_L8 )
qed

Induction on integers, implication between two forms of the induction step.

lemma (in int0) Int_ZF_3_L10:

assumes A1: \( \forall n.\ n\leq i \wedge P(n) \longrightarrow P(n - 1 ) \)

shows \( \forall n.\ n\leq i \wedge P(n) \longrightarrow P(n \ \$ + \ \$ -(\ \$ #1)) \)proof
{
fix \( n \)
assume \( n\leq i \wedge P(n) \)
with A1 have T1: \( n\in \mathbb{Z} \), \( P(n - 1 ) \) using Int_ZF_2_L1A
then have \( n - 1 = n - (\ \$ # 1) \) using Int_ZF_1_L8
with T1 have \( P(n \ \$ + \ \$ -(\ \$ #1)) \) using Int_ZF_1_L10
}
then show \( thesis \)
qed

Backwards induction on integers.

theorem (in int0) Back_induct_on_int:

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

shows \( P(k) \)proof
from A3 have \( \forall n.\ n\leq i \wedge P(n) \longrightarrow P(n \ \$ + \ \$ -(\ \$ #1)) \) by (rule Int_ZF_3_L10 )
with A1, A2 show \( P(k) \) by (rule Int_ZF_3_L9A )
qed

Bounded vs. finite subsets of integers

The goal of this section is to establish that a subset of integers is bounded is and only is it is finite. The fact that all finite sets are bounded is already shown for all linearly ordered groups in OrderedGroups_ZF.thy. To show the other implication we show that all intervals starting at 0 are finite and then use a result from OrderedGroups_ZF.thy.

There are no integers between \(k\) and \(k+1\).

lemma (in int0) Int_ZF_4_L1:

assumes A1: \( k\in \mathbb{Z} \), \( m\in \mathbb{Z} \), \( n\in nat \) and A2: \( k \ \$ + \ \$ #1 = m \ \$ + \ \$ #n \)

shows \( m = k \ \$ + \ \$ #1 \vee m \leq k \)proof
{
assume \( n=0 \)
with A1, A2 have \( m = k \ \$ + \ \$ #1 \vee m \leq k \) using zadd_int0
}
moreover {
assume \( n\neq 0 \)
with A1 obtain \( j \) where D1: \( j\in nat \), \( n = succ(j) \) using Nat_ZF_1_L3
with A1, A2, D1 have \( m = k \ \$ + \ \$ #1 \vee m \leq k \) using Int_ZF_2_L13
} ultimately show \( thesis \)
qed

A trivial calculation lemma that allows to subtract and add one.

lemma Int_ZF_4_L1A:

assumes \( m\in int \)

shows \( m \ \$ - \ \$ #1 \ \$ + \ \$ #1 = m \) using assms, eq_zdiff_iff

There are no integers between \(k\) and \(k+1\), another formulation.

lemma (in int0) Int_ZF_4_L1B:

assumes A1: \( m \leq L \)

shows \( m = L \vee m + 1 \leq L \), \( m = L \vee m \leq L - 1 \)proof
let \( k = L \ \$ - \ \$ #1 \)
from A1 have T1: \( m\in \mathbb{Z} \), \( L\in \mathbb{Z} \), \( L = k \ \$ + \ \$ #1 \) using Int_ZF_2_L1A, Int_ZF_4_L1A
moreover
from A1 obtain \( n \) where D1: \( n\in nat \), \( L = m \ \$ + \ \$ # n \) using Int_ZF_3_L2
ultimately have \( m = L \vee m \leq k \) using Int_ZF_4_L1
with T1 show \( m = L \vee m + 1 \leq L \) using Int_ZF_2_L9A
with T1 show \( m = L \vee m \leq L - 1 \) using Int_ZF_1_L8A, Int_ZF_2_L9B
qed

If \(j\in m..k+1\), then \(j\in m..n\) or \(j=k+1\).

lemma (in int0) Int_ZF_4_L2:

assumes A1: \( k\in \mathbb{Z} \) and A2: \( j \in m.\ .\ (k \ \$ + \ \$ #1) \)

shows \( j \in m.\ .\ k \vee j \in \{k \ \$ + \ \$ #1\} \)proof
from A2 have T1: \( m\leq j \), \( j\leq (k \ \$ + \ \$ #1) \) using Order_ZF_2_L1A
then have T2: \( m\in \mathbb{Z} \), \( j\in \mathbb{Z} \) using Int_ZF_2_L1A
from T1 obtain \( n \) where \( n\in nat \), \( k \ \$ + \ \$ #1 = j \ \$ + \ \$ # n \) using Int_ZF_3_L2
with A1, T1, T2 have \( (m\leq j \wedge j \leq k) \vee j \in \{k \ \$ + \ \$ #1\} \) using Int_ZF_4_L1
then show \( thesis \) using Order_ZF_2_L1B
qed

Extending an integer interval by one is the same as adding the new endpoint.

lemma (in int0) Int_ZF_4_L3:

assumes A1: \( m\leq k \)

shows \( m.\ .\ (k \ \$ + \ \$ #1) = m.\ .\ k \cup \{k \ \$ + \ \$ #1\} \)proof
from A1 have T1: \( m\in \mathbb{Z} \), \( k\in \mathbb{Z} \) using Int_ZF_2_L1A
then show \( m .\ .\ (k \ \$ + \ \$ # 1) \subseteq m .\ .\ k \cup \{k \ \$ + \ \$ # 1\} \) using Int_ZF_4_L2
from T1 have \( m\leq m \) using Int_ZF_2_T1, OrderedGroup_ZF_1_L3
with T1, A1 have \( m .\ .\ k \subseteq m .\ .\ (k \ \$ + \ \$ # 1) \) using Int_ZF_2_L12, Int_ZF_2_L6, Order_ZF_2_L3
with T1, A1 show \( m.\ .\ k \cup \{k \ \$ + \ \$ #1\} \subseteq m.\ .\ (k \ \$ + \ \$ #1) \) using Int_ZF_2_L12A, int_ord_is_refl, Order_ZF_2_L2
qed

Integer intervals are finite - induction step.

lemma (in int0) Int_ZF_4_L4:

assumes A1: \( i\leq m \) and A2: \( i.\ .\ m \in Fin(\mathbb{Z} ) \)

shows \( i.\ .\ (m \ \$ + \ \$ #1) \in Fin(\mathbb{Z} ) \) using assms, Int_ZF_4_L3

Integer intervals are finite.

lemma (in int0) Int_ZF_4_L5:

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

shows \( i.\ .\ k \in Fin(\mathbb{Z} ) \)proof
{
assume A2: \( i\leq k \)
moreover
from A1 have \( i.\ .\ i \in Fin(\mathbb{Z} ) \) using int_ord_is_refl, Int_ZF_2_L4, Order_ZF_2_L4
moreover
from A2 have \( \forall m.\ i\leq m \wedge i.\ .\ m \in Fin(\mathbb{Z} ) \longrightarrow i.\ .\ (m \ \$ + \ \$ #1) \in Fin(\mathbb{Z} ) \) using Int_ZF_4_L4
ultimately have \( i.\ .\ k \in Fin(\mathbb{Z} ) \) by (rule Int_ZF_3_L7 )
}
moreover {
assume \( \neg i \leq k \)
then have \( i.\ .\ k \in Fin(\mathbb{Z} ) \) using Int_ZF_2_L6, Order_ZF_2_L5
} ultimately show \( thesis \)
qed

Bounded integer sets are finite.

lemma (in int0) Int_ZF_4_L6:

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

shows \( A \in Fin(\mathbb{Z} ) \)proof
have T1: \( \forall m \in \text{Nonnegative}(\mathbb{Z} ,IntegerAddition,IntegerOrder).\ \) \( \ \$ #0.\ .\ m \in Fin(\mathbb{Z} ) \)proof
fix \( m \)
assume \( m \in \text{Nonnegative}(\mathbb{Z} ,IntegerAddition,IntegerOrder) \)
then have \( m\in \mathbb{Z} \) using Int_ZF_2_T1, OrderedGroup_ZF_1_L4E
then show \( \ \$ #0.\ .\ m \in Fin(\mathbb{Z} ) \) using Int_ZF_4_L5
qed
have \( group3(\mathbb{Z} ,IntegerAddition,IntegerOrder) \) using Int_ZF_2_T1
moreover
from T1 have \( \forall m \in \text{Nonnegative}(\mathbb{Z} ,IntegerAddition,IntegerOrder).\ \) \( \text{Interval}(IntegerOrder,\text{ TheNeutralElement}(\mathbb{Z} ,IntegerAddition),m) \) \( \in Fin(\mathbb{Z} ) \) using Int_ZF_1_L8
moreover
note A1
ultimately show \( A \in Fin(\mathbb{Z} ) \) by (rule OrderedGroup_ZF_2_T1 )
qed

A subset of integers is bounded iff it is finite.

theorem (in int0) Int_bounded_iff_fin:

shows \( \text{IsBounded}(A,IntegerOrder)\longleftrightarrow A\in Fin(\mathbb{Z} ) \) using Int_ZF_4_L6, Int_ZF_2_T1, ord_group_fin_bounded

The image of an interval by any integer function is finite, hence bounded.

lemma (in int0) Int_ZF_4_L8:

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

shows \( f(i.\ .\ k) \in Fin(\mathbb{Z} ) \), \( \text{IsBounded}(f(i.\ .\ k),IntegerOrder) \) using assms, Int_ZF_4_L5, Finite1_L6A, Int_bounded_iff_fin

If for every integer we can find one in \(A\) that is greater or equal, then \(A\) is is not bounded above, hence infinite.

lemma (in int0) Int_ZF_4_L9:

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

shows \( \neg \text{IsBoundedAbove}(A,IntegerOrder) \), \( A \notin Fin(\mathbb{Z} ) \)proof
have \( \mathbb{Z} \neq \{ 0 \} \) using Int_ZF_1_L8A, int_zero_not_one
with A1 show \( \neg \text{IsBoundedAbove}(A,IntegerOrder) \), \( A \notin Fin(\mathbb{Z} ) \) using Int_ZF_2_T1, OrderedGroup_ZF_2_L2A
qed
end
lemma func1_1_L11A:

assumes \( \forall x\in X.\ b(x) \in Y \)

shows \( \{\langle x,y\rangle \in X\times Y.\ b(x) = y\} : X\rightarrow Y \)
Definition of IntegerAddition: \( IntegerAddition \equiv \{ \langle x,c\rangle \in (int\times int)\times int.\ \text{fst}(x) \ \$ + \text{snd}(x) = c\} \)
Definition of IntegerMultiplication: \( IntegerMultiplication \equiv \) \( \{ \langle x,c\rangle \in (int\times int)\times int.\ \text{fst}(x) \ \$ * \text{snd}(x) = c\} \)
lemma Int_ZF_1_L1: shows \( IntegerAddition : int\times int \rightarrow int \), \( IntegerMultiplication : int\times int \rightarrow int \)
lemma (in int0) Int_ZF_1_L2:

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

shows \( a + b = a \ \$ + b \), \( a\cdot b = a \ \$ * b \)
lemma (in int0) Int_ZF_1_L4:

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

shows \( x + y = y + x \), \( x\cdot y = y\cdot x \)
lemma (in int0) Int_ZF_1_L5:

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

shows \( (\ \$ # 0) + x = x \wedge x + (\ \$ # 0) = x \), \( (\ \$ # 1)\cdot x = x \wedge x\cdot (\ \$ # 1) = x \)
lemma (in int0) Int_ZF_1_L6: shows \( (\ \$ # 0)\in \mathbb{Z} \wedge \) \( (\forall x\in \mathbb{Z} .\ (\ \$ # 0) + x = x \wedge x + (\ \$ # 0) = x) \), \( (\ \$ # 1)\in \mathbb{Z} \wedge \) \( (\forall x\in \mathbb{Z} .\ (\ \$ # 1)\cdot x = x \wedge x\cdot (\ \$ # 1) = x) \)
Definition of IsAmonoid: \( \text{IsAmonoid}(G,f) \equiv \) \( f \text{ is associative on } G \wedge \) \( (\exists e\in G.\ (\forall g\in G.\ ( (f(\langle e,g\rangle ) = g) \wedge (f(\langle g,e\rangle ) = g)))) \)
Definition of IsAssociative: \( P \text{ is associative on } G \equiv P : G\times G\rightarrow G \wedge \) \( (\forall x \in G.\ \forall y \in G.\ \forall z \in G.\ \) \( ( P(\langle P(\langle x,y\rangle ),z\rangle ) = P( \langle x,P(\langle y,z\rangle )\rangle ))) \)
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) \)
theorem (in int0) Int_ZF_1_T1: shows \( \text{IsAmonoid}(\mathbb{Z} ,IntegerAddition) \), \( \text{IsAmonoid}(\mathbb{Z} ,IntegerMultiplication) \)
lemma (in monoid0) group0_1_L4:

assumes \( e \in G \wedge (\forall g\in G.\ e \oplus g = g \wedge g \oplus e = g) \)

shows \( e = \text{ TheNeutralElement}(G,f) \)
lemma (in int0) Int_ZF_1_L8: shows \( (\ \$ # 0) = 0 \), \( (\ \$ # 1) = 1 \)
lemma (in int0) Int_ZF_1_L8A: shows \( 0 \in \mathbb{Z} \), \( 1 \in \mathbb{Z} \)
lemma (in int0) int_zero_not_one: shows \( 0 \neq 1 \)
lemma (in int0) Int_ZF_1_L9:

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

shows \( \exists b\in \mathbb{Z} .\ g + b = 0 \)
Definition of IsAgroup: \( \text{IsAgroup}(G,f) \equiv \) \( ( \text{IsAmonoid}(G,f) \wedge (\forall g\in G.\ \exists b\in G.\ f\langle g,b\rangle = \text{ TheNeutralElement}(G,f))) \)
Definition of IsCommutative: \( f \text{ is commutative on } G \equiv \forall x\in G.\ \forall y\in G.\ f\langle x,y\rangle = f\langle y,x\rangle \)
theorem Int_ZF_1_T2: shows \( \text{IsAgroup}(int,IntegerAddition) \), \( IntegerAddition \text{ is commutative on } int \), \( group0(int,IntegerAddition) \)
lemma (in group0) group0_2_L9:

assumes \( a\in G \) and \( b\in G \) and \( a\cdot b = 1 \)

shows \( a = b^{-1} \) and \( b = a^{-1} \)
lemma (in group0) inverse_in_group:

assumes \( x\in G \)

shows \( x^{-1}\in G \)
lemma (in int0) Int_ZF_1_L9A:

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

shows \( \ \$ -m = - m \)
lemma (in group0) group_inv_of_one: shows \( 1 ^{-1} = 1 \)
lemma Int_ZF_1_L12:

assumes \( m\in int \)

shows \( m \ \$ - \ \$ #1 \ \$ + \ \$ #1 = m \)
lemma (in group0) group0_2_L7:

assumes \( a\in G \) and \( b\in G \) and \( a\cdot b = a \)

shows \( b=1 \)
lemma (in group0) inv_cancel_two:

assumes \( a\in G \), \( b\in G \)

shows \( a\cdot b^{-1}\cdot b = a \), \( a\cdot b\cdot b^{-1} = a \), \( a^{-1}\cdot (a\cdot b) = b \), \( a\cdot (a^{-1}\cdot b) = b \)
lemma (in group0) group0_2_L11A:

assumes \( a\in G \), \( b\in G \) and \( a\cdot b^{-1} = 1 \)

shows \( a=b \)
Definition of IntegerOrder: \( IntegerOrder \equiv \{p \in int\times int.\ \text{fst}(p) \ \$ \leq \text{snd}(p)\} \)
lemma Int_ZF_2_L1B: shows \( IntegerOrder \subseteq int\times int \)
lemma Order_ZF_3_L1B:

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

shows \( A\subseteq X \)
lemma (in int0) Int_ZF_2_L1:

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

shows \( m \leq n \)
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_L3:

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

shows \( m=n \)
lemma Int_ZF_2_L5:

assumes \( \langle m,n\rangle \in IntegerOrder \), \( \langle n,k\rangle \in IntegerOrder \)

shows \( \langle m,k\rangle \in IntegerOrder \)
lemma Fol1_L2:

assumes \( \forall x y z.\ \langle x, y\rangle \in r \wedge \langle y, z\rangle \in r \longrightarrow \langle x, z\rangle \in r \)

shows \( \text{trans}(r) \)
lemma (in int0) int_ord_is_refl: shows \( \text{refl}(\mathbb{Z} ,IntegerOrder) \)
lemma (in int0) Int_ZF_2_L4: shows \( \text{antisym}(IntegerOrder) \)
lemma Int_ZF_2_L6: shows \( \text{trans}(IntegerOrder) \)
Definition of IsPartOrder: \( \text{IsPartOrder}(X,r) \equiv \text{refl}(X,r) \wedge \text{antisym}(r) \wedge \text{trans}(r) \)
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 Int_ZF_2_L7: shows \( \text{IsPartOrder}(int,IntegerOrder) \)
Definition of IsAnOrdGroup: \( \text{IsAnOrdGroup}(G,P,r) \equiv \) \( ( \text{IsAgroup}(G,P) \wedge r\subseteq G\times G \wedge \text{IsPartOrder}(G,r) \wedge (\forall g\in G.\ \forall a b.\ \) \( \langle a,b\rangle \in r \longrightarrow \langle P\langle a,g\rangle ,P\langle b,g\rangle \rangle \in r \wedge \langle P\langle g,a\rangle ,P\langle g,b\rangle \rangle \in r ) ) \)
Definition of IsTotal: \( r \text{ is total on } X \equiv (\forall a\in X.\ \forall b\in X.\ \langle a,b\rangle \in r \vee \langle b,a\rangle \in r) \)
Definition of IsLinOrder: \( \text{IsLinOrder}(X,r) \equiv \text{antisym}(r) \wedge \text{trans}(r) \wedge (r \text{ is total on } X) \)
lemma (in int0) Int_ZF_1_L13:

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

shows \( (m \ \$ - \ \$ #1) + 1 = m \)
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_1_L9A:

assumes \( a\in G \), \( b\in G \), \( c\in G \)

shows \( a\cdot b \leq c \longleftrightarrow a \leq c\cdot b^{-1} \)
lemma (in group3) OrderedGroup_ZF_1_L9B:

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

shows \( a \leq c\cdot b \)
lemma (in group3) OrderedGroup_ZF_1_L5:

assumes \( a\leq b \)

shows \( b^{-1}\leq a^{-1} \)
lemma (in group3) OrderedGroup_ZF_1_L5AD:

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

shows \( b \leq a^{-1} \)
lemma (in group3) OrderedGroup_ZF_1_L5AF:

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

shows \( c\leq b \)
lemma (in group3) OrderedGroup_ZF_1_L5A:

assumes \( a\leq 1 \)

shows \( 1 \leq a^{-1} \)
lemma (in group3) OrderedGroup_ZF_1_L5AA:

assumes \( a\in G \) and \( 1 \leq a^{-1} \)

shows \( a\leq 1 \)
lemma Nat_ZF_1_L3:

assumes \( n \in nat \) and \( n\neq 0 \)

shows \( \exists k\in nat.\ n = succ(k) \)
lemma (in int0) Int_ZF_2_L12:

assumes \( i\in \mathbb{Z} \) and \( n\in nat \)

shows \( i \leq i \ \$ + \ \$ #n \)
lemma (in int0) Int_ZF_2_L12A:

assumes \( j\leq k \)

shows \( j \leq k \ \$ + \ \$ #1 \), \( j \leq k + 1 \)
lemma (in int0) Int_ZF_2_L11: shows \( i \ \$ + \ \$ # n \ \$ + (\ \$ # 1) = i \ \$ + \ \$ # succ(n) \)
lemma (in group3) OrderedGroup_ZF_3_L1: shows \( \text{AbsoluteValue}(G,P,r) : G\rightarrow G \)
lemma (in group3) OrderedGroup_ZF_1_L5AC:

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

shows \( a^{-1} \leq b \)
lemma (in group3) OrderedGroup_ZF_1_L12:

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

shows \( 1 \leq a\cdot b \)
lemma (in group3) OrderedGroup_ZF_1_L5E:

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

shows \( a \leq b_1\cdot c_1 \)
lemma (in group3) OrderedGroup_ZF_1_L5B:

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

shows \( a\cdot c \leq b\cdot d \)
lemma (in group3) OrderedGroup_ZF_1_L5I:

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

shows \( a\cdot d^{-1} \leq b\cdot c^{-1} \)
lemma (in group3) OrderedGroup_ZF_1_L5D:

assumes \( b\in G \) and \( a \leq b\cdot c \) and \( c\leq b_1 \)

shows \( a \leq b\cdot b_1 \)
lemma (in group3) OrderedGroup_ZF_1_L10:

assumes \( a\in G \), \( b\in G \) and \( c\leq d \)

shows \( a\cdot c\cdot b \leq a\cdot d\cdot b \)
lemma (in group3) OrderedGroup_ZF_1_L5F:

assumes \( 1 \leq a \) and \( b\in G \)

shows \( b\leq a\cdot b \), \( b\leq b\cdot a \)
lemma (in group3) OrderedGroup_ZF_3_L6A:

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

shows \( a\cdot b \leq \vert a\vert \cdot \vert b\vert \), \( a\cdot b^{-1} \leq \vert a\vert \cdot \vert b\vert \), \( a^{-1}\cdot b \leq \vert a\vert \cdot \vert b\vert \), \( a^{-1}\cdot b^{-1} \leq \vert a\vert \cdot \vert b\vert \)
lemma (in group3) OrderedGroup_ZF_1_L5G:

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

shows \( a\leq b\cdot c \), \( a\leq c\cdot b \)
theorem (in group3) OrdGroup_triangle_ineq:

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

shows \( \vert a\cdot b\vert \leq \vert a\vert \cdot \vert b\vert \)
lemma (in group3) OrderedGroup_ZF_1_L2: shows \( g\in G^+ \longleftrightarrow 1 \leq g \)
lemma (in group3) OrderedGroup_ZF_3_L2:

assumes \( a\in G^+ \)

shows \( \vert a\vert = a \)
lemma (in group0) group0_2_L2: shows \( 1 \in G \wedge (\forall g\in G.\ (1 \cdot g = g \wedge g\cdot 1 = g)) \)
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_L16A: shows \( 0 \leq 1 \) and \( abs(1 ) = 1 \)
lemma (in int0) Int_order_transitive:

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

shows \( m\leq k \)
lemma (in int0) Int_ZF_2_L16B: shows \( 1 \leq 2 \)
lemma (in group3) OrderedGroup_ZF_3_L7A:

assumes \( r \text{ is total on } G \) and \( a\in G \)

shows \( \vert a^{-1}\vert = \vert a\vert \)
lemma (in group3) OrderedGroup_ZF_3_L2A: shows \( \vert 1 \vert = 1 \)
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 int0) Int_ZF_2_L17:

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

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

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

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

assumes \( P \text{ is commutative on } G \) and \( r \text{ is total on } G \) and \( a\in G \), \( b\in G \) and \( \vert a\cdot b^{-1}\vert \leq c \)

shows \( \vert a\vert \leq c\cdot \vert b\vert \), \( \vert a\vert \leq \vert b\vert \cdot c \), \( c^{-1}\cdot a \leq b \), \( a\cdot c^{-1} \leq b \), \( a \leq b\cdot c \)
lemma (in group3) OrderedGroup_ZF_3_L7E:

assumes \( P \text{ is commutative on } G \) and \( r \text{ is total on } G \) and \( a\in G \), \( b\in G \) and \( \vert a\cdot b^{-1}\vert \leq c \)

shows \( b\cdot c^{-1} \leq a \)
lemma (in group0) group_op_closed:

assumes \( a\in G \), \( b\in G \)

shows \( a\cdot b \in G \)
lemma (in int0) Int_ZF_2_L10:

assumes \( k \leq i \)

shows \( ( - i) \leq ( - k) \), \( \ \$ -i \leq \ \$ -k \)
lemma (in group3) OrderedGroup_ZF_1_L8AA:

assumes \( a\leq b \) and \( a\neq b \)

shows \( \neg (b\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 group3) OrderedGroup_ZF_1_L18:

assumes \( r \text{ is total on } G \) and \( b\in G \) and \( Q(1 ) \) and \( \forall a\in G_+.\ Q(a) \) and \( \forall a\in G_+.\ Q(a^{-1}) \)

shows \( Q(b) \)
lemma (in group3) OrderedGroup_ZF_3_L5:

assumes \( r \text{ is total on } G \) and \( a\in G \)

shows \( a \leq \vert a\vert \)
lemma (in group3) OrderedGroup_ZF_3_L6:

assumes \( a\in G \)

shows \( a^{-1} \leq \vert a\vert \)
lemma (in group3) OrderedGroup_ZF_3_L7B:

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

shows \( \vert a\cdot b^{-1}\vert = \vert b\cdot a^{-1}\vert \)
lemma (in group3) OrderedGroup_ZF_3_L7C:

assumes \( P \text{ is commutative on } G \) and \( r \text{ is total on } G \), \( a\in G \), \( b\in G \) and \( \vert a\vert \leq c \), \( \vert b\vert \leq d \)

shows \( \vert a\cdot b\vert \leq c\cdot d \)
lemma (in group3) OrderedGroup_ZF_3_L7CA:

assumes \( P \text{ is commutative on } G \) and \( r \text{ is total on } G \) and \( a\in G \), \( b\in G \) and \( \vert a\vert \leq c \), \( \vert b\vert \leq d \)

shows \( \vert a\cdot b^{-1}\vert \leq c\cdot d \)
lemma (in group3) OrderedGroup_ZF_3_L3C:

assumes \( r \text{ is total on } G \)

shows \( \text{AbsoluteValue}(G,P,r) : G\rightarrow G^+ \)
lemma (in int0) Int_ZF_2_L9:

assumes \( i \leq m \) and \( i\neq m \)

shows \( i \ \$ \lt m \)
lemma (in int0) Int_ZF_3_L2:

assumes \( i \leq m \)

shows \( \exists n\in nat.\ m = i \ \$ + \ \$ # n \)
lemma (in int0) Int_ZF_3_L6:

assumes \( i\in \mathbb{Z} \) and \( \forall m.\ i\leq m \wedge Q(m) \longrightarrow Q(m \ \$ + (\ \$ # 1)) \)

shows \( \forall k\in nat.\ Q(i \ \$ + (\ \$ # k)) \longrightarrow Q(i \ \$ + (\ \$ # succ(k))) \)
theorem ind_on_nat:

assumes \( n\in nat \) and \( P(0) \) and \( \forall k\in nat.\ P(k)\longrightarrow P(succ(k)) \)

shows \( P(n) \)
lemma (in int0) Int_ZF_3_L7A:

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

shows \( \forall m.\ i\leq m \wedge Q(m) \longrightarrow Q(m \ \$ + (\ \$ # 1)) \)
lemma (in int0) Int_ZF_3_L7:

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_3_L9:

assumes \( i\in \mathbb{Z} \) and \( \forall n.\ n\leq i \wedge P(n) \longrightarrow P(n \ \$ + \ \$ -(\ \$ #1)) \)

shows \( \forall m.\ \ \$ -i\leq m \wedge P(\ \$ -m) \longrightarrow P(\ \$ -(m \ \$ + (\ \$ # 1))) \)
lemma (in int0) Int_ZF_3_L8:

assumes \( k\leq i \) and \( P(i) \) and \( \forall m.\ \ \$ -i\leq m \wedge P(\ \$ -m) \longrightarrow P(\ \$ -(m \ \$ + (\ \$ # 1))) \)

shows \( P(k) \)
lemma (in int0) Int_ZF_1_L10:

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

shows \( m - n = m \ \$ + \ \$ -n \)
lemma (in int0) Int_ZF_3_L10:

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

shows \( \forall n.\ n\leq i \wedge P(n) \longrightarrow P(n \ \$ + \ \$ -(\ \$ #1)) \)
lemma (in int0) Int_ZF_3_L9A:

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

assumes \( k\in \mathbb{Z} \), \( m\in \mathbb{Z} \) and \( n\in nat \) and \( k \ \$ + (\ \$ # 1) = m \ \$ + \ \$ # succ(n) \)

shows \( m \leq k \)
lemma Int_ZF_4_L1A:

assumes \( m\in int \)

shows \( m \ \$ - \ \$ #1 \ \$ + \ \$ #1 = m \)
lemma (in int0) Int_ZF_4_L1:

assumes \( k\in \mathbb{Z} \), \( m\in \mathbb{Z} \), \( n\in nat \) and \( k \ \$ + \ \$ #1 = m \ \$ + \ \$ #n \)

shows \( m = k \ \$ + \ \$ #1 \vee m \leq k \)
lemma (in int0) Int_ZF_2_L9A:

assumes \( k\in \mathbb{Z} \) and \( m \leq k \ \$ - (\ \$ # 1) \)

shows \( m + 1 \leq k \)
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 Order_ZF_2_L1A:

assumes \( x \in \text{Interval}(r,a,b) \)

shows \( \langle a,x\rangle \in r \), \( \langle x,b\rangle \in r \)
lemma Order_ZF_2_L1B:

assumes \( \langle a,x\rangle \in r \), \( \langle x,b\rangle \in r \)

shows \( x \in \text{Interval}(r,a,b) \)
lemma (in int0) Int_ZF_4_L2:

assumes \( k\in \mathbb{Z} \) and \( j \in m.\ .\ (k \ \$ + \ \$ #1) \)

shows \( j \in m.\ .\ k \vee j \in \{k \ \$ + \ \$ #1\} \)
lemma (in group3) OrderedGroup_ZF_1_L3:

assumes \( g\in G \)

shows \( g\leq g \)
lemma Order_ZF_2_L3:

assumes \( \text{trans}(r) \) and \( \langle a,b\rangle \in r \), \( \langle b,c\rangle \in r \), \( \langle c,d\rangle \in r \)

shows \( \text{Interval}(r,b,c) \subseteq \text{Interval}(r,a,d) \)
lemma Order_ZF_2_L2:

assumes \( \text{refl}(X,r) \) and \( a\in X \), \( b\in X \) and \( \langle a,b\rangle \in r \)

shows \( a \in \text{Interval}(r,a,b) \), \( b \in \text{Interval}(r,a,b) \)
lemma (in int0) Int_ZF_4_L3:

assumes \( m\leq k \)

shows \( m.\ .\ (k \ \$ + \ \$ #1) = m.\ .\ k \cup \{k \ \$ + \ \$ #1\} \)
lemma Order_ZF_2_L4:

assumes \( \text{refl}(X,r) \) and \( \text{antisym}(r) \) and \( a\in X \)

shows \( \text{Interval}(r,a,a) = \{a\} \)
lemma (in int0) Int_ZF_4_L4:

assumes \( i\leq m \) and \( i.\ .\ m \in Fin(\mathbb{Z} ) \)

shows \( i.\ .\ (m \ \$ + \ \$ #1) \in Fin(\mathbb{Z} ) \)
lemma Order_ZF_2_L5:

assumes \( \text{trans}(r) \) and \( \langle a,b\rangle \notin r \)

shows \( \text{Interval}(r,a,b) = 0 \)
lemma (in group3) OrderedGroup_ZF_1_L4E: shows \( G^+ \subseteq G \)
lemma (in int0) Int_ZF_4_L5:

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

shows \( i.\ .\ k \in Fin(\mathbb{Z} ) \)
theorem (in group3) OrderedGroup_ZF_2_T1:

assumes \( \forall g\in G^+.\ \text{Interval}(r,1 ,g) \in Fin(G) \) and \( \text{IsBounded}(A,r) \)

shows \( A \in Fin(G) \)
lemma (in int0) Int_ZF_4_L6:

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

shows \( A \in Fin(\mathbb{Z} ) \)
theorem (in group3) ord_group_fin_bounded:

assumes \( r \text{ is total on } G \) and \( B\in Fin(G) \)

shows \( \text{IsBounded}(B,r) \)
lemma Finite1_L6A:

assumes \( f:X\rightarrow Y \) and \( N \in Fin(X) \)

shows \( f(N) \in Fin(Y) \)
theorem (in int0) Int_bounded_iff_fin: shows \( \text{IsBounded}(A,IntegerOrder)\longleftrightarrow A\in Fin(\mathbb{Z} ) \)
lemma (in group3) OrderedGroup_ZF_2_L2A:

assumes \( r \text{ is total on } G \) and \( G \neq \{1 \} \) and \( \forall a\in G.\ \exists b\in A.\ a\leq b \)

shows \( \forall a\in G.\ \exists b\in A.\ a\neq b \wedge a\leq b \), \( \neg \text{IsBoundedAbove}(A,r) \), \( A \notin Fin(G) \)