IsarMathLib

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

theory Int_ZF_1 imports Int_ZF_IML OrderedRing_ZF
begin

This theory file considers the set of integers as an ordered ring.

Integers as a ring

In this section we show that integers form a commutative ring.

The next lemma provides the condition to show that addition is distributive with respect to multiplication.

lemma (in int0) Int_ZF_1_1_L1:

assumes A1: \( 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 \) using assms, Int_ZF_1_L2, zadd_zmult_distrib, zadd_zmult_distrib2

Integers form a commutative ring, hence we can use theorems proven in ring0 context (locale).

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) \)proof
have \( \forall a\in \mathbb{Z} .\ \forall b\in \mathbb{Z} .\ \forall c\in \mathbb{Z} .\ \) \( a\cdot (b + c) = a\cdot b + a\cdot c \wedge (b + c)\cdot a = b\cdot a + c\cdot a \) using Int_ZF_1_1_L1
then have \( \text{IsDistributive}(\mathbb{Z} ,IntegerAddition,IntegerMultiplication) \) using IsDistributive_def
then show \( \text{IsAring}(\mathbb{Z} ,IntegerAddition,IntegerMultiplication) \), \( ring0(\mathbb{Z} ,IntegerAddition,IntegerMultiplication) \) using Int_ZF_1_T1, Int_ZF_1_T2, IsAring_def, ring0_def
have \( \forall a\in \mathbb{Z} .\ \forall b\in \mathbb{Z} .\ a\cdot b = b\cdot a \) using Int_ZF_1_L4
then show \( IntegerMultiplication \text{ is commutative on } \mathbb{Z} \) using IsCommutative_def
qed

Zero and one are integers.

lemma (in int0) int_zero_one_are_int:

shows \( 0 \in \mathbb{Z} \), \( 1 \in \mathbb{Z} \) using Int_ZF_1_1_L2, Ring_ZF_1_L2

Negative of zero is zero.

lemma (in int0) int_zero_one_are_intA:

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

Properties with one integer.

lemma (in int0) Int_ZF_1_1_L4:

assumes A1: \( 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 \)proof
from A1 show \( a + 0 = a \), \( 0 + a = a \), \( a\cdot 1 = a \), \( 1 \cdot a = a \), \( a - a = 0 \), \( a - 0 = a \), \( ( - a) \in \mathbb{Z} \), \( 2 \cdot a = a + a \), \( ( - ( - a)) = a \) using Int_ZF_1_1_L2, Ring_ZF_1_L3
from A1 show \( 0 \cdot a = 0 \), \( a\cdot 0 = 0 \) using Int_ZF_1_1_L2, Ring_ZF_1_L6
qed

Properties that require two integers.

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 \) using assms, Int_ZF_1_1_L2, Ring_ZF_1_L4, Ring_ZF_1_L9, Ring_ZF_1_L7, Ring_ZF_1_L7A, Int_ZF_1_L4

\(2\) and \(3\) are integers.

lemma (in int0) int_two_three_are_int:

shows \( 2 \in \mathbb{Z} \), \( 3 \in \mathbb{Z} \) using int_zero_one_are_int, Int_ZF_1_1_L5

Another property with two integers.

lemma (in int0) Int_ZF_1_1_L5B:

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

shows \( a - ( - b) = a + b \) using assms, Int_ZF_1_1_L2, Ring_ZF_1_L9

Properties that require three integers.

lemma (in int0) Int_ZF_1_1_L6:

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

shows \( a - (b + c) = a - b - c \), \( a - (b - c) = a - b + c \), \( a\cdot (b - c) = a\cdot b - a\cdot c \), \( (b - c)\cdot a = b\cdot a - c\cdot a \) using assms, Int_ZF_1_1_L2, Ring_ZF_1_L10, Ring_ZF_1_L8

One more property with three integers.

lemma (in int0) Int_ZF_1_1_L6A:

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

shows \( a + (b - c) = a + b - c \) using assms, Int_ZF_1_1_L2, Ring_ZF_1_L10A

Associativity of addition and multiplication.

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) \) using assms, Int_ZF_1_1_L2, Ring_ZF_1_L11

Rearrangement lemmas

In this section we collect lemmas about identities related to rearranging the terms in expresssions

A formula with a positive integer.

lemma (in int0) Int_ZF_1_2_L1:

assumes \( 0 \leq a \)

shows \( abs(a) + 1 = abs(a + 1 ) \) using assms, Int_ZF_2_L16, Int_ZF_2_L12A

A formula with two integers, one positive.

lemma (in int0) Int_ZF_1_2_L2:

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

shows \( a + (abs(b) + 1 )\cdot a = (abs(b + 1 ) + 1 )\cdot a \)proof
from A2 have \( abs(b + 1 ) \in \mathbb{Z} \) using Int_ZF_2_L12A, Int_ZF_2_L1A, Int_ZF_2_L14
with A1, A2 show \( thesis \) using Int_ZF_1_2_L1, Int_ZF_1_1_L2, Ring_ZF_2_L1
qed

A couple of formulae about canceling opposite integers.

lemma (in int0) Int_ZF_1_2_L3:

assumes A1: \( 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 \) using assms, Int_ZF_1_T2, group0_4_L6A, inv_cancel_two, group0_2_L16A, group0_4_L6AA, group0_4_L6AB, group0_4_L6F, group0_4_L6AC

Subtracting one does not increase integers. This may be moved to a theory about ordered rings one day.

lemma (in int0) Int_ZF_1_2_L3A:

assumes A1: \( a\leq b \)

shows \( a - 1 \leq b \)proof
from A1 have \( b + 1 - 1 = b \) using Int_ZF_2_L1A, int_zero_one_are_int, Int_ZF_1_2_L3
moreover
from A1 have \( a - 1 \leq b + 1 - 1 \) using Int_ZF_2_L12A, int_zero_one_are_int, Int_ZF_1_1_L4, int_ord_transl_inv
ultimately show \( a - 1 \leq b \)
qed

Subtracting one does not increase integers, special case.

lemma (in int0) Int_ZF_1_2_L3AA:

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

shows \( a - 1 \leq a \), \( a - 1 \neq a \), \( \neg (a\leq a - 1 ) \), \( \neg (a + 1 \leq a) \), \( \neg (1 + a \leq a) \)proof
from A1 have \( a\leq a \) using int_ord_is_refl, refl_def
then show \( a - 1 \leq a \) using Int_ZF_1_2_L3A
moreover
from A1 show \( a - 1 \neq a \) using Int_ZF_1_L14
ultimately show I: \( \neg (a\leq a - 1 ) \) using Int_ZF_2_L19AA
with A1 show \( \neg (a + 1 \leq a) \) using int_zero_one_are_int, Int_ZF_2_L9B
with A1 show \( \neg (1 + a \leq a) \) using int_zero_one_are_int, Int_ZF_1_1_L5
qed

A formula with a nonpositive integer.

lemma (in int0) Int_ZF_1_2_L4:

assumes \( a\leq 0 \)

shows \( abs(a) + 1 = abs(a - 1 ) \) using assms, int_zero_one_are_int, Int_ZF_1_2_L3A, Int_ZF_2_T1, OrderedGroup_ZF_3_L3A, Int_ZF_2_L1A, int_zero_one_are_int, Int_ZF_1_1_L5

A formula with two integers, one negative.

lemma (in int0) Int_ZF_1_2_L5:

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

shows \( a + (abs(b) + 1 )\cdot a = (abs(b - 1 ) + 1 )\cdot a \)proof
from A2 have \( abs(b - 1 ) \in \mathbb{Z} \) using int_zero_one_are_int, Int_ZF_1_2_L3A, Int_ZF_2_L1A, Int_ZF_2_L14
with A1, A2 show \( thesis \) using Int_ZF_1_2_L4, Int_ZF_1_1_L2, Ring_ZF_2_L1
qed

A rearrangement with four integers.

lemma (in int0) Int_ZF_1_2_L6:

assumes A1: \( 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) \)proof
from A1 have T1: \( (d - b\cdot c) \in \mathbb{Z} \), \( d - a \in \mathbb{Z} \), \( ( - (b\cdot c)) \in \mathbb{Z} \) using Int_ZF_1_1_L5, Int_ZF_1_1_L4
with A1 have \( (d - b\cdot c) - (d - a - c) = ( - (b\cdot c)) + a + c \) using Int_ZF_1_1_L6, Int_ZF_1_2_L3
also
from A1, T1 have \( ( - (b\cdot c)) + a + c = a - (b - 1 )\cdot c \) using int_zero_one_are_int, Int_ZF_1_1_L6, Int_ZF_1_1_L4, Int_ZF_1_1_L5
finally show \( thesis \)
qed

Some other rearrangements with two integers.

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 \) using assms, Int_ZF_1_1_L1, Int_ZF_1_1_L5, int_zero_one_are_int, Int_ZF_1_1_L6, Int_ZF_1_1_L4, Int_ZF_1_T2, inv_cancel_two

Another rearrangement with two integers.

lemma (in int0) Int_ZF_1_2_L8:

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

shows \( a + 1 + (b + 1 ) = b + a + 2 \) using assms, int_zero_one_are_int, Int_ZF_1_T2, group0_4_L8

A couple of rearrangement with three integers.

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 \) using assms, Int_ZF_1_T2, group0_4_L4B, group0_4_L6D, group0_4_L4D, group0_4_L6B, group0_4_L6E

Another couple of rearrangements with three integers.

lemma (in int0) Int_ZF_1_2_L9A:

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

shows \( ( - (a - b - c)) = c + b - a \)proof
from A1 have T: \( a - b \in \mathbb{Z} \), \( ( - (a - b)) \in \mathbb{Z} \), \( ( - b) \in \mathbb{Z} \) using Int_ZF_1_1_L4, Int_ZF_1_1_L5
with A1 have \( ( - (a - b - c)) = c - (( - b) + a) \) using Int_ZF_1_1_L5
also
from A1, T have \( \ldots = c + b - a \) using Int_ZF_1_1_L6, Int_ZF_1_1_L5B
finally show \( ( - (a - b - c)) = c + b - a \)
qed

Another rearrangement with three integers.

lemma (in int0) Int_ZF_1_2_L10:

assumes A1: \( 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 \)proof
from A1 have \( a + 1 \in \mathbb{Z} \), \( c + 1 \in \mathbb{Z} \) using int_zero_one_are_int, Int_ZF_1_1_L5
with A1 have \( (a + 1 )\cdot b + (c + 1 )\cdot b = (a + 1 + (c + 1 ))\cdot b \) using Int_ZF_1_1_L1
also
from A1 have \( \ldots = (c + a + 2 )\cdot b \) using Int_ZF_1_2_L8
finally show \( thesis \)
qed

A technical rearrangement involing inequalities with absolute value.

lemma (in int0) Int_ZF_1_2_L10A:

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

shows \( abs(c - e) \leq f + d \)proof
from A1, A2 have T1: \( d\in \mathbb{Z} \), \( f\in \mathbb{Z} \), \( a\cdot b \in \mathbb{Z} \), \( a\cdot b - c \in \mathbb{Z} \), \( b\cdot a - e \in \mathbb{Z} \) using Int_ZF_2_L1A, Int_ZF_1_1_L5
with A2 have \( abs((b\cdot a - e) - (a\cdot b - c)) \leq f + d \) using Int_ZF_2_L21
with A1, T1 show \( abs(c - e) \leq f + d \) using Int_ZF_1_1_L5, Int_ZF_1_2_L9
qed

Some arithmetics.

lemma (in int0) Int_ZF_1_2_L11:

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

shows \( a + 1 + 2 = a + 3 \), \( a = 2 \cdot a - a \)proof
from A1 show \( a + 1 + 2 = a + 3 \) using int_zero_one_are_int, int_two_three_are_int, Int_ZF_1_T2, group0_4_L4C
from A1 show \( a = 2 \cdot a - a \) using int_zero_one_are_int, Int_ZF_1_1_L1, Int_ZF_1_1_L4, Int_ZF_1_T2, inv_cancel_two
qed

A simple rearrangement with three integers.

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 \) using assms, Int_ZF_1_1_L6, Int_ZF_1_1_L5

A big rearrangement with five integers.

lemma (in int0) Int_ZF_1_2_L13:

assumes A1: \( 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) \)proof
from A1 have T1: \( a\cdot x \in \mathbb{Z} \), \( (a + 1 )\cdot x \in \mathbb{Z} \), \( (a + 1 )\cdot x + b \in \mathbb{Z} \) using Int_ZF_1_1_L5, int_zero_one_are_int
with A1 have \( (x + (a\cdot x + b) + c)\cdot d = ((a + 1 )\cdot x + b)\cdot d + c\cdot d \) using Int_ZF_1_1_L7, Int_ZF_1_2_L7, Int_ZF_1_1_L1
also
from A1, T1 have \( \ldots = (a + 1 )\cdot x\cdot d + b \cdot d + c\cdot d \) using Int_ZF_1_1_L1
finally have \( (x + (a\cdot x + b) + c)\cdot d = (a + 1 )\cdot x\cdot d + b\cdot d + c\cdot d \)
moreover
from A1, T1 have \( (a + 1 )\cdot x\cdot d = d\cdot (a + 1 )\cdot x \) using int_zero_one_are_int, Int_ZF_1_1_L5, Int_ZF_1_1_L7
ultimately have \( (x + (a\cdot x + b) + c)\cdot d = d\cdot (a + 1 )\cdot x + b\cdot d + c\cdot d \)
moreover
from A1, T1 have \( d\cdot (a + 1 )\cdot x \in \mathbb{Z} \), \( b\cdot d \in \mathbb{Z} \), \( c\cdot d \in \mathbb{Z} \) using int_zero_one_are_int, Int_ZF_1_1_L5
ultimately show \( thesis \) using Int_ZF_1_1_L7
qed

Rerrangement about adding linear functions.

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) \) using assms, Int_ZF_1_1_L2, Ring_ZF_2_L3

A rearrangement with four integers. Again we have to use the generic set notation to use a theorem proven in different context.

lemma (in int0) Int_ZF_1_2_L15:

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

shows \( d = b - a - c \), \( d = ( - a) + b - c \), \( b = a + d + c \)proof
let \( G = int \)
let \( f = IntegerAddition \)
from A1, A2 have I: \( group0(G, f) \), \( f \text{ is commutative on } G \), \( a \in G \), \( b \in G \), \( c \in G \), \( d \in G \), \( a = f\langle f\langle b, \text{GroupInv}(G, f)(c)\rangle , \text{GroupInv}(G, f)(d)\rangle \) using Int_ZF_1_T2
then have \( d = f\langle f\langle b, \text{GroupInv}(G, f)(a)\rangle , \text{GroupInv}(G,f)(c)\rangle \) by (rule group0_4_L9 )
then show \( d = b - a - c \)
from I have \( d = f\langle f\langle \text{GroupInv}(G, f)(a),b\rangle , \text{GroupInv}(G, f)(c)\rangle \) by (rule group0_4_L9 )
thus \( d = ( - a) + b - c \)
from I have \( b = f\langle f\langle a, d\rangle ,c\rangle \) by (rule group0_4_L9 )
thus \( b = a + d + c \)
qed

