List of theorems referencing the symbol RA
(551) Theorem 403: [Fractions are equivalent if and only if the rational numbers they define are equal] (FORALL x, y | ((x in Fr) & (y in Fr)) •imp ((Same_frac(x,y) •eq (Fr_to_Ra(x) = Fr_to_Ra(y))))) & (FORALL x | (x in Ra) •imp ((arb(x) in Fr) & (Fr_to_Ra(arb(x)) = x))) & (FORALL x | (x in Fr) •imp (Fr_to_Ra(x) in Ra)) & (FORALL x | (x in Fr) •imp Same_frac(x,arb(Fr_to_Ra(x))))
(552) Theorem 404: [Every fraction is equivalent to every member of its rational number class] (X in Fr) •imp ((Fr_to_Ra(X) in Ra) & Same_frac(X,arb(Fr_to_Ra(X))))
(554) Theorem 406: [Alternate version of Theorem 404] (Y in Ra) •imp ((arb(Y) in Fr) & (Fr_to_Ra(arb(Y)) = Y))
(566) Theorem 416: [Rational numbers are classes of pairs of signed integers] (N in Ra) •imp ((arb(N) in Fr) & (arb(N) = [car(arb(N)),cdr(arb(N))]) & (car(arb(N)) in Si) & (cdr(arb(N)) in Si) & (cdr(arb(N)) /= [0,0]))
(570) Theorem 421: [The sum of a rational number and a formal fraction can be expressed as a sum of formal fractions] ((X in Ra) & (Y in Si) & (Z in Si) & (Z /= [0,0])) •imp (X •Ra_PLUS Fr_to_Ra([Y,Z]) = Fr_to_Ra([(car(arb(X)) •S_TIMES Z) •S_PLUS (cdr(arb(X)) •S_TIMES Y),(cdr(arb(X)) •S_TIMES Z)]))
(571) Theorem 422: [The product of a rational number and a formal fraction can be expressed as a product of formal fractions] ((X in Ra) & (Y in Si) & (Z in Si) & (Z /= [0,0])) •imp (X •Ra_TIMES Fr_to_Ra([Y,Z]) = Fr_to_Ra([car(arb(X)) •S_TIMES Y,cdr(arb(X)) •S_TIMES Z]))
(577) Theorem 428: [Commutativity of rational addition] ((N in Ra) & (M in Ra)) •imp ((N •Ra_PLUS M in Ra) & (N •Ra_PLUS M = M •Ra_PLUS N))
(578) Theorem 429: [?] ((X in Ra) & (Y in Si) & (Z in Si) & (Z /= [0,0])) •imp (Fr_to_Ra([Y,Z]) •Ra_PLUS X = Fr_to_Ra([(car(arb(X)) •S_TIMES Z) •S_PLUS (cdr(arb(X)) •S_TIMES Y),(cdr(arb(X)) •S_TIMES Z)]))
(579) Theorem 431: [Commutativity of rational multiplication] ((N in Ra) & (M in Ra)) •imp ((N •Ra_TIMES M in Ra) & (N •Ra_TIMES M = M •Ra_TIMES N))
(580) Theorem 432: [?] ((X in Ra) & (Y in Si) & (Z in Si) & (Z /= [0,0])) •imp ((Fr_to_Ra([Y,Z]) •Ra_TIMES X) = Fr_to_Ra([car(arb(X)) •S_TIMES Y,cdr(arb(X)) •S_TIMES Z]))
(581) Theorem 433: [Associative law for rational addition] ((K in Ra) & (N in Ra) & (M in Ra)) •imp (N •Ra_PLUS (M •Ra_PLUS K) = (N •Ra_PLUS M) •Ra_PLUS K)
(582) Theorem 434: [The zero rational is the identity for rational addition] (Ra_0 in Ra) & (Ra_1 in Ra) & ((M in Ra) •imp (M = M •Ra_PLUS Ra_0))
(583) Theorem 435: [The sum of a rational number and its additive inverse is zero] (M in Ra) •imp ((Ra_Rev(M) in Ra) & ((M •Ra_PLUS Ra_Rev(M)) = Ra_0))
(584) Theorem 436: [The sum of a rational number and its additive inverse is zero, 2] (M in Ra) •imp ((Ra_Rev(M) in Ra) & ((Ra_Rev(M) •Ra_PLUS M) = Ra_0))
(585) Theorem 437: [The difference of two rationals is rational] ((N in Ra) & (M in Ra)) •imp ((N •Ra_MINUS M) in Ra)
(586) Theorem 438: [Rational subtraction is equivalent to addition of the rational negative] ((N in Ra) & (M in Ra)) •imp (N = M •Ra_PLUS (N •Ra_MINUS M))
(587) Theorem 439: [Associative law for rational multiplication] ((K in Ra) & (N in Ra) & (M in Ra)) •imp (N •Ra_TIMES (M •Ra_TIMES K) = (N •Ra_TIMES M) •Ra_TIMES K)
(589) Theorem 441: [Distributive law for rationals] ((K in Ra) & (N in Ra) & (M in Ra)) •imp (N •Ra_TIMES (M •Ra_PLUS K) = (N •Ra_TIMES M) •Ra_PLUS (N •Ra_TIMES K))
(592) Theorem 444: [The unit rational is the rational multiplicative identity] (M in Ra) •imp (M = M •Ra_TIMES Ra_1)
(593) Theorem 445: [Multiplication of a rational by its reciprocal gives 1] ((M in Ra) & (M /= Ra_0)) •imp ((Recip(M) in Ra) & (M •Ra_TIMES Recip(M) = Ra_1))
(594) Theorem 446: ((N in Ra) & (M in Ra) & (M /= Ra_0)) •imp (((N •Ra_TIMES (M •Ra_TIMES M)) •Ra_TIMES (Recip(M) •Ra_TIMES Recip(M))) = N)
(595) Theorem 447: [Rational division is multiplication by the reciprocal] ((N in Ra) & (M in Ra) & (M /= Ra_0)) •imp (N = M •Ra_TIMES (N •Ra_OVER M))
(597) Theorem 449: [One of a rational and its additive inverse is always non-negative, and both are non-negative only if the rational is zero] (X in Ra) •imp ((Ra_is_nonneg(X) or Ra_is_nonneg(Ra_Rev(X))) & ((Ra_is_nonneg(X) & Ra_is_nonneg(Ra_Rev(X))) •imp (X = Ra_0)))
(598) Theorem 450: [?] (FORALL x,y | ((x •Ra_GE y) •eq Ra_is_nonneg(x •Ra_PLUS Ra_Rev(y)))) & (FORALL x,y | ((x •Ra_LE y) •eq (y •Ra_GE x))) & (FORALL x,y | ((x •Ra_GT y) •eq ((x •Ra_GE y) & (x /= y)))) & (FORALL x,y | ((x •Ra_LT y) •eq (y •Ra_GT x))) & (FORALL x,y | ((x •Ra_LE y) •eq Ra_is_nonneg(y •Ra_PLUS Ra_Rev(x)))) & (FORALL x,y | (((x in Ra) & (y in Ra)) •imp ((x •Ra_GT y) •eq (Ra_is_nonneg(x •Ra_PLUS Ra_Rev(y)) & (x /= y))))) & (FORALL x,y | (((y in Ra) & (y in Ra)) •imp ((x •Ra_GT y) •eq (Ra_is_nonneg(x •Ra_MINUS y) & (x /= y))))) & (FORALL x,y | (((x in Ra) & (y in Ra) & ((x = y) or (not(x •Ra_GE y)))) •imp (y •Ra_GE x)))
(599) Theorem 451: [Various basic properties of rational comparison] ((X •Ra_GE Y) •eq Ra_is_nonneg(X •Ra_PLUS Ra_Rev(Y))) & ((X •Ra_LE Y) •eq (Y •Ra_GE X)) & ((X •Ra_GT Y) •eq ((X •Ra_GE Y) & (X /= Y))) & ((X •Ra_LT Y) •eq (Y •Ra_GT X)) & ((X •Ra_LE Y) •eq Ra_is_nonneg(Y •Ra_PLUS Ra_Rev(X))) & (((X in Ra) & (Y in Ra)) •imp ((X •Ra_GT Y) •eq (Ra_is_nonneg(X •Ra_PLUS Ra_Rev(Y)) & (X /= Y)))) & (((X in Ra) & (Y in Ra)) •imp ((X •Ra_GT Y) •eq (Ra_is_nonneg(X •Ra_MINUS Y) & (X /= Y)))) & (((X in Ra) & (Y in Ra) & ((X = Y) or (not(X •Ra_GE Y)))) •imp (Y •Ra_GE X))
(600) Theorem 452: [Greater_than_equal is greater-than and equal] ((X in Ra) & (Y in Ra)) •imp ((X •Ra_GE Y) •eq ((X •Ra_GT Y) or (X = Y)))
(601) Theorem 453: [Less_than_equal is less-than and equal] ((X in Ra) & (Y in Ra)) •imp ((X •Ra_LE Y) •eq ((X •Ra_LT Y) or (X = Y)))
(602) Theorem 454: [The rationals are a linearly ordered set] ((X in Ra) & (Y in Ra)) •imp ((X •Ra_GT Y) or (X = Y) or (Y •Ra_GT X))
(603) Theorem 455: [The rationals are a linearly ordered set, 2] ((X in Ra) & (Y in Ra)) •imp ((X •Ra_LT Y) or (X = Y) or (Y •Ra_LT X))
(604) Theorem 456: [The rationals are a linearly ordered set,3] ((X in Ra) & (Y in Ra)) •imp ((X •Ra_GT Y) or (Y •Ra_GE X))
(605) Theorem 457: [The rationals are a linearly ordered set,4] ((X in Ra) & (Y in Ra)) •imp ((X •Ra_LT Y) or (Y •Ra_LE X))
(606) Theorem 458: [The unit rational is the identity for multiplication] (X in Ra) •imp (X = X •Ra_TIMES Ra_1)
(607) Theorem 459: [The zero rational is represented by any fraction whose numerator is 0] (X in Ra) •imp ((X = Ra_0) •eq (car(arb(X)) = [0,0]))
(608) Theorem 460: [The sum and product of two non-negative rationals is non-negative] ((X in Ra) & (Y in Ra) & Ra_is_nonneg(X) & Ra_is_nonneg(Y)) •imp (Ra_is_nonneg(X •Ra_PLUS Y) & Ra_is_nonneg(X •Ra_TIMES Y))
(609) Theorem 461: [Transitivity of ordering] ((X in Ra) & (Y in Ra) & (Z in Ra)) •imp (((X •Ra_GE Y) & (Y •Ra_GE Z)) •imp (X •Ra_GE Z))
(611) Theorem 463: [Alternate characterization of non-negativity for rationals] (X in Ra) •imp ((Ra_is_nonneg(X) •eq (X •Ra_GE Ra_0)) & ((X •Ra_GT Ra_0) •imp Ra_is_nonneg(X)))
(614) Theorem 466: [First law of signs for rational multiplication] ((X in Ra) & (Y in Ra)) •imp ((X •Ra_TIMES Ra_Rev(Y)) = Ra_Rev(X •Ra_TIMES Y))
(615) Theorem 467: [The reverse of a rational X is the reverse of 1, times X] (X in Ra) •imp (Ra_Rev(X) = (Ra_Rev(Ra_1) •Ra_TIMES X))
(616) Theorem 468: ((X in Ra) & (Y in Ra) & (Z in Ra)) •imp ((X •Ra_TIMES (Y •Ra_MINUS Z)) = (X •Ra_TIMES Y) •Ra_MINUS (X •Ra_TIMES Z))
(617) Theorem 469: [Strict monotonicity of rational multiplication over 1st argument] ((X in Ra) & (Y in Ra) & (X1 in Ra) & (X •Ra_GT Y) & (X1 •Ra_GT Ra_0)) •imp ((X •Ra_TIMES X1) •Ra_GT (Y •Ra_TIMES X1))
(618) Theorem 470: (X in Ra) •imp (X •Ra_TIMES Ra_0 = Ra_0)
(618+) Theorem 471: ((X in Ra) & (Y in Ra) & (X •Ra_GT Ra_0) & (Y •Ra_GT Ra_0)) •imp ((X •Ra_TIMES Y) •Ra_GT Ra_0)
(619) Theorem 472: ((X in Ra) & (X •Ra_GT Ra_0)) •imp (Recip(X) •Ra_GT Ra_0)
(620) Theorem 473: ((X in Ra) & (Y in Ra)) •imp (Ra_Rev(X •Ra_PLUS Y) = (Ra_Rev(X) •Ra_PLUS Ra_Rev(Y)))
(621) Theorem 474: ((X in Ra) & (Y in Ra) & (XP in Ra) & (YP in Ra) & (X •Ra_GE Y) & (XP •Ra_GE YP)) •imp ((X •Ra_PLUS XP) •Ra_GE (Y •Ra_PLUS YP))
(622) Theorem 475: (X in Ra) •imp (Ra_Rev(Ra_Rev(X)) = X)
(623) Theorem 476: ((X in Ra) & (Y in Ra)) •imp (((X •Ra_GE Y) or (Y •Ra_GE X)) & (((X •Ra_GE Y) & (Y •Ra_GE X)) •imp (X = Y)))
(624) Theorem 477: [Transitivity of ordering, strict case] ((X in Ra) & (Y in Ra) & (Z in Ra)) •imp (((X •Ra_GE Y) & (Y •Ra_GT Z)) •imp (X •Ra_GT Z))
(625) Theorem 478: [Transitivity of ordering, strict case 2] ((X in Ra) & (Y in Ra) & (Z in Ra)) •imp (((X •Ra_GT Y) & (Y •Ra_GE Z)) •imp (X •Ra_GT Z))
(626) Theorem 479: [Transitivity of ordering, strict case 3] ((X in Ra) & (Y in Ra) & (Z in Ra)) •imp (((X •Ra_GT Y) & (Y •Ra_GT Z)) •imp (X •Ra_GT Z))
(627) Theorem 480: [Transitivity of ordering by 'less than'] ((X in Ra) & (Y in Ra) & (Z in Ra)) •imp (((X •Ra_LE Y) & (Y •Ra_LT Z)) •imp (X •Ra_LT Z))
(628) Theorem 481: [Transitivity of ordering by 'less than', 2] ((X in Ra) & (Y in Ra) & (Z in Ra)) •imp (((X •Ra_LT Y) & (Y •Ra_LE Z)) •imp (X •Ra_LT Z))
(629) Theorem 482: [Transitivity of ordering by 'less than', 3] ((X in Ra) & (Y in Ra) & (Z in Ra)) •imp (((X •Ra_LT Y) & (Y •Ra_LT Z)) •imp (X •Ra_LT Z))
(630) Theorem 483: ((X in Ra) & (Y in Ra) & (X •Ra_GE Y)) •imp (Ra_Rev(Y) •Ra_GE Ra_Rev(X))
(631) Theorem 484: ((X in Ra) & (Y in Ra) & (X •Ra_GT Y)) •imp (Ra_Rev(Y) •Ra_GT Ra_Rev(X))
(632) Theorem 485: ((X in Ra) & (Y in Ra) & (XP in Ra) & (YP in Ra) & (X •Ra_GE Y) & (XP •Ra_GT YP)) •imp ((X •Ra_PLUS XP) •Ra_GT (Y •Ra_PLUS YP))
(633) Theorem 486: ((X in Ra) & (Y in Ra) & (XP in Ra) & (YP in Ra) & (X •Ra_GT Y) & (XP •Ra_GE YP)) •imp ((X •Ra_PLUS XP) •Ra_GT (Y •Ra_PLUS YP))
(634) Theorem 487: ((X in Ra) & (X /= Ra_0)) •imp ((Recip(X) /= Ra_0) & Recip(Recip(X)) = X)
(635) Theorem 488: ([2,0] in Si) & (is_nonneg([2,0])) & is_nonneg([1,0]) & (Fr_to_Ra([[1,0],[2,0]]) in Ra) & (Fr_to_Ra([[1,0],[2,0]]) •Ra_GT Ra_0)
(636) Theorem 489: ((X in Ra) & (Y in Ra) & (Z in Ra) & (X •Ra_GE Y) & (Y •Ra_GE Z)) •imp (X •Ra_GE Z)
(637) Theorem 490: ((X in Ra) & (Y in Ra) & (Z in Ra) & (X •Ra_GT Y) & (Y •Ra_GE Z)) •imp (X •Ra_GT Z)
(638) Theorem 491: ((X in Ra) & (Y in Ra) & (Z in Ra) & (X •Ra_GE Y) & (Y •Ra_GT Z)) •imp (X •Ra_GT Z)
(639) Theorem 492: ((X in Ra) & (Y in Ra) & (Z in Ra) & (X •Ra_GT Y) & (Y •Ra_GT Z)) •imp (X •Ra_GT Z)
(640) Theorem 493: (FORALL x in Ra, y in Ra, z in Ra | ((x •Ra_LT y) & (y •Ra_LT z)) •imp (x •Ra_LT z))
(641) Theorem 494: (FORALL x in Ra | not(x •Ra_LT x))
(642) Theorem 495: (FORALL x in Ra, y in Ra | (x •Ra_LT y) or (x = y) or (y •Ra_LT x))
(643) Theorem 496: (FORALL x, y | smaller_Ra(x,y) = if ((x notin Ra) & (y notin Ra)) then Ra elseif (x notin Ra) then y elseif (y notin Ra) then x elseif (x •Ra_LT y) then x else y end if) & (FORALL x, y | smaller_Ra(x,y) = smaller_Ra(y,x)) & (FORALL x, y | ({x,y} •incin Ra) •imp (smaller_Ra(x,y) in {x,y})) & (FORALL x | (x in next(Ra)) •imp (smaller_Ra(x,Ra) = x)) & (FORALL x, y, z | smaller_Ra(x,smaller_Ra(y,z)) = smaller_Ra(smaller_Ra(x,y),z)) & (FORALL x, y | ((x in next(Ra)) & (y in next(Ra))) •imp (smaller_Ra(x,y) in next(Ra))) & (FORALL f,p,a | (Svm(f) & (range(f) •incin Ra) & Finite(f)) •imp (((p in f) •imp (min_over_Ra({p}) = (f~[car(p)]))) & (min_over_Ra(f) = smaller_Ra(min_over_Ra(f •ON (domain(f) * a)),min_over_Ra(f •ON (domain(f) - a)))))) & (FORALL f | (Svm(f) & (range(f) •incin Ra) & Finite(f) & (f /= 0)) •imp (min_over_Ra(f) in range(f))) & (FORALL x, y | ({x,y} •incin Ra) •imp ((smaller_Ra(x,y) = x) •eq ((x •Ra_LT y) or (x = y)))) & (FORALL t | ubs_Ra(t) = {x in Ra | (FORALL y in (t * Ra) | smaller_Ra(y,x) = y)}) & (FORALL t | max_Ra(t) = arb({Ra} + (t * ubs_Ra(t)))) & (FORALL t | lub_Ra(t) = arb({Ra} + {x in ubs_Ra(t) | ubs_Ra(t) •incin ubs_Ra({x})})) & (ubs_Ra(0) = Ra) & (max_Ra(0) = Ra) & (FORALL t | (ubs_Ra(t) •incin Ra) & (ubs_Ra(t) = ubs_Ra(t * Ra)) & (max_Ra(t) = max_Ra(t * Ra))) & (FORALL t, x | (Finite(t) & (x in t) & (t •incin Ra)) •imp ((max_Ra(t) in t) & ((x = max_Ra(t)) or ((x •Ra_LT max_Ra(t))))))
(644) Theorem 497: ((X in Ra) & (Y in Ra) & (XP in Ra) & (YP in Ra) & (X •Ra_GE Y) & (Y •Ra_GE Ra_0) & (YP •Ra_GE Ra_0) & (XP •Ra_GE YP)) •imp ((X •Ra_TIMES XP) •Ra_GE (Y •Ra_TIMES YP))
(645) Theorem 498: ((X in Ra) & (Y in Ra) & (XP in Ra) & (YP in Ra) & (X •Ra_GT Y) & (Y •Ra_GT Ra_0) & (YP •Ra_GT Ra_0) & (XP •Ra_GE YP)) •imp ((X •Ra_TIMES XP) •Ra_GT (Y •Ra_TIMES YP))
(646) Theorem 499: [The rational reciprocal is monotone decreasing for positive rationals] ((X in Ra) & (Y in Ra) & (X •Ra_GT Y) & (Y •Ra_GT Ra_0)) •imp (Recip(Y) •Ra_GT Recip(X))
(647) Theorem 500: [The average of two rational numbers lies between them] ((X in Ra) & (Y in Ra) & (X •Ra_GT Y)) •imp ((X •Ra_GT ((X •Ra_PLUS Y) •Ra_OVER (Ra_1 •Ra_PLUS Ra_1))) & (((X •Ra_PLUS Y) •Ra_OVER (Ra_1 •Ra_PLUS Ra_1)) •Ra_GT Y))
(648) Theorem 501: [Properties of the rational number 2] ((Ra_1 •Ra_PLUS Ra_1) in Ra) & ((Ra_1 •Ra_PLUS Ra_1) •Ra_GT Ra_0) & (Recip(Ra_1 •Ra_PLUS Ra_1) in Ra) & ((X in Ra) •imp ((X •Ra_OVER (Ra_1 •Ra_PLUS Ra_1)) in Ra))
(649) Theorem 502: [Any rational number can be divided into two equal halves] (X in Ra) •imp (X = ((X •Ra_OVER (Ra_1 •Ra_PLUS Ra_1)) •Ra_PLUS (X •Ra_OVER (Ra_1 •Ra_PLUS Ra_1))))
(650) Theorem 503: [Every positive rational exceeds the sum of two smaller positive rationals] ((X in Ra) & (X •Ra_GT Ra_0)) •imp (EXISTS e in Ra, e0 in Ra | (X •Ra_GT e) & (e •Ra_GT e0) & (e0 •Ra_GT Ra_0) & (e •Ra_GT Ra_0) & (X •Ra_GT (e •Ra_PLUS e0)))
(651) Theorem 504: [Every positive rational exceeds some smaller positive rational] ((X in Ra) & (X •Ra_GT Ra_0)) •imp (EXISTS e in Ra | (X •Ra_GT e) & (e •Ra_GT Ra_0))
(652) Theorem 505: [?] (X in Ra) •imp ((X •Ra_TIMES X) •Ra_GE Ra_0)
(653) Theorem 506: [?] (FORALL x | Ra_ABS(x) = if Ra_is_nonneg(x) then x else Ra_Rev(x) end if) & (FORALL x,y,z | ((x in Ra) & (y in Ra) & (z in Ra)) •imp (((x •Ra_PLUS y) = (x •Ra_PLUS z)) •imp (y = z))) & (FORALL x,y | ((x in Ra) & (y in Ra)) •imp (Ra_Rev(x •Ra_PLUS Ra_Rev(y)) = (y •Ra_PLUS Ra_Rev(x)))) & (FORALL x,y | ((x in Ra) & (y in Ra)) •imp ((x •Ra_LE y) or (y •Ra_LE x))) & (FORALL x | (x in Ra) •imp (x •Ra_LE x)) & (FORALL x,y,z | ((x in Ra) & (y in Ra) & (z in Ra)) •imp (((x •Ra_LE y) & (y •Ra_LE z)) •imp (x •Ra_LE z))) & (FORALL x,y,z | ((x in Ra) & (y in Ra) & (z in Ra)) •imp (((x •Ra_LE y) & (x /= y) & (y •Ra_LE z)) •imp (x /= z))) & (FORALL x,y,z | ((x in Ra) & (y in Ra) & (z in Ra)) •imp (((x •Ra_LE y) & (y •Ra_LE z) & (y /= z)) •imp (x /= z))) & (FORALL x,y,z | ((x in Ra) & (y in Ra) & (z in Ra)) •imp ((x •Ra_LE y) •imp ((x •Ra_PLUS z) •Ra_LE (y •Ra_PLUS z)))) & (FORALL x,y,z | ((x in Ra) & (y in Ra) & (z in Ra)) •imp (((x •Ra_PLUS z) = (y •Ra_PLUS z)) •imp (x = y))) & (FORALL x,y,z | ((x in Ra) & (y in Ra) & (z in Ra)) •imp (((x •Ra_LE y) & (x /= y)) •imp ((x •Ra_PLUS z) /= (y •Ra_PLUS z)))) & (FORALL x | (x in Ra) •imp (Ra_ABS(x •Ra_PLUS Ra_Rev(x)) = Ra_0)) & (FORALL x | (x in Ra) •imp (x •Ra_LE Ra_ABS(x))) & (FORALL x | (x in Ra) •imp (Ra_ABS(Ra_ABS(x)) = Ra_ABS(x))) & (FORALL x | (x in Ra) •imp ((Ra_ABS(x) = Ra_0) •eq (x = Ra_0))) & (FORALL x | (x in Ra) •imp (Ra_ABS(Ra_Rev(x)) = Ra_ABS(x))) & (FORALL x,y | ((x in Ra) & (y in Ra)) •imp ((x •Ra_PLUS y) •Ra_LE (Ra_ABS(x) •Ra_PLUS Ra_ABS(y)))) & (FORALL x,y,z | ((x in Ra) & (y in Ra) & (z in Ra)) •imp ((Ra_ABS(x •Ra_PLUS Ra_Rev(y)) •Ra_LE z) •imp (y •Ra_LE (x •Ra_PLUS z)))) & (FORALL x,y | ((x in Ra) & (y in Ra)) •imp (Ra_ABS(x •Ra_PLUS y) •Ra_LE (Ra_ABS(x) •Ra_PLUS Ra_ABS(y)))) & (FORALL x,y | ((x in Ra) & (y in Ra)) •imp ((not(Ra_is_nonneg(x))) •imp ((x •Ra_LE Ra_ABS(y)) & (x /= Ra_ABS(y))))) & (FORALL x,y,z | ((x in Ra) & (y in Ra) & (z in Ra)) •imp (Ra_ABS((x •Ra_PLUS Ra_Rev(z))) •Ra_LE (Ra_ABS(x •Ra_PLUS Ra_Rev(y)) •Ra_PLUS Ra_ABS(y •Ra_PLUS Ra_Rev(z))))) & (FORALL x,y | ((x in Ra) & (y in Ra)) •imp (Ra_is_nonneg(y) •imp ((x •Ra_PLUS Ra_Rev(y)) •Ra_LE (x •Ra_PLUS y)))) & (FORALL x,y | ((x in Ra) & (y in Ra)) •imp (Ra_ABS(Ra_ABS(x) •Ra_PLUS Ra_Rev(Ra_ABS(y))) •Ra_LE Ra_ABS(x •Ra_PLUS Ra_Rev(y)))) & (FORALL x,y | ((x in Ra) & (y in Ra)) •imp (Ra_ABS(x) •Ra_PLUS Ra_Rev(Ra_ABS(Ra_ABS(y) •Ra_PLUS Ra_Rev(Ra_ABS(x)))) •Ra_LE Ra_ABS(y)))
(654) Theorem 507: ((X in Ra) & (Y in Ra) & (not(X •Ra_LE Y))) •imp (X •Ra_GT Y)
(655) Theorem 508: [The absolute value of a rational x is a non-negative rational no smaller than x] (X in Ra) •imp ((Ra_ABS(X) in Ra) & (Ra_ABS(X) •Ra_GE Ra_0) & (Ra_ABS(X) •Ra_GE X))
(656) Theorem 509: [The absolute value of a non-negative rational x is x] (X in Ra) •imp ((X •Ra_GE Ra_0) •eq (Ra_ABS(X) = X))
(657) Theorem 510: [The absolute value of a rational x greater than Ra_0 is x] ((X in Ra) & (X •Ra_GT Ra_0)) •imp (Ra_ABS(X) = X)
(658) Theorem 511: [The absolute value of a rational product is the product of the absolute values] ((X in Ra) & (Y in Ra)) •imp (Ra_ABS(X •Ra_TIMES Y) = (Ra_ABS(X) •Ra_TIMES Ra_ABS(Y)))
(659) Theorem 512: [If the product of two rationals is 0, one of them is 0] ((X in Ra) & (Y in Ra)) •imp (((X •Ra_TIMES Y) = Ra_0) •eq ((X = Ra_0) or (Y = Ra_0)))
(660) Theorem 513: [Cancellation rule for rational multiplication] ((X in Ra) & (Y in Ra) & (U in Ra) & (X /= Ra_0) & ((X •Ra_TIMES Y) = (X •Ra_TIMES U))) •imp (Y = U)
(661) Theorem 514: [The reciprocal of a rational product is the product of the reciprocals] ((X in Ra) & (Y in Ra) & (X /= Ra_0) & (Y /= Ra_0)) •imp (Recip(X •Ra_TIMES Y) = (Recip(X) •Ra_TIMES Recip(Y)))
(662) Theorem 515: [Formula for the sum of two rational quotients] ((X in Ra) & (Y in Ra) & (U in Ra) & (V in Ra) & (X /= Ra_0) & (Y /= Ra_0)) •imp (((U •Ra_OVER X) •Ra_PLUS (V •Ra_OVER Y)) = (((Y •Ra_TIMES U) •Ra_PLUS (X •Ra_TIMES V)) •Ra_OVER (X •Ra_TIMES Y)))
(663) Theorem 516: ((X in Ra) & (Y in Ra) & (X /= Ra_0) & (Y /= Ra_0)) •imp ((Recip(X) •Ra_MINUS Recip(Y)) = ((Y •Ra_MINUS X) •Ra_OVER (X •Ra_TIMES Y)))
(664) Theorem 517: [The absolute value of the reciprocal equals the reciprocal of the absolute value] ((X in Ra) & (X /= Ra_0)) •imp (Ra_ABS(Recip(X)) = Recip(Ra_ABS(X)))
(664+) Theorem 518: ((X in Ra) & (Y in Ra)) •imp (Ra_ABS(X •Ra_MINUS Y) = Ra_ABS(Y •Ra_MINUS X))
(665) Theorem 519: ((X in Ra) & (Y in Ra) & (A in Ra) & (B in Ra) & (Ra_ABS(X) •Ra_GT A) & (Ra_ABS(Y) •Ra_GT B) & (A •Ra_GT Ra_0) & (B •Ra_GT Ra_0)) •imp (Ra_ABS(Recip(X) •Ra_MINUS Recip(Y)) •Ra_LE (Ra_ABS(X •Ra_MINUS Y) •Ra_TIMES (Recip(A) •Ra_TIMES Recip(B))))
(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})))
(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))
(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])))) ))
(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])))))
(689) Theorem 538: ((S •incin Ra) & Finite(S)) •imp (EXISTS u in Ra | (FORALL y in S | u •Ra_GE y))
(691) Theorem 540: [Every Cauchy sequence has an upper bound] (F in RaCauchy) •imp (EXISTS x in Ra | (FORALL y in range(F) | y •Ra_LE x))
(692) Theorem 541: (F in RaCauchy) •imp (EXISTS x in Ra | (FORALL y in range(F) | Ra_ABS(y) •Ra_LT x ))
(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]))))))
(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) ))
(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)))
(857) Theorem 704: [The embedding of rationals into reals preserves all elementary algebraic operations, 1] (Y in Ra) •imp ((ReRa(Y) in Re) & (ReRa(Ra_Rev(Y)) = R_Rev(ReRa(Y))) & (R_is_nonneg(ReRa(Y)) •eq Ra_is_nonneg(Y)) & (ReRa(Ra_ABS(Y)) = abs(ReRa(Y))))
(858) Theorem 705: [The embedding of rationals into reals preserves all elementary algebraic operations, 2] ((X in Ra) & (Y in Ra)) •imp ((ReRa(X) in Re) & (ReRa(Y) in Re) & (ReRa(X •Ra_PLUS Y) = ReRa(X) •R_PLUS ReRa(Y)) & (ReRa(X •Ra_TIMES Y) = ReRa(X) •R_TIMES ReRa(Y)))
(859) Theorem 706: [The embedding of rationals into reals preserves all elementary algebraic operations, 3] ((X in Ra) & (Y in Ra)) •imp (ReRa(X •Ra_MINUS Y) = (ReRa(X) •R_MINUS ReRa(Y)))
(860) Theorem 707: [The embedding of rationals into reals is 1-1] ((X in Ra) & (Y in Ra)) •imp ((ReRa(X) = ReRa(Y)) •eq (X = Y))
(862) Theorem 709: [The embedding of rationals into reals preserves quotients by nonzero quantities] ((X in Ra) & (Y in Ra) & (Y /= Ra_0)) •imp ((R_Recip(ReRa(Y)) = ReRa(Recip(Y))) & ((ReRa(X) •R_OVER ReRa(Y)) = ReRa(X •Ra_OVER Y)))
(863) Theorem 710: [The embedding of rationals into reals preserves ordering] ((X in Ra) & (Y in Ra)) •imp (((ReRa(X) •R_GE ReRa(Y)) •eq (X •Ra_GE Y)) & ((ReRa(X) •R_GT ReRa(Y)) •eq (X •Ra_GT Y)) & ((ReRa(Y) •R_LE ReRa(X)) •eq (Y •Ra_LE X)) & ((ReRa(Y) •R_LT ReRa(X)) •eq (Y •Ra_LT 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}) )
(865) Theorem 711: [The embedding of signed integers into rationals preserves all elementary algebraic operations, 1] (X in Si) •imp ((RaSi(X) in Ra) & (Ra_is_nonneg(RaSi(X)) •eq is_nonneg(X)) & (RaSi(S_Rev(X)) = Ra_Rev(RaSi(X))) & (RaSi(S_ABS(X)) = Ra_ABS(RaSi(X))))
(866) Theorem 712: [The embedding of signed integers into rationals preserves all elementary algebraic operations, 2] ((X in Si) & (Y in Si)) •imp ((RaSi(X) in Ra) & (RaSi(Y) in Ra) & (RaSi(X •S_PLUS Y) = RaSi(X) •Ra_PLUS RaSi(Y)) & (RaSi(X •S_TIMES Y) = RaSi(X) •Ra_TIMES RaSi(Y)))
(883) Theorem 728: [Any real x is included between two rationals which can be arbitrarily close together] ((X in Re) & (EPS in Re) & (EPS •R_GT R_0)) •imp (EXISTS r1 in Ra, r2 in Ra | ((ReRa(r1) •R_GT X) & (X •R_GT ReRa(r2)) & (ReRa(r1 •Ra_MINUS r2) •R_LE EPS)))
(884) Theorem 729: [For any real x, there exists a rational r such that r >= x] (x in Re) •imp (EXISTS r in Ra | ReRa(r) •R_GT x)
(885) Theorem 730: [Any rational r is the quotient of two signed integers, of which the second is positive] (x in Ra) •imp (EXISTS m in Si, n in Si | ((n •S_GE [1,0]) & (x = RaSi(m) •Ra_OVER RaSi(n))))
(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)