IsarMathLib

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

theory Int_ZF_IML imports OrderedGroup_ZF_1 Finite_ZF_1 ZF.Int Nat_ZF_IML

begin

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

Addition and multiplication as ZF-functions.

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

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

definition

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

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

definition

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

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

definition

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

This defines the set of positive integers.

definition

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

IntegerAddition and IntegerMultiplication are functions on $ int \times int $.

lemma Int_ZF_1_L1:

shows $ IntegerAddition : int\times int \rightarrow int $, $ IntegerMultiplication : int\times int \rightarrow int $proof

have $ \{\langle x,c\rangle \in (int\times int)\times int.\ \text{fst}(x) \ \$ + \text{snd}(x) = c\} \in int\times int\rightarrow int $, $ \{\langle x,c\rangle \in (int\times int)\times int.\ \text{fst}(x) \ \$ * \text{snd}(x) = c\} \in int\times int\rightarrow int $ using func1_1_L11A

then show $ IntegerAddition : int\times int \rightarrow int $, $ IntegerMultiplication : int\times int \rightarrow int $ using IntegerAddition_def, IntegerMultiplication_def

qed

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

locale int0

defines $ \mathbb{Z} \equiv int $

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

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

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

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

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

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

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

defines $ 2 \equiv 1 + 1 $

defines $ 3 \equiv 2 + 1 $

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

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

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

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

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

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

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

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

lemma (in int0) Int_ZF_1_L2:

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

shows $ a + b = a \ \$ + b $, $ a\cdot b = a \ \$ * b $proof

let $ x = \langle a,b\rangle $

let $ c = a \ \$ + b $

let $ d = a \ \$ * b $

from A1 have $ \langle x,c\rangle \in \{\langle x,c\rangle \in (\mathbb{Z} \times \mathbb{Z} )\times \mathbb{Z} .\ \text{fst}(x) \ \$ + \text{snd}(x) = c\} $, $ \langle x,d\rangle \in \{\langle x,d\rangle \in (\mathbb{Z} \times \mathbb{Z} )\times \mathbb{Z} .\ \text{fst}(x) \ \$ * \text{snd}(x) = d\} $

then show $ a + b = a \ \$ + b $, $ a\cdot b = a \ \$ * b $ using IntegerAddition_def, IntegerMultiplication_def, Int_ZF_1_L1, apply_iff

qed

Integer addition and multiplication are associative.

lemma (in int0) Int_ZF_1_L3:

assumes $ x\in \mathbb{Z} $, $ y\in \mathbb{Z} $, $ z\in \mathbb{Z} $

shows $ x + y + z = x + (y + z) $, $ x\cdot y\cdot z = x\cdot (y\cdot z) $ using assms, Int_ZF_1_L2, zadd_assoc, zmult_assoc

Integer addition and multiplication are commutative.

lemma (in int0) Int_ZF_1_L4:

assumes $ x\in \mathbb{Z} $, $ y\in \mathbb{Z} $

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

Zero is neutral for addition and one for multiplication.

lemma (in int0) Int_ZF_1_L5:

assumes A1: $ x\in \mathbb{Z} $

