Up to index of Isabelle/ZF/IsarMathLib
theory Int_ZF_2(* This file is a part of IsarMathLib -
a library of formalized mathematics for Isabelle/Isar.
Copyright (C) 2005, 2006 Slawomir Kolodynski
This program is free software; Redistribution and use in source and binary forms,
with or without modification, are permitted provided that the following conditions are met:
1. Redistributions of source code must retain the above copyright notice,
this list of conditions and the following disclaimer.
2. Redistributions in binary form must reproduce the above copyright notice,
this list of conditions and the following disclaimer in the documentation and/or
other materials provided with the distribution.
3. The name of the author may not be used to endorse or promote products
derived from this software without specific prior written permission.
THIS SOFTWARE IS PROVIDED BY THE AUTHOR ``AS IS'' AND ANY EXPRESS OR IMPLIED
WARRANTIES, INCLUDING, BUT NOT LIMITED TO, THE IMPLIED WARRANTIES OF
MERCHANTABILITY AND FITNESS FOR A PARTICULAR PURPOSE ARE DISCLAIMED.
IN NO EVENT SHALL THE AUTHOR BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL,
SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT LIMITED TO,
PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF USE, DATA, OR PROFITS;
OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND ON ANY THEORY OF LIABILITY,
WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT (INCLUDING NEGLIGENCE OR
OTHERWISE) ARISING IN ANY WAY OUT OF THE USE OF THIS SOFTWARE,
EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.
*)
header {*\isaheader{Int\_ZF\_2.thy}*}
theory Int_ZF_2 imports Int_ZF_1 IntDiv_ZF Group_ZF_3
begin
text{*In this theory file we consider the properties of integers that are
needed for the real numbers construction in @{text "Real_ZF_x.thy"} series.*}
section{*Slopes*}
text{*In this section we study basic properties of slopes - the integer
almost homomorphisms.
The general definition of an almost homomorphism $f$ on a group $G$
written in additive notation requires the set
$\{f(m+n) - f(m) - f(n): m,n\in G\}$ to be finite.
In this section we establish a definition that is equivalent for integers:
that for all integer $m,n$ we have $|f(m+n) - f(m) - f(n)| \leq L$ for
some $L$. *}
text{*First we extend the standard notation for integers with notation related
to slopes. We define slopes as almost homomorphisms on the additive group of
integers. The set of slopes is denoted @{text "\<S>"}. We also define "positive"
slopes as those that take infinite number of positive values on positive integers.
We write @{text "δ(s,m,n)"} to denote the homomorphism
difference of $s$ at $m,n$ (i.e the expression $s(m+n) - s(m) - s(n)$).
We denote @{text "maxδ(s)"} the maximum absolute value of homomorphism
difference of $s$ as $m,n$ range over integers.
If $s$ is a slope,
then the set of homomorphism differences is finite and
this maximum exists.
In @{text "Group_ZF_3.thy"} we define the equivalence relation on
almost homomorphisms using the notion of a quotient group relation
and use "@{text "≈"}" to denote it. As here this symbol seems to be hogged
by the standard Isabelle, we will use "@{text "∼"}" instead "@{text "≈"}".
We show in this section that $s\sim r$ iff for some $L$ we
have $|s(m)-r(m)| \leq L$ for all integer $m$.
The "@{text "\<fp>"}" denotes the first operation on almost homomorphisms.
For slopes this is addition of functions defined in the natural way.
The "@{text "o"}" symbol denotes the second operation on almost homomorphisms
(see @{text "Group_ZF_3.thy"} for definition),
defined for the group of integers. In short "@{text "o"}"
is the composition of slopes.
The "@{text "¯"}" symbol acts as an infix operator that assigns the value
$\min\{n\in Z_+: p\leq f(n)\}$ to a pair (of sets) $f$ and $p$.
In application
$f$ represents a function defined on $Z_+$ and $p$ is a positive integer.
We choose this notation because we use it to construct the right inverse
in the ring of classes of slopes and show that this ring is in fact a field.
To study the homomorphism difference of the function defined by $p\mapsto f^{-1}(p)$
we introduce the symbol @{text "ε"} defined as
$\varepsilon(f,\langle m,n \rangle ) = f^{-1}(m+n)-f^{-1}(m)-f^{-1}(n)$. Of course the intention is
to use the fact that $\varepsilon(f,\langle m,n \rangle )$ is the homomorphism difference
of the function $g$ defined as $g(m) = f^{-1}(m)$. We also define $\gamma (s,m,n)$ as the
expression $\delta(f,m,-n)+s(0)-\delta (f,n,-n)$. This is useful because of the identity
$f(m-n) = \gamma (m,n) + f(m)-f(n)$ that allows to obtain bounds on the value of a slope
at the difference of of two integers.
For every integer $m$ we introduce notation $m^S$ defined by $m^E(n)=m\cdot n$. The mapping
$q\mapsto q^S$ embeds integers into @{text "\<S>"} preserving the order, (that is,
maps positive integers into @{text "\<S>+"}). *}
locale int1 = int0 +
fixes slopes ("\<S>" )
defines slopes_def [simp]: "\<S> ≡ AlmostHoms(\<int>,IntegerAddition)"
fixes posslopes ("\<S>+")
defines posslopes_def [simp]: "\<S>+ ≡ {s∈\<S>. s``(\<int>+) ∩ \<int>+ ∉ Fin(\<int>)}"
fixes δ
defines δ_def [simp] : "δ(s,m,n) ≡ s`(m\<ra>n)\<rs>s`(m)\<rs>s`(n)"
fixes maxhomdiff ("maxδ" )
defines maxhomdiff_def [simp]:
"maxδ(s) ≡ Maximum(IntegerOrder,{abs(δ(s,m,n)). <m,n> ∈ \<int>×\<int>})"
fixes AlEqRel
defines AlEqRel_def [simp]:
"AlEqRel ≡ QuotientGroupRel(\<S>,AlHomOp1(\<int>,IntegerAddition),FinRangeFunctions(\<int>,\<int>))"
fixes AlEq :: "[i,i]=>o" (infix "∼" 68)
defines AlEq_def [simp]: "s ∼ r ≡ <s,r> ∈ AlEqRel"
fixes slope_add (infix "\<fp>" 70)
defines slope_add_def [simp]: "s \<fp> r ≡ AlHomOp1(\<int>,IntegerAddition)`<s,r>"
fixes slope_comp (infix "o" 70)
defines slope_comp_def [simp]: "s o r ≡ AlHomOp2(\<int>,IntegerAddition)`<s,r>"
fixes neg :: "i=>i" ("\<fm>_" [90] 91)
defines neg_def [simp]: "\<fm>s ≡ GroupInv(\<int>,IntegerAddition) O s"
fixes slope_inv (infix "¯" 71)
defines slope_inv_def [simp]:
"f¯(p) ≡ Minimum(IntegerOrder,{n∈\<int>+. p \<lsq> f`(n)})"
fixes ε
defines ε_def [simp]:
"ε(f,p) ≡ f¯(fst(p)\<ra>snd(p)) \<rs> f¯(fst(p)) \<rs> f¯(snd(p))"
fixes γ
defines γ_def [simp]:
"γ(s,m,n) ≡ δ(s,m,\<rm>n) \<rs> δ(s,n,\<rm>n) \<ra> s`(\<zero>)"
fixes intembed ("_S")
defines intembed_def [simp]: "mS ≡ {⟨n,m·n⟩. n∈\<int>}";
text{*We can use theorems proven in the @{text "group1"} context.*}
lemma (in int1) Int_ZF_2_1_L1: shows "group1(\<int>,IntegerAddition)"
using Int_ZF_1_T2 group1_axioms.intro group1_def by simp;
text{*Type information related to the homomorphism difference expression.*}
lemma (in int1) Int_ZF_2_1_L2: assumes "f∈\<S>" and "n∈\<int>" "m∈\<int>"
shows
"m\<ra>n ∈ \<int>"
"f`(m\<ra>n) ∈ \<int>"
"f`(m) ∈ \<int>" "f`(n) ∈ \<int>"
"f`(m) \<ra> f`(n) ∈ \<int>"
"HomDiff(\<int>,IntegerAddition,f,<m,n>) ∈ \<int>"
using prems Int_ZF_2_1_L1 group1.Group_ZF_3_2_L4A
by auto;
text{*Type information related to the homomorphism difference expression.*}
lemma (in int1) Int_ZF_2_1_L2A:
assumes "f:\<int>->\<int>" and "n∈\<int>" "m∈\<int>"
shows
"m\<ra>n ∈ \<int>"
"f`(m\<ra>n) ∈ \<int>" "f`(m) ∈ \<int>" "f`(n) ∈ \<int>"
"f`(m) \<ra> f`(n) ∈ \<int>"
"HomDiff(\<int>,IntegerAddition,f,<m,n>) ∈ \<int>"
using prems Int_ZF_2_1_L1 group1.Group_ZF_3_2_L4
by auto;
text{*Slopes map integers into integers.*}
lemma (in int1) Int_ZF_2_1_L2B:
assumes A1: "f∈\<S>" and A2: "m∈\<int>"
shows "f`(m) ∈ \<int>"
proof -;
from A1 have "f:\<int>->\<int>" using AlmostHoms_def by simp
with A2 show "f`(m) ∈ \<int>" using apply_funtype by simp;
qed;
text{*The homomorphism difference in multiplicative notation is defined as
the expression $s(m\cdot n)\cdot(s(m)\cdot s(n))^{-1}$. The next lemma
shows that
in the additive notation used for integers the homomorphism
difference is $f(m+n) - f(m) - f(n)$ which we denote as @{text "δ(f,m,n)"}.*}
lemma (in int1) Int_ZF_2_1_L3:
assumes "f:\<int>->\<int>" and "m∈\<int>" "n∈\<int>"
shows "HomDiff(\<int>,IntegerAddition,f,<m,n>) = δ(f,m,n)"
using prems Int_ZF_2_1_L2A Int_ZF_1_T2 group0.group0_4_L4A
HomDiff_def by auto;
text{*The next formula restates the definition of the homomorphism
difference to express the value an almost homomorphism on a sum.*}
lemma (in int1) Int_ZF_2_1_L3A:
assumes A1: "f∈\<S>" and A2: "m∈\<int>" "n∈\<int>"
shows
"f`(m\<ra>n) = f`(m)\<ra>(f`(n)\<ra>δ(f,m,n))"
proof -
from A1 A2 have
T: "f`(m)∈ \<int>" "f`(n) ∈ \<int>" "δ(f,m,n) ∈ \<int>" and
"HomDiff(\<int>,IntegerAddition,f,<m,n>) = δ(f,m,n)"
using Int_ZF_2_1_L2 AlmostHoms_def Int_ZF_2_1_L3 by auto;
with A1 A2 show "f`(m\<ra>n) = f`(m)\<ra>(f`(n)\<ra>δ(f,m,n))"
using Int_ZF_2_1_L3 Int_ZF_1_L3
Int_ZF_2_1_L1 group1.Group_ZF_3_4_L1
by simp;
qed;
text{*The homomorphism difference of any integer function is integer.*}
lemma (in int1) Int_ZF_2_1_L3B:
assumes "f:\<int>->\<int>" and "m∈\<int>" "n∈\<int>"
shows "δ(f,m,n) ∈ \<int>"
using prems Int_ZF_2_1_L2A Int_ZF_2_1_L3 by simp;
text{*The value of an integer function at a sum expressed in
terms of @{text "δ"}.*}
lemma (in int1) Int_ZF_2_1_L3C: assumes A1: "f:\<int>->\<int>" and A2: "m∈\<int>" "n∈\<int>"
shows "f`(m\<ra>n) = δ(f,m,n) \<ra> f`(n) \<ra> f`(m)"
proof -
from A1 A2 have T:
"δ(f,m,n) ∈ \<int>" "f`(m\<ra>n) ∈ \<int>" "f`(m) ∈ \<int>" "f`(n) ∈ \<int>"
using Int_ZF_1_1_L5 apply_funtype by auto;
then show "f`(m\<ra>n) = δ(f,m,n) \<ra> f`(n) \<ra> f`(m)"
using Int_ZF_1_2_L15 by simp;
qed;
text{*The next lemma presents two ways the set of homomorphism differences
can be written. *}
lemma (in int1) Int_ZF_2_1_L4: assumes A1: "f:\<int>->\<int>"
shows "{abs(HomDiff(\<int>,IntegerAddition,f,x)). x ∈ \<int>×\<int>} =
{abs(δ(f,m,n)). <m,n> ∈ \<int>×\<int>}"
proof -
from A1 have "∀m∈\<int>. ∀n∈\<int>.
abs(HomDiff(\<int>,IntegerAddition,f,<m,n>)) = abs(δ(f,m,n))"
using Int_ZF_2_1_L3 by simp;
then show ?thesis by (rule ZF1_1_L4A);
qed;
text{*If $f$ maps integers into integers and
for all $m,n\in Z$ we have $|f(m+n) - f(m) - f(n)| \leq L$ for some $L$,
then $f$ is a slope.*}
lemma (in int1) Int_ZF_2_1_L5: assumes A1: "f:\<int>->\<int>"
and A2: "∀m∈\<int>.∀n∈\<int>. abs(δ(f,m,n)) \<lsq> L"
shows "f∈\<S>"
proof -;
let ?Abs = "AbsoluteValue(\<int>,IntegerAddition,IntegerOrder)"
have "group3(\<int>,IntegerAddition,IntegerOrder)"
"IntegerOrder {is total on} \<int>"
using Int_ZF_2_T1 by auto
moreover from A1 A2 have
"∀x∈\<int>×\<int>. HomDiff(\<int>,IntegerAddition,f,x) ∈ \<int> ∧
⟨?Abs`(HomDiff(\<int>,IntegerAddition,f,x)),L ⟩ ∈ IntegerOrder"
using Int_ZF_2_1_L2A Int_ZF_2_1_L3 by auto;
ultimately have
"IsBounded({HomDiff(\<int>,IntegerAddition,f,x). x∈\<int>×\<int>},IntegerOrder)"
by (rule group3.OrderedGroup_ZF_3_L9A);
with A1 show "f ∈ \<S>" using Int_bounded_iff_fin AlmostHoms_def
by simp;
qed;
text{*The absolute value of homomorphism difference
of a slope $s$ does not exceed @{text "maxδ(s)"}.*}
lemma (in int1) Int_ZF_2_1_L7:
assumes A1: "s∈\<S>" and A2: "n∈\<int>" "m∈\<int>"
shows
"abs(δ(s,m,n)) \<lsq> maxδ(s)"
"δ(s,m,n) ∈ \<int>" "maxδ(s) ∈ \<int>"
"(\<rm>maxδ(s)) \<lsq> δ(s,m,n)"
proof -
from A1 A2 show T: "δ(s,m,n) ∈ \<int>"
using Int_ZF_2_1_L2 Int_ZF_1_1_L5 by simp;
let ?A = "{abs(HomDiff(\<int>,IntegerAddition,s,x)). x∈\<int>×\<int>}"
let ?B = "{abs(δ(s,m,n)). <m,n> ∈ \<int>×\<int>}"
let ?d = "abs(δ(s,m,n))"
have "IsLinOrder(\<int>,IntegerOrder)" using Int_ZF_2_T1
by simp;
moreover have "?A ∈ Fin(\<int>)"
proof -;
have "∀k∈\<int>. abs(k) ∈ \<int>" using Int_ZF_2_L14 by simp;
moreover from A1 have
"{HomDiff(\<int>,IntegerAddition,s,x). x ∈ \<int>×\<int>} ∈ Fin(\<int>)"
using AlmostHoms_def by simp;
ultimately show "?A ∈ Fin(\<int>)" by (rule Finite1_L6C);
qed;
moreover have "?A≠0" by auto;
ultimately have "∀k∈?A. ⟨k,Maximum(IntegerOrder,?A)⟩ ∈ IntegerOrder"
by (rule Finite_ZF_1_T2)
moreover from A1 A2 have "?d∈?A" using AlmostHoms_def Int_ZF_2_1_L4
by auto;
ultimately have "?d \<lsq> Maximum(IntegerOrder,?A)" by auto;
with A1 show "?d \<lsq> maxδ(s)" "maxδ(s) ∈ \<int>"
using AlmostHoms_def Int_ZF_2_1_L4 Int_ZF_2_L1A
by auto;
with T show "(\<rm>maxδ(s)) \<lsq> δ(s,m,n)"
using Int_ZF_1_3_L19 by simp;
qed;
text{*A useful estimate for the value of a slope at $0$, plus some type information
for slopes.*}
lemma (in int1) Int_ZF_2_1_L8: assumes A1: "s∈\<S>"
shows
"abs(s`(\<zero>)) \<lsq> maxδ(s)"
"\<zero> \<lsq> maxδ(s)"
"abs(s`(\<zero>)) ∈ \<int>" "maxδ(s) ∈ \<int>"
"abs(s`(\<zero>)) \<ra> maxδ(s) ∈ \<int>"
proof -;
from A1 have "s`(\<zero>) ∈ \<int>"
using int_zero_one_are_int Int_ZF_2_1_L2B by simp;
then have I: "\<zero> \<lsq> abs(s`(\<zero>))"
and "abs(δ(s,\<zero>,\<zero>)) = abs(s`(\<zero>))"
using int_abs_nonneg int_zero_one_are_int Int_ZF_1_1_L4
Int_ZF_2_L17 by auto
moreover from A1 have "abs(δ(s,\<zero>,\<zero>)) \<lsq> maxδ(s)"
using int_zero_one_are_int Int_ZF_2_1_L7 by simp;
ultimately show II: "abs(s`(\<zero>)) \<lsq> maxδ(s)"
by simp;
with I show "\<zero>\<lsq>maxδ(s)" by (rule Int_order_transitive);
with II show
"maxδ(s) ∈ \<int>" "abs(s`(\<zero>)) ∈ \<int>"
"abs(s`(\<zero>)) \<ra> maxδ(s) ∈ \<int>"
using Int_ZF_2_L1A Int_ZF_1_1_L5 by auto;
qed;
text{*Int @{text "Group_ZF_3.thy"} we show that finite range functions
valued in an abelian group
form a normal subgroup of almost homomorphisms.
This allows to define the equivalence relation
between almost homomorphisms as the relation resulting from dividing
by that normal subgroup.
Then we show in @{text "Group_ZF_3_4_L12"} that if the difference of $f$ and $g$
has finite range (actually $f(n)\cdot g(n)^{-1}$ as we use multiplicative
notation
in @{text "Group_ZF_3.thy"}), then $f$ and $g$ are equivalent.
The next lemma translates that fact into the notation used in @{text "int1"}
context.*}
lemma (in int1) Int_ZF_2_1_L9: assumes A1: "s∈\<S>" "r∈\<S>"
and A2: "∀m∈\<int>. abs(s`(m)\<rs>r`(m)) \<lsq> L"
shows "s ∼ r"
proof -
from A1 A2 have
"∀m∈\<int>. s`(m)\<rs>r`(m) ∈ \<int> ∧ abs(s`(m)\<rs>r`(m)) \<lsq> L"
using Int_ZF_2_1_L2B Int_ZF_1_1_L5 by simp;
then have
"IsBounded({s`(n)\<rs>r`(n). n∈\<int>}, IntegerOrder)"
by (rule Int_ZF_1_3_L20);
with A1 show "s ∼ r" using Int_bounded_iff_fin
Int_ZF_2_1_L1 group1.Group_ZF_3_4_L12 by simp;
qed;
text{*A neccessary condition for two slopes to be almost equal.
For slopes the definition postulates the
set $\{f(m)-g(m): m\in Z\}$ to be finite.
This lemma shows that this imples that
$|f(m)-g(m)|$ is bounded (by some integer) as $m$ varies over integers.
We also mention here that in this context @{text "s ∼ r"} implies that both
$s$ and $r$ are slopes.*}
lemma (in int1) Int_ZF_2_1_L9A: assumes "s ∼ r"
shows
"∃L∈\<int>. ∀m∈\<int>. abs(s`(m)\<rs>r`(m)) \<lsq> L"
"s∈\<S>" "r∈\<S>"
using prems Int_ZF_2_1_L1 group1.Group_ZF_3_4_L11
Int_ZF_1_3_L20AA QuotientGroupRel_def by auto;
text{*Let's recall that the relation of almost equality is an equivalence relation
on the set of slopes.*}
lemma (in int1) Int_ZF_2_1_L9B: shows
"AlEqRel ⊆ \<S>×\<S>"
"equiv(\<S>,AlEqRel)"
using Int_ZF_2_1_L1 group1.Group_ZF_3_3_L3 by auto;
text{*Another version of sufficient condition for two slopes to be almost
equal: if the difference of two slopes is a finite range function, then
they are almost equal.*}
lemma (in int1) Int_ZF_2_1_L9C: assumes "s∈\<S>" "r∈\<S>" and
"s \<fp> (\<fm>r) ∈ FinRangeFunctions(\<int>,\<int>)"
shows
"s ∼ r"
"r ∼ s"
using prems Int_ZF_2_1_L1
group1.Group_ZF_3_2_L13 group1.Group_ZF_3_4_L12A
by auto;
text{*If two slopes are almost equal, then the difference has finite range.
This is the inverse of @{text "Int_ZF_2_1_L9C"}.*}
lemma (in int1) Int_ZF_2_1_L9D: assumes A1: "s ∼ r"
shows "s \<fp> (\<fm>r) ∈ FinRangeFunctions(\<int>,\<int>)"
proof -
let ?G = "\<int>"
let ?f = "IntegerAddition"
from A1 have "AlHomOp1(?G, ?f)`⟨s,GroupInv(AlmostHoms(?G, ?f),AlHomOp1(?G, ?f))`(r)⟩
∈ FinRangeFunctions(?G, ?G)"
using Int_ZF_2_1_L1 group1.Group_ZF_3_4_L12B by auto;
with A1 show "s \<fp> (\<fm>r) ∈ FinRangeFunctions(\<int>,\<int>)"
using Int_ZF_2_1_L9A Int_ZF_2_1_L1 group1.Group_ZF_3_2_L13
by simp;
qed;
text{*What is the value of a composition of slopes?*}
lemma (in int1) Int_ZF_2_1_L10:
assumes "s∈\<S>" "r∈\<S>" and "m∈\<int>"
shows "(sor)`(m) = s`(r`(m))" "s`(r`(m)) ∈ \<int>"
using prems Int_ZF_2_1_L1 group1.Group_ZF_3_4_L2 by auto;
text{*Composition of slopes is a slope.*}
lemma (in int1) Int_ZF_2_1_L11:
assumes "s∈\<S>" "r∈\<S>"
shows "sor ∈ \<S>"
using prems Int_ZF_2_1_L1 group1.Group_ZF_3_4_T1 by simp;
text{*Negative of a slope is a slope.*}
lemma (in int1) Int_ZF_2_1_L12: assumes "s∈\<S>" shows "\<fm>s ∈ \<S>"
using prems Int_ZF_1_T2 Int_ZF_2_1_L1 group1.Group_ZF_3_2_L13
by simp;
text{*What is the value of a negative of a slope?*}
lemma (in int1) Int_ZF_2_1_L12A:
assumes "s∈\<S>" and "m∈\<int>" shows "(\<fm>s)`(m) = \<rm>(s`(m))"
using prems Int_ZF_2_1_L1 group1.Group_ZF_3_2_L5
by simp;
text{*What are the values of a sum of slopes?*}
lemma (in int1) Int_ZF_2_1_L12B: assumes "s∈\<S>" "r∈\<S>" and "m∈\<int>"
shows "(s\<fp>r)`(m) = s`(m) \<ra> r`(m)"
using prems Int_ZF_2_1_L1 group1.Group_ZF_3_2_L12
by simp;
text{*Sum of slopes is a slope.*}
lemma (in int1) Int_ZF_2_1_L12C: assumes "s∈\<S>" "r∈\<S>"
shows "s\<fp>r ∈ \<S>"
using prems Int_ZF_2_1_L1 group1.Group_ZF_3_2_L16
by simp;
text{*A simple but useful identity.*}
lemma (in int1) Int_ZF_2_1_L13:
assumes "s∈\<S>" and "n∈\<int>" "m∈\<int>"
shows "s`(n·m) \<ra> (s`(m) \<ra> δ(s,n·m,m)) = s`((n\<ra>\<one>)·m)"
using prems Int_ZF_1_1_L5 Int_ZF_2_1_L2B Int_ZF_1_2_L9 Int_ZF_1_2_L7
by simp;
text{*Some estimates for the absolute value of a slope at the opposite
integer.*}
lemma (in int1) Int_ZF_2_1_L14: assumes A1: "s∈\<S>" and A2: "m∈\<int>"
shows
"s`(\<rm>m) = s`(\<zero>) \<rs> δ(s,m,\<rm>m) \<rs> s`(m)"
"abs(s`(m)\<ra>s`(\<rm>m)) \<lsq> \<two>·maxδ(s)"
"abs(s`(\<rm>m)) \<lsq> \<two>·maxδ(s) \<ra> abs(s`(m))"
"s`(\<rm>m) \<lsq> abs(s`(\<zero>)) \<ra> maxδ(s) \<rs> s`(m)"
proof -
from A1 A2 have T:
"(\<rm>m) ∈ \<int>" "abs(s`(m)) ∈ \<int>" "s`(\<zero>) ∈ \<int>" "abs(s`(\<zero>)) ∈ \<int>"
"δ(s,m,\<rm>m) ∈ \<int>" "s`(m) ∈ \<int>" "s`(\<rm>m) ∈ \<int>"
"(\<rm>(s`(m))) ∈ \<int>" "s`(\<zero>) \<rs> δ(s,m,\<rm>m) ∈ \<int>"
using Int_ZF_1_1_L4 Int_ZF_2_1_L2B Int_ZF_2_L14 Int_ZF_2_1_L2
Int_ZF_1_1_L5 int_zero_one_are_int by auto;
with A2 show I: "s`(\<rm>m) = s`(\<zero>) \<rs> δ(s,m,\<rm>m) \<rs> s`(m)"
using Int_ZF_1_1_L4 Int_ZF_1_2_L15 by simp;
from T have "abs(s`(\<zero>) \<rs> δ(s,m,\<rm>m)) \<lsq> abs(s`(\<zero>)) \<ra> abs(δ(s,m,\<rm>m))"
using Int_triangle_ineq1 by simp;
moreover from A1 A2 T have "abs(s`(\<zero>)) \<ra> abs(δ(s,m,\<rm>m)) \<lsq> \<two>·maxδ(s)"
using Int_ZF_2_1_L7 Int_ZF_2_1_L8 Int_ZF_1_3_L21 by simp;
ultimately have "abs(s`(\<zero>) \<rs> δ(s,m,\<rm>m)) \<lsq> \<two>·maxδ(s)"
by (rule Int_order_transitive);
moreover
from I have "s`(m) \<ra> s`(\<rm>m) = s`(m) \<ra> (s`(\<zero>) \<rs> δ(s,m,\<rm>m) \<rs> s`(m))"
by simp;
with T have "abs(s`(m) \<ra> s`(\<rm>m)) = abs(s`(\<zero>) \<rs> δ(s,m,\<rm>m))"
using Int_ZF_1_2_L3 by simp;
ultimately show "abs(s`(m)\<ra>s`(\<rm>m)) \<lsq> \<two>·maxδ(s)"
by simp;
from I have "abs(s`(\<rm>m)) = abs(s`(\<zero>) \<rs> δ(s,m,\<rm>m) \<rs> s`(m))"
by simp;
with T have
"abs(s`(\<rm>m)) \<lsq> abs(s`(\<zero>)) \<ra> abs(δ(s,m,\<rm>m)) \<ra> abs(s`(m))"
using int_triangle_ineq3 by simp;
moreover from A1 A2 T have
"abs(s`(\<zero>)) \<ra> abs(δ(s,m,\<rm>m)) \<ra> abs(s`(m)) \<lsq> \<two>·maxδ(s) \<ra> abs(s`(m))"
using Int_ZF_2_1_L7 Int_ZF_2_1_L8 Int_ZF_1_3_L21 int_ord_transl_inv by simp;
ultimately show "abs(s`(\<rm>m)) \<lsq> \<two>·maxδ(s) \<ra> abs(s`(m))"
by (rule Int_order_transitive);
from T have "s`(\<zero>) \<rs> δ(s,m,\<rm>m) \<lsq> abs(s`(\<zero>)) \<ra> abs(δ(s,m,\<rm>m))"
using Int_ZF_2_L15E by simp;
moreover from A1 A2 T have
"abs(s`(\<zero>)) \<ra> abs(δ(s,m,\<rm>m)) \<lsq> abs(s`(\<zero>)) \<ra> maxδ(s)"
using Int_ZF_2_1_L7 int_ord_transl_inv by simp;
ultimately have "s`(\<zero>) \<rs> δ(s,m,\<rm>m) \<lsq> abs(s`(\<zero>)) \<ra> maxδ(s)"
by (rule Int_order_transitive)
with T have
"s`(\<zero>) \<rs> δ(s,m,\<rm>m) \<rs> s`(m) \<lsq> abs(s`(\<zero>)) \<ra> maxδ(s) \<rs> s`(m)"
using int_ord_transl_inv by simp;
with I show "s`(\<rm>m) \<lsq> abs(s`(\<zero>)) \<ra> maxδ(s) \<rs> s`(m)"
by simp;
qed;
text{*An identity that expresses the value of an integer function at the opposite
integer in terms of the value of that function at the integer, zero, and the
homomorphism difference. We have a similar identity in @{text "Int_ZF_2_1_L14"}, but
over there we assume that $f$ is a slope.*}
lemma (in int1) Int_ZF_2_1_L14A: assumes A1: "f:\<int>->\<int>" and A2: "m∈\<int>"
shows "f`(\<rm>m) = (\<rm>δ(f,m,\<rm>m)) \<ra> f`(\<zero>) \<rs> f`(m)"
proof -
from A1 A2 have T:
"f`(\<rm>m) ∈ \<int>" "δ(f,m,\<rm>m) ∈ \<int>" "f`(\<zero>) ∈ \<int>" "f`(m) ∈ \<int>"
using Int_ZF_1_1_L4 Int_ZF_1_1_L5 int_zero_one_are_int apply_funtype
by auto;
with A2 show "f`(\<rm>m) = (\<rm>δ(f,m,\<rm>m)) \<ra> f`(\<zero>) \<rs> f`(m)"
using Int_ZF_1_1_L4 Int_ZF_1_2_L15 by simp;
qed;
text{*The next lemma allows to use the expression @{text "maxf(f,\<zero>..M-1)"}.
Recall that @{text "maxf(f,A)"} is the maximum of (function) $f$ on
(the set) $A$.*}
lemma (in int1) Int_ZF_2_1_L15:
assumes "s∈\<S>" and "M ∈ \<int>+"
shows
"maxf(s,\<zero>..(M\<rs>\<one>)) ∈ \<int>"
"∀n ∈ \<zero>..(M\<rs>\<one>). s`(n) \<lsq> maxf(s,\<zero>..(M\<rs>\<one>))"
"minf(s,\<zero>..(M\<rs>\<one>)) ∈ \<int>"
"∀n ∈ \<zero>..(M\<rs>\<one>). minf(s,\<zero>..(M\<rs>\<one>)) \<lsq> s`(n)"
using prems AlmostHoms_def Int_ZF_1_5_L6 Int_ZF_1_4_L2
by auto;
text{*A lower estimate for the value of a slope at $nM+k$.*}
lemma (in int1) Int_ZF_2_1_L16:
assumes A1: "s∈\<S>" and A2: "m∈\<int>" and A3: "M ∈ \<int>+" and A4: "k ∈ \<zero>..(M\<rs>\<one>)"
shows "s`(m·M) \<ra> (minf(s,\<zero>..(M\<rs>\<one>))\<rs> maxδ(s)) \<lsq> s`(m·M\<ra>k)"
proof -
from A3 have "\<zero>..(M\<rs>\<one>) ⊆ \<int>"
using Int_ZF_1_5_L6 by simp;
with A1 A2 A3 A4 have T: "m·M ∈ \<int>" "k ∈ \<int>" "s`(m·M) ∈ \<int>"
using PositiveSet_def Int_ZF_1_1_L5 Int_ZF_2_1_L2B
by auto;
with A1 A3 A4 have
"s`(m·M) \<ra> (minf(s,\<zero>..(M\<rs>\<one>)) \<rs> maxδ(s)) \<lsq> s`(m·M) \<ra> (s`(k) \<ra> δ(s,m·M,k))"
using Int_ZF_2_1_L15 Int_ZF_2_1_L7 int_ineq_add_sides int_ord_transl_inv
by simp;
with A1 T show ?thesis using Int_ZF_2_1_L3A by simp;
qed;
text{*Identity is a slope.*}
lemma (in int1) Int_ZF_2_1_L17: shows "id(\<int>) ∈ \<S>"
using Int_ZF_2_1_L1 group1.Group_ZF_3_4_L15 by simp;
text{*Simple identities about (absolute value of) homomorphism differences.*}
lemma (in int1) Int_ZF_2_1_L18:
assumes A1: "f:\<int>->\<int>" and A2: "m∈\<int>" "n∈\<int>"
shows
"abs(f`(n) \<ra> f`(m) \<rs> f`(m\<ra>n)) = abs(δ(f,m,n))"
"abs(f`(m) \<ra> f`(n) \<rs> f`(m\<ra>n)) = abs(δ(f,m,n))"
"(\<rm>(f`(m))) \<rs> f`(n) \<ra> f`(m\<ra>n) = δ(f,m,n)"
"(\<rm>(f`(n))) \<rs> f`(m) \<ra> f`(m\<ra>n) = δ(f,m,n)"
"abs((\<rm>f`(m\<ra>n)) \<ra> f`(m) \<ra> f`(n)) = abs(δ(f,m,n))"
proof -
from A1 A2 have T:
"f`(m\<ra>n) ∈ \<int>" "f`(m) ∈ \<int>" "f`(n) ∈ \<int>"
"f`(m\<ra>n) \<rs> f`(m) \<rs> f`(n) ∈ \<int>"
"(\<rm>(f`(m))) ∈ \<int>"
"(\<rm>f`(m\<ra>n)) \<ra> f`(m) \<ra> f`(n) ∈ \<int>"
using apply_funtype Int_ZF_1_1_L4 Int_ZF_1_1_L5 by auto;
then have
"abs(\<rm>(f`(m\<ra>n) \<rs> f`(m) \<rs> f`(n))) = abs(f`(m\<ra>n) \<rs> f`(m) \<rs> f`(n))"
using Int_ZF_2_L17 by simp;
moreover from T have
"(\<rm>(f`(m\<ra>n) \<rs> f`(m) \<rs> f`(n))) = f`(n) \<ra> f`(m) \<rs> f`(m\<ra>n)"
using Int_ZF_1_2_L9A by simp;
ultimately show "abs(f`(n) \<ra> f`(m) \<rs> f`(m\<ra>n)) = abs(δ(f,m,n))"
by simp;
moreover from T have "f`(n) \<ra> f`(m) = f`(m) \<ra> f`(n)"
using Int_ZF_1_1_L5 by simp
ultimately show "abs(f`(m) \<ra> f`(n) \<rs> f`(m\<ra>n)) = abs(δ(f,m,n))"
by simp;
from T show
"(\<rm>(f`(m))) \<rs> f`(n) \<ra> f`(m\<ra>n) = δ(f,m,n)"
"(\<rm>(f`(n))) \<rs> f`(m) \<ra> f`(m\<ra>n) = δ(f,m,n)"
using Int_ZF_1_2_L9 by auto;
from T have
"abs((\<rm>f`(m\<ra>n)) \<ra> f`(m) \<ra> f`(n)) =
abs(\<rm>((\<rm>f`(m\<ra>n)) \<ra> f`(m) \<ra> f`(n)))"
using Int_ZF_2_L17 by simp;
also from T have
"abs(\<rm>((\<rm>f`(m\<ra>n)) \<ra> f`(m) \<ra> f`(n))) = abs(δ(f,m,n))"
using Int_ZF_1_2_L9 by simp
finally show "abs((\<rm>f`(m\<ra>n)) \<ra> f`(m) \<ra> f`(n)) = abs(δ(f,m,n))"
by simp;
qed;
text{*Some identities about the homomorphism difference of odd functions.*}
lemma (in int1) Int_ZF_2_1_L19:
assumes A1: "f:\<int>->\<int>" and A2: "∀x∈\<int>. (\<rm>f`(\<rm>x)) = f`(x)"
and A3: "m∈\<int>" "n∈\<int>"
shows
"abs(δ(f,\<rm>m,m\<ra>n)) = abs(δ(f,m,n))"
"abs(δ(f,\<rm>n,m\<ra>n)) = abs(δ(f,m,n))"
"δ(f,n,\<rm>(m\<ra>n)) = δ(f,m,n)"
"δ(f,m,\<rm>(m\<ra>n)) = δ(f,m,n)"
"abs(δ(f,\<rm>m,\<rm>n)) = abs(δ(f,m,n))"
proof -
from A1 A2 A3 show
"abs(δ(f,\<rm>m,m\<ra>n)) = abs(δ(f,m,n))"
"abs(δ(f,\<rm>n,m\<ra>n)) = abs(δ(f,m,n))"
using Int_ZF_1_2_L3 Int_ZF_2_1_L18 by auto;
from A3 have T: "m\<ra>n ∈ \<int>" using Int_ZF_1_1_L5 by simp
from A1 A2 have I: "∀x∈\<int>. f`(\<rm>x) = (\<rm>f`(x))"
using Int_ZF_1_5_L13 by simp;
with A1 A2 A3 T show
"δ(f,n,\<rm>(m\<ra>n)) = δ(f,m,n)"
"δ(f,m,\<rm>(m\<ra>n)) = δ(f,m,n)"
using Int_ZF_1_2_L3 Int_ZF_2_1_L18 by auto;
from A3 have
"abs(δ(f,\<rm>m,\<rm>n)) = abs(f`(\<rm>(m\<ra>n)) \<rs> f`(\<rm>m) \<rs> f`(\<rm>n))"
using Int_ZF_1_1_L5 by simp;
also from A1 A2 A3 T I have "… = abs(δ(f,m,n))"
using Int_ZF_2_1_L18 by simp;
finally show "abs(δ(f,\<rm>m,\<rm>n)) = abs(δ(f,m,n))" by simp;
qed;
text{*Recall that $f$ is a slope iff $f(m+n)-f(m)-f(n)$ is bounded
as $m,n$ ranges over integers. The next lemma is the first
step in showing that we only need to check this condition as $m,n$ ranges
over positive intergers. Namely we show that if the condition holds for
positive integers, then it holds if one integer is positive and the second
one is nonnegative.*}
lemma (in int1) Int_ZF_2_1_L20: assumes A1: "f:\<int>->\<int>" and
A2: "∀a∈\<int>+. ∀b∈\<int>+. abs(δ(f,a,b)) \<lsq> L" and
A3: "m∈\<int>+" "n∈\<int>+"
shows
"\<zero> \<lsq> L"
"abs(δ(f,m,n)) \<lsq> L \<ra> abs(f`(\<zero>))"
proof -
from A1 A2 have
"δ(f,\<one>,\<one>) ∈ \<int>" and "abs(δ(f,\<one>,\<one>)) \<lsq> L"
using int_one_two_are_pos PositiveSet_def Int_ZF_2_1_L3B
by auto;
then show I: "\<zero> \<lsq> L" using Int_ZF_1_3_L19 by simp;
from A1 A3 have T:
"n ∈ \<int>" "f`(n) ∈ \<int>" "f`(\<zero>) ∈ \<int>"
"δ(f,m,n) ∈ \<int>" "abs(δ(f,m,n)) ∈ \<int>"
using PositiveSet_def int_zero_one_are_int apply_funtype
Nonnegative_def Int_ZF_2_1_L3B Int_ZF_2_L14 by auto;
from A3 have "m=\<zero> ∨ m∈\<int>+" using Int_ZF_1_5_L3A by auto;
moreover
{ assume "m = \<zero>"
with T I have "abs(δ(f,m,n)) \<lsq> L \<ra> abs(f`(\<zero>))"
using Int_ZF_1_1_L4 Int_ZF_1_2_L3 Int_ZF_2_L17
int_ord_is_refl refl_def Int_ZF_2_L15F by simp }
moreover
{ assume "m∈\<int>+"
with A2 A3 T have "abs(δ(f,m,n)) \<lsq> L \<ra> abs(f`(\<zero>))"
using int_abs_nonneg Int_ZF_2_L15F by simp }
ultimately show "abs(δ(f,m,n)) \<lsq> L \<ra> abs(f`(\<zero>))"
by auto;
qed;
text{*If the slope condition holds for all pairs of integers such that one integer is
positive and the second one is nonnegative, then it holds when both integers are
nonnegative.*}
lemma (in int1) Int_ZF_2_1_L21: assumes A1: "f:\<int>->\<int>" and
A2: "∀a∈\<int>+. ∀b∈\<int>+. abs(δ(f,a,b)) \<lsq> L" and
A3: "n∈\<int>+" "m∈\<int>+"
shows "abs(δ(f,m,n)) \<lsq> L \<ra> abs(f`(\<zero>))"
proof -
from A1 A2 have
"δ(f,\<one>,\<one>) ∈ \<int>" and "abs(δ(f,\<one>,\<one>)) \<lsq> L"
using int_one_two_are_pos PositiveSet_def Nonnegative_def Int_ZF_2_1_L3B
by auto;
then have I: "\<zero> \<lsq> L" using Int_ZF_1_3_L19 by simp;
from A1 A3 have T:
"m ∈ \<int>" "f`(m) ∈ \<int>" "f`(\<zero>) ∈ \<int>" "(\<rm>f`(\<zero>)) ∈ \<int>"
"δ(f,m,n) ∈ \<int>" "abs(δ(f,m,n)) ∈ \<int>"
using int_zero_one_are_int apply_funtype Nonnegative_def
Int_ZF_2_1_L3B Int_ZF_2_L14 Int_ZF_1_1_L4 by auto;
from A3 have "n=\<zero> ∨ n∈\<int>+" using Int_ZF_1_5_L3A by auto;
moreover
{ assume "n=\<zero>"
with T have "δ(f,m,n) = \<rm>f`(\<zero>)"
using Int_ZF_1_1_L4 by simp;
with T have "abs(δ(f,m,n)) = abs(f`(\<zero>))"
using Int_ZF_2_L17 by simp;
with T have "abs(δ(f,m,n)) \<lsq> abs(f`(\<zero>))"
using int_ord_is_refl refl_def by simp;
with T I have "abs(δ(f,m,n)) \<lsq> L \<ra> abs(f`(\<zero>))"
using Int_ZF_2_L15F by simp }
moreover
{ assume "n∈\<int>+"
with A2 A3 T have "abs(δ(f,m,n)) \<lsq> L \<ra> abs(f`(\<zero>))"
using int_abs_nonneg Int_ZF_2_L15F by simp }
ultimately show "abs(δ(f,m,n)) \<lsq> L \<ra> abs(f`(\<zero>))"
by auto;
qed;
text{*If the homomorphism difference is bounded on @{text "\<int>+×\<int>+"},
then it is bounded on @{text "\<int>+×\<int>+"}.*}
lemma (in int1) Int_ZF_2_1_L22: assumes A1: "f:\<int>->\<int>" and
A2: "∀a∈\<int>+. ∀b∈\<int>+. abs(δ(f,a,b)) \<lsq> L"
shows "∃M. ∀m∈\<int>+. ∀n∈\<int>+. abs(δ(f,m,n)) \<lsq> M"
proof -
from A1 A2 have
"∀m∈\<int>+. ∀n∈\<int>+. abs(δ(f,m,n)) \<lsq> L \<ra> abs(f`(\<zero>)) \<ra> abs(f`(\<zero>))"
using Int_ZF_2_1_L20 Int_ZF_2_1_L21 by simp;
then show ?thesis by auto
qed;
text{*For odd functions we can do better than in @{text "Int_ZF_2_1_L22"}:
if the homomorphism
difference of $f$ is bounded on @{text "\<int>+×\<int>+"}, then it is bounded
on @{text "\<int>×\<int>"}, hence $f$ is a slope.
Loong prof by splitting the @{text "\<int>×\<int>"} into six subsets.*}
lemma (in int1) Int_ZF_2_1_L23: assumes A1: "f:\<int>->\<int>" and
A2: "∀a∈\<int>+. ∀b∈\<int>+. abs(δ(f,a,b)) \<lsq> L"
and A3: "∀x∈\<int>. (\<rm>f`(\<rm>x)) = f`(x)"
shows (*"∃M. ∀m∈\<int>. ∀n∈\<int>. abs(δ(f,m,n)) \<lsq> M"*) "f∈\<S>"
proof -
from A1 A2 have
"∃M.∀a∈\<int>+. ∀b∈\<int>+. abs(δ(f,a,b)) \<lsq> M"
by (rule Int_ZF_2_1_L22);
then obtain M where I: "∀m∈\<int>+. ∀n∈\<int>+. abs(δ(f,m,n)) \<lsq> M"
by auto
{ fix a b assume A4: "a∈\<int>" "b∈\<int>"
then have
"\<zero>\<lsq>a ∧ \<zero>\<lsq>b ∨ a\<lsq>\<zero> ∧ b\<lsq>\<zero> ∨
a\<lsq>\<zero> ∧ \<zero>\<lsq>b ∧ \<zero> \<lsq> a\<ra>b ∨ a\<lsq>\<zero> ∧ \<zero>\<lsq>b ∧ a\<ra>b \<lsq> \<zero> ∨
\<zero>\<lsq>a ∧ b\<lsq>\<zero> ∧ \<zero> \<lsq> a\<ra>b ∨ \<zero>\<lsq>a ∧ b\<lsq>\<zero> ∧ a\<ra>b \<lsq> \<zero>"
using int_plane_split_in6 by simp;
moreover
{ assume "\<zero>\<lsq>a ∧ \<zero>\<lsq>b"
then have "a∈\<int>+" "b∈\<int>+"
using Int_ZF_2_L16 by auto;
with I have "abs(δ(f,a,b)) \<lsq> M" by simp };
moreover
{ assume "a\<lsq>\<zero> ∧ b\<lsq>\<zero>"
with I have "abs(δ(f,\<rm>a,\<rm>b)) \<lsq> M"
using Int_ZF_2_L10A Int_ZF_2_L16 by simp;
with A1 A3 A4 have "abs(δ(f,a,b)) \<lsq> M"
using Int_ZF_2_1_L19 by simp }
moreover
{ assume "a\<lsq>\<zero> ∧ \<zero>\<lsq>b ∧ \<zero> \<lsq> a\<ra>b"
with I have "abs(δ(f,\<rm>a,a\<ra>b)) \<lsq> M"
using Int_ZF_2_L10A Int_ZF_2_L16 by simp;
with A1 A3 A4 have "abs(δ(f,a,b)) \<lsq> M"
using Int_ZF_2_1_L19 by simp }
moreover
{ assume "a\<lsq>\<zero> ∧ \<zero>\<lsq>b ∧ a\<ra>b \<lsq> \<zero>"
with I have "abs(δ(f,b,\<rm>(a\<ra>b))) \<lsq> M"
using Int_ZF_2_L10A Int_ZF_2_L16 by simp;
with A1 A3 A4 have "abs(δ(f,a,b)) \<lsq> M"
using Int_ZF_2_1_L19 by simp };
moreover
{ assume "\<zero>\<lsq>a ∧ b\<lsq>\<zero> ∧ \<zero> \<lsq> a\<ra>b"
with I have "abs(δ(f,\<rm>b,a\<ra>b)) \<lsq> M"
using Int_ZF_2_L10A Int_ZF_2_L16 by simp;
with A1 A3 A4 have "abs(δ(f,a,b)) \<lsq> M"
using Int_ZF_2_1_L19 by simp };
moreover
{ assume "\<zero>\<lsq>a ∧ b\<lsq>\<zero> ∧ a\<ra>b \<lsq> \<zero>"
with I have "abs(δ(f,a,\<rm>(a\<ra>b))) \<lsq> M"
using Int_ZF_2_L10A Int_ZF_2_L16 by simp;
with A1 A3 A4 have "abs(δ(f,a,b)) \<lsq> M"
using Int_ZF_2_1_L19 by simp }
ultimately have "abs(δ(f,a,b)) \<lsq> M" by auto; }
then have "∀m∈\<int>. ∀n∈\<int>. abs(δ(f,m,n)) \<lsq> M" by simp;
with A1 show "f∈\<S>" by (rule Int_ZF_2_1_L5);
qed;
text{* If the homomorphism difference of a function defined
on positive integers is bounded, then the odd extension
of this function is a slope.*}
lemma (in int1) Int_ZF_2_1_L24:
assumes A1: "f:\<int>+->\<int>" and A2: "∀a∈\<int>+. ∀b∈\<int>+. abs(δ(f,a,b)) \<lsq> L"
shows "OddExtension(\<int>,IntegerAddition,IntegerOrder,f) ∈ \<S>"
proof -
let ?g = "OddExtension(\<int>,IntegerAddition,IntegerOrder,f)"
from A1 have "?g : \<int>->\<int>"
using Int_ZF_1_5_L10 by simp
moreover have "∀a∈\<int>+. ∀b∈\<int>+. abs(δ(?g,a,b)) \<lsq> L"
proof -
{ fix a b assume A3: "a∈\<int>+" "b∈\<int>+"
with A1 have "abs(δ(f,a,b)) = abs(δ(?g,a,b))"
using pos_int_closed_add_unfolded Int_ZF_1_5_L11
by simp;
moreover from A2 A3 have "abs(δ(f,a,b)) \<lsq> L" by simp;
ultimately have "abs(δ(?g,a,b)) \<lsq> L" by simp;
} then show ?thesis by simp;
qed
moreover from A1 have "∀x∈\<int>. (\<rm>?g`(\<rm>x)) = ?g`(x)"
using int_oddext_is_odd_alt by simp;
ultimately show "?g ∈ \<S>" by (rule Int_ZF_2_1_L23);
qed
text{*Type information related to $\gamma$.*}
lemma (in int1) Int_ZF_2_1_L25:
assumes A1: "f:\<int>->\<int>" and A2: "m∈\<int>" "n∈\<int>"
shows
"δ(f,m,\<rm>n) ∈ \<int>"
"δ(f,n,\<rm>n) ∈ \<int>"
"(\<rm>δ(f,n,\<rm>n)) ∈ \<int>"
"f`(\<zero>) ∈ \<int>"
"γ(f,m,n) ∈ \<int>"
proof -
from A1 A2 show T1:
"δ(f,m,\<rm>n) ∈ \<int>" "f`(\<zero>) ∈ \<int>"
using Int_ZF_1_1_L4 Int_ZF_2_1_L3B int_zero_one_are_int apply_funtype
by auto;
from A2 have "(\<rm>n) ∈ \<int>"
using Int_ZF_1_1_L4 by simp;
with A1 A2 show "δ(f,n,\<rm>n) ∈ \<int>"
using Int_ZF_2_1_L3B by simp;
then show "(\<rm>δ(f,n,\<rm>n)) ∈ \<int>"
using Int_ZF_1_1_L4 by simp;
with T1 show "γ(f,m,n) ∈ \<int>"
using Int_ZF_1_1_L5 by simp;
qed;
text{*A couple of formulae involving $f(m-n)$ and $\gamma(f,m,n)$.*}
lemma (in int1) Int_ZF_2_1_L26:
assumes A1: "f:\<int>->\<int>" and A2: "m∈\<int>" "n∈\<int>"
shows
"f`(m\<rs>n) = γ(f,m,n) \<ra> f`(m) \<rs> f`(n)"
"f`(m\<rs>n) = γ(f,m,n) \<ra> (f`(m) \<rs> f`(n))"
"f`(m\<rs>n) \<ra> (f`(n) \<rs> γ(f,m,n)) = f`(m)"
proof -
from A1 A2 have T:
"(\<rm>n) ∈ \<int>" "δ(f,m,\<rm>n) ∈ \<int>"
"f`(\<zero>) ∈ \<int>" "f`(m) ∈ \<int>" "f`(n) ∈ \<int>" "(\<rm>f`(n)) ∈ \<int>"
"(\<rm>δ(f,n,\<rm>n)) ∈ \<int>"
"(\<rm>δ(f,n,\<rm>n)) \<ra> f`(\<zero>) ∈ \<int>"
"γ(f,m,n) ∈ \<int>"
using Int_ZF_1_1_L4 Int_ZF_2_1_L25 apply_funtype Int_ZF_1_1_L5
by auto;
with A1 A2 have "f`(m\<rs>n) =
δ(f,m,\<rm>n) \<ra> ((\<rm>δ(f,n,\<rm>n)) \<ra> f`(\<zero>) \<rs> f`(n)) \<ra> f`(m)"
using Int_ZF_2_1_L3C Int_ZF_2_1_L14A by simp;
with T have "f`(m\<rs>n) =
δ(f,m,\<rm>n) \<ra> ((\<rm>δ(f,n,\<rm>n)) \<ra> f`(\<zero>)) \<ra> f`(m) \<rs> f`(n)"
using Int_ZF_1_2_L16 by simp;
moreover from T have
"δ(f,m,\<rm>n) \<ra> ((\<rm>δ(f,n,\<rm>n)) \<ra> f`(\<zero>)) = γ(f,m,n)"
using Int_ZF_1_1_L7 by simp;
ultimately show I: "f`(m\<rs>n) = γ(f,m,n) \<ra> f`(m) \<rs> f`(n)"
by simp
then have "f`(m\<rs>n) \<ra> (f`(n) \<rs> γ(f,m,n)) =
(γ(f,m,n) \<ra> f`(m) \<rs> f`(n)) \<ra> (f`(n) \<rs> γ(f,m,n))"
by simp
moreover from T have "… = f`(m)" using Int_ZF_1_2_L18
by simp;
ultimately show "f`(m\<rs>n) \<ra> (f`(n) \<rs> γ(f,m,n)) = f`(m)"
by simp;
from T have "γ(f,m,n) ∈ \<int>" "f`(m) ∈ \<int>" "(\<rm>f`(n)) ∈ \<int>"
by auto;
then have
"γ(f,m,n) \<ra> f`(m) \<ra> (\<rm>f`(n)) = γ(f,m,n) \<ra> (f`(m) \<ra> (\<rm>f`(n)))"
by (rule Int_ZF_1_1_L7);
with I show "f`(m\<rs>n) = γ(f,m,n) \<ra> (f`(m) \<rs> f`(n))" by simp;
qed;
text{*A formula expressing the difference between $f(m-n-k)$ and
$f(m)-f(n)-f(k)$ in terms of $\gamma$.*}
lemma (in int1) Int_ZF_2_1_L26A:
assumes A1: "f:\<int>->\<int>" and A2: "m∈\<int>" "n∈\<int>" "k∈\<int>"
shows
"f`(m\<rs>n\<rs>k) \<rs> (f`(m)\<rs> f`(n) \<rs> f`(k)) = γ(f,m\<rs>n,k) \<ra> γ(f,m,n)"
proof -
from A1 A2 have
T: "m\<rs>n ∈ \<int>" "γ(f,m\<rs>n,k) ∈ \<int>" "f`(m) \<rs> f`(n) \<rs> f`(k) ∈ \<int>" and
T1: "γ(f,m,n) ∈ \<int>" "f`(m) \<rs> f`(n) ∈ \<int>" "(\<rm>f`(k)) ∈ \<int>"
using Int_ZF_1_1_L4 Int_ZF_1_1_L5 Int_ZF_2_1_L25 apply_funtype
by auto
from A1 A2 have
"f`(m\<rs>n) \<rs> f`(k) = γ(f,m,n) \<ra> (f`(m) \<rs> f`(n)) \<ra> (\<rm>f`(k))"
using Int_ZF_2_1_L26 by simp;
also from T1 have "… = γ(f,m,n) \<ra> (f`(m) \<rs> f`(n) \<ra> (\<rm>f`(k)))"
by (rule Int_ZF_1_1_L7);
finally have
"f`(m\<rs>n) \<rs> f`(k) = γ(f,m,n) \<ra> (f`(m) \<rs> f`(n) \<rs> f`(k))"
by simp;
moreover from A1 A2 T have
"f`(m\<rs>n\<rs>k) = γ(f,m\<rs>n,k) \<ra> (f`(m\<rs>n)\<rs>f`(k))"
using Int_ZF_2_1_L26 by simp;
ultimately have
"f`(m\<rs>n\<rs>k) \<rs> (f`(m)\<rs> f`(n) \<rs> f`(k)) =
γ(f,m\<rs>n,k) \<ra> ( γ(f,m,n) \<ra> (f`(m) \<rs> f`(n) \<rs> f`(k)))
\<rs> (f`(m)\<rs> f`(n) \<rs> f`(k))"
by simp;
with T T1 show ?thesis
using Int_ZF_1_2_L17 by simp;
qed;
text{*If $s$ is a slope, then $\gamma (s,m,n)$ is uniformly bounded.*}
lemma (in int1) Int_ZF_2_1_L27: assumes A1: "s∈\<S>"
shows "∃L∈\<int>. ∀m∈\<int>.∀n∈\<int>. abs(γ(s,m,n)) \<lsq> L"
proof -
let ?L = "maxδ(s) \<ra> maxδ(s) \<ra> abs(s`(\<zero>))"
from A1 have T:
"maxδ(s) ∈ \<int>" "abs(s`(\<zero>)) ∈ \<int>" "?L ∈ \<int>"
using Int_ZF_2_1_L8 int_zero_one_are_int Int_ZF_2_1_L2B
Int_ZF_2_L14 Int_ZF_1_1_L5 by auto
moreover
{ fix m
fix n
assume A2: "m∈\<int>" "n∈\<int>"
with A1 have T:
"(\<rm>n) ∈ \<int>"
"δ(s,m,\<rm>n) ∈ \<int>"
"δ(s,n,\<rm>n) ∈ \<int>"
"(\<rm>δ(s,n,\<rm>n)) ∈ \<int>"
"s`(\<zero>) ∈ \<int>" "abs(s`(\<zero>)) ∈ \<int>"
using Int_ZF_1_1_L4 AlmostHoms_def Int_ZF_2_1_L25 Int_ZF_2_L14
by auto;
with T have
"abs(δ(s,m,\<rm>n) \<rs> δ(s,n,\<rm>n) \<ra> s`(\<zero>)) \<lsq>
abs(δ(s,m,\<rm>n)) \<ra> abs(\<rm>δ(s,n,\<rm>n)) \<ra> abs(s`(\<zero>))"
using Int_triangle_ineq3 by simp;
moreover from A1 A2 T have
"abs(δ(s,m,\<rm>n)) \<ra> abs(\<rm>δ(s,n,\<rm>n)) \<ra> abs(s`(\<zero>)) \<lsq> ?L"
using Int_ZF_2_1_L7 int_ineq_add_sides int_ord_transl_inv Int_ZF_2_L17
by simp;
ultimately have "abs(δ(s,m,\<rm>n) \<rs> δ(s,n,\<rm>n) \<ra> s`(\<zero>)) \<lsq> ?L"
by (rule Int_order_transitive);
then have "abs(γ(s,m,n)) \<lsq> ?L" by simp }
ultimately show "∃L∈\<int>. ∀m∈\<int>.∀n∈\<int>. abs(γ(s,m,n)) \<lsq> L"
by auto;
qed;
text{*If $s$ is a slope, then $s(m) \leq s(m-1) + M$, where $L$ does not depend
on $m$.*}
lemma (in int1) Int_ZF_2_1_L28: assumes A1: "s∈\<S>"
shows "∃M∈\<int>. ∀m∈\<int>. s`(m) \<lsq> s`(m\<rs>\<one>) \<ra> M"
proof -
from A1 have
"∃L∈\<int>. ∀m∈\<int>.∀n∈\<int>.abs(γ(s,m,n)) \<lsq> L"
using Int_ZF_2_1_L27 by simp;
then obtain L where T: "L∈\<int>" and "∀m∈\<int>.∀n∈\<int>.abs(γ(s,m,n)) \<lsq> L"
using Int_ZF_2_1_L27 by auto;
then have I: "∀m∈\<int>.abs(γ(s,m,\<one>)) \<lsq> L"
using int_zero_one_are_int by simp;
let ?M = "s`(\<one>) \<ra> L"
from A1 T have "?M ∈ \<int>"
using int_zero_one_are_int Int_ZF_2_1_L2B Int_ZF_1_1_L5
by simp;
moreover
{ fix m assume A2: "m∈\<int>"
with A1 have
T1: "s:\<int>->\<int>" "m∈\<int>" "\<one>∈\<int>" and
T2: "γ(s,m,\<one>) ∈ \<int>" "s`(\<one>) ∈ \<int>"
using int_zero_one_are_int AlmostHoms_def
Int_ZF_2_1_L25 by auto;
from A2 T1 have T3: "s`(m\<rs>\<one>) ∈ \<int>"
using Int_ZF_1_1_L5 apply_funtype by simp;
from I A2 T2 have
"(\<rm>γ(s,m,\<one>)) \<lsq> abs(γ(s,m,\<one>))"
"abs(γ(s,m,\<one>)) \<lsq> L"
using Int_ZF_2_L19C by auto;
then have "(\<rm>γ(s,m,\<one>)) \<lsq> L"
by (rule Int_order_transitive);
with T2 T3 have
"s`(m\<rs>\<one>) \<ra> (s`(\<one>) \<rs> γ(s,m,\<one>)) \<lsq> s`(m\<rs>\<one>) \<ra> ?M"
using int_ord_transl_inv by simp;
moreover from T1 have
"s`(m\<rs>\<one>) \<ra> (s`(\<one>) \<rs> γ(s,m,\<one>)) = s`(m)"
by (rule Int_ZF_2_1_L26)
ultimately have "s`(m) \<lsq> s`(m\<rs>\<one>) \<ra> ?M" by simp }
ultimately show "∃M∈\<int>. ∀m∈\<int>. s`(m) \<lsq> s`(m\<rs>\<one>) \<ra> M"
by auto;
qed;
text{*If $s$ is a slope, then the difference between
$s(m-n-k)$ and $s(m)-s(n)-s(k)$ is uniformly bounded.*}
lemma (in int1) Int_ZF_2_1_L29: assumes A1: "s∈\<S>"
shows
"∃M∈\<int>. ∀m∈\<int>.∀n∈\<int>.∀k∈\<int>. abs(s`(m\<rs>n\<rs>k) \<rs> (s`(m)\<rs>s`(n)\<rs>s`(k))) \<lsq>M"
proof -
from A1 have "∃L∈\<int>. ∀m∈\<int>.∀n∈\<int>. abs(γ(s,m,n)) \<lsq> L"
using Int_ZF_2_1_L27 by simp;
then obtain L where I: "L∈\<int>" and
II: "∀m∈\<int>.∀n∈\<int>. abs(γ(s,m,n)) \<lsq> L"
by auto;
from I have "L\<ra>L ∈ \<int>"
using Int_ZF_1_1_L5 by simp;
moreover
{ fix m n k assume A2: "m∈\<int>" "n∈\<int>" "k∈\<int>"
with A1 have T:
"m\<rs>n ∈ \<int>" "γ(s,m\<rs>n,k) ∈ \<int>" "γ(s,m,n) ∈ \<int>"
using Int_ZF_1_1_L5 AlmostHoms_def Int_ZF_2_1_L25
by auto;
then have
I: "abs(γ(s,m\<rs>n,k) \<ra> γ(s,m,n)) \<lsq> abs(γ(s,m\<rs>n,k)) \<ra> abs(γ(s,m,n))"
using Int_triangle_ineq by simp;
from II A2 T have
"abs(γ(s,m\<rs>n,k)) \<lsq> L"
"abs(γ(s,m,n)) \<lsq> L"
by auto;
then have "abs(γ(s,m\<rs>n,k)) \<ra> abs(γ(s,m,n)) \<lsq> L\<ra>L"
using int_ineq_add_sides by simp;
with I have "abs(γ(s,m\<rs>n,k) \<ra> γ(s,m,n)) \<lsq> L\<ra>L"
by (rule Int_order_transitive);
moreover from A1 A2 have
"s`(m\<rs>n\<rs>k) \<rs> (s`(m)\<rs> s`(n) \<rs> s`(k)) = γ(s,m\<rs>n,k) \<ra> γ(s,m,n)"
using AlmostHoms_def Int_ZF_2_1_L26A by simp;
ultimately have
"abs(s`(m\<rs>n\<rs>k) \<rs> (s`(m)\<rs> s`(n) \<rs> s`(k))) \<lsq> L\<ra>L"
by simp }
ultimately show ?thesis by auto;
qed;
text{*If $s$ is a slope, then we can find integers $M,K$ such that
$s(m-n-k) \leq s(m)-s(n)-s(k) + M$ and $s(m)-s(n)-s(k) + K \leq s(m-n-k)$,
for all integer $m,n,k$.*}
lemma (in int1) Int_ZF_2_1_L30: assumes A1: "s∈\<S>"
shows
"∃M∈\<int>. ∀m∈\<int>.∀n∈\<int>.∀k∈\<int>. s`(m\<rs>n\<rs>k) \<lsq> s`(m)\<rs>s`(n)\<rs>s`(k)\<ra>M"
"∃K∈\<int>. ∀m∈\<int>.∀n∈\<int>.∀k∈\<int>. s`(m)\<rs>s`(n)\<rs>s`(k)\<ra>K \<lsq> s`(m\<rs>n\<rs>k)"
proof -
from A1 have
"∃M∈\<int>. ∀m∈\<int>.∀n∈\<int>.∀k∈\<int>. abs(s`(m\<rs>n\<rs>k) \<rs> (s`(m)\<rs>s`(n)\<rs>s`(k))) \<lsq>M"
using Int_ZF_2_1_L29 by simp;
then obtain M where I: "M∈\<int>" and II:
"∀m∈\<int>.∀n∈\<int>.∀k∈\<int>. abs(s`(m\<rs>n\<rs>k) \<rs> (s`(m)\<rs>s`(n)\<rs>s`(k))) \<lsq>M"
by auto;
from I have III: "(\<rm>M) ∈ \<int>" using Int_ZF_1_1_L4 by simp
{ fix m n k assume A2: "m∈\<int>" "n∈\<int>" "k∈\<int>"
with A1 have "s`(m\<rs>n\<rs>k) ∈ \<int>" and "s`(m)\<rs>s`(n)\<rs>s`(k) ∈ \<int>"
using Int_ZF_1_1_L5 Int_ZF_2_1_L2B by auto;
moreover from II A2 have
"abs(s`(m\<rs>n\<rs>k) \<rs> (s`(m)\<rs>s`(n)\<rs>s`(k))) \<lsq>M"
by simp;
ultimately have
"s`(m\<rs>n\<rs>k) \<lsq> s`(m)\<rs>s`(n)\<rs>s`(k)\<ra>M ∧
s`(m)\<rs>s`(n)\<rs>s`(k) \<rs> M \<lsq> s`(m\<rs>n\<rs>k)"
using Int_triangle_ineq2 by simp;
} then have
"∀m∈\<int>.∀n∈\<int>.∀k∈\<int>. s`(m\<rs>n\<rs>k) \<lsq> s`(m)\<rs>s`(n)\<rs>s`(k)\<ra>M"
"∀m∈\<int>.∀n∈\<int>.∀k∈\<int>. s`(m)\<rs>s`(n)\<rs>s`(k) \<rs> M \<lsq> s`(m\<rs>n\<rs>k)"
by auto;
with I III show
"∃M∈\<int>. ∀m∈\<int>.∀n∈\<int>.∀k∈\<int>. s`(m\<rs>n\<rs>k) \<lsq> s`(m)\<rs>s`(n)\<rs>s`(k)\<ra>M"
"∃K∈\<int>. ∀m∈\<int>.∀n∈\<int>.∀k∈\<int>. s`(m)\<rs>s`(n)\<rs>s`(k)\<ra>K \<lsq> s`(m\<rs>n\<rs>k)"
by auto;
qed;
text{*By definition functions $f,g$ are almost equal if $f-g$* is bounded.
In the next lemma we show it is sufficient to check the boundedness on positive
integers.*}
lemma (in int1) Int_ZF_2_1_L31: assumes A1: "s∈\<S>" "r∈\<S>"
and A2: "∀m∈\<int>+. abs(s`(m)\<rs>r`(m)) \<lsq> L"
shows "s ∼ r"
proof -
let ?a = "abs(s`(\<zero>) \<rs> r`(\<zero>))"
let ?c = "\<two>·maxδ(s) \<ra> \<two>·maxδ(r) \<ra> L"
let ?M = "Maximum(IntegerOrder,{?a,L,?c})"
from A2 have "abs(s`(\<one>)\<rs>r`(\<one>)) \<lsq> L"
using int_one_two_are_pos by simp
then have T: "L∈\<int>" using Int_ZF_2_L1A by simp;
moreover from A1 have "?a ∈ \<int>"
using int_zero_one_are_int Int_ZF_2_1_L2B
Int_ZF_1_1_L5 Int_ZF_2_L14 by simp
moreover from A1 T have "?c ∈ \<int>"
using Int_ZF_2_1_L8 int_two_three_are_int Int_ZF_1_1_L5
by simp
ultimately have
I: "?a \<lsq> ?M" and
II: "L \<lsq> ?M" and
III: "?c \<lsq> ?M"
using Int_ZF_1_4_L1A by auto;
{ fix m assume A5: "m∈\<int>"
with A1 have T:
"s`(m) ∈ \<int>" "r`(m) ∈ \<int>" "s`(m) \<rs> r`(m) ∈ \<int>"
"s`(\<rm>m) ∈ \<int>" "r`(\<rm>m) ∈ \<int>"
using Int_ZF_2_1_L2B Int_ZF_1_1_L4 Int_ZF_1_1_L5
by auto;
from A5 have "m=\<zero> ∨ m∈\<int>+ ∨ (\<rm>m) ∈ \<int>+"
using int_decomp_cases by simp
moreover
{ assume "m=\<zero>"
with I have "abs(s`(m) \<rs> r`(m)) \<lsq> ?M"
by simp }
moreover
{ assume "m∈\<int>+"
with A2 II have
"abs(s`(m)\<rs>r`(m)) \<lsq> L" and "L\<lsq>?M"
by auto
then have "abs(s`(m)\<rs>r`(m)) \<lsq> ?M"
by (rule Int_order_transitive) }
moreover
{ assume A6: "(\<rm>m) ∈ \<int>+"
from T have "abs(s`(m)\<rs>r`(m)) \<lsq>
abs(s`(m)\<ra>s`(\<rm>m)) \<ra> abs(r`(m)\<ra>r`(\<rm>m)) \<ra> abs(s`(\<rm>m)\<rs>r`(\<rm>m))"
using Int_ZF_1_3_L22A by simp;
moreover
from A1 A2 III A5 A6 have
"abs(s`(m)\<ra>s`(\<rm>m)) \<ra> abs(r`(m)\<ra>r`(\<rm>m)) \<ra> abs(s`(\<rm>m)\<rs>r`(\<rm>m)) \<lsq> ?c"
"?c \<lsq> ?M"
using Int_ZF_2_1_L14 int_ineq_add_sides by auto;
then have
"abs(s`(m)\<ra>s`(\<rm>m)) \<ra> abs(r`(m)\<ra>r`(\<rm>m)) \<ra> abs(s`(\<rm>m)\<rs>r`(\<rm>m)) \<lsq> ?M"
by (rule Int_order_transitive);
ultimately have "abs(s`(m)\<rs>r`(m)) \<lsq> ?M"
by (rule Int_order_transitive); }
ultimately have "abs(s`(m) \<rs> r`(m)) \<lsq> ?M"
by auto;
} then have "∀m∈\<int>. abs(s`(m)\<rs>r`(m)) \<lsq> ?M"
by simp;
with A1 show "s ∼ r" by (rule Int_ZF_2_1_L9);
qed;
text{*A sufficient condition for an odd slope to be almost equal to identity:
If for all positive integers the value of the slope at $m$ is between $m$ and
$m$ plus some constant independent of $m$, then the slope is almost identity.*}
lemma (in int1) Int_ZF_2_1_L32: assumes A1: "s∈\<S>" "M∈\<int>"
and A2: "∀m∈\<int>+. m \<lsq> s`(m) ∧ s`(m) \<lsq> m\<ra>M"
shows "s ∼ id(\<int>)"
proof -
let ?r = "id(\<int>)"
from A1 have "s∈\<S>" "?r ∈ \<S>"
using Int_ZF_2_1_L17 by auto
moreover from A1 A2 have "∀m∈\<int>+. abs(s`(m)\<rs>?r`(m)) \<lsq> M"
using Int_ZF_1_3_L23 PositiveSet_def id_conv by simp;
ultimately show "s ∼ id(\<int>)" by (rule Int_ZF_2_1_L31);
qed;
text{*A lemma about adding a constant to slopes. This is actually proven in
@{text "Group_ZF_3_5_L1"}, in @{text "Group_ZF_3.thy"} here we just refer to
that lemma to show it in notation used for integers. Unfortunately we have
to use raw set notation in the proof.*}
lemma (in int1) Int_ZF_2_1_L33:
assumes A1: "s∈\<S>" and A2: "c∈\<int>" and
A3: "r = {⟨m,s`(m)\<ra>c⟩. m∈\<int>}"
shows
"∀m∈\<int>. r`(m) = s`(m)\<ra>c"
"r∈\<S>"
"s ∼ r"
proof -
let ?G = "\<int>"
let ?f = "IntegerAddition"
let ?AH = "AlmostHoms(?G, ?f)"
from prems have I:
"group1(?G, ?f)"
"s ∈ AlmostHoms(?G, ?f)"
"c ∈ ?G"
"r = {⟨x, ?f`⟨s`(x), c⟩⟩ . x ∈ ?G}"
using Int_ZF_2_1_L1 by auto;
then have "∀x∈?G. r`(x) = ?f`⟨s`(x),c⟩"
by (rule group1.Group_ZF_3_5_L1);
moreover from I have "r ∈ AlmostHoms(?G, ?f)"
by (rule group1.Group_ZF_3_5_L1)
moreover from I have
"⟨s, r⟩ ∈ QuotientGroupRel(AlmostHoms(?G, ?f), AlHomOp1(?G, ?f), FinRangeFunctions(?G, ?G))"
by (rule group1.Group_ZF_3_5_L1);
ultimately show
"∀m∈\<int>. r`(m) = s`(m)\<ra>c"
"r∈\<S>"
"s ∼ r"
by auto;
qed
section{*Composing slopes*}
text{*Composition of slopes is not commutative. However, as we show in this
section if $f$ and $g$ are slopes then the range of $f\circ g - g\circ f$
is bounded. This allows to show that the multiplication of real
numbers is commutative.*}
text{*Two useful estimates.*}
lemma (in int1) Int_ZF_2_2_L1:
assumes A1: "f:\<int>->\<int>" and A2: "p∈\<int>" "q∈\<int>"
shows
"abs(f`((p\<ra>\<one>)·q)\<rs>(p\<ra>\<one>)·f`(q)) \<lsq> abs(δ(f,p·q,q))\<ra>abs(f`(p·q)\<rs>p·f`(q))"
"abs(f`((p\<rs>\<one>)·q)\<rs>(p\<rs>\<one>)·f`(q)) \<lsq> abs(δ(f,(p\<rs>\<one>)·q,q))\<ra>abs(f`(p·q)\<rs>p·f`(q))"
proof -;
let ?R = "\<int>"
let ?A = "IntegerAddition"
let ?M = "IntegerMultiplication"
let ?I = "GroupInv(?R, ?A)"
let ?a = "f`((p\<ra>\<one>)·q)"
let ?b = "p"
let ?c = "f`(q)"
let ?d = "f`(p·q)"
from A1 A2 have T1:
"ring0(?R, ?A, ?M)" "?a ∈ ?R" "?b ∈ ?R" "?c ∈ ?R" "?d ∈ ?R"
using Int_ZF_1_1_L2 int_zero_one_are_int Int_ZF_1_1_L5 apply_funtype
by auto;
then have
"?A`⟨?a,?I`(?M`⟨?A`⟨?b, TheNeutralElement(?R, ?M)⟩,?c⟩)⟩ =
?A`⟨?A`⟨?A`⟨?a,?I`(?d)⟩,?I`(?c)⟩,?A`⟨?d, ?I`(?M`⟨?b, ?c⟩)⟩⟩"
by (rule ring0.Ring_ZF_2_L2);
with A2 have
"f`((p\<ra>\<one>)·q)\<rs>(p\<ra>\<one>)·f`(q) = δ(f,p·q,q)\<ra>(f`(p·q)\<rs>p·f`(q))"
using int_zero_one_are_int Int_ZF_1_1_L1 Int_ZF_1_1_L4 by simp;
moreover from A1 A2 T1 have "δ(f,p·q,q) ∈ \<int>" "f`(p·q)\<rs>p·f`(q) ∈ \<int>"
using Int_ZF_1_1_L5 apply_funtype by auto;
ultimately show
"abs(f`((p\<ra>\<one>)·q)\<rs>(p\<ra>\<one>)·f`(q)) \<lsq> abs(δ(f,p·q,q))\<ra>abs(f`(p·q)\<rs>p·f`(q))"
using Int_triangle_ineq by simp;
from A1 A2 have T1:
"f`((p\<rs>\<one>)·q) ∈ \<int>" "p∈\<int>" "f`(q) ∈ \<int>" "f`(p·q) ∈ \<int>"
using int_zero_one_are_int Int_ZF_1_1_L5 apply_funtype by auto;
then have
"f`((p\<rs>\<one>)·q)\<rs>(p\<rs>\<one>)·f`(q) = (f`(p·q)\<rs>p·f`(q))\<rs>(f`(p·q)\<rs>f`((p\<rs>\<one>)·q)\<rs>f`(q))"
by (rule Int_ZF_1_2_L6);
with A2 have "f`((p\<rs>\<one>)·q)\<rs>(p\<rs>\<one>)·f`(q) = (f`(p·q)\<rs>p·f`(q))\<rs>δ(f,(p\<rs>\<one>)·q,q)"
using Int_ZF_1_2_L7 by simp;
moreover from A1 A2 have
"f`(p·q)\<rs>p·f`(q) ∈ \<int>" "δ(f,(p\<rs>\<one>)·q,q) ∈ \<int>"
using Int_ZF_1_1_L5 int_zero_one_are_int apply_funtype by auto;
ultimately show
"abs(f`((p\<rs>\<one>)·q)\<rs>(p\<rs>\<one>)·f`(q)) \<lsq> abs(δ(f,(p\<rs>\<one>)·q,q))\<ra>abs(f`(p·q)\<rs>p·f`(q))"
using Int_triangle_ineq1 by simp;
qed;
text{*If $f$ is a slope, then
$|f(p\cdot q)-p\cdot f(q)|\leq (|p|+1)\cdot$@{text "maxδ(f)"}.
The proof is by induction on $p$ and the next lemma is the induction step for the case when $0\leq p$.*}
lemma (in int1) Int_ZF_2_2_L2:
assumes A1: "f∈\<S>" and A2: "\<zero>\<lsq>p" "q∈\<int>"
and A3: "abs(f`(p·q)\<rs>p·f`(q)) \<lsq> (abs(p)\<ra>\<one>)·maxδ(f)"
shows
"abs(f`((p\<ra>\<one>)·q)\<rs>(p\<ra>\<one>)·f`(q)) \<lsq> (abs(p\<ra>\<one>)\<ra> \<one>)·maxδ(f)"
proof -
from A2 have "q∈\<int>" "p·q ∈ \<int>"
using Int_ZF_2_L1A Int_ZF_1_1_L5 by auto;
with A1 have I: "abs(δ(f,p·q,q)) \<lsq> maxδ(f)" by (rule Int_ZF_2_1_L7);
moreover from A3 have "abs(f`(p·q)\<rs>p·f`(q)) \<lsq> (abs(p)\<ra>\<one>)·maxδ(f)" .
moreover from A1 A2 have
"abs(f`((p\<ra>\<one>)·q)\<rs>(p\<ra>\<one>)·f`(q)) \<lsq> abs(δ(f,p·q,q))\<ra>abs(f`(p·q)\<rs>p·f`(q))"
using AlmostHoms_def Int_ZF_2_L1A Int_ZF_2_2_L1 by simp;
ultimately have
"abs(f`((p\<ra>\<one>)·q)\<rs>(p\<ra>\<one>)·f`(q)) \<lsq> maxδ(f)\<ra>(abs(p)\<ra>\<one>)·maxδ(f)"
by (rule Int_ZF_2_L15);
moreover from I A2 have
"maxδ(f)\<ra>(abs(p)\<ra>\<one>)·maxδ(f) = (abs(p\<ra>\<one>)\<ra> \<one>)·maxδ(f)"
using Int_ZF_2_L1A Int_ZF_1_2_L2 by simp;
ultimately show
"abs(f`((p\<ra>\<one>)·q)\<rs>(p\<ra>\<one>)·f`(q)) \<lsq> (abs(p\<ra>\<one>)\<ra> \<one>)·maxδ(f)"
by simp;
qed;
text{*If $f$ is a slope, then
$|f(p\cdot q)-p\cdot f(q)|\leq (|p|+1)\cdot$@{text "maxδ"}.
The proof is by induction on $p$ and the next lemma is the induction step for the case when $p\leq 0$.*}
lemma (in int1) Int_ZF_2_2_L3:
assumes A1: "f∈\<S>" and A2: "p\<lsq>\<zero>" "q∈\<int>"
and A3: "abs(f`(p·q)\<rs>p·f`(q)) \<lsq> (abs(p)\<ra>\<one>)·maxδ(f)"
shows "abs(f`((p\<rs>\<one>)·q)\<rs>(p\<rs>\<one>)·f`(q)) \<lsq> (abs(p\<rs>\<one>)\<ra> \<one>)·maxδ(f)"
proof -;
from A2 have "q∈\<int>" "(p\<rs>\<one>)·q ∈ \<int>"
using Int_ZF_2_L1A int_zero_one_are_int Int_ZF_1_1_L5 by auto;
with A1 have I: "abs(δ(f,(p\<rs>\<one>)·q,q)) \<lsq> maxδ(f)" by (rule Int_ZF_2_1_L7);
moreover from A3 have "abs(f`(p·q)\<rs>p·f`(q)) \<lsq> (abs(p)\<ra>\<one>)·maxδ(f)" .
moreover from A1 A2 have
"abs(f`((p\<rs>\<one>)·q)\<rs>(p\<rs>\<one>)·f`(q)) \<lsq> abs(δ(f,(p\<rs>\<one>)·q,q))\<ra>abs(f`(p·q)\<rs>p·f`(q))"
using AlmostHoms_def Int_ZF_2_L1A Int_ZF_2_2_L1 by simp;
ultimately have
"abs(f`((p\<rs>\<one>)·q)\<rs>(p\<rs>\<one>)·f`(q)) \<lsq> maxδ(f)\<ra>(abs(p)\<ra>\<one>)·maxδ(f)"
by (rule Int_ZF_2_L15);
with I A2 show ?thesis using Int_ZF_2_L1A Int_ZF_1_2_L5 by simp;
qed;
text{*If $f$ is a slope, then
$|f(p\cdot q)-p\cdot f(q)|\leq (|p|+1)\cdot$@{text "maxδ"}$(f)$.*}
lemma (in int1) Int_ZF_2_2_L4:
assumes A1: "f∈\<S>" and A2: "p∈\<int>" "q∈\<int>"
shows "abs(f`(p·q)\<rs>p·f`(q)) \<lsq> (abs(p)\<ra>\<one>)·maxδ(f)"
proof (cases "\<zero>\<lsq>p")
assume "\<zero>\<lsq>p"
moreover from A1 A2 have "abs(f`(\<zero>·q)\<rs>\<zero>·f`(q)) \<lsq> (abs(\<zero>)\<ra>\<one>)·maxδ(f)"
using int_zero_one_are_int Int_ZF_2_1_L2B Int_ZF_1_1_L4
Int_ZF_2_1_L8 Int_ZF_2_L18 by simp;
moreover from A1 A2 have
"∀p. \<zero>\<lsq>p ∧ abs(f`(p·q)\<rs>p·f`(q)) \<lsq> (abs(p)\<ra>\<one>)·maxδ(f) -->
abs(f`((p\<ra>\<one>)·q)\<rs>(p\<ra>\<one>)·f`(q)) \<lsq> (abs(p\<ra>\<one>)\<ra> \<one>)·maxδ(f)"
using Int_ZF_2_2_L2 by simp;
ultimately show "abs(f`(p·q)\<rs>p·f`(q)) \<lsq> (abs(p)\<ra>\<one>)·maxδ(f)"
by (rule Induction_on_int);
next assume "¬(\<zero>\<lsq>p)"
with A2 have "p\<lsq>\<zero>" using Int_ZF_2_L19A by simp;
moreover from A1 A2 have "abs(f`(\<zero>·q)\<rs>\<zero>·f`(q)) \<lsq> (abs(\<zero>)\<ra>\<one>)·maxδ(f)"
using int_zero_one_are_int Int_ZF_2_1_L2B Int_ZF_1_1_L4
Int_ZF_2_1_L8 Int_ZF_2_L18 by simp;
moreover from A1 A2 have
"∀p. p\<lsq>\<zero> ∧ abs(f`(p·q)\<rs>p·f`(q)) \<lsq> (abs(p)\<ra>\<one>)·maxδ(f) -->
abs(f`((p\<rs>\<one>)·q)\<rs>(p\<rs>\<one>)·f`(q)) \<lsq> (abs(p\<rs>\<one>)\<ra> \<one>)·maxδ(f)"
using Int_ZF_2_2_L3 by simp;
ultimately show "abs(f`(p·q)\<rs>p·f`(q)) \<lsq> (abs(p)\<ra>\<one>)·maxδ(f)"
by (rule Back_induct_on_int);
qed;
text{*The next elegant result is Lemma 7 in the Arthan's paper \cite{Arthan2004} .*}
lemma (in int1) Arthan_Lem_7:
assumes A1: "f∈\<S>" and A2: "p∈\<int>" "q∈\<int>"
shows "abs(q·f`(p)\<rs>p·f`(q)) \<lsq> (abs(p)\<ra>abs(q)\<ra>\<two>)·maxδ(f)"
proof -;
from A1 A2 have T:
"q·f`(p)\<rs>f`(p·q) ∈ \<int>"
"f`(p·q)\<rs>p·f`(q) ∈ \<int>"
"f`(q·p) ∈ \<int>" "f`(p·q) ∈ \<int>"
"q·f`(p) ∈ \<int>" "p·f`(q) ∈ \<int>"
"maxδ(f) ∈ \<int>"
"abs(q) ∈ \<int>" "abs(p) ∈ \<int>"
using Int_ZF_1_1_L5 Int_ZF_2_1_L2B Int_ZF_2_1_L7 Int_ZF_2_L14 by auto;
moreover have "abs(q·f`(p)\<rs>f`(p·q)) \<lsq> (abs(q)\<ra>\<one>)·maxδ(f)"
proof -
from A1 A2 have "abs(f`(q·p)\<rs>q·f`(p)) \<lsq> (abs(q)\<ra>\<one>)·maxδ(f)"
using Int_ZF_2_2_L4 by simp;
with T A2 show ?thesis
using Int_ZF_2_L20 Int_ZF_1_1_L5 by simp;
qed;
moreover from A1 A2 have "abs(f`(p·q)\<rs>p·f`(q)) \<lsq> (abs(p)\<ra>\<one>)·maxδ(f)"
using Int_ZF_2_2_L4 by simp;
ultimately have
"abs(q·f`(p)\<rs>f`(p·q)\<ra>(f`(p·q)\<rs>p·f`(q))) \<lsq> (abs(q)\<ra>\<one>)·maxδ(f)\<ra>(abs(p)\<ra>\<one>)·maxδ(f)"
using Int_ZF_2_L21 by simp;
with T show ?thesis using Int_ZF_1_2_L9 int_zero_one_are_int Int_ZF_1_2_L10
by simp;
qed;
text{*This is Lemma 8 in the Arthan's paper.*}
lemma (in int1) Arthan_Lem_8: assumes A1: "f∈\<S>"
shows "∃A B. A∈\<int> ∧ B∈\<int> ∧ (∀p∈\<int>. abs(f`(p)) \<lsq> A·abs(p)\<ra>B)"
proof -
let ?A = "maxδ(f) \<ra> abs(f`(\<one>))"
let ?B = "\<three>·maxδ(f)"
from A1 have "?A∈\<int>" "?B∈\<int>"
using int_zero_one_are_int Int_ZF_1_1_L5 Int_ZF_2_1_L2B
Int_ZF_2_1_L7 Int_ZF_2_L14 by auto;
moreover have "∀p∈\<int>. abs(f`(p)) \<lsq> ?A·abs(p)\<ra>?B"
proof
fix p assume A2: "p∈\<int>"
with A1 have T:
"f`(p) ∈ \<int>" "abs(p) ∈ \<int>" "f`(\<one>) ∈ \<int>"
"p·f`(\<one>) ∈ \<int>" "\<three>∈\<int>" "maxδ(f) ∈ \<int>"
using Int_ZF_2_1_L2B Int_ZF_2_L14 int_zero_one_are_int
Int_ZF_1_1_L5 Int_ZF_2_1_L7 by auto;
from A1 A2 have
"abs(\<one>·f`(p)\<rs>p·f`(\<one>)) \<lsq> (abs(p)\<ra>abs(\<one>)\<ra>\<two>)·maxδ(f)"
using int_zero_one_are_int Arthan_Lem_7 by simp;
with T have "abs(f`(p)) \<lsq> abs(p·f`(\<one>))\<ra>(abs(p)\<ra>\<three>)·maxδ(f)"
using Int_ZF_2_L16A Int_ZF_1_1_L4 Int_ZF_1_2_L11
Int_triangle_ineq2 by simp
with A2 T show "abs(f`(p)) \<lsq> ?A·abs(p)\<ra>?B"
using Int_ZF_1_3_L14 by simp;
qed
ultimately show ?thesis by auto;
qed;
text{*If $f$ and $g$ are slopes, then $f\circ g$ is equivalent
(almost equal) to $g\circ f$. This is Theorem 9 in Arthan's paper \cite{Arthan2004} .*}
theorem (in int1) Arthan_Th_9: assumes A1: "f∈\<S>" "g∈\<S>"
shows "fog ∼ gof"
proof -
from A1 have
"∃A B. A∈\<int> ∧ B∈\<int> ∧ (∀p∈\<int>. abs(f`(p)) \<lsq> A·abs(p)\<ra>B)"
"∃C D. C∈\<int> ∧ D∈\<int> ∧ (∀p∈\<int>. abs(g`(p)) \<lsq> C·abs(p)\<ra>D)"
using Arthan_Lem_8 by auto;
then obtain A B C D where D1: "A∈\<int>" "B∈\<int>" "C∈\<int>" "D∈\<int>" and D2:
"∀p∈\<int>. abs(f`(p)) \<lsq> A·abs(p)\<ra>B"
"∀p∈\<int>. abs(g`(p)) \<lsq> C·abs(p)\<ra>D"
by auto;
let ?E = "maxδ(g)·(A\<ra>\<one>) \<ra> maxδ(f)·(C\<ra>\<one>)"
let ?F = "(B·maxδ(g) \<ra> \<two>·maxδ(g)) \<ra> (D·maxδ(f) \<ra> \<two>·maxδ(f))"
{ fix p assume A2: "p∈\<int>"
with A1 have T1:
"g`(p) ∈ \<int>" "f`(p) ∈ \<int>" "abs(p) ∈ \<int>" "\<two> ∈ \<int>"
"f`(g`(p)) ∈ \<int>" "g`(f`(p)) ∈ \<int>" "f`(g`(p)) \<rs> g`(f`(p)) ∈ \<int>"
"p·f`(g`(p)) ∈ \<int>" "p·g`(f`(p)) ∈ \<int>"
"abs(f`(g`(p))\<rs>g`(f`(p))) ∈ \<int>"
using Int_ZF_2_1_L2B Int_ZF_2_1_L10 Int_ZF_1_1_L5 Int_ZF_2_L14 int_two_three_are_int
by auto;
with A1 A2 have
"abs((f`(g`(p))\<rs>g`(f`(p)))·p) \<lsq>
(abs(p)\<ra>abs(f`(p))\<ra>\<two>)·maxδ(g) \<ra> (abs(p)\<ra>abs(g`(p))\<ra>\<two>)·maxδ(f)"
using Arthan_Lem_7 Int_ZF_1_2_L10A Int_ZF_1_2_L12 by simp;
moreover have
"(abs(p)\<ra>abs(f`(p))\<ra>\<two>)·maxδ(g) \<ra> (abs(p)\<ra>abs(g`(p))\<ra>\<two>)·maxδ(f) \<lsq>
((maxδ(g)·(A\<ra>\<one>) \<ra> maxδ(f)·(C\<ra>\<one>)))·abs(p) \<ra>
((B·maxδ(g) \<ra> \<two>·maxδ(g)) \<ra> (D·maxδ(f) \<ra> \<two>·maxδ(f)))"
proof -
from D2 A2 T1 have
"abs(p)\<ra>abs(f`(p))\<ra>\<two> \<lsq> abs(p)\<ra>(A·abs(p)\<ra>B)\<ra>\<two>"
"abs(p)\<ra>abs(g`(p))\<ra>\<two> \<lsq> abs(p)\<ra>(C·abs(p)\<ra>D)\<ra>\<two>"
using Int_ZF_2_L15C by auto;
with A1 have
"(abs(p)\<ra>abs(f`(p))\<ra>\<two>)·maxδ(g) \<lsq> (abs(p)\<ra>(A·abs(p)\<ra>B)\<ra>\<two>)·maxδ(g)"
"(abs(p)\<ra>abs(g`(p))\<ra>\<two>)·maxδ(f) \<lsq> (abs(p)\<ra>(C·abs(p)\<ra>D)\<ra>\<two>)·maxδ(f)"
using Int_ZF_2_1_L8 Int_ZF_1_3_L13 by auto;
moreover from A1 D1 T1 have
"(abs(p)\<ra>(A·abs(p)\<ra>B)\<ra>\<two>)·maxδ(g) =
maxδ(g)·(A\<ra>\<one>)·abs(p) \<ra> (B·maxδ(g) \<ra> \<two>·maxδ(g))"
"(abs(p)\<ra>(C·abs(p)\<ra>D)\<ra>\<two>)·maxδ(f) =
maxδ(f)·(C\<ra>\<one>)·abs(p) \<ra> (D·maxδ(f) \<ra> \<two>·maxδ(f))"
using Int_ZF_2_1_L8 Int_ZF_1_2_L13 by auto;
ultimately have
"(abs(p)\<ra>abs(f`(p))\<ra>\<two>)·maxδ(g) \<ra> (abs(p)\<ra>abs(g`(p))\<ra>\<two>)·maxδ(f) \<lsq>
(maxδ(g)·(A\<ra>\<one>)·abs(p) \<ra> (B·maxδ(g) \<ra> \<two>·maxδ(g))) \<ra>
(maxδ(f)·(C\<ra>\<one>)·abs(p) \<ra> (D·maxδ(f) \<ra> \<two>·maxδ(f)))"
using int_ineq_add_sides by simp;
moreover from A1 A2 D1 have "abs(p) ∈ \<int>"
"maxδ(g)·(A\<ra>\<one>) ∈ \<int>" "B·maxδ(g) \<ra> \<two>·maxδ(g) ∈ \<int>"
"maxδ(f)·(C\<ra>\<one>) ∈ \<int>" "D·maxδ(f) \<ra> \<two>·maxδ(f) ∈ \<int>"
using Int_ZF_2_L14 Int_ZF_2_1_L8 int_zero_one_are_int
Int_ZF_1_1_L5 int_two_three_are_int by auto;
ultimately show ?thesis using Int_ZF_1_2_L14 by simp;
qed
ultimately have
"abs((f`(g`(p))\<rs>g`(f`(p)))·p) \<lsq> ?E·abs(p) \<ra> ?F"
by (rule Int_order_transitive);
with A2 T1 have
"abs(f`(g`(p))\<rs>g`(f`(p)))·abs(p) \<lsq> ?E·abs(p) \<ra> ?F"
"abs(f`(g`(p))\<rs>g`(f`(p))) ∈ \<int>"
using Int_ZF_1_3_L5 by auto
} then have
"∀p∈\<int>. abs(f`(g`(p))\<rs>g`(f`(p))) ∈ \<int>"
"∀p∈\<int>. abs(f`(g`(p))\<rs>g`(f`(p)))·abs(p) \<lsq> ?E·abs(p) \<ra> ?F"
by auto;
moreover from A1 D1 have "?E ∈ \<int>" "?F ∈ \<int>"
using int_zero_one_are_int int_two_three_are_int Int_ZF_2_1_L8 Int_ZF_1_1_L5
by auto;
ultimately have
"∃L. ∀p∈\<int>. abs(f`(g`(p))\<rs>g`(f`(p))) \<lsq> L"
by (rule Int_ZF_1_7_L1);
with A1 obtain L where "∀p∈\<int>. abs((fog)`(p)\<rs>(gof)`(p)) \<lsq> L"
using Int_ZF_2_1_L10 by auto;
moreover from A1 have "fog ∈ \<S>" "gof ∈ \<S>"
using Int_ZF_2_1_L11 by auto;
ultimately show "fog ∼ gof" using Int_ZF_2_1_L9 by auto;
qed;
section{*Positive slopes*}
text{*This section provides background material for defining the order relation on real numbers.*}
text{*Positive slopes are functions (of course.)*}
lemma (in int1) Int_ZF_2_3_L1: assumes A1: "f∈\<S>+" shows "f:\<int>->\<int>"
using prems AlmostHoms_def PositiveSet_def by simp;
text{*A small technical lemma to simplify the proof of the next theorem.*}
lemma (in int1) Int_ZF_2_3_L1A:
assumes A1: "f∈\<S>+" and A2: "∃n ∈ f``(\<int>+) ∩ \<int>+. a\<lsq>n"
shows "∃M∈\<int>+. a \<lsq> f`(M)"
proof -
from A1 have "f:\<int>->\<int>" "\<int>+ ⊆ \<int>"
using AlmostHoms_def PositiveSet_def by auto
with A2 show ?thesis using func_imagedef by auto;
qed;
text{*The next lemma is Lemma 3 in the Arthan's paper.*}
lemma (in int1) Arthan_Lem_3:
assumes A1: "f∈\<S>+" and A2: "D ∈ \<int>+"
shows "∃M∈\<int>+. ∀m∈\<int>+. (m\<ra>\<one>)·D \<lsq> f`(m·M)"
proof -
let ?E = "maxδ(f) \<ra> D"
let ?A = "f``(\<int>+) ∩ \<int>+"
from A1 A2 have I: "D\<lsq>?E"
using Int_ZF_1_5_L3 Int_ZF_2_1_L8 Int_ZF_2_L1A Int_ZF_2_L15D
by simp;
from A1 A2 have "?A ⊆ \<int>+" "?A ∉ Fin(\<int>)" "\<two>·?E ∈ \<int>"
using int_two_three_are_int Int_ZF_2_1_L8 PositiveSet_def Int_ZF_1_1_L5
by auto;
with A1 have "∃M∈\<int>+. \<two>·?E \<lsq> f`(M)"
using Int_ZF_1_5_L2A Int_ZF_2_3_L1A by simp;
then obtain M where II: "M∈\<int>+" and III: "\<two>·?E \<lsq> f`(M)"
by auto;
{ fix m assume "m∈\<int>+" then have A4: "\<one>\<lsq>m"
using Int_ZF_1_5_L3 by simp
moreover from II III have "(\<one>\<ra>\<one>) ·?E \<lsq> f`(\<one>·M)"
using PositiveSet_def Int_ZF_1_1_L4 by simp;
moreover have "∀k.
\<one>\<lsq>k ∧ (k\<ra>\<one>)·?E \<lsq> f`(k·M) --> (k\<ra>\<one>\<ra>\<one>)·?E \<lsq> f`((k\<ra>\<one>)·M)"
proof -
{ fix k assume A5: "\<one>\<lsq>k" and A6: "(k\<ra>\<one>)·?E \<lsq> f`(k·M)"
with A1 A2 II have T:
"k∈\<int>" "M∈\<int>" "k\<ra>\<one> ∈ \<int>" "?E∈\<int>" "(k\<ra>\<one>)·?E ∈ \<int>" "\<two>·?E ∈ \<int>"
using Int_ZF_2_L1A PositiveSet_def int_zero_one_are_int
Int_ZF_1_1_L5 Int_ZF_2_1_L8 by auto;
from A1 A2 A5 II have
"δ(f,k·M,M) ∈ \<int>" "abs(δ(f,k·M,M)) \<lsq> maxδ(f)" "\<zero>\<lsq>D"
using Int_ZF_2_L1A PositiveSet_def Int_ZF_1_1_L5
Int_ZF_2_1_L7 Int_ZF_2_L16C by auto;
with III A6 have
"(k\<ra>\<one>)·?E \<ra> (\<two>·?E \<rs> ?E) \<lsq> f`(k·M) \<ra> (f`(M) \<ra> δ(f,k·M,M))"
using Int_ZF_1_3_L19A int_ineq_add_sides by simp;
with A1 T have "(k\<ra>\<one>\<ra>\<one>)·?E \<lsq> f`((k\<ra>\<one>)·M)"
using Int_ZF_1_1_L1 int_zero_one_are_int Int_ZF_1_1_L4
Int_ZF_1_2_L11 Int_ZF_2_1_L13 by simp;
} then show ?thesis by simp;
qed;
ultimately have "(m\<ra>\<one>)·?E \<lsq> f`(m·M)" by (rule Induction_on_int);
with A4 I have "(m\<ra>\<one>)·D \<lsq> f`(m·M)" using Int_ZF_1_3_L13A
by simp;
} then have "∀m∈\<int>+.(m\<ra>\<one>)·D \<lsq> f`(m·M)" by simp;
with II show ?thesis by auto;
qed;
text{*A special case of @{text " Arthan_Lem_3"} when $D=1$.*}
corollary (in int1) Arthan_L_3_spec: assumes A1: "f ∈ \<S>+"
shows "∃M∈\<int>+.∀n∈\<int>+. n\<ra>\<one> \<lsq> f`(n·M)"
proof -
have "∀n∈\<int>+. n\<ra>\<one> ∈ \<int>"
using PositiveSet_def int_zero_one_are_int Int_ZF_1_1_L5
by simp;
then have "∀n∈\<int>+. (n\<ra>\<one>)·\<one> = n\<ra>\<one>"
using Int_ZF_1_1_L4 by simp;
moreover from A1 have "∃M∈\<int>+. ∀n∈\<int>+. (n\<ra>\<one>)·\<one> \<lsq> f`(n·M)"
using int_one_two_are_pos Arthan_Lem_3 by simp;
ultimately show ?thesis by simp;
qed;
text{*We know from @{text "Group_ZF_3.thy"} that finite range functions are almost homomorphisms.
Besides reminding that fact for slopes the next lemma shows
that finite range functions do not belong to @{text "\<S>+"}.
This is important, because the projection
of the set of finite range functions defines zero in the real number construction in @{text "Real_ZF_x.thy"}
series, while the projection of @{text "\<S>+"} becomes the set of (strictly) positive reals.
We don't want zero to be positive, do we? The next lemma is a part of Lemma 5 in the Arthan's paper
\cite{Arthan2004}.*}
lemma (in int1) Int_ZF_2_3_L1B:
assumes A1: "f ∈ FinRangeFunctions(\<int>,\<int>)"
shows "f∈\<S>" "f ∉ \<S>+"
proof -
from A1 show "f∈\<S>" using Int_ZF_2_1_L1 group1.Group_ZF_3_3_L1
by auto;
have "\<int>+ ⊆ \<int>" using PositiveSet_def by auto;
with A1 have "f``(\<int>+) ∈ Fin(\<int>)"
using Finite1_L21 by simp;
then have "f``(\<int>+) ∩ \<int>+ ∈ Fin(\<int>)"
using Fin_subset_lemma by blast;
thus "f ∉ \<S>+" by auto;
qed;
text{*We want to show that if $f$ is a slope and neither $f$ nor $-f$ are in @{text "\<S>+"},
then $f$ is bounded. The next lemma is the first step towards that goal and
shows that if slope is not in @{text "\<S>+"} then $f($@{text "\<int>+"}$)$ is bounded above.*}
lemma (in int1) Int_ZF_2_3_L2: assumes A1: "f∈\<S>" and A2: "f ∉ \<S>+"
shows "IsBoundedAbove(f``(\<int>+), IntegerOrder)"
proof -
from A1 have "f:\<int>->\<int>" using AlmostHoms_def by simp
then have "f``(\<int>+) ⊆ \<int>" using func1_1_L6 by simp;
moreover from A1 A2 have "f``(\<int>+) ∩ \<int>+ ∈ Fin(\<int>)" by auto;
ultimately show ?thesis using Int_ZF_2_T1 group3.OrderedGroup_ZF_2_L4
by simp;
qed;
text{*If $f$ is a slope and $-f\notin$ @{text "\<S>+"}, then
$f($@{text "\<int>+"}$)$ is bounded below.*}
lemma (in int1) Int_ZF_2_3_L3: assumes A1: "f∈\<S>" and A2: "\<fm>f ∉ \<S>+"
shows "IsBoundedBelow(f``(\<int>+), IntegerOrder)"
proof -
from A1 have T: "f:\<int>->\<int>" using AlmostHoms_def by simp
then have "(\<sm>(f``(\<int>+))) = (\<fm>f)``(\<int>+)"
using Int_ZF_1_T2 group0_2_T2 PositiveSet_def func1_1_L15C
by auto;
with A1 A2 T show "IsBoundedBelow(f``(\<int>+), IntegerOrder)"
using Int_ZF_2_1_L12 Int_ZF_2_3_L2 PositiveSet_def func1_1_L6
Int_ZF_2_T1 group3.OrderedGroup_ZF_2_L5 by simp;
qed;
text{* A slope that is bounded on @{text "\<int>+"} is bounded everywhere.*}
lemma (in int1) Int_ZF_2_3_L4:
assumes A1: "f∈\<S>" and A2: "m∈\<int>"
and A3: "∀n∈\<int>+. abs(f`(n)) \<lsq> L"
shows "abs(f`(m)) \<lsq> \<two>·maxδ(f) \<ra> L"
proof -
from A1 A3 have
"\<zero> \<lsq> abs(f`(\<one>))" "abs(f`(\<one>)) \<lsq> L"
using int_zero_one_are_int Int_ZF_2_1_L2B int_abs_nonneg int_one_two_are_pos
by auto;
then have II: "\<zero>\<lsq>L" by (rule Int_order_transitive);
from A2 have "m∈\<int>" .
moreover have "abs(f`(\<zero>)) \<lsq> \<two>·maxδ(f) \<ra> L"
proof -
from A1 have
"abs(f`(\<zero>)) \<lsq> maxδ(f)" "\<zero> \<lsq> maxδ(f)"
and T: "maxδ(f) ∈ \<int>"
using Int_ZF_2_1_L8 by auto;
with II have "abs(f`(\<zero>)) \<lsq> maxδ(f) \<ra> maxδ(f) \<ra> L"
using Int_ZF_2_L15F by simp;
with T show ?thesis using Int_ZF_1_1_L4 by simp;
qed;
moreover from A1 A3 II have
"∀n∈\<int>+. abs(f`(n)) \<lsq> \<two>·maxδ(f) \<ra> L"
using Int_ZF_2_1_L8 Int_ZF_1_3_L5A Int_ZF_2_L15F
by simp;
moreover have "∀n∈\<int>+. abs(f`(\<rm>n)) \<lsq> \<two>·maxδ(f) \<ra> L"
proof;
fix n assume "n∈\<int>+"
with A1 A3 have
"\<two>·maxδ(f) ∈ \<int>"
"abs(f`(\<rm>n)) \<lsq> \<two>·maxδ(f) \<ra> abs(f`(n))"
"abs(f`(n)) \<lsq> L"
using int_two_three_are_int Int_ZF_2_1_L8 Int_ZF_1_1_L5
PositiveSet_def Int_ZF_2_1_L14 by auto;
then show "abs(f`(\<rm>n)) \<lsq> \<two>·maxδ(f) \<ra> L"
using Int_ZF_2_L15A by blast;
qed;
ultimately show ?thesis by (rule Int_ZF_2_L19B);
qed;
text{*A slope whose image of the set of positive integers is bounded
is a finite range function.*}
lemma (in int1) Int_ZF_2_3_L4A:
assumes A1: "f∈\<S>" and A2: "IsBounded(f``(\<int>+), IntegerOrder)"
shows "f ∈ FinRangeFunctions(\<int>,\<int>)"
proof -
have T1: "\<int>+ ⊆ \<int>" using PositiveSet_def by auto;
from A1 have T2: "f:\<int>->\<int>" using AlmostHoms_def by simp
from A2 obtain L where "∀a∈f``(\<int>+). abs(a) \<lsq> L"
using Int_ZF_1_3_L20A by auto;
with T2 T1 have "∀n∈\<int>+. abs(f`(n)) \<lsq> L"
by (rule func1_1_L15B);
with A1 have "∀m∈\<int>. abs(f`(m)) \<lsq> \<two>·maxδ(f) \<ra> L"
using Int_ZF_2_3_L4 by simp;
with T2 have "f``(\<int>) ∈ Fin(\<int>)"
by (rule Int_ZF_1_3_L20C);
with T2 show "f ∈ FinRangeFunctions(\<int>,\<int>)"
using FinRangeFunctions_def by simp
qed;
text{*A slope whose image of the set of positive integers is bounded
below is a finite range function or a positive slope.*}
lemma (in int1) Int_ZF_2_3_L4B:
assumes "f∈\<S>" and "IsBoundedBelow(f``(\<int>+), IntegerOrder)"
shows "f ∈ FinRangeFunctions(\<int>,\<int>) ∨ f∈\<S>+"
using prems Int_ZF_2_3_L2 IsBounded_def Int_ZF_2_3_L4A
by auto;
text{*If one slope is not greater then another on positive integers,
then they are almost equal or the difference is a positive slope.*}
lemma (in int1) Int_ZF_2_3_L4C: assumes A1: "f∈\<S>" "g∈\<S>" and
A2: "∀n∈\<int>+. f`(n) \<lsq> g`(n)"
shows "f∼g ∨ g \<fp> (\<fm>f) ∈ \<S>+"
proof -
let ?h = "g \<fp> (\<fm>f)"
from A1 have "(\<fm>f) ∈ \<S>" using Int_ZF_2_1_L12
by simp;
with A1 have I: "?h ∈ \<S>" using Int_ZF_2_1_L12C
by simp;
moreover have "IsBoundedBelow(?h``(\<int>+), IntegerOrder)"
proof -
from I have
"?h:\<int>->\<int>" and "\<int>+⊆\<int>" using AlmostHoms_def PositiveSet_def
by auto
moreover from A1 A2 have "∀n∈\<int>+. ⟨\<zero>, ?h`(n)⟩ ∈ IntegerOrder"
using Int_ZF_2_1_L2B PositiveSet_def Int_ZF_1_3_L10A
Int_ZF_2_1_L12 Int_ZF_2_1_L12B Int_ZF_2_1_L12A
by simp;
ultimately show "IsBoundedBelow(?h``(\<int>+), IntegerOrder)"
by (rule func_ZF_8_L1);
qed
ultimately have "?h ∈ FinRangeFunctions(\<int>,\<int>) ∨ ?h∈\<S>+"
using Int_ZF_2_3_L4B by simp
with A1 show "f∼g ∨ g \<fp> (\<fm>f) ∈ \<S>+"
using Int_ZF_2_1_L9C by auto;
qed;
text{*Positive slopes are arbitrarily large for large enough arguments.*}
lemma (in int1) Int_ZF_2_3_L5:
assumes A1: "f∈\<S>+" and A2: "K∈\<int>"
shows "∃N∈\<int>+. ∀m. N\<lsq>m --> K \<lsq> f`(m)"
proof -
from A1 obtain M where I: "M∈\<int>+" and II: "∀n∈\<int>+. n\<ra>\<one> \<lsq> f`(n·M)"
using Arthan_L_3_spec by auto;
let ?j = "GreaterOf(IntegerOrder,M,K \<rs> (minf(f,\<zero>..(M\<rs>\<one>)) \<rs> maxδ(f)) \<rs> \<one>)"
from A1 I have T1:
"minf(f,\<zero>..(M\<rs>\<one>)) \<rs> maxδ(f) ∈ \<int>" "M∈\<int>"
using Int_ZF_2_1_L15 Int_ZF_2_1_L8 Int_ZF_1_1_L5 PositiveSet_def
by auto;
with A2 I have T2:
"K \<rs> (minf(f,\<zero>..(M\<rs>\<one>)) \<rs> maxδ(f)) ∈ \<int>"
"K \<rs> (minf(f,\<zero>..(M\<rs>\<one>)) \<rs> maxδ(f)) \<rs> \<one> ∈ \<int>"
using Int_ZF_1_1_L5 int_zero_one_are_int by auto;
with T1 have III: "M \<lsq> ?j" and
"K \<rs> (minf(f,\<zero>..(M\<rs>\<one>)) \<rs> maxδ(f)) \<rs> \<one> \<lsq> ?j"
using Int_ZF_1_3_L18 by auto;
with A2 T1 T2 have
IV: "K \<lsq> ?j\<ra>\<one> \<ra> (minf(f,\<zero>..(M\<rs>\<one>)) \<rs> maxδ(f))"
using int_zero_one_are_int Int_ZF_2_L9C by simp;
let ?N = "GreaterOf(IntegerOrder,\<one>,?j·M)"
from T1 III have T3: "?j ∈ \<int>" "?j·M ∈ \<int>"
using Int_ZF_2_L1A Int_ZF_1_1_L5 by auto;
then have V: "?N ∈ \<int>+" and VI: "?j·M \<lsq> ?N"
using int_zero_one_are_int Int_ZF_1_5_L3 Int_ZF_1_3_L18
by auto;
{ fix m
let ?n = "m zdiv M"
let ?k = "m zmod M"
assume "?N\<lsq>m"
with VI have "?j·M \<lsq> m" by (rule Int_order_transitive);
with I III have
VII: "m = ?n·M\<ra>?k"
"?j \<lsq> ?n" and
VIII: "?n ∈ \<int>+" "?k ∈ \<zero>..(M\<rs>\<one>)"
using IntDiv_ZF_1_L5 by auto;
with II have
"?j \<ra> \<one> \<lsq> ?n \<ra> \<one>" "?n\<ra>\<one> \<lsq> f`(?n·M)"
using int_zero_one_are_int int_ord_transl_inv by auto;
then have "?j \<ra> \<one> \<lsq> f`(?n·M)"
by (rule Int_order_transitive);
with T1 have
"?j\<ra>\<one> \<ra> (minf(f,\<zero>..(M\<rs>\<one>)) \<rs> maxδ(f)) \<lsq>
f`(?n·M) \<ra> (minf(f,\<zero>..(M\<rs>\<one>)) \<rs> maxδ(f))"
using int_ord_transl_inv by simp;
with IV have "K \<lsq> f`(?n·M) \<ra> (minf(f,\<zero>..(M\<rs>\<one>)) \<rs> maxδ(f))"
by (rule Int_order_transitive);
moreover from A1 I VIII have
"f`(?n·M) \<ra> (minf(f,\<zero>..(M\<rs>\<one>))\<rs> maxδ(f)) \<lsq> f`(?n·M\<ra>?k)"
using PositiveSet_def Int_ZF_2_1_L16 by simp;
ultimately have "K \<lsq> f`(?n·M\<ra>?k)"
by (rule Int_order_transitive);
with VII have "K \<lsq> f`(m)" by simp;
} then have "∀m. ?N\<lsq>m --> K \<lsq> f`(m)"
by simp;
with V show ?thesis by auto;
qed;
text{*Positive slopes are arbitrarily small for small enough arguments.
Kind of dual to @{text "Int_ZF_2_3_L5"}.*}
lemma (in int1) Int_ZF_2_3_L5A: assumes A1: "f∈\<S>+" and A2: "K∈\<int>"
shows "∃N∈\<int>+. ∀m. N\<lsq>m --> f`(\<rm>m) \<lsq> K"
proof -
from A1 have T1: "abs(f`(\<zero>)) \<ra> maxδ(f) ∈ \<int>"
using Int_ZF_2_1_L8 by auto;
with A2 have "abs(f`(\<zero>)) \<ra> maxδ(f) \<rs> K ∈ \<int>"
using Int_ZF_1_1_L5 by simp;
with A1 have
"∃N∈\<int>+. ∀m. N\<lsq>m --> abs(f`(\<zero>)) \<ra> maxδ(f) \<rs> K \<lsq> f`(m)"
using Int_ZF_2_3_L5 by simp;
then obtain N where I: "N∈\<int>+" and II:
"∀m. N\<lsq>m --> abs(f`(\<zero>)) \<ra> maxδ(f) \<rs> K \<lsq> f`(m)"
by auto;
{ fix m assume A3: "N\<lsq>m"
with A1 have
"f`(\<rm>m) \<lsq> abs(f`(\<zero>)) \<ra> maxδ(f) \<rs> f`(m)"
using Int_ZF_2_L1A Int_ZF_2_1_L14 by simp;
moreover
from II T1 A3 have "abs(f`(\<zero>)) \<ra> maxδ(f) \<rs> f`(m) \<lsq>
(abs(f`(\<zero>)) \<ra> maxδ(f)) \<rs>(abs(f`(\<zero>)) \<ra> maxδ(f) \<rs> K)"
using Int_ZF_2_L10 int_ord_transl_inv by simp;
with A2 T1 have "abs(f`(\<zero>)) \<ra> maxδ(f) \<rs> f`(m) \<lsq> K"
using Int_ZF_1_2_L3 by simp;
ultimately have "f`(\<rm>m) \<lsq> K"
by (rule Int_order_transitive)
} then have "∀m. N\<lsq>m --> f`(\<rm>m) \<lsq> K"
by simp;
with I show ?thesis by auto;
qed;
(*lemma (in int1) Int_ZF_2_3_L5A: assumes A1: "f∈\<S>+" and A2: "K∈\<int>"
shows "∃N∈\<int>+. ∀m. m\<lsq>(\<rm>N) --> f`(m) \<lsq> K"
proof -
from A1 have T1: "abs(f`(\<zero>)) \<ra> maxδ(f) ∈ \<int>"
using Int_ZF_2_1_L8 by auto;
with A2 have "abs(f`(\<zero>)) \<ra> maxδ(f) \<rs> K ∈ \<int>"
using Int_ZF_1_1_L5 by simp;
with A1 have
"∃N∈\<int>+. ∀m. N\<lsq>m --> abs(f`(\<zero>)) \<ra> maxδ(f) \<rs> K \<lsq> f`(m)"
using Int_ZF_2_3_L5 by simp;
then obtain N where I: "N∈\<int>+" and II:
"∀m. N\<lsq>m --> abs(f`(\<zero>)) \<ra> maxδ(f) \<rs> K \<lsq> f`(m)"
by auto;
{ fix m assume A3: "m\<lsq>(\<rm>N)"
with A1 have T2: "f`(m) ∈ \<int>"
using Int_ZF_2_L1A Int_ZF_2_1_L2B by simp;
from A1 I II A3 have
"abs(f`(\<zero>)) \<ra> maxδ(f) \<rs> K \<lsq> f`(\<rm>m)" and
"f`(\<rm>m) \<lsq> abs(f`(\<zero>)) \<ra> maxδ(f) \<rs> f`(m)"
using PositiveSet_def Int_ZF_2_L10AA Int_ZF_2_L1A Int_ZF_2_1_L14
by auto;
then have
"abs(f`(\<zero>)) \<ra> maxδ(f) \<rs> K \<lsq> abs(f`(\<zero>)) \<ra> maxδ(f) \<rs> f`(m)"
by (rule Int_order_transitive)
with T1 A2 T2 have "f`(m) \<lsq> K"
using Int_ZF_2_L10AB by simp;
} then have "∀m. m\<lsq>(\<rm>N) --> f`(m) \<lsq> K"
by simp;
with I show ?thesis by auto;
qed;*)
text{*A special case of @{text "Int_ZF_2_3_L5"} where $K=1$.*}
corollary (in int1) Int_ZF_2_3_L6: assumes "f∈\<S>+"
shows "∃N∈\<int>+. ∀m. N\<lsq>m --> f`(m) ∈ \<int>+"
using prems int_zero_one_are_int Int_ZF_2_3_L5 Int_ZF_1_5_L3
by simp;
text{*A special case of @{text "Int_ZF_2_3_L5"} where $m=N$.*}
corollary (in int1) Int_ZF_2_3_L6A: assumes "f∈\<S>+" and "K∈\<int>"
shows "∃N∈\<int>+. K \<lsq> f`(N)"
proof -
from prems have "∃N∈\<int>+. ∀m. N\<lsq>m --> K \<lsq> f`(m)"
using Int_ZF_2_3_L5 by simp;
then obtain N where I: "N ∈ \<int>+" and II: "∀m. N\<lsq>m --> K \<lsq> f`(m)"
by auto;
then show ?thesis using PositiveSet_def int_ord_is_refl refl_def
by auto;
qed;
text{*If values of a slope are not bounded above,
then the slope is positive.*}
lemma (in int1) Int_ZF_2_3_L7: assumes A1: "f∈\<S>"
and A2: "∀K∈\<int>. ∃n∈\<int>+. K \<lsq> f`(n)"
shows "f ∈ \<S>+"
proof -
{ fix K assume "K∈\<int>"
with A2 obtain n where "n∈\<int>+" "K \<lsq> f`(n)"
by auto
moreover from A1 have "\<int>+ ⊆ \<int>" "f:\<int>->\<int>"
using PositiveSet_def AlmostHoms_def by auto
ultimately have "∃m ∈ f``(\<int>+). K \<lsq> m"
using func1_1_L15D by auto;
} then have "∀K∈\<int>. ∃m ∈ f``(\<int>+). K \<lsq> m" by simp;
with A1 show "f ∈ \<S>+" using Int_ZF_4_L9 Int_ZF_2_3_L2
by auto;
qed;
text{*For unbounded slope $f$ either $f\in$@{text "\<S>+"} of
$-f\in$@{text "\<S>+"}.*}
theorem (in int1) Int_ZF_2_3_L8:
assumes A1: "f∈\<S>" and A2: "f ∉ FinRangeFunctions(\<int>,\<int>)"
shows "(f ∈ \<S>+) Xor ((\<fm>f) ∈ \<S>+)"
proof -
have T1: "\<int>+ ⊆ \<int>" using PositiveSet_def by auto;
from A1 have T2: "f:\<int>->\<int>" using AlmostHoms_def by simp
then have I: "f``(\<int>+) ⊆ \<int>" using func1_1_L6 by auto;
from A1 A2 have "f ∈ \<S>+ ∨ (\<fm>f) ∈ \<S>+"
using Int_ZF_2_3_L2 Int_ZF_2_3_L3 IsBounded_def Int_ZF_2_3_L4A
by auto;
moreover have "¬(f ∈ \<S>+ ∧ (\<fm>f) ∈ \<S>+)"
proof -
{ assume A3: "f ∈ \<S>+" and A4: "(\<fm>f) ∈ \<S>+"
from A3 obtain N1 where
I: "N1∈\<int>+" and II: "∀m. N1\<lsq>m --> f`(m) ∈ \<int>+"
using Int_ZF_2_3_L6 by auto;
from A4 obtain N2 where
III: "N2∈\<int>+" and IV: "∀m. N2\<lsq>m --> (\<fm>f)`(m) ∈ \<int>+"
using Int_ZF_2_3_L6 by auto;
let ?N = "GreaterOf(IntegerOrder,N1,N2)"
from I III have "N1 \<lsq> ?N" "N2 \<lsq> ?N"
using PositiveSet_def Int_ZF_1_3_L18 by auto;
with A1 II IV have
"f`(?N) ∈ \<int>+" "(\<fm>f)`(?N) ∈ \<int>+" "(\<fm>f)`(?N) = \<rm>(f`(?N))"
using Int_ZF_2_L1A PositiveSet_def Int_ZF_2_1_L12A
by auto;
then have False using Int_ZF_1_5_L8 by simp;
} thus ?thesis by auto
qed;
ultimately show "(f ∈ \<S>+) Xor ((\<fm>f) ∈ \<S>+)"
using Xor_def by simp
qed;
text{*The sum of positive slopes is a positive slope.*}
theorem (in int1) sum_of_pos_sls_is_pos_sl:
assumes A1: "f ∈ \<S>+" "g ∈ \<S>+"
shows "f\<fp>g ∈ \<S>+"
proof -
{ fix K assume "K∈\<int>"
with A1 have "∃N∈\<int>+. ∀m. N\<lsq>m --> K \<lsq> f`(m)"
using Int_ZF_2_3_L5 by simp;
then obtain N where I: "N∈\<int>+" and II: "∀m. N\<lsq>m --> K \<lsq> f`(m)"
by auto;
from A1 have "∃M∈\<int>+. ∀m. M\<lsq>m --> \<zero> \<lsq> g`(m)"
using int_zero_one_are_int Int_ZF_2_3_L5 by simp;
then obtain M where III: "M∈\<int>+" and IV: "∀m. M\<lsq>m --> \<zero> \<lsq> g`(m)"
by auto;
let ?L = "GreaterOf(IntegerOrder,N,M)"
from I III have V: "?L ∈ \<int>+" "\<int>+ ⊆ \<int>"
using GreaterOf_def PositiveSet_def by auto
moreover from A1 V have "(f\<fp>g)`(?L) = f`(?L) \<ra> g`(?L)"
using Int_ZF_2_1_L12B by auto;
moreover from I II III IV have "K \<lsq> f`(?L) \<ra> g`(?L)"
using PositiveSet_def Int_ZF_1_3_L18 Int_ZF_2_L15F
by simp;
ultimately have "?L ∈ \<int>+" "K \<lsq> (f\<fp>g)`(?L)"
by auto;
then have "∃n ∈\<int>+. K \<lsq> (f\<fp>g)`(n)"
by auto;
} with A1 show "f\<fp>g ∈ \<S>+"
using Int_ZF_2_1_L12C Int_ZF_2_3_L7 by simp;
qed
text{*The composition of positive slopes is a positive slope.*}
theorem (in int1) comp_of_pos_sls_is_pos_sl:
assumes A1: "f ∈ \<S>+" "g ∈ \<S>+"
shows "fog ∈ \<S>+"
proof -
{ fix K assume "K∈\<int>"
with A1 have "∃N∈\<int>+. ∀m. N\<lsq>m --> K \<lsq> f`(m)"
using Int_ZF_2_3_L5 by simp;
then obtain N where "N∈\<int>+" and I: "∀m. N\<lsq>m --> K \<lsq> f`(m)"
by auto;
with A1 have "∃M∈\<int>+. N \<lsq> g`(M)"
using PositiveSet_def Int_ZF_2_3_L6A by simp;
then obtain M where "M∈\<int>+" "N \<lsq> g`(M)"
by auto;
with A1 I have "∃M∈\<int>+. K \<lsq> (fog)`(M)"
using PositiveSet_def Int_ZF_2_1_L10
by auto;
} with A1 show "fog ∈ \<S>+"
using Int_ZF_2_1_L11 Int_ZF_2_3_L7
by simp;
qed;
text{*A slope equivalent to a positive one is positive.*}
lemma (in int1) Int_ZF_2_3_L9:
assumes A1: "f ∈ \<S>+" and A2: "⟨f,g⟩ ∈ AlEqRel" shows "g ∈ \<S>+"
proof -
from A2 have T: "g∈\<S>" and "∃L∈\<int>. ∀m∈\<int>. abs(f`(m)\<rs>g`(m)) \<lsq> L"
using Int_ZF_2_1_L9A by auto;
then obtain L where
I: "L∈\<int>" and II: "∀m∈\<int>. abs(f`(m)\<rs>g`(m)) \<lsq> L"
by auto;
{ fix K assume A3: "K∈\<int>"
with I have "K\<ra>L ∈ \<int>"
using Int_ZF_1_1_L5 by simp;
with A1 obtain M where III: "M∈\<int>+" and IV: "K\<ra>L \<lsq> f`(M)"
using Int_ZF_2_3_L6A by auto;
with A1 A3 I have "K \<lsq> f`(M)\<rs>L"
using PositiveSet_def Int_ZF_2_1_L2B Int_ZF_2_L9B
by simp;
moreover from A1 T II III have
"f`(M)\<rs>L \<lsq> g`(M)"
using PositiveSet_def Int_ZF_2_1_L2B Int_triangle_ineq2
by simp;
ultimately have "K \<lsq> g`(M)"
by (rule Int_order_transitive);
with III have "∃n∈\<int>+. K \<lsq> g`(n)"
by auto;
} with T show "g ∈ \<S>+"
using Int_ZF_2_3_L7 by simp;
qed;
text{* The set of positive slopes is saturated with respect to the relation of
equivalence of slopes.*}
lemma (in int1) pos_slopes_saturated: shows "IsSaturated(AlEqRel,\<S>+)"
proof -
have
"equiv(\<S>,AlEqRel)"
"AlEqRel ⊆ \<S> × \<S>"
using Int_ZF_2_1_L9B by auto
moreover have "\<S>+ ⊆ \<S>" by auto
moreover have "∀f∈\<S>+. ∀g∈\<S>. ⟨f,g⟩ ∈ AlEqRel --> g ∈ \<S>+"
using Int_ZF_2_3_L9 by blast;
ultimately show "IsSaturated(AlEqRel,\<S>+)"
by (rule EquivClass_3_L3);
qed;
text{*A technical lemma involving a projection of the set of positive slopes
and a logical epression with exclusive or.*}
lemma (in int1) Int_ZF_2_3_L10:
assumes A1: "f∈\<S>" "g∈\<S>"
and A2: "R = {AlEqRel``{s}. s∈\<S>+}"
and A3: "(f∈\<S>+) Xor (g∈\<S>+)"
shows "(AlEqRel``{f} ∈ R) Xor (AlEqRel``{g} ∈ R)"
proof -
from A1 A2 A3 have
"equiv(\<S>,AlEqRel)"
"IsSaturated(AlEqRel,\<S>+)"
"\<S>+ ⊆ \<S>"
"f∈\<S>" "g∈\<S>"
"R = {AlEqRel``{s}. s∈\<S>+}"
"(f∈\<S>+) Xor (g∈\<S>+)"
using pos_slopes_saturated Int_ZF_2_1_L9B by auto;
then show ?thesis by (rule EquivClass_3_L7);
qed;
text{*Identity function is a positive slope.*}
lemma (in int1) Int_ZF_2_3_L11: shows "id(\<int>) ∈ \<S>+"
proof -
let ?f = "id(\<int>)"
{ fix K assume "K∈\<int>"
then obtain n where T: "n∈\<int>+" and "K\<lsq>n"
using Int_ZF_1_5_L9 by auto;
moreover from T have "?f`(n) = n"
using PositiveSet_def by simp;
ultimately have "n∈\<int>+" and "K\<lsq>?f`(n)"
by auto;
then have "∃n∈\<int>+. K\<lsq>?f`(n)" by auto;
} then show "?f ∈ \<S>+"
using Int_ZF_2_1_L17 Int_ZF_2_3_L7 by simp;
qed;
text{*The identity function is not almost equal to any bounded function.*}
lemma (in int1) Int_ZF_2_3_L12: assumes A1: "f ∈ FinRangeFunctions(\<int>,\<int>)"
shows "¬(id(\<int>) ∼ f)"
proof -
{ from A1 have "id(\<int>) ∈ \<S>+"
using Int_ZF_2_3_L11 by simp
moreover assume "⟨id(\<int>),f⟩ ∈ AlEqRel"
ultimately have "f ∈ \<S>+"
by (rule Int_ZF_2_3_L9);
with A1 have False using Int_ZF_2_3_L1B
by simp;
} then show "¬(id(\<int>) ∼ f)" by auto;
qed;
section{*Inverting slopes*}
text{*Not every slope is a 1:1 function. However, we can still invert slopes
in the sense that if $f$ is a slope, then we can find a slope $g$ such that
$f\circ g$ is almost equal to the identity function.
The goal of this this section is to establish this fact for positive slopes.
*}
text{*If $f$ is a positive slope, then for every positive integer $p$
the set $\{n\in Z_+: p\leq f(n)\}$ is a nonempty subset of positive integers.
Recall that $f^{-1}(p)$ is the notation for the smallest element of this set.*}
lemma (in int1) Int_ZF_2_4_L1:
assumes A1: "f ∈ \<S>+" and A2: "p∈\<int>+" and A3: "A = {n∈\<int>+. p \<lsq> f`(n)}"
shows
"A ⊆ \<int>+"
"A ≠ 0"
"f¯(p) ∈ A"
"∀m∈A. f¯(p) \<lsq> m"
proof -
from A3 show I: "A ⊆ \<int>+" by auto
from A1 A2 have "∃n∈\<int>+. p \<lsq> f`(n)"
using PositiveSet_def Int_ZF_2_3_L6A by simp;
with A3 show II: "A ≠ 0" by auto;
from A3 I II show
"f¯(p) ∈ A"
"∀m∈A. f¯(p) \<lsq> m"
using Int_ZF_1_5_L1C by auto;
qed;
text{*If $f$ is a positive slope and $p$ is a positive integer $p$, then
$f^{-1}(p)$ (defined as the minimum of the set $\{n\in Z_+: p\leq f(n)\}$ )
is a (well defined) positive integer.*}
lemma (in int1) Int_ZF_2_4_L2:
assumes "f ∈ \<S>+" and "p∈\<int>+"
shows
"f¯(p) ∈ \<int>+"
"p \<lsq> f`(f¯(p))"
using prems Int_ZF_2_4_L1 by auto;
text{*If $f$ is a positive slope and $p$ is a positive integer such
that $n\leq f(p)$, then
$f^{-1}(n) \leq p$.*}
lemma (in int1) Int_ZF_2_4_L3:
assumes "f ∈ \<S>+" and "m∈\<int>+" "p∈\<int>+" and "m \<lsq> f`(p)"
shows "f¯(m) \<lsq> p"
using prems Int_ZF_2_4_L1 by simp;
text{*An upper bound $f(f^{-1}(m) -1)$ for positive slopes.*}
lemma (in int1) Int_ZF_2_4_L4:
assumes A1: "f ∈ \<S>+" and A2: "m∈\<int>+" and A3: "f¯(m)\<rs>\<one> ∈ \<int>+"
shows "f`(f¯(m)\<rs>\<one>) \<lsq> m" "f`(f¯(m)\<rs>\<one>) ≠ m"
proof -
from A1 A2 have T: "f¯(m) ∈ \<int>" using Int_ZF_2_4_L2 PositiveSet_def
by simp;
from A1 A3 have "f:\<int>->\<int>" and "f¯(m)\<rs>\<one> ∈ \<int>"
using Int_ZF_2_3_L1 PositiveSet_def by auto;
with A1 A2 have T1: "f`(f¯(m)\<rs>\<one>) ∈ \<int>" "m∈\<int>"
using apply_funtype PositiveSet_def by auto;
{ assume "m \<lsq> f`(f¯(m)\<rs>\<one>)"
with A1 A2 A3 have "f¯(m) \<lsq> f¯(m)\<rs>\<one>"
by (rule Int_ZF_2_4_L3);
with T have False using Int_ZF_1_2_L3AA
by simp;
} then have I: "¬(m \<lsq> f`(f¯(m)\<rs>\<one>))" by auto;
with T1 show "f`(f¯(m)\<rs>\<one>) \<lsq> m"
by (rule Int_ZF_2_L19);
from T1 I show "f`(f¯(m)\<rs>\<one>) ≠ m"
by (rule Int_ZF_2_L19);
qed;
text{*The (candidate for) the inverse of a positive slope is nondecreasing.*}
lemma (in int1) Int_ZF_2_4_L5:
assumes A1: "f ∈ \<S>+" and A2: "m∈\<int>+" and A3: "m\<lsq>n"
shows "f¯(m) \<lsq> f¯(n)"
proof -
from A2 A3 have T: "n ∈ \<int>+" using Int_ZF_1_5_L7 by blast;
with A1 have "n \<lsq> f`(f¯(n))" using Int_ZF_2_4_L2
by simp;
with A3 have "m \<lsq> f`(f¯(n))" by (rule Int_order_transitive)
with A1 A2 T show "f¯(m) \<lsq> f¯(n)"
using Int_ZF_2_4_L2 Int_ZF_2_4_L3 by simp;
qed;
text{*If $f^{-1}(m)$ is positive and $n$ is a positive integer, then,
then $f^{-1}(m+n)-1$ is positive.*}
lemma (in int1) Int_ZF_2_4_L6:
assumes A1: "f ∈ \<S>+" and A2: "m∈\<int>+" "n∈\<int>+" and
A3: "f¯(m)\<rs>\<one> ∈ \<int>+"
shows "f¯(m\<ra>n)\<rs>\<one> ∈ \<int>+"
proof -
from A1 A2 have "f¯(m)\<rs>\<one> \<lsq> f¯(m\<ra>n) \<rs> \<one>"
using PositiveSet_def Int_ZF_1_5_L7A Int_ZF_2_4_L2
Int_ZF_2_4_L5 int_zero_one_are_int Int_ZF_1_1_L4
int_ord_transl_inv by simp;
with A3 show "f¯(m\<ra>n)\<rs>\<one> ∈ \<int>+" using Int_ZF_1_5_L7
by blast;
qed;
text{*If $f$ is a slope, then $f(f^{-1}(m+n)-f^{-1}(m) - f^{-1}(n))$ is
uniformly bounded above and below. Will it be the messiest IsarMathLib
proof ever? Only time will tell.*}
lemma (in int1) Int_ZF_2_4_L7: assumes A1: "f ∈ \<S>+" and
A2: "∀m∈\<int>+. f¯(m)\<rs>\<one> ∈ \<int>+"
shows
"∃U∈\<int>. ∀m∈\<int>+. ∀n∈\<int>+. f`(f¯(m\<ra>n)\<rs>f¯(m)\<rs>f¯(n)) \<lsq> U"
"∃N∈\<int>. ∀m∈\<int>+. ∀n∈\<int>+. N \<lsq> f`(f¯(m\<ra>n)\<rs>f¯(m)\<rs>f¯(n))"
proof -
from A1 have "∃L∈\<int>. ∀r∈\<int>. f`(r) \<lsq> f`(r\<rs>\<one>) \<ra> L"
using Int_ZF_2_1_L28 by simp;
then obtain L where
I: "L∈\<int>" and II: "∀r∈\<int>. f`(r) \<lsq> f`(r\<rs>\<one>) \<ra> L"
by auto;
from A1 have
"∃M∈\<int>. ∀r∈\<int>.∀p∈\<int>.∀q∈\<int>. f`(r\<rs>p\<rs>q) \<lsq> f`(r)\<rs>f`(p)\<rs>f`(q)\<ra>M"
"∃K∈\<int>. ∀r∈\<int>.∀p∈\<int>.∀q∈\<int>. f`(r)\<rs>f`(p)\<rs>f`(q)\<ra>K \<lsq> f`(r\<rs>p\<rs>q)"
using Int_ZF_2_1_L30 by auto
then obtain M K where III: "M∈\<int>" and
IV: "∀r∈\<int>.∀p∈\<int>.∀q∈\<int>. f`(r\<rs>p\<rs>q) \<lsq> f`(r)\<rs>f`(p)\<rs>f`(q)\<ra>M"
and
V: "K∈\<int>" and VI: "∀r∈\<int>.∀p∈\<int>.∀q∈\<int>. f`(r)\<rs>f`(p)\<rs>f`(q)\<ra>K \<lsq> f`(r\<rs>p\<rs>q)"
by auto;
from I III V have
"L\<ra>M ∈ \<int>" "(\<rm>L) \<rs> L \<ra> K ∈ \<int>"
using Int_ZF_1_1_L4 Int_ZF_1_1_L5 by auto;
moreover
{ fix m n
assume A3: "m∈\<int>+" "n∈\<int>+"
have "f`(f¯(m\<ra>n)\<rs>f¯(m)\<rs>f¯(n)) \<lsq> L\<ra>M ∧
(\<rm>L)\<rs>L\<ra>K \<lsq> f`(f¯(m\<ra>n)\<rs>f¯(m)\<rs>f¯(n))"
proof -
let ?r = "f¯(m\<ra>n)"
let ?p = "f¯(m)"
let ?q = "f¯(n)"
from A1 A3 have T1:
"?p ∈ \<int>+" "?q ∈ \<int>+" "?r ∈ \<int>+"
using Int_ZF_2_4_L2 pos_int_closed_add_unfolded by auto;
with A3 have T2:
"m ∈ \<int>" "n ∈ \<int>" "?p ∈ \<int>" "?q ∈ \<int>" "?r ∈ \<int>"
using PositiveSet_def by auto;
from A2 A3 have T3:
"?r\<rs>\<one> ∈ \<int>+" "?p\<rs>\<one> ∈ \<int>+" "?q\<rs>\<one> ∈ \<int>+"
using pos_int_closed_add_unfolded by auto;
from A1 A3 have VII:
"m\<ra>n \<lsq> f`(?r)"
"m \<lsq> f`(?p)"
"n \<lsq> f`(?q)"
using Int_ZF_2_4_L2 pos_int_closed_add_unfolded by auto;
from A1 A3 T3 have VIII:
"f`(?r\<rs>\<one>) \<lsq> m\<ra>n"
"f`(?p\<rs>\<one>) \<lsq> m"
"f`(?q\<rs>\<one>) \<lsq> n"
using pos_int_closed_add_unfolded Int_ZF_2_4_L4 by auto;
have "f`(?r\<rs>?p\<rs>?q) \<lsq> L\<ra>M"
proof -
from IV T2 have "f`(?r\<rs>?p\<rs>?q) \<lsq> f`(?r)\<rs>f`(?p)\<rs>f`(?q)\<ra>M"
by simp;
moreover
from I II T2 VIII have
"f`(?r) \<lsq> f`(?r\<rs>\<one>) \<ra> L"
"f`(?r\<rs>\<one>) \<ra> L \<lsq> m\<ra>n\<ra>L"
using int_ord_transl_inv by auto;
then have "f`(?r) \<lsq> m\<ra>n\<ra>L"
by (rule Int_order_transitive);
with VII have "f`(?r) \<rs> f`(?p) \<lsq> m\<ra>n\<ra>L\<rs>m"
using int_ineq_add_sides by simp;
with I T2 VII have "f`(?r) \<rs> f`(?p) \<rs> f`(?q) \<lsq> n\<ra>L\<rs>n"
using Int_ZF_1_2_L9 int_ineq_add_sides by simp;
with I III T2 have "f`(?r) \<rs> f`(?p) \<rs> f`(?q) \<ra> M \<lsq> L\<ra>M"
using Int_ZF_1_2_L3 int_ord_transl_inv by simp;
ultimately show "f`(?r\<rs>?p\<rs>?q) \<lsq> L\<ra>M"
by (rule Int_order_transitive);
qed
moreover have "(\<rm>L)\<rs>L \<ra>K \<lsq> f`(?r\<rs>?p\<rs>?q)"
proof -
from I II T2 VIII have
"f`(?p) \<lsq> f`(?p\<rs>\<one>) \<ra> L"
"f`(?p\<rs>\<one>) \<ra> L \<lsq> m \<ra>L"
using int_ord_transl_inv by auto;
then have "f`(?p) \<lsq> m \<ra>L"
by (rule Int_order_transitive);
with VII have "m\<ra>n \<rs>(m\<ra>L) \<lsq> f`(?r) \<rs> f`(?p)"
using int_ineq_add_sides by simp;
with I T2 have "n \<rs> L \<lsq> f`(?r) \<rs> f`(?p)"
using Int_ZF_1_2_L9 by simp;
moreover
from I II T2 VIII have
"f`(?q) \<lsq> f`(?q\<rs>\<one>) \<ra> L"
"f`(?q\<rs>\<one>) \<ra> L \<lsq> n \<ra>L"
using int_ord_transl_inv by auto;
then have "f`(?q) \<lsq> n \<ra>L"
by (rule Int_order_transitive);
ultimately have
"n \<rs> L \<rs> (n\<ra>L) \<lsq> f`(?r) \<rs> f`(?p) \<rs> f`(?q)"
using int_ineq_add_sides by simp;
with I V T2 have
"(\<rm>L)\<rs>L \<ra>K \<lsq> f`(?r) \<rs> f`(?p) \<rs> f`(?q) \<ra> K"
using Int_ZF_1_2_L3 int_ord_transl_inv by simp;
moreover from VI T2 have
"f`(?r) \<rs> f`(?p) \<rs> f`(?q) \<ra> K \<lsq> f`(?r\<rs>?p\<rs>?q)"
by simp;
ultimately show "(\<rm>L)\<rs>L \<ra>K \<lsq> f`(?r\<rs>?p\<rs>?q)"
by (rule Int_order_transitive);
qed
ultimately show
"f`(?r\<rs>?p\<rs>?q) \<lsq> L\<ra>M ∧
(\<rm>L)\<rs>L\<ra>K \<lsq> f`(f¯(m\<ra>n)\<rs>f¯(m)\<rs>f¯(n))"
by simp
qed
}
ultimately show
"∃U∈\<int>. ∀m∈\<int>+. ∀n∈\<int>+. f`(f¯(m\<ra>n)\<rs>f¯(m)\<rs>f¯(n)) \<lsq> U"
"∃N∈\<int>. ∀m∈\<int>+. ∀n∈\<int>+. N \<lsq> f`(f¯(m\<ra>n)\<rs>f¯(m)\<rs>f¯(n))"
by auto;
qed;
text{*The expression $f^{-1}(m+n)-f^{-1}(m) - f^{-1}(n)$ is uniformly bounded
for all pairs $\langle m,n \rangle \in$ @{text "\<int>+×\<int>+"}.
Recall that in the @{text "int1"}
context @{text "ε(f,x)"} is defined so that
$\varepsilon(f,\langle m,n \rangle ) = f^{-1}(m+n)-f^{-1}(m) - f^{-1}(n)$.*}
lemma (in int1) Int_ZF_2_4_L8: assumes A1: "f ∈ \<S>+" and
A2: "∀m∈\<int>+. f¯(m)\<rs>\<one> ∈ \<int>+"
shows "∃M. ∀x∈\<int>+×\<int>+. abs(ε(f,x)) \<lsq> M"
proof -
from A1 A2 have
"∃U∈\<int>. ∀m∈\<int>+. ∀n∈\<int>+. f`(f¯(m\<ra>n)\<rs>f¯(m)\<rs>f¯(n)) \<lsq> U"
"∃N∈\<int>. ∀m∈\<int>+. ∀n∈\<int>+. N \<lsq> f`(f¯(m\<ra>n)\<rs>f¯(m)\<rs>f¯(n))"
using Int_ZF_2_4_L7 by auto;
then obtain U N where I:
"∀m∈\<int>+. ∀n∈\<int>+. f`(f¯(m\<ra>n)\<rs>f¯(m)\<rs>f¯(n)) \<lsq> U"
"∀m∈\<int>+. ∀n∈\<int>+. N \<lsq> f`(f¯(m\<ra>n)\<rs>f¯(m)\<rs>f¯(n))"
by auto;
have "\<int>+×\<int>+ ≠ 0" using int_one_two_are_pos by auto;
moreover from A1 have "f: \<int>->\<int>"
using AlmostHoms_def by simp;
moreover from A1 have
"∀a∈\<int>.∃b∈\<int>+.∀x. b\<lsq>x --> a \<lsq> f`(x)"
using Int_ZF_2_3_L5 by simp;
moreover from A1 have
"∀a∈\<int>.∃b∈\<int>+.∀y. b\<lsq>y --> f`(\<rm>y) \<lsq> a"
using Int_ZF_2_3_L5A by simp;
moreover have
"∀x∈\<int>+×\<int>+. ε(f,x) ∈ \<int> ∧ f`(ε(f,x)) \<lsq> U ∧ N \<lsq> f`(ε(f,x))"
proof -
{ fix x assume A3: "x ∈ \<int>+×\<int>+"
let ?m = "fst(x)"
let ?n = "snd(x)"
from A3 have T: "?m ∈ \<int>+" "?n ∈ \<int>+" "?m\<ra>?n ∈ \<int>+"
using pos_int_closed_add_unfolded by auto;
with A1 have
"f¯(?m\<ra>?n) ∈ \<int>" "f¯(?m) ∈ \<int>" "f¯(?n) ∈ \<int>"
using Int_ZF_2_4_L2 PositiveSet_def by auto;
with I T have
"ε(f,x) ∈ \<int> ∧ f`(ε(f,x)) \<lsq> U ∧ N \<lsq> f`(ε(f,x))"
using Int_ZF_1_1_L5 by auto;
} thus ?thesis by simp;
qed;
ultimately show "∃M.∀x∈\<int>+×\<int>+. abs(ε(f,x)) \<lsq> M"
by (rule Int_ZF_1_6_L4);
qed;
text{*The (candidate for) inverse of a positive slope is a (well defined)
function on @{text "\<int>+"}.*}
lemma (in int1) Int_ZF_2_4_L9:
assumes A1: "f ∈ \<S>+" and A2: "g = {⟨p,f¯(p)⟩. p∈\<int>+}"
shows
"g : \<int>+->\<int>+"
"g : \<int>+->\<int>"
proof -
from A1 have
"∀p∈\<int>+. f¯(p) ∈ \<int>+"
"∀p∈\<int>+. f¯(p) ∈ \<int>"
using Int_ZF_2_4_L2 PositiveSet_def by auto;
with A2 show
"g : \<int>+->\<int>+" and "g : \<int>+->\<int>"
using ZF_fun_from_total by auto;
qed;
text{*What are the values of the (candidate for) the inverse of a positive slope?*}
lemma (in int1) Int_ZF_2_4_L10:
assumes A1: "f ∈ \<S>+" and A2: "g = {⟨p,f¯(p)⟩. p∈\<int>+}" and A3: "p∈\<int>+"
shows "g`(p) = f¯(p)"
proof -
from A1 A2 have "g : \<int>+->\<int>+" using Int_ZF_2_4_L9 by simp;
with A2 A3 show "g`(p) = f¯(p)" using ZF_fun_from_tot_val by simp;
qed;
text{*The (candidate for) the inverse of a positive slope is a slope.*}
lemma (in int1) Int_ZF_2_4_L11: assumes A1: "f ∈ \<S>+" and
A2: "∀m∈\<int>+. f¯(m)\<rs>\<one> ∈ \<int>+" and
A3: "g = {⟨p,f¯(p)⟩. p∈\<int>+}"
shows "OddExtension(\<int>,IntegerAddition,IntegerOrder,g) ∈ \<S>"
proof -
from A1 A2 have "∃L. ∀x∈\<int>+×\<int>+. abs(ε(f,x)) \<lsq> L"
using Int_ZF_2_4_L8 by simp;
then obtain L where I: "∀x∈\<int>+×\<int>+. abs(ε(f,x)) \<lsq> L"
by auto;
from A1 A3 have "g : \<int>+->\<int>" using Int_ZF_2_4_L9
by simp;
moreover have "∀m∈\<int>+. ∀n∈\<int>+. abs(δ(g,m,n)) \<lsq> L"
proof-
{ fix m n
assume A4: "m∈\<int>+" "n∈\<int>+"
then have "⟨m,n⟩ ∈ \<int>+×\<int>+" by simp
with I have "abs(ε(f,⟨m,n⟩)) \<lsq> L" by simp;
moreover have "ε(f,⟨m,n⟩) = f¯(m\<ra>n) \<rs> f¯(m) \<rs> f¯(n)"
by simp;
moreover from A1 A3 A4 have
"f¯(m\<ra>n) = g`(m\<ra>n)" "f¯(m) = g`(m)" "f¯(n) = g`(n)"
using pos_int_closed_add_unfolded Int_ZF_2_4_L10 by auto;
ultimately have "abs(δ(g,m,n)) \<lsq> L" by simp;
} thus "∀m∈\<int>+. ∀n∈\<int>+. abs(δ(g,m,n)) \<lsq> L" by simp
qed
ultimately show ?thesis by (rule Int_ZF_2_1_L24);
qed;
text{*Every positive slope that is at least $2$ on positive integers
almost has an inverse.*}
lemma (in int1) Int_ZF_2_4_L12: assumes A1: "f ∈ \<S>+" and
A2: "∀m∈\<int>+. f¯(m)\<rs>\<one> ∈ \<int>+"
shows "∃h∈\<S>. foh ∼ id(\<int>)"
proof -
let ?g = "{⟨p,f¯(p)⟩. p∈\<int>+}"
let ?h = "OddExtension(\<int>,IntegerAddition,IntegerOrder,?g)"
from A1 have
"∃M∈\<int>. ∀n∈\<int>. f`(n) \<lsq> f`(n\<rs>\<one>) \<ra> M"
using Int_ZF_2_1_L28 by simp;
then obtain M where
I: "M∈\<int>" and II: "∀n∈\<int>. f`(n) \<lsq> f`(n\<rs>\<one>) \<ra> M"
by auto;
from A1 A2 have T: "?h ∈ \<S>"
using Int_ZF_2_4_L11 by simp
moreover have "fo?h ∼ id(\<int>)"
proof -
from A1 T have "fo?h ∈ \<S>" using Int_ZF_2_1_L11
by simp;
moreover note I
moreover
{ fix m assume A3: "m∈\<int>+"
with A1 have "f¯(m) ∈ \<int>"
using Int_ZF_2_4_L2 PositiveSet_def by simp;
with II have "f`(f¯(m)) \<lsq> f`(f¯(m)\<rs>\<one>) \<ra> M"
by simp;
moreover from A1 A2 I A3 have "f`(f¯(m)\<rs>\<one>) \<ra> M \<lsq> m\<ra>M"
using Int_ZF_2_4_L4 int_ord_transl_inv by simp;
ultimately have "f`(f¯(m)) \<lsq> m\<ra>M"
by (rule Int_order_transitive);
moreover from A1 A3 have "m \<lsq> f`(f¯(m))"
using Int_ZF_2_4_L2 by simp;
moreover from A1 A2 T A3 have "f`(f¯(m)) = (fo?h)`(m)"
using Int_ZF_2_4_L9 Int_ZF_1_5_L11
Int_ZF_2_4_L10 PositiveSet_def Int_ZF_2_1_L10
by simp;
ultimately have "m \<lsq> (fo?h)`(m) ∧ (fo?h)`(m) \<lsq> m\<ra>M"
by simp; }
ultimately show "fo?h ∼ id(\<int>)" using Int_ZF_2_1_L32
by simp
qed
ultimately show "∃h∈\<S>. foh ∼ id(\<int>)"
by auto
qed;
text{*@{text "Int_ZF_2_4_L12"} is almost what we need, except that it has an assumption
that the values of the slope that we get the inverse for are not smaller than $2$ on
positive integers. The Arthan's proof of Theorem 11 has a mistake where he says "note that
for all but finitely many $m,n\in N$ $p=g(m)$ and $q=g(n)$ are both positive". Of course
there may be infinitely many pairs $\langle m,n \rangle$ such that $p,q$ are not both
positive. This is however easy to workaround: we just modify the slope by adding a
constant so that the slope is large enough on positive integers and then look
for the inverse.*}
theorem (in int1) pos_slope_has_inv: assumes A1: "f ∈ \<S>+"
shows "∃g∈\<S>. f∼g ∧ (∃h∈\<S>. goh ∼ id(\<int>))"
proof -
from A1 have "f: \<int>->\<int>" "\<one>∈\<int>" "\<two> ∈ \<int>"
using AlmostHoms_def int_zero_one_are_int int_two_three_are_int
by auto
moreover from A1 have
"∀a∈\<int>.∃b∈\<int>+.∀x. b\<lsq>x --> a \<lsq> f`(x)"
using Int_ZF_2_3_L5 by simp;
ultimately have
"∃c∈\<int>. \<two> \<lsq> Minimum(IntegerOrder,{n∈\<int>+. \<one> \<lsq> f`(n)\<ra>c})"
by (rule Int_ZF_1_6_L7);
then obtain c where I: "c∈\<int>" and
II: "\<two> \<lsq> Minimum(IntegerOrder,{n∈\<int>+. \<one> \<lsq> f`(n)\<ra>c})"
by auto;
let ?g = "{⟨m,f`(m)\<ra>c⟩. m∈\<int>}"
from A1 I have III: "?g∈\<S>" and IV: "f∼?g" using Int_ZF_2_1_L33
by auto
from IV have "⟨f,?g⟩ ∈ AlEqRel" by simp
with A1 have T: "?g ∈ \<S>+" by (rule Int_ZF_2_3_L9);
moreover have "∀m∈\<int>+. ?g¯(m)\<rs>\<one> ∈ \<int>+"
proof
fix m assume A2: "m∈\<int>+"
from A1 I II have V: "\<two> \<lsq> ?g¯(\<one>)"
using Int_ZF_2_1_L33 PositiveSet_def by simp;
moreover from A2 T have "?g¯(\<one>) \<lsq> ?g¯(m)"
using Int_ZF_1_5_L3 int_one_two_are_pos Int_ZF_2_4_L5
by simp;
ultimately have "\<two> \<lsq> ?g¯(m)"
by (rule Int_order_transitive);
then have "\<two>\<rs>\<one> \<lsq> ?g¯(m)\<rs>\<one>"
using int_zero_one_are_int Int_ZF_1_1_L4 int_ord_transl_inv
by simp;
then show "?g¯(m)\<rs>\<one> ∈ \<int>+"
using int_zero_one_are_int Int_ZF_1_2_L3 Int_ZF_1_5_L3
by simp;
qed;
ultimately have "∃h∈\<S>. ?goh ∼ id(\<int>)"
by (rule Int_ZF_2_4_L12);
with III IV show ?thesis by auto;
qed;
section{*Completeness*}
text{*In this section we consider properties of slopes that are
needed for the proof of completeness of real numbers constructred
in @{text "Real_ZF_1.thy"}. In particular we consider properties
of embedding of integers into the set of slopes by the mapping
$m \mapsto m^S$ , where $m^S$ is defined by $m^S(n) = m\cdot n$.*}
text{*If m is an integer, then $m^S$ is a slope whose value
is $m\cdot n$ for every integer.*}
lemma (in int1) Int_ZF_2_5_L1: assumes A1: "m ∈ \<int>"
shows
"∀n ∈ \<int>. (mS)`(n) = m·n"
"mS ∈ \<S>"
proof -
from A1 have I: "mS:\<int>->\<int>"
using Int_ZF_1_1_L5 ZF_fun_from_total by simp;
then show II: "∀n ∈ \<int>. (mS)`(n) = m·n" using ZF_fun_from_tot_val
by simp
{ fix n k
assume A2: "n∈\<int>" "k∈\<int>"
with A1 have T: "m·n ∈ \<int>" "m·k ∈ \<int>"
using Int_ZF_1_1_L5 by auto
from A1 A2 II T have "δ(mS,n,k) = m·k \<rs> m·k"
using Int_ZF_1_1_L5 Int_ZF_1_1_L1 Int_ZF_1_2_L3
by simp;
also from T have "… = \<zero>" using Int_ZF_1_1_L4
by simp;
finally have "δ(mS,n,k) = \<zero>" by simp;
then have "abs(δ(mS,n,k)) \<lsq> \<zero>"
using Int_ZF_2_L18 int_zero_one_are_int int_ord_is_refl refl_def
by simp;
} then have "∀n∈\<int>.∀k∈\<int>. abs(δ(mS,n,k)) \<lsq> \<zero>"
by simp
with I show "mS ∈ \<S>" by (rule Int_ZF_2_1_L5);
qed;
text{*For any slope $f$ there is an integer $m$ such that there is some slope $g$
that is almost equal to $m^S$ and dominates $f$ in the sense that $f\leq g$
on positive integers (which implies that either $g$ is almost equal to $f$ or
$g-f$ is a positive slope. This will be used in @{text "Real_ZF_1.thy"} to show
that for any real number there is an integer that (whose real embedding)
is greater or equal.*}
lemma (in int1) Int_ZF_2_5_L2: assumes A1: "f ∈ \<S>"
shows "∃m∈\<int>. ∃g∈\<S>. (mS∼g ∧ (f∼g ∨ g\<fp>(\<fm>f) ∈ \<S>+))"
proof -
from A1 have
"∃m k. m∈\<int> ∧ k∈\<int> ∧ (∀p∈\<int>. abs(f`(p)) \<lsq> m·abs(p)\<ra>k)"
using Arthan_Lem_8 by simp;
then obtain m k where I: "m∈\<int>" and II: "k∈\<int>" and
III: "∀p∈\<int>. abs(f`(p)) \<lsq> m·abs(p)\<ra>k"
by auto;
let ?g = "{⟨n,mS`(n) \<ra>k⟩. n∈\<int>}"
from I have IV: "mS ∈ \<S>" using Int_ZF_2_5_L1 by simp;
with II have V: "?g∈\<S>" and VI: "mS∼?g" using Int_ZF_2_1_L33
by auto;
{ fix n assume A2: "n∈\<int>+"
with A1 have "f`(n) ∈ \<int>"
using Int_ZF_2_1_L2B PositiveSet_def by simp;
then have "f`(n) \<lsq> abs(f`(n))" using Int_ZF_2_L19C
by simp;
moreover
from III A2 have "abs(f`(n)) \<lsq> m·abs(n) \<ra> k"
using PositiveSet_def by simp;
with A2 have "abs(f`(n)) \<lsq> m·n\<ra>k"
using Int_ZF_1_5_L4A by simp;
ultimately have "f`(n) \<lsq> m·n\<ra>k"
by (rule Int_order_transitive);
moreover
from II IV A2 have "?g`(n) = (mS)`(n)\<ra>k"
using Int_ZF_2_1_L33 PositiveSet_def by simp;
with I A2 have "?g`(n) = m·n\<ra>k"
using Int_ZF_2_5_L1 PositiveSet_def by simp;
ultimately have "f`(n) \<lsq> ?g`(n)"
by simp;
} then have "∀n∈\<int>+. f`(n) \<lsq> ?g`(n)"
by simp;
with A1 V have "f∼?g ∨ ?g \<fp> (\<fm>f) ∈ \<S>+"
using Int_ZF_2_3_L4C by simp;
with I V VI show ?thesis by auto;
qed;
text{*The negative of an integer embeds in slopes as a negative of the
orgiginal embedding.*}
lemma (in int1) Int_ZF_2_5_L3: assumes A1: "m ∈ \<int>"
shows "(\<rm>m)S = \<fm>(mS)"
proof -
from A1 have "(\<rm>m)S: \<int>->\<int>" and "(\<fm>(mS)): \<int>->\<int>"
using Int_ZF_1_1_L4 Int_ZF_2_5_L1 AlmostHoms_def Int_ZF_2_1_L12
by auto;
moreover have "∀n∈\<int>. ((\<rm>m)S)`(n) = (\<fm>(mS))`(n)"
proof
fix n assume A2: "n∈\<int>"
with A1 have
"((\<rm>m)S)`(n) = (\<rm>m)·n"
"(\<fm>(mS))`(n) = \<rm>(m·n)"
using Int_ZF_1_1_L4 Int_ZF_2_5_L1 Int_ZF_2_1_L12A
by auto;
with A1 A2 show "((\<rm>m)S)`(n) = (\<fm>(mS))`(n)"
using Int_ZF_1_1_L5 by simp;
qed
ultimately show "(\<rm>m)S = \<fm>(mS)" using fun_extension_iff
by simp;
qed;
text{*The sum of embeddings is the embeding of the sum.*}
lemma (in int1) Int_ZF_2_5_L3A: assumes A1: "m∈\<int>" "k∈\<int>"
shows "(mS) \<fp> (kS) = ((m\<ra>k)S)"
proof -
from A1 have T1: "m\<ra>k ∈ \<int>" using Int_ZF_1_1_L5
by simp
with A1 have T2:
"(mS) ∈ \<S>" "(kS) ∈ \<S>"
"(m\<ra>k)S ∈ \<S>"
"(mS) \<fp> (kS) ∈ \<S>"
using Int_ZF_2_5_L1 Int_ZF_2_1_L12C by auto;
then have
"(mS) \<fp> (kS) : \<int>->\<int>"
"(m\<ra>k)S : \<int>->\<int>"
using AlmostHoms_def by auto;
moreover have "∀n∈\<int>. ((mS) \<fp> (kS))`(n) = ((m\<ra>k)S)`(n)"
proof
fix n assume A2: "n∈\<int>"
with A1 T1 T2 have "((mS) \<fp> (kS))`(n) = (m\<ra>k)·n"
using Int_ZF_2_1_L12B Int_ZF_2_5_L1 Int_ZF_1_1_L1
by simp;
also from T1 A2 have "… = ((m\<ra>k)S)`(n)"
using Int_ZF_2_5_L1 by simp;
finally show "((mS) \<fp> (kS))`(n) = ((m\<ra>k)S)`(n)"
by simp;
qed;
ultimately show "(mS) \<fp> (kS) = ((m\<ra>k)S)"
using fun_extension_iff by simp
qed;
text{*The composition of embeddings is the embeding of the product.*}
lemma (in int1) Int_ZF_2_5_L3B: assumes A1: "m∈\<int>" "k∈\<int>"
shows "(mS) o (kS) = ((m·k)S)"
proof -
from A1 have T1: "m·k ∈ \<int>" using Int_ZF_1_1_L5
by simp
with A1 have T2:
"(mS) ∈ \<S>" "(kS) ∈ \<S>"
"(m·k)S ∈ \<S>"
"(mS) o (kS) ∈ \<S>"
using Int_ZF_2_5_L1 Int_ZF_2_1_L11 by auto;
then have
"(mS) o (kS) : \<int>->\<int>"
"(m·k)S : \<int>->\<int>"
using AlmostHoms_def by auto;
moreover have "∀n∈\<int>. ((mS) o (kS))`(n) = ((m·k)S)`(n)"
proof
fix n assume A2: "n∈\<int>"
with A1 T2 have
"((mS) o (kS))`(n) = (mS)`(k·n)"
using Int_ZF_2_1_L10 Int_ZF_2_5_L1 by simp;
moreover
from A1 A2 have "k·n ∈ \<int>" using Int_ZF_1_1_L5
by simp;
with A1 A2 have "(mS)`(k·n) = m·k·n"
using Int_ZF_2_5_L1 Int_ZF_1_1_L7 by simp;
ultimately have "((mS) o (kS))`(n) = m·k·n"
by simp;
also from T1 A2 have "m·k·n = ((m·k)S)`(n)"
using Int_ZF_2_5_L1 by simp;
finally show "((mS) o (kS))`(n) = ((m·k)S)`(n)"
by simp;
qed;
ultimately show "(mS) o (kS) = ((m·k)S)"
using fun_extension_iff by simp
qed;
text{*Embedding integers in slopes preserves order.*}
lemma (in int1) Int_ZF_2_5_L4: assumes A1: "m\<lsq>n"
shows "(mS) ∼ (nS) ∨ (nS)\<fp>(\<fm>(mS)) ∈ \<S>+"
proof -
from A1 have "mS ∈ \<S>" and "nS ∈ \<S>"
using Int_ZF_2_L1A Int_ZF_2_5_L1 by auto;
moreover from A1 have "∀k∈\<int>+. (mS)`(k) \<lsq> (nS)`(k)"
using Int_ZF_1_3_L13B Int_ZF_2_L1A PositiveSet_def Int_ZF_2_5_L1
by simp;
ultimately show ?thesis using Int_ZF_2_3_L4C
by simp;
qed;
text{*We aim at showing that $m\mapsto m^S$ is an injection modulo
the relation of almost equality. To do that we first show that if
$m^S$ has finite range, then $m=0$.*}
lemma (in int1) Int_ZF_2_5_L5:
assumes "m∈\<int>" and "mS ∈ FinRangeFunctions(\<int>,\<int>)"
shows "m=\<zero>"
using prems FinRangeFunctions_def Int_ZF_2_5_L1 AlmostHoms_def
func_imagedef Int_ZF_1_6_L8 by simp;
text{*Embeddings of two integers are almost equal only if
the integers are equal.*}
lemma (in int1) Int_ZF_2_5_L6:
assumes A1: "m∈\<int>" "k∈\<int>" and A2: "(mS) ∼ (kS)"
shows "m=k"
proof -
from A1 have T: "m\<rs>k ∈ \<int>" using Int_ZF_1_1_L5 by simp
from A1 have "(\<fm>(kS)) = ((\<rm>k)S)"
using Int_ZF_2_5_L3 by simp;
then have "mS \<fp> (\<fm>(kS)) = (mS) \<fp> ((\<rm>k)S)"
by simp;
with A1 have "mS \<fp> (\<fm>(kS)) = ((m\<rs>k)S)"
using Int_ZF_1_1_L4 Int_ZF_2_5_L3A by simp;
moreover from A1 A2 have "mS \<fp> (\<fm>(kS)) ∈ FinRangeFunctions(\<int>,\<int>)"
using Int_ZF_2_5_L1 Int_ZF_2_1_L9D by simp;
ultimately have "(m\<rs>k)S ∈ FinRangeFunctions(\<int>,\<int>)"
by simp;
with T have "m\<rs>k = \<zero>" using Int_ZF_2_5_L5
by simp;
with A1 show "m=k" by (rule Int_ZF_1_L15);
qed;
text{*Embedding of $1$ is the identity slope and embedding of zero is a
finite range function.*}
lemma (in int1) Int_ZF_2_5_L7: shows
"\<one>S = id(\<int>)"
"\<zero>S ∈ FinRangeFunctions(\<int>,\<int>)"
proof -
have "id(\<int>) = {⟨x,x⟩. x∈\<int>}"
using id_def by blast;
then show "\<one>S = id(\<int>)" using Int_ZF_1_1_L4 by simp;
have "{\<zero>S`(n). n∈\<int>} = {\<zero>·n. n∈\<int>}"
using int_zero_one_are_int Int_ZF_2_5_L1 by simp;
also have "… = {\<zero>}" using Int_ZF_1_1_L4 int_not_empty
by simp;
finally have "{\<zero>S`(n). n∈\<int>} = {\<zero>}" by simp;
then have "{\<zero>S`(n). n∈\<int>} ∈ Fin(\<int>)"
using int_zero_one_are_int Finite1_L16 by simp;
moreover have "\<zero>S: \<int>->\<int>"
using int_zero_one_are_int Int_ZF_2_5_L1 AlmostHoms_def
by simp;
ultimately show "\<zero>S ∈ FinRangeFunctions(\<int>,\<int>)"
using Finite1_L19 by simp;
qed;
text{*A somewhat technical condition for a embedding of an integer
to be "less or equal" (in the sense apriopriate for slopes) than
the composition of a slope and another integer (embedding).*}
lemma (in int1) Int_ZF_2_5_L8:
assumes A1: "f ∈ \<S>" and A2: "N ∈ \<int>" "M ∈ \<int>" and
A3: "∀n∈\<int>+. M·n \<lsq> f`(N·n)"
shows "MS ∼ fo(NS) ∨ (fo(NS)) \<fp> (\<fm>(MS)) ∈ \<S>+"
proof -
from A1 A2 have "MS ∈ \<S>" "fo(NS) ∈ \<S>"
using Int_ZF_2_5_L1 Int_ZF_2_1_L11 by auto;
moreover from A1 A2 A3 have "∀n∈\<int>+. (MS)`(n) \<lsq> (fo(NS))`(n)"
using Int_ZF_2_5_L1 PositiveSet_def Int_ZF_2_1_L10
by simp;
ultimately show ?thesis using Int_ZF_2_3_L4C
by simp;
qed;
text{*Another technical condition for the composition of a slope and
an integer (embedding) to be "less or equal" (in the sense apriopriate
for slopes) than embedding of another integer.*}
lemma (in int1) Int_ZF_2_5_L9:
assumes A1: "f ∈ \<S>" and A2: "N ∈ \<int>" "M ∈ \<int>" and
A3: "∀n∈\<int>+. f`(N·n) \<lsq> M·n "
shows "fo(NS) ∼ (MS) ∨ (MS) \<fp> (\<fm>(fo(NS))) ∈ \<S>+"
proof -;
from A1 A2 have "fo(NS) ∈ \<S>" "MS ∈ \<S>"
using Int_ZF_2_5_L1 Int_ZF_2_1_L11 by auto;
moreover from A1 A2 A3 have "∀n∈\<int>+. (fo(NS))`(n) \<lsq> (MS)`(n) "
using Int_ZF_2_5_L1 PositiveSet_def Int_ZF_2_1_L10
by simp;
ultimately show ?thesis using Int_ZF_2_3_L4C
by simp;
qed;
end
lemma Int_ZF_2_1_L1:
group1(int, IntegerAddition)
lemma Int_ZF_2_1_L2:
[| f ∈ AlmostHoms(int, IntegerAddition); n ∈ int; m ∈ int |] ==> IntegerAddition ` ⟨m, n⟩ ∈ int
[| f ∈ AlmostHoms(int, IntegerAddition); n ∈ int; m ∈ int |] ==> f ` (IntegerAddition ` ⟨m, n⟩) ∈ int
[| f ∈ AlmostHoms(int, IntegerAddition); n ∈ int; m ∈ int |] ==> f ` m ∈ int
[| f ∈ AlmostHoms(int, IntegerAddition); n ∈ int; m ∈ int |] ==> f ` n ∈ int
[| f ∈ AlmostHoms(int, IntegerAddition); n ∈ int; m ∈ int |] ==> IntegerAddition ` ⟨f ` m, f ` n⟩ ∈ int
[| f ∈ AlmostHoms(int, IntegerAddition); n ∈ int; m ∈ int |] ==> HomDiff(int, IntegerAddition, f, ⟨m, n⟩) ∈ int
lemma Int_ZF_2_1_L2A:
[| f ∈ int -> int; n ∈ int; m ∈ int |] ==> IntegerAddition ` ⟨m, n⟩ ∈ int
[| f ∈ int -> int; n ∈ int; m ∈ int |] ==> f ` (IntegerAddition ` ⟨m, n⟩) ∈ int
[| f ∈ int -> int; n ∈ int; m ∈ int |] ==> f ` m ∈ int
[| f ∈ int -> int; n ∈ int; m ∈ int |] ==> f ` n ∈ int
[| f ∈ int -> int; n ∈ int; m ∈ int |] ==> IntegerAddition ` ⟨f ` m, f ` n⟩ ∈ int
[| f ∈ int -> int; n ∈ int; m ∈ int |] ==> HomDiff(int, IntegerAddition, f, ⟨m, n⟩) ∈ int
lemma Int_ZF_2_1_L2B:
[| f ∈ AlmostHoms(int, IntegerAddition); m ∈ int |] ==> f ` m ∈ int
lemma Int_ZF_2_1_L3:
[| f ∈ int -> int; m ∈ int; n ∈ int |] ==> HomDiff(int, IntegerAddition, f, ⟨m, n⟩) = IntegerAddition ` ⟨IntegerAddition ` ⟨f ` (IntegerAddition ` ⟨m, n⟩), GroupInv(int, IntegerAddition) ` (f ` m)⟩, GroupInv(int, IntegerAddition) ` (f ` n)⟩
lemma Int_ZF_2_1_L3A:
[| f ∈ AlmostHoms(int, IntegerAddition); m ∈ int; n ∈ int |] ==> f ` (IntegerAddition ` ⟨m, n⟩) = IntegerAddition ` ⟨f ` m, IntegerAddition ` ⟨f ` n, IntegerAddition ` ⟨IntegerAddition ` ⟨f ` (IntegerAddition ` ⟨m, n⟩), GroupInv(int, IntegerAddition) ` (f ` m)⟩, GroupInv(int, IntegerAddition) ` (f ` n)⟩⟩⟩
lemma Int_ZF_2_1_L3B:
[| f ∈ int -> int; m ∈ int; n ∈ int |] ==> IntegerAddition ` ⟨IntegerAddition ` ⟨f ` (IntegerAddition ` ⟨m, n⟩), GroupInv(int, IntegerAddition) ` (f ` m)⟩, GroupInv(int, IntegerAddition) ` (f ` n)⟩ ∈ int
lemma Int_ZF_2_1_L3C:
[| f ∈ int -> int; m ∈ int; n ∈ int |] ==> f ` (IntegerAddition ` ⟨m, n⟩) = IntegerAddition ` ⟨IntegerAddition ` ⟨IntegerAddition ` ⟨IntegerAddition ` ⟨f ` (IntegerAddition ` ⟨m, n⟩), GroupInv(int, IntegerAddition) ` (f ` m)⟩, GroupInv(int, IntegerAddition) ` (f ` n)⟩, f ` n⟩, f ` m⟩
lemma Int_ZF_2_1_L4:
f ∈ int -> int ==> {AbsoluteValue(int, IntegerAddition, IntegerOrder) ` HomDiff(int, IntegerAddition, f, x) . x ∈ int × int} = {AbsoluteValue(int, IntegerAddition, IntegerOrder) ` (IntegerAddition ` ⟨IntegerAddition ` ⟨f ` (IntegerAddition ` ⟨m, n⟩), GroupInv(int, IntegerAddition) ` (f ` m)⟩, GroupInv(int, IntegerAddition) ` (f ` n)⟩) . ⟨m,n⟩ ∈ int × int}
lemma Int_ZF_2_1_L5:
[| f ∈ int -> int; ∀m∈int. ∀n∈int. ⟨AbsoluteValue(int, IntegerAddition, IntegerOrder) ` (IntegerAddition ` ⟨IntegerAddition ` ⟨f ` (IntegerAddition ` ⟨m, n⟩), GroupInv(int, IntegerAddition) ` (f ` m)⟩, GroupInv(int, IntegerAddition) ` (f ` n)⟩), L⟩ ∈ IntegerOrder |] ==> f ∈ AlmostHoms(int, IntegerAddition)
lemma Int_ZF_2_1_L7:
[| s ∈ AlmostHoms(int, IntegerAddition); n ∈ int; m ∈ int |] ==> ⟨AbsoluteValue(int, IntegerAddition, IntegerOrder) ` (IntegerAddition ` ⟨IntegerAddition ` ⟨s ` (IntegerAddition ` ⟨m, n⟩), GroupInv(int, IntegerAddition) ` (s ` m)⟩, GroupInv(int, IntegerAddition) ` (s ` n)⟩), Maximum (IntegerOrder, {AbsoluteValue(int, IntegerAddition, IntegerOrder) ` (IntegerAddition ` ⟨IntegerAddition ` ⟨s ` (IntegerAddition ` ⟨m, n⟩), GroupInv(int, IntegerAddition) ` (s ` m)⟩, GroupInv(int, IntegerAddition) ` (s ` n)⟩) . ⟨m,n⟩ ∈ int × int})⟩ ∈ IntegerOrder
[| s ∈ AlmostHoms(int, IntegerAddition); n ∈ int; m ∈ int |] ==> IntegerAddition ` ⟨IntegerAddition ` ⟨s ` (IntegerAddition ` ⟨m, n⟩), GroupInv(int, IntegerAddition) ` (s ` m)⟩, GroupInv(int, IntegerAddition) ` (s ` n)⟩ ∈ int
[| s ∈ AlmostHoms(int, IntegerAddition); n ∈ int; m ∈ int |] ==> Maximum (IntegerOrder, {AbsoluteValue(int, IntegerAddition, IntegerOrder) ` (IntegerAddition ` ⟨IntegerAddition ` ⟨s ` (IntegerAddition ` ⟨m, n⟩), GroupInv(int, IntegerAddition) ` (s ` m)⟩, GroupInv(int, IntegerAddition) ` (s ` n)⟩) . ⟨m,n⟩ ∈ int × int}) ∈ int
[| s ∈ AlmostHoms(int, IntegerAddition); n ∈ int; m ∈ int |] ==> ⟨GroupInv(int, IntegerAddition) ` Maximum (IntegerOrder, {AbsoluteValue(int, IntegerAddition, IntegerOrder) ` (IntegerAddition ` ⟨IntegerAddition ` ⟨s ` (IntegerAddition ` ⟨m, n⟩), GroupInv(int, IntegerAddition) ` (s ` m)⟩, GroupInv(int, IntegerAddition) ` (s ` n)⟩) . ⟨m,n⟩ ∈ int × int}), IntegerAddition ` ⟨IntegerAddition ` ⟨s ` (IntegerAddition ` ⟨m, n⟩), GroupInv(int, IntegerAddition) ` (s ` m)⟩, GroupInv(int, IntegerAddition) ` (s ` n)⟩⟩ ∈ IntegerOrder
lemma Int_ZF_2_1_L8:
s ∈ AlmostHoms(int, IntegerAddition) ==> ⟨AbsoluteValue(int, IntegerAddition, IntegerOrder) ` (s ` TheNeutralElement(int, IntegerAddition)), Maximum (IntegerOrder, {AbsoluteValue(int, IntegerAddition, IntegerOrder) ` (IntegerAddition ` ⟨IntegerAddition ` ⟨s ` (IntegerAddition ` ⟨m, n⟩), GroupInv(int, IntegerAddition) ` (s ` m)⟩, GroupInv(int, IntegerAddition) ` (s ` n)⟩) . ⟨m,n⟩ ∈ int × int})⟩ ∈ IntegerOrder
s ∈ AlmostHoms(int, IntegerAddition) ==> ⟨TheNeutralElement(int, IntegerAddition), Maximum (IntegerOrder, {AbsoluteValue(int, IntegerAddition, IntegerOrder) ` (IntegerAddition ` ⟨IntegerAddition ` ⟨s ` (IntegerAddition ` ⟨m, n⟩), GroupInv(int, IntegerAddition) ` (s ` m)⟩, GroupInv(int, IntegerAddition) ` (s ` n)⟩) . ⟨m,n⟩ ∈ int × int})⟩ ∈ IntegerOrder
s ∈ AlmostHoms(int, IntegerAddition) ==> AbsoluteValue(int, IntegerAddition, IntegerOrder) ` (s ` TheNeutralElement(int, IntegerAddition)) ∈ int
s ∈ AlmostHoms(int, IntegerAddition) ==> Maximum (IntegerOrder, {AbsoluteValue(int, IntegerAddition, IntegerOrder) ` (IntegerAddition ` ⟨IntegerAddition ` ⟨s ` (IntegerAddition ` ⟨m, n⟩), GroupInv(int, IntegerAddition) ` (s ` m)⟩, GroupInv(int, IntegerAddition) ` (s ` n)⟩) . ⟨m,n⟩ ∈ int × int}) ∈ int
s ∈ AlmostHoms(int, IntegerAddition) ==> IntegerAddition ` ⟨AbsoluteValue(int, IntegerAddition, IntegerOrder) ` (s ` TheNeutralElement(int, IntegerAddition)), Maximum (IntegerOrder, {AbsoluteValue(int, IntegerAddition, IntegerOrder) ` (IntegerAddition ` ⟨IntegerAddition ` ⟨s ` (IntegerAddition ` ⟨m, n⟩), GroupInv(int, IntegerAddition) ` (s ` m)⟩, GroupInv(int, IntegerAddition) ` (s ` n)⟩) . ⟨m,n⟩ ∈ int × int})⟩ ∈ int
lemma Int_ZF_2_1_L9:
[| s ∈ AlmostHoms(int, IntegerAddition); r ∈ AlmostHoms(int, IntegerAddition); ∀m∈int. ⟨AbsoluteValue(int, IntegerAddition, IntegerOrder) ` (IntegerAddition ` ⟨s ` m, GroupInv(int, IntegerAddition) ` (r ` m)⟩), L⟩ ∈ IntegerOrder |] ==> ⟨s, r⟩ ∈ QuotientGroupRel (AlmostHoms(int, IntegerAddition), AlHomOp1(int, IntegerAddition), FinRangeFunctions(int, int))
lemma Int_ZF_2_1_L9A:
⟨s, r⟩ ∈ QuotientGroupRel (AlmostHoms(int, IntegerAddition), AlHomOp1(int, IntegerAddition), FinRangeFunctions(int, int)) ==> ∃L∈int. ∀m∈int. ⟨AbsoluteValue(int, IntegerAddition, IntegerOrder) ` (IntegerAddition ` ⟨s ` m, GroupInv(int, IntegerAddition) ` (r ` m)⟩), L⟩ ∈ IntegerOrder
⟨s, r⟩ ∈ QuotientGroupRel (AlmostHoms(int, IntegerAddition), AlHomOp1(int, IntegerAddition), FinRangeFunctions(int, int)) ==> s ∈ AlmostHoms(int, IntegerAddition)
⟨s, r⟩ ∈ QuotientGroupRel (AlmostHoms(int, IntegerAddition), AlHomOp1(int, IntegerAddition), FinRangeFunctions(int, int)) ==> r ∈ AlmostHoms(int, IntegerAddition)
lemma Int_ZF_2_1_L9B:
QuotientGroupRel
(AlmostHoms(int, IntegerAddition), AlHomOp1(int, IntegerAddition),
FinRangeFunctions(int, int)) ⊆
AlmostHoms(int, IntegerAddition) × AlmostHoms(int, IntegerAddition)
equiv(AlmostHoms(int, IntegerAddition),
QuotientGroupRel
(AlmostHoms(int, IntegerAddition), AlHomOp1(int, IntegerAddition),
FinRangeFunctions(int, int)))
lemma Int_ZF_2_1_L9C:
[| s ∈ AlmostHoms(int, IntegerAddition); r ∈ AlmostHoms(int, IntegerAddition); AlHomOp1(int, IntegerAddition) ` ⟨s, GroupInv(int, IntegerAddition) O r⟩ ∈ FinRangeFunctions(int, int) |] ==> ⟨s, r⟩ ∈ QuotientGroupRel (AlmostHoms(int, IntegerAddition), AlHomOp1(int, IntegerAddition), FinRangeFunctions(int, int))
[| s ∈ AlmostHoms(int, IntegerAddition); r ∈ AlmostHoms(int, IntegerAddition); AlHomOp1(int, IntegerAddition) ` ⟨s, GroupInv(int, IntegerAddition) O r⟩ ∈ FinRangeFunctions(int, int) |] ==> ⟨r, s⟩ ∈ QuotientGroupRel (AlmostHoms(int, IntegerAddition), AlHomOp1(int, IntegerAddition), FinRangeFunctions(int, int))
lemma Int_ZF_2_1_L9D:
⟨s, r⟩ ∈ QuotientGroupRel (AlmostHoms(int, IntegerAddition), AlHomOp1(int, IntegerAddition), FinRangeFunctions(int, int)) ==> AlHomOp1(int, IntegerAddition) ` ⟨s, GroupInv(int, IntegerAddition) O r⟩ ∈ FinRangeFunctions(int, int)
lemma Int_ZF_2_1_L10:
[| s ∈ AlmostHoms(int, IntegerAddition); r ∈ AlmostHoms(int, IntegerAddition); m ∈ int |] ==> AlHomOp2(int, IntegerAddition) ` ⟨s, r⟩ ` m = s ` (r ` m)
[| s ∈ AlmostHoms(int, IntegerAddition); r ∈ AlmostHoms(int, IntegerAddition); m ∈ int |] ==> s ` (r ` m) ∈ int
lemma Int_ZF_2_1_L11:
[| s ∈ AlmostHoms(int, IntegerAddition); r ∈ AlmostHoms(int, IntegerAddition) |] ==> AlHomOp2(int, IntegerAddition) ` ⟨s, r⟩ ∈ AlmostHoms(int, IntegerAddition)
lemma Int_ZF_2_1_L12:
s ∈ AlmostHoms(int, IntegerAddition) ==> GroupInv(int, IntegerAddition) O s ∈ AlmostHoms(int, IntegerAddition)
lemma Int_ZF_2_1_L12A:
[| s ∈ AlmostHoms(int, IntegerAddition); m ∈ int |] ==> (GroupInv(int, IntegerAddition) O s) ` m = GroupInv(int, IntegerAddition) ` (s ` m)
lemma Int_ZF_2_1_L12B:
[| s ∈ AlmostHoms(int, IntegerAddition); r ∈ AlmostHoms(int, IntegerAddition); m ∈ int |] ==> AlHomOp1(int, IntegerAddition) ` ⟨s, r⟩ ` m = IntegerAddition ` ⟨s ` m, r ` m⟩
lemma Int_ZF_2_1_L12C:
[| s ∈ AlmostHoms(int, IntegerAddition); r ∈ AlmostHoms(int, IntegerAddition) |] ==> AlHomOp1(int, IntegerAddition) ` ⟨s, r⟩ ∈ AlmostHoms(int, IntegerAddition)
lemma Int_ZF_2_1_L13:
[| s ∈ AlmostHoms(int, IntegerAddition); n ∈ int; m ∈ int |] ==> IntegerAddition ` ⟨s ` (IntegerMultiplication ` ⟨n, m⟩), IntegerAddition ` ⟨s ` m, IntegerAddition ` ⟨IntegerAddition ` ⟨s ` (IntegerAddition ` ⟨IntegerMultiplication ` ⟨n, m⟩, m⟩), GroupInv(int, IntegerAddition) ` (s ` (IntegerMultiplication ` ⟨n, m⟩))⟩, GroupInv(int, IntegerAddition) ` (s ` m)⟩⟩⟩ = s ` (IntegerMultiplication ` ⟨IntegerAddition ` ⟨n, TheNeutralElement(int, IntegerMultiplication)⟩, m⟩)
lemma Int_ZF_2_1_L14:
[| s ∈ AlmostHoms(int, IntegerAddition); m ∈ int |] ==> s ` (GroupInv(int, IntegerAddition) ` m) = IntegerAddition ` ⟨IntegerAddition ` ⟨s ` TheNeutralElement(int, IntegerAddition), GroupInv(int, IntegerAddition) ` (IntegerAddition ` ⟨IntegerAddition ` ⟨s ` (IntegerAddition ` ⟨m, GroupInv(int, IntegerAddition) ` m⟩), GroupInv(int, IntegerAddition) ` (s ` m)⟩, GroupInv(int, IntegerAddition) ` (s ` (GroupInv(int, IntegerAddition) ` m))⟩)⟩, GroupInv(int, IntegerAddition) ` (s ` m)⟩
[| s ∈ AlmostHoms(int, IntegerAddition); m ∈ int |] ==> ⟨AbsoluteValue(int, IntegerAddition, IntegerOrder) ` (IntegerAddition ` ⟨s ` m, s ` (GroupInv(int, IntegerAddition) ` m)⟩), IntegerMultiplication ` ⟨IntegerAddition ` ⟨TheNeutralElement(int, IntegerMultiplication), TheNeutralElement(int, IntegerMultiplication)⟩, Maximum (IntegerOrder, {AbsoluteValue(int, IntegerAddition, IntegerOrder) ` (IntegerAddition ` ⟨IntegerAddition ` ⟨s ` (IntegerAddition ` ⟨m, n⟩), GroupInv(int, IntegerAddition) ` (s ` m)⟩, GroupInv(int, IntegerAddition) ` (s ` n)⟩) . ⟨m,n⟩ ∈ int × int})⟩⟩ ∈ IntegerOrder
[| s ∈ AlmostHoms(int, IntegerAddition); m ∈ int |] ==> ⟨AbsoluteValue(int, IntegerAddition, IntegerOrder) ` (s ` (GroupInv(int, IntegerAddition) ` m)), IntegerAddition ` ⟨IntegerMultiplication ` ⟨IntegerAddition ` ⟨TheNeutralElement(int, IntegerMultiplication), TheNeutralElement(int, IntegerMultiplication)⟩, Maximum (IntegerOrder, {AbsoluteValue(int, IntegerAddition, IntegerOrder) ` (IntegerAddition ` ⟨IntegerAddition ` ⟨s ` (IntegerAddition ` ⟨m, n⟩), GroupInv(int, IntegerAddition) ` (s ` m)⟩, GroupInv(int, IntegerAddition) ` (s ` n)⟩) . ⟨m,n⟩ ∈ int × int})⟩, AbsoluteValue(int, IntegerAddition, IntegerOrder) ` (s ` m)⟩⟩ ∈ IntegerOrder
[| s ∈ AlmostHoms(int, IntegerAddition); m ∈ int |] ==> ⟨s ` (GroupInv(int, IntegerAddition) ` m), IntegerAddition ` ⟨IntegerAddition ` ⟨AbsoluteValue(int, IntegerAddition, IntegerOrder) ` (s ` TheNeutralElement(int, IntegerAddition)), Maximum (IntegerOrder, {AbsoluteValue(int, IntegerAddition, IntegerOrder) ` (IntegerAddition ` ⟨IntegerAddition ` ⟨s ` (IntegerAddition ` ⟨m, n⟩), GroupInv(int, IntegerAddition) ` (s ` m)⟩, GroupInv(int, IntegerAddition) ` (s ` n)⟩) . ⟨m,n⟩ ∈ int × int})⟩, GroupInv(int, IntegerAddition) ` (s ` m)⟩⟩ ∈ IntegerOrder
lemma Int_ZF_2_1_L14A:
[| f ∈ int -> int; m ∈ int |] ==> f ` (GroupInv(int, IntegerAddition) ` m) = IntegerAddition ` ⟨IntegerAddition ` ⟨GroupInv(int, IntegerAddition) ` (IntegerAddition ` ⟨IntegerAddition ` ⟨f ` (IntegerAddition ` ⟨m, GroupInv(int, IntegerAddition) ` m⟩), GroupInv(int, IntegerAddition) ` (f ` m)⟩, GroupInv(int, IntegerAddition) ` (f ` (GroupInv(int, IntegerAddition) ` m))⟩), f ` TheNeutralElement(int, IntegerAddition)⟩, GroupInv(int, IntegerAddition) ` (f ` m)⟩
lemma Int_ZF_2_1_L15:
[| s ∈ AlmostHoms(int, IntegerAddition); M ∈ PositiveSet(int, IntegerAddition, IntegerOrder) |] ==> Maximum (IntegerOrder, s `` Interval (IntegerOrder, TheNeutralElement(int, IntegerAddition), IntegerAddition ` ⟨M, GroupInv(int, IntegerAddition) ` TheNeutralElement(int, IntegerMultiplication)⟩)) ∈ int
[| s ∈ AlmostHoms(int, IntegerAddition); M ∈ PositiveSet(int, IntegerAddition, IntegerOrder) |] ==> ∀n∈Interval (IntegerOrder, TheNeutralElement(int, IntegerAddition), IntegerAddition ` ⟨M, GroupInv(int, IntegerAddition) ` TheNeutralElement(int, IntegerMultiplication)⟩). ⟨s ` n, Maximum (IntegerOrder, s `` Interval (IntegerOrder, TheNeutralElement(int, IntegerAddition), IntegerAddition ` ⟨M, GroupInv(int, IntegerAddition) ` TheNeutralElement(int, IntegerMultiplication)⟩))⟩ ∈ IntegerOrder
[| s ∈ AlmostHoms(int, IntegerAddition); M ∈ PositiveSet(int, IntegerAddition, IntegerOrder) |] ==> Minimum (IntegerOrder, s `` Interval (IntegerOrder, TheNeutralElement(int, IntegerAddition), IntegerAddition ` ⟨M, GroupInv(int, IntegerAddition) ` TheNeutralElement(int, IntegerMultiplication)⟩)) ∈ int
[| s ∈ AlmostHoms(int, IntegerAddition); M ∈ PositiveSet(int, IntegerAddition, IntegerOrder) |] ==> ∀n∈Interval (IntegerOrder, TheNeutralElement(int, IntegerAddition), IntegerAddition ` ⟨M, GroupInv(int, IntegerAddition) ` TheNeutralElement(int, IntegerMultiplication)⟩). ⟨Minimum (IntegerOrder, s `` Interval (IntegerOrder, TheNeutralElement(int, IntegerAddition), IntegerAddition ` ⟨M, GroupInv(int, IntegerAddition) ` TheNeutralElement(int, IntegerMultiplication)⟩)), s ` n⟩ ∈ IntegerOrder
lemma Int_ZF_2_1_L16:
[| s ∈ AlmostHoms(int, IntegerAddition); m ∈ int; M ∈ PositiveSet(int, IntegerAddition, IntegerOrder); k ∈ Interval (IntegerOrder, TheNeutralElement(int, IntegerAddition), IntegerAddition ` ⟨M, GroupInv(int, IntegerAddition) ` TheNeutralElement(int, IntegerMultiplication)⟩) |] ==> ⟨IntegerAddition ` ⟨s ` (IntegerMultiplication ` ⟨m, M⟩), IntegerAddition ` ⟨Minimum (IntegerOrder, s `` Interval (IntegerOrder, TheNeutralElement(int, IntegerAddition), IntegerAddition ` ⟨M, GroupInv(int, IntegerAddition) ` TheNeutralElement(int, IntegerMultiplication)⟩)), GroupInv(int, IntegerAddition) ` Maximum (IntegerOrder, {AbsoluteValue(int, IntegerAddition, IntegerOrder) ` (IntegerAddition ` ⟨IntegerAddition ` ⟨s ` (IntegerAddition ` ⟨m, n⟩), GroupInv(int, IntegerAddition) ` (s ` m)⟩, GroupInv(int, IntegerAddition) ` (s ` n)⟩) . ⟨m,n⟩ ∈ int × int})⟩⟩, s ` (IntegerAddition ` ⟨IntegerMultiplication ` ⟨m, M⟩, k⟩)⟩ ∈ IntegerOrder
lemma Int_ZF_2_1_L17:
id(int) ∈ AlmostHoms(int, IntegerAddition)
lemma Int_ZF_2_1_L18:
[| f ∈ int -> int; m ∈ int; n ∈ int |] ==> AbsoluteValue(int, IntegerAddition, IntegerOrder) ` (IntegerAddition ` ⟨IntegerAddition ` ⟨f ` n, f ` m⟩, GroupInv(int, IntegerAddition) ` (f ` (IntegerAddition ` ⟨m, n⟩))⟩) = AbsoluteValue(int, IntegerAddition, IntegerOrder) ` (IntegerAddition ` ⟨IntegerAddition ` ⟨f ` (IntegerAddition ` ⟨m, n⟩), GroupInv(int, IntegerAddition) ` (f ` m)⟩, GroupInv(int, IntegerAddition) ` (f ` n)⟩)
[| f ∈ int -> int; m ∈ int; n ∈ int |] ==> AbsoluteValue(int, IntegerAddition, IntegerOrder) ` (IntegerAddition ` ⟨IntegerAddition ` ⟨f ` m, f ` n⟩, GroupInv(int, IntegerAddition) ` (f ` (IntegerAddition ` ⟨m, n⟩))⟩) = AbsoluteValue(int, IntegerAddition, IntegerOrder) ` (IntegerAddition ` ⟨IntegerAddition ` ⟨f ` (IntegerAddition ` ⟨m, n⟩), GroupInv(int, IntegerAddition) ` (f ` m)⟩, GroupInv(int, IntegerAddition) ` (f ` n)⟩)
[| f ∈ int -> int; m ∈ int; n ∈ int |] ==> IntegerAddition ` ⟨IntegerAddition ` ⟨GroupInv(int, IntegerAddition) ` (f ` m), GroupInv(int, IntegerAddition) ` (f ` n)⟩, f ` (IntegerAddition ` ⟨m, n⟩)⟩ = IntegerAddition ` ⟨IntegerAddition ` ⟨f ` (IntegerAddition ` ⟨m, n⟩), GroupInv(int, IntegerAddition) ` (f ` m)⟩, GroupInv(int, IntegerAddition) ` (f ` n)⟩
[| f ∈ int -> int; m ∈ int; n ∈ int |] ==> IntegerAddition ` ⟨IntegerAddition ` ⟨GroupInv(int, IntegerAddition) ` (f ` n), GroupInv(int, IntegerAddition) ` (f ` m)⟩, f ` (IntegerAddition ` ⟨m, n⟩)⟩ = IntegerAddition ` ⟨IntegerAddition ` ⟨f ` (IntegerAddition ` ⟨m, n⟩), GroupInv(int, IntegerAddition) ` (f ` m)⟩, GroupInv(int, IntegerAddition) ` (f ` n)⟩
[| f ∈ int -> int; m ∈ int; n ∈ int |] ==> AbsoluteValue(int, IntegerAddition, IntegerOrder) ` (IntegerAddition ` ⟨IntegerAddition ` ⟨GroupInv(int, IntegerAddition) ` (f ` (IntegerAddition ` ⟨m, n⟩)), f ` m⟩, f ` n⟩) = AbsoluteValue(int, IntegerAddition, IntegerOrder) ` (IntegerAddition ` ⟨IntegerAddition ` ⟨f ` (IntegerAddition ` ⟨m, n⟩), GroupInv(int, IntegerAddition) ` (f ` m)⟩, GroupInv(int, IntegerAddition) ` (f ` n)⟩)
lemma Int_ZF_2_1_L19:
[| f ∈ int -> int; ∀x∈int. GroupInv(int, IntegerAddition) ` (f ` (GroupInv(int, IntegerAddition) ` x)) = f ` x; m ∈ int; n ∈ int |] ==> AbsoluteValue(int, IntegerAddition, IntegerOrder) ` (IntegerAddition ` ⟨IntegerAddition ` ⟨f ` (IntegerAddition ` ⟨GroupInv(int, IntegerAddition) ` m, IntegerAddition ` ⟨m, n⟩⟩), GroupInv(int, IntegerAddition) ` (f ` (GroupInv(int, IntegerAddition) ` m))⟩, GroupInv(int, IntegerAddition) ` (f ` (IntegerAddition ` ⟨m, n⟩))⟩) = AbsoluteValue(int, IntegerAddition, IntegerOrder) ` (IntegerAddition ` ⟨IntegerAddition ` ⟨f ` (IntegerAddition ` ⟨m, n⟩), GroupInv(int, IntegerAddition) ` (f ` m)⟩, GroupInv(int, IntegerAddition) ` (f ` n)⟩)
[| f ∈ int -> int; ∀x∈int. GroupInv(int, IntegerAddition) ` (f ` (GroupInv(int, IntegerAddition) ` x)) = f ` x; m ∈ int; n ∈ int |] ==> AbsoluteValue(int, IntegerAddition, IntegerOrder) ` (IntegerAddition ` ⟨IntegerAddition ` ⟨f ` (IntegerAddition ` ⟨GroupInv(int, IntegerAddition) ` n, IntegerAddition ` ⟨m, n⟩⟩), GroupInv(int, IntegerAddition) ` (f ` (GroupInv(int, IntegerAddition) ` n))⟩, GroupInv(int, IntegerAddition) ` (f ` (IntegerAddition ` ⟨m, n⟩))⟩) = AbsoluteValue(int, IntegerAddition, IntegerOrder) ` (IntegerAddition ` ⟨IntegerAddition ` ⟨f ` (IntegerAddition ` ⟨m, n⟩), GroupInv(int, IntegerAddition) ` (f ` m)⟩, GroupInv(int, IntegerAddition) ` (f ` n)⟩)
[| f ∈ int -> int; ∀x∈int. GroupInv(int, IntegerAddition) ` (f ` (GroupInv(int, IntegerAddition) ` x)) = f ` x; m ∈ int; n ∈ int |] ==> IntegerAddition ` ⟨IntegerAddition ` ⟨f ` (IntegerAddition ` ⟨n, GroupInv(int, IntegerAddition) ` (IntegerAddition ` ⟨m, n⟩)⟩), GroupInv(int, IntegerAddition) ` (f ` n)⟩, GroupInv(int, IntegerAddition) ` (f ` (GroupInv(int, IntegerAddition) ` (IntegerAddition ` ⟨m, n⟩)))⟩ = IntegerAddition ` ⟨IntegerAddition ` ⟨f ` (IntegerAddition ` ⟨m, n⟩), GroupInv(int, IntegerAddition) ` (f ` m)⟩, GroupInv(int, IntegerAddition) ` (f ` n)⟩
[| f ∈ int -> int; ∀x∈int. GroupInv(int, IntegerAddition) ` (f ` (GroupInv(int, IntegerAddition) ` x)) = f ` x; m ∈ int; n ∈ int |] ==> IntegerAddition ` ⟨IntegerAddition ` ⟨f ` (IntegerAddition ` ⟨m, GroupInv(int, IntegerAddition) ` (IntegerAddition ` ⟨m, n⟩)⟩), GroupInv(int, IntegerAddition) ` (f ` m)⟩, GroupInv(int, IntegerAddition) ` (f ` (GroupInv(int, IntegerAddition) ` (IntegerAddition ` ⟨m, n⟩)))⟩ = IntegerAddition ` ⟨IntegerAddition ` ⟨f ` (IntegerAddition ` ⟨m, n⟩), GroupInv(int, IntegerAddition) ` (f ` m)⟩, GroupInv(int, IntegerAddition) ` (f ` n)⟩
[| f ∈ int -> int; ∀x∈int. GroupInv(int, IntegerAddition) ` (f ` (GroupInv(int, IntegerAddition) ` x)) = f ` x; m ∈ int; n ∈ int |] ==> AbsoluteValue(int, IntegerAddition, IntegerOrder) ` (IntegerAddition ` ⟨IntegerAddition ` ⟨f ` (IntegerAddition ` ⟨GroupInv(int, IntegerAddition) ` m, GroupInv(int, IntegerAddition) ` n⟩), GroupInv(int, IntegerAddition) ` (f ` (GroupInv(int, IntegerAddition) ` m))⟩, GroupInv(int, IntegerAddition) ` (f ` (GroupInv(int, IntegerAddition) ` n))⟩) = AbsoluteValue(int, IntegerAddition, IntegerOrder) ` (IntegerAddition ` ⟨IntegerAddition ` ⟨f ` (IntegerAddition ` ⟨m, n⟩), GroupInv(int, IntegerAddition) ` (f ` m)⟩, GroupInv(int, IntegerAddition) ` (f ` n)⟩)
lemma Int_ZF_2_1_L20:
[| f ∈ int -> int; ∀a∈PositiveSet(int, IntegerAddition, IntegerOrder). ∀b∈PositiveSet(int, IntegerAddition, IntegerOrder). ⟨AbsoluteValue(int, IntegerAddition, IntegerOrder) ` (IntegerAddition ` ⟨IntegerAddition ` ⟨f ` (IntegerAddition ` ⟨a, b⟩), GroupInv(int, IntegerAddition) ` (f ` a)⟩, GroupInv(int, IntegerAddition) ` (f ` b)⟩), L⟩ ∈ IntegerOrder; m ∈ Nonnegative(int, IntegerAddition, IntegerOrder); n ∈ PositiveSet(int, IntegerAddition, IntegerOrder) |] ==> ⟨TheNeutralElement(int, IntegerAddition), L⟩ ∈ IntegerOrder
[| f ∈ int -> int; ∀a∈PositiveSet(int, IntegerAddition, IntegerOrder). ∀b∈PositiveSet(int, IntegerAddition, IntegerOrder). ⟨AbsoluteValue(int, IntegerAddition, IntegerOrder) ` (IntegerAddition ` ⟨IntegerAddition ` ⟨f ` (IntegerAddition ` ⟨a, b⟩), GroupInv(int, IntegerAddition) ` (f ` a)⟩, GroupInv(int, IntegerAddition) ` (f ` b)⟩), L⟩ ∈ IntegerOrder; m ∈ Nonnegative(int, IntegerAddition, IntegerOrder); n ∈ PositiveSet(int, IntegerAddition, IntegerOrder) |] ==> ⟨AbsoluteValue(int, IntegerAddition, IntegerOrder) ` (IntegerAddition ` ⟨IntegerAddition ` ⟨f ` (IntegerAddition ` ⟨m, n⟩), GroupInv(int, IntegerAddition) ` (f ` m)⟩, GroupInv(int, IntegerAddition) ` (f ` n)⟩), IntegerAddition ` ⟨L, AbsoluteValue(int, IntegerAddition, IntegerOrder) ` (f ` TheNeutralElement(int, IntegerAddition))⟩⟩ ∈ IntegerOrder
lemma Int_ZF_2_1_L21:
[| f ∈ int -> int; ∀a∈Nonnegative(int, IntegerAddition, IntegerOrder). ∀b∈PositiveSet(int, IntegerAddition, IntegerOrder). ⟨AbsoluteValue(int, IntegerAddition, IntegerOrder) ` (IntegerAddition ` ⟨IntegerAddition ` ⟨f ` (IntegerAddition ` ⟨a, b⟩), GroupInv(int, IntegerAddition) ` (f ` a)⟩, GroupInv(int, IntegerAddition) ` (f ` b)⟩), L⟩ ∈ IntegerOrder; n ∈ Nonnegative(int, IntegerAddition, IntegerOrder); m ∈ Nonnegative(int, IntegerAddition, IntegerOrder) |] ==> ⟨AbsoluteValue(int, IntegerAddition, IntegerOrder) ` (IntegerAddition ` ⟨IntegerAddition ` ⟨f ` (IntegerAddition ` ⟨m, n⟩), GroupInv(int, IntegerAddition) ` (f ` m)⟩, GroupInv(int, IntegerAddition) ` (f ` n)⟩), IntegerAddition ` ⟨L, AbsoluteValue(int, IntegerAddition, IntegerOrder) ` (f ` TheNeutralElement(int, IntegerAddition))⟩⟩ ∈ IntegerOrder
lemma Int_ZF_2_1_L22:
[| f ∈ int -> int; ∀a∈PositiveSet(int, IntegerAddition, IntegerOrder). ∀b∈PositiveSet(int, IntegerAddition, IntegerOrder). ⟨AbsoluteValue(int, IntegerAddition, IntegerOrder) ` (IntegerAddition ` ⟨IntegerAddition ` ⟨f ` (IntegerAddition ` ⟨a, b⟩), GroupInv(int, IntegerAddition) ` (f ` a)⟩, GroupInv(int, IntegerAddition) ` (f ` b)⟩), L⟩ ∈ IntegerOrder |] ==> ∃M. ∀m∈Nonnegative(int, IntegerAddition, IntegerOrder). ∀n∈Nonnegative(int, IntegerAddition, IntegerOrder). ⟨AbsoluteValue(int, IntegerAddition, IntegerOrder) ` (IntegerAddition ` ⟨IntegerAddition ` ⟨f ` (IntegerAddition ` ⟨m, n⟩), GroupInv(int, IntegerAddition) ` (f ` m)⟩, GroupInv(int, IntegerAddition) ` (f ` n)⟩), M⟩ ∈ IntegerOrder
lemma Int_ZF_2_1_L23:
[| f ∈ int -> int; ∀a∈PositiveSet(int, IntegerAddition, IntegerOrder). ∀b∈PositiveSet(int, IntegerAddition, IntegerOrder). ⟨AbsoluteValue(int, IntegerAddition, IntegerOrder) ` (IntegerAddition ` ⟨IntegerAddition ` ⟨f ` (IntegerAddition ` ⟨a, b⟩), GroupInv(int, IntegerAddition) ` (f ` a)⟩, GroupInv(int, IntegerAddition) ` (f ` b)⟩), L⟩ ∈ IntegerOrder; ∀x∈int. GroupInv(int, IntegerAddition) ` (f ` (GroupInv(int, IntegerAddition) ` x)) = f ` x |] ==> f ∈ AlmostHoms(int, IntegerAddition)
lemma Int_ZF_2_1_L24:
[| f ∈ PositiveSet(int, IntegerAddition, IntegerOrder) -> int; ∀a∈PositiveSet(int, IntegerAddition, IntegerOrder). ∀b∈PositiveSet(int, IntegerAddition, IntegerOrder). ⟨AbsoluteValue(int, IntegerAddition, IntegerOrder) ` (IntegerAddition ` ⟨IntegerAddition ` ⟨f ` (IntegerAddition ` ⟨a, b⟩), GroupInv(int, IntegerAddition) ` (f ` a)⟩, GroupInv(int, IntegerAddition) ` (f ` b)⟩), L⟩ ∈ IntegerOrder |] ==> OddExtension(int, IntegerAddition, IntegerOrder, f) ∈ AlmostHoms(int, IntegerAddition)
lemma Int_ZF_2_1_L25:
[| f ∈ int -> int; m ∈ int; n ∈ int |] ==> IntegerAddition ` ⟨IntegerAddition ` ⟨f ` (IntegerAddition ` ⟨m, GroupInv(int, IntegerAddition) ` n⟩), GroupInv(int, IntegerAddition) ` (f ` m)⟩, GroupInv(int, IntegerAddition) ` (f ` (GroupInv(int, IntegerAddition) ` n))⟩ ∈ int
[| f ∈ int -> int; m ∈ int; n ∈ int |] ==> IntegerAddition ` ⟨IntegerAddition ` ⟨f ` (IntegerAddition ` ⟨n, GroupInv(int, IntegerAddition) ` n⟩), GroupInv(int, IntegerAddition) ` (f ` n)⟩, GroupInv(int, IntegerAddition) ` (f ` (GroupInv(int, IntegerAddition) ` n))⟩ ∈ int
[| f ∈ int -> int; m ∈ int; n ∈ int |] ==> GroupInv(int, IntegerAddition) ` (IntegerAddition ` ⟨IntegerAddition ` ⟨f ` (IntegerAddition ` ⟨n, GroupInv(int, IntegerAddition) ` n⟩), GroupInv(int, IntegerAddition) ` (f ` n)⟩, GroupInv(int, IntegerAddition) ` (f ` (GroupInv(int, IntegerAddition) ` n))⟩) ∈ int
[| f ∈ int -> int; m ∈ int; n ∈ int |] ==> f ` TheNeutralElement(int, IntegerAddition) ∈ int
[| f ∈ int -> int; m ∈ int; n ∈ int |] ==> IntegerAddition ` ⟨IntegerAddition ` ⟨IntegerAddition ` ⟨IntegerAddition ` ⟨f ` (IntegerAddition ` ⟨m, GroupInv(int, IntegerAddition) ` n⟩), GroupInv(int, IntegerAddition) ` (f ` m)⟩, GroupInv(int, IntegerAddition) ` (f ` (GroupInv(int, IntegerAddition) ` n))⟩, GroupInv(int, IntegerAddition) ` (IntegerAddition ` ⟨IntegerAddition ` ⟨f ` (IntegerAddition ` ⟨n, GroupInv(int, IntegerAddition) ` n⟩), GroupInv(int, IntegerAddition) ` (f ` n)⟩, GroupInv(int, IntegerAddition) ` (f ` (GroupInv(int, IntegerAddition) ` n))⟩)⟩, f ` TheNeutralElement(int, IntegerAddition)⟩ ∈ int
lemma Int_ZF_2_1_L26:
[| f ∈ int -> int; m ∈ int; n ∈ int |] ==> f ` (IntegerAddition ` ⟨m, GroupInv(int, IntegerAddition) ` n⟩) = IntegerAddition ` ⟨IntegerAddition ` ⟨IntegerAddition ` ⟨IntegerAddition ` ⟨IntegerAddition ` ⟨IntegerAddition ` ⟨f ` (IntegerAddition ` ⟨m, GroupInv(int, IntegerAddition) ` n⟩), GroupInv(int, IntegerAddition) ` (f ` m)⟩, GroupInv(int, IntegerAddition) ` (f ` (GroupInv(int, IntegerAddition) ` n))⟩, GroupInv(int, IntegerAddition) ` (IntegerAddition ` ⟨IntegerAddition ` ⟨f ` (IntegerAddition ` ⟨n, GroupInv(int, IntegerAddition) ` n⟩), GroupInv(int, IntegerAddition) ` (f ` n)⟩, GroupInv(int, IntegerAddition) ` (f ` (GroupInv(int, IntegerAddition) ` n))⟩)⟩, f ` TheNeutralElement(int, IntegerAddition)⟩, f ` m⟩, GroupInv(int, IntegerAddition) ` (f ` n)⟩
[| f ∈ int -> int; m ∈ int; n ∈ int |] ==> f ` (IntegerAddition ` ⟨m, GroupInv(int, IntegerAddition) ` n⟩) = IntegerAddition ` ⟨IntegerAddition ` ⟨IntegerAddition ` ⟨IntegerAddition ` ⟨IntegerAddition ` ⟨f ` (IntegerAddition ` ⟨m, GroupInv(int, IntegerAddition) ` n⟩), GroupInv(int, IntegerAddition) ` (f ` m)⟩, GroupInv(int, IntegerAddition) ` (f ` (GroupInv(int, IntegerAddition) ` n))⟩, GroupInv(int, IntegerAddition) ` (IntegerAddition ` ⟨IntegerAddition ` ⟨f ` (IntegerAddition ` ⟨n, GroupInv(int, IntegerAddition) ` n⟩), GroupInv(int, IntegerAddition) ` (f ` n)⟩, GroupInv(int, IntegerAddition) ` (f ` (GroupInv(int, IntegerAddition) ` n))⟩)⟩, f ` TheNeutralElement(int, IntegerAddition)⟩, IntegerAddition ` ⟨f ` m, GroupInv(int, IntegerAddition) ` (f ` n)⟩⟩
[| f ∈ int -> int; m ∈ int; n ∈ int |] ==> IntegerAddition ` ⟨f ` (IntegerAddition ` ⟨m, GroupInv(int, IntegerAddition) ` n⟩), IntegerAddition ` ⟨f ` n, GroupInv(int, IntegerAddition) ` (IntegerAddition ` ⟨IntegerAddition ` ⟨IntegerAddition ` ⟨IntegerAddition ` ⟨f ` (IntegerAddition ` ⟨m, GroupInv(int, IntegerAddition) ` n⟩), GroupInv(int, IntegerAddition) ` (f ` m)⟩, GroupInv(int, IntegerAddition) ` (f ` (GroupInv(int, IntegerAddition) ` n))⟩, GroupInv(int, IntegerAddition) ` (IntegerAddition ` ⟨IntegerAddition ` ⟨f ` (IntegerAddition ` ⟨n, GroupInv(int, IntegerAddition) ` n⟩), GroupInv(int, IntegerAddition) ` (f ` n)⟩, GroupInv(int, IntegerAddition) ` (f ` (GroupInv(int, IntegerAddition) ` n))⟩)⟩, f ` TheNeutralElement(int, IntegerAddition)⟩)⟩⟩ = f ` m
lemma Int_ZF_2_1_L26A:
[| f ∈ int -> int; m ∈ int; n ∈ int; k ∈ int |] ==> IntegerAddition ` ⟨f ` (IntegerAddition ` ⟨IntegerAddition ` ⟨m, GroupInv(int, IntegerAddition) ` n⟩, GroupInv(int, IntegerAddition) ` k⟩), GroupInv(int, IntegerAddition) ` (IntegerAddition ` ⟨IntegerAddition ` ⟨f ` m, GroupInv(int, IntegerAddition) ` (f ` n)⟩, GroupInv(int, IntegerAddition) ` (f ` k)⟩)⟩ = IntegerAddition ` ⟨IntegerAddition ` ⟨IntegerAddition ` ⟨IntegerAddition ` ⟨IntegerAddition ` ⟨f ` (IntegerAddition ` ⟨IntegerAddition ` ⟨m, GroupInv(int, IntegerAddition) ` n⟩, GroupInv(int, IntegerAddition) ` k⟩), GroupInv(int, IntegerAddition) ` (f ` (IntegerAddition ` ⟨m, GroupInv(int, IntegerAddition) ` n⟩))⟩, GroupInv(int, IntegerAddition) ` (f ` (GroupInv(int, IntegerAddition) ` k))⟩, GroupInv(int, IntegerAddition) ` (IntegerAddition ` ⟨IntegerAddition ` ⟨f ` (IntegerAddition ` ⟨k, GroupInv(int, IntegerAddition) ` k⟩), GroupInv(int, IntegerAddition) ` (f ` k)⟩, GroupInv(int, IntegerAddition) ` (f ` (GroupInv(int, IntegerAddition) ` k))⟩)⟩, f ` TheNeutralElement(int, IntegerAddition)⟩, IntegerAddition ` ⟨IntegerAddition ` ⟨IntegerAddition ` ⟨IntegerAddition ` ⟨f ` (IntegerAddition ` ⟨m, GroupInv(int, IntegerAddition) ` n⟩), GroupInv(int, IntegerAddition) ` (f ` m)⟩, GroupInv(int, IntegerAddition) ` (f ` (GroupInv(int, IntegerAddition) ` n))⟩, GroupInv(int, IntegerAddition) ` (IntegerAddition ` ⟨IntegerAddition ` ⟨f ` (IntegerAddition ` ⟨n, GroupInv(int, IntegerAddition) ` n⟩), GroupInv(int, IntegerAddition) ` (f ` n)⟩, GroupInv(int, IntegerAddition) ` (f ` (GroupInv(int, IntegerAddition) ` n))⟩)⟩, f ` TheNeutralElement(int, IntegerAddition)⟩⟩
lemma Int_ZF_2_1_L27:
s ∈ AlmostHoms(int, IntegerAddition) ==> ∃L∈int. ∀m∈int. ∀n∈int. ⟨AbsoluteValue(int, IntegerAddition, IntegerOrder) ` (IntegerAddition ` ⟨IntegerAddition ` ⟨IntegerAddition ` ⟨IntegerAddition ` ⟨s ` (IntegerAddition ` ⟨m, GroupInv(int, IntegerAddition) ` n⟩), GroupInv(int, IntegerAddition) ` (s ` m)⟩, GroupInv(int, IntegerAddition) ` (s ` (GroupInv(int, IntegerAddition) ` n))⟩, GroupInv(int, IntegerAddition) ` (IntegerAddition ` ⟨IntegerAddition ` ⟨s ` (IntegerAddition ` ⟨n, GroupInv(int, IntegerAddition) ` n⟩), GroupInv(int, IntegerAddition) ` (s ` n)⟩, GroupInv(int, IntegerAddition) ` (s ` (GroupInv(int, IntegerAddition) ` n))⟩)⟩, s ` TheNeutralElement(int, IntegerAddition)⟩), L⟩ ∈ IntegerOrder
lemma Int_ZF_2_1_L28:
s ∈ AlmostHoms(int, IntegerAddition) ==> ∃M∈int. ∀m∈int. ⟨s ` m, IntegerAddition ` ⟨s ` (IntegerAddition ` ⟨m, GroupInv(int, IntegerAddition) ` TheNeutralElement(int, IntegerMultiplication)⟩), M⟩⟩ ∈ IntegerOrder
lemma Int_ZF_2_1_L29:
s ∈ AlmostHoms(int, IntegerAddition) ==> ∃M∈int. ∀m∈int. ∀n∈int. ∀k∈int. ⟨AbsoluteValue(int, IntegerAddition, IntegerOrder) ` (IntegerAddition ` ⟨s ` (IntegerAddition ` ⟨IntegerAddition ` ⟨m, GroupInv(int, IntegerAddition) ` n⟩, GroupInv(int, IntegerAddition) ` k⟩), GroupInv(int, IntegerAddition) ` (IntegerAddition ` ⟨IntegerAddition ` ⟨s ` m, GroupInv(int, IntegerAddition) ` (s ` n)⟩, GroupInv(int, IntegerAddition) ` (s ` k)⟩)⟩), M⟩ ∈ IntegerOrder
lemma Int_ZF_2_1_L30:
s ∈ AlmostHoms(int, IntegerAddition) ==> ∃M∈int. ∀m∈int. ∀n∈int. ∀k∈int. ⟨s ` (IntegerAddition ` ⟨IntegerAddition ` ⟨m, GroupInv(int, IntegerAddition) ` n⟩, GroupInv(int, IntegerAddition) ` k⟩), IntegerAddition ` ⟨IntegerAddition ` ⟨IntegerAddition ` ⟨s ` m, GroupInv(int, IntegerAddition) ` (s ` n)⟩, GroupInv(int, IntegerAddition) ` (s ` k)⟩, M⟩⟩ ∈ IntegerOrder
s ∈ AlmostHoms(int, IntegerAddition) ==> ∃K∈int. ∀m∈int. ∀n∈int. ∀k∈int. ⟨IntegerAddition ` ⟨IntegerAddition ` ⟨IntegerAddition ` ⟨s ` m, GroupInv(int, IntegerAddition) ` (s ` n)⟩, GroupInv(int, IntegerAddition) ` (s ` k)⟩, K⟩, s ` (IntegerAddition ` ⟨IntegerAddition ` ⟨m, GroupInv(int, IntegerAddition) ` n⟩, GroupInv(int, IntegerAddition) ` k⟩)⟩ ∈ IntegerOrder
lemma Int_ZF_2_1_L31:
[| s ∈ AlmostHoms(int, IntegerAddition); r ∈ AlmostHoms(int, IntegerAddition); ∀m∈PositiveSet(int, IntegerAddition, IntegerOrder). ⟨AbsoluteValue(int, IntegerAddition, IntegerOrder) ` (IntegerAddition ` ⟨s ` m, GroupInv(int, IntegerAddition) ` (r ` m)⟩), L⟩ ∈ IntegerOrder |] ==> ⟨s, r⟩ ∈ QuotientGroupRel (AlmostHoms(int, IntegerAddition), AlHomOp1(int, IntegerAddition), FinRangeFunctions(int, int))
lemma Int_ZF_2_1_L32:
[| s ∈ AlmostHoms(int, IntegerAddition); M ∈ int; ∀m∈PositiveSet(int, IntegerAddition, IntegerOrder). ⟨m, s ` m⟩ ∈ IntegerOrder ∧ ⟨s ` m, IntegerAddition ` ⟨m, M⟩⟩ ∈ IntegerOrder |] ==> ⟨s, id(int)⟩ ∈ QuotientGroupRel (AlmostHoms(int, IntegerAddition), AlHomOp1(int, IntegerAddition), FinRangeFunctions(int, int))
lemma Int_ZF_2_1_L33:
[| s ∈ AlmostHoms(int, IntegerAddition); c ∈ int; r = {⟨m, IntegerAddition ` ⟨s ` m, c⟩⟩ . m ∈ int} |] ==> ∀m∈int. r ` m = IntegerAddition ` ⟨s ` m, c⟩
[| s ∈ AlmostHoms(int, IntegerAddition); c ∈ int; r = {⟨m, IntegerAddition ` ⟨s ` m, c⟩⟩ . m ∈ int} |] ==> r ∈ AlmostHoms(int, IntegerAddition)
[| s ∈ AlmostHoms(int, IntegerAddition); c ∈ int; r = {⟨m, IntegerAddition ` ⟨s ` m, c⟩⟩ . m ∈ int} |] ==> ⟨s, r⟩ ∈ QuotientGroupRel (AlmostHoms(int, IntegerAddition), AlHomOp1(int, IntegerAddition), FinRangeFunctions(int, int))
lemma Int_ZF_2_2_L1:
[| f ∈ int -> int; p ∈ int; q ∈ int |] ==> ⟨AbsoluteValue(int, IntegerAddition, IntegerOrder) ` (IntegerAddition ` ⟨f ` (IntegerMultiplication ` ⟨IntegerAddition ` ⟨p, TheNeutralElement(int, IntegerMultiplication)⟩, q⟩), GroupInv(int, IntegerAddition) ` (IntegerMultiplication ` ⟨IntegerAddition ` ⟨p, TheNeutralElement(int, IntegerMultiplication)⟩, f ` q⟩)⟩), IntegerAddition ` ⟨AbsoluteValue(int, IntegerAddition, IntegerOrder) ` (IntegerAddition ` ⟨IntegerAddition ` ⟨f ` (IntegerAddition ` ⟨IntegerMultiplication ` ⟨p, q⟩, q⟩), GroupInv(int, IntegerAddition) ` (f ` (IntegerMultiplication ` ⟨p, q⟩))⟩, GroupInv(int, IntegerAddition) ` (f ` q)⟩), AbsoluteValue(int, IntegerAddition, IntegerOrder) ` (IntegerAddition ` ⟨f ` (IntegerMultiplication ` ⟨p, q⟩), GroupInv(int, IntegerAddition) ` (IntegerMultiplication ` ⟨p, f ` q⟩)⟩)⟩⟩ ∈ IntegerOrder
[| f ∈ int -> int; p ∈ int; q ∈ int |] ==> ⟨AbsoluteValue(int, IntegerAddition, IntegerOrder) ` (IntegerAddition ` ⟨f ` (IntegerMultiplication ` ⟨IntegerAddition ` ⟨p, GroupInv(int, IntegerAddition) ` TheNeutralElement(int, IntegerMultiplication)⟩, q⟩), GroupInv(int, IntegerAddition) ` (IntegerMultiplication ` ⟨IntegerAddition ` ⟨p, GroupInv(int, IntegerAddition) ` TheNeutralElement(int, IntegerMultiplication)⟩, f ` q⟩)⟩), IntegerAddition ` ⟨AbsoluteValue(int, IntegerAddition, IntegerOrder) ` (IntegerAddition ` ⟨IntegerAddition ` ⟨f ` (IntegerAddition ` ⟨IntegerMultiplication ` ⟨IntegerAddition ` ⟨p, GroupInv(int, IntegerAddition) ` TheNeutralElement(int, IntegerMultiplication)⟩, q⟩, q⟩), GroupInv(int, IntegerAddition) ` (f ` (IntegerMultiplication ` ⟨IntegerAddition ` ⟨p, GroupInv(int, IntegerAddition) ` TheNeutralElement(int, IntegerMultiplication)⟩, q⟩))⟩, GroupInv(int, IntegerAddition) ` (f ` q)⟩), AbsoluteValue(int, IntegerAddition, IntegerOrder) ` (IntegerAddition ` ⟨f ` (IntegerMultiplication ` ⟨p, q⟩), GroupInv(int, IntegerAddition) ` (IntegerMultiplication ` ⟨p, f ` q⟩)⟩)⟩⟩ ∈ IntegerOrder
lemma Int_ZF_2_2_L2:
[| f ∈ AlmostHoms(int, IntegerAddition); ⟨TheNeutralElement(int, IntegerAddition), p⟩ ∈ IntegerOrder; q ∈ int; ⟨AbsoluteValue(int, IntegerAddition, IntegerOrder) ` (IntegerAddition ` ⟨f ` (IntegerMultiplication ` ⟨p, q⟩), GroupInv(int, IntegerAddition) ` (IntegerMultiplication ` ⟨p, f ` q⟩)⟩), IntegerMultiplication ` ⟨IntegerAddition ` ⟨AbsoluteValue(int, IntegerAddition, IntegerOrder) ` p, TheNeutralElement(int, IntegerMultiplication)⟩, Maximum (IntegerOrder, {AbsoluteValue(int, IntegerAddition, IntegerOrder) ` (IntegerAddition ` ⟨IntegerAddition ` ⟨f ` (IntegerAddition ` ⟨m, n⟩), GroupInv(int, IntegerAddition) ` (f ` m)⟩, GroupInv(int, IntegerAddition) ` (f ` n)⟩) . ⟨m,n⟩ ∈ int × int})⟩⟩ ∈ IntegerOrder |] ==> ⟨AbsoluteValue(int, IntegerAddition, IntegerOrder) ` (IntegerAddition ` ⟨f ` (IntegerMultiplication ` ⟨IntegerAddition ` ⟨p, TheNeutralElement(int, IntegerMultiplication)⟩, q⟩), GroupInv(int, IntegerAddition) ` (IntegerMultiplication ` ⟨IntegerAddition ` ⟨p, TheNeutralElement(int, IntegerMultiplication)⟩, f ` q⟩)⟩), IntegerMultiplication ` ⟨IntegerAddition ` ⟨AbsoluteValue(int, IntegerAddition, IntegerOrder) ` (IntegerAddition ` ⟨p, TheNeutralElement(int, IntegerMultiplication)⟩), TheNeutralElement(int, IntegerMultiplication)⟩, Maximum (IntegerOrder, {AbsoluteValue(int, IntegerAddition, IntegerOrder) ` (IntegerAddition ` ⟨IntegerAddition ` ⟨f ` (IntegerAddition ` ⟨m, n⟩), GroupInv(int, IntegerAddition) ` (f ` m)⟩, GroupInv(int, IntegerAddition) ` (f ` n)⟩) . ⟨m,n⟩ ∈ int × int})⟩⟩ ∈ IntegerOrder
lemma Int_ZF_2_2_L3:
[| f ∈ AlmostHoms(int, IntegerAddition); ⟨p, TheNeutralElement(int, IntegerAddition)⟩ ∈ IntegerOrder; q ∈ int; ⟨AbsoluteValue(int, IntegerAddition, IntegerOrder) ` (IntegerAddition ` ⟨f ` (IntegerMultiplication ` ⟨p, q⟩), GroupInv(int, IntegerAddition) ` (IntegerMultiplication ` ⟨p, f ` q⟩)⟩), IntegerMultiplication ` ⟨IntegerAddition ` ⟨AbsoluteValue(int, IntegerAddition, IntegerOrder) ` p, TheNeutralElement(int, IntegerMultiplication)⟩, Maximum (IntegerOrder, {AbsoluteValue(int, IntegerAddition, IntegerOrder) ` (IntegerAddition ` ⟨IntegerAddition ` ⟨f ` (IntegerAddition ` ⟨m, n⟩), GroupInv(int, IntegerAddition) ` (f ` m)⟩, GroupInv(int, IntegerAddition) ` (f ` n)⟩) . ⟨m,n⟩ ∈ int × int})⟩⟩ ∈ IntegerOrder |] ==> ⟨AbsoluteValue(int, IntegerAddition, IntegerOrder) ` (IntegerAddition ` ⟨f ` (IntegerMultiplication ` ⟨IntegerAddition ` ⟨p, GroupInv(int, IntegerAddition) ` TheNeutralElement(int, IntegerMultiplication)⟩, q⟩), GroupInv(int, IntegerAddition) ` (IntegerMultiplication ` ⟨IntegerAddition ` ⟨p, GroupInv(int, IntegerAddition) ` TheNeutralElement(int, IntegerMultiplication)⟩, f ` q⟩)⟩), IntegerMultiplication ` ⟨IntegerAddition ` ⟨AbsoluteValue(int, IntegerAddition, IntegerOrder) ` (IntegerAddition ` ⟨p, GroupInv(int, IntegerAddition) ` TheNeutralElement(int, IntegerMultiplication)⟩), TheNeutralElement(int, IntegerMultiplication)⟩, Maximum (IntegerOrder, {AbsoluteValue(int, IntegerAddition, IntegerOrder) ` (IntegerAddition ` ⟨IntegerAddition ` ⟨f ` (IntegerAddition ` ⟨m, n⟩), GroupInv(int, IntegerAddition) ` (f ` m)⟩, GroupInv(int, IntegerAddition) ` (f ` n)⟩) . ⟨m,n⟩ ∈ int × int})⟩⟩ ∈ IntegerOrder
lemma Int_ZF_2_2_L4:
[| f ∈ AlmostHoms(int, IntegerAddition); p ∈ int; q ∈ int |] ==> ⟨AbsoluteValue(int, IntegerAddition, IntegerOrder) ` (IntegerAddition ` ⟨f ` (IntegerMultiplication ` ⟨p, q⟩), GroupInv(int, IntegerAddition) ` (IntegerMultiplication ` ⟨p, f ` q⟩)⟩), IntegerMultiplication ` ⟨IntegerAddition ` ⟨AbsoluteValue(int, IntegerAddition, IntegerOrder) ` p, TheNeutralElement(int, IntegerMultiplication)⟩, Maximum (IntegerOrder, {AbsoluteValue(int, IntegerAddition, IntegerOrder) ` (IntegerAddition ` ⟨IntegerAddition ` ⟨f ` (IntegerAddition ` ⟨m, n⟩), GroupInv(int, IntegerAddition) ` (f ` m)⟩, GroupInv(int, IntegerAddition) ` (f ` n)⟩) . ⟨m,n⟩ ∈ int × int})⟩⟩ ∈ IntegerOrder
lemma Arthan_Lem_7:
[| f ∈ AlmostHoms(int, IntegerAddition); p ∈ int; q ∈ int |] ==> ⟨AbsoluteValue(int, IntegerAddition, IntegerOrder) ` (IntegerAddition ` ⟨IntegerMultiplication ` ⟨q, f ` p⟩, GroupInv(int, IntegerAddition) ` (IntegerMultiplication ` ⟨p, f ` q⟩)⟩), IntegerMultiplication ` ⟨IntegerAddition ` ⟨IntegerAddition ` ⟨AbsoluteValue(int, IntegerAddition, IntegerOrder) ` p, AbsoluteValue(int, IntegerAddition, IntegerOrder) ` q⟩, IntegerAddition ` ⟨TheNeutralElement(int, IntegerMultiplication), TheNeutralElement(int, IntegerMultiplication)⟩⟩, Maximum (IntegerOrder, {AbsoluteValue(int, IntegerAddition, IntegerOrder) ` (IntegerAddition ` ⟨IntegerAddition ` ⟨f ` (IntegerAddition ` ⟨m, n⟩), GroupInv(int, IntegerAddition) ` (f ` m)⟩, GroupInv(int, IntegerAddition) ` (f ` n)⟩) . ⟨m,n⟩ ∈ int × int})⟩⟩ ∈ IntegerOrder
lemma Arthan_Lem_8:
f ∈ AlmostHoms(int, IntegerAddition) ==> ∃A B. A ∈ int ∧ B ∈ int ∧ (∀p∈int. ⟨AbsoluteValue(int, IntegerAddition, IntegerOrder) ` (f ` p), IntegerAddition ` ⟨IntegerMultiplication ` ⟨A, AbsoluteValue(int, IntegerAddition, IntegerOrder) ` p⟩, B⟩⟩ ∈ IntegerOrder)
theorem Arthan_Th_9:
[| f ∈ AlmostHoms(int, IntegerAddition); g ∈ AlmostHoms(int, IntegerAddition) |] ==> ⟨AlHomOp2(int, IntegerAddition) ` ⟨f, g⟩, AlHomOp2(int, IntegerAddition) ` ⟨g, f⟩⟩ ∈ QuotientGroupRel (AlmostHoms(int, IntegerAddition), AlHomOp1(int, IntegerAddition), FinRangeFunctions(int, int))
lemma Int_ZF_2_3_L1:
f ∈ {s ∈ AlmostHoms(int, IntegerAddition) . s `` PositiveSet(int, IntegerAddition, IntegerOrder) ∩ PositiveSet(int, IntegerAddition, IntegerOrder) ∉ Fin(int)} ==> f ∈ int -> int
lemma Int_ZF_2_3_L1A:
[| f ∈ {s ∈ AlmostHoms(int, IntegerAddition) . s `` PositiveSet(int, IntegerAddition, IntegerOrder) ∩ PositiveSet(int, IntegerAddition, IntegerOrder) ∉ Fin(int)}; ∃n∈f `` PositiveSet(int, IntegerAddition, IntegerOrder) ∩ PositiveSet(int, IntegerAddition, IntegerOrder). ⟨a, n⟩ ∈ IntegerOrder |] ==> ∃M∈PositiveSet(int, IntegerAddition, IntegerOrder). ⟨a, f ` M⟩ ∈ IntegerOrder
lemma Arthan_Lem_3:
[| f ∈ {s ∈ AlmostHoms(int, IntegerAddition) . s `` PositiveSet(int, IntegerAddition, IntegerOrder) ∩ PositiveSet(int, IntegerAddition, IntegerOrder) ∉ Fin(int)}; D ∈ PositiveSet(int, IntegerAddition, IntegerOrder) |] ==> ∃M∈PositiveSet(int, IntegerAddition, IntegerOrder). ∀m∈PositiveSet(int, IntegerAddition, IntegerOrder). ⟨IntegerMultiplication ` ⟨IntegerAddition ` ⟨m, TheNeutralElement(int, IntegerMultiplication)⟩, D⟩, f ` (IntegerMultiplication ` ⟨m, M⟩)⟩ ∈ IntegerOrder
corollary Arthan_L_3_spec:
f ∈ {s ∈ AlmostHoms(int, IntegerAddition) . s `` PositiveSet(int, IntegerAddition, IntegerOrder) ∩ PositiveSet(int, IntegerAddition, IntegerOrder) ∉ Fin(int)} ==> ∃M∈PositiveSet(int, IntegerAddition, IntegerOrder). ∀n∈PositiveSet(int, IntegerAddition, IntegerOrder). ⟨IntegerAddition ` ⟨n, TheNeutralElement(int, IntegerMultiplication)⟩, f ` (IntegerMultiplication ` ⟨n, M⟩)⟩ ∈ IntegerOrder
lemma Int_ZF_2_3_L1B:
f ∈ FinRangeFunctions(int, int) ==> f ∈ AlmostHoms(int, IntegerAddition)
f ∈ FinRangeFunctions(int, int) ==> f ∉ {s ∈ AlmostHoms(int, IntegerAddition) . s `` PositiveSet(int, IntegerAddition, IntegerOrder) ∩ PositiveSet(int, IntegerAddition, IntegerOrder) ∉ Fin(int)}
lemma Int_ZF_2_3_L2:
[| f ∈ AlmostHoms(int, IntegerAddition); f ∉ {s ∈ AlmostHoms(int, IntegerAddition) . s `` PositiveSet(int, IntegerAddition, IntegerOrder) ∩ PositiveSet(int, IntegerAddition, IntegerOrder) ∉ Fin(int)} |] ==> IsBoundedAbove (f `` PositiveSet(int, IntegerAddition, IntegerOrder), IntegerOrder)
lemma Int_ZF_2_3_L3:
[| f ∈ AlmostHoms(int, IntegerAddition); GroupInv(int, IntegerAddition) O f ∉ {s ∈ AlmostHoms(int, IntegerAddition) . s `` PositiveSet(int, IntegerAddition, IntegerOrder) ∩ PositiveSet(int, IntegerAddition, IntegerOrder) ∉ Fin(int)} |] ==> IsBoundedBelow (f `` PositiveSet(int, IntegerAddition, IntegerOrder), IntegerOrder)
lemma Int_ZF_2_3_L4:
[| f ∈ AlmostHoms(int, IntegerAddition); m ∈ int; ∀n∈PositiveSet(int, IntegerAddition, IntegerOrder). ⟨AbsoluteValue(int, IntegerAddition, IntegerOrder) ` (f ` n), L⟩ ∈ IntegerOrder |] ==> ⟨AbsoluteValue(int, IntegerAddition, IntegerOrder) ` (f ` m), IntegerAddition ` ⟨IntegerMultiplication ` ⟨IntegerAddition ` ⟨TheNeutralElement(int, IntegerMultiplication), TheNeutralElement(int, IntegerMultiplication)⟩, Maximum (IntegerOrder, {AbsoluteValue(int, IntegerAddition, IntegerOrder) ` (IntegerAddition ` ⟨IntegerAddition ` ⟨f ` (IntegerAddition ` ⟨m, n⟩), GroupInv(int, IntegerAddition) ` (f ` m)⟩, GroupInv(int, IntegerAddition) ` (f ` n)⟩) . ⟨m,n⟩ ∈ int × int})⟩, L⟩⟩ ∈ IntegerOrder
lemma Int_ZF_2_3_L4A:
[| f ∈ AlmostHoms(int, IntegerAddition); IsBounded (f `` PositiveSet(int, IntegerAddition, IntegerOrder), IntegerOrder) |] ==> f ∈ FinRangeFunctions(int, int)
lemma Int_ZF_2_3_L4B:
[| f ∈ AlmostHoms(int, IntegerAddition); IsBoundedBelow (f `` PositiveSet(int, IntegerAddition, IntegerOrder), IntegerOrder) |] ==> f ∈ FinRangeFunctions(int, int) ∨ f ∈ {s ∈ AlmostHoms(int, IntegerAddition) . s `` PositiveSet(int, IntegerAddition, IntegerOrder) ∩ PositiveSet(int, IntegerAddition, IntegerOrder) ∉ Fin(int)}
lemma Int_ZF_2_3_L4C:
[| f ∈ AlmostHoms(int, IntegerAddition); g ∈ AlmostHoms(int, IntegerAddition); ∀n∈PositiveSet(int, IntegerAddition, IntegerOrder). ⟨f ` n, g ` n⟩ ∈ IntegerOrder |] ==> ⟨f, g⟩ ∈ QuotientGroupRel (AlmostHoms(int, IntegerAddition), AlHomOp1(int, IntegerAddition), FinRangeFunctions(int, int)) ∨ AlHomOp1(int, IntegerAddition) ` ⟨g, GroupInv(int, IntegerAddition) O f⟩ ∈ {s ∈ AlmostHoms(int, IntegerAddition) . s `` PositiveSet(int, IntegerAddition, IntegerOrder) ∩ PositiveSet(int, IntegerAddition, IntegerOrder) ∉ Fin(int)}
lemma Int_ZF_2_3_L5:
[| f ∈ {s ∈ AlmostHoms(int, IntegerAddition) . s `` PositiveSet(int, IntegerAddition, IntegerOrder) ∩ PositiveSet(int, IntegerAddition, IntegerOrder) ∉ Fin(int)}; K ∈ int |] ==> ∃N∈PositiveSet(int, IntegerAddition, IntegerOrder). ∀m. ⟨N, m⟩ ∈ IntegerOrder --> ⟨K, f ` m⟩ ∈ IntegerOrder
lemma Int_ZF_2_3_L5A:
[| f ∈ {s ∈ AlmostHoms(int, IntegerAddition) . s `` PositiveSet(int, IntegerAddition, IntegerOrder) ∩ PositiveSet(int, IntegerAddition, IntegerOrder) ∉ Fin(int)}; K ∈ int |] ==> ∃N∈PositiveSet(int, IntegerAddition, IntegerOrder). ∀m. ⟨N, m⟩ ∈ IntegerOrder --> ⟨f ` (GroupInv(int, IntegerAddition) ` m), K⟩ ∈ IntegerOrder
corollary Int_ZF_2_3_L6:
f ∈ {s ∈ AlmostHoms(int, IntegerAddition) . s `` PositiveSet(int, IntegerAddition, IntegerOrder) ∩ PositiveSet(int, IntegerAddition, IntegerOrder) ∉ Fin(int)} ==> ∃N∈PositiveSet(int, IntegerAddition, IntegerOrder). ∀m. ⟨N, m⟩ ∈ IntegerOrder --> f ` m ∈ PositiveSet(int, IntegerAddition, IntegerOrder)
corollary Int_ZF_2_3_L6A:
[| f ∈ {s ∈ AlmostHoms(int, IntegerAddition) . s `` PositiveSet(int, IntegerAddition, IntegerOrder) ∩ PositiveSet(int, IntegerAddition, IntegerOrder) ∉ Fin(int)}; K ∈ int |] ==> ∃N∈PositiveSet(int, IntegerAddition, IntegerOrder). ⟨K, f ` N⟩ ∈ IntegerOrder
lemma Int_ZF_2_3_L7:
[| f ∈ AlmostHoms(int, IntegerAddition); ∀K∈int. ∃n∈PositiveSet(int, IntegerAddition, IntegerOrder). ⟨K, f ` n⟩ ∈ IntegerOrder |] ==> f ∈ {s ∈ AlmostHoms(int, IntegerAddition) . s `` PositiveSet(int, IntegerAddition, IntegerOrder) ∩ PositiveSet(int, IntegerAddition, IntegerOrder) ∉ Fin(int)}
theorem Int_ZF_2_3_L8:
[| f ∈ AlmostHoms(int, IntegerAddition); f ∉ FinRangeFunctions(int, int) |] ==> (f ∈ {s ∈ AlmostHoms(int, IntegerAddition) . s `` PositiveSet(int, IntegerAddition, IntegerOrder) ∩ PositiveSet(int, IntegerAddition, IntegerOrder) ∉ Fin(int)}) Xor (GroupInv(int, IntegerAddition) O f ∈ {s ∈ AlmostHoms(int, IntegerAddition) . s `` PositiveSet(int, IntegerAddition, IntegerOrder) ∩ PositiveSet(int, IntegerAddition, IntegerOrder) ∉ Fin(int)})
theorem sum_of_pos_sls_is_pos_sl:
[| f ∈ {s ∈ AlmostHoms(int, IntegerAddition) . s `` PositiveSet(int, IntegerAddition, IntegerOrder) ∩ PositiveSet(int, IntegerAddition, IntegerOrder) ∉ Fin(int)}; g ∈ {s ∈ AlmostHoms(int, IntegerAddition) . s `` PositiveSet(int, IntegerAddition, IntegerOrder) ∩ PositiveSet(int, IntegerAddition, IntegerOrder) ∉ Fin(int)} |] ==> AlHomOp1(int, IntegerAddition) ` ⟨f, g⟩ ∈ {s ∈ AlmostHoms(int, IntegerAddition) . s `` PositiveSet(int, IntegerAddition, IntegerOrder) ∩ PositiveSet(int, IntegerAddition, IntegerOrder) ∉ Fin(int)}
theorem comp_of_pos_sls_is_pos_sl:
[| f ∈ {s ∈ AlmostHoms(int, IntegerAddition) . s `` PositiveSet(int, IntegerAddition, IntegerOrder) ∩ PositiveSet(int, IntegerAddition, IntegerOrder) ∉ Fin(int)}; g ∈ {s ∈ AlmostHoms(int, IntegerAddition) . s `` PositiveSet(int, IntegerAddition, IntegerOrder) ∩ PositiveSet(int, IntegerAddition, IntegerOrder) ∉ Fin(int)} |] ==> AlHomOp2(int, IntegerAddition) ` ⟨f, g⟩ ∈ {s ∈ AlmostHoms(int, IntegerAddition) . s `` PositiveSet(int, IntegerAddition, IntegerOrder) ∩ PositiveSet(int, IntegerAddition, IntegerOrder) ∉ Fin(int)}
lemma Int_ZF_2_3_L9:
[| f ∈ {s ∈ AlmostHoms(int, IntegerAddition) . s `` PositiveSet(int, IntegerAddition, IntegerOrder) ∩ PositiveSet(int, IntegerAddition, IntegerOrder) ∉ Fin(int)}; ⟨f, g⟩ ∈ QuotientGroupRel (AlmostHoms(int, IntegerAddition), AlHomOp1(int, IntegerAddition), FinRangeFunctions(int, int)) |] ==> g ∈ {s ∈ AlmostHoms(int, IntegerAddition) . s `` PositiveSet(int, IntegerAddition, IntegerOrder) ∩ PositiveSet(int, IntegerAddition, IntegerOrder) ∉ Fin(int)}
lemma pos_slopes_saturated:
IsSaturated
(QuotientGroupRel
(AlmostHoms(int, IntegerAddition), AlHomOp1(int, IntegerAddition),
FinRangeFunctions(int, int)),
{s ∈ AlmostHoms(int, IntegerAddition) .
s `` PositiveSet(int, IntegerAddition, IntegerOrder) ∩
PositiveSet(int, IntegerAddition, IntegerOrder) ∉
Fin(int)})
lemma Int_ZF_2_3_L10:
[| f ∈ AlmostHoms(int, IntegerAddition); g ∈ AlmostHoms(int, IntegerAddition); R = {QuotientGroupRel (AlmostHoms(int, IntegerAddition), AlHomOp1(int, IntegerAddition), FinRangeFunctions(int, int)) `` {s} . s ∈ {s ∈ AlmostHoms(int, IntegerAddition) . s `` PositiveSet(int, IntegerAddition, IntegerOrder) ∩ PositiveSet(int, IntegerAddition, IntegerOrder) ∉ Fin(int)}}; (f ∈ {s ∈ AlmostHoms(int, IntegerAddition) . s `` PositiveSet(int, IntegerAddition, IntegerOrder) ∩ PositiveSet(int, IntegerAddition, IntegerOrder) ∉ Fin(int)}) Xor (g ∈ {s ∈ AlmostHoms(int, IntegerAddition) . s `` PositiveSet(int, IntegerAddition, IntegerOrder) ∩ PositiveSet(int, IntegerAddition, IntegerOrder) ∉ Fin(int)}) |] ==> (QuotientGroupRel (AlmostHoms(int, IntegerAddition), AlHomOp1(int, IntegerAddition), FinRangeFunctions(int, int)) `` {f} ∈ R) Xor (QuotientGroupRel (AlmostHoms(int, IntegerAddition), AlHomOp1(int, IntegerAddition), FinRangeFunctions(int, int)) `` {g} ∈ R)
lemma Int_ZF_2_3_L11:
id(int) ∈
{s ∈ AlmostHoms(int, IntegerAddition) .
s `` PositiveSet(int, IntegerAddition, IntegerOrder) ∩
PositiveSet(int, IntegerAddition, IntegerOrder) ∉
Fin(int)}
lemma Int_ZF_2_3_L12:
f ∈ FinRangeFunctions(int, int) ==> ⟨id(int), f⟩ ∉ QuotientGroupRel (AlmostHoms(int, IntegerAddition), AlHomOp1(int, IntegerAddition), FinRangeFunctions(int, int))
lemma Int_ZF_2_4_L1:
[| f ∈ {s ∈ AlmostHoms(int, IntegerAddition) . s `` PositiveSet(int, IntegerAddition, IntegerOrder) ∩ PositiveSet(int, IntegerAddition, IntegerOrder) ∉ Fin(int)}; p ∈ PositiveSet(int, IntegerAddition, IntegerOrder); A = {n ∈ PositiveSet(int, IntegerAddition, IntegerOrder) . ⟨p, f ` n⟩ ∈ IntegerOrder} |] ==> A ⊆ PositiveSet(int, IntegerAddition, IntegerOrder)
[| f ∈ {s ∈ AlmostHoms(int, IntegerAddition) . s `` PositiveSet(int, IntegerAddition, IntegerOrder) ∩ PositiveSet(int, IntegerAddition, IntegerOrder) ∉ Fin(int)}; p ∈ PositiveSet(int, IntegerAddition, IntegerOrder); A = {n ∈ PositiveSet(int, IntegerAddition, IntegerOrder) . ⟨p, f ` n⟩ ∈ IntegerOrder} |] ==> A ≠ 0
[| f ∈ {s ∈ AlmostHoms(int, IntegerAddition) . s `` PositiveSet(int, IntegerAddition, IntegerOrder) ∩ PositiveSet(int, IntegerAddition, IntegerOrder) ∉ Fin(int)}; p ∈ PositiveSet(int, IntegerAddition, IntegerOrder); A = {n ∈ PositiveSet(int, IntegerAddition, IntegerOrder) . ⟨p, f ` n⟩ ∈ IntegerOrder} |] ==> Minimum (IntegerOrder, {n ∈ PositiveSet(int, IntegerAddition, IntegerOrder) . ⟨p, f ` n⟩ ∈ IntegerOrder}) ∈ A
[| f ∈ {s ∈ AlmostHoms(int, IntegerAddition) . s `` PositiveSet(int, IntegerAddition, IntegerOrder) ∩ PositiveSet(int, IntegerAddition, IntegerOrder) ∉ Fin(int)}; p ∈ PositiveSet(int, IntegerAddition, IntegerOrder); A = {n ∈ PositiveSet(int, IntegerAddition, IntegerOrder) . ⟨p, f ` n⟩ ∈ IntegerOrder} |] ==> ∀m∈A. ⟨Minimum (IntegerOrder, {n ∈ PositiveSet(int, IntegerAddition, IntegerOrder) . ⟨p, f ` n⟩ ∈ IntegerOrder}), m⟩ ∈ IntegerOrder
lemma Int_ZF_2_4_L2:
[| f ∈ {s ∈ AlmostHoms(int, IntegerAddition) . s `` PositiveSet(int, IntegerAddition, IntegerOrder) ∩ PositiveSet(int, IntegerAddition, IntegerOrder) ∉ Fin(int)}; p ∈ PositiveSet(int, IntegerAddition, IntegerOrder) |] ==> Minimum (IntegerOrder, {n ∈ PositiveSet(int, IntegerAddition, IntegerOrder) . ⟨p, f ` n⟩ ∈ IntegerOrder}) ∈ PositiveSet(int, IntegerAddition, IntegerOrder)
[| f ∈ {s ∈ AlmostHoms(int, IntegerAddition) . s `` PositiveSet(int, IntegerAddition, IntegerOrder) ∩ PositiveSet(int, IntegerAddition, IntegerOrder) ∉ Fin(int)}; p ∈ PositiveSet(int, IntegerAddition, IntegerOrder) |] ==> ⟨p, f ` Minimum (IntegerOrder, {n ∈ PositiveSet(int, IntegerAddition, IntegerOrder) . ⟨p, f ` n⟩ ∈ IntegerOrder})⟩ ∈ IntegerOrder
lemma Int_ZF_2_4_L3:
[| f ∈ {s ∈ AlmostHoms(int, IntegerAddition) . s `` PositiveSet(int, IntegerAddition, IntegerOrder) ∩ PositiveSet(int, IntegerAddition, IntegerOrder) ∉ Fin(int)}; m ∈ PositiveSet(int, IntegerAddition, IntegerOrder); p ∈ PositiveSet(int, IntegerAddition, IntegerOrder); ⟨m, f ` p⟩ ∈ IntegerOrder |] ==> ⟨Minimum (IntegerOrder, {n ∈ PositiveSet(int, IntegerAddition, IntegerOrder) . ⟨m, f ` n⟩ ∈ IntegerOrder}), p⟩ ∈ IntegerOrder
lemma Int_ZF_2_4_L4:
[| f ∈ {s ∈ AlmostHoms(int, IntegerAddition) . s `` PositiveSet(int, IntegerAddition, IntegerOrder) ∩ PositiveSet(int, IntegerAddition, IntegerOrder) ∉ Fin(int)}; m ∈ PositiveSet(int, IntegerAddition, IntegerOrder); IntegerAddition ` ⟨Minimum (IntegerOrder, {n ∈ PositiveSet(int, IntegerAddition, IntegerOrder) . ⟨m, f ` n⟩ ∈ IntegerOrder}), GroupInv(int, IntegerAddition) ` TheNeutralElement(int, IntegerMultiplication)⟩ ∈ PositiveSet(int, IntegerAddition, IntegerOrder) |] ==> ⟨f ` (IntegerAddition ` ⟨Minimum (IntegerOrder, {n ∈ PositiveSet(int, IntegerAddition, IntegerOrder) . ⟨m, f ` n⟩ ∈ IntegerOrder}), GroupInv(int, IntegerAddition) ` TheNeutralElement(int, IntegerMultiplication)⟩), m⟩ ∈ IntegerOrder
[| f ∈ {s ∈ AlmostHoms(int, IntegerAddition) . s `` PositiveSet(int, IntegerAddition, IntegerOrder) ∩ PositiveSet(int, IntegerAddition, IntegerOrder) ∉ Fin(int)}; m ∈ PositiveSet(int, IntegerAddition, IntegerOrder); IntegerAddition ` ⟨Minimum (IntegerOrder, {n ∈ PositiveSet(int, IntegerAddition, IntegerOrder) . ⟨m, f ` n⟩ ∈ IntegerOrder}), GroupInv(int, IntegerAddition) ` TheNeutralElement(int, IntegerMultiplication)⟩ ∈ PositiveSet(int, IntegerAddition, IntegerOrder) |] ==> f ` (IntegerAddition ` ⟨Minimum (IntegerOrder, {n ∈ PositiveSet(int, IntegerAddition, IntegerOrder) . ⟨m, f ` n⟩ ∈ IntegerOrder}), GroupInv(int, IntegerAddition) ` TheNeutralElement(int, IntegerMultiplication)⟩) ≠ m
lemma Int_ZF_2_4_L5:
[| f ∈ {s ∈ AlmostHoms(int, IntegerAddition) . s `` PositiveSet(int, IntegerAddition, IntegerOrder) ∩ PositiveSet(int, IntegerAddition, IntegerOrder) ∉ Fin(int)}; m ∈ PositiveSet(int, IntegerAddition, IntegerOrder); ⟨m, n⟩ ∈ IntegerOrder |] ==> ⟨Minimum (IntegerOrder, {n ∈ PositiveSet(int, IntegerAddition, IntegerOrder) . ⟨m, f ` n⟩ ∈ IntegerOrder}), Minimum (IntegerOrder, {n ∈ PositiveSet(int, IntegerAddition, IntegerOrder) . ⟨n, f ` n⟩ ∈ IntegerOrder})⟩ ∈ IntegerOrder
lemma Int_ZF_2_4_L6:
[| f ∈ {s ∈ AlmostHoms(int, IntegerAddition) . s `` PositiveSet(int, IntegerAddition, IntegerOrder) ∩ PositiveSet(int, IntegerAddition, IntegerOrder) ∉ Fin(int)}; m ∈ PositiveSet(int, IntegerAddition, IntegerOrder); n ∈ PositiveSet(int, IntegerAddition, IntegerOrder); IntegerAddition ` ⟨Minimum (IntegerOrder, {n ∈ PositiveSet(int, IntegerAddition, IntegerOrder) . ⟨m, f ` n⟩ ∈ IntegerOrder}), GroupInv(int, IntegerAddition) ` TheNeutralElement(int, IntegerMultiplication)⟩ ∈ PositiveSet(int, IntegerAddition, IntegerOrder) |] ==> IntegerAddition ` ⟨Minimum (IntegerOrder, {n ∈ PositiveSet(int, IntegerAddition, IntegerOrder) . ⟨IntegerAddition ` ⟨m, n⟩, f ` n⟩ ∈ IntegerOrder}), GroupInv(int, IntegerAddition) ` TheNeutralElement(int, IntegerMultiplication)⟩ ∈ PositiveSet(int, IntegerAddition, IntegerOrder)
lemma Int_ZF_2_4_L7:
[| f ∈ {s ∈ AlmostHoms(int, IntegerAddition) . s `` PositiveSet(int, IntegerAddition, IntegerOrder) ∩ PositiveSet(int, IntegerAddition, IntegerOrder) ∉ Fin(int)}; ∀m∈PositiveSet(int, IntegerAddition, IntegerOrder). IntegerAddition ` ⟨Minimum (IntegerOrder, {n ∈ PositiveSet(int, IntegerAddition, IntegerOrder) . ⟨m, f ` n⟩ ∈ IntegerOrder}), GroupInv(int, IntegerAddition) ` TheNeutralElement(int, IntegerMultiplication)⟩ ∈ PositiveSet(int, IntegerAddition, IntegerOrder) |] ==> ∃U∈int. ∀m∈PositiveSet(int, IntegerAddition, IntegerOrder). ∀n∈PositiveSet(int, IntegerAddition, IntegerOrder). ⟨f ` (IntegerAddition ` ⟨IntegerAddition ` ⟨Minimum (IntegerOrder, {na ∈ PositiveSet(int, IntegerAddition, IntegerOrder) . ⟨IntegerAddition ` ⟨m, n⟩, f ` na⟩ ∈ IntegerOrder}), GroupInv(int, IntegerAddition) ` Minimum (IntegerOrder, {n ∈ PositiveSet(int, IntegerAddition, IntegerOrder) . ⟨m, f ` n⟩ ∈ IntegerOrder})⟩, GroupInv(int, IntegerAddition) ` Minimum (IntegerOrder, {na ∈ PositiveSet(int, IntegerAddition, IntegerOrder) . ⟨n, f ` na⟩ ∈ IntegerOrder})⟩), U⟩ ∈ IntegerOrder
[| f ∈ {s ∈ AlmostHoms(int, IntegerAddition) . s `` PositiveSet(int, IntegerAddition, IntegerOrder) ∩ PositiveSet(int, IntegerAddition, IntegerOrder) ∉ Fin(int)}; ∀m∈PositiveSet(int, IntegerAddition, IntegerOrder). IntegerAddition ` ⟨Minimum (IntegerOrder, {n ∈ PositiveSet(int, IntegerAddition, IntegerOrder) . ⟨m, f ` n⟩ ∈ IntegerOrder}), GroupInv(int, IntegerAddition) ` TheNeutralElement(int, IntegerMultiplication)⟩ ∈ PositiveSet(int, IntegerAddition, IntegerOrder) |] ==> ∃N∈int. ∀m∈PositiveSet(int, IntegerAddition, IntegerOrder). ∀n∈PositiveSet(int, IntegerAddition, IntegerOrder). ⟨N, f ` (IntegerAddition ` ⟨IntegerAddition ` ⟨Minimum (IntegerOrder, {na ∈ PositiveSet (int, IntegerAddition, IntegerOrder) . ⟨IntegerAddition ` ⟨m, n⟩, f ` na⟩ ∈ IntegerOrder}), GroupInv(int, IntegerAddition) ` Minimum (IntegerOrder, {n ∈ PositiveSet(int, IntegerAddition, IntegerOrder) . ⟨m, f ` n⟩ ∈ IntegerOrder})⟩, GroupInv(int, IntegerAddition) ` Minimum (IntegerOrder, {na ∈ PositiveSet(int, IntegerAddition, IntegerOrder) . ⟨n, f ` na⟩ ∈ IntegerOrder})⟩)⟩ ∈ IntegerOrder
lemma Int_ZF_2_4_L8:
[| f ∈ {s ∈ AlmostHoms(int, IntegerAddition) . s `` PositiveSet(int, IntegerAddition, IntegerOrder) ∩ PositiveSet(int, IntegerAddition, IntegerOrder) ∉ Fin(int)}; ∀m∈PositiveSet(int, IntegerAddition, IntegerOrder). IntegerAddition ` ⟨Minimum (IntegerOrder, {n ∈ PositiveSet(int, IntegerAddition, IntegerOrder) . ⟨m, f ` n⟩ ∈ IntegerOrder}), GroupInv(int, IntegerAddition) ` TheNeutralElement(int, IntegerMultiplication)⟩ ∈ PositiveSet(int, IntegerAddition, IntegerOrder) |] ==> ∃M. ∀x∈PositiveSet(int, IntegerAddition, IntegerOrder) × PositiveSet(int, IntegerAddition, IntegerOrder). ⟨AbsoluteValue(int, IntegerAddition, IntegerOrder) ` (IntegerAddition ` ⟨IntegerAddition ` ⟨Minimum (IntegerOrder, {n ∈ PositiveSet(int, IntegerAddition, IntegerOrder) . ⟨IntegerAddition ` ⟨fst(x), snd(x)⟩, f ` n⟩ ∈ IntegerOrder}), GroupInv(int, IntegerAddition) ` Minimum (IntegerOrder, {n ∈ PositiveSet(int, IntegerAddition, IntegerOrder) . ⟨fst(x), f ` n⟩ ∈ IntegerOrder})⟩, GroupInv(int, IntegerAddition) ` Minimum (IntegerOrder, {n ∈ PositiveSet(int, IntegerAddition, IntegerOrder) . ⟨snd(x), f ` n⟩ ∈ IntegerOrder})⟩), M⟩ ∈ IntegerOrder
lemma Int_ZF_2_4_L9:
[| f ∈ {s ∈ AlmostHoms(int, IntegerAddition) . s `` PositiveSet(int, IntegerAddition, IntegerOrder) ∩ PositiveSet(int, IntegerAddition, IntegerOrder) ∉ Fin(int)}; g = {⟨p, Minimum (IntegerOrder, {n ∈ PositiveSet(int, IntegerAddition, IntegerOrder) . ⟨p, f ` n⟩ ∈ IntegerOrder})⟩ . p ∈ PositiveSet(int, IntegerAddition, IntegerOrder)} |] ==> g ∈ PositiveSet(int, IntegerAddition, IntegerOrder) -> PositiveSet(int, IntegerAddition, IntegerOrder)
[| f ∈ {s ∈ AlmostHoms(int, IntegerAddition) . s `` PositiveSet(int, IntegerAddition, IntegerOrder) ∩ PositiveSet(int, IntegerAddition, IntegerOrder) ∉ Fin(int)}; g = {⟨p, Minimum (IntegerOrder, {n ∈ PositiveSet(int, IntegerAddition, IntegerOrder) . ⟨p, f ` n⟩ ∈ IntegerOrder})⟩ . p ∈ PositiveSet(int, IntegerAddition, IntegerOrder)} |] ==> g ∈ PositiveSet(int, IntegerAddition, IntegerOrder) -> int
lemma Int_ZF_2_4_L10:
[| f ∈ {s ∈ AlmostHoms(int, IntegerAddition) . s `` PositiveSet(int, IntegerAddition, IntegerOrder) ∩ PositiveSet(int, IntegerAddition, IntegerOrder) ∉ Fin(int)}; g = {⟨p, Minimum (IntegerOrder, {n ∈ PositiveSet(int, IntegerAddition, IntegerOrder) . ⟨p, f ` n⟩ ∈ IntegerOrder})⟩ . p ∈ PositiveSet(int, IntegerAddition, IntegerOrder)}; p ∈ PositiveSet(int, IntegerAddition, IntegerOrder) |] ==> g ` p = Minimum (IntegerOrder, {n ∈ PositiveSet(int, IntegerAddition, IntegerOrder) . ⟨p, f ` n⟩ ∈ IntegerOrder})
lemma Int_ZF_2_4_L11:
[| f ∈ {s ∈ AlmostHoms(int, IntegerAddition) . s `` PositiveSet(int, IntegerAddition, IntegerOrder) ∩ PositiveSet(int, IntegerAddition, IntegerOrder) ∉ Fin(int)}; ∀m∈PositiveSet(int, IntegerAddition, IntegerOrder). IntegerAddition ` ⟨Minimum (IntegerOrder, {n ∈ PositiveSet(int, IntegerAddition, IntegerOrder) . ⟨m, f ` n⟩ ∈ IntegerOrder}), GroupInv(int, IntegerAddition) ` TheNeutralElement(int, IntegerMultiplication)⟩ ∈ PositiveSet(int, IntegerAddition, IntegerOrder); g = {⟨p, Minimum (IntegerOrder, {n ∈ PositiveSet(int, IntegerAddition, IntegerOrder) . ⟨p, f ` n⟩ ∈ IntegerOrder})⟩ . p ∈ PositiveSet(int, IntegerAddition, IntegerOrder)} |] ==> OddExtension(int, IntegerAddition, IntegerOrder, g) ∈ AlmostHoms(int, IntegerAddition)
lemma Int_ZF_2_4_L12:
[| f ∈ {s ∈ AlmostHoms(int, IntegerAddition) . s `` PositiveSet(int, IntegerAddition, IntegerOrder) ∩ PositiveSet(int, IntegerAddition, IntegerOrder) ∉ Fin(int)}; ∀m∈PositiveSet(int, IntegerAddition, IntegerOrder). IntegerAddition ` ⟨Minimum (IntegerOrder, {n ∈ PositiveSet(int, IntegerAddition, IntegerOrder) . ⟨m, f ` n⟩ ∈ IntegerOrder}), GroupInv(int, IntegerAddition) ` TheNeutralElement(int, IntegerMultiplication)⟩ ∈ PositiveSet(int, IntegerAddition, IntegerOrder) |] ==> ∃h∈AlmostHoms(int, IntegerAddition). ⟨AlHomOp2(int, IntegerAddition) ` ⟨f, h⟩, id(int)⟩ ∈ QuotientGroupRel (AlmostHoms(int, IntegerAddition), AlHomOp1(int, IntegerAddition), FinRangeFunctions(int, int))
theorem pos_slope_has_inv:
f ∈ {s ∈ AlmostHoms(int, IntegerAddition) . s `` PositiveSet(int, IntegerAddition, IntegerOrder) ∩ PositiveSet(int, IntegerAddition, IntegerOrder) ∉ Fin(int)} ==> ∃g∈AlmostHoms(int, IntegerAddition). ⟨f, g⟩ ∈ QuotientGroupRel (AlmostHoms(int, IntegerAddition), AlHomOp1(int, IntegerAddition), FinRangeFunctions(int, int)) ∧ (∃h∈AlmostHoms(int, IntegerAddition). ⟨AlHomOp2(int, IntegerAddition) ` ⟨g, h⟩, id(int)⟩ ∈ QuotientGroupRel (AlmostHoms(int, IntegerAddition), AlHomOp1(int, IntegerAddition), FinRangeFunctions(int, int)))
lemma Int_ZF_2_5_L1:
m ∈ int ==> ∀n∈int. {⟨n, IntegerMultiplication ` ⟨m, n⟩⟩ . n ∈ int} ` n = IntegerMultiplication ` ⟨m, n⟩
m ∈ int ==> {⟨n, IntegerMultiplication ` ⟨m, n⟩⟩ . n ∈ int} ∈ AlmostHoms(int, IntegerAddition)
lemma Int_ZF_2_5_L2:
f ∈ AlmostHoms(int, IntegerAddition) ==> ∃m∈int. ∃g∈AlmostHoms(int, IntegerAddition). ⟨{⟨n, IntegerMultiplication ` ⟨m, n⟩⟩ . n ∈ int}, g⟩ ∈ QuotientGroupRel (AlmostHoms(int, IntegerAddition), AlHomOp1(int, IntegerAddition), FinRangeFunctions(int, int)) ∧ (⟨f, g⟩ ∈ QuotientGroupRel (AlmostHoms(int, IntegerAddition), AlHomOp1(int, IntegerAddition), FinRangeFunctions(int, int)) ∨ AlHomOp1(int, IntegerAddition) ` ⟨g, GroupInv(int, IntegerAddition) O f⟩ ∈ {s ∈ AlmostHoms(int, IntegerAddition) . s `` PositiveSet(int, IntegerAddition, IntegerOrder) ∩ PositiveSet(int, IntegerAddition, IntegerOrder) ∉ Fin(int)})
lemma Int_ZF_2_5_L3:
m ∈ int ==> {⟨n, IntegerMultiplication ` ⟨GroupInv(int, IntegerAddition) ` m, n⟩⟩ . n ∈ int} = GroupInv(int, IntegerAddition) O {⟨n, IntegerMultiplication ` ⟨m, n⟩⟩ . n ∈ int}
lemma Int_ZF_2_5_L3A:
[| m ∈ int; k ∈ int |] ==> AlHomOp1(int, IntegerAddition) ` ⟨{⟨n, IntegerMultiplication ` ⟨m, n⟩⟩ . n ∈ int}, {⟨n, IntegerMultiplication ` ⟨k, n⟩⟩ . n ∈ int}⟩ = {⟨n, IntegerMultiplication ` ⟨IntegerAddition ` ⟨m, k⟩, n⟩⟩ . n ∈ int}
lemma Int_ZF_2_5_L3B:
[| m ∈ int; k ∈ int |] ==> AlHomOp2(int, IntegerAddition) ` ⟨{⟨n, IntegerMultiplication ` ⟨m, n⟩⟩ . n ∈ int}, {⟨n, IntegerMultiplication ` ⟨k, n⟩⟩ . n ∈ int}⟩ = {⟨n, IntegerMultiplication ` ⟨IntegerMultiplication ` ⟨m, k⟩, n⟩⟩ . n ∈ int}
lemma Int_ZF_2_5_L4:
⟨m, n⟩ ∈ IntegerOrder ==> ⟨{⟨n, IntegerMultiplication ` ⟨m, n⟩⟩ . n ∈ int}, {⟨n, IntegerMultiplication ` ⟨n, n⟩⟩ . n ∈ int}⟩ ∈ QuotientGroupRel (AlmostHoms(int, IntegerAddition), AlHomOp1(int, IntegerAddition), FinRangeFunctions(int, int)) ∨ AlHomOp1(int, IntegerAddition) ` ⟨{⟨n, IntegerMultiplication ` ⟨n, n⟩⟩ . n ∈ int}, GroupInv(int, IntegerAddition) O {⟨n, IntegerMultiplication ` ⟨m, n⟩⟩ . n ∈ int}⟩ ∈ {s ∈ AlmostHoms(int, IntegerAddition) . s `` PositiveSet(int, IntegerAddition, IntegerOrder) ∩ PositiveSet(int, IntegerAddition, IntegerOrder) ∉ Fin(int)}
lemma Int_ZF_2_5_L5:
[| m ∈ int; {⟨n, IntegerMultiplication ` ⟨m, n⟩⟩ . n ∈ int} ∈ FinRangeFunctions(int, int) |] ==> m = TheNeutralElement(int, IntegerAddition)
lemma Int_ZF_2_5_L6:
[| m ∈ int; k ∈ int; ⟨{⟨n, IntegerMultiplication ` ⟨m, n⟩⟩ . n ∈ int}, {⟨n, IntegerMultiplication ` ⟨k, n⟩⟩ . n ∈ int}⟩ ∈ QuotientGroupRel (AlmostHoms(int, IntegerAddition), AlHomOp1(int, IntegerAddition), FinRangeFunctions(int, int)) |] ==> m = k
lemma Int_ZF_2_5_L7:
{⟨n, IntegerMultiplication `
⟨TheNeutralElement(int, IntegerMultiplication), n⟩⟩ .
n ∈ int} =
id(int)
{⟨n, IntegerMultiplication ` ⟨TheNeutralElement(int, IntegerAddition), n⟩⟩ .
n ∈ int} ∈
FinRangeFunctions(int, int)
lemma Int_ZF_2_5_L8:
[| f ∈ AlmostHoms(int, IntegerAddition); N ∈ int; M ∈ int; ∀n∈PositiveSet(int, IntegerAddition, IntegerOrder). ⟨IntegerMultiplication ` ⟨M, n⟩, f ` (IntegerMultiplication ` ⟨N, n⟩)⟩ ∈ IntegerOrder |] ==> ⟨{⟨n, IntegerMultiplication ` ⟨M, n⟩⟩ . n ∈ int}, AlHomOp2(int, IntegerAddition) ` ⟨f, {⟨n, IntegerMultiplication ` ⟨N, n⟩⟩ . n ∈ int}⟩⟩ ∈ QuotientGroupRel (AlmostHoms(int, IntegerAddition), AlHomOp1(int, IntegerAddition), FinRangeFunctions(int, int)) ∨ AlHomOp1(int, IntegerAddition) ` ⟨AlHomOp2(int, IntegerAddition) ` ⟨f, {⟨n, IntegerMultiplication ` ⟨N, n⟩⟩ . n ∈ int}⟩, GroupInv(int, IntegerAddition) O {⟨n, IntegerMultiplication ` ⟨M, n⟩⟩ . n ∈ int}⟩ ∈ {s ∈ AlmostHoms(int, IntegerAddition) . s `` PositiveSet(int, IntegerAddition, IntegerOrder) ∩ PositiveSet(int, IntegerAddition, IntegerOrder) ∉ Fin(int)}
lemma Int_ZF_2_5_L9:
[| f ∈ AlmostHoms(int, IntegerAddition); N ∈ int; M ∈ int; ∀n∈PositiveSet(int, IntegerAddition, IntegerOrder). ⟨f ` (IntegerMultiplication ` ⟨N, n⟩), IntegerMultiplication ` ⟨M, n⟩⟩ ∈ IntegerOrder |] ==> ⟨AlHomOp2(int, IntegerAddition) ` ⟨f, {⟨n, IntegerMultiplication ` ⟨N, n⟩⟩ . n ∈ int}⟩, {⟨n, IntegerMultiplication ` ⟨M, n⟩⟩ . n ∈ int}⟩ ∈ QuotientGroupRel (AlmostHoms(int, IntegerAddition), AlHomOp1(int, IntegerAddition), FinRangeFunctions(int, int)) ∨ AlHomOp1(int, IntegerAddition) ` ⟨{⟨n, IntegerMultiplication ` ⟨M, n⟩⟩ . n ∈ int}, GroupInv(int, IntegerAddition) O AlHomOp2(int, IntegerAddition) ` ⟨f, {⟨n, IntegerMultiplication ` ⟨N, n⟩⟩ . n ∈ int}⟩⟩ ∈ {s ∈ AlmostHoms(int, IntegerAddition) . s `` PositiveSet(int, IntegerAddition, IntegerOrder) ∩ PositiveSet(int, IntegerAddition, IntegerOrder) ∉ Fin(int)}