A rearrangement with four integers. Property of groups.

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 \) using assms, Int_ZF_1_T2, group0_4_L8

Some rearrangements with three integers. Properties of groups.

lemma (in int0) Int_ZF_1_2_L17:

assumes A1: \( 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 \)proof
let \( G = int \)
let \( f = IntegerAddition \)
from A1 have I: \( group0(G, f) \), \( a \in G \), \( b \in G \), \( c \in G \) using Int_ZF_1_T2
then have \( f\langle f\langle f\langle a,b\rangle , \text{GroupInv}(G, f)(c)\rangle ,f\langle c, \text{GroupInv}(G, f)(b)\rangle \rangle = a \) by (rule group0_2_L14A )
thus \( a + b - c + (c - b) = a \)
from I have \( f\langle f\langle a,f\langle b,c\rangle \rangle , \text{GroupInv}(G, f)(c)\rangle = f\langle a,b\rangle \) by (rule group0_2_L14A )
thus \( a + (b + c) - c = a + b \)
qed

Another rearrangement with three integers. Property of abelian groups.

lemma (in int0) Int_ZF_1_2_L18:

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

shows \( a + b - c + (c - a) = b \)proof
let \( G = int \)
let \( f = IntegerAddition \)
from A1 have \( group0(G, f) \), \( f \text{ is commutative on } G \), \( a \in G \), \( b \in G \), \( c \in G \) using Int_ZF_1_T2
then have \( f\langle f\langle f\langle a,b\rangle , \text{GroupInv}(G, f)(c)\rangle ,f\langle c, \text{GroupInv}(G, f)(a)\rangle \rangle = b \) by (rule group0_4_L6D )
thus \( a + b - c + (c - a) = b \)
qed

Integers as an ordered ring

We already know from Int_ZF that integers with addition form a linearly ordered group. To show that integers form an ordered ring we need the fact that the set of nonnegative integers is closed under multiplication.

We start with the property that a product of nonnegative integers is nonnegative. The proof is by induction and the next lemma is the induction step.

lemma (in int0) Int_ZF_1_3_L1:

assumes A1: \( 0 \leq a \), \( 0 \leq b \) and A3: \( 0 \leq a\cdot b \)

shows \( 0 \leq a\cdot (b + 1 ) \)proof
from A1, A3 have \( 0 + 0 \leq a\cdot b + a \) using int_ineq_add_sides
with A1 show \( 0 \leq a\cdot (b + 1 ) \) using int_zero_one_are_int, Int_ZF_1_1_L4, Int_ZF_2_L1A, Int_ZF_1_2_L7
qed

Product of nonnegative integers is nonnegative.

lemma (in int0) Int_ZF_1_3_L2:

assumes A1: \( 0 \leq a \), \( 0 \leq b \)

shows \( 0 \leq a\cdot b \)proof
from A1 have \( 0 \leq b \)
moreover
from A1 have \( 0 \leq a\cdot 0 \) using Int_ZF_2_L1A, Int_ZF_1_1_L4, int_zero_one_are_int, int_ord_is_refl, refl_def
moreover
from A1 have \( \forall m.\ 0 \leq m \wedge 0 \leq a\cdot m \longrightarrow 0 \leq a\cdot (m + 1 ) \) using Int_ZF_1_3_L1
ultimately show \( 0 \leq a\cdot b \) by (rule Induction_on_int )
qed

The set of nonnegative integers is closed under multiplication.

lemma (in int0) Int_ZF_1_3_L2A:

shows \( \mathbb{Z} ^+ \text{ is closed under } IntegerMultiplication \)proof
{
fix \( a \) \( b \)
assume \( a\in \mathbb{Z} ^+ \), \( b\in \mathbb{Z} ^+ \)
then have \( a\cdot b \in \mathbb{Z} ^+ \) using Int_ZF_1_3_L2, Int_ZF_2_T1, OrderedGroup_ZF_1_L2
}
then have \( \forall a\in \mathbb{Z} ^+.\ \forall b\in \mathbb{Z} ^+.\ a\cdot b \in \mathbb{Z} ^+ \)
then show \( thesis \) using IsOpClosed_def
qed

Integers form an ordered ring. All theorems proven in the ring1 context are valid in int0 context.

theorem (in int0) Int_ZF_1_3_T1:

shows \( \text{IsAnOrdRing}(\mathbb{Z} ,IntegerAddition,IntegerMultiplication,IntegerOrder) \), \( ring1(\mathbb{Z} ,IntegerAddition,IntegerMultiplication,IntegerOrder) \) using Int_ZF_1_1_L2, Int_ZF_2_L1B, Int_ZF_1_3_L2A, Int_ZF_2_T1, OrdRing_ZF_1_L6, OrdRing_ZF_1_L2

Product of integers that are greater that one is greater than one. The proof is by induction and the next step is the induction step.

lemma (in int0) Int_ZF_1_3_L3_indstep:

assumes A1: \( 1 \leq a \), \( 1 \leq b \) and A2: \( 1 \leq a\cdot b \)

shows \( 1 \leq a\cdot (b + 1 ) \)proof
from A1, A2 have \( 1 \leq 2 \) and \( 2 \leq a\cdot (b + 1 ) \) using Int_ZF_2_L1A, int_ineq_add_sides, Int_ZF_2_L16B, Int_ZF_1_2_L7
then show \( 1 \leq a\cdot (b + 1 ) \) by (rule Int_order_transitive )
qed

Product of integers that are greater that one is greater than one.

lemma (in int0) Int_ZF_1_3_L3:

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

shows \( 1 \leq a\cdot b \)proof
from A1 have \( 1 \leq b \), \( 1 \leq a\cdot 1 \) using Int_ZF_2_L1A, Int_ZF_1_1_L4
moreover
from A1 have \( \forall m.\ 1 \leq m \wedge 1 \leq a\cdot m \longrightarrow 1 \leq a\cdot (m + 1 ) \) using Int_ZF_1_3_L3_indstep
ultimately show \( 1 \leq a\cdot b \) by (rule Induction_on_int )
qed

\(|a\cdot (-b)| = |(-a)\cdot b| = |(-a)\cdot (-b)| = |a\cdot b|\) This is a property of ordered rings..

lemma (in int0) Int_ZF_1_3_L4:

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

shows \( abs(( - a)\cdot b) = abs(a\cdot b) \), \( abs(a\cdot ( - b)) = abs(a\cdot b) \), \( abs(( - a)\cdot ( - b)) = abs(a\cdot b) \) using assms, Int_ZF_1_1_L5, Int_ZF_2_L17

Absolute value of a product is the product of absolute values. Property of ordered rings.

lemma (in int0) Int_ZF_1_3_L5:

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

shows \( abs(a\cdot b) = abs(a)\cdot abs(b) \) using assms, Int_ZF_1_3_T1, OrdRing_ZF_2_L5

Double nonnegative is nonnegative. Property of ordered rings.

lemma (in int0) Int_ZF_1_3_L5A:

assumes \( 0 \leq a \)

shows \( 0 \leq 2 \cdot a \) using assms, Int_ZF_1_3_T1, OrdRing_ZF_1_L5A

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

lemma (in int0) Int_ZF_1_3_L6:

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

shows \( \neg (b\leq a) \longleftrightarrow a + 1 \leq b \)proof
assume A3: \( \neg (b\leq a) \)
with A1 have \( a\leq b \) by (rule Int_ZF_2_L19 )
then have \( a = b \vee a + 1 \leq b \) using Int_ZF_4_L1B
moreover
from A1, A3 have \( a\neq b \) by (rule Int_ZF_2_L19 )
ultimately show \( a + 1 \leq b \)
next
assume A4: \( a + 1 \leq b \)
{
assume \( b\leq a \)
with A4 have \( a + 1 \leq a \) by (rule Int_order_transitive )
moreover
from A1 have \( a \leq a + 1 \) using Int_ZF_2_L12B
ultimately have \( a + 1 = a \) by (rule Int_ZF_2_L3 )
with A1 have \( False \) using Int_ZF_1_L14
}
then show \( \neg (b\leq a) \)
qed

Another form of stating that there are no integers between integers \(m\) and \(m+1\).

corollary (in int0) no_int_between:

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

shows \( b\leq a \vee a + 1 \leq b \) using A1, Int_ZF_1_3_L6

Another way of saying what it means that one integer is not greater or equal than another.

corollary (in int0) Int_ZF_1_3_L6A:

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

shows \( a \leq b - 1 \)proof
from A1, A2 have \( a + 1 - 1 \leq b - 1 \) using Int_ZF_1_3_L6, int_zero_one_are_int, Int_ZF_1_1_L4, int_ord_transl_inv
with A1 show \( a \leq b - 1 \) using int_zero_one_are_int, Int_ZF_1_2_L3
qed

Yet another form of stating that there are nointegers between \(m\) and \(m+1\).

lemma (in int0) no_int_between1:

assumes A1: \( a\leq b \) and A2: \( a\neq b \)

shows \( a + 1 \leq b \), \( a \leq b - 1 \)proof
from A1 have T: \( a\in \mathbb{Z} \), \( b\in \mathbb{Z} \) using Int_ZF_2_L1A
{
assume \( b\leq a \)
with A1 have \( a=b \) by (rule Int_ZF_2_L3 )
with A2 have \( False \)
}
then have \( \neg (b\leq a) \)
with T show \( a + 1 \leq b \), \( a \leq b - 1 \) using no_int_between, Int_ZF_1_3_L6A
qed

We can decompose proofs into three cases: \(a=b\), \(a\leq b-1b\) or \(a\geq b+1b\).

lemma (in int0) Int_ZF_1_3_L6B:

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

shows \( a=b \vee (a \leq b - 1 ) \vee (b + 1 \leq a) \)proof
from A1 have \( a=b \vee (a\leq b \wedge a\neq b) \vee (b\leq a \wedge b\neq a) \) using Int_ZF_2_T1, OrderedGroup_ZF_1_L31
then show \( thesis \) using no_int_between1
qed

A special case of Int_ZF_1_3_L6B when \(b=0\). This allows to split the proofs in cases \(a\leq -1\), \(a=0\) and \(a\geq 1\).

corollary (in int0) Int_ZF_1_3_L6C:

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

shows \( a= 0 \vee (a \leq - 1 ) \vee (1 \leq a) \)proof
from A1 have \( a= 0 \vee (a \leq 0 - 1 ) \vee ( 0 + 1 \leq a) \) using int_zero_one_are_int, Int_ZF_1_3_L6B
then show \( thesis \) using Int_ZF_1_1_L4, int_zero_one_are_int
qed

An integer is not less or equal zero iff it is greater or equal one.

lemma (in int0) Int_ZF_1_3_L7:

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

shows \( \neg (a\leq 0 ) \longleftrightarrow 1 \leq a \) using assms, int_zero_one_are_int, Int_ZF_1_3_L6, Int_ZF_1_1_L4

Product of positive integers is positive.

lemma (in int0) Int_ZF_1_3_L8:

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

shows \( \neg ((a\cdot b) \leq 0 ) \) using assms, Int_ZF_1_3_L7, Int_ZF_1_3_L3, Int_ZF_1_1_L5, Int_ZF_1_3_L7

If \(a\cdot b\) is nonnegative and \(b\) is positive, then \(a\) is nonnegative. Proof by contradiction.

lemma (in int0) Int_ZF_1_3_L9:

assumes A1: \( a\in \mathbb{Z} \), \( b\in \mathbb{Z} \) and A2: \( \neg (b\leq 0 ) \) and A3: \( a\cdot b \leq 0 \)

shows \( a\leq 0 \)proof
{
assume \( \neg (a\leq 0 ) \)
with A1, A2 have \( \neg ((a\cdot b) \leq 0 ) \) using Int_ZF_1_3_L8
}
with A3 show \( a\leq 0 \)
qed

One integer is less or equal another iff the difference is nonpositive.

lemma (in int0) Int_ZF_1_3_L10:

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

shows \( a\leq b \longleftrightarrow a - b \leq 0 \) using assms, Int_ZF_2_T1, OrderedGroup_ZF_1_L9

Some conclusions from the fact that one integer is less or equal than another.

lemma (in int0) Int_ZF_1_3_L10A:

assumes \( a\leq b \)

shows \( 0 \leq b - a \) using assms, Int_ZF_2_T1, OrderedGroup_ZF_1_L12A

We can simplify out a positive element on both sides of an inequality.

lemma (in int0) Int_ineq_simpl_positive:

assumes A1: \( a\in \mathbb{Z} \), \( b\in \mathbb{Z} \), \( c\in \mathbb{Z} \) and A2: \( a\cdot c \leq b\cdot c \) and A4: \( \neg (c\leq 0 ) \)

shows \( a \leq b \)proof
from A1, A4 have \( a - b \in \mathbb{Z} \), \( c\in \mathbb{Z} \), \( \neg (c\leq 0 ) \) using Int_ZF_1_1_L5
moreover
from A1, A2 have \( (a - b)\cdot c \leq 0 \) using Int_ZF_1_1_L5, Int_ZF_1_3_L10, Int_ZF_1_1_L6
ultimately have \( a - b \leq 0 \) by (rule Int_ZF_1_3_L9 )
with A1 show \( a \leq b \) using Int_ZF_1_3_L10
qed

A technical lemma about conclusion from an inequality between absolute values. This is a property of ordered rings.

lemma (in int0) Int_ZF_1_3_L11:

assumes A1: \( a\in \mathbb{Z} \), \( b\in \mathbb{Z} \) and A2: \( \neg (abs(a) \leq abs(b)) \)

shows \( \neg (abs(a) \leq 0 ) \)proof
{
assume \( abs(a) \leq 0 \)
moreover
from A1 have \( 0 \leq abs(a) \) using int_abs_nonneg
ultimately have \( abs(a) = 0 \) by (rule Int_ZF_2_L3 )
with A1, A2 have \( False \) using int_abs_nonneg
}
then show \( \neg (abs(a) \leq 0 ) \)
qed

Negative times positive is negative. This a property of ordered rings.

lemma (in int0) Int_ZF_1_3_L12:

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

shows \( a\cdot b \leq 0 \) using assms, Int_ZF_1_3_T1, OrdRing_ZF_1_L8