shows $ (\ \$ # 0) + x = x \wedge x + (\ \$ # 0) = x $, $ (\ \$ # 1)\cdot x = x \wedge x\cdot (\ \$ # 1) = x $proof

from A1 show $ (\ \$ # 0) + x = x \wedge x + (\ \$ # 0) = x $ using Int_ZF_1_L2, zadd_int0, Int_ZF_1_L4

from A1 have $ (\ \$ # 1)\cdot x = x $ using Int_ZF_1_L2, zmult_int1

with A1 show $ (\ \$ # 1)\cdot x = x \wedge x\cdot (\ \$ # 1) = x $ using Int_ZF_1_L4

qed

Zero is neutral for addition and one for multiplication.

lemma (in int0) Int_ZF_1_L6:

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

Integers with addition and integers with multiplication form monoids.

theorem (in int0) Int_ZF_1_T1:

shows $ \text{IsAmonoid}(\mathbb{Z} ,IntegerAddition) $, $ \text{IsAmonoid}(\mathbb{Z} ,IntegerMultiplication) $proof

have $ \exists e\in \mathbb{Z} .\ \forall x\in \mathbb{Z} .\ e + x = x \wedge x + e = x $, $ \exists e\in \mathbb{Z} .\ \forall x\in \mathbb{Z} .\ e\cdot x = x \wedge x\cdot e = x $ using Int_ZF_1_L6

then show $ \text{IsAmonoid}(\mathbb{Z} ,IntegerAddition) $, $ \text{IsAmonoid}(\mathbb{Z} ,IntegerMultiplication) $ using IsAmonoid_def, IsAssociative_def, Int_ZF_1_L1, Int_ZF_1_L3

qed

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

lemma (in int0) Int_ZF_1_L8:

shows $ (\ \$ # 0) = 0 $, $ (\ \$ # 1) = 1 $proof

have $ monoid0(\mathbb{Z} ,IntegerAddition) $ using Int_ZF_1_T1, monoid0_def

moreover

have $ (\ \$ # 0)\in \mathbb{Z} \wedge $ $ (\forall x\in \mathbb{Z} .\ IntegerAddition\langle \ \$ # 0,x\rangle = x \wedge $ $ IntegerAddition\langle x ,\ \$ # 0\rangle = x) $ using Int_ZF_1_L6

ultimately have $ (\ \$ # 0) = \text{ TheNeutralElement}(\mathbb{Z} ,IntegerAddition) $ by (rule group0_1_L4 )

then show $ (\ \$ # 0) = 0 $

have $ monoid0(int,IntegerMultiplication) $ using Int_ZF_1_T1, monoid0_def

moreover

have $ (\ \$ # 1) \in int \wedge $ $ (\forall x\in int.\ IntegerMultiplication\langle \ \$ # 1, x\rangle = x \wedge $ $ IntegerMultiplication\langle x ,\ \$ # 1\rangle = x) $ using Int_ZF_1_L6

ultimately have $ (\ \$ # 1) = \text{ TheNeutralElement}(int,IntegerMultiplication) $ by (rule group0_1_L4 )

then show $ (\ \$ # 1) = 1 $

qed

$0$ and $1$, as defined in int0 context, are integers.

lemma (in int0) Int_ZF_1_L8A:

shows $ 0 \in \mathbb{Z} $, $ 1 \in \mathbb{Z} $proof

have $ (\ \$ # 0) \in \mathbb{Z} $, $ (\ \$ # 1) \in \mathbb{Z} $

then show $ 0 \in \mathbb{Z} $, $ 1 \in \mathbb{Z} $ using Int_ZF_1_L8

qed

Zero is not one.

lemma (in int0) int_zero_not_one:

shows $ 0 \neq 1 $proof

have $ (\ \$ # 0) \neq (\ \$ # 1) $

then show $ 0 \neq 1 $ using Int_ZF_1_L8

qed

The set of integers is not empty, of course.

lemma (in int0) int_not_empty:

shows $ \mathbb{Z} \neq 0 $ using Int_ZF_1_L8A

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

lemma (in int0) int_not_trivial:

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

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

lemma (in int0) Int_ZF_1_L9:

assumes A1: $ g \in \mathbb{Z} $

shows $ \exists b\in \mathbb{Z} .\ g + b = 0 $proof

from A1 have $ g + \ \$ -g = 0 $ using Int_ZF_1_L2, Int_ZF_1_L8

thus $ thesis $

qed

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

theorem Int_ZF_1_T2:

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

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

lemma (in int0) Int_ZF_1_L9A:

assumes A1: $ m\in \mathbb{Z} $

shows $ \ \$ -m = - m $proof

from A1 have $ m\in int $, $ \ \$ -m \in int $, $ IntegerAddition\langle m,\ \$ -m\rangle = $ $ \text{ TheNeutralElement}(int,IntegerAddition) $ using zminus_type, Int_ZF_1_L2, Int_ZF_1_L8

then have $ \ \$ -m = \text{GroupInv}(int,IntegerAddition)(m) $ using Int_ZF_1_T2, group0_2_L9

then show $ thesis $

qed

Subtracting integers corresponds to adding the negative.

lemma (in int0) Int_ZF_1_L10:

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

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

Negative of zero is zero.

lemma (in int0) Int_ZF_1_L11:

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

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

lemma Int_ZF_1_L12:

assumes $ m\in int $

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

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

lemma (in int0) Int_ZF_1_L13:

assumes $ m\in \mathbb{Z} $

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

Adding or subtracing one changes integers.

lemma (in int0) Int_ZF_1_L14:

assumes A1: $ m\in \mathbb{Z} $

shows $ m + 1 \neq m $, $ m - 1 \neq m $proof

{

assume $ m + 1 = m $

with A1 have $ group0(\mathbb{Z} ,IntegerAddition) $, $ m\in \mathbb{Z} $, $ 1 \in \mathbb{Z} $, $ IntegerAddition\langle m,1 \rangle = m $ using Int_ZF_1_T2, Int_ZF_1_L8A

then have $ 1 = \text{ TheNeutralElement}(\mathbb{Z} ,IntegerAddition) $ by (rule group0_2_L7 )

then have $ False $ using int_zero_not_one

}

then show I: $ m + 1 \neq m $

{

from A1 have $ m - 1 + 1 = m $ using Int_ZF_1_L8A, Int_ZF_1_T2, inv_cancel_two

moreover

assume $ m - 1 = m $

ultimately have $ m + 1 = m $

with I have $ False $

}

then show $ m - 1 \neq m $

qed

If the difference is zero, the integers are equal.

lemma (in int0) Int_ZF_1_L15:

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

shows $ m=n $proof

let $ G = \mathbb{Z} $

let $ f = IntegerAddition $

from A1, A2 have $ group0(G, f) $, $ m \in G $, $ n \in G $, $ f\langle m, \text{GroupInv}(G, f)(n)\rangle = \text{ TheNeutralElement}(G, f) $ using Int_ZF_1_T2

then show $ m=n $ by (rule group0_2_L11A )

qed

Integers as an ordered group

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

The next lemma interprets the order definition one way.

lemma (in int0) Int_ZF_2_L1:

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

shows $ m \leq n $proof

from A1, A2 have $ \langle m,n\rangle \in \{x\in \mathbb{Z} \times \mathbb{Z} .\ \text{fst}(x) \ \$ \leq \text{snd}(x)\} $

then show $ thesis $ using IntegerOrder_def

qed

The next lemma interprets the definition the other way.

lemma (in int0) Int_ZF_2_L1A:

assumes A1: $ m \leq n $

shows $ m \ \$ \leq n $, $ m\in \mathbb{Z} $, $ n\in \mathbb{Z} $proof

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

thus $ m \ \$ \leq n $, $ m\in \mathbb{Z} $, $ n\in \mathbb{Z} $

qed

Integer order is a relation on integers.

lemma Int_ZF_2_L1B:

shows $ IntegerOrder \subseteq int\times int $proof

fix $ x $

assume $ x\in IntegerOrder $

then have $ x \in \{p\in int\times int.\ \text{fst}(p) \ \$ \leq \text{snd}(p)\} $ using IntegerOrder_def

then show $ x\in int\times int $

qed

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

lemma (in int0) Int_ZF_2_L1C:

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

shows $ A\subseteq \mathbb{Z} $proof

from A1 have $ IntegerOrder \subseteq \mathbb{Z} \times \mathbb{Z} $, $ \text{IsBoundedBelow}(A,IntegerOrder) $ using Int_ZF_2_L1B

then show $ A\subseteq \mathbb{Z} $ by (rule Order_ZF_3_L1B )

qed

The order on integers is reflexive.

lemma (in int0) int_ord_is_refl:

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

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

lemma (in int0) Int_ZF_2_L3:

assumes A1: $ m \leq n $, $ n \leq m $

shows $ m=n $proof

from A1 have $ m \ \$ \leq n $, $ n \ \$ \leq m $, $ m\in \mathbb{Z} $, $ n\in \mathbb{Z} $ using Int_ZF_2_L1A

then show $ m=n $ using zle_anti_sym

qed

The order on integers is antisymmetric.

lemma (in int0) Int_ZF_2_L4:

shows $ \text{antisym}(IntegerOrder) $proof

have $ \forall m n.\ m \leq n \wedge n \leq m \longrightarrow m=n $ using Int_ZF_2_L3

then show $ thesis $ using imp_conj, antisym_def

qed

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

lemma Int_ZF_2_L5:

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

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

from A1 have T1: $ m \ \$ \leq n $, $ n \ \$ \leq k $ and T2: $ m\in int $, $ k\in int $ using Int_ZF_2_L1A

from T1 have $ m \ \$ \leq k $ by (rule zle_trans )

with T2 show $ thesis $ using Int_ZF_2_L1

qed

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

lemma (in int0) Int_order_transitive:

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

shows $ m\leq k $proof

from A1 have $ \langle m,n\rangle \in IntegerOrder $, $ \langle n,k\rangle \in IntegerOrder $

then have $ \langle m,k\rangle \in IntegerOrder $ by (rule Int_ZF_2_L5 )

then show $ m\leq k $

qed

The order on integers is transitive.

lemma Int_ZF_2_L6:

shows $ \text{trans}(IntegerOrder) $proof

have $ \forall m n k.\ $ $ \langle m, n\rangle \in IntegerOrder \wedge \langle n, k\rangle \in IntegerOrder \longrightarrow $ $ \langle m, k\rangle \in IntegerOrder $ using Int_ZF_2_L5

then show $ thesis $ by (rule Fol1_L2 )

qed

The order on integers is a partial order.

lemma Int_ZF_2_L7:

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

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

lemma (in int0) int_ord_transl_inv:

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

shows $ m + k \leq n + k $, $ k + m\leq k + n $proof

from A2 have $ m \ \$ \leq n $ and $ m\in \mathbb{Z} $, $ n\in \mathbb{Z} $ using Int_ZF_2_L1A

with A1 show $ m + k \leq n + k $, $ k + m\leq k + n $ using zadd_right_cancel_zle, zadd_left_cancel_zle, Int_ZF_1_L2, Int_ZF_1_L1, apply_funtype, Int_ZF_1_L2, Int_ZF_2_L1, Int_ZF_1_L2

qed

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

theorem (in int0) Int_ZF_2_T1:

shows $ \text{IsAnOrdGroup}(\mathbb{Z} ,IntegerAddition,IntegerOrder) $, $ IntegerOrder \text{ is total on } \mathbb{Z} $, $ group3(\mathbb{Z} ,IntegerAddition,IntegerOrder) $, $ \text{IsLinOrder}(\mathbb{Z} ,IntegerOrder) $proof

have $ \forall k\in \mathbb{Z} .\ \forall m n.\ m \leq n \longrightarrow $ $ m + k \leq n + k \wedge k + m\leq k + n $ using int_ord_transl_inv

then show T1: $ \text{IsAnOrdGroup}(\mathbb{Z} ,IntegerAddition,IntegerOrder) $ using Int_ZF_1_T2, Int_ZF_2_L1B, Int_ZF_2_L7, IsAnOrdGroup_def

then show $ group3(\mathbb{Z} ,IntegerAddition,IntegerOrder) $ using group3_def

have $ \forall n\in \mathbb{Z} .\ \forall m\in \mathbb{Z} .\ n\leq m \vee m\leq n $ using zle_linear, Int_ZF_2_L1

then show $ IntegerOrder \text{ is total on } \mathbb{Z} $ using IsTotal_def

with T1 show $ \text{IsLinOrder}(\mathbb{Z} ,IntegerOrder) $ using IsAnOrdGroup_def, IsPartOrder_def, IsLinOrder_def

qed

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

lemma (in int0) Int_ZF_2_L9:

assumes A1: $ i \leq m $ and A2: $ i\neq m $

shows $ i \ \$ \lt m $proof

from A1 have $ i \ \$ \leq m $, $ i\in \mathbb{Z} $, $ m\in \mathbb{Z} $ using Int_ZF_2_L1A

with A2 show $ i \ \$ \lt m $ using zle_def

qed

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

lemma (in int0) Int_ZF_2_L9AA:

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

shows $ m\leq n $, $ m \neq n $ using assms, zle_def, Int_ZF_2_L1

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

lemma (in int0) Int_ZF_2_L9A:

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

shows $ m + 1 \leq k $proof

from A2 have $ m + 1 \leq (k \ \$ - (\ \$ # 1)) + 1 $ using Int_ZF_1_L8A, int_ord_transl_inv

with A1 show $ m + 1 \leq k $ using Int_ZF_1_L13

qed

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

lemma (in int0) Int_ZF_2_L9B:

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

shows $ i + m \leq k \longleftrightarrow i \leq k - m $ using assms, Int_ZF_2_T1, OrderedGroup_ZF_1_L9A

A special case of Int_ZF_2_L9B with weaker assumptions.

lemma (in int0) Int_ZF_2_L9C:

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

shows $ i \leq k + m $ using assms, Int_ZF_2_T1, OrderedGroup_ZF_1_L9B

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

lemma (in int0) Int_ZF_2_L10:

assumes $ k \leq i $

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

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

lemma (in int0) Int_ZF_2_L10AA:

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

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

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

lemma (in int0) Int_ZF_2_L10AB:

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

shows $ k\leq n $ using assms, Int_ZF_2_T1, OrderedGroup_ZF_1_L5AF

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

lemma (in int0) Int_ZF_2_L10A:

assumes $ k \leq 0 $

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

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

lemma (in int0) Int_ZF_2_L10B:

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

shows $ k\leq 0 $ using assms, Int_ZF_2_T1, OrderedGroup_ZF_1_L5AA

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

lemma (in int0) Int_ZF_2_L11:

shows $ i \ \$ + \ \$ # n \ \$ + (\ \$ # 1) = i \ \$ + \ \$ # succ(n) $proof

have $ \ \$ # succ(n) = \ \$ #1 \ \$ + \ \$ # n $ using int_succ_int_1

then have $ i \ \$ + \ \$ # succ(n) = i \ \$ + (\ \$ # n \ \$ + \ \$ #1) $ using zadd_commute

then show $ thesis $ using zadd_assoc

qed

Adding a natural number increases integers.

lemma (in int0) Int_ZF_2_L12:

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

shows $ i \leq i \ \$ + \ \$ #n $proof

{

assume $ n = 0 $

with A1 have $ i \leq i \ \$ + \ \$ #n $ using zadd_int0, int_ord_is_refl, refl_def

}

moreover {

assume $ n\neq 0 $

with A2 obtain $ k $ where $ k\in nat $, $ n = succ(k) $ using Nat_ZF_1_L3

with A1 have $ i \leq i \ \$ + \ \$ #n $ using zless_succ_zadd, zless_imp_zle, Int_ZF_2_L1

} ultimately show $ thesis $

qed

Adding one increases integers.

lemma (in int0) Int_ZF_2_L12A:

assumes A1: $ j\leq k $

shows $ j \leq k \ \$ + \ \$ #1 $, $ j \leq k + 1 $proof

from A1 have T1: $ j\in \mathbb{Z} $, $ k\in \mathbb{Z} $, $ j \ \$ \leq k $ using Int_ZF_2_L1A

moreover

from T1 have $ k \ \$ \leq k \ \$ + \ \$ #1 $ using Int_ZF_2_L12, Int_ZF_2_L1A

ultimately have $ j \ \$ \leq k \ \$ + \ \$ #1 $ using zle_trans

with T1 show $ j \leq k \ \$ + \ \$ #1 $ using Int_ZF_2_L1

with T1 have $ j\leq k + \ \$ #1 $ using Int_ZF_1_L2

then show $ j \leq k + 1 $ using Int_ZF_1_L8

qed

Adding one increases integers, yet one more version.

lemma (in int0) Int_ZF_2_L12B:

assumes A1: $ m\in \mathbb{Z} $

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

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

lemma (in int0) Int_ZF_2_L13:

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

shows $ m \leq k $proof

from A1 have $ k\in \mathbb{Z} $, $ m \ \$ + \ \$ # n \in \mathbb{Z} $

moreover

from assms have $ k \ \$ + \ \$ # 1 = m \ \$ + \ \$ # n \ \$ + \ \$ #1 $ using Int_ZF_2_L11

ultimately have $ k = m \ \$ + \ \$ # n $ using zadd_right_cancel

with A1, A2 show $ thesis $ using Int_ZF_2_L12

qed

The absolute value of an integer is an integer.

lemma (in int0) Int_ZF_2_L14:

assumes A1: $ m\in \mathbb{Z} $

shows $ abs(m) \in \mathbb{Z} $proof

have $ \text{AbsoluteValue}(\mathbb{Z} ,IntegerAddition,IntegerOrder) : \mathbb{Z} \rightarrow \mathbb{Z} $ using Int_ZF_2_T1, OrderedGroup_ZF_3_L1

with A1 show $ thesis $ using apply_funtype

qed

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

lemma (in int0) Int_ZF_2_L14A:

assumes $ 0 \leq m $, $ 0 \leq n $

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

We can increase components in an estimate.

lemma (in int0) Int_ZF_2_L15:

assumes $ b\leq b_1 $, $ c\leq c_1 $ and $ a\leq b + c $

shows $ a\leq b_1 + c_1 $proof

from assms have $ group3(\mathbb{Z} ,IntegerAddition,IntegerOrder) $, $ \langle a,IntegerAddition\langle b,c\rangle \rangle \in IntegerOrder $, $ \langle b,b_1\rangle \in IntegerOrder $, $ \langle c,c_1\rangle \in IntegerOrder $ using Int_ZF_2_T1

then have $ \langle a,IntegerAddition\langle b_1,c_1\rangle \rangle \in IntegerOrder $ by (rule OrderedGroup_ZF_1_L5E )

thus $ thesis $

qed

We can add or subtract the sides of two inequalities.

lemma (in int0) int_ineq_add_sides:

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

shows $ a + c \leq b + d $, $ a - d \leq b - c $ using assms, Int_ZF_2_T1, OrderedGroup_ZF_1_L5B, OrderedGroup_ZF_1_L5I

We can increase the second component in an estimate.

lemma (in int0) Int_ZF_2_L15A:

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

shows $ a\leq b + c_1 $proof

from assms have $ group3(\mathbb{Z} ,IntegerAddition,IntegerOrder) $, $ b \in \mathbb{Z} $, $ \langle a,IntegerAddition\langle b,c\rangle \rangle \in IntegerOrder $, $ \langle c,c_1\rangle \in IntegerOrder $ using Int_ZF_2_T1

then have $ \langle a,IntegerAddition\langle b,c_1\rangle \rangle \in IntegerOrder $ by (rule OrderedGroup_ZF_1_L5D )

thus $ thesis $

qed

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

lemma (in int0) Int_ZF_2_L15C:

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

shows $ m + k + n \leq m + L + n $proof

let $ P = IntegerAddition $

from assms have $ group3(int,P,IntegerOrder) $, $ m \in int $, $ n \in int $, $ \langle k,L\rangle \in IntegerOrder $ using Int_ZF_2_T1

then have $ \langle P\langle P\langle m,k\rangle ,n\rangle , P\langle P\langle m,L\rangle ,n\rangle \rangle \in IntegerOrder $ by (rule OrderedGroup_ZF_1_L10 )

then show $ m + k + n \leq m + L + n $

qed

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

lemma (in int0) Int_ZF_2_L15D:

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

shows $ m \leq n + m $ using assms, Int_ZF_2_T1, OrderedGroup_ZF_1_L5F

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

lemma (in int0) Int_ZF_2_L15E:

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

shows $ m + n \leq abs(m) + abs(n) $, $ m - n \leq abs(m) + abs(n) $, $ ( - m) + n \leq abs(m) + abs(n) $, $ ( - m) - n \leq abs(m) + abs(n) $ using assms, Int_ZF_2_T1, OrderedGroup_ZF_3_L6A

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

lemma (in int0) Int_ZF_2_L15F:

assumes $ m\leq k $ and $ 0 \leq n $

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

Triangle inequality for integers.

lemma (in int0) Int_triangle_ineq:

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

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

Taking absolute value does not change nonnegative integers.

lemma (in int0) Int_ZF_2_L16:

assumes $ 0 \leq m $

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

$0\leq 1$, so $|1| = 1$.

lemma (in int0) Int_ZF_2_L16A:

shows $ 0 \leq 1 $ and $ abs(1 ) = 1 $proof

have $ (\ \$ # 0) \in \mathbb{Z} $, $ (\ \$ # 1)\in \mathbb{Z} $

then have $ 0 \leq 0 $ and T1: $ 1 \in \mathbb{Z} $ using Int_ZF_1_L8, int_ord_is_refl, refl_def

then have $ 0 \leq 0 + 1 $ using Int_ZF_2_L12A

with T1 show $ 0 \leq 1 $ using Int_ZF_1_T2, group0_2_L2

then show $ abs(1 ) = 1 $ using Int_ZF_2_L16

qed

$1\leq 2$.

lemma (in int0) Int_ZF_2_L16B:

shows $ 1 \leq 2 $proof

have $ (\ \$ # 1)\in \mathbb{Z} $

then show $ 1 \leq 2 $ using Int_ZF_1_L8, int_ord_is_refl, refl_def, Int_ZF_2_L12A

qed

Integers greater or equal one are greater or equal zero.

lemma (in int0) Int_ZF_2_L16C:

assumes A1: $ 1 \leq a $

shows $ 0 \leq a $, $ a\neq 0 $, $ 2 \leq a + 1 $, $ 1 \leq a + 1 $, $ 0 \leq a + 1 $proof

from A1 have $ 0 \leq 1 $ and $ 1 \leq a $ using Int_ZF_2_L16A

then show $ 0 \leq a $ by (rule Int_order_transitive )

have I: $ 0 \leq 1 $ using Int_ZF_2_L16A

have $ 1 \leq 2 $ using Int_ZF_2_L16B

moreover

from A1 show $ 2 \leq a + 1 $ using Int_ZF_1_L8A, int_ord_transl_inv

ultimately show $ 1 \leq a + 1 $ by (rule Int_order_transitive )

with I show $ 0 \leq a + 1 $ by (rule Int_order_transitive )

from A1 show $ a\neq 0 $ using Int_ZF_2_L16A, Int_ZF_2_L3, int_zero_not_one

qed

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

lemma (in int0) Int_ZF_2_L17:

assumes $ m\in \mathbb{Z} $

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

The absolute value of zero is zero.

lemma (in int0) Int_ZF_2_L18:

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

A different version of the triangle inequality.

lemma (in int0) Int_triangle_ineq1:

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

shows $ abs(m - n) \leq abs(n) + abs(m) $, $ abs(m - n) \leq abs(m) + abs(n) $proof

have $ \ \$ -n \in \mathbb{Z} $

with A1 have $ abs(m - n) \leq abs(m) + abs( - n) $ using Int_ZF_1_L9A, Int_triangle_ineq

with A1 show $ abs(m - n) \leq abs(n) + abs(m) $, $ abs(m - n) \leq abs(m) + abs(n) $ using Int_ZF_2_L17, Int_ZF_2_L14, Int_ZF_1_T2, IsCommutative_def

qed

Another version of the triangle inequality.

lemma (in int0) Int_triangle_ineq2:

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

shows $ abs(m) \leq abs(n) + k $, $ m - k \leq n $, $ m \leq n + k $, $ n - k \leq m $ using assms, Int_ZF_1_T2, Int_ZF_2_T1, OrderedGroup_ZF_3_L7D, OrderedGroup_ZF_3_L7E

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

lemma (in int0) Int_triangle_ineq3:

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

shows $ abs(m + n + k) \leq abs(m) + abs(n) + abs(k) $proof

from A1 have T: $ m + n \in \mathbb{Z} $, $ abs(k) \in \mathbb{Z} $ using Int_ZF_1_T2, group_op_closed, Int_ZF_2_L14

with A1 have $ abs(m + n + k) \leq abs(m + n) + abs(k) $ using Int_triangle_ineq

moreover

from A1, T have $ abs(m + n) + abs(k) \leq abs(m) + abs(n) + abs(k) $ using Int_triangle_ineq, int_ord_transl_inv

ultimately show $ thesis $ by (rule Int_order_transitive )

qed

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

lemma (in int0) Int_ZF_2_L19:

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

shows $ m\leq n $, $ ( - n) \leq ( - m) $, $ m\neq n $proof

from A1, A2 show $ m\leq n $ using Int_ZF_2_T1, IsTotal_def

then show $ ( - n) \leq ( - m) $ using Int_ZF_2_L10

from A1 have $ n \leq n $ using int_ord_is_refl, refl_def

with A2 show $ m\neq n $

qed

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

lemma (in int0) Int_ZF_2_L19AA:

assumes A1: $ m\leq n $ and A2: $ m\neq n $

shows $ \neg (n\leq m) $proof

from A1, A2 have $ group3(\mathbb{Z} , IntegerAddition, IntegerOrder) $, $ \langle m,n\rangle \in IntegerOrder $, $ m\neq n $ using Int_ZF_2_T1

then have $ \langle n,m\rangle \notin IntegerOrder $ by (rule OrderedGroup_ZF_1_L8AA )

thus $ \neg (n\leq m) $

qed

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

lemma (in int0) Int_ZF_2_L19A:

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

shows $ m\leq 0 $, $ 0 \leq ( - m) $, $ m\neq 0 $proof

from A1 have T: $ 0 \in \mathbb{Z} $ using Int_ZF_1_T2, group0_2_L2

with A1, A2 show $ m\leq 0 $ using Int_ZF_2_L19

from A1, T, A2 show $ m\neq 0 $ by (rule Int_ZF_2_L19 )

from A1, T, A2 have $ ( - 0 )\leq ( - m) $ by (rule Int_ZF_2_L19 )

then show $ 0 \leq ( - m) $ using Int_ZF_1_T2, group_inv_of_one

qed

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

lemma (in int0) Int_ZF_2_L19B:

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

shows $ Q(m) $proof

let $ G = \mathbb{Z} $

let $ P = IntegerAddition $

let $ r = IntegerOrder $

let $ b = m $

from assms have $ group3(G, P, r) $, $ r \text{ is total on } G $, $ b \in G $, $ Q(\text{ TheNeutralElement}(G, P)) $, $ \forall a\in \text{PositiveSet}(G, P, r).\ Q(a) $, $ \forall a\in \text{PositiveSet}(G, P, r).\ Q( \text{GroupInv}(G, P)(a)) $ using Int_ZF_2_T1

then show $ Q(b) $ by (rule OrderedGroup_ZF_1_L18 )

qed

An integer is not greater than its absolute value.

lemma (in int0) Int_ZF_2_L19C:

assumes A1: $ m\in \mathbb{Z} $

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

$|m-n| = |n-m|$.

lemma (in int0) Int_ZF_2_L20:

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

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

We can add the sides of inequalities with absolute values.

lemma (in int0) Int_ZF_2_L21:

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

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

Absolute value is nonnegative.

lemma (in int0) int_abs_nonneg:

assumes A1: $ m\in \mathbb{Z} $

shows $ abs(m) \in \mathbb{Z} ^+ $, $ 0 \leq abs(m) $proof

have $ \text{AbsoluteValue}(\mathbb{Z} ,IntegerAddition,IntegerOrder) : \mathbb{Z} \rightarrow \mathbb{Z} ^+ $ using Int_ZF_2_T1, OrderedGroup_ZF_3_L3C

with A1 show $ abs(m) \in \mathbb{Z} ^+ $ using apply_funtype

then show $ 0 \leq abs(m) $ using Int_ZF_2_T1, OrderedGroup_ZF_1_L2

qed

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

lemma (in int0) Int_ZF_2_L23:

assumes $ 0 \leq m $, $ m\leq k $

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

Induction on integers.

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

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

lemma (in int0) Int_ZF_3_L2:

assumes A1: $ i \leq m $

shows $ \exists n\in nat.\ m = i \ \$ + \ \$ # n $proof

let $ n = 0 $

{

assume A2: $ i=m $

from A1, A2 have $ n \in nat $, $ m = i \ \$ + \ \$ # n $ using Int_ZF_2_L1A, zadd_int0_right

hence $ \exists n\in nat.\ m = i \ \$ + \ \$ # n $

}

moreover {

assume A3: $ i\neq m $

with A1 have $ i \ \$ \lt m $, $ i\in \mathbb{Z} $, $ m\in \mathbb{Z} $ using Int_ZF_2_L9, Int_ZF_2_L1A

then obtain $ k $ where D1: $ k\in nat $, $ m = i \ \$ + \ \$ # succ(k) $ using zless_imp_succ_zadd_lemma

let $ n = succ(k) $

from D1 have $ n\in nat $, $ m = i \ \$ + \ \$ # n $

hence $ \exists n\in nat.\ m = i \ \$ + \ \$ # n $

} ultimately show $ thesis $

qed

Induction for integers, the induction step.

lemma (in int0) Int_ZF_3_L6:

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

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

fix $ k $

assume A3: $ k\in nat $

show $ Q(i \ \$ + \ \$ # k) \longrightarrow Q(i \ \$ + \ \$ # succ(k)) $proof

assume A4: $ Q(i \ \$ + \ \$ # k) $

from A1, A3 have $ i\leq i \ \$ + (\ \$ # k) $ using Int_ZF_2_L12

with A4, A2 have $ Q(i \ \$ + (\ \$ # k) \ \$ + (\ \$ # 1)) $

then show $ Q(i \ \$ + (\ \$ # succ(k))) $ using Int_ZF_2_L11

qed

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

lemma (in int0) Int_ZF_3_L7:

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

shows $ Q(k) $proof

from A1 obtain $ n $ where D1: $ n\in nat $ and D2: $ k = i \ \$ + \ \$ # n $ using Int_ZF_3_L2

from A1 have T1: $ i\in \mathbb{Z} $ using Int_ZF_2_L1A

note $ n\in nat $

moreover

from A1, A2 have $ Q(i \ \$ + \ \$ #0) $ using Int_ZF_2_L1A, zadd_int0

moreover

from T1, A3 have $ \forall k\in nat.\ Q(i \ \$ + (\ \$ # k)) \longrightarrow Q(i \ \$ + (\ \$ # succ(k))) $ by (rule Int_ZF_3_L6 )

ultimately have $ Q(i \ \$ + (\ \$ # n)) $ by (rule ind_on_nat )

with D2 show $ Q(k) $

qed

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

lemma (in int0) Int_ZF_3_L7A:

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

shows $ \forall m.\ i\leq m \wedge Q(m) \longrightarrow Q(m \ \$ + (\ \$ # 1)) $proof

{

fix $ m $

assume $ i\leq m \wedge Q(m) $

with A1 have T1: $ m\in \mathbb{Z} $, $ Q(m + 1 ) $ using Int_ZF_2_L1A

then have $ m + 1 = m + (\ \$ # 1) $ using Int_ZF_1_L8

with T1 have $ Q(m \ \$ + (\ \$ # 1)) $ using Int_ZF_1_L2

}

then show $ thesis $

qed

Induction on integers, version with ZF increment function.

theorem (in int0) Induction_on_int:

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

shows $ Q(k) $proof

from A3 have $ \forall m.\ i\leq m \wedge Q(m) \longrightarrow Q(m \ \$ + (\ \$ # 1)) $ by (rule Int_ZF_3_L7A )

with A1, A2 show $ thesis $ by (rule Int_ZF_3_L7 )

qed

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

lemma (in int0) Int_ZF_3_L7B:

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

shows $ P(\ \$ -k) $proof

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

qed

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

lemma (in int0) Int_ZF_3_L8:

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

shows $ P(k) $proof

from A1 have T1: $ \ \$ -i\leq \ \$ -k $ using Int_ZF_2_L10

from A1, A2 have T2: $ P(\ \$ - \ \$ - i) $ using Int_ZF_2_L1A, zminus_zminus

from T1, T2, A3 have $ P(\ \$ -(\ \$ -k)) $ by (rule Int_ZF_3_L7 )

with A1 show $ P(k) $ using Int_ZF_2_L1A, zminus_zminus

qed

An implication between two forms of induction steps.

lemma (in int0) Int_ZF_3_L9:

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

shows $ \forall m.\ \ \$ -i\leq m \wedge P(\ \$ -m) \longrightarrow P(\ \$ -(m \ \$ + (\ \$ # 1))) $proof

fix $ m $

show $ \ \$ -i\leq m \wedge P(\ \$ -m) \longrightarrow P(\ \$ -(m \ \$ + (\ \$ # 1))) $proof

assume A3: $ \ \$ - i \leq m \wedge P(\ \$ - m) $

then have $ \ \$ - i \leq m $

then have $ \ \$ -m \leq \ \$ - (\ \$ - i) $ by (rule Int_ZF_2_L10 )

with A1, A2, A3 show $ P(\ \$ -(m \ \$ + (\ \$ # 1))) $ using zminus_zminus, zminus_zadd_distrib

qed

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

lemma (in int0) Int_ZF_3_L9A:

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

shows $ P(k) $proof

from A1 have T1: $ i\in \mathbb{Z} $ using Int_ZF_2_L1A

from T1, A3 have T2: $ \forall m.\ \ \$ -i\leq m \wedge P(\ \$ -m) \longrightarrow P(\ \$ -(m \ \$ + (\ \$ # 1))) $ by (rule Int_ZF_3_L9 )

from A1, A2, T2 show $ P(k) $ by (rule Int_ZF_3_L8 )

qed

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

lemma (in int0) Int_ZF_3_L10:

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

shows $ \forall n.\ n\leq i \wedge P(n) \longrightarrow P(n \ \$ + \ \$ -(\ \$ #1)) $proof

{

fix $ n $

assume $ n\leq i \wedge P(n) $

with A1 have T1: $ n\in \mathbb{Z} $, $ P(n - 1 ) $ using Int_ZF_2_L1A

then have $ n - 1 = n - (\ \$ # 1) $ using Int_ZF_1_L8

with T1 have $ P(n \ \$ + \ \$ -(\ \$ #1)) $ using Int_ZF_1_L10

}

then show $ thesis $

qed

Backwards induction on integers.

theorem (in int0) Back_induct_on_int:

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

shows $ P(k) $proof

from A3 have $ \forall n.\ n\leq i \wedge P(n) \longrightarrow P(n \ \$ + \ \$ -(\ \$ #1)) $ by (rule Int_ZF_3_L10 )

with A1, A2 show $ P(k) $ by (rule Int_ZF_3_L9A )

qed

Bounded vs. finite subsets of integers

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

There are no integers between $k$ and $k+1$.

lemma (in int0) Int_ZF_4_L1:

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

shows $ m = k \ \$ + \ \$ #1 \vee m \leq k $proof

{

assume $ n=0 $

with A1, A2 have $ m = k \ \$ + \ \$ #1 \vee m \leq k $ using zadd_int0

}

moreover {

assume $ n\neq 0 $

with A1 obtain $ j $ where D1: $ j\in nat $, $ n = succ(j) $ using Nat_ZF_1_L3

with A1, A2, D1 have $ m = k \ \$ + \ \$ #1 \vee m \leq k $ using Int_ZF_2_L13

} ultimately show $ thesis $

qed

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

lemma Int_ZF_4_L1A:

assumes $ m\in int $

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

There are no integers between $k$ and $k+1$, another formulation.

lemma (in int0) Int_ZF_4_L1B:

assumes A1: $ m \leq L $

shows $ m = L \vee m + 1 \leq L $, $ m = L \vee m \leq L - 1 $proof

let $ k = L \ \$ - \ \$ #1 $

from A1 have T1: $ m\in \mathbb{Z} $, $ L\in \mathbb{Z} $, $ L = k \ \$ + \ \$ #1 $ using Int_ZF_2_L1A, Int_ZF_4_L1A

moreover

from A1 obtain $ n $ where D1: $ n\in nat $, $ L = m \ \$ + \ \$ # n $ using Int_ZF_3_L2

ultimately have $ m = L \vee m \leq k $ using Int_ZF_4_L1

with T1 show $ m = L \vee m + 1 \leq L $ using Int_ZF_2_L9A

with T1 show $ m = L \vee m \leq L - 1 $ using Int_ZF_1_L8A, Int_ZF_2_L9B

qed

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

lemma (in int0) Int_ZF_4_L2:

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

shows $ j \in m.\ .\ k \vee j \in \{k \ \$ + \ \$ #1\} $proof

from A2 have T1: $ m\leq j $, $ j\leq (k \ \$ + \ \$ #1) $ using Order_ZF_2_L1A

then have T2: $ m\in \mathbb{Z} $, $ j\in \mathbb{Z} $ using Int_ZF_2_L1A

from T1 obtain $ n $ where $ n\in nat $, $ k \ \$ + \ \$ #1 = j \ \$ + \ \$ # n $ using Int_ZF_3_L2

with A1, T1, T2 have $ (m\leq j \wedge j \leq k) \vee j \in \{k \ \$ + \ \$ #1\} $ using Int_ZF_4_L1

then show $ thesis $ using Order_ZF_2_L1B

qed

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

lemma (in int0) Int_ZF_4_L3:

assumes A1: $ m\leq k $

shows $ m.\ .\ (k \ \$ + \ \$ #1) = m.\ .\ k \cup \{k \ \$ + \ \$ #1\} $proof

from A1 have T1: $ m\in \mathbb{Z} $, $ k\in \mathbb{Z} $ using Int_ZF_2_L1A

then show $ m .\ .\ (k \ \$ + \ \$ # 1) \subseteq m .\ .\ k \cup \{k \ \$ + \ \$ # 1\} $ using Int_ZF_4_L2

from T1 have $ m\leq m $ using Int_ZF_2_T1, OrderedGroup_ZF_1_L3

with T1, A1 have $ m .\ .\ k \subseteq m .\ .\ (k \ \$ + \ \$ # 1) $ using Int_ZF_2_L12, Int_ZF_2_L6, Order_ZF_2_L3

with T1, A1 show $ m.\ .\ k \cup \{k \ \$ + \ \$ #1\} \subseteq m.\ .\ (k \ \$ + \ \$ #1) $ using Int_ZF_2_L12A, int_ord_is_refl, Order_ZF_2_L2

qed

Integer intervals are finite - induction step.

lemma (in int0) Int_ZF_4_L4:

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

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

Integer intervals are finite.

lemma (in int0) Int_ZF_4_L5:

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

shows $ i.\ .\ k \in Fin(\mathbb{Z} ) $proof

{

assume A2: $ i\leq k $

moreover

from A1 have $ i.\ .\ i \in Fin(\mathbb{Z} ) $ using int_ord_is_refl, Int_ZF_2_L4, Order_ZF_2_L4

moreover

from A2 have $ \forall m.\ i\leq m \wedge i.\ .\ m \in Fin(\mathbb{Z} ) \longrightarrow i.\ .\ (m \ \$ + \ \$ #1) \in Fin(\mathbb{Z} ) $ using Int_ZF_4_L4

ultimately have $ i.\ .\ k \in Fin(\mathbb{Z} ) $ by (rule Int_ZF_3_L7 )

}

moreover {

assume $ \neg i \leq k $

then have $ i.\ .\ k \in Fin(\mathbb{Z} ) $ using Int_ZF_2_L6, Order_ZF_2_L5

} ultimately show $ thesis $

qed

Bounded integer sets are finite.

lemma (in int0) Int_ZF_4_L6:

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

shows $ A \in Fin(\mathbb{Z} ) $proof

have T1: $ \forall m \in \text{Nonnegative}(\mathbb{Z} ,IntegerAddition,IntegerOrder).\ $ $ \ \$ #0.\ .\ m \in Fin(\mathbb{Z} ) $proof

fix $ m $

assume $ m \in \text{Nonnegative}(\mathbb{Z} ,IntegerAddition,IntegerOrder) $

then have $ m\in \mathbb{Z} $ using Int_ZF_2_T1, OrderedGroup_ZF_1_L4E

then show $ \ \$ #0.\ .\ m \in Fin(\mathbb{Z} ) $ using Int_ZF_4_L5

qed

have $ group3(\mathbb{Z} ,IntegerAddition,IntegerOrder) $ using Int_ZF_2_T1

moreover

from T1 have $ \forall m \in \text{Nonnegative}(\mathbb{Z} ,IntegerAddition,IntegerOrder).\ $ $ \text{Interval}(IntegerOrder,\text{ TheNeutralElement}(\mathbb{Z} ,IntegerAddition),m) $ $ \in Fin(\mathbb{Z} ) $ using Int_ZF_1_L8

moreover

note A1

ultimately show $ A \in Fin(\mathbb{Z} ) $ by (rule OrderedGroup_ZF_2_T1 )

qed

A subset of integers is bounded iff it is finite.

theorem (in int0) Int_bounded_iff_fin:

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

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

lemma (in int0) Int_ZF_4_L8:

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

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

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

lemma (in int0) Int_ZF_4_L9:

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

shows $ \neg \text{IsBoundedAbove}(A,IntegerOrder) $, $ A \notin Fin(\mathbb{Z} ) $proof

have $ \mathbb{Z} \neq \{ 0 \} $ using Int_ZF_1_L8A, int_zero_not_one

with A1 show $ \neg \text{IsBoundedAbove}(A,IntegerOrder) $, $ A \notin Fin(\mathbb{Z} ) $ using Int_ZF_2_T1, OrderedGroup_ZF_2_L2A

qed

end

lemma func1_1_L11A:

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

shows $ \{\langle x,y\rangle \in X\times Y.\ b(x) = y\} : X\rightarrow Y $

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

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

lemma Int_ZF_1_L1: shows $ IntegerAddition : int\times int \rightarrow int $, $ IntegerMultiplication : int\times int \rightarrow int $

lemma (in int0) Int_ZF_1_L2:

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

shows $ a + b = a \ \$ + b $, $ a\cdot b = a \ \$ * b $

lemma (in int0) Int_ZF_1_L4:

assumes $ x\in \mathbb{Z} $, $ y\in \mathbb{Z} $

shows $ x + y = y + x $, $ x\cdot y = y\cdot x $

lemma (in int0) Int_ZF_1_L5:

assumes $ x\in \mathbb{Z} $

shows $ (\ \$ # 0) + x = x \wedge x + (\ \$ # 0) = x $, $ (\ \$ # 1)\cdot x = x \wedge x\cdot (\ \$ # 1) = x $

lemma (in int0) Int_ZF_1_L6: shows $ (\ \$ # 0)\in \mathbb{Z} \wedge $ $ (\forall x\in \mathbb{Z} .\ (\ \$ # 0) + x = x \wedge x + (\ \$ # 0) = x) $, $ (\ \$ # 1)\in \mathbb{Z} \wedge $ $ (\forall x\in \mathbb{Z} .\ (\ \$ # 1)\cdot x = x \wedge x\cdot (\ \$ # 1) = x) $

Definition of IsAmonoid: $ \text{IsAmonoid}(G,f) \equiv $ $ f \text{ is associative on } G \wedge $ $ (\exists e\in G.\ (\forall g\in G.\ ( (f(\langle e,g\rangle ) = g) \wedge (f(\langle g,e\rangle ) = g)))) $

Definition of IsAssociative: $ P \text{ is associative on } G \equiv P : G\times G\rightarrow G \wedge $ $ (\forall x \in G.\ \forall y \in G.\ \forall z \in G.\ $ $ ( P(\langle P(\langle x,y\rangle ),z\rangle ) = P( \langle x,P(\langle y,z\rangle )\rangle ))) $

lemma (in int0) Int_ZF_1_L3:

assumes $ x\in \mathbb{Z} $, $ y\in \mathbb{Z} $, $ z\in \mathbb{Z} $

shows $ x + y + z = x + (y + z) $, $ x\cdot y\cdot z = x\cdot (y\cdot z) $

theorem (in int0) Int_ZF_1_T1: shows $ \text{IsAmonoid}(\mathbb{Z} ,IntegerAddition) $, $ \text{IsAmonoid}(\mathbb{Z} ,IntegerMultiplication) $

lemma (in monoid0) group0_1_L4:

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

shows $ e = \text{ TheNeutralElement}(G,f) $

lemma (in int0) Int_ZF_1_L8: shows $ (\ \$ # 0) = 0 $, $ (\ \$ # 1) = 1 $

lemma (in int0) Int_ZF_1_L8A: shows $ 0 \in \mathbb{Z} $, $ 1 \in \mathbb{Z} $

lemma (in int0) int_zero_not_one: shows $ 0 \neq 1 $

lemma (in int0) Int_ZF_1_L9:

assumes $ g \in \mathbb{Z} $

shows $ \exists b\in \mathbb{Z} .\ g + b = 0 $

Definition of IsAgroup: $ \text{IsAgroup}(G,f) \equiv $ $ ( \text{IsAmonoid}(G,f) \wedge (\forall g\in G.\ \exists b\in G.\ f\langle g,b\rangle = \text{ TheNeutralElement}(G,f))) $

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

theorem Int_ZF_1_T2: shows $ \text{IsAgroup}(int,IntegerAddition) $, $ IntegerAddition \text{ is commutative on } int $, $ group0(int,IntegerAddition) $

lemma (in group0) group0_2_L9:

assumes $ a\in G $ and $ b\in G $ and $ a\cdot b = 1 $

shows $ a = b^{-1} $ and $ b = a^{-1} $

lemma (in group0) inverse_in_group:

assumes $ x\in G $

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

lemma (in int0) Int_ZF_1_L9A:

assumes $ m\in \mathbb{Z} $

shows $ \ \$ -m = - m $

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

lemma Int_ZF_1_L12:

assumes $ m\in int $

shows $ m \ \$ - \ \$ #1 \ \$ + \ \$ #1 = m $

lemma (in group0) group0_2_L7:

assumes $ a\in G $ and $ b\in G $ and $ a\cdot b = a $

shows $ b=1 $

lemma (in group0) inv_cancel_two:

assumes $ a\in G $, $ b\in G $

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

lemma (in group0) group0_2_L11A:

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

shows $ a=b $

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

lemma Int_ZF_2_L1B: shows $ IntegerOrder \subseteq int\times int $

lemma Order_ZF_3_L1B:

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

shows $ A\subseteq X $

lemma (in int0) Int_ZF_2_L1:

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

shows $ m \leq n $

lemma (in int0) Int_ZF_2_L1A:

assumes $ m \leq n $

shows $ m \ \$ \leq n $, $ m\in \mathbb{Z} $, $ n\in \mathbb{Z} $

lemma (in int0) Int_ZF_2_L3:

assumes $ m \leq n $, $ n \leq m $

shows $ m=n $

lemma Int_ZF_2_L5:

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

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

lemma Fol1_L2:

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

shows $ \text{trans}(r) $

lemma (in int0) int_ord_is_refl: shows $ \text{refl}(\mathbb{Z} ,IntegerOrder) $

lemma (in int0) Int_ZF_2_L4: shows $ \text{antisym}(IntegerOrder) $

lemma Int_ZF_2_L6: shows $ \text{trans}(IntegerOrder) $

Definition of IsPartOrder: $ \text{IsPartOrder}(X,r) \equiv \text{refl}(X,r) \wedge \text{antisym}(r) \wedge \text{trans}(r) $

lemma (in int0) int_ord_transl_inv:

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

shows $ m + k \leq n + k $, $ k + m\leq k + n $

lemma Int_ZF_2_L7: shows $ \text{IsPartOrder}(int,IntegerOrder) $

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

Definition of IsTotal: $ r \text{ is total on } X \equiv (\forall a\in X.\ \forall b\in X.\ \langle a,b\rangle \in r \vee \langle b,a\rangle \in r) $

Definition of IsLinOrder: $ \text{IsLinOrder}(X,r) \equiv \text{antisym}(r) \wedge \text{trans}(r) \wedge (r \text{ is total on } X) $

lemma (in int0) Int_ZF_1_L13:

assumes $ m\in \mathbb{Z} $

shows $ (m \ \$ - \ \$ #1) + 1 = m $

theorem (in int0) Int_ZF_2_T1: shows $ \text{IsAnOrdGroup}(\mathbb{Z} ,IntegerAddition,IntegerOrder) $, $ IntegerOrder \text{ is total on } \mathbb{Z} $, $ group3(\mathbb{Z} ,IntegerAddition,IntegerOrder) $, $ \text{IsLinOrder}(\mathbb{Z} ,IntegerOrder) $

lemma (in group3) OrderedGroup_ZF_1_L9A:

assumes $ a\in G $, $ b\in G $, $ c\in G $

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

lemma (in group3) OrderedGroup_ZF_1_L9B:

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

shows $ a \leq c\cdot b $

lemma (in group3) OrderedGroup_ZF_1_L5:

assumes $ a\leq b $

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

lemma (in group3) OrderedGroup_ZF_1_L5AD:

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

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

lemma (in group3) OrderedGroup_ZF_1_L5AF:

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

shows $ c\leq b $

lemma (in group3) OrderedGroup_ZF_1_L5A:

assumes $ a\leq 1 $

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

lemma (in group3) OrderedGroup_ZF_1_L5AA:

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

shows $ a\leq 1 $

lemma Nat_ZF_1_L3:

assumes $ n \in nat $ and $ n\neq 0 $

shows $ \exists k\in nat.\ n = succ(k) $

lemma (in int0) Int_ZF_2_L12:

assumes $ i\in \mathbb{Z} $ and $ n\in nat $

shows $ i \leq i \ \$ + \ \$ #n $

lemma (in int0) Int_ZF_2_L12A:

assumes $ j\leq k $

shows $ j \leq k \ \$ + \ \$ #1 $, $ j \leq k + 1 $

lemma (in int0) Int_ZF_2_L11: shows $ i \ \$ + \ \$ # n \ \$ + (\ \$ # 1) = i \ \$ + \ \$ # succ(n) $

lemma (in group3) OrderedGroup_ZF_3_L1: shows $ \text{AbsoluteValue}(G,P,r) : G\rightarrow G $

lemma (in group3) OrderedGroup_ZF_1_L5AC:

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

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

lemma (in group3) OrderedGroup_ZF_1_L12:

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

shows $ 1 \leq a\cdot b $

lemma (in group3) OrderedGroup_ZF_1_L5E:

assumes $ a \leq b\cdot c $ and $ b\leq b_1 $, $ c\leq c_1 $

shows $ a \leq b_1\cdot c_1 $

lemma (in group3) OrderedGroup_ZF_1_L5B:

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

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

lemma (in group3) OrderedGroup_ZF_1_L5I:

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

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

lemma (in group3) OrderedGroup_ZF_1_L5D:

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

shows $ a \leq b\cdot b_1 $

lemma (in group3) OrderedGroup_ZF_1_L10:

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

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

lemma (in group3) OrderedGroup_ZF_1_L5F:

assumes $ 1 \leq a $ and $ b\in G $

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

lemma (in group3) OrderedGroup_ZF_3_L6A:

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

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

lemma (in group3) OrderedGroup_ZF_1_L5G:

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

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

theorem (in group3) OrdGroup_triangle_ineq:

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

shows $ \vert a\cdot b\vert \leq \vert a\vert \cdot \vert b\vert $

lemma (in group3) OrderedGroup_ZF_1_L2: shows $ g\in G^+ \longleftrightarrow 1 \leq g $

lemma (in group3) OrderedGroup_ZF_3_L2:

assumes $ a\in G^+ $

shows $ \vert a\vert = a $

lemma (in group0) group0_2_L2: shows $ 1 \in G \wedge (\forall g\in G.\ (1 \cdot g = g \wedge g\cdot 1 = g)) $

lemma (in int0) Int_ZF_2_L16:

assumes $ 0 \leq m $

shows $ m\in \mathbb{Z} ^+ $ and $ abs(m) = m $

lemma (in int0) Int_ZF_2_L16A: shows $ 0 \leq 1 $ and $ abs(1 ) = 1 $

lemma (in int0) Int_order_transitive:

assumes $ m\leq n $, $ n\leq k $

shows $ m\leq k $

lemma (in int0) Int_ZF_2_L16B: shows $ 1 \leq 2 $

lemma (in group3) OrderedGroup_ZF_3_L7A:

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

shows $ \vert a^{-1}\vert = \vert a\vert $

lemma (in group3) OrderedGroup_ZF_3_L2A: shows $ \vert 1 \vert = 1 $

lemma (in int0) Int_triangle_ineq:

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

shows $ abs(m + n)\leq abs(m) + abs(n) $

lemma (in int0) Int_ZF_2_L17:

assumes $ m\in \mathbb{Z} $

shows $ abs( - m) = abs(m) $

lemma (in int0) Int_ZF_2_L14:

assumes $ m\in \mathbb{Z} $

shows $ abs(m) \in \mathbb{Z} $

lemma (in group3) OrderedGroup_ZF_3_L7D:

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

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

lemma (in group3) OrderedGroup_ZF_3_L7E:

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

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

lemma (in group0) group_op_closed:

assumes $ a\in G $, $ b\in G $

shows $ a\cdot b \in G $

lemma (in int0) Int_ZF_2_L10:

assumes $ k \leq i $

shows $ ( - i) \leq ( - k) $, $ \ \$ -i \leq \ \$ -k $

lemma (in group3) OrderedGroup_ZF_1_L8AA:

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

shows $ \neg (b\leq a) $

lemma (in int0) Int_ZF_2_L19:

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

shows $ m\leq n $, $ ( - n) \leq ( - m) $, $ m\neq n $

lemma (in group3) OrderedGroup_ZF_1_L18:

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

shows $ Q(b) $

lemma (in group3) OrderedGroup_ZF_3_L5:

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

shows $ a \leq \vert a\vert $

lemma (in group3) OrderedGroup_ZF_3_L6:

assumes $ a\in G $

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

lemma (in group3) OrderedGroup_ZF_3_L7B:

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

shows $ \vert a\cdot b^{-1}\vert = \vert b\cdot a^{-1}\vert $

lemma (in group3) OrderedGroup_ZF_3_L7C:

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

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

lemma (in group3) OrderedGroup_ZF_3_L7CA:

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

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

lemma (in group3) OrderedGroup_ZF_3_L3C:

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

shows $ \text{AbsoluteValue}(G,P,r) : G\rightarrow G^+ $

lemma (in int0) Int_ZF_2_L9:

assumes $ i \leq m $ and $ i\neq m $

shows $ i \ \$ \lt m $

lemma (in int0) Int_ZF_3_L2:

assumes $ i \leq m $

shows $ \exists n\in nat.\ m = i \ \$ + \ \$ # n $

lemma (in int0) Int_ZF_3_L6:

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

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

theorem ind_on_nat:

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

shows $ P(n) $

lemma (in int0) Int_ZF_3_L7A:

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

shows $ \forall m.\ i\leq m \wedge Q(m) \longrightarrow Q(m \ \$ + (\ \$ # 1)) $

lemma (in int0) Int_ZF_3_L7:

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

shows $ Q(k) $

lemma (in int0) Int_ZF_3_L9:

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

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

lemma (in int0) Int_ZF_3_L8:

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

shows $ P(k) $

lemma (in int0) Int_ZF_1_L10:

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

shows $ m - n = m \ \$ + \ \$ -n $

lemma (in int0) Int_ZF_3_L10:

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

shows $ \forall n.\ n\leq i \wedge P(n) \longrightarrow P(n \ \$ + \ \$ -(\ \$ #1)) $

lemma (in int0) Int_ZF_3_L9A:

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

shows $ P(k) $

lemma (in int0) Int_ZF_2_L13:

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

shows $ m \leq k $

lemma Int_ZF_4_L1A:

assumes $ m\in int $

shows $ m \ \$ - \ \$ #1 \ \$ + \ \$ #1 = m $

lemma (in int0) Int_ZF_4_L1:

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

shows $ m = k \ \$ + \ \$ #1 \vee m \leq k $

lemma (in int0) Int_ZF_2_L9A:

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

shows $ m + 1 \leq k $

lemma (in int0) Int_ZF_2_L9B:

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

shows $ i + m \leq k \longleftrightarrow i \leq k - m $

lemma Order_ZF_2_L1A:

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

shows $ \langle a,x\rangle \in r $, $ \langle x,b\rangle \in r $

lemma Order_ZF_2_L1B:

assumes $ \langle a,x\rangle \in r $, $ \langle x,b\rangle \in r $

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

lemma (in int0) Int_ZF_4_L2:

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

shows $ j \in m.\ .\ k \vee j \in \{k \ \$ + \ \$ #1\} $

lemma (in group3) OrderedGroup_ZF_1_L3:

assumes $ g\in G $

shows $ g\leq g $

lemma Order_ZF_2_L3:

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

shows $ \text{Interval}(r,b,c) \subseteq \text{Interval}(r,a,d) $

lemma Order_ZF_2_L2:

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

shows $ a \in \text{Interval}(r,a,b) $, $ b \in \text{Interval}(r,a,b) $

lemma (in int0) Int_ZF_4_L3:

assumes $ m\leq k $

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

lemma Order_ZF_2_L4:

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

shows $ \text{Interval}(r,a,a) = \{a\} $

lemma (in int0) Int_ZF_4_L4:

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

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

lemma Order_ZF_2_L5:

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

shows $ \text{Interval}(r,a,b) = 0 $

lemma (in group3) OrderedGroup_ZF_1_L4E: shows $ G^+ \subseteq G $

lemma (in int0) Int_ZF_4_L5:

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

shows $ i.\ .\ k \in Fin(\mathbb{Z} ) $

theorem (in group3) OrderedGroup_ZF_2_T1:

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

shows $ A \in Fin(G) $

lemma (in int0) Int_ZF_4_L6:

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

shows $ A \in Fin(\mathbb{Z} ) $

theorem (in group3) ord_group_fin_bounded:

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

shows $ \text{IsBounded}(B,r) $

lemma Finite1_L6A:

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

shows $ f(N) \in Fin(Y) $

theorem (in int0) Int_bounded_iff_fin: shows $ \text{IsBounded}(A,IntegerOrder)\longleftrightarrow A\in Fin(\mathbb{Z} ) $

lemma (in group3) OrderedGroup_ZF_2_L2A:

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

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

CommutativeSemigroup_ZF

TopologicalGroup_Uniformity_ZF

MMI_prelude

Metamath_Interface

Metamath_Sampler

This page by Slawomir Kolodynski is licensed under CC BY 4.0. BTC: 189qAMLvqevxMrCsZaABMJ3cLkXdSwMNK8