List of theorems referencing the symbol ZA
(247) Theorem 201: [The set of integers is an infinite ordinal consisting of all finite ordinals] Ord(Za) & (not Finite(Za)) & ((Card(X) & Finite(X)) •eq (X in Za))
(248) Theorem 202: [All integers are finite ordinals and cardinals] (X in Za) •imp ((X = #X) & Card(X) & Ord(X) & Finite(X))
(249) Theorem 203: [Transitivity of integer comparison] (({M,N} •incin Za) & (I in N)) •imp ((M in N) or (I in M))
(250) Theorem 204: [The set of integers is a Cardinal] Card(Za)
(251) Theorem 205: [The successor of an integer is an integer] (I in Za) •imp (Card(next(I)) & (next(I) in Za))
(252) Theorem 206: [The first few integers are all cardinals] Ord(0) & (0 in Za) & (1 in Za) & (2 in Za) & (3 in Za) & Card(0) & Card(1) & Card(2) & Card(3)
(253) Theorem 207: [The first few integers are all distinct] (0 in Za) & (1 in Za) & (2 in Za) & (3 in Za) & (1 /= 0) & (2 /= 0) & (3 /= 0) & (1 /= 2) & (1 /= 3) & (2 /= 3)
(277) Theorem 230: [Removal of an initial segment from Za yields an infinite set] (N in Za) •imp (not Finite(Za - N))
(293) Theorem 246: [0 is bilateral additive identity] (X in Za) •imp (((X •PLUS 0) = X) & ((0 •PLUS X) = X))
(316) Theorem 269: [Extended division monotonicity lemma] ((M /= 0) & (N in Za)) •imp (((N •OVER M) in Za) & ((N •OVER M) •incin N))
(317) Theorem 270: [Closure properties of arithmetic operators] ((N in Za) & (M in Za)) •imp ((N •PLUS M in Za) & (N •TIMES M in Za) & (N •MINUS M in Za))
(318) Theorem 271: [Strict monotonicity of addition] ((M in Za) & (N in Za) & (N /= 0)) •imp (M in (M •PLUS N))
(320) Theorem 273: [Strict monotonicity of addition] ((M in Za) & (N in Za) & (K in N)) •imp (M •PLUS K in M •PLUS N)
(321) Theorem 274: [Strict monotonicity of addition] ((M in Za) & (N in Za) & (K in N)) •imp (M •PLUS K in M •PLUS N)
(322) Theorem 275: [Strict monotonicity of addition, 2] ((M in Za) & (N in Za) & (K in N)) •imp (K •PLUS M in N •PLUS M)
(323) Theorem 276: [Cancellation] ((M in Za) & (N in Za) & (K in Za) & (M •PLUS K = N •PLUS K)) •imp (M = N)
(326) Theorem 279: [Monotonicity of addition, 3] (M in Za) •imp ((M •incin (I •PLUS M)) & (M •incin (M •PLUS I)) & ((M •PLUS I) notin M) & ((I •PLUS M) notin M))
(328) Theorem 281: [Strict monotonicity of integer multiplication] ((M in N) & (N in Za) & (K in Za) & (K /= 0)) •imp ((M •TIMES K) in (N •TIMES K))
(329) Theorem 282: [The sum of non-negative integers is at least as big at each addend] ((X in Za) & (Y in Za)) •imp ((X •PLUS Y) notin Y)
(330) Theorem 283: [Strict monotonicity of addition] ((M in Za) & (N in Za) & (K in Za)) •imp (((M •PLUS K) •incin (N •PLUS K)) •eq (M •incin N))
(331) Theorem 284: [Strict monotonicity of addition] ((M in Za) & (N in M) & (K in Za)) •imp ((N •PLUS K) in (M •PLUS K))
(332) Theorem 285: [Subtraction Lemma] (N in Za) •imp ((N •MINUS M) in Za)
(333) Theorem 286: [Strict monotonicity of subtraction] ((N in Za) & (M in Za) & (K in N) & (M incs N)) •imp ((M •MINUS N) in (M •MINUS K))
(336) Theorem 289: [Strict monotonicity of subtraction, 2] ((N in Za) & (M in Za) & (K in M) & (K incs N)) •imp ((K •MINUS N) in (M •MINUS N))
(337) Theorem 290: [Addition-subtraction commutativity] ((M in Za) & (N in Za) & (K in Za) & (N incs M) & ((N •MINUS M) incs K)) •imp ((N incs (M •PLUS K)) & (N •MINUS (M •PLUS K) = (N •MINUS M) •MINUS K))
(338) Theorem 291: [Subtraction reverses addition] ((M in Za) & (N in Za)) •imp ((M •PLUS N) •MINUS N = M)
(340) Theorem 293: [Integer division with remainder] ((M in Za) & (N in Za) & (N /= 0)) •imp (((M •OVER N) in Za) & (M incs ((M •OVER N) •TIMES N)) & ((M •MOD N) in N))
(344) Theorem 297: [Strong monotonicity of integer addition] ((N in Za) & (M in Za) & (K in Za)) •imp ((N incs M) •eq ((N •PLUS K) incs (M •PLUS K)))
(346) Theorem 299: [Addition-subtraction commutativity, 2] ((N in Za) & (M in Za) & (K in Za) & (N incs M)) •imp ((N •PLUS K) •MINUS (M •PLUS K) = N •MINUS M)
(347) Theorem 300: [Addition-subtraction lemma] ((N in Za) & (M in Za)) •imp (N = (M •PLUS (N •MINUS M)) or N = (M •MINUS (M •MINUS N)))
(349) Theorem 302: [The successor integer as a sum, 2] (N in Za) •imp ((next(N) in Za) & ((N •PLUS 1) = next(N)))
(350) Theorem 303: [The union set of a finite collection of integers is an integer] ((M •incin Za) & Finite(M)) •imp (((M /= 0) •imp (Un(M) in M)) & (Un(M) in Za))
(351) Theorem 304: [The union set of a set of integers is the least upper bound of its elements] (M in Za) •imp (((Un(M) in Za) & (Un(M) •incin M)) & ((M /= 0) •imp (Un(M) in M)))
(352) Theorem 305: [Every nonzero integer has a predecessor] ((M in Za) & (M /= 0)) •imp (M = (Un(M) •PLUS 1))
(353) Theorem 306: [The sum of integers as the union of smaller sums] ((X in Za) & (Y in Za)) •imp ((X •PLUS Y) = X + {(X •PLUS u): u in Y})
(354) Theorem 307: [The sum of integers as the union of smaller sums, 2] ((X in Za) & (Y in Za)) •imp ((X •PLUS Y) = X + {(u •PLUS X): u in Y})
(355) Theorem 308: [Subtraction reverses addition] ((X in Za) & (Y in Za) & (Y •incin X)) •imp (X = Y •PLUS (X •MINUS Y))
(356) Theorem 309: [Subtraction monotonicity lemma, 2] ((X in Za) & (Y in Za) & (U in (X •PLUS Y)) & (Y /= 0)) •imp ((U •MINUS X) in Y)
(357) Theorem 310: [The integer difference as a set of smaller differences] ((N in Za) & (M in Za)) •imp ((N •MINUS M) = {k •MINUS M: k in N | M •incin k})
(358) Theorem 311: [The integer difference as a set of smaller differences] ((N in Za) & (M in Za)) •imp ((N •MINUS M) = {k in Za | (k •PLUS M) in N})
(359) Theorem 312: ((J in Za - X) & (FORALL i | (next(i) in X) •imp (i in X))) •imp ({h in Za | (h notin J) & (h in X)} = 0)
(360) Theorem 313: ((X •incin Za) & (FORALL i | (next(i) in X) •imp (i in X))) •eq (X in next(Za))
(361) Theorem 314: (({X,Y} •incin next(Za)) & (#X in next(Y))) •imp (((X = Y) & (Y = Za)) or (X in (next(Y) * Za)))
(362) Theorem unsigned_integer_bynd.0: [Every finite set of unsigned integers has an upper bound] (bynd_thryvar in Za) & (FORALL i in Za | (Q1(i) •imp (i in bynd_thryvar)))
(363) Theorem unsigned_integer_bynd.1: [Every finite set of unsigned integers has an upper bound] (bynd_thryvar in Za) & (Za incs bynd_thryvar) & Ord(bynd_thryvar) & (FORALL i in Za | (Q1(i) •imp (i in bynd_thryvar))) & (not Finite(Za - bynd_thryvar))
(364) Theorem cauchyseq_lemma.1: (not Finite({i * j : i in (Za - n0), j in (Za - n0) | R(i,j)}))
(366) Theorem 316: [Integer member maximum and minimum] ((S in Za) & (T in Za)) •imp ((S + T in Za) & (S * T in Za))
(367) Theorem cauchyseq_lemma2.1: (EXISTS k in Za | (FORALL i in Za, j in Za | ((i incs k) & (j incs k)) •imp (not (R(i,j)))))
(368) Theorem 317: ((N in Za) & (S •incin N) & (#S = N)) •imp (S = N)
(369) Theorem 318: [Finite sequences are single_valued maps with integer domains] (F in Fin_seqs(S)) •eq (Svm(F) & (domain(F) in Za) & (range(F) •incin S))
(370) Theorem 319: [Other properties of finite sequences] (F in Fin_seqs(S)) •imp ((domain(F) = #domain(F)) & (domain(F) = #F) & (#F in Za) & Finite(F))
(373) Theorem 322: [The shift-map of an integer is single-valued and maps Za into Za] ((M in Za) & (N in Za)) •imp (Svm(Shift(M)) & (domain(Shift(M)) = Za) & (range(Shift(M)) •incin Za) & (Shift(M)~[N] = M •PLUS N))
(374) Theorem 323: [Composition of shift-maps yields a shift-map] ((M in Za) & (N in Za)) •imp (Shift(M) @ Shift(N) = Shift(M •PLUS N))
(375) Theorem 324: [Double shifting can be emulated by a single shift] ((M in Za) & (N in Za)) •imp (shifted_seq(shifted_seq(F,M),N) = shifted_seq(F,M •PLUS N))
(376) Theorem 325: [Shift(0) is the identity map on Za] (Shift(0) = {[n,n]: n in Za}) & ((Is_map(F) & (domain(F) •incin Za)) •imp (F @ Shift(0) = F))
(377) Theorem 326: [Shift-by-0 is the identity map on sequences] (Is_map(F) & (domain(F) •incin Za)) •imp (shifted_seq(F,0) = F)
(378) Theorem 327: [Form of a shifted sequence] ((M in Za) & (domain(F) •incin Za)) •imp (shifted_seq(F,M) = {[car(x) •MINUS M,cdr(x)]: x in F | car(x) incs M})
(380) Theorem 329: ((F in Fin_seqs(S)) & (M in Za)) •imp (((F •ON M) in Fin_seqs(S)) & (shifted_seq(F,M) in Fin_seqs(S)) & (domain(shifted_seq(F,M)) = (#F •MINUS M)))
(385) Theorem subseq.1: (g = (f @ h_thryvar)) & one_1_map(h_thryvar) & (domain(h_thryvar) in next(Za)) & (range(h_thryvar) •incin domain(f)) & (FORALL i in domain(h_thryvar), j in domain(h_thryvar) | (i in j) •imp ((h_thryvar~[i]) in (h_thryvar~[j])))
(387) Theorem subseq.3: Svm(g) & (g •incin (domain(f) •PROD range(f))) & (domain(g) in (next(Za) * next(domain(f))))
(388) Theorem subseq.4: (domain(h_thryvar) /= Za) •imp Finite(g)
(390) Theorem 335: (M in Za) •imp (shifted_seq(F,M) in Subseqs(F))
(391) Theorem 336: ((F in Fin_seqs(S)) & (M in Za)) •imp ((shifted_seq(F,M) in Fin_seqs(S)) & (domain(shifted_seq(F,M)) in next(domain(F))))
(392) Theorem 337: ((domain(F) = Za) & (M in Za)) •imp (domain(shifted_seq(F,M)) = Za)
(442) Theorem 349: [Reduced form of an integer pair] ((M in Za) & (N in Za)) •imp ((Red([M,N]) in Si) & (M * N in Za))
(443) Theorem 350: [Embedding of integers in the signed integers] (N in Za) •imp (([N,0] in Si) & ([0,N] in Si))
(445) Theorem 352: [The signed integers as integer pairs with one component equal to 0] (N in Si) •imp ((N = [car(N),cdr(N)]) & (car(N) = 0 or cdr(N) = 0) & (car(N) in Za) & (cdr(N) in Za) & (Red(N) = N) & (car(N) * cdr(N) = 0))
(446) Theorem 353: [Signed integers as integer pairs, 2] (N in Si) •imp ((N = [car(N),0] or N = [0,cdr(N)]) & (car(N) = 0 or cdr(N) = 0) & (car(N) in Za) & (cdr(N) in Za) & (Red(N) = N) & (car(N) * cdr(N) = 0))
(449) Theorem 356: [Reduction of an integer pair (n,n) always gives the signed 0 value] (N in Za) •imp (Red([N,N]) = [0,0])
(450) Theorem 357: [Reduction removes any common value added to the components of an integer pair] ((J in Za) & (K in Za) & (M in Za)) •imp (Red([J •PLUS M,K •PLUS M]) = Red([J,K]))
(451) Theorem 358: [The intersection of two unsigned integers is the smaller of the two] ((N in Za) & (M in Za)) •imp (((N * M) in Za) & ((N * M) in {N,M}) & ((N •MINUS (N * M)) in Za) & ((M •MINUS (N * M)) in Za))
(452) Theorem 359: [The signed sum of two integer pairs is the sum of the first with the reduced form of the second] ((J in Za) & (K in Za) & (N in Za) & (M in Za)) •imp ([J,K] •S_PLUS [N,M] = [J,K] •S_PLUS Red([N,M]))
(453) Theorem 360: [The sum of a signed integer and an integer pair remains the same if the pair is reduced] ((K in Si) & (N in Za) & (M in Za)) •imp (K •S_PLUS [N,M] = K •S_PLUS Red([N,M]))
(454) Theorem 361: [The product of a signed integer and an integer pair remains the same if the pair is reduced] ((K in Si) & (N in Za) & (M in Za)) •imp (K •S_TIMES [N,M] = K •S_TIMES Red([N,M]))
(455) Theorem 362: [Commutativity lemma for signed integers] ((K in Si) & (N in Za) & (M in Za)) •imp (K •S_PLUS [N,M] = [N,M] •S_PLUS K)
(456) Theorem 363: [Commutativity lemma for signed integers, 2] ((J in Za) & (K in Za) & (N in Za) & (M in Za)) •imp ([J,K] •S_PLUS [N,M] = [N,M] •S_PLUS [J,K])
(458) Theorem 365: [The sum of two integer pairs remains the same if the first is reduced] ((J in Za) & (K in Za) & (N in Za) & (M in Za)) •imp ([J,K] •S_PLUS [N,M] = Red([J,K]) •S_PLUS [N,M])
(459) Theorem 366: [The sum of two integer pairs remains the same if both are reduced] ((J in Za) & (K in Za) & (N in Za) & (M in Za)) •imp ([J,K] •S_PLUS [N,M] = Red([J,K]) •S_PLUS Red([N,M]))
(463) Theorem 370: [Reduction of a pair (N,0) gives (N,0)] (N in Za) •imp (Red([N,0]) = [N,0])
(464) Theorem 371: [Embedding of Integers in Signed Integers] ((N in Za) & (M in Za)) •imp (([N •PLUS M,0] = [N,0] •S_PLUS [M,0] & [N •TIMES M,0] = [N,0] •S_TIMES [M,0]) & ((N incs M) •imp ([N,0] •S_MINUS [M,0] = [N •MINUS M,0])))
(465) Theorem 372: [Sign-reversal of signed integers] ((N in Za) & (M in Za)) •imp (S_Rev(Red([M,N])) = Red([N,M]))
(470) Theorem 377: [Associativity lemma] ((N in Za) & (M in Za) & (K in Za)) •imp ([N,0] •S_TIMES ([M,0] •S_TIMES [K,0]) = ([N,0] •S_TIMES [M,0]) •S_TIMES [K,0])
(471) Theorem 378: [Associativity lemma] ((K in Si) & (N in Za) & (M in Za)) •imp ([N,0] •S_TIMES ([M,0] •S_TIMES K) = ([N,0] •S_TIMES [M,0]) •S_TIMES K)
(472) Theorem 379: [Associativity lemma II] ((K in Si) & (N in Za) & (M in Si)) •imp ([N,0] •S_TIMES (M •S_TIMES K) = ([N,0] •S_TIMES M) •S_TIMES K)
(487) Theorem mathematical_induction00: [Basic assumption for proofs by mathematical induction] (n in Za) & P(n)
(488) Theorem mathematical_induction0: [The minimum integer having a given property, preliminary version] (FORALL k | ((m_thryvar in Za) & P(m_thryvar)) & ((k in m_thryvar) •imp (not ((k in Za) & P(k)))))
(489) Theorem mathematical_induction1: [The minimum integer having a given property] (m_thryvar in Za) & P(m_thryvar) & (FORALL k in m_thryvar | not P(k))
(494) Theorem double_mathematical_induction.0: [Basic assumption for double integer induction] (EXISTS i | (i in Za) & R(n,i))
(494+) Theorem double_mathematical_induction.1: [Minimum first element for a double integer induction] (mm_thryvar in Za) & (EXISTS i | (i in Za) & R(mm_thryvar,i)) & (FORALL k in mm_thryvar | not (EXISTS i | (i in Za) & R(k,i)))
(495) Theorem double_mathematical_induction.2: (EXISTS i | (i in Za) & R(mm_thryvar,i))
(495+) Theorem double_mathematical_induction.3: (ei in Za) & R(mm_thryvar,ei)
(496) Theorem double_mathematical_induction.4: (FORALL i | (j_thryvar in Za) & R(mm_thryvar,j_thryvar) & ((i in j_thryvar) •imp (not ((i in Za) & R(mm_thryvar,i)))))
(497) Theorem double_mathematical_induction.5: (mm_thryvar in Za) & (j_thryvar in Za) & R(mm_thryvar,j_thryvar) & (((K in mm_thryvar) & (I in Za)) •imp (not R(K,I))) & ((I in j_thryvar) •imp (not R(mm_thryvar,I)))
(498) Theorem confinedIncrSeq1: [global increase of a stepwise increasing sequence] ((I in J) & (J in Za)) •imp (e(I) •incin e(J))
(498+) Theorem confinedIncrSeq2: [position of first repetition in confined increasing sequence] (m_thryvar in Za) & (e(next(m_thryvar)) = e(m_thryvar)) & ((m_thryvar * {i in Za | e(next(i)) •incin e(i)}) = 0)
(667) Theorem 521: [The range of a rational sequence is included in the set of rationals] (F in RaSeq) •imp ((domain(F) = Za) & (range(F) •incin Ra) & ((X in Za) •imp (F~[X] in Ra)))
(668) Theorem 522: [Reformulation of condition for sequence equivalence] ({F,G} •incin RaSeq) •imp (Ra_eqseq(F,G) •eq (FORALL eps in Ra | (eps •Ra_GT Ra_0) •imp Finite({x : x in Za | Ra_ABS((F~[x]) •Ra_MINUS (G~[x])) •Ra_GT eps})))
(669) Theorem 523: [Condition for rational sequence equality] (FORALL n in Za | ((F in RaSeq) & (G in RaSeq) & (F~[n] = G~[n]))) •imp (F = G)
(675) Theorem 524: (X in Ra) •imp ((Za •PROD {X}) in RaCauchy)
(676) Theorem 525: (X in Ra) •imp (Ras_ABS(Za •PROD {X}) = (Za •PROD {Ra_ABS(X)}))
(678) Theorem 527: (F in RaSeq) •imp ((domain(F) = Za) & Svm(F) & (range(F) •incin Ra) & Ra_eqseq(F,F))
(679) Theorem 528: ((F in RaSeq) & (N in Za) & (I in Za)) •imp ((shifted_seq(F,N)~[I]) = (F~[N •PLUS I]))
(680) Theorem 529: (U in Za) •imp (((Ra0Seq~[U]) = Ra_0) & ((Ra1Seq~[U]) = Ra_1))
(682) Theorem 531: (F in RaCauchy) •imp ((H in Za) •imp (F~[H] in Ra))
(683) Theorem 532: ((Eps in Ra) & (Eps •Ra_GT Ra_0) & (F in RaCauchy)) •imp (EXISTS k in Za | (FORALL i in Za, j in Za | ((i notin k) & (j notin k)) •imp (not (Ra_ABS((F~[i]) •Ra_MINUS (F~[j]))) •Ra_GT Eps)))
(684) Theorem 533: ((Eps in Ra) & (Eps •Ra_GT Ra_0) & (F in RaCauchy)) •imp (EXISTS k in Za | (FORALL i in Za, j in Za | ((i notin k) & (j notin k)) •imp (Eps •Ra_GT (Ra_ABS((F~[i]) •Ra_MINUS (F~[j])))) ))
(686) Theorem 535: ({F,G} •incin RaSeq) •imp (((F •Ras_PLUS G) in RaSeq) & (Ras_ABS(G) in RaSeq) & (Ras_Rev(G) in RaSeq) & ((F •Ras_TIMES G) in RaSeq) & ((F •Ras_PLUS G) = {[u,((F~[u]) •Ra_PLUS (G~[u]))]: u in Za}) & (Ras_ABS(G) = {[u,Ra_ABS(G~[u])]: u in Za}) & (Ras_Rev(G) = {[u,Ra_Rev(G~[u])]: u in Za}) & ((F •Ras_TIMES G) = {[u,((F~[u]) •Ra_TIMES (G~[u]))]: u in Za}))
(687) Theorem 536: (({F1,G1} •incin RaSeq) & (N in Za)) •imp ((F1~[N] in Ra) & (G1~[N] in Ra) & ((F1 •Ras_PLUS G1 in RaSeq) & ((F1 •Ras_PLUS G1)~[N] = (F1~[N]) •Ra_PLUS (G1~[N]))) & (((Ras_ABS(G1) in RaSeq) & (Ras_ABS(G1)~[N] = Ra_ABS(G1~[N])))) & (((Ras_Rev(G1) in RaSeq) & (Ras_Rev(G1)~[N] = Ra_Rev(G1~[N])))) & (((F1 •Ras_TIMES G1 in RaSeq) & (F1 •Ras_TIMES G1)~[N] = ((F1~[N]) •Ra_TIMES (G1~[N])))))
(690) Theorem 539: [Every finite set of integers has a strict upper bound] ((S •incin Za) & Finite(S)) •imp (EXISTS u in Za | (FORALL y in S | y in u))
(694) Theorem 543: ((G in RaCauchy) & (not Ra_eqseq(G,Ra0Seq))) •imp (EXISTS eps in Ra | (eps •Ra_GT Ra_0) & Finite({i in Za | eps •Ra_GE Ra_ABS(G~[i])}))
(695) Theorem 544: ((G in RaCauchy) & (not Ra_eqseq(G,Ra0Seq))) •imp (EXISTS eps in Ra, n in Za | (eps •Ra_GT Ra_0) & (FORALL i in (Za - n) | (Ra_ABS(G~[i]) •Ra_GT eps) & (Ra_ABS(G~[i]) •Ra_GT Ra_0)) & (Ra_ABS(G~[n]) •Ra_GT Ra_0))
(696) Theorem 545: ((H in RaCauchy) & (not Ra_eqseq(H,Ra0Seq))) •imp (EXISTS eps in Ra, n in Za | (eps •Ra_GT Ra_0) & (FORALL i in (Za - n) | Ra_ABS(H~[i]) •Ra_GT eps) & (FORALL i in Za, j in Za | ((i notin n) & (j notin n)) •imp (eps •Ra_GT (Ra_ABS((H~[i]) •Ra_MINUS (H~[j]))))))
(697) Theorem 546: ((G in RaCauchy) & (not Ra_eqseq(G,Ra0Seq))) •imp ({h in Za | (FORALL i in (Za - h) | (G~[i]) /= Ra_0)} /= 0)
(698) Theorem 547: ((F in RaSeq) & (M = arb({h in Za | (FORALL i in (Za - h) | (F~[i]) /= Ra_0)}))) •imp (Ras_Recip(F) = Ras_Recip(shifted_seq(F,M)))
(699) Theorem 548: ((F in RaCauchy) & (M in Za)) •imp ((shifted_seq(F,M) in RaCauchy) & Ra_eqseq(F,shifted_seq(F,M)))
(700) Theorem 549: ((F in RaCauchy) & (not Ra_eqseq(F,Ra0Seq))) •imp (EXISTS g in RaCauchy | Ra_eqseq(F,g) & (Ras_Recip(F) = Ras_Recip(g)) & (FORALL i in Za | ((g~[i]) /= Ra_0) & (Ras_Recip(g)~[i] = Recip(g~[i]))))
(730) Theorem 579: [All terms of a Cauchy sequence not equivalent to zero have the same sign and have an absolute value bounded below beyond a certain point] ((F in RaCauchy) & (not Ra_eqseq(F,Ra0Seq))) •imp (EXISTS eps in Ra, n in Za | (eps •Ra_GT Ra_0) & (FORALL i in (Za - n) | (Ra_ABS(F~[i]) •Ra_GT eps) & (Ra_ABS(F~[i]) = if ((F~[n]) •Ra_GE Ra_0) then (F~[i]) else Ra_Rev(F~[i]) end if) ))
(731) Theorem 580: [All terms of a Cauchy sequence not equivalent to zero have the same sign beyond a certain point] ((F in RaCauchy) & (not Ra_eqseq(F,Ra0Seq))) •imp (EXISTS n in Za | shifted_seq(Ras_ABS(F),n) = if ((F~[n]) •Ra_GE Ra_0) then shifted_seq(F,n) else shifted_seq(Ras_Rev(F),n) end if)
(855) Theorem 702: (X in Ra) •imp (Ra_is_nonneg(X) •eq Ra_eqseq(Za •PROD {Ra_ABS(X)},Za •PROD {X}))
(856) Theorem 703: (X in Ra) •imp (R_is_nonneg(Cauchy_to_Re(Za •PROD {X})) •eq (ReRa(Ra_ABS(X)) = ReRa(X)))
(864) Theorem 710a: [The images of rationals via the embedding form a dense subset of the reals, 1] ((X in Re) & (Eps in Ra) & (Eps •Ra_GT Ra_0)) •imp (EXISTS y in Ra | Finite({m in Za | Ra_ABS(((arb(X))~[m]) •Ra_MINUS y) •Ra_GE Eps}) )
(870) Theorem 717: [The embedding of integers into signed integers preserves all elementary algebraic operations on integers] ((X in Za) & (Y in Za)) •imp ((SiZa(X) in Si) & (SiZa(Y) in Si) & (SiZa(X •PLUS Y) = SiZa(X) •S_PLUS SiZa(Y)) & (SiZa(X •TIMES Y) = SiZa(X) •S_TIMES SiZa(Y)))
(871) Theorem 718: [The embedding of integers into signed integers is 1-1] ((X in Za) & (Y in Za) & (SiZa(X) = SiZa(Y))) •imp (X = Y)
(873) Theorem 720: [The embedding of integers into signed integers preserves ordering] ((X in Za) & (Y in Za)) •imp (((SiZa(X) •S_GE SiZa(Y)) •eq (X incs Y)) & ((SiZa(X) •S_GT SiZa(Y)) •eq (Y in X)) & ((SiZa(Y) •S_LE SiZa(X)) •eq (Y •incin X)) & ((SiZa(Y) •S_LT SiZa(X)) •eq (Y in X)))
(886) Theorem 731: [For any rational r, there exists an integer n such that n >= r] (r in Ra) •imp (EXISTS n in Za | RaSi(SiZa(n)) •R_GE x)
(887) Theorem 732: [For any real x, there exists an integer n such that n > x] (x in Re) •imp (EXISTS n in Za | ReRa(RaSi(SiZa(n))) •R_GT x)
(888) Theorem 733: [For any real x and eps > 0, there exists an integer n such that n • eps > x] ((x in Re) & (eps in Re) & (eps •R_GT R_0)) •imp (EXISTS n in Za | ((ReRa(RaSi(SiZa(n))) •R_TIMES e) •R_GT x))
(889) Theorem 734: [For any real x and eps > 0, there exists an integer n such that eps > x/n] ((x in Re) & (eps in Re) & (eps •R_GT R_0)) •imp (EXISTS n in Za | (eps •R_GT (x •R_OVER ReRa(RaSi(SiZa(n))))))
(890) Theorem 735: [For any non-negative real x and eps > 0, there exists an integer n such that n •R_TIMES eps > x and (n - 1) • eps <= x] ((x in Re) & (eps in Re) & (eps •R_GT R_0)) •imp (EXISTS n in Za | (e •R_GT (x •R_OVER ReRa(RaSi(SiZa(n))))))
(891) Theorem 736: [Every positive real is bounded below by a rational fraction of the form 1/n] ((x in Re) & (x •R_GT R_0)) •imp (EXISTS n in Za | (R_1 •R_OVER ReRa(RaSi(SiZa(n)))) •R_LT x)
(897) Theorem 742: ((N in Za) & (X in Re)) •imp (X •ToThe N = if (N = 0) then R_1 else X •R_TIMES (X •ToThe (N - 1)) end if)
(898) Theorem 743: (X in Re) •imp ((X •ToThe 0 = R_0) & (X •ToThe 1 = X) & (((M in Za) & (N in Za)) •imp (X •ToThe (M •PLUS N) = (X •ToThe M) •R_TIMES (X •ToThe N))))
(899) Theorem 744: ((X in Re) & (M in Za) & (N in Za)) •imp (((X •ToThe M) •ToThe N) = (X •ToThe (M •TIMES N)))