We can multiply an inequality by a nonnegative number. This is a property of ordered rings.

lemma (in int0) Int_ZF_1_3_L13:

assumes A1: \( a\leq b \) and A2: \( 0 \leq c \)

shows \( a\cdot c \leq b\cdot c \), \( c\cdot a \leq c\cdot b \) using assms, Int_ZF_1_3_T1, OrdRing_ZF_1_L9

A technical lemma about decreasing a factor in an inequality.

lemma (in int0) Int_ZF_1_3_L13A:

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

shows \( (a + 1 )\cdot b \leq d \)proof
from assms have \( (a + 1 )\cdot b \leq (a + 1 )\cdot c \), \( (a + 1 )\cdot c \leq d \) using Int_ZF_2_L16C, Int_ZF_1_3_L13
then show \( (a + 1 )\cdot b \leq d \) by (rule Int_order_transitive )
qed

We can multiply an inequality by a positive number. This is a property of ordered rings.

lemma (in int0) Int_ZF_1_3_L13B:

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

shows \( a\cdot c \leq b\cdot c \), \( c\cdot a \leq c\cdot b \)proof
let \( R = \mathbb{Z} \)
let \( A = IntegerAddition \)
let \( M = IntegerMultiplication \)
let \( r = IntegerOrder \)
from A1, A2 have \( ring1(R, A, M, r) \), \( \langle a,b\rangle \in r \), \( c \in \text{PositiveSet}(R, A, r) \) using Int_ZF_1_3_T1
then show \( a\cdot c \leq b\cdot c \), \( c\cdot a \leq c\cdot b \) using OrdRing_ZF_1_L9A
qed

A rearrangement with four integers and absolute value.

lemma (in int0) Int_ZF_1_3_L14:

assumes A1: \( 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 \)proof
from A1 have T1: \( abs(a) \in \mathbb{Z} \), \( abs(b) \in \mathbb{Z} \), \( abs(a)\cdot abs(b) \in \mathbb{Z} \), \( abs(a)\cdot d \in \mathbb{Z} \), \( c\cdot d \in \mathbb{Z} \), \( abs(b) + d \in \mathbb{Z} \) using Int_ZF_2_L14, Int_ZF_1_1_L5
with A1 have \( abs(a\cdot b) + (abs(a) + c)\cdot d = abs(a)\cdot (abs(b) + d) + c\cdot d \) using Int_ZF_1_3_L5, Int_ZF_1_1_L1, Int_ZF_1_1_L7
with A1, T1 show \( thesis \) using Int_ZF_1_1_L5
qed

A technical lemma about what happens when one absolute value is not greater or equal than another.

lemma (in int0) Int_ZF_1_3_L15:

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

shows \( n \leq abs(m) \), \( m\neq 0 \)proof
from A1 have T1: \( n \leq abs(n) \) using Int_ZF_2_L19C
from A1 have \( abs(n) \in \mathbb{Z} \), \( abs(m) \in \mathbb{Z} \) using Int_ZF_2_L14
moreover
note A2
ultimately have \( abs(n) \leq abs(m) \) by (rule Int_ZF_2_L19 )
with T1 show \( n \leq abs(m) \) by (rule Int_order_transitive )
from A1, A2 show \( m\neq 0 \) using Int_ZF_2_L18, int_abs_nonneg
qed

Negative of a nonnegative is nonpositive.

lemma (in int0) Int_ZF_1_3_L16:

assumes A1: \( 0 \leq m \)

shows \( ( - m) \leq 0 \)proof
from A1 have \( ( - m) \leq ( - 0 ) \) using Int_ZF_2_L10
then show \( ( - m) \leq 0 \) using Int_ZF_1_L11
qed

Some statements about intervals centered at \(0\).

lemma (in int0) Int_ZF_1_3_L17:

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

shows \( ( - abs(m)) \leq abs(m) \), \( ( - abs(m)).\ .\ abs(m) \neq 0 \)proof
from A1 have \( ( - abs(m)) \leq 0 \), \( 0 \leq abs(m) \) using int_abs_nonneg, Int_ZF_1_3_L16
then show \( ( - abs(m)) \leq abs(m) \) by (rule Int_order_transitive )
then have \( abs(m) \in ( - abs(m)).\ .\ abs(m) \) using int_ord_is_refl, Int_ZF_2_L1A, Order_ZF_2_L2
thus \( ( - abs(m)).\ .\ abs(m) \neq 0 \)
qed

The greater of two integers is indeed greater than both, and the smaller one is smaller that both.

lemma (in int0) Int_ZF_1_3_L18:

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

shows \( m \leq \text{GreaterOf}(IntegerOrder,m,n) \), \( n \leq \text{GreaterOf}(IntegerOrder,m,n) \), \( \text{SmallerOf}(IntegerOrder,m,n) \leq m \), \( \text{SmallerOf}(IntegerOrder,m,n) \leq n \) using assms, Int_ZF_2_T1, Order_ZF_3_L2

If \(|m| \leq n\), then \(m \in -n..n\).

lemma (in int0) Int_ZF_1_3_L19:

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

shows \( ( - n) \leq m \), \( m \leq n \), \( m \in ( - n).\ .\ n \), \( 0 \leq n \) using assms, Int_ZF_2_T1, OrderedGroup_ZF_3_L8, OrderedGroup_ZF_3_L8A, Order_ZF_2_L1

A slight generalization of the above lemma.

lemma (in int0) Int_ZF_1_3_L19A:

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

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

Sets of integers that have absolute value bounded are bounded.

lemma (in int0) Int_ZF_1_3_L20:

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

shows \( \text{IsBounded}(\{b(x).\ x\in X\},IntegerOrder) \)proof
let \( G = \mathbb{Z} \)
let \( P = IntegerAddition \)
let \( r = IntegerOrder \)
from A1 have \( group3(G, P, r) \), \( r \text{ is total on } G \), \( \forall x\in X.\ b(x) \in G \wedge \langle \text{AbsoluteValue}(G, P, r) b(x), L\rangle \in r \) using Int_ZF_2_T1
then show \( \text{IsBounded}(\{b(x).\ x\in X\},IntegerOrder) \) by (rule OrderedGroup_ZF_3_L9A )
qed

If a set is bounded, then the absolute values of the elements of that set are bounded.

lemma (in int0) Int_ZF_1_3_L20A:

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

shows \( \exists L.\ \forall a\in A.\ abs(a) \leq L \) using assms, Int_ZF_2_T1, OrderedGroup_ZF_3_L10A

Absolute vaues of integers from a finite image of integers are bounded by an integer.

lemma (in int0) Int_ZF_1_3_L20AA:

assumes A1: \( \{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 \) using assms, int_not_empty, Int_ZF_2_T1, OrderedGroup_ZF_3_L11A

If absolute values of values of some integer function are bounded, then the image a set from the domain is a bounded set.

lemma (in int0) Int_ZF_1_3_L20B:

assumes \( f:X\rightarrow \mathbb{Z} \) and \( A\subseteq X \) and \( \forall x\in A.\ abs(f(x)) \leq L \)

shows \( \text{IsBounded}(f(A),IntegerOrder) \)proof
let \( G = \mathbb{Z} \)
let \( P = IntegerAddition \)
let \( r = IntegerOrder \)
from assms have \( group3(G, P, r) \), \( r \text{ is total on } G \), \( f:X\rightarrow G \), \( A\subseteq X \), \( \forall x\in A.\ \langle \text{AbsoluteValue}(G, P, r)(f(x)), L\rangle \in r \) using Int_ZF_2_T1
then show \( \text{IsBounded}(f(A), r) \) by (rule OrderedGroup_ZF_3_L9B )
qed

A special case of the previous lemma for a function from integers to integers.

corollary (in int0) Int_ZF_1_3_L20C:

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

shows \( f(\mathbb{Z} ) \in Fin(\mathbb{Z} ) \)proof
from assms have \( f:\mathbb{Z} \rightarrow \mathbb{Z} \), \( \mathbb{Z} \subseteq \mathbb{Z} \), \( \forall m\in \mathbb{Z} .\ abs(f(m)) \leq L \)
then have \( \text{IsBounded}(f(\mathbb{Z} ),IntegerOrder) \) by (rule Int_ZF_1_3_L20B )
then show \( f(\mathbb{Z} ) \in Fin(\mathbb{Z} ) \) using Int_bounded_iff_fin
qed

A triangle inequality with three integers. Property of linearly ordered abelian groups.

lemma (in int0) int_triangle_ineq3:

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

shows \( abs(a - b - c) \leq abs(a) + abs(b) + abs(c) \)proof
from A1 have T: \( a - b \in \mathbb{Z} \), \( abs(c) \in \mathbb{Z} \) using Int_ZF_1_1_L5, Int_ZF_2_L14
with A1 have \( abs(a - b - c) \leq abs(a - b) + abs(c) \) using Int_triangle_ineq1
moreover
from A1, T have \( abs(a - b) + abs(c) \leq abs(a) + abs(b) + abs(c) \) using Int_triangle_ineq1, int_ord_transl_inv
ultimately show \( thesis \) by (rule Int_order_transitive )
qed

If \(a\leq c\) and \(b\leq c\), then \(a+b\leq 2\cdot c\). Property of ordered rings.

lemma (in int0) Int_ZF_1_3_L21:

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

shows \( a + b \leq 2 \cdot c \) using assms, Int_ZF_1_3_T1, OrdRing_ZF_2_L6

If an integer \(a\) is between \(b\) and \(b+c\), then \(|b-a| \leq c\). Property of ordered groups.

lemma (in int0) Int_ZF_1_3_L22:

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

shows \( abs(b - a) \leq c \) using assms, Int_ZF_2_T1, OrderedGroup_ZF_3_L8C

An application of the triangle inequality with four integers. Property of linearly ordered abelian groups.

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

If an integer \(a\) is between \(b\) and \(b+c\), then \(|b-a| \leq c\). Property of ordered groups. A version of Int_ZF_1_3_L22 with sligtly different assumptions.

lemma (in int0) Int_ZF_1_3_L23:

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

shows \( abs(b - a) \leq c \)proof
from A1 have \( a \in \mathbb{Z} \) using Int_ZF_2_L1A
with A2, A3 have \( b\leq c + a \) using Int_ZF_1_1_L5
with A1, A2 show \( abs(b - a) \leq c \) using Int_ZF_1_3_L22
qed

Maximum and minimum of a set of integers

In this section we provide some sufficient conditions for integer subsets to have extrema (maxima and minima).

Finite nonempty subsets of integers attain maxima and minima.

theorem (in int0) Int_fin_have_max_min:

assumes A1: \( A \in Fin(\mathbb{Z} ) \) and A2: \( A\neq 0 \)

shows \( \text{HasAmaximum}(IntegerOrder,A) \), \( \text{HasAminimum}(IntegerOrder,A) \), \( \text{Maximum}(IntegerOrder,A) \in A \), \( \text{Minimum}(IntegerOrder,A) \in A \), \( \forall x\in A.\ x \leq \text{Maximum}(IntegerOrder,A) \), \( \forall x\in A.\ \text{Minimum}(IntegerOrder,A) \leq x \), \( \text{Maximum}(IntegerOrder,A) \in \mathbb{Z} \), \( \text{Minimum}(IntegerOrder,A) \in \mathbb{Z} \)proof
from A1 have \( A=0 \vee \text{HasAmaximum}(IntegerOrder,A) \) and \( A=0 \vee \text{HasAminimum}(IntegerOrder,A) \) using Int_ZF_2_T1, Int_ZF_2_L6, Finite_ZF_1_1_T1A, Finite_ZF_1_1_T1B
with A2 show \( \text{HasAmaximum}(IntegerOrder,A) \), \( \text{HasAminimum}(IntegerOrder,A) \)
from A1, A2 show \( \text{Maximum}(IntegerOrder,A) \in A \), \( \text{Minimum}(IntegerOrder,A) \in A \), \( \forall x\in A.\ x \leq \text{Maximum}(IntegerOrder,A) \), \( \forall x\in A.\ \text{Minimum}(IntegerOrder,A) \leq x \) using Int_ZF_2_T1, Finite_ZF_1_T2
moreover
from A1 have \( A\subseteq \mathbb{Z} \) using FinD
ultimately show \( \text{Maximum}(IntegerOrder,A) \in \mathbb{Z} \), \( \text{Minimum}(IntegerOrder,A) \in \mathbb{Z} \)
qed

Bounded nonempty integer subsets attain maximum and minimum.

theorem (in int0) Int_bounded_have_max_min:

assumes \( \text{IsBounded}(A,IntegerOrder) \) and \( A\neq 0 \)

shows \( \text{HasAmaximum}(IntegerOrder,A) \), \( \text{HasAminimum}(IntegerOrder,A) \), \( \text{Maximum}(IntegerOrder,A) \in A \), \( \text{Minimum}(IntegerOrder,A) \in A \), \( \forall x\in A.\ x \leq \text{Maximum}(IntegerOrder,A) \), \( \forall x\in A.\ \text{Minimum}(IntegerOrder,A) \leq x \), \( \text{Maximum}(IntegerOrder,A) \in \mathbb{Z} \), \( \text{Minimum}(IntegerOrder,A) \in \mathbb{Z} \) using assms, Int_fin_have_max_min, Int_bounded_iff_fin

Nonempty set of integers that is bounded below attains its minimum.

theorem (in int0) int_bounded_below_has_min:

assumes A1: \( \text{IsBoundedBelow}(A,IntegerOrder) \) and A2: \( A\neq 0 \)

shows \( \) \( \text{HasAminimum}(IntegerOrder,A) \), \( \text{Minimum}(IntegerOrder,A) \in A \), \( \forall x\in A.\ \text{Minimum}(IntegerOrder,A) \leq x \)proof
from A1, A2 have \( IntegerOrder \text{ is total on } \mathbb{Z} \), \( \text{trans}(IntegerOrder) \), \( IntegerOrder \subseteq \mathbb{Z} \times \mathbb{Z} \), \( \forall A.\ \text{IsBounded}(A,IntegerOrder) \wedge A\neq 0 \longrightarrow \text{HasAminimum}(IntegerOrder,A) \), \( A\neq 0 \), \( \text{IsBoundedBelow}(A,IntegerOrder) \) using Int_ZF_2_T1, Int_ZF_2_L6, Int_ZF_2_L1B, Int_bounded_have_max_min
then show \( \text{HasAminimum}(IntegerOrder,A) \) by (rule Order_ZF_4_L11 )
then show \( \text{Minimum}(IntegerOrder,A) \in A \), \( \forall x\in A.\ \text{Minimum}(IntegerOrder,A) \leq x \) using Int_ZF_2_L4, Order_ZF_4_L4
qed

Nonempty set of integers that is bounded above attains its maximum.

theorem (in int0) int_bounded_above_has_max:

assumes A1: \( \text{IsBoundedAbove}(A,IntegerOrder) \) and A2: \( A\neq 0 \)

shows \( \text{HasAmaximum}(IntegerOrder,A) \), \( \text{Maximum}(IntegerOrder,A) \in A \), \( \text{Maximum}(IntegerOrder,A) \in \mathbb{Z} \), \( \forall x\in A.\ x \leq \text{Maximum}(IntegerOrder,A) \)proof
from A1, A2 have \( IntegerOrder \text{ is total on } \mathbb{Z} \), \( \text{trans}(IntegerOrder) \) and I: \( IntegerOrder \subseteq \mathbb{Z} \times \mathbb{Z} \) and \( \forall A.\ \text{IsBounded}(A,IntegerOrder) \wedge A\neq 0 \longrightarrow \text{HasAmaximum}(IntegerOrder,A) \), \( A\neq 0 \), \( \text{IsBoundedAbove}(A,IntegerOrder) \) using Int_ZF_2_T1, Int_ZF_2_L6, Int_ZF_2_L1B, Int_bounded_have_max_min
then show \( \text{HasAmaximum}(IntegerOrder,A) \) by (rule Order_ZF_4_L11A )
then show II: \( \text{Maximum}(IntegerOrder,A) \in A \) and \( \forall x\in A.\ x \leq \text{Maximum}(IntegerOrder,A) \) using Int_ZF_2_L4, Order_ZF_4_L3
from I, A1 have \( A \subseteq \mathbb{Z} \) by (rule Order_ZF_3_L1A )
with II show \( \text{Maximum}(IntegerOrder,A) \in \mathbb{Z} \)
qed

A set defined by separation over a bounded set attains its maximum and minimum.

lemma (in int0) Int_ZF_1_4_L1:

assumes A1: \( \text{IsBounded}(A,IntegerOrder) \) and A2: \( A\neq 0 \) and A3: \( \forall q\in \mathbb{Z} .\ F(q) \in \mathbb{Z} \) and A4: \( K = \{F(q).\ q \in A\} \)

shows \( \text{HasAmaximum}(IntegerOrder,K) \), \( \text{HasAminimum}(IntegerOrder,K) \), \( \text{Maximum}(IntegerOrder,K) \in K \), \( \text{Minimum}(IntegerOrder,K) \in K \), \( \text{Maximum}(IntegerOrder,K) \in \mathbb{Z} \), \( \text{Minimum}(IntegerOrder,K) \in \mathbb{Z} \), \( \forall q\in A.\ F(q) \leq \text{Maximum}(IntegerOrder,K) \), \( \forall q\in A.\ \text{Minimum}(IntegerOrder,K) \leq F(q) \), \( \text{IsBounded}(K,IntegerOrder) \)proof
from A1 have \( A \in Fin(\mathbb{Z} ) \) using Int_bounded_iff_fin
with A3 have \( \{F(q).\ q \in A\} \in Fin(\mathbb{Z} ) \) by (rule fin_image_fin )
with A2, A4 have T1: \( K \in Fin(\mathbb{Z} ) \), \( K\neq 0 \)
then show T2: \( \text{HasAmaximum}(IntegerOrder,K) \), \( \text{HasAminimum}(IntegerOrder,K) \) and \( \text{Maximum}(IntegerOrder,K) \in K \), \( \text{Minimum}(IntegerOrder,K) \in K \), \( \text{Maximum}(IntegerOrder,K) \in \mathbb{Z} \), \( \text{Minimum}(IntegerOrder,K) \in \mathbb{Z} \) using Int_fin_have_max_min
{
fix \( q \)
assume \( q\in A \)
with A4 have \( F(q) \in K \)
with T1 have \( F(q) \leq \text{Maximum}(IntegerOrder,K) \), \( \text{Minimum}(IntegerOrder,K) \leq F(q) \) using Int_fin_have_max_min
}
then show \( \forall q\in A.\ F(q) \leq \text{Maximum}(IntegerOrder,K) \), \( \forall q\in A.\ \text{Minimum}(IntegerOrder,K) \leq F(q) \)
from T2 show \( \text{IsBounded}(K,IntegerOrder) \) using Order_ZF_4_L7, Order_ZF_4_L8A, IsBounded_def
qed

A three element set has a maximume and minimum.

lemma (in int0) Int_ZF_1_4_L1A:

assumes A1: \( 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\}) \) using assms, Int_ZF_2_T1, Finite_ZF_1_L2A

