List of theorems referencing the symbol DOT_RA_MINUS
(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))
(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))
(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))
(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 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))))
(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])))) ))
(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]))))))
(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)))
(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}) )
(867) Theorem 713: [The embedding of signed integers into rationals preserves all elementary algebraic operations, 3] ((X in Si) & (Y in Si)) •imp (RaSi(X •S_MINUS Y) = RaSi(X) •Ra_MINUS 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)))