List of theorems referencing the symbol DOT_R_MINUS
(744) Theorem 593: ({X,Y} •incin Re) •imp (((X •R_MINUS Y) in Re) & ((X •R_TIMES Y) in Re))
(760) Theorem 609: [0 is right identity for real subtraction] (X in Re) •imp (X •R_MINUS R_0 = X)
(761) Theorem 610: [Real subtraction principle] (X in Re) •imp (X •R_MINUS X = R_0)
(764) Theorem 614: [Real subtraction is addition of the negative] ((X in Re) & (Y in Re)) •imp ((X •R_MINUS Y) = (X •R_PLUS R_Rev(Y)))
(768) Theorem 618: [Real addition-subtraction commutativity] ((X in Re) & (Y in Re) & (V in Re)) •imp (X •R_MINUS (Y •R_PLUS V) = (X •R_MINUS Y) •R_MINUS V)
(769) Theorem 619: [Real subtraction reverses addition] ((X in Re) & (Y in Re)) •imp ((X •R_PLUS Y) •R_MINUS Y = X)
(770) Theorem 620: [Real subtraction reverses addition, 2] ((X in Re) & (Y in Re)) •imp (X = (Y •R_PLUS (X •R_MINUS Y)))
(772) Theorem 622: [Distributivity of multiplication over subtraction] ((X in Re) & (Y in Re) & (V in Re)) •imp ((X •R_TIMES (Y •R_MINUS V)) = ((X •R_TIMES Y) •R_MINUS (X •R_TIMES V)))
(773) Theorem 623: [Additive inverse of real difference] ((X in Re) & (Y in Re)) •imp (R_Rev(X •R_MINUS Y) = (Y •R_MINUS X))
(789) Theorem 639: [Distributivity of division over subtraction] ((X in Re) & (Y in Re) & (V in Re) & (V /= R_0)) •imp (((X •R_MINUS Y) •R_OVER V) = ((X •R_OVER V) •R_MINUS (Y •R_OVER V)))
(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))
(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)))
(880) Theorem 725: [The limit of a difference is the difference of limits] ((F in ReCauchy) & (G in ReCauchy)) •imp (limit(F •Res_MINUS G) = limit(F) •R_MINUS limit(G))
(902) Theorem 747: ((F in Fin_Seqs(Re)) & (G in Fin_Seqs(Re)) & (X in Re)) •imp (((Polval(F,X) •R_PLUS Polval(G,X)) = Polval(F •PolPlus G,X)) & ((Polval(F,X) •R_MINUS Polval(G,X)) = Polval(F •PolMinus G,X)) & ((Polval(F,X) •R_TIMES Polval(G,X)) = Polval(F •PolTimes G,X)))
(921) Theorem 20001: ((N in Re) & (M in Re)) •imp (((abs(N) •R_PLUS abs(M)) •R_GT abs(N •R_MINUS M)) or ((abs(N) •R_PLUS abs(M)) = abs(N •R_MINUS M)))