Integer functions attain maxima and minima over intervals.

lemma (in int0) Int_ZF_1_4_L2:

assumes A1: \( f:\mathbb{Z} \rightarrow \mathbb{Z} \) and A2: \( 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) \)proof
from A2 have T: \( a\in \mathbb{Z} \), \( b\in \mathbb{Z} \), \( a.\ .\ b \subseteq \mathbb{Z} \) using Int_ZF_2_L1A, Int_ZF_2_L1B, Order_ZF_2_L6
with A1, A2 have \( \text{Maximum}(IntegerOrder,f(a.\ .\ b)) \in f(a.\ .\ b) \), \( \forall x\in f(a.\ .\ b).\ x \leq \text{Maximum}(IntegerOrder,f(a.\ .\ b)) \), \( \text{Maximum}(IntegerOrder,f(a.\ .\ b)) \in \mathbb{Z} \), \( \text{Minimum}(IntegerOrder,f(a.\ .\ b)) \in f(a.\ .\ b) \), \( \forall x\in f(a.\ .\ b).\ \text{Minimum}(IntegerOrder,f(a.\ .\ b)) \leq x \), \( \text{Minimum}(IntegerOrder,f(a.\ .\ b)) \in \mathbb{Z} \) using Int_ZF_4_L8, Int_ZF_2_T1, OrderedGroup_ZF_2_L6, Int_fin_have_max_min
with A1, T show \( 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) \) using func_imagedef
qed

The set of nonnegative integers

The set of nonnegative integers looks like the set of natural numbers. We explore that in this section. We also rephrase some lemmas about the set of positive integers known from the theory of ordered groups.

The set of positive integers is closed under addition.

lemma (in int0) pos_int_closed_add:

shows \( \mathbb{Z} _+ \text{ is closed under } IntegerAddition \) using Int_ZF_2_T1, OrderedGroup_ZF_1_L13

Text expended version of the fact that the set of positive integers is closed under addition

lemma (in int0) pos_int_closed_add_unfolded:

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

shows \( a + b \in \mathbb{Z} _+ \) using assms, pos_int_closed_add, IsOpClosed_def

\( \mathbb{Z} ^+ \) is bounded below.

lemma (in int0) Int_ZF_1_5_L1:

shows \( \text{IsBoundedBelow}(\mathbb{Z} ^+,IntegerOrder) \), \( \text{IsBoundedBelow}(\mathbb{Z} _+,IntegerOrder) \) using Nonnegative_def, PositiveSet_def, IsBoundedBelow_def

Subsets of \( \mathbb{Z} ^+ \) are bounded below.

lemma (in int0) Int_ZF_1_5_L1A:

assumes \( A \subseteq \mathbb{Z} ^+ \)

shows \( \text{IsBoundedBelow}(A,IntegerOrder) \) using assms, Int_ZF_1_5_L1, Order_ZF_3_L12

Subsets of \( \mathbb{Z} _+ \) are bounded below.

lemma (in int0) Int_ZF_1_5_L1B:

assumes A1: \( A \subseteq \mathbb{Z} _+ \)

shows \( \text{IsBoundedBelow}(A,IntegerOrder) \) using A1, Int_ZF_1_5_L1, Order_ZF_3_L12

Every nonempty subset of positive integers has a mimimum.

lemma (in int0) Int_ZF_1_5_L1C:

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

shows \( \text{HasAminimum}(IntegerOrder,A) \), \( \text{Minimum}(IntegerOrder,A) \in A \), \( \forall x\in A.\ \text{Minimum}(IntegerOrder,A) \leq x \) using assms, Int_ZF_1_5_L1B, int_bounded_below_has_min

Infinite subsets of \(Z^+\) do not have a maximum - If \(A\subseteq Z^+\) then for every integer we can find one in the set that is not smaller.

lemma (in int0) Int_ZF_1_5_L2:

assumes A1: \( A \subseteq \mathbb{Z} ^+ \) and A2: \( A \notin Fin(\mathbb{Z} ) \) and A3: \( D\in \mathbb{Z} \)

shows \( \exists n\in A.\ D\leq n \)proof
{
assume \( \forall n\in A.\ \neg (D\leq n) \)
moreover
from A1, A3 have \( D\in \mathbb{Z} \), \( \forall n\in A.\ n\in \mathbb{Z} \) using Nonnegative_def
ultimately have \( \forall n\in A.\ n\leq D \) using Int_ZF_2_L19
hence \( \forall n\in A.\ \langle n,D\rangle \in IntegerOrder \)
then have \( \text{IsBoundedAbove}(A,IntegerOrder) \) by (rule Order_ZF_3_L10 )
with A1 have \( \text{IsBounded}(A,IntegerOrder) \) using Int_ZF_1_5_L1A, IsBounded_def
with A2 have \( False \) using Int_bounded_iff_fin
}
thus \( thesis \)
qed

Infinite subsets of \(Z_+\) do not have a maximum - If \(A\subseteq Z_+\) then for every integer we can find one in the set that is not smaller. This is very similar to Int_ZF_1_5_L2, except we have \( \mathbb{Z} _+ \) instead of \( \mathbb{Z} ^+ \) here.

lemma (in int0) Int_ZF_1_5_L2A:

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

shows \( \exists n\in A.\ D\leq n \)proof
{
assume \( \forall n\in A.\ \neg (D\leq n) \)
moreover
from A1, A3 have \( D\in \mathbb{Z} \), \( \forall n\in A.\ n\in \mathbb{Z} \) using PositiveSet_def
ultimately have \( \forall n\in A.\ n\leq D \) using Int_ZF_2_L19
hence \( \forall n\in A.\ \langle n,D\rangle \in IntegerOrder \)
then have \( \text{IsBoundedAbove}(A,IntegerOrder) \) by (rule Order_ZF_3_L10 )
with A1 have \( \text{IsBounded}(A,IntegerOrder) \) using Int_ZF_1_5_L1B, IsBounded_def
with A2 have \( False \) using Int_bounded_iff_fin
}
thus \( thesis \)
qed

An integer is either positive, zero, or its opposite is postitive.

lemma (in int0) Int_decomp:

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

shows \( \text{Exactly_1_of_3_holds} (m= 0 ,m\in \mathbb{Z} _+,( - m)\in \mathbb{Z} _+) \) using assms, Int_ZF_2_T1, OrdGroup_decomp

An integer is zero, positive, or it's inverse is positive.

lemma (in int0) int_decomp_cases:

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

shows \( m= 0 \vee m\in \mathbb{Z} _+ \vee ( - m) \in \mathbb{Z} _+ \) using assms, Int_ZF_2_T1, OrderedGroup_ZF_1_L14

An integer is in the positive set iff it is greater or equal one.

lemma (in int0) Int_ZF_1_5_L3:

shows \( m\in \mathbb{Z} _+ \longleftrightarrow 1 \leq m \)proof
assume \( m\in \mathbb{Z} _+ \)
then have \( 0 \leq m \), \( m\neq 0 \) using PositiveSet_def
then have \( 0 + 1 \leq m \) using Int_ZF_4_L1B
then show \( 1 \leq m \) using int_zero_one_are_int, Int_ZF_1_T2, group0_2_L2
next
assume \( 1 \leq m \)
then have \( m\in \mathbb{Z} \), \( 0 \leq m \), \( m\neq 0 \) using Int_ZF_2_L1A, Int_ZF_2_L16C
then show \( m\in \mathbb{Z} _+ \) using PositiveSet_def
qed

The set of positive integers is closed under multiplication. The unfolded form.

lemma (in int0) pos_int_closed_mul_unfold:

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

shows \( a\cdot b \in \mathbb{Z} _+ \) using assms, Int_ZF_1_5_L3, Int_ZF_1_3_L3

The set of positive integers is closed under multiplication.

lemma (in int0) pos_int_closed_mul:

shows \( \mathbb{Z} _+ \text{ is closed under } IntegerMultiplication \) using pos_int_closed_mul_unfold, IsOpClosed_def

It is an overkill to prove that the ring of integers has no zero divisors this way, but why not?

lemma (in int0) int_has_no_zero_divs:

shows \( \text{HasNoZeroDivs}(\mathbb{Z} ,IntegerAddition,IntegerMultiplication) \) using pos_int_closed_mul, Int_ZF_1_3_T1, OrdRing_ZF_3_L3

Nonnegative integers are positive ones plus zero.

lemma (in int0) Int_ZF_1_5_L3A:

shows \( \mathbb{Z} ^+ = \mathbb{Z} _+ \cup \{ 0 \} \) using Int_ZF_2_T1, OrderedGroup_ZF_1_L24

We can make a function smaller than any constant on a given interval of positive integers by adding another constant.

lemma (in int0) Int_ZF_1_5_L4:

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

shows \( \exists C\in \mathbb{Z} .\ \forall n\in \mathbb{Z} _+.\ K \leq f(n) + C \longrightarrow N\leq n \)proof
from A2 have \( N\leq 1 \vee 2 \leq N \) using int_zero_one_are_int, no_int_between
moreover {
assume A3: \( N\leq 1 \)
let \( C = 0 \)
have \( C \in \mathbb{Z} \) using int_zero_one_are_int
moreover {
fix \( n \)
assume \( n\in \mathbb{Z} _+ \)
then have \( 1 \leq n \) using Int_ZF_1_5_L3
with A3 have \( N\leq n \) by (rule Int_order_transitive )
}
then have \( \forall n\in \mathbb{Z} _+.\ K \leq f(n) + C \longrightarrow N\leq n \)
ultimately have \( \exists C\in \mathbb{Z} .\ \forall n\in \mathbb{Z} _+.\ K \leq f(n) + C \longrightarrow N\leq n \)
} moreover {
let \( C = K - 1 - maxf(f,1 .\ .\ (N - 1 )) \)
assume \( 2 \leq N \)
then have \( 2 - 1 \leq N - 1 \) using int_zero_one_are_int, Int_ZF_1_1_L4, int_ord_transl_inv
then have I: \( 1 \leq N - 1 \) using int_zero_one_are_int, Int_ZF_1_2_L3
with A1, A2 have T: \( maxf(f,1 .\ .\ (N - 1 )) \in \mathbb{Z} \), \( K - 1 \in \mathbb{Z} \), \( C \in \mathbb{Z} \) using Int_ZF_1_4_L2, Int_ZF_1_1_L5, int_zero_one_are_int
moreover {
fix \( n \)
assume A4: \( n\in \mathbb{Z} _+ \)
{
assume A5: \( K \leq f(n) + C \) and \( \neg (N\leq n) \)
with A2, A4 have \( n \leq N - 1 \) using PositiveSet_def, Int_ZF_1_3_L6A
with A4 have \( n \in 1 .\ .\ (N - 1 ) \) using Int_ZF_1_5_L3, Interval_def
with A1, I, T have \( f(n) + C \leq maxf(f,1 .\ .\ (N - 1 )) + C \) using Int_ZF_1_4_L2, int_ord_transl_inv
with T have \( f(n) + C \leq K - 1 \) using Int_ZF_1_2_L3
with A5 have \( K \leq K - 1 \) by (rule Int_order_transitive )
with A2 have \( False \) using Int_ZF_1_2_L3AA
}
then have \( K \leq f(n) + C \longrightarrow N\leq n \)
}
then have \( \forall n\in \mathbb{Z} _+.\ K \leq f(n) + C \longrightarrow N\leq n \)
ultimately have \( \exists C\in \mathbb{Z} .\ \forall n\in \mathbb{Z} _+.\ K \leq f(n) + C \longrightarrow N\leq n \)
} ultimately show \( thesis \)
qed

