This theory is a continuation of Int_ZF_2. We consider here the properties of slopes (almost homomorphisms on integers) that allow to define the order relation and multiplicative inverse on real numbers. We also prove theorems that allow to show completeness of the order relation of real numbers we define in Real_ZF.
This section provides background material for defining the order relation on real numbers.
Positive slopes are functions (of course.)
lemma (in int1) Int_ZF_2_3_L1:
assumes A1: \( f\in \mathcal{S} _+ \)
shows \( f:\mathbb{Z} \rightarrow \mathbb{Z} \) using assms, AlmostHoms_def, PositiveSet_defA small technical lemma to simplify the proof of the next theorem.
lemma (in int1) Int_ZF_2_3_L1A:
assumes A1: \( f\in \mathcal{S} _+ \) and A2: \( \exists n \in f(\mathbb{Z} _+) \cap \mathbb{Z} _+.\ a\leq n \)
shows \( \exists M\in \mathbb{Z} _+.\ a \leq f(M) \)proofThe next lemma is Lemma 3 in the Arthan's paper.
lemma (in int1) Arthan_Lem_3:
assumes A1: \( f\in \mathcal{S} _+ \) and A2: \( D \in \mathbb{Z} _+ \)
shows \( \exists M\in \mathbb{Z} _+.\ \forall m\in \mathbb{Z} _+.\ (m + 1 )\cdot D \leq f(m\cdot M) \)proofA special case of Arthan_Lem_3 when \(D=1\).
corollary (in int1) Arthan_L_3_spec:
assumes A1: \( f \in \mathcal{S} _+ \)
shows \( \exists M\in \mathbb{Z} _+.\ \forall n\in \mathbb{Z} _+.\ n + 1 \leq f(n\cdot M) \)proofWe know from 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 \( \mathcal{S} _+ \). This is important, because the projection of the set of finite range functions defines zero in the real number construction in Real_ZF_x.thy series, while the projection of \( \mathcal{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 \in \text{FinRangeFunctions}(\mathbb{Z} ,\mathbb{Z} ) \)
shows \( f\in \mathcal{S} \), \( f \notin \mathcal{S} _+ \)proofWe want to show that if \(f\) is a slope and neither \(f\) nor \(-f\) are in \( \mathcal{S} _+ \), then \(f\) is bounded. The next lemma is the first step towards that goal and shows that if slope is not in \( \mathcal{S} _+ \) then \(f(\)\( \mathbb{Z} _+ \)\()\) is bounded above.
lemma (in int1) Int_ZF_2_3_L2:
assumes A1: \( f\in \mathcal{S} \) and A2: \( f \notin \mathcal{S} _+ \)
shows \( \text{IsBoundedAbove}(f(\mathbb{Z} _+), IntegerOrder) \)proofIf \(f\) is a slope and \(-f\notin\) \( \mathcal{S} _+ \), then \(f(\)\( \mathbb{Z} _+ \)\()\) is bounded below.
lemma (in int1) Int_ZF_2_3_L3:
assumes A1: \( f\in \mathcal{S} \) and A2: \( - f \notin \mathcal{S} _+ \)
shows \( \text{IsBoundedBelow}(f(\mathbb{Z} _+), IntegerOrder) \)proofA slope that is bounded on \( \mathbb{Z} _+ \) is bounded everywhere.
lemma (in int1) Int_ZF_2_3_L4:
assumes A1: \( f\in \mathcal{S} \) and A2: \( m\in \mathbb{Z} \) and A3: \( \forall n\in \mathbb{Z} _+.\ abs(f(n)) \leq L \)
shows \( abs(f(m)) \leq 2 \cdot \text{ max}\delta (f) + L \)proofA 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\in \mathcal{S} \) and A2: \( \text{IsBounded}(f(\mathbb{Z} _+), IntegerOrder) \)
shows \( f \in \text{FinRangeFunctions}(\mathbb{Z} ,\mathbb{Z} ) \)proofA 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\in \mathcal{S} \) and \( \text{IsBoundedBelow}(f(\mathbb{Z} _+), IntegerOrder) \)
shows \( f \in \text{FinRangeFunctions}(\mathbb{Z} ,\mathbb{Z} ) \vee f\in \mathcal{S} _+ \) using assms, Int_ZF_2_3_L2, IsBounded_def, Int_ZF_2_3_L4AIf 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\in \mathcal{S} \), \( g\in \mathcal{S} \) and A2: \( \forall n\in \mathbb{Z} _+.\ f(n) \leq g(n) \)
shows \( f\sim g \vee g + ( - f) \in \mathcal{S} _+ \)proofPositive slopes are arbitrarily large for large enough arguments.
lemma (in int1) Int_ZF_2_3_L5:
assumes A1: \( f\in \mathcal{S} _+ \) and A2: \( K\in \mathbb{Z} \)
shows \( \exists N\in \mathbb{Z} _+.\ \forall m.\ N\leq m \longrightarrow K \leq f(m) \)proofPositive slopes are arbitrarily small for small enough arguments. Kind of dual to Int_ZF_2_3_L5.
lemma (in int1) Int_ZF_2_3_L5A:
assumes A1: \( f\in \mathcal{S} _+ \) and A2: \( K\in \mathbb{Z} \)
shows \( \exists N\in \mathbb{Z} _+.\ \forall m.\ N\leq m \longrightarrow f( - m) \leq K \)proofA special case of Int_ZF_2_3_L5 where \(K=1\).
corollary (in int1) Int_ZF_2_3_L6:
assumes \( f\in \mathcal{S} _+ \)
shows \( \exists N\in \mathbb{Z} _+.\ \forall m.\ N\leq m \longrightarrow f(m) \in \mathbb{Z} _+ \) using assms, int_zero_one_are_int, Int_ZF_2_3_L5, Int_ZF_1_5_L3A special case of Int_ZF_2_3_L5 where \(m=N\).
corollary (in int1) Int_ZF_2_3_L6A:
assumes \( f\in \mathcal{S} _+ \) and \( K\in \mathbb{Z} \)
shows \( \exists N\in \mathbb{Z} _+.\ K \leq f(N) \)proofIf values of a slope are not bounded above, then the slope is positive.
lemma (in int1) Int_ZF_2_3_L7:
assumes A1: \( f\in \mathcal{S} \) and A2: \( \forall K\in \mathbb{Z} .\ \exists n\in \mathbb{Z} _+.\ K \leq f(n) \)
shows \( f \in \mathcal{S} _+ \)proofFor unbounded slope \(f\) either \(f\in\)\( \mathcal{S} _+ \) of \(-f\in\)\( \mathcal{S} _+ \).
theorem (in int1) Int_ZF_2_3_L8:
assumes A1: \( f\in \mathcal{S} \) and A2: \( f \notin \text{FinRangeFunctions}(\mathbb{Z} ,\mathbb{Z} ) \)
shows \( (f \in \mathcal{S} _+) \text{ Xor } (( - f) \in \mathcal{S} _+) \)proofThe sum of positive slopes is a positive slope.
theorem (in int1) sum_of_pos_sls_is_pos_sl:
assumes A1: \( f \in \mathcal{S} _+ \), \( g \in \mathcal{S} _+ \)
shows \( f + g \in \mathcal{S} _+ \)proofThe composition of positive slopes is a positive slope.
theorem (in int1) comp_of_pos_sls_is_pos_sl:
assumes A1: \( f \in \mathcal{S} _+ \), \( g \in \mathcal{S} _+ \)
shows \( f\circ g \in \mathcal{S} _+ \)proofA slope equivalent to a positive one is positive.
lemma (in int1) Int_ZF_2_3_L9:
assumes A1: \( f \in \mathcal{S} _+ \) and A2: \( \langle f,g\rangle \in AlEqRel \)
shows \( g \in \mathcal{S} _+ \)proofThe set of positive slopes is saturated with respect to the relation of equivalence of slopes.
lemma (in int1) pos_slopes_saturated:
shows \( \text{IsSaturated}(AlEqRel,\mathcal{S} _+) \)proofA 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\in \mathcal{S} \), \( g\in \mathcal{S} \) and A2: \( R = \{AlEqRel\{s\}.\ s\in \mathcal{S} _+\} \) and A3: \( (f\in \mathcal{S} _+) \text{ Xor } (g\in \mathcal{S} _+) \)
shows \( (AlEqRel\{f\} \in R) \text{ Xor } (AlEqRel\{g\} \in R) \)proofIdentity function is a positive slope.
lemma (in int1) Int_ZF_2_3_L11:
shows \( id(\mathbb{Z} ) \in \mathcal{S} _+ \)proofThe identity function is not almost equal to any bounded function.
lemma (in int1) Int_ZF_2_3_L12:
assumes A1: \( f \in \text{FinRangeFunctions}(\mathbb{Z} ,\mathbb{Z} ) \)
shows \( \neg (id(\mathbb{Z} ) \sim f) \)proofNot 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.
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 \in \mathcal{S} _+ \) and A2: \( p\in \mathbb{Z} _+ \) and A3: \( A = \{n\in \mathbb{Z} _+.\ p \leq f(n)\} \)
shows \( A \subseteq \mathbb{Z} _+ \), \( A \neq 0 \), \( f^{-1}(p) \in A \), \( \forall m\in A.\ f^{-1}(p) \leq m \)proofIf \(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 \in \mathcal{S} _+ \) and \( p\in \mathbb{Z} _+ \)
shows \( f^{-1}(p) \in \mathbb{Z} _+ \), \( p \leq f(f^{-1}(p)) \) using assms, Int_ZF_2_4_L1If \(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 \in \mathcal{S} _+ \) and \( m\in \mathbb{Z} _+ \), \( p\in \mathbb{Z} _+ \) and \( m \leq f(p) \)
shows \( f^{-1}(m) \leq p \) using assms, Int_ZF_2_4_L1An upper bound \(f(f^{-1}(m) -1)\) for positive slopes.
lemma (in int1) Int_ZF_2_4_L4:
assumes A1: \( f \in \mathcal{S} _+ \) and A2: \( m\in \mathbb{Z} _+ \) and A3: \( f^{-1}(m) - 1 \in \mathbb{Z} _+ \)
shows \( f(f^{-1}(m) - 1 ) \leq m \), \( f(f^{-1}(m) - 1 ) \neq m \)proofThe (candidate for) the inverse of a positive slope is nondecreasing.
lemma (in int1) Int_ZF_2_4_L5:
assumes A1: \( f \in \mathcal{S} _+ \) and A2: \( m\in \mathbb{Z} _+ \) and A3: \( m\leq n \)
shows \( f^{-1}(m) \leq f^{-1}(n) \)proofIf \(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 \in \mathcal{S} _+ \) and A2: \( m\in \mathbb{Z} _+ \), \( n\in \mathbb{Z} _+ \) and A3: \( f^{-1}(m) - 1 \in \mathbb{Z} _+ \)
shows \( f^{-1}(m + n) - 1 \in \mathbb{Z} _+ \)proofIf \(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 \in \mathcal{S} _+ \) and A2: \( \forall m\in \mathbb{Z} _+.\ f^{-1}(m) - 1 \in \mathbb{Z} _+ \)
shows \( \exists U\in \mathbb{Z} .\ \forall m\in \mathbb{Z} _+.\ \forall n\in \mathbb{Z} _+.\ f(f^{-1}(m + n) - f^{-1}(m) - f^{-1}(n)) \leq U \), \( \exists N\in \mathbb{Z} .\ \forall m\in \mathbb{Z} _+.\ \forall n\in \mathbb{Z} _+.\ N \leq f(f^{-1}(m + n) - f^{-1}(m) - f^{-1}(n)) \)proofThe expression \(f^{-1}(m+n)-f^{-1}(m) - f^{-1}(n)\) is uniformly bounded for all pairs \(\langle m,n \rangle \in\) \( \mathbb{Z} _+\times \mathbb{Z} _+ \). Recall that in the int1 context \( \varepsilon (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 \in \mathcal{S} _+ \) and A2: \( \forall m\in \mathbb{Z} _+.\ f^{-1}(m) - 1 \in \mathbb{Z} _+ \)
shows \( \exists M.\ \forall x\in \mathbb{Z} _+\times \mathbb{Z} _+.\ abs(\varepsilon (f,x)) \leq M \)proofThe (candidate for) inverse of a positive slope is a (well defined) function on \( \mathbb{Z} _+ \).
lemma (in int1) Int_ZF_2_4_L9:
assumes A1: \( f \in \mathcal{S} _+ \) and A2: \( g = \{\langle p,f^{-1}(p)\rangle .\ p\in \mathbb{Z} _+\} \)
shows \( g : \mathbb{Z} _+\rightarrow \mathbb{Z} _+ \), \( g : \mathbb{Z} _+\rightarrow \mathbb{Z} \)proofWhat are the values of the (candidate for) the inverse of a positive slope?
lemma (in int1) Int_ZF_2_4_L10:
assumes A1: \( f \in \mathcal{S} _+ \) and A2: \( g = \{\langle p,f^{-1}(p)\rangle .\ p\in \mathbb{Z} _+\} \) and A3: \( p\in \mathbb{Z} _+ \)
shows \( g(p) = f^{-1}(p) \)proofThe (candidate for) the inverse of a positive slope is a slope.
lemma (in int1) Int_ZF_2_4_L11:
assumes A1: \( f \in \mathcal{S} _+ \) and A2: \( \forall m\in \mathbb{Z} _+.\ f^{-1}(m) - 1 \in \mathbb{Z} _+ \) and A3: \( g = \{\langle p,f^{-1}(p)\rangle .\ p\in \mathbb{Z} _+\} \)
shows \( \text{OddExtension}(\mathbb{Z} ,IntegerAddition,IntegerOrder,g) \in \mathcal{S} \)proofEvery 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 \in \mathcal{S} _+ \) and A2: \( \forall m\in \mathbb{Z} _+.\ f^{-1}(m) - 1 \in \mathbb{Z} _+ \)
shows \( \exists h\in \mathcal{S} .\ f\circ h \sim id(\mathbb{Z} ) \)proofInt_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 \in \mathcal{S} _+ \)
shows \( \exists g\in \mathcal{S} .\ f\sim g \wedge (\exists h\in \mathcal{S} .\ g\circ h \sim id(\mathbb{Z} )) \)proofIn this section we consider properties of slopes that are needed for the proof of completeness of real numbers constructred in 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\).
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 \in \mathbb{Z} \)
shows \( \forall n \in \mathbb{Z} .\ (m^S)(n) = m\cdot n \), \( m^S \in \mathcal{S} \)proofFor 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 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 \in \mathcal{S} \)
shows \( \exists m\in \mathbb{Z} .\ \exists g\in \mathcal{S} .\ (m^S\sim g \wedge (f\sim g \vee g + ( - f) \in \mathcal{S} _+)) \)proofThe 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 \in \mathbb{Z} \)
shows \( ( - m)^S = - (m^S) \)proofThe sum of embeddings is the embeding of the sum.
lemma (in int1) Int_ZF_2_5_L3A:
assumes A1: \( m\in \mathbb{Z} \), \( k\in \mathbb{Z} \)
shows \( (m^S) + (k^S) = ((m + k)^S) \)proofThe composition of embeddings is the embeding of the product.
lemma (in int1) Int_ZF_2_5_L3B:
assumes A1: \( m\in \mathbb{Z} \), \( k\in \mathbb{Z} \)
shows \( (m^S) \circ (k^S) = ((m\cdot k)^S) \)proofEmbedding integers in slopes preserves order.
lemma (in int1) Int_ZF_2_5_L4:
assumes A1: \( m\leq n \)
shows \( (m^S) \sim (n^S) \vee (n^S) + ( - (m^S)) \in \mathcal{S} _+ \)proofWe 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\in \mathbb{Z} \) and \( m^S \in \text{FinRangeFunctions}(\mathbb{Z} ,\mathbb{Z} ) \)
shows \( m= 0 \) using assms, FinRangeFunctions_def, Int_ZF_2_5_L1, AlmostHoms_def, func_imagedef, Int_ZF_1_6_L8Embeddings of two integers are almost equal only if the integers are equal.
lemma (in int1) Int_ZF_2_5_L6:
assumes A1: \( m\in \mathbb{Z} \), \( k\in \mathbb{Z} \) and A2: \( (m^S) \sim (k^S) \)
shows \( m=k \)proofEmbedding of \(1\) is the identity slope and embedding of zero is a finite range function.
lemma (in int1) Int_ZF_2_5_L7:
shows \( 1 ^S = id(\mathbb{Z} ) \), \( 0 ^S \in \text{FinRangeFunctions}(\mathbb{Z} ,\mathbb{Z} ) \)proofA 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 \in \mathcal{S} \) and A2: \( N \in \mathbb{Z} \), \( M \in \mathbb{Z} \) and A3: \( \forall n\in \mathbb{Z} _+.\ M\cdot n \leq f(N\cdot n) \)
shows \( M^S \sim f\circ (N^S) \vee (f\circ (N^S)) + ( - (M^S)) \in \mathcal{S} _+ \)proofAnother 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 \in \mathcal{S} \) and A2: \( N \in \mathbb{Z} \), \( M \in \mathbb{Z} \) and A3: \( \forall n\in \mathbb{Z} _+.\ f(N\cdot n) \leq M\cdot n \)
shows \( f\circ (N^S) \sim (M^S) \vee (M^S) + ( - (f\circ (N^S))) \in \mathcal{S} _+ \)proofassumes \( f:X\rightarrow Y \) and \( A\subseteq X \)
shows \( f(A) = \{f(x).\ x \in A\} \)assumes \( s\in \mathcal{S} \)
shows \( abs(s( 0 )) \leq \text{ max}\delta (s) \), \( 0 \leq \text{ max}\delta (s) \), \( abs(s( 0 )) \in \mathbb{Z} \), \( \text{ max}\delta (s) \in \mathbb{Z} \), \( abs(s( 0 )) + \text{ max}\delta (s) \in \mathbb{Z} \)assumes \( m \leq n \)
shows \( m $\leq n \), \( m\in \mathbb{Z} \), \( n\in \mathbb{Z} \)assumes \( 0 \leq n \), \( m\in \mathbb{Z} \)
shows \( m \leq n + m \)assumes \( a\in \mathbb{Z} \), \( b\in \mathbb{Z} \)
shows \( a + b \in \mathbb{Z} \), \( a - b \in \mathbb{Z} \), \( a\cdot b \in \mathbb{Z} \), \( a + b = b + a \), \( a\cdot b = b\cdot a \), \( ( - b) - a = ( - a) - b \), \( ( - (a + b)) = ( - a) - b \), \( ( - (a - b)) = (( - a) + b) \), \( ( - a)\cdot b = - (a\cdot b) \), \( a\cdot ( - b) = - (a\cdot b) \), \( ( - a)\cdot ( - b) = a\cdot b \)assumes \( A \subseteq \mathbb{Z} _+ \) and \( A \notin Fin(\mathbb{Z} ) \) and \( D\in \mathbb{Z} \)
shows \( \exists n\in A.\ D\leq n \)assumes \( f\in \mathcal{S} _+ \) and \( \exists n \in f(\mathbb{Z} _+) \cap \mathbb{Z} _+.\ a\leq n \)
shows \( \exists M\in \mathbb{Z} _+.\ a \leq f(M) \)assumes \( a \in \mathbb{Z} \)
shows \( a + 0 = a \), \( 0 + a = a \), \( a\cdot 1 = a \), \( 1 \cdot a = a \), \( 0 \cdot a = 0 \), \( a\cdot 0 = 0 \), \( ( - a) \in \mathbb{Z} \), \( ( - ( - a)) = a \), \( a - a = 0 \), \( a - 0 = a \), \( 2 \cdot a = a + a \)assumes \( s\in \mathcal{S} \) and \( n\in \mathbb{Z} \), \( m\in \mathbb{Z} \)
shows \( abs(\delta (s,m,n)) \leq \text{ max}\delta (s) \), \( \delta (s,m,n) \in \mathbb{Z} \), \( \text{ max}\delta (s) \in \mathbb{Z} \), \( ( - \text{ max}\delta (s)) \leq \delta (s,m,n) \)assumes \( 1 \leq a \)
shows \( 0 \leq a \), \( a\neq 0 \), \( 2 \leq a + 1 \), \( 1 \leq a + 1 \), \( 0 \leq a + 1 \)assumes \( m\in \mathbb{Z} \) and \( abs(m) \leq n \) and \( 0 \leq k \)
shows \( ( - (n + k)) \leq m \)assumes \( a\leq b \) and \( c\leq d \)
shows \( a + c \leq b + d \), \( a - d \leq b - c \)assumes \( a\in \mathbb{Z} \), \( b\in \mathbb{Z} \), \( c\in \mathbb{Z} \)
shows \( a\cdot (b + c) = a\cdot b + a\cdot c \), \( (b + c)\cdot a = b\cdot a + c\cdot a \)assumes \( a\in \mathbb{Z} \)
shows \( a + 1 + 2 = a + 3 \), \( a = 2 \cdot a - a \)assumes \( s\in \mathcal{S} \) and \( n\in \mathbb{Z} \), \( m\in \mathbb{Z} \)
shows \( s(n\cdot m) + (s(m) + \delta (s,n\cdot m,m)) = s((n + 1 )\cdot m) \)assumes \( i\leq k \) and \( Q(i) \) and \( \forall m.\ i\leq m \wedge Q(m) \longrightarrow Q(m + 1 ) \)
shows \( Q(k) \)assumes \( 1 \leq a \) and \( b\leq c \) and \( (a + 1 )\cdot c \leq d \)
shows \( (a + 1 )\cdot b \leq d \)assumes \( f\in \mathcal{S} _+ \) and \( D \in \mathbb{Z} _+ \)
shows \( \exists M\in \mathbb{Z} _+.\ \forall m\in \mathbb{Z} _+.\ (m + 1 )\cdot D \leq f(m\cdot M) \)assumes \( f \in \text{FinRangeFunctions}(X,Y) \) and \( A\subseteq X \)
shows \( f(A) \in Fin(Y) \)assumes \( f:X\rightarrow Y \)
shows \( f(B) \subseteq \text{range}(f) \) and \( f(B) \subseteq Y \)assumes \( r \text{ is total on } G \) and \( A\subseteq G \) and \( A \cap G_+ \in Fin(G) \)
shows \( \text{IsBoundedAbove}(A,r) \)assumes \( \text{IsAgroup}(G,f) \)
shows \( \text{GroupInv}(G,f) : G\rightarrow G \)assumes \( f:X\rightarrow Y \) and \( g:Y\rightarrow Z \) and \( A\subseteq X \)
shows \( g(f(A)) = \{g(f(x)).\ x\in A\} \), \( g(f(A)) = (g\circ f)(A) \)assumes \( s\in \mathcal{S} \)
shows \( - s \in \mathcal{S} \)assumes \( f\in \mathcal{S} \) and \( f \notin \mathcal{S} _+ \)
shows \( \text{IsBoundedAbove}(f(\mathbb{Z} _+), IntegerOrder) \)assumes \( A\subseteq G \) and \( \text{IsBoundedAbove}(-A,r) \)
shows \( \text{IsBoundedBelow}(A,r) \)assumes \( f\in \mathcal{S} \) and \( m\in \mathbb{Z} \)
shows \( f(m) \in \mathbb{Z} \)assumes \( m\in \mathbb{Z} \)
shows \( abs(m) \in \mathbb{Z} ^+ \), \( 0 \leq abs(m) \)assumes \( m\leq n \), \( n\leq k \)
shows \( m\leq k \)assumes \( m\leq k \) and \( 0 \leq n \)
shows \( m \leq k + n \), \( m \leq n + k \)assumes \( 0 \leq a \)
shows \( 0 \leq 2 \cdot a \)assumes \( s\in \mathcal{S} \) and \( m\in \mathbb{Z} \)
shows \( s( - m) = s( 0 ) - \delta (s,m, - m) - s(m) \), \( abs(s(m) + s( - m)) \leq 2 \cdot \text{ max}\delta (s) \), \( abs(s( - m)) \leq 2 \cdot \text{ max}\delta (s) + abs(s(m)) \), \( s( - m) \leq abs(s( 0 )) + \text{ max}\delta (s) - s(m) \)assumes \( b\in \mathbb{Z} \) and \( a\leq b + c \) and \( c\leq c_1 \)
shows \( a\leq b + c_1 \)assumes \( m\in \mathbb{Z} \) and \( Q( 0 ) \) and \( \forall n\in \mathbb{Z} _+.\ Q(n) \) and \( \forall n\in \mathbb{Z} _+.\ Q( - n) \)
shows \( Q(m) \)assumes \( \text{IsBounded}(A,IntegerOrder) \)
shows \( \exists L.\ \forall a\in A.\ abs(a) \leq L \)assumes \( f:X\rightarrow Y \) and \( A\subseteq X \) and \( \forall y\in f(A).\ P(y) \)
shows \( \forall x\in A.\ P(f(x)) \)assumes \( f\in \mathcal{S} \) and \( m\in \mathbb{Z} \) and \( \forall n\in \mathbb{Z} _+.\ abs(f(n)) \leq L \)
shows \( abs(f(m)) \leq 2 \cdot \text{ max}\delta (f) + L \)assumes \( f:\mathbb{Z} \rightarrow \mathbb{Z} \) and \( \forall m\in \mathbb{Z} .\ abs(f(m)) \leq L \)
shows \( f(\mathbb{Z} ) \in Fin(\mathbb{Z} ) \)assumes \( f\in \mathcal{S} \) and \( \text{IsBounded}(f(\mathbb{Z} _+), IntegerOrder) \)
shows \( f \in \text{FinRangeFunctions}(\mathbb{Z} ,\mathbb{Z} ) \)assumes \( s\in \mathcal{S} \), \( r\in \mathcal{S} \)
shows \( s + r \in \mathcal{S} \)assumes \( a\leq b \)
shows \( 0 \leq b - a \)assumes \( s\in \mathcal{S} \), \( r\in \mathcal{S} \) and \( m\in \mathbb{Z} \)
shows \( (s + r)(m) = s(m) + r(m) \)assumes \( s\in \mathcal{S} \) and \( m\in \mathbb{Z} \)
shows \( ( - s)(m) = - (s(m)) \)assumes \( f:X\rightarrow Y \) and \( A\subseteq X \) and \( \forall x\in A.\ \langle L,f(x)\rangle \in r \)
shows \( \text{IsBoundedBelow}(f(A),r) \)assumes \( f\in \mathcal{S} \) and \( \text{IsBoundedBelow}(f(\mathbb{Z} _+), IntegerOrder) \)
shows \( f \in \text{FinRangeFunctions}(\mathbb{Z} ,\mathbb{Z} ) \vee f\in \mathcal{S} _+ \)assumes \( s\in \mathcal{S} \), \( r\in \mathcal{S} \) and \( s + ( - r) \in \text{FinRangeFunctions}(\mathbb{Z} ,\mathbb{Z} ) \)
shows \( s \sim r \), \( r \sim s \)assumes \( f \in \mathcal{S} _+ \)
shows \( \exists M\in \mathbb{Z} _+.\ \forall n\in \mathbb{Z} _+.\ n + 1 \leq f(n\cdot M) \)assumes \( s\in \mathcal{S} \) and \( M \in \mathbb{Z} _+ \)
shows \( maxf(s, 0 .\ .\ (M - 1 )) \in \mathbb{Z} \), \( \forall n \in 0 .\ .\ (M - 1 ).\ s(n) \leq maxf(s, 0 .\ .\ (M - 1 )) \), \( minf(s, 0 .\ .\ (M - 1 )) \in \mathbb{Z} \), \( \forall n \in 0 .\ .\ (M - 1 ).\ minf(s, 0 .\ .\ (M - 1 )) \leq s(n) \)assumes \( m\in \mathbb{Z} \), \( n\in \mathbb{Z} \)
shows \( m \leq \text{GreaterOf}(IntegerOrder,m,n) \), \( n \leq \text{GreaterOf}(IntegerOrder,m,n) \), \( \text{SmallerOf}(IntegerOrder,m,n) \leq m \), \( \text{SmallerOf}(IntegerOrder,m,n) \leq n \)assumes \( i\in \mathbb{Z} \), \( m\in \mathbb{Z} \) and \( i - m \leq k \)
shows \( i \leq k + m \)assumes \( n \in \mathbb{Z} _+ \) and \( n \leq k \) and \( k\cdot n \leq m \)
shows \( m = n\cdot (m\text{ zdiv }n) + (m\text{ zmod }n) \), \( m = (m\text{ zdiv }n)\cdot n + (m\text{ zmod }n) \), \( (m\text{ zmod }n) \in 0 .\ .\ (n - 1 ) \), \( k \leq (m\text{ zdiv }n) \), \( m\text{ zdiv }n \in \mathbb{Z} _+ \)assumes \( k \in \mathbb{Z} \) and \( m \leq n \)
shows \( m + k \leq n + k \), \( k + m\leq k + n \)assumes \( s\in \mathcal{S} \) and \( m\in \mathbb{Z} \) and \( M \in \mathbb{Z} _+ \) and \( k \in 0 .\ .\ (M - 1 ) \)
shows \( s(m\cdot M) + (minf(s, 0 .\ .\ (M - 1 )) - \text{ max}\delta (s)) \leq s(m\cdot M + k) \)assumes \( f\in \mathcal{S} _+ \) and \( K\in \mathbb{Z} \)
shows \( \exists N\in \mathbb{Z} _+.\ \forall m.\ N\leq m \longrightarrow K \leq f(m) \)assumes \( k \leq i \)
shows \( ( - i) \leq ( - k) \), \( \ \$\!-\!i \leq \ \$\!-\!k \)assumes \( a\in \mathbb{Z} \), \( b\in \mathbb{Z} \)
shows \( a + b - a = b \), \( a + (b - a) = b \), \( a + b - b = a \), \( a - b + b = a \), \( ( - a) + (a + b) = b \), \( a + (b - a) = b \), \( ( - b) + (a + b) = a \), \( a - (b + a) = - b \), \( a - (a + b) = - b \), \( a - (a - b) = b \), \( a - b - a = - b \), \( a - b - (a + b) = ( - b) - b \)assumes \( f:X\rightarrow Y \), \( x\in A \), \( A\subseteq X \)
shows \( f(x) \in f(A) \)assumes \( \forall m\in \mathbb{Z} .\ \exists k\in A.\ m\leq k \)
shows \( \neg \text{IsBoundedAbove}(A,IntegerOrder) \), \( A \notin Fin(\mathbb{Z} ) \)assumes \( f\in \mathcal{S} \) and \( - f \notin \mathcal{S} _+ \)
shows \( \text{IsBoundedBelow}(f(\mathbb{Z} _+), IntegerOrder) \)assumes \( f\in \mathcal{S} _+ \)
shows \( \exists N\in \mathbb{Z} _+.\ \forall m.\ N\leq m \longrightarrow f(m) \in \mathbb{Z} _+ \)assumes \( a \in \mathbb{Z} _+ \)
shows \( ( - a) \notin \mathbb{Z} _+ \)assumes \( f\in \mathcal{S} \) and \( \forall K\in \mathbb{Z} .\ \exists n\in \mathbb{Z} _+.\ K \leq f(n) \)
shows \( f \in \mathcal{S} _+ \)assumes \( f\in \mathcal{S} _+ \) and \( K\in \mathbb{Z} \)
shows \( \exists N\in \mathbb{Z} _+.\ K \leq f(N) \)assumes \( s\in \mathcal{S} \), \( r\in \mathcal{S} \) and \( m\in \mathbb{Z} \)
shows \( (s\circ r)(m) = s(r(m)) \), \( s(r(m)) \in \mathbb{Z} \)assumes \( s\in \mathcal{S} \), \( r\in \mathcal{S} \)
shows \( s\circ r \in \mathcal{S} \)assumes \( s \sim r \)
shows \( \exists L\in \mathbb{Z} .\ \forall m\in \mathbb{Z} .\ abs(s(m) - r(m)) \leq L \), \( s\in \mathcal{S} \), \( r\in \mathcal{S} \)assumes \( i\in \mathbb{Z} \), \( m\in \mathbb{Z} \), \( k\in \mathbb{Z} \)
shows \( i + m \leq k \longleftrightarrow i \leq k - m \)assumes \( m\in \mathbb{Z} \), \( n\in \mathbb{Z} \) and \( abs(m - n) \leq k \)
shows \( abs(m) \leq abs(n) + k \), \( m - k \leq n \), \( m \leq n + k \), \( n - k \leq m \)assumes \( f \in \mathcal{S} _+ \) and \( \langle f,g\rangle \in AlEqRel \)
shows \( g \in \mathcal{S} _+ \)assumes \( \text{equiv}(X,r) \) and \( r \subseteq X\times X \) and \( A\subseteq X \) and \( \forall x\in A.\ \forall y\in X.\ \langle x,y\rangle \in r \longrightarrow y\in A \)
shows \( \text{IsSaturated}(r,A) \)assumes \( \text{equiv}(X,r) \) and \( \text{IsSaturated}(r,A) \) and \( A\subseteq X \) and \( x\in X \), \( y\in X \) and \( B = \{r\{x\}.\ x\in A\} \) and \( (x\in A) \text{ Xor } (y\in A) \)
shows \( (r\{x\} \in B) \text{ Xor } (r\{y\} \in B) \)assumes \( a\in \mathbb{Z} \)
shows \( \exists b\in \mathbb{Z} _+.\ a\leq b \)assumes \( f \in \text{FinRangeFunctions}(\mathbb{Z} ,\mathbb{Z} ) \)
shows \( f\in \mathcal{S} \), \( f \notin \mathcal{S} _+ \)assumes \( A \subseteq \mathbb{Z} _+ \) and \( A \neq 0 \)
shows \( \text{HasAminimum}(IntegerOrder,A) \), \( \text{Minimum}(IntegerOrder,A) \in A \), \( \forall x\in A.\ \text{Minimum}(IntegerOrder,A) \leq x \)assumes \( f \in \mathcal{S} _+ \) and \( p\in \mathbb{Z} _+ \) and \( A = \{n\in \mathbb{Z} _+.\ p \leq f(n)\} \)
shows \( A \subseteq \mathbb{Z} _+ \), \( A \neq 0 \), \( f^{-1}(p) \in A \), \( \forall m\in A.\ f^{-1}(p) \leq m \)assumes \( f \in \mathcal{S} _+ \) and \( p\in \mathbb{Z} _+ \)
shows \( f^{-1}(p) \in \mathbb{Z} _+ \), \( p \leq f(f^{-1}(p)) \)assumes \( f\in \mathcal{S} _+ \)
shows \( f:\mathbb{Z} \rightarrow \mathbb{Z} \)assumes \( f \in \mathcal{S} _+ \) and \( m\in \mathbb{Z} _+ \), \( p\in \mathbb{Z} _+ \) and \( m \leq f(p) \)
shows \( f^{-1}(m) \leq p \)assumes \( a\in \mathbb{Z} \)
shows \( a - 1 \leq a \), \( a - 1 \neq a \), \( \neg (a\leq a - 1 ) \), \( \neg (a + 1 \leq a) \), \( \neg (1 + a \leq a) \)assumes \( m\in \mathbb{Z} \), \( n\in \mathbb{Z} \) and \( \neg (n\leq m) \)
shows \( m\leq n \), \( ( - n) \leq ( - m) \), \( m\neq n \)assumes \( a \in \mathbb{Z} _+ \) and \( a\leq b \)
shows \( b \in \mathbb{Z} _+ \)assumes \( a\in \mathbb{Z} \), \( b \in \mathbb{Z} _+ \)
shows \( a \leq a + b \), \( a \neq a + b \), \( a + b \in \mathbb{Z} \)assumes \( f \in \mathcal{S} _+ \) and \( m\in \mathbb{Z} _+ \) and \( m\leq n \)
shows \( f^{-1}(m) \leq f^{-1}(n) \)assumes \( s\in \mathcal{S} \)
shows \( \exists M\in \mathbb{Z} .\ \forall m\in \mathbb{Z} .\ s(m) \leq s(m - 1 ) + M \)assumes \( s\in \mathcal{S} \)
shows \( \exists M\in \mathbb{Z} .\ \forall m\in \mathbb{Z} .\ \forall n\in \mathbb{Z} .\ \forall k\in \mathbb{Z} .\ s(m - n - k) \leq s(m) - s(n) - s(k) + M \), \( \exists K\in \mathbb{Z} .\ \forall m\in \mathbb{Z} .\ \forall n\in \mathbb{Z} .\ \forall k\in \mathbb{Z} .\ s(m) - s(n) - s(k) + K \leq s(m - n - k) \)assumes \( a\in \mathbb{Z} _+ \), \( b\in \mathbb{Z} _+ \)
shows \( a + b \in \mathbb{Z} _+ \)assumes \( f \in \mathcal{S} _+ \) and \( m\in \mathbb{Z} _+ \) and \( f^{-1}(m) - 1 \in \mathbb{Z} _+ \)
shows \( f(f^{-1}(m) - 1 ) \leq m \), \( f(f^{-1}(m) - 1 ) \neq m \)assumes \( a\in \mathbb{Z} \), \( b\in \mathbb{Z} \), \( c\in \mathbb{Z} \)
shows \( (a - b) + (b - c) = a - c \), \( (a - b) - (a - c) = c - b \), \( a + (b + (c - a - b)) = c \), \( ( - a) - b + c = c - a - b \), \( ( - b) - a + c = c - a - b \), \( ( - (( - a) + b + c)) = a - b - c \), \( a + b + c - a = b + c \), \( a + b - (a + c) = b - c \)assumes \( f \in \mathcal{S} _+ \) and \( \forall m\in \mathbb{Z} _+.\ f^{-1}(m) - 1 \in \mathbb{Z} _+ \)
shows \( \exists U\in \mathbb{Z} .\ \forall m\in \mathbb{Z} _+.\ \forall n\in \mathbb{Z} _+.\ f(f^{-1}(m + n) - f^{-1}(m) - f^{-1}(n)) \leq U \), \( \exists N\in \mathbb{Z} .\ \forall m\in \mathbb{Z} _+.\ \forall n\in \mathbb{Z} _+.\ N \leq f(f^{-1}(m + n) - f^{-1}(m) - f^{-1}(n)) \)assumes \( f\in \mathcal{S} _+ \) and \( K\in \mathbb{Z} \)
shows \( \exists N\in \mathbb{Z} _+.\ \forall m.\ N\leq m \longrightarrow f( - m) \leq K \)assumes \( X\neq 0 \) and \( f: \mathbb{Z} \rightarrow \mathbb{Z} \) and \( \forall a\in \mathbb{Z} .\ \exists b\in \mathbb{Z} _+.\ \forall x.\ b\leq x \longrightarrow a \leq f(x) \) and \( \forall a\in \mathbb{Z} .\ \exists b\in \mathbb{Z} _+.\ \forall y.\ b\leq y \longrightarrow f( - y) \leq a \) and \( \forall x\in X.\ b(x) \in \mathbb{Z} \wedge f(b(x)) \leq U \wedge L \leq f(b(x)) \)
shows \( \exists M.\ \forall x\in X.\ abs(b(x)) \leq M \)assumes \( \forall x\in X.\ b(x) \in Y \)
shows \( \{\langle x,b(x)\rangle .\ x\in X\} : X\rightarrow Y \)assumes \( f \in \mathcal{S} _+ \) and \( g = \{\langle p,f^{-1}(p)\rangle .\ p\in \mathbb{Z} _+\} \)
shows \( g : \mathbb{Z} _+\rightarrow \mathbb{Z} _+ \), \( g : \mathbb{Z} _+\rightarrow \mathbb{Z} \)assumes \( f:X\rightarrow Y \), \( x\in X \) and \( f = \{\langle x,b(x)\rangle .\ x\in X\} \)
shows \( f(x) = b(x) \) and \( b(x)\in Y \)assumes \( f \in \mathcal{S} _+ \) and \( \forall m\in \mathbb{Z} _+.\ f^{-1}(m) - 1 \in \mathbb{Z} _+ \)
shows \( \exists M.\ \forall x\in \mathbb{Z} _+\times \mathbb{Z} _+.\ abs(\varepsilon (f,x)) \leq M \)assumes \( f \in \mathcal{S} _+ \) and \( g = \{\langle p,f^{-1}(p)\rangle .\ p\in \mathbb{Z} _+\} \) and \( p\in \mathbb{Z} _+ \)
shows \( g(p) = f^{-1}(p) \)assumes \( f:\mathbb{Z} _+\rightarrow \mathbb{Z} \) and \( \forall a\in \mathbb{Z} _+.\ \forall b\in \mathbb{Z} _+.\ abs(\delta (f,a,b)) \leq L \)
shows \( \text{OddExtension}(\mathbb{Z} ,IntegerAddition,IntegerOrder,f) \in \mathcal{S} \)assumes \( f \in \mathcal{S} _+ \) and \( \forall m\in \mathbb{Z} _+.\ f^{-1}(m) - 1 \in \mathbb{Z} _+ \) and \( g = \{\langle p,f^{-1}(p)\rangle .\ p\in \mathbb{Z} _+\} \)
shows \( \text{OddExtension}(\mathbb{Z} ,IntegerAddition,IntegerOrder,g) \in \mathcal{S} \)assumes \( f : \mathbb{Z} _+\rightarrow \mathbb{Z} \) and \( a \in \mathbb{Z} _+ \) and \( g = \text{OddExtension}(\mathbb{Z} ,IntegerAddition,IntegerOrder,f) \)
shows \( g(a) = f(a) \)assumes \( s\in \mathcal{S} \), \( M\in \mathbb{Z} \) and \( \forall m\in \mathbb{Z} _+.\ m \leq s(m) \wedge s(m) \leq m + M \)
shows \( s \sim id(\mathbb{Z} ) \)assumes \( f: \mathbb{Z} \rightarrow \mathbb{Z} \) and \( K\in \mathbb{Z} \), \( N\in \mathbb{Z} \) and \( \forall a\in \mathbb{Z} .\ \exists b\in \mathbb{Z} _+.\ \forall x.\ b\leq x \longrightarrow a \leq f(x) \)
shows \( \exists C\in \mathbb{Z} .\ N \leq \text{Minimum}(IntegerOrder,\{n\in \mathbb{Z} _+.\ K \leq f(n) + C\}) \)assumes \( s\in \mathcal{S} \) and \( c\in \mathbb{Z} \) and \( r = \{\langle m,s(m) + c\rangle .\ m\in \mathbb{Z} \} \)
shows \( \forall m\in \mathbb{Z} .\ r(m) = s(m) + c \), \( r\in \mathcal{S} \), \( s \sim r \)assumes \( f \in \mathcal{S} _+ \) and \( \forall m\in \mathbb{Z} _+.\ f^{-1}(m) - 1 \in \mathbb{Z} _+ \)
shows \( \exists h\in \mathcal{S} .\ f\circ h \sim id(\mathbb{Z} ) \)assumes \( f:\mathbb{Z} \rightarrow \mathbb{Z} \) and \( \forall m\in \mathbb{Z} .\ \forall n\in \mathbb{Z} .\ abs(\delta (f,m,n)) \leq L \)
shows \( f\in \mathcal{S} \)assumes \( f\in \mathcal{S} \)
shows \( \exists A B.\ A\in \mathbb{Z} \wedge B\in \mathbb{Z} \wedge (\forall p\in \mathbb{Z} .\ abs(f(p)) \leq A\cdot abs(p) + B) \)assumes \( m \in \mathbb{Z} \)
shows \( \forall n \in \mathbb{Z} .\ (m^S)(n) = m\cdot n \), \( m^S \in \mathcal{S} \)assumes \( m\in \mathbb{Z} \)
shows \( m \leq abs(m) \), \( ( - m) \leq abs(m) \)assumes \( a\in \mathbb{Z} _+ \)
shows \( abs(a) = a \)assumes \( f\in \mathcal{S} \), \( g\in \mathcal{S} \) and \( \forall n\in \mathbb{Z} _+.\ f(n) \leq g(n) \)
shows \( f\sim g \vee g + ( - f) \in \mathcal{S} _+ \)assumes \( a\in \mathbb{Z} \), \( b\in \mathbb{Z} \), \( c\in \mathbb{Z} \)
shows \( a + b + c = a + (b + c) \), \( a\cdot b\cdot c = a\cdot (b\cdot c) \)assumes \( a\leq b \) and \( c\in \mathbb{Z} _+ \)
shows \( a\cdot c \leq b\cdot c \), \( c\cdot a \leq c\cdot b \)assumes \( a\in \mathbb{Z} \) and \( \{a\cdot x.\ x\in \mathbb{Z} \} \in Fin(\mathbb{Z} ) \)
shows \( a = 0 \)assumes \( m \in \mathbb{Z} \)
shows \( ( - m)^S = - (m^S) \)assumes \( m\in \mathbb{Z} \), \( k\in \mathbb{Z} \)
shows \( (m^S) + (k^S) = ((m + k)^S) \)assumes \( s \sim r \)
shows \( s + ( - r) \in \text{FinRangeFunctions}(\mathbb{Z} ,\mathbb{Z} ) \)assumes \( m\in \mathbb{Z} \) and \( m^S \in \text{FinRangeFunctions}(\mathbb{Z} ,\mathbb{Z} ) \)
shows \( m= 0 \)assumes \( m\in \mathbb{Z} \), \( n\in \mathbb{Z} \) and \( m - n = 0 \)
shows \( m=n \)assumes \( x\in X \)
shows \( \{x\} \in Fin(X) \)assumes \( f:X\rightarrow Y \) and \( \{f(x).\ x\in X\} \in Fin(Y) \)
shows \( f \in \text{FinRangeFunctions}(X,Y) \)