List of theorems referencing the symbol DOT_EQ
(16) Theorem setformer.1: [Equality of setformers] ((x_thryvar notin s) or ((e(x_thryvar) = e0(x_thryvar)) & (P(x_thryvar) •eq PP(x_thryvar)))) •imp ({e(x): x in s | P(x)} = {e0(x): x in s | PP(x)})
(19) Theorem setformer2_1: [Equality of mapformers] (((x_thryvar notin s) or (y_thryvar notin (f(x_thryvar) + fp(x_thryvar)))) or (((f(x_thryvar) = fp(x_thryvar)) & (e2(x_thryvar,y_thryvar) = ep2(x_thryvar,y_thryvar)) & (R(x_thryvar,y_thryvar) •eq PQ(x_thryvar,y_thryvar))))) •imp ({e2(x,y): x in s, y in f(x) | R(x,y)} = {ep2(x,y): x in s, y in fp(x) | PQ(x,y)})
(20) Theorem comprehension1: [Setformer existence] (X in tt_thryvar) •eq ((X in s) & P(X))
(37) Theorem 24: [Only the null set has a null domain] (S = 0) •eq (domain(S) = 0)
(38) Theorem 25: [Only the null set has a null range] (S = 0) •eq (range(S) = 0)
(39) Theorem 26: [Maps are mapformers] Is_map(F) •eq (F •incin {[car(x),cdr(x)]: x in F})
(47) Theorem one_1_test_2.1: [One-one map former test, two-variable case] ((x_thryvar in s) & (y_thryvar in t) & (x2_thryvar in s) & (y2_thryvar in t) & (not((a2(x_thryvar,y_thryvar) = a2(x2_thryvar,y2_thryvar)) •eq (b2(x_thryvar,y_thryvar) = b2(x2_thryvar,y2_thryvar))))) or one_1_map({[a2(x,y),b2(x,y)]: x in s, y in t})
(48) Theorem one_1_test_3.1: [Single-valued map former, three-variable case] ((x_thryvar in s) & (y_thryvar in t) & (z_thryvar in r) & (xp_thryvar in s) & (yp_thryvar in t) & (zp_thryvar in r) & P3(x_thryvar,y_thryvar,z_thryvar) & P3(xp_thryvar,yp_thryvar,zp_thryvar) & (((a3(x_thryvar,y_thryvar,z_thryvar) /= a3(xp_thryvar,yp_thryvar,zp_thryvar)) •eq (b3(x_thryvar,y_thryvar,z_thryvar) = b3(xp_thryvar,yp_thryvar,zp_thryvar))))) or one_1_map({[a3(x,y,wz),b3(x,y,wz)]: x in s, y in t,wz in r | P3(x,y,wz)})
(56) Theorem 34: [Third ordinal comparison lemma] (Ord(S) & Ord(T)) •imp ((T •incin S) •eq ((T in S) or (T = S)))
(57) Theorem 35: [Ordinal membership and comparison] (Ord(S) & Ord(T)) •imp ((T notin S) •eq (S •incin T))
(58) Theorem 36: [Membership in the successor of an ordinal s] Ord(S) •imp ((T in next(S)) •eq ((T •incin S) & Ord(T)))
(61) Theorem 39: [There is no antinomic Russell's set] not(EXISTS x | (FORALL y | (y in x) •eq (y notin y)))
(62) Theorem 40: [The class of ordinals is not a set] not (FORALL x | ((x in OS) •eq Ord(x)))
(102) Theorem 72: [Form of a single-valued map] Svm(F) •eq (F = {[x,F~[x]]: x in domain(F)})
(107) Theorem 77: [Map domain member lemma] Is_map(F) •imp ((X in domain(F)) •eq ([X,F~[X]] in F))
(118) Theorem 86: [Domain is null only when range is null] (domain(F) = 0) •eq (range(F) = 0)
(122) Theorem 90: [Members of the inverse map] Is_map(F) •imp (([X,Y] in F) •eq ([Y,X] in inv(F)))
(155) Theorem 116: [One-one-ness and singlevaluedness] one_1_map(F) •eq (Svm(F) & Svm(inv(F)))
(166) Theorem 127: [Single-valued and one-one maps] Is_map(F) •imp (one_1_map(F) •eq one_1_map(inv(F)))
(168) Theorem 129: [Elements are defined uniquely by their one-one images] Svm(F) •imp (one_1_map(F) •eq (FORALL x in domain(F), y in domain(F) | ((F~[x] = F~[y]) •imp (x = y))))
(175) Theorem 136: [Subsets of Cartesian products] (Y •incin (S •PROD T)) •eq (Is_map(Y) & (domain(Y) •incin S) & (range(Y) •incin T))
(192) Theorem 153: [Equicardinality is equivalent to one-one correspondence] (EXISTS F in OM | (one_1_map(F) & (range(F) = S) & (domain(F) = T))) •eq (#S = #T)
(196) Theorem 157: [Sets of cardinality 0 must be null] (#S = 0) •eq (S = 0)
(197) Theorem 158: [Non-null sets have cardinality greater than 0] (0 in #S) •eq (S /= 0)
(198) Theorem 159: [A cardinal is its own cardinality] Card(S) •eq (S = #S)
(211) Theorem 171: [Condition for existence of a single-valued map between two sets] (#S incs #T) •eq (T = 0 or (EXISTS f in OM | Svm(f) & (domain(f) = S) & (range(f) = T)))
(226) Theorem 186: [One-one maps preserve finiteness, 2] one_1_map(F) •imp (Finite(domain(F)) •eq Finite(range(F)))
(229) Theorem 188: [A set is finite if and only if its cardinality is finite] Finite(S) •eq Finite(#S)
(231) Theorem 190: [A set is finite if and only if it is not the single-valued image of any of its finite subsets] Finite(S) •eq (not(EXISTS f in OM | (Svm(f) & (range(f) = S) & (domain(f) •incin S) & (S /= domain(f)))))
(235) Theorem 194: [Adding one element to a finite set leaves it finite] Finite(S) •eq Finite(S + {X})
(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))
(276) Theorem 229: [The union of finite sets is finite] (Finite(N) & Finite(M)) •eq Finite(N + M)
(279) Theorem 232: [An arithmetic sum is finite if its two terms are finite] Finite(N •PLUS M) •eq Finite(N + M)
(280) Theorem 233: [An arithmetic sum is finite if and only if both its terms are finite] (Finite(N) & Finite(M)) •eq Finite(N •PLUS M)
(302) Theorem 255: [If the product of two nonzero terms is finite, so are the terms] ((Finite(N) & Finite(M)) or N = 0 or M = 0) •eq Finite(N •TIMES M)
(303) Theorem 256: [A set is finite if and only if its powerset is finite] Finite(N) •eq Finite(pow(N))
(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))
(341) Theorem 294: [If an integer product is zero, one of its factors is 0] (N •TIMES M = 0) •eq (N = 0 or M = 0)
(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)))
(360) Theorem 313: ((X •incin Za) & (FORALL i | (next(i) in X) •imp (i in X))) •eq (X in next(Za))
(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))
(403) Theorem well_founded_set.2: (s •incin {ordenm_thryvar(y): y in X}) •eq (ordenm_thryvar(X) = s)
(412) Theorem well_ordered_set.100: (FORALL x,y | ((x in s) & (y in s)) •imp ((not (arg1_bef_arg2(x,y) & arg1_bef_arg2(y,x))) & (not arg1_bef_arg2(x,x)))) & (FORALL x | (not(s •incin {ordenm_thryvar(y): y in x})) •imp ((ordenm_thryvar(x) in (s - {ordenm_thryvar(y): y in x})) & (FORALL y in (s - {ordenm_thryvar(y): y in x}) | not(arg1_bef_arg2(y,ordenm_thryvar(x)))))) & (FORALL x | (s •incin {ordenm_thryvar(y): y in x}) •eq (ordenm_thryvar(x) = s)) & (FORALL x | (ordenm_thryvar(x) /= s) •imp (ordenm_thryvar(x) in s)) & (FORALL u, v | (Ord(u) & Ord(v) & (ordenm_thryvar(u) /= s) & arg1_bef_arg2(ordenm_thryvar(u),ordenm_thryvar(v))) •imp (u in v)) & (FORALL v | {u: u in s | arg1_bef_arg2(u,ordenm_thryvar(v))} •incin {ordenm_thryvar(x): x in v}) & (FORALL u, v | (Ord(u) & Ord(v) & (ordenm_thryvar(u) /= s) & (ordenm_thryvar(v) /= s) & (u /= v)) •imp (ordenm_thryvar(u) /= ordenm_thryvar(v))) & (EXISTS o in next(#pow(s)) | (Ord(o) & (s = {ordenm_thryvar(x): x in o}) & (FORALL x in o | (ordenm_thryvar(x) /= s)) & one_1_map({[x,ordenm_thryvar(x)]: x in o}))) & (FORALL x | ordenm_thryvar(x) = Minrel_thryvar(s - {ordenm_thryvar(y): y in x})) & (FORALL t | Minrel_thryvar(t) = if (t •incin s) & (t /= 0) then arb({m: m in t | (FORALL y in t | (not arg1_bef_arg2(y,m)))}) else s end if)
(414) Theorem well_ordered_set.2: ((s •incin {ordenm_thryvar(y): y in X}) •eq (ordenm_thryvar(X) = s))
(422) Theorem well_ordered_set.5: [Any well-ordering is isomorphic to an ordinal enumeration] (Ord(U) & Ord(V) & (ordenm_thryvar(U) /= s) & (ordenm_thryvar(V) /= s)) •imp (arg1_bef_arg2(ordenm_thryvar(U),ordenm_thryvar(V)) •eq (U in V))
(436) Theorem 343: (Ord(O1) & Ord(O2)) •imp (EXISTS f in OM | one_1_map(f) & Ord(domain(f)) & (range(f) = (O1 •PROD O2)) & (FORALL x in domain(f), y in domain(f) | (x in y) •eq (((car(f~[x]) + cdr(f~[x])) in (car(f~[y]) + cdr(f~[y]))) or (((car(f~[x]) + cdr(f~[x])) = (car(f~[y]) + cdr(f~[y]))) & (car(f~[x]) in car(f~[y]))) or (((car(f~[x]) + cdr(f~[x])) = (car(f~[y]) + cdr(f~[y]))) & (car(f~[x]) = car(f~[y])) & (cdr(f~[x]) in cdr(f~[y]))))))
(521) Theorem equivalence_classes1: [Elements are equivalent if and only if their equivalence classes are equal] ((X in s) & (Y in s)) •imp (R(X,Y) •eq (f_thryvar(X) = f_thryvar(Y)))
(536) Theorem linear_order_15: ({X,Y} •incin s0) •imp ((smaller_thryvar(X,Y) = X) •eq (arg1_bef_arg2(X,Y) or (X = Y)))
(541) Theorem linear_order_20: (FORALL x, y | larger_thryvar(x,y) = if ((x notin s0) & (y notin s0)) then s0 elseif (x notin s0) then y elseif (y notin s0) then x elseif arg1_aft_arg2(x,y) then x else y end if) & (FORALL x, y | larger_thryvar(x,y) = larger_thryvar(y,x)) & (FORALL x, y | ({x,y} •incin s0) •imp (larger_thryvar(x,y) in {x,y})) & (FORALL x | (x in next(s0)) •imp (larger_thryvar(x,s0) = x)) & (FORALL x, y, z | larger_thryvar(x,larger_thryvar(y,z)) = larger_thryvar(larger_thryvar(x,y),z)) & (FORALL x, y | ((x in next(s0)) & (y in next(s0))) •imp (larger_thryvar(x,y) in next(s0))) & (FORALL f,p,a | (Svm(f) & (range(f) •incin s0) & Finite(f)) •imp (((p in f) •imp (max_over_thryvar({p}) = (f~[car(p)]))) & (max_over_thryvar(f) = larger_thryvar(max_over_thryvar(f •ON (domain(f) * a)),max_over_thryvar(f •ON (domain(f) - a)))))) & (FORALL f | (Svm(f) & (range(f) •incin s0) & Finite(f) & (f /= 0)) •imp (max_over_thryvar(f) in range(f))) & (FORALL x, y | ({x,y} •incin s0) •imp ((larger_thryvar(x,y) = x) •eq (arg1_aft_arg2(x,y) or (x = y)))) & (FORALL t | lbs_thryvar(t) = {x in s0 | (FORALL y in (t * s0) | larger_thryvar(y,x) = y)}) & (FORALL t | min_thryvar(t) = arb({s0} + (t * lbs_thryvar(t)))) & (FORALL t | glb_thryvar(t) = arb({s0} + {x in lbs_thryvar(t) | lbs_thryvar(t) •incin lbs_thryvar({x})})) & (lbs_thryvar(0) = s0) & (min_thryvar(0) = s0) & (FORALL t | (lbs_thryvar(t) •incin s0) & (lbs_thryvar(t) = lbs_thryvar(t * s0)) & (min_thryvar(t) = min_thryvar(t * s0))) & (FORALL t, x | (Finite(t) & (x in t) & (t •incin s0)) •imp ((min_thryvar(t) in t) & ((x = min_thryvar(t)) or (arg1_aft_arg2(x,min_thryvar(t))))))
(548) Theorem 399: (S /= 0) •imp ((Filter(T,S) & (FORALL x •incin pow(S) | ((x incs T) & Filter(x,S)) •imp (x = T))) •eq Ultrafilter(T,S))
(549+) Theorem 401: [Equivalence of fractions is reflexive and symmetric] (FORALL x in Fr,y in Fr | (Same_frac(x,y) •eq Same_frac(y,x)) & Same_frac(x,x))
(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))))
(553) Theorem 405: [Alternate version of Theorem 403] ((X in Fr) & (Y in Fr)) •imp (Same_frac(X,Y) •eq (Fr_to_Ra(X) = Fr_to_Ra(Y)))
(555) Theorem Ordered_add.0: [Echo of relator definitions] (GE_thryvar(X,Y) •eq nneg(pluz(X,rvz(Y)))) & (LE_thryvar(X,Y) •eq GE_thryvar(Y,X)) & (GT_thryvar(X,Y) •eq (GE_thryvar(X,Y) & (X /= Y))) & (LT_thryvar(X,Y) •eq GT_thryvar(Y,X))
(556) Theorem Ordered_add.1: [Interface to Otter-based THEORY of orderedGroups] (LE_thryvar(X,Y) •eq nneg(pluz(Y,rvz(X)))) & (((X in g) & (Y in g)) •imp (GT_thryvar(X,Y) •eq (nneg(pluz(X,rvz(Y))) & (X /= Y)))) & (((X in g) & (Y in g)) •imp (GT_thryvar(X,Y) •eq (nneg(minz(X,Y)) & (X /= Y))))
(560) Theorem 410: [The ordering of two signed integers is defined by the sign of their differences] (FORALL x, y | (S_GE(x,y) •eq is_nonneg(x •S_PLUS S_Rev(y))) & (S_LE(x,y) •eq S_GE(y,x)) & (S_GT(x,y) •eq (S_GE(x,y) & (x /= y))) & (S_LT(x,y) •eq S_GT(y,x)))
(561) Theorem 411: [The ordering of two signed integers is defined by the sign of their differences] ((X •S_GE Y) •eq is_nonneg(X •S_PLUS S_Rev(Y))) & ((X •S_LE Y) •eq (Y •S_GE X)) & ((X •S_GT Y) •eq ((X •S_GE Y) & (X /= Y))) & ((X •S_LT Y) •eq (Y •S_GT X))
(563) Theorem 413: [The product of signed integers x,y of which x is positive is non-negative iff y is non-negative] ((X in Si) & (Y in Si) & (X /= [0,0]) & is_nonneg(X)) •imp (is_nonneg(X •S_TIMES Y) •eq is_nonneg(Y))
(564) Theorem 414: [Fractions are pairs of signed integers with non-zero denominator] (X in Fr) •eq ((X = [car(X),cdr(X)]) & (car(X) in Si) & (cdr(X) in Si) & (cdr(X) /= [0,0]))
(565) Theorem 415: [Fractions are pairs of signed integers with non-zero denominator, 2] ((X in Si) & (Y in Si)) •imp (([X,Y] in Fr) •eq (Y /= [0,0]))
(573) Theorem 424: [?] ((X in Fr) & (Y in Fr) & Same_frac(X,Y) & is_nonneg(cdr(X)) & is_nonneg(cdr(Y))) •imp ((is_nonneg(car(X)) or car(X) = [0,0]) •eq (is_nonneg(car(Y)) or car(Y) = [0,0]))
(574) Theorem 425: [The sign of the product of the numerator and denominator of a fraction defines the sign of the rational number which it represents] ((X in Fr) & (Y in Fr) & Same_frac(X,Y)) •imp (is_nonneg(car(X) •S_TIMES cdr(X)) •eq is_nonneg(car(Y) •S_TIMES cdr(Y)))
(575) Theorem 426: [?] (X in Fr) •imp (Fr_is_nonneg(X) •eq Fr_is_nonneg([S_Rev(car(X)),S_Rev(cdr(X))]))
(576) Theorem 427: [?] ((X in Fr) & (Y in Fr) & Same_frac(X,Y)) •imp (Fr_is_nonneg(X) •eq Fr_is_nonneg(Y))
(590) Theorem 442: [Expressing the sign of a rational in terms of the numerator and denominator of any representing fraction] ((X in Si) & (Y in Si) & (Y /= [0,0])) •imp (Ra_is_nonneg(Fr_to_Ra([X,Y])) •eq is_nonneg(X •S_TIMES Y))
(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)))
(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]))
(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)))
(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))))))
(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)))
(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))
(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)))
(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})))
(736) Theorem 585: (FORALL f in RaCauchy, g in RaCauchy | (Ra_eqseq(f,g) •eq Ra_eqseq(g,f)) & Ra_eqseq(f,f))
(737) Theorem 586: ((F in RaCauchy) & (G in RaCauchy)) •imp ((Ra_eqseq(F,G) •eq Ra_eqseq(G,F)) & Ra_eqseq(F,F))
(739) Theorem 588: (FORALL x, y | ((x in RaCauchy) & (y in RaCauchy)) •imp ((Ra_eqseq(x,y) •eq (Cauchy_to_Re(x) = Cauchy_to_Re(y))))) & (FORALL x | (x in Re) •imp ((arb(x) in RaCauchy) & (Cauchy_to_Re(arb(x)) = x))) & (FORALL x | (x in RaCauchy) •imp (Cauchy_to_Re(x) in Re)) & (FORALL x | (x in RaCauchy) •imp Ra_eqseq(x,arb(Cauchy_to_Re(x))))
(740) Theorem 589: ((X in RaCauchy) & (Y in RaCauchy)) •imp ((Ra_eqseq(X,Y) •eq (Cauchy_to_Re(X) = Cauchy_to_Re(Y))) & (Cauchy_to_Re(X) in Re) & Ra_eqseq(X,arb(Cauchy_to_Re(X))))
(766) Theorem 616: [The negative of a real x is zero iff x is zero] (X in Re) •imp ((R_Rev(X) = R_0) •eq (X = R_0))
(793) Theorem 643: [Each non-negative rational Cauchy sequences is equivalent to its own absolute value] (X in Re) •imp (R_is_nonneg(X) •eq Ra_eqseq(arb(X),Ras_ABS(arb(X))))
(802) Theorem 652: [The ordering of reals is defined by the sign of their differences] ((((X in Re) & (Y in Re)) •imp ((X •R_GE Y) •eq R_is_nonneg(X •R_PLUS R_Rev(Y))))) & ((X •R_LE Y) •eq (Y •R_GE X)) & ((X •R_GT Y) •eq ((X •R_GE Y) & (X /= Y))) & ((X •R_LT Y) •eq (Y •R_GT X))
(803) Theorem 653: [Various basic properties of real comparison, quantified form] (FORALL x, y | ((x in Re) & (y in Re)) •imp ((x •R_GE y) •eq R_is_nonneg(x •R_PLUS R_Rev(y)))) & (FORALL x, y | ((x •R_LE y) •eq (y •R_GE x))) & (FORALL x, y | ((x •R_GT y) •eq ((x •R_GE y) & (x /= y)))) & (FORALL x, y | ((x •R_LT y) •eq (y •R_GT x))) & (FORALL x, y | ((x in Re) & (y in Re)) •imp ((x •R_LE y) •eq (R_is_nonneg(y •R_PLUS R_Rev(x))))) & (FORALL x, y | ((x in Re) & (y in Re)) •imp ((x •R_GT y) •eq (R_is_nonneg(x •R_PLUS R_Rev(y)) & (x /= y)))) & (FORALL x, y | (((x in Re) & (y in Re)) •imp ((x •R_GT y) •eq (R_is_nonneg(x •R_MINUS y) & (x /= y))))) & (FORALL x, y | ((x in Re) & (y in Re) & ((x = y) or (not(x •R_GE y)))) •imp (y •R_GE x))
(804) Theorem 654: [Various basic properties of real comparison] (((X in Re) & (Y in Re)) •imp ((X •R_GE Y) •eq R_is_nonneg(X •R_PLUS R_Rev(Y)))) & ((X •R_LE Y) •eq (Y •R_GE X)) & ((X •R_GT Y) •eq ((X •R_GE Y) & (X /= Y))) & ((X •R_LT Y) •eq (Y •R_GT X)) & (((X in Re) & (Y in Re)) •imp ((X •R_LE Y) •eq R_is_nonneg(Y •R_PLUS R_Rev(X)))) & (((X in Re) & (Y in Re)) •imp ((X •R_GT Y) •eq (R_is_nonneg(X •R_PLUS R_Rev(Y)) & (X /= Y)))) & (((X in Re) & (Y in Re)) •imp ((X •R_GT Y) •eq (R_is_nonneg(X •R_MINUS Y) & (X /= Y)))) & (((X in Re) & (Y in Re) & ((X = Y) or (not(X •R_GE Y)))) •imp (Y •R_GE X))
(808) Theorem 658: [Greater_than_equal is greater-than and equal] ((X in Re) & (Y in Re)) •imp ((X •R_GE Y) •eq ((X •R_GT Y) or (X = Y)))
(809) Theorem 659: [Greater_than_equal is greater-than and equal] (X in Re) •imp ((X •R_GE R_0) •eq R_is_nonneg(X))
(810) Theorem 660: [Less_than_equal is less-than and equal] ((X in Re) & (Y in Re)) •imp ((X •R_LE Y) •eq ((X •R_LT Y) or (X = Y)))
(816) Theorem 666: [Sign reversal inverts comparisons,2] ((X in Re) & (Y in Re)) •imp (((X •R_GE Y) •eq (R_Rev(Y) •R_GE R_Rev(X))) & ((X •R_GT Y) •eq (R_Rev(Y) •R_GT R_Rev(X))))
(821) Theorem 671: [Strict monotonicity of addition, 2] ((X in Re) & (Y in Re) & (V in Re) & (X •R_GE Y)) •imp (((Y •R_PLUS V) •R_GE (X •R_PLUS V)) •eq (X = Y))
(823) Theorem 672: [The product of two reals is 0 if and only if one of them is 0] ((X in Re) & (Y in Re)) •imp (((X •R_TIMES Y) = R_0) •eq ((X = R_0) or (Y = R_0)))
(829) Theorem 678: [The product of reals x,y of which x is positive is non-negative iff y is non-negative] ((X in Re) & (Y in Re) & (X /= R_0) & R_is_nonneg(X)) •imp (R_is_nonneg(X •R_TIMES Y) •eq R_is_nonneg(Y))
(831) Theorem 680: [Condition for positiveness of a product of reals] ((X in Re) & (Y in Re)) •imp (((X •R_TIMES Y) •R_GT R_0) •eq (((X •R_GT R_0) & (Y •R_GT R_0)) or ((R_0 •R_GT X) & (R_0 •R_GT Y))))
(837) Theorem 684a: [Monotonicity of squaring] ((X in Re) & (Y in Re) & (X •R_GE R_0) & (Y •R_GE R_0)) •imp ((X •R_GE Y) •eq ((X •R_TIMES X) •R_GE (Y •R_TIMES Y)))
(843) Theorem 690: [Trigger for Otter theory 'orderedGroups'] (R_0 in Re) & (FORALL x,y | ((x in Re) & (y in Re)) •imp ((x •R_PLUS y) in Re)) & (FORALL x | (x in Re) •imp (R_Rev(x) in Re)) & (FORALL x,y,z | ((x in Re) & (y in Re) & (z in Re)) •imp (((x •R_PLUS y) •R_PLUS z) = (x •R_PLUS (y •R_PLUS z)))) & (FORALL x | (x in Re) •imp ((x •R_PLUS R_0) = x)) & (FORALL x | (x in Re) •imp ((x •R_PLUS R_Rev(x)) = R_0)) & (FORALL x,y | ((x in Re) & (y in Re)) •imp ((x •R_PLUS y) = (y •R_PLUS x))) & (FORALL x,y | ((x in Re) & (y in Re)) •imp ((R_is_nonneg(x) & R_is_nonneg(y)) •imp R_is_nonneg(x •R_PLUS y))) & (FORALL x | (x in Re) •imp (R_is_nonneg(x) or R_is_nonneg(R_Rev(x)))) & (FORALL x | (x in Re) •imp ((R_is_nonneg(x) & R_is_nonneg(R_Rev(x))) •imp (x = R_0))) & (FORALL x,y | ((x in Re) & (y in Re)) •imp ((x •R_LE y) •eq R_is_nonneg(y •R_PLUS R_Rev(x))))
(844) Theorem 691: [Basic properties of the absolute value function] (FORALL x | abs(x) = if R_is_nonneg(x) then x else R_Rev(x) end if) & (FORALL x | (x in Re) •imp (x •R_LE abs(x))) & (FORALL x | (x in Re) •imp (abs(abs(x)) = abs(x))) & (FORALL x | (x in Re) •imp ((abs(x) = R_0) •eq (x = R_0))) & (FORALL x | (x in Re) •imp (abs(R_Rev(x)) = abs(x))) & (FORALL x,y | ((x in Re) & (y in Re)) •imp ((x •R_PLUS y) •R_LE (abs(x) •R_PLUS abs(y)))) & (FORALL x,y,z | ((x in Re) & (y in Re) & (z in Re)) •imp ((abs(x •R_PLUS R_Rev(y)) •R_LE z) •imp (y •R_LE (x •R_PLUS z)))) & (FORALL x,y | ((x in Re) & (y in Re)) •imp (abs(x •R_PLUS y) •R_LE (abs(x) •R_PLUS abs(y)))) & (FORALL x,y | ((x in Re) & (y in Re)) •imp ((not(R_is_nonneg(x))) •imp ((x •R_LE abs(y)) & (x /= abs(y))))) & (FORALL x,y,z | ((x in Re) & (y in Re) & (z in Re)) •imp (abs((x •R_PLUS R_Rev(z))) •R_LE (abs(x •R_PLUS R_Rev(y)) •R_PLUS abs(y •R_PLUS R_Rev(z))))) & (FORALL x,y | ((x in Re) & (y in Re)) •imp (abs(abs(x) •R_PLUS R_Rev(abs(y))) •R_LE abs(x •R_PLUS R_Rev(y)))) & (FORALL x,y | ((x in Re) & (y in Re)) •imp (abs(x) •R_PLUS R_Rev(abs(abs(y) •R_PLUS R_Rev(abs(x)))) •R_LE abs(y)))
(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))))
(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))
(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)))
(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))))
(868) Theorem 714: [The embedding of signed integers into rationals is 1-1] ((X in Si) & (Y in Si)) •imp ((RaSi(X) = RaSi(Y)) •eq (X = Y))
(869) Theorem 716: [The embedding of signed integers into rationals preserves ordering] ((X in Si) & (Y in Si)) •imp (((RaSi(X) •Ra_GE RaSi(Y)) •eq (X •S_GE Y)) & ((RaSi(X) •Ra_GT RaSi(Y)) •eq (X •S_GT Y)) & ((RaSi(Y) •Ra_LE RaSi(X)) •eq (Y •S_LE X)) & ((RaSi(Y) •Ra_LT RaSi(X)) •eq (Y •S_LT X)))
(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)))
(926) Theorem 804: (M in Cm) •eq ((M = [car(M),cdr(M)]) & (car(M) in Re) & (cdr(M) in Re))