Absolute value is identity on positive integers.

lemma (in int0) Int_ZF_1_5_L4A:

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

shows \( abs(a) = a \) using assms, Int_ZF_2_T1, OrderedGroup_ZF_3_L2B

One and two are in \( \mathbb{Z} _+ \).

lemma (in int0) int_one_two_are_pos:

shows \( 1 \in \mathbb{Z} _+ \), \( 2 \in \mathbb{Z} _+ \) using int_zero_one_are_int, int_ord_is_refl, refl_def, Int_ZF_1_5_L3, Int_ZF_2_L16B

The image of \( \mathbb{Z} _+ \) by a function defined on integers is not empty.

lemma (in int0) Int_ZF_1_5_L5:

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

shows \( f(\mathbb{Z} _+) \neq 0 \)proof
have \( \mathbb{Z} _+ \subseteq \mathbb{Z} \) using PositiveSet_def
with A1 show \( f(\mathbb{Z} _+) \neq 0 \) using int_one_two_are_pos, func_imagedef
qed

If \(n\) is positive, then \(n-1\) is nonnegative.

lemma (in int0) Int_ZF_1_5_L6:

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

shows \( 0 \leq n - 1 \), \( 0 \in 0 .\ .\ (n - 1 ) \), \( 0 .\ .\ (n - 1 ) \subseteq \mathbb{Z} \)proof
from A1 have \( 1 \leq n \), \( ( - 1 ) \in \mathbb{Z} \) using Int_ZF_1_5_L3, int_zero_one_are_int, Int_ZF_1_1_L4
then have \( 1 - 1 \leq n - 1 \) using int_ord_transl_inv
then show \( 0 \leq n - 1 \) using int_zero_one_are_int, Int_ZF_1_1_L4
then show \( 0 \in 0 .\ .\ (n - 1 ) \) using int_zero_one_are_int, int_ord_is_refl, refl_def, Order_ZF_2_L1B
show \( 0 .\ .\ (n - 1 ) \subseteq \mathbb{Z} \) using Int_ZF_2_L1B, Order_ZF_2_L6
qed

Intgers greater than one in \( \mathbb{Z} _+ \) belong to \( \mathbb{Z} _+ \). This is a property of ordered groups and follows from OrderedGroup_ZF_1_L19, but Isabelle's simplifier has problems using that result directly, so we reprove it specifically for integers.

lemma (in int0) Int_ZF_1_5_L7:

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

shows \( b \in \mathbb{Z} _+ \)proof
from assms have \( 1 \leq a \), \( a\leq b \) using Int_ZF_1_5_L3
then have \( 1 \leq b \) by (rule Int_order_transitive )
then show \( b \in \mathbb{Z} _+ \) using Int_ZF_1_5_L3
qed

Adding a positive integer increases integers.

lemma (in int0) Int_ZF_1_5_L7A:

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

shows \( a \leq a + b \), \( a \neq a + b \), \( a + b \in \mathbb{Z} \) using assms, Int_ZF_2_T1, OrderedGroup_ZF_1_L22

For any integer \(m\) the greater of \(m\) and \(1\) is a positive integer that is greater or equal than \(m\). If we add \(1\) to it we get a positive integer that is strictly greater than \(m\).

lemma (in int0) Int_ZF_1_5_L7B:

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

shows \( a \leq \text{GreaterOf}(IntegerOrder,1 ,a) \), \( \text{GreaterOf}(IntegerOrder,1 ,a) \in \mathbb{Z} _+ \), \( \text{GreaterOf}(IntegerOrder,1 ,a) + 1 \in \mathbb{Z} _+ \), \( a \leq \text{GreaterOf}(IntegerOrder,1 ,a) + 1 \), \( a \neq \text{GreaterOf}(IntegerOrder,1 ,a) + 1 \) using assms, int_zero_not_one, Int_ZF_1_3_T1, OrdRing_ZF_3_L12

The opposite of an element of \( \mathbb{Z} _+ \) cannot belong to \( \mathbb{Z} _+ \).

lemma (in int0) Int_ZF_1_5_L8:

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

shows \( ( - a) \notin \mathbb{Z} _+ \) using assms, Int_ZF_2_T1, OrderedGroup_ZF_1_L20

For every integer there is one in \( \mathbb{Z} _+ \) that is greater or equal.

lemma (in int0) Int_ZF_1_5_L9:

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

shows \( \exists b\in \mathbb{Z} _+.\ a\leq b \) using assms, int_not_trivial, Int_ZF_2_T1, OrderedGroup_ZF_1_L23

A theorem about odd extensions. Recall from OrdereGroup_ZF.thy that the odd extension of an integer function \(f\) defined on \( \mathbb{Z} _+ \) is the odd function on \( \mathbb{Z} \) equal to \(f\) on \( \mathbb{Z} _+ \). First we show that the odd extension is defined on \( \mathbb{Z} \).

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

On \( \mathbb{Z} _+ \), the odd extension of \(f\) is the same as \(f\).

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

On \( -\mathbb{Z} _+ \), the value of the odd extension of \(f\) is the negative of \(f(-a)\).

lemma (in int0) Int_ZF_1_5_L12:

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

Odd extensions are odd on \( \mathbb{Z} \).

lemma (in int0) int_oddext_is_odd:

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

Alternative definition of an odd function.

lemma (in int0) Int_ZF_1_5_L13:

assumes A1: \( 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)) \) using assms, Int_ZF_1_T2, group0_6_L2

Another way of expressing the fact that odd extensions are odd.

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

Functions with infinite limits

In this section we consider functions (integer sequences) that have infinite limits. An integer function has infinite positive limit if it is arbitrarily large for large enough arguments. Similarly, a function has infinite negative limit if it is arbitrarily small for small enough arguments. The material in this come mostly from the section in OrderedGroup_ZF.thy with he same title. Here we rewrite the theorems from that section in the notation we use for integers and add some results specific for the ordered group of integers.

If an image of a set by a function with infinite positive limit is bounded above, then the set itself is bounded above.

lemma (in int0) Int_ZF_1_6_L1:

assumes \( f: \mathbb{Z} \rightarrow \mathbb{Z} \) and \( \forall a\in \mathbb{Z} .\ \exists b\in \mathbb{Z} _+.\ \forall x.\ b\leq x \longrightarrow a \leq f(x) \) and \( A \subseteq \mathbb{Z} \) and \( \text{IsBoundedAbove}(f(A),IntegerOrder) \)

shows \( \text{IsBoundedAbove}(A,IntegerOrder) \) using assms, int_not_trivial, Int_ZF_2_T1, OrderedGroup_ZF_7_L1

If an image of a set defined by separation by a function with infinite positive limit is bounded above, then the set itself is bounded above.

lemma (in int0) Int_ZF_1_6_L2:

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

shows \( \exists u.\ \forall x\in X.\ b(x) \leq u \)proof
let \( G = \mathbb{Z} \)
let \( P = IntegerAddition \)
let \( r = IntegerOrder \)
from A1, A2, A3, A4 have \( group3(G, P, r) \), \( r \text{ is total on } G \), \( G \neq \{\text{ TheNeutralElement}(G, P)\} \), \( X\neq 0 \), \( f: G\rightarrow G \), \( \forall a\in G.\ \exists b\in \text{PositiveSet}(G, P, r).\ \forall y.\ \langle b, y\rangle \in r \longrightarrow \langle a, f(y)\rangle \in r \), \( \forall x\in X.\ b(x) \in G \wedge \langle f(b(x)), U\rangle \in r \) using int_not_trivial, Int_ZF_2_T1
then have \( \exists u.\ \forall x\in X.\ \langle b(x), u\rangle \in r \) by (rule OrderedGroup_ZF_7_L2 )
thus \( thesis \)
qed

If an image of a set defined by separation by a integer function with infinite negative limit is bounded below, then the set itself is bounded above. This is dual to Int_ZF_1_6_L2.

lemma (in int0) Int_ZF_1_6_L3:

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

shows \( \exists l.\ \forall x\in X.\ l \leq b(x) \)proof
let \( G = \mathbb{Z} \)
let \( P = IntegerAddition \)
let \( r = IntegerOrder \)
from A1, A2, A3, A4 have \( group3(G, P, r) \), \( r \text{ is total on } G \), \( G \neq \{\text{ TheNeutralElement}(G, P)\} \), \( X\neq 0 \), \( f: G\rightarrow G \), \( \forall a\in G.\ \exists b\in \text{PositiveSet}(G, P, r).\ \forall y.\ \) \( \langle b, y\rangle \in r \longrightarrow \langle f( \text{GroupInv}(G, P)(y)),a\rangle \in r \), \( \forall x\in X.\ b(x) \in G \wedge \langle L,f(b(x))\rangle \in r \) using int_not_trivial, Int_ZF_2_T1
then have \( \exists l.\ \forall x\in X.\ \langle l, b(x)\rangle \in r \) by (rule OrderedGroup_ZF_7_L3 )
thus \( thesis \)
qed

The next lemma combines Int_ZF_1_6_L2 and Int_ZF_1_6_L3 to show that if the image of a set defined by separation by a function with infinite limits is bounded, then the set itself is bounded. The proof again uses directly a fact from OrderedGroup_ZF.

lemma (in int0) Int_ZF_1_6_L4:

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

shows \( \exists M.\ \forall x\in X.\ abs(b(x)) \leq M \)proof
let \( G = \mathbb{Z} \)
let \( P = IntegerAddition \)
let \( r = IntegerOrder \)
from A1, A2, A3, A4, A5 have \( group3(G, P, r) \), \( r \text{ is total on } G \), \( G \neq \{\text{ TheNeutralElement}(G, P)\} \), \( X\neq 0 \), \( f: G\rightarrow G \), \( \forall a\in G.\ \exists b\in \text{PositiveSet}(G, P, r).\ \forall y.\ \langle b, y\rangle \in r \longrightarrow \langle a, f(y)\rangle \in r \), \( \forall a\in G.\ \exists b\in \text{PositiveSet}(G, P, r).\ \forall y.\ \) \( \langle b, y\rangle \in r \longrightarrow \langle f( \text{GroupInv}(G, P)(y)),a\rangle \in r \), \( \forall x\in X.\ b(x) \in G \wedge \langle L,f(b(x))\rangle \in r \wedge \langle f(b(x)), U\rangle \in r \) using int_not_trivial, Int_ZF_2_T1
then have \( \exists M.\ \forall x\in X.\ \langle \text{AbsoluteValue}(G, P, r) b(x), M\rangle \in r \) by (rule OrderedGroup_ZF_7_L4 )
thus \( thesis \)
qed

If a function is larger than some constant for arguments large enough, then the image of a set that is bounded below is bounded below. This is not true for ordered groups in general, but only for those for which bounded sets are finite. This does not require the function to have infinite limit, but such functions do have this property.

lemma (in int0) Int_ZF_1_6_L5:

assumes A1: \( f: \mathbb{Z} \rightarrow \mathbb{Z} \) and A2: \( N\in \mathbb{Z} \) and A3: \( \forall m.\ N\leq m \longrightarrow L \leq f(m) \) and A4: \( \text{IsBoundedBelow}(A,IntegerOrder) \)

shows \( \text{IsBoundedBelow}(f(A),IntegerOrder) \)proof
from A2, A4 have \( A = \{x\in A.\ x\leq N\} \cup \{x\in A.\ N\leq x\} \) using Int_ZF_2_T1, Int_ZF_2_L1C, Order_ZF_1_L5
moreover
have \( f(\{x\in A.\ x\leq N\} \cup \{x\in A.\ N\leq x\}) =\) \( f\{x\in A.\ x\leq N\} \cup f\{x\in A.\ N\leq x\} \) by (rule image_Un )
ultimately have \( f(A) = f\{x\in A.\ x\leq N\} \cup f\{x\in A.\ N\leq x\} \)
moreover
have \( \text{IsBoundedBelow}(f\{x\in A.\ x\leq N\},IntegerOrder) \)proof
let \( B = \{x\in A.\ x\leq N\} \)
from A4 have \( B \in Fin(\mathbb{Z} ) \) using Order_ZF_3_L16, Int_bounded_iff_fin
with A1 have \( \text{IsBounded}(f(B),IntegerOrder) \) using Finite1_L6A, Int_bounded_iff_fin
then show \( \text{IsBoundedBelow}(f(B),IntegerOrder) \) using IsBounded_def
qed
moreover
have \( \text{IsBoundedBelow}(f\{x\in A.\ N\leq x\},IntegerOrder) \)proof
let \( C = \{x\in A.\ N\leq x\} \)
from A4 have \( C \subseteq \mathbb{Z} \) using Int_ZF_2_L1C
with A1, A3 have \( \forall y \in f(C).\ \langle L,y\rangle \in IntegerOrder \) using func_imagedef
then show \( \text{IsBoundedBelow}(f(C),IntegerOrder) \) by (rule Order_ZF_3_L9 )
qed
ultimately show \( \text{IsBoundedBelow}(f(A),IntegerOrder) \) using Int_ZF_2_T1, Int_ZF_2_L6, Int_ZF_2_L1B, Order_ZF_3_L6
qed

A function that has an infinite limit can be made arbitrarily large on positive integers by adding a constant. This does not actually require the function to have infinite limit, just to be larger than a constant for arguments large enough.

lemma (in int0) Int_ZF_1_6_L6:

assumes A1: \( N\in \mathbb{Z} \) and A2: \( \forall m.\ N\leq m \longrightarrow L \leq f(m) \) and A3: \( f: \mathbb{Z} \rightarrow \mathbb{Z} \) and A4: \( K\in \mathbb{Z} \)

shows \( \exists c\in \mathbb{Z} .\ \forall n\in \mathbb{Z} _+.\ K \leq f(n) + c \)proof
have \( \text{IsBoundedBelow}(\mathbb{Z} _+,IntegerOrder) \) using Int_ZF_1_5_L1
with A3, A1, A2 have \( \text{IsBoundedBelow}(f(\mathbb{Z} _+),IntegerOrder) \) by (rule Int_ZF_1_6_L5 )
with A1 obtain \( l \) where I: \( \forall y\in f(\mathbb{Z} _+).\ l \leq y \) using Int_ZF_1_5_L5, IsBoundedBelow_def
let \( c = K - l \)
from A3 have \( f(\mathbb{Z} _+) \neq 0 \) using Int_ZF_1_5_L5
then have \( \exists y.\ y \in f(\mathbb{Z} _+) \) by (rule nonempty_has_element )
then obtain \( y \) where \( y \in f(\mathbb{Z} _+) \)
with A4, I have T: \( l \in \mathbb{Z} \), \( c \in \mathbb{Z} \) using Int_ZF_2_L1A, Int_ZF_1_1_L5
{
fix \( n \)
assume A5: \( n\in \mathbb{Z} _+ \)
have \( \mathbb{Z} _+ \subseteq \mathbb{Z} \) using PositiveSet_def
with A3, I, T, A5 have \( l + c \leq f(n) + c \) using func_imagedef, int_ord_transl_inv
with I, T have \( l + c \leq f(n) + c \) using int_ord_transl_inv
with A4, T have \( K \leq f(n) + c \) using Int_ZF_1_2_L3
}
then have \( \forall n\in \mathbb{Z} _+.\ K \leq f(n) + c \)
with T show \( thesis \)
qed

If a function has infinite limit, then we can add such constant such that minimum of those arguments for which the function (plus the constant) is larger than another given constant is greater than a third constant. It is not as complicated as it sounds.

lemma (in int0) Int_ZF_1_6_L7:

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

shows \( \exists C\in \mathbb{Z} .\ N \leq \text{Minimum}(IntegerOrder,\{n\in \mathbb{Z} _+.\ K \leq f(n) + C\}) \)proof
from A1, A2 have \( \exists C\in \mathbb{Z} .\ \forall n\in \mathbb{Z} _+.\ K \leq f(n) + C \longrightarrow N\leq n \) using Int_ZF_1_5_L4
then obtain \( C \) where I: \( C\in \mathbb{Z} \) and II: \( \forall n\in \mathbb{Z} _+.\ K \leq f(n) + C \longrightarrow N\leq n \)
have \( \text{antisym}(IntegerOrder) \) using Int_ZF_2_L4
moreover
have \( \text{HasAminimum}(IntegerOrder,\{n\in \mathbb{Z} _+.\ K \leq f(n) + C\}) \)proof
from A2, A3, I have \( \exists n\in \mathbb{Z} _+.\ \forall x.\ n\leq x \longrightarrow K - C \leq f(x) \) using Int_ZF_1_1_L5
then obtain \( n \) where \( n\in \mathbb{Z} _+ \) and \( \forall x.\ n\leq x \longrightarrow K - C \leq f(x) \)
with A2, I have \( \{n\in \mathbb{Z} _+.\ K \leq f(n) + C\} \neq 0 \), \( \{n\in \mathbb{Z} _+.\ K \leq f(n) + C\} \subseteq \mathbb{Z} _+ \) using int_ord_is_refl, refl_def, PositiveSet_def, Int_ZF_2_L9C
then show \( \text{HasAminimum}(IntegerOrder,\{n\in \mathbb{Z} _+.\ K \leq f(n) + C\}) \) using Int_ZF_1_5_L1C
qed
moreover
from II have \( \forall n \in \{n\in \mathbb{Z} _+.\ K \leq f(n) + C\}.\ \langle N,n\rangle \in IntegerOrder \)
ultimately have \( \langle N, \text{Minimum}(IntegerOrder,\{n\in \mathbb{Z} _+.\ K \leq f(n) + C\})\rangle \in IntegerOrder \) by (rule Order_ZF_4_L12 )
with I show \( thesis \)
qed

For any integer \(m\) the function \(k\mapsto m\cdot k\) has an infinite limit (or negative of that). This is why we put some properties of these functions here, even though they properly belong to a (yet nonexistent) section on homomorphisms. The next lemma shows that the set \(\{a\cdot x: x\in Z\}\) can finite only if \(a=0\).

lemma (in int0) Int_ZF_1_6_L8:

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

shows \( a = 0 \)proof
from A1 have \( a= 0 \vee (a \leq - 1 ) \vee (1 \leq a) \) using Int_ZF_1_3_L6C
moreover {
assume \( a \leq - 1 \)
then have \( \{a\cdot x.\ x\in \mathbb{Z} \} \notin Fin(\mathbb{Z} ) \) using int_zero_not_one, Int_ZF_1_3_T1, OrdRing_ZF_3_L6
with A2 have \( False \)
} moreover {
assume \( 1 \leq a \)
then have \( \{a\cdot x.\ x\in \mathbb{Z} \} \notin Fin(\mathbb{Z} ) \) using int_zero_not_one, Int_ZF_1_3_T1, OrdRing_ZF_3_L5
with A2 have \( False \)
} ultimately show \( a = 0 \)
qed

Miscelaneous

In this section we put some technical lemmas needed in various other places that are hard to classify.

Suppose we have an integer expression (a meta-function)\(F\) such that \(F(p)|p|\) is bounded by a linear function of \(|p|\), that is for some integers \(A,B\) we have \(F(p)|p|\leq A|p|+B.\) We show that \(F\) is then bounded. The proof is easy, we just divide both sides by \(|p|\) and take the limit (just kidding).

lemma (in int0) Int_ZF_1_7_L1:

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

shows \( \exists L.\ \forall p\in \mathbb{Z} .\ F(p) \leq L \)proof
let \( I = ( - abs(B)).\ .\ abs(B) \)
let \( K = \{F(q).\ q \in I\} \)
let \( M = \text{Maximum}(IntegerOrder,K) \)
let \( L = \text{GreaterOf}(IntegerOrder,M,A + 1 ) \)
from A3, A1 have C1: \( \text{IsBounded}(I,IntegerOrder) \), \( I \neq 0 \), \( \forall q\in \mathbb{Z} .\ F(q) \in \mathbb{Z} \), \( K = \{F(q).\ q \in I\} \) using Order_ZF_3_L11, Int_ZF_1_3_L17
then have \( M \in \mathbb{Z} \) by (rule Int_ZF_1_4_L1 )
with A3 have T1: \( M \leq L \), \( A + 1 \leq L \) using int_zero_one_are_int, Int_ZF_1_1_L5, Int_ZF_1_3_L18
from C1 have T2: \( \forall q\in I.\ F(q) \leq M \) by (rule Int_ZF_1_4_L1 )
{
fix \( p \)
assume A4: \( p\in \mathbb{Z} \)
have \( F(p) \leq L \)proof
{
assume \( abs(p) \leq abs(B) \)
with A4, T1, T2 have \( F(p) \leq M \), \( M \leq L \) using Int_ZF_1_3_L19
then have \( F(p) \leq L \) by (rule Int_order_transitive )
}
moreover {
assume A5: \( \neg (abs(p) \leq abs(B)) \)
from A3, A2, A4 have \( A\cdot abs(p) \in \mathbb{Z} \), \( F(p)\cdot abs(p) \leq A\cdot abs(p) + B \) using Int_ZF_2_L14, Int_ZF_1_1_L5
moreover
from A3, A4, A5 have \( B \leq abs(p) \) using Int_ZF_1_3_L15
ultimately have \( F(p)\cdot abs(p) \leq A\cdot abs(p) + abs(p) \) using Int_ZF_2_L15A
with A3, A4 have \( F(p)\cdot abs(p) \leq (A + 1 )\cdot abs(p) \) using Int_ZF_2_L14, Int_ZF_1_2_L7
moreover
from A3, A1, A4, A5 have \( F(p) \in \mathbb{Z} \), \( A + 1 \in \mathbb{Z} \), \( abs(p) \in \mathbb{Z} \), \( \neg (abs(p) \leq 0 ) \) using int_zero_one_are_int, Int_ZF_1_1_L5, Int_ZF_2_L14, Int_ZF_1_3_L11
ultimately have \( F(p) \leq A + 1 \) using Int_ineq_simpl_positive
moreover
from T1 have \( A + 1 \leq L \)
ultimately have \( F(p) \leq L \) by (rule Int_order_transitive )
} ultimately show \( thesis \)
qed
}
then have \( \forall p\in \mathbb{Z} .\ F(p) \leq L \)
thus \( thesis \)
qed

A lemma about splitting (not really, there is some overlap) the \( \mathbb{Z} \times \mathbb{Z} \) into six subsets (cases). The subsets are as follows: first and third qaudrant, and second and fourth quadrant farther split by the \(b =-a\) line.

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 \) using assms, Int_ZF_2_T1, OrdGroup_6cases
end
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_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 \)
Definition of IsDistributive: \( \text{IsDistributive}(X,A,M) \equiv (\forall a\in X.\ \forall b\in X.\ \forall c\in X.\ \) \( M\langle a,A\langle b,c\rangle \rangle = A\langle M\langle a,b\rangle ,M\langle a,c\rangle \rangle \wedge \) \( M\langle A\langle b,c\rangle ,a\rangle = A\langle M\langle b,a\rangle ,M\langle c,a\rangle \rangle ) \)
theorem (in int0) Int_ZF_1_T1: shows \( \text{IsAmonoid}(\mathbb{Z} ,IntegerAddition) \), \( \text{IsAmonoid}(\mathbb{Z} ,IntegerMultiplication) \)
theorem Int_ZF_1_T2: shows \( \text{IsAgroup}(int,IntegerAddition) \), \( IntegerAddition \text{ is commutative on } int \), \( group0(int,IntegerAddition) \)
Definition of IsAring: \( \text{IsAring}(R,A,M) \equiv \text{IsAgroup}(R,A) \wedge (A \text{ is commutative on } R) \wedge \) \( \text{IsAmonoid}(R,M) \wedge \text{IsDistributive}(R,A,M) \)
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 \)
Definition of IsCommutative: \( f \text{ is commutative on } G \equiv \forall x\in G.\ \forall y\in G.\ f\langle x,y\rangle = f\langle y,x\rangle \)
lemma (in 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_1_L2: shows \( 0 \in R \), \( 1 \in R \), \( ( - 0 ) = 0 \)
lemma (in group0) group_inv_of_one: shows \( 1 ^{-1} = 1 \)
lemma (in ring0) Ring_ZF_1_L3:

assumes \( a\in R \)

shows \( ( - a) \in R \), \( ( - ( - a)) = a \), \( a + 0 = a \), \( 0 + a = a \), \( a\cdot 1 = a \), \( 1 \cdot a = a \), \( a - a = 0 \), \( a - 0 = a \), \( 2 \cdot a = a + a \), \( ( - a) + a = 0 \)
lemma (in ring0) Ring_ZF_1_L6:

assumes \( x\in R \)

shows \( 0 \cdot x = 0 \), \( x\cdot 0 = 0 \)
lemma (in ring0) Ring_ZF_1_L4:

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

shows \( a + b \in R \), \( a - b \in R \), \( a\cdot b \in R \), \( a + b = b + a \)
lemma (in ring0) Ring_ZF_1_L9:

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

shows \( ( - b) - a = ( - a) - b \), \( ( - (a + b)) = ( - a) - b \), \( ( - (a - b)) = (( - a) + b) \), \( a - ( - b) = a + b \)
lemma (in ring0) Ring_ZF_1_L7:

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

shows \( ( - a)\cdot b = - (a\cdot b) \), \( a\cdot ( - b) = - (a\cdot b) \), \( ( - a)\cdot b = a\cdot ( - b) \)
lemma (in ring0) Ring_ZF_1_L7A:

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

shows \( ( - a)\cdot ( - b) = a\cdot b \)
lemma (in int0) int_zero_one_are_int: shows \( 0 \in \mathbb{Z} \), \( 1 \in \mathbb{Z} \)
lemma (in int0) Int_ZF_1_1_L5:

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

shows \( a + b \in \mathbb{Z} \), \( a - b \in \mathbb{Z} \), \( a\cdot b \in \mathbb{Z} \), \( a + b = b + a \), \( a\cdot b = b\cdot a \), \( ( - b) - a = ( - a) - b \), \( ( - (a + b)) = ( - a) - b \), \( ( - (a - b)) = (( - a) + b) \), \( ( - a)\cdot b = - (a\cdot b) \), \( a\cdot ( - b) = - (a\cdot b) \), \( ( - a)\cdot ( - b) = a\cdot b \)
lemma (in ring0) Ring_ZF_1_L10:

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

shows \( a + (b + c) = a + b + c \), \( a - (b + c) = a - b - c \), \( a - (b - c) = a - b + c \)
lemma (in ring0) Ring_ZF_1_L8:

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

shows \( a\cdot (b - c) = a\cdot b - a\cdot c \), \( (b - c)\cdot a = b\cdot a - c\cdot a \)
lemma (in ring0) Ring_ZF_1_L10A:

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

shows \( a + (b - c) = a + b - c \)
lemma (in ring0) Ring_ZF_1_L11:

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

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

assumes \( j\leq k \)

shows \( j \leq k \ \$ + \ \$ #1 \), \( j \leq k + 1 \)
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_L14:

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

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

assumes \( 0 \leq a \)

shows \( abs(a) + 1 = abs(a + 1 ) \)
lemma (in ring0) Ring_ZF_2_L1:

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

shows \( a + b\cdot a = (b + 1 )\cdot a \)
lemma (in group0) group0_4_L6A:

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

shows \( a\cdot b\cdot a^{-1} = b \), \( a^{-1}\cdot b\cdot a = b \), \( a^{-1}\cdot (b\cdot a) = b \), \( a\cdot (b\cdot a^{-1}) = b \)
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_L16A:

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

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

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

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

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

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

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

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

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

shows \( a\cdot (a\cdot b^{-1})^{-1} = b \)
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_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_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_ord_is_refl: shows \( \text{refl}(\mathbb{Z} ,IntegerOrder) \)
lemma (in int0) Int_ZF_1_2_L3A:

assumes \( a\leq b \)

shows \( a - 1 \leq b \)
lemma (in int0) Int_ZF_1_L14:

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

shows \( m + 1 \neq m \), \( m - 1 \neq m \)
lemma (in int0) Int_ZF_2_L19AA:

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

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

assumes \( a\leq 1 \)

shows \( \vert a\vert = a^{-1} \)
lemma (in int0) Int_ZF_1_2_L4:

assumes \( a\leq 0 \)

shows \( abs(a) + 1 = abs(a - 1 ) \)
lemma (in int0) Int_ZF_1_1_L6:

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

shows \( a - (b + c) = a - b - c \), \( a - (b - c) = a - b + c \), \( a\cdot (b - c) = a\cdot b - a\cdot c \), \( (b - c)\cdot a = b\cdot a - c\cdot a \)
lemma (in group0) group0_4_L8:

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

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

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

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

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

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

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

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

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

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

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

shows \( a\cdot b\cdot (a\cdot c)^{-1} = b\cdot c^{-1} \)
lemma (in int0) Int_ZF_1_1_L5B:

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

shows \( a - ( - b) = a + b \)
lemma (in int0) Int_ZF_1_2_L8:

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

shows \( a + 1 + (b + 1 ) = b + a + 2 \)
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_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_two_three_are_int: shows \( 2 \in \mathbb{Z} \), \( 3 \in \mathbb{Z} \)
lemma (in group0) group0_4_L4C:

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\cdot b\cdot c = a\cdot (c\cdot b) \), \( a\cdot b\cdot c = c\cdot (a\cdot b) \), \( a\cdot b\cdot c = c\cdot b\cdot a \)
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_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 ring0) Ring_ZF_2_L3:

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

shows \( (a\cdot x + b) + (c\cdot x + d) = (a + c)\cdot x + (b + d) \)
lemma (in group0) group0_4_L9:

assumes \( P \text{ is commutative on } G \) and \( a\in G \), \( b\in G \), \( c\in G \), \( d\in G \) and \( a = b\cdot c^{-1}\cdot d^{-1} \)

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

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

shows \( a\cdot c^{-1}= (a\cdot b^{-1})\cdot (b\cdot c^{-1}) \), \( a^{-1}\cdot c = (a^{-1}\cdot b)\cdot (b^{-1}\cdot c) \), \( a\cdot (b\cdot c)^{-1} = a\cdot c^{-1}\cdot b^{-1} \), \( a\cdot (b\cdot c^{-1}) = a\cdot b\cdot c^{-1} \), \( (a\cdot b^{-1}\cdot c^{-1})^{-1} = c\cdot b\cdot a^{-1} \), \( a\cdot b\cdot c^{-1}\cdot (c\cdot b^{-1}) = a \), \( a\cdot (b\cdot c)\cdot c^{-1} = a\cdot b \)
lemma (in int0) int_ineq_add_sides:

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

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

assumes \( 0 \leq a \), \( 0 \leq b \) and \( 0 \leq a\cdot b \)

shows \( 0 \leq a\cdot (b + 1 ) \)
theorem (in int0) Induction_on_int:

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

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

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

shows \( 0 \leq a\cdot b \)
lemma (in group3) OrderedGroup_ZF_1_L2: shows \( g\in G^+ \longleftrightarrow 1 \leq g \)
Definition of IsOpClosed: \( A \text{ is closed under } f \equiv \forall x\in A.\ \forall y\in A.\ f\langle x,y\rangle \in A \)
lemma Int_ZF_2_L1B: shows \( IntegerOrder \subseteq int\times int \)
lemma (in int0) Int_ZF_1_3_L2A: shows \( \mathbb{Z} ^+ \text{ is closed under } IntegerMultiplication \)
lemma OrdRing_ZF_1_L6:

assumes \( \text{IsAring}(R,A,M) \), \( M \text{ is commutative on } R \), \( \text{Nonnegative}(R,A,r) \text{ is closed under } M \), \( \text{IsAnOrdGroup}(R,A,r) \), \( r \text{ is total on } R \)

shows \( \text{IsAnOrdRing}(R,A,M,r) \)
lemma OrdRing_ZF_1_L2:

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

shows \( ring1(R,A,M,r) \)
lemma (in int0) Int_ZF_2_L16B: shows \( 1 \leq 2 \)
lemma (in int0) Int_order_transitive:

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

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

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

shows \( 1 \leq a\cdot (b + 1 ) \)
lemma (in int0) Int_ZF_2_L17:

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

shows \( abs( - m) = abs(m) \)
theorem (in int0) Int_ZF_1_3_T1: shows \( \text{IsAnOrdRing}(\mathbb{Z} ,IntegerAddition,IntegerMultiplication,IntegerOrder) \), \( ring1(\mathbb{Z} ,IntegerAddition,IntegerMultiplication,IntegerOrder) \)
lemma (in ring1) OrdRing_ZF_2_L5:

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

shows \( \vert a\cdot b\vert = \vert a\vert \cdot \vert b\vert \)
lemma (in ring1) OrdRing_ZF_1_L5A:

assumes \( 0 \leq a \)

shows \( 0 \leq 2 \cdot a \)
lemma (in int0) Int_ZF_2_L19:

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

shows \( m\leq n \), \( ( - n) \leq ( - m) \), \( m\neq n \)
lemma (in int0) Int_ZF_4_L1B:

assumes \( m \leq L \)

shows \( m = L \vee m + 1 \leq L \), \( m = L \vee m \leq L - 1 \)
lemma (in int0) Int_ZF_2_L12B:

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

shows \( m \leq m + 1 \)
lemma (in int0) Int_ZF_2_L3:

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

shows \( m=n \)
lemma (in int0) Int_ZF_1_3_L6:

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

shows \( \neg (b\leq a) \longleftrightarrow a + 1 \leq b \)
corollary (in int0) no_int_between:

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

shows \( b\leq a \vee a + 1 \leq b \)
corollary (in int0) Int_ZF_1_3_L6A:

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

shows \( a \leq b - 1 \)
lemma (in group3) OrderedGroup_ZF_1_L31:

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

shows \( a=b \vee (a\leq b \wedge a\neq b) \vee (b\leq a \wedge b\neq a) \)
lemma (in int0) no_int_between1:

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

shows \( a + 1 \leq b \), \( a \leq b - 1 \)
lemma (in int0) Int_ZF_1_3_L6B:

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

shows \( a=b \vee (a \leq b - 1 ) \vee (b + 1 \leq a) \)
lemma (in int0) Int_ZF_1_3_L7:

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

shows \( \neg (a\leq 0 ) \longleftrightarrow 1 \leq a \)
lemma (in int0) Int_ZF_1_3_L3:

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

shows \( 1 \leq a\cdot b \)
lemma (in int0) Int_ZF_1_3_L8:

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

shows \( \neg ((a\cdot b) \leq 0 ) \)
lemma (in group3) OrderedGroup_ZF_1_L9:

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

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

assumes \( a\leq b \)

shows \( 1 \leq b\cdot a^{-1} \)
lemma (in int0) Int_ZF_1_3_L10:

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

shows \( a\leq b \longleftrightarrow a - b \leq 0 \)
lemma (in int0) Int_ZF_1_3_L9:

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

shows \( a\leq 0 \)
lemma (in int0) int_abs_nonneg:

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

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

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

shows \( a\cdot b \leq 0 \)
lemma (in ring1) OrdRing_ZF_1_L9:

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

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

assumes \( 1 \leq a \)

shows \( 0 \leq a \), \( a\neq 0 \), \( 2 \leq a + 1 \), \( 1 \leq a + 1 \), \( 0 \leq a + 1 \)
lemma (in int0) Int_ZF_1_3_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 ring1) OrdRing_ZF_1_L9A:

assumes \( a\leq b \) and \( c\in R_+ \)

shows \( a\cdot c \leq b\cdot c \), \( c\cdot a \leq c\cdot b \)
lemma (in 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_2_L19C:

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

shows \( m \leq abs(m) \), \( ( - m) \leq abs(m) \)
lemma (in int0) Int_ZF_2_L18: shows \( abs( 0 ) = 0 \)
lemma (in int0) Int_ZF_2_L10:

assumes \( k \leq i \)

shows \( ( - i) \leq ( - k) \), \( \ \$ -i \leq \ \$ -k \)
lemma (in int0) Int_ZF_1_L11: shows \( ( - 0 ) = 0 \)
lemma (in int0) Int_ZF_1_3_L16:

assumes \( 0 \leq m \)

shows \( ( - m) \leq 0 \)
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 Order_ZF_3_L2:

assumes \( r \text{ is total on } X \) and \( x\in X \), \( y\in X \)

shows \( \langle x, \text{GreaterOf}(r,x,y)\rangle \in r \), \( \langle y, \text{GreaterOf}(r,x,y)\rangle \in r \), \( \langle \text{SmallerOf}(r,x,y),x\rangle \in r \), \( \langle \text{SmallerOf}(r,x,y),y\rangle \in r \)
lemma (in group3) OrderedGroup_ZF_3_L8:

assumes \( a\in G \) and \( \vert a\vert \leq L \)

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

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

shows \( a\leq L \), \( 1 \leq L \)
lemma Order_ZF_2_L1: shows \( x \in \text{Interval}(r,a,b) \longleftrightarrow \langle a,x\rangle \in r \wedge \langle x,b\rangle \in r \)
lemma (in group3) OrderedGroup_ZF_3_L8B:

assumes \( a\in G \) and \( \vert a\vert \leq L \) and \( 1 \leq c \)

shows \( (L\cdot c)^{-1} \leq a \)
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) \)
lemma (in group3) OrderedGroup_ZF_3_L10A:

assumes \( r \text{ is total on } G \) and \( \text{IsBounded}(A,r) \)

shows \( \exists L.\ \forall a\in A.\ \vert a\vert \leq L \)
lemma (in int0) int_not_empty: shows \( \mathbb{Z} \neq 0 \)
lemma (in group3) OrderedGroup_ZF_3_L11A:

assumes \( r \text{ is total on } G \) and \( X\neq 0 \) and \( \{b(x).\ x\in X\} \in Fin(G) \)

shows \( \exists L\in G.\ \forall x\in X.\ \vert b(x)\vert \leq L \)
lemma (in group3) OrderedGroup_ZF_3_L9B:

assumes \( r \text{ is total on } G \) and \( f:X\rightarrow G \) and \( A\subseteq X \) and \( \forall x\in A.\ \vert f(x)\vert \leq L \)

shows \( \text{IsBounded}(f(A),r) \)
lemma (in int0) Int_ZF_1_3_L20B:

assumes \( f:X\rightarrow \mathbb{Z} \) and \( A\subseteq X \) and \( \forall x\in A.\ abs(f(x)) \leq L \)

shows \( \text{IsBounded}(f(A),IntegerOrder) \)
theorem (in int0) Int_bounded_iff_fin: shows \( \text{IsBounded}(A,IntegerOrder)\longleftrightarrow A\in Fin(\mathbb{Z} ) \)
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 ring1) OrdRing_ZF_2_L6:

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

shows \( a + b \leq 2 \cdot c \)
lemma (in group3) OrderedGroup_ZF_3_L8C:

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

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

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

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

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

shows \( abs(b - a) \leq c \)
lemma Int_ZF_2_L6: shows \( \text{trans}(IntegerOrder) \)
theorem Finite_ZF_1_1_T1A:

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

shows \( B=0 \vee \text{HasAmaximum}(r,B) \)
theorem Finite_ZF_1_1_T1B:

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

shows \( B=0 \vee \text{HasAminimum}(r,B) \)
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 \)
theorem (in int0) Int_fin_have_max_min:

assumes \( A \in Fin(\mathbb{Z} ) \) and \( A\neq 0 \)

shows \( \text{HasAmaximum}(IntegerOrder,A) \), \( \text{HasAminimum}(IntegerOrder,A) \), \( \text{Maximum}(IntegerOrder,A) \in A \), \( \text{Minimum}(IntegerOrder,A) \in A \), \( \forall x\in A.\ x \leq \text{Maximum}(IntegerOrder,A) \), \( \forall x\in A.\ \text{Minimum}(IntegerOrder,A) \leq x \), \( \text{Maximum}(IntegerOrder,A) \in \mathbb{Z} \), \( \text{Minimum}(IntegerOrder,A) \in \mathbb{Z} \)
theorem (in int0) Int_bounded_have_max_min:

assumes \( \text{IsBounded}(A,IntegerOrder) \) and \( A\neq 0 \)

shows \( \text{HasAmaximum}(IntegerOrder,A) \), \( \text{HasAminimum}(IntegerOrder,A) \), \( \text{Maximum}(IntegerOrder,A) \in A \), \( \text{Minimum}(IntegerOrder,A) \in A \), \( \forall x\in A.\ x \leq \text{Maximum}(IntegerOrder,A) \), \( \forall x\in A.\ \text{Minimum}(IntegerOrder,A) \leq x \), \( \text{Maximum}(IntegerOrder,A) \in \mathbb{Z} \), \( \text{Minimum}(IntegerOrder,A) \in \mathbb{Z} \)
lemma Order_ZF_4_L11:

assumes \( r \text{ is total on } X \) and \( \text{trans}(r) \) and \( r \subseteq X\times X \) and \( \forall A.\ \text{IsBounded}(A,r) \wedge A\neq 0 \longrightarrow \text{HasAminimum}(r,A) \) and \( B\neq 0 \) and \( \text{IsBoundedBelow}(B,r) \)

shows \( \text{HasAminimum}(r,B) \)
lemma (in int0) Int_ZF_2_L4: shows \( \text{antisym}(IntegerOrder) \)
lemma Order_ZF_4_L4:

assumes \( \text{antisym}(r) \) and \( \text{HasAminimum}(r,A) \)

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

assumes \( r \text{ is total on } X \) and \( \text{trans}(r) \) and \( r \subseteq X\times X \) and \( \forall A.\ \text{IsBounded}(A,r) \wedge A\neq 0 \longrightarrow \text{HasAmaximum}(r,A) \) and \( B\neq 0 \) and \( \text{IsBoundedAbove}(B,r) \)

shows \( \text{HasAmaximum}(r,B) \)
lemma Order_ZF_4_L3:

assumes \( \text{antisym}(r) \) and \( \text{HasAmaximum}(r,A) \)

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

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

shows \( A\subseteq X \)
lemma fin_image_fin:

assumes \( \forall V\in B.\ K(V)\in C \) and \( N \in \text{FinPow}(B) \)

shows \( \{K(V).\ V\in N\} \in \text{FinPow}(C) \)
lemma Order_ZF_4_L7:

assumes \( \text{HasAmaximum}(r,A) \)

shows \( \text{IsBoundedAbove}(A,r) \)
lemma Order_ZF_4_L8A:

assumes \( \text{HasAminimum}(r,A) \)

shows \( \text{IsBoundedBelow}(A,r) \)
Definition of IsBounded: \( \text{IsBounded}(A,r) \equiv ( \text{IsBoundedAbove}(A,r) \wedge \text{IsBoundedBelow}(A,r)) \)
corollary Finite_ZF_1_L2A:

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

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

assumes \( r \subseteq X\times X \)

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

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

shows \( f(i.\ .\ k) \in Fin(\mathbb{Z} ) \), \( \text{IsBounded}(f(i.\ .\ k),IntegerOrder) \)
lemma (in group3) OrderedGroup_ZF_2_L6:

assumes \( a\leq b \) and \( f:G\rightarrow G \)

shows \( f( \text{Interval}(r,a,b)) \neq 0 \)
lemma func_imagedef:

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

shows \( f(A) = \{f(x).\ x \in A\} \)
lemma (in group3) OrderedGroup_ZF_1_L13: shows \( G_+ \text{ is closed under } P \)
lemma (in int0) pos_int_closed_add: shows \( \mathbb{Z} _+ \text{ is closed under } IntegerAddition \)
Definition of Nonnegative: \( \text{Nonnegative}(L,A,r) \equiv \{x\in L.\ \langle \text{ TheNeutralElement}(L,A),x\rangle \in r\} \)
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\} \)
Definition of IsBoundedBelow: \( \text{IsBoundedBelow}(A,r) \equiv (A=0 \vee (\exists l.\ \forall x\in A.\ \langle l,x\rangle \in r)) \)
lemma (in int0) Int_ZF_1_5_L1: shows \( \text{IsBoundedBelow}(\mathbb{Z} ^+,IntegerOrder) \), \( \text{IsBoundedBelow}(\mathbb{Z} _+,IntegerOrder) \)
lemma Order_ZF_3_L12:

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

shows \( \text{IsBoundedBelow}(B,r) \)
lemma (in int0) Int_ZF_1_5_L1B:

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

shows \( \text{IsBoundedBelow}(A,IntegerOrder) \)
theorem (in int0) int_bounded_below_has_min:

assumes \( \text{IsBoundedBelow}(A,IntegerOrder) \) and \( A\neq 0 \)

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

assumes \( \forall a\in A.\ \langle a,u\rangle \in r \)

shows \( \text{IsBoundedAbove}(A,r) \)
lemma (in int0) Int_ZF_1_5_L1A:

assumes \( A \subseteq \mathbb{Z} ^+ \)

shows \( \text{IsBoundedBelow}(A,IntegerOrder) \)
lemma (in group3) OrdGroup_decomp:

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

shows \( \text{Exactly_1_of_3_holds} (a=1 ,a\in G_+,a^{-1}\in G_+) \)
lemma (in group3) OrderedGroup_ZF_1_L14:

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

shows \( a=1 \vee a\in G_+ \vee a^{-1}\in G_+ \)
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_1_5_L3: shows \( m\in \mathbb{Z} _+ \longleftrightarrow 1 \leq m \)
lemma (in int0) pos_int_closed_mul_unfold:

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

shows \( a\cdot b \in \mathbb{Z} _+ \)
lemma (in int0) pos_int_closed_mul: shows \( \mathbb{Z} _+ \text{ is closed under } IntegerMultiplication \)
lemma (in ring1) OrdRing_ZF_3_L3: shows \( (R_+ \text{ is closed under } M)\longleftrightarrow \text{HasNoZeroDivs}(R,A,M) \)
lemma (in group3) OrderedGroup_ZF_1_L24: shows \( G^+ = G_+\cup \{1 \} \)
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 Interval: \( \text{Interval}(r,a,b) \equiv r\{a\} \cap r^{-1}\{b\} \)
lemma (in int0) Int_ZF_1_2_L3AA:

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

shows \( a - 1 \leq a \), \( a - 1 \neq a \), \( \neg (a\leq a - 1 ) \), \( \neg (a + 1 \leq a) \), \( \neg (1 + a \leq a) \)
lemma (in group3) OrderedGroup_ZF_3_L2B:

assumes \( a\in G_+ \)

shows \( \vert a\vert = a \)
lemma (in int0) int_one_two_are_pos: shows \( 1 \in \mathbb{Z} _+ \), \( 2 \in \mathbb{Z} _+ \)
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 group3) OrderedGroup_ZF_1_L22:

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

shows \( a\leq a\cdot b \), \( a \neq a\cdot b \), \( a\cdot b \in G \)
lemma (in int0) int_zero_not_one: shows \( 0 \neq 1 \)
lemma (in ring1) OrdRing_ZF_3_L12:

assumes \( 0 \neq 1 \) and \( a\in R \)

shows \( a \leq \text{GreaterOf}(r,1 ,a) \), \( \text{GreaterOf}(r,1 ,a) \in R_+ \), \( \text{GreaterOf}(r,1 ,a) + 1 \in R_+ \), \( a \leq \text{GreaterOf}(r,1 ,a) + 1 \), \( a \neq \text{GreaterOf}(r,1 ,a) + 1 \)
lemma (in group3) OrderedGroup_ZF_1_L20:

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

shows \( a^{-1} \notin G_+ \)
lemma (in int0) int_not_trivial: shows \( \mathbb{Z} \neq \{ 0 \} \)
lemma (in group3) OrderedGroup_ZF_1_L23:

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

shows \( \exists b\in G_+.\ a\leq b \)
lemma (in group3) odd_ext_props:

assumes \( r \text{ is total on } G \) and \( f: G_+\rightarrow G \)

shows \( f^\circ : G \rightarrow G \), \( \forall a\in G_+.\ (f^\circ )(a) = f(a) \), \( \forall a\in (-G_+).\ (f^\circ )(a) = (f(a^{-1}))^{-1} \), \( (f^\circ )(1 ) = 1 \)
lemma (in group3) oddext_is_odd:

assumes \( r \text{ is total on } G \) and \( f: G_+\rightarrow G \) and \( a\in G \)

shows \( (f^\circ )(a^{-1}) = ((f^\circ )(a))^{-1} \)
lemma (in group0) group0_6_L2:

assumes \( p : G\rightarrow G \)

shows \( (\forall a\in G.\ p(a^{-1}) = (p(a))^{-1}) \longleftrightarrow (\forall a\in G.\ (p(a^{-1}))^{-1} = p(a)) \)
lemma (in group3) oddext_is_odd_alt:

assumes \( r \text{ is total on } G \) and \( f: G_+\rightarrow G \) and \( a\in G \)

shows \( ((f^\circ )(a^{-1}))^{-1} = (f^\circ )(a) \)
lemma (in group3) OrderedGroup_ZF_7_L1:

assumes \( r \text{ is total on } G \) and \( G \neq \{1 \} \) and \( f:G\rightarrow G \) and \( \forall a\in G.\ \exists b\in G_+.\ \forall x.\ b\leq x \longrightarrow a \leq f(x) \) and \( A\subseteq G \) and \( \text{IsBoundedAbove}(f(A),r) \)

shows \( \text{IsBoundedAbove}(A,r) \)
lemma (in group3) OrderedGroup_ZF_7_L2:

assumes \( r \text{ is total on } G \) and \( G \neq \{1 \} \) and \( X\neq 0 \) and \( f:G\rightarrow G \) and \( \forall a\in G.\ \exists b\in G_+.\ \forall y.\ b\leq y \longrightarrow a \leq f(y) \) and \( \forall x\in X.\ b(x) \in G \wedge f(b(x)) \leq U \)

shows \( \exists u.\ \forall x\in X.\ b(x) \leq u \)
lemma (in group3) OrderedGroup_ZF_7_L3:

assumes \( r \text{ is total on } G \) and \( G \neq \{1 \} \) and \( X\neq 0 \) and \( f:G\rightarrow G \) and \( \forall a\in G.\ \exists b\in G_+.\ \forall y.\ b\leq y \longrightarrow f(y^{-1}) \leq a \) and \( \forall x\in X.\ b(x) \in G \wedge L \leq f(b(x)) \)

shows \( \exists l.\ \forall x\in X.\ l \leq b(x) \)
lemma (in group3) OrderedGroup_ZF_7_L4:

assumes \( r \text{ is total on } G \) and \( G \neq \{1 \} \) and \( X\neq 0 \) and \( f:G\rightarrow G \) and \( \forall a\in G.\ \exists b\in G_+.\ \forall y.\ b\leq y \longrightarrow a \leq f(y) \) and \( \forall a\in G.\ \exists b\in G_+.\ \forall y.\ b\leq y \longrightarrow f(y^{-1}) \leq a \) and \( \forall x\in X.\ b(x) \in G \wedge L \leq f(b(x)) \wedge f(b(x)) \leq U \)

shows \( \exists M.\ \forall x\in X.\ \vert b(x)\vert \leq M \)
lemma (in int0) Int_ZF_2_L1C:

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

shows \( A\subseteq \mathbb{Z} \)
lemma Order_ZF_1_L5:

assumes \( r \text{ is total on } X \) and \( A\subseteq X \) and \( a\in X \)

shows \( A = \{x\in A.\ \langle x,a\rangle \in r\} \cup \{x\in A.\ \langle a,x\rangle \in r\} \)
lemma Order_ZF_3_L16:

assumes \( \text{IsBoundedBelow}(A,r) \)

shows \( \text{IsBounded}(\{x\in A.\ \langle x,a\rangle \in r\},r) \)
lemma Finite1_L6A:

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

shows \( f(N) \in Fin(Y) \)
lemma Order_ZF_3_L9:

assumes \( \forall a\in A.\ \langle l,a\rangle \in r \)

shows \( \text{IsBoundedBelow}(A,r) \)
lemma Order_ZF_3_L6:

assumes \( r \text{ is total on } X \) and \( \text{trans}(r) \) and \( \text{IsBoundedBelow}(A,r) \), \( \text{IsBoundedBelow}(B,r) \) and \( r \subseteq X\times X \)

shows \( \text{IsBoundedBelow}(A\cup B,r) \)
lemma (in int0) Int_ZF_1_6_L5:

assumes \( f: \mathbb{Z} \rightarrow \mathbb{Z} \) and \( N\in \mathbb{Z} \) and \( \forall m.\ N\leq m \longrightarrow L \leq f(m) \) and \( \text{IsBoundedBelow}(A,IntegerOrder) \)

shows \( \text{IsBoundedBelow}(f(A),IntegerOrder) \)
lemma (in int0) Int_ZF_1_5_L5:

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

shows \( f(\mathbb{Z} _+) \neq 0 \)
lemma nonempty_has_element:

assumes \( X\neq 0 \)

shows \( \exists x.\ x\in X \)
lemma (in int0) Int_ZF_1_5_L4:

assumes \( f:\mathbb{Z} \rightarrow \mathbb{Z} \) and \( K\in \mathbb{Z} \), \( N\in \mathbb{Z} \)

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

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

shows \( i \leq k + m \)
lemma (in int0) Int_ZF_1_5_L1C:

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

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

assumes \( \text{antisym}(r) \) and \( \text{HasAminimum}(r,A) \) and \( \forall a\in A.\ \langle L,a\rangle \in r \)

shows \( \langle L, \text{Minimum}(r,A)\rangle \in r \)
corollary (in int0) Int_ZF_1_3_L6C:

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

shows \( a= 0 \vee (a \leq - 1 ) \vee (1 \leq a) \)
lemma (in ring1) OrdRing_ZF_3_L6:

assumes \( 0 \neq 1 \) and \( m \leq - 1 \)

shows \( \{m\cdot x.\ x\in R\} \notin Fin(R) \)
lemma (in ring1) OrdRing_ZF_3_L5:

assumes \( 0 \neq 1 \) and \( 1 \leq m \)

shows \( \{m\cdot x.\ x\in R_+\} \notin Fin(R) \), \( \{m\cdot x.\ x\in R\} \notin Fin(R) \), \( \{( - m)\cdot x.\ x\in R\} \notin Fin(R) \)
lemma Order_ZF_3_L11: shows \( \text{IsBoundedAbove}( \text{Interval}(r,a,b),r) \), \( \text{IsBoundedBelow}( \text{Interval}(r,a,b),r) \), \( \text{IsBounded}( \text{Interval}(r,a,b),r) \)
lemma (in int0) Int_ZF_1_3_L17:

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

shows \( ( - abs(m)) \leq abs(m) \), \( ( - abs(m)).\ .\ abs(m) \neq 0 \)
lemma (in int0) Int_ZF_1_4_L1:

assumes \( \text{IsBounded}(A,IntegerOrder) \) and \( A\neq 0 \) and \( \forall q\in \mathbb{Z} .\ F(q) \in \mathbb{Z} \) and \( K = \{F(q).\ q \in A\} \)

shows \( \text{HasAmaximum}(IntegerOrder,K) \), \( \text{HasAminimum}(IntegerOrder,K) \), \( \text{Maximum}(IntegerOrder,K) \in K \), \( \text{Minimum}(IntegerOrder,K) \in K \), \( \text{Maximum}(IntegerOrder,K) \in \mathbb{Z} \), \( \text{Minimum}(IntegerOrder,K) \in \mathbb{Z} \), \( \forall q\in A.\ F(q) \leq \text{Maximum}(IntegerOrder,K) \), \( \forall q\in A.\ \text{Minimum}(IntegerOrder,K) \leq F(q) \), \( \text{IsBounded}(K,IntegerOrder) \)
lemma (in int0) Int_ZF_1_3_L18:

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

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

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

shows \( n \leq abs(m) \), \( m\neq 0 \)
lemma (in int0) Int_ZF_2_L15A:

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

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

assumes \( a\in \mathbb{Z} \), \( b\in \mathbb{Z} \) and \( \neg (abs(a) \leq abs(b)) \)

shows \( \neg (abs(a) \leq 0 ) \)
lemma (in int0) Int_ineq_simpl_positive:

assumes \( a\in \mathbb{Z} \), \( b\in \mathbb{Z} \), \( c\in \mathbb{Z} \) and \( a\cdot c \leq b\cdot c \) and \( \neg (c\leq 0 ) \)

shows \( a \leq b \)
lemma (in group3) OrdGroup_6cases:

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

shows \( 1 \leq a \wedge 1 \leq b \vee a\leq 1 \wedge b\leq 1 \vee \) \( a\leq 1 \wedge 1 \leq b \wedge 1 \leq a\cdot b \vee a\leq 1 \wedge 1 \leq b \wedge a\cdot b \leq 1 \vee \) \( 1 \leq a \wedge b\leq 1 \wedge 1 \leq a\cdot b \vee 1 \leq a \wedge b\leq 1 \wedge a\cdot b \leq 1 \)