List of theorems referencing the symbol S_REV
(448) Theorem 355: [Sign reversal and subtraction for signed integers] ((N in Si) & (M in Si)) •imp ((S_Rev(M) in Si) & (N •S_MINUS M in Si))
(465) Theorem 372: [Sign-reversal of signed integers] ((N in Za) & (M in Za)) •imp (S_Rev(Red([M,N])) = Red([N,M]))
(466) Theorem 373: [n*-m=-(n*m) for signed integers] ((N in Si) & (M in Si)) •imp (N •S_TIMES S_Rev(M) = S_Rev(N •S_TIMES M))
(467) Theorem 374: [Basic properties of the signed negative] (N in Si) •imp ((S_Rev(N) in Si) & (S_Rev(N) •S_PLUS N = [0,0]) & (S_Rev(S_Rev(N)) = N))
(468) Theorem 375: [Inversion lemma] ((N in Si) & (M in Si)) •imp ((S_Rev(N •S_TIMES M) = S_Rev(N) •S_TIMES M) & (S_Rev(N •S_TIMES M) = N •S_TIMES S_Rev(M)))
(469) Theorem 376: [Inversion lemma II] (N in Si) •imp (S_Rev(S_Rev(N)) = N)
(474) Theorem 381: [Subtraction is addition of the negative] ((N in Si) & (M in Si)) •imp ((N •S_MINUS M) = (N •S_PLUS S_Rev(M)))
(476) Theorem 383: [The negative of a sum is the sum of the negatives] ((N in Si) & (M in Si)) •imp (S_Rev(N •S_PLUS M) = S_Rev(N) •S_PLUS S_Rev(M))
(486) Theorem 393: [Multiplication by -1] (N in Si) •imp (S_Rev(N) = [0,1] •S_TIMES N)
(557+) Theorem 407: [If a signed integer and its additive inverse are both nonnegative, the signed integer is zero] (X in Si) •imp ((is_nonneg(X) or is_nonneg(S_Rev(X))) & ((is_nonneg(X) & is_nonneg(S_Rev(X))) •imp (X = [0,0])))
(559) Theorem 409: ([0,0] in Si) & (FORALL x in Si | ((x •S_PLUS [0,0]) = x) & ((x •S_PLUS S_Rev(x)) = [0,0]) & (S_Rev(x) in Si)) & (FORALL x in Si, y in Si | ((x •S_PLUS y) in Si) & ((x •S_PLUS y) = (y •S_PLUS x)) & ((x •S_PLUS S_Rev(y)) = (x •S_MINUS y))) & (FORALL x in Si, y in Si, z in Si | ((x •S_PLUS y) •S_PLUS z) = (x •S_PLUS (y •S_PLUS z))) & (FORALL x in Si, y in Si | (is_nonneg(x) & is_nonneg(y)) •imp is_nonneg(x •S_PLUS y)) & (FORALL x in Si | (is_nonneg(x) or is_nonneg(S_Rev(x))) & ((is_nonneg(x) & is_nonneg(S_Rev(x))) •imp (x = [0,0])))
(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))
(572) Theorem 423: [Reversing both the numerator and denominator of a formal fraction does not change the rational it represents] (X in Fr) •imp Same_frac(X,[S_Rev(car(X)),S_Rev(cdr(X))])
(575) Theorem 426: [?] (X in Fr) •imp (Fr_is_nonneg(X) •eq Fr_is_nonneg([S_Rev(car(X)),S_Rev(cdr(X))]))
(612) Theorem 464: [Reversing the numerators of two equivalent rational fractions leaves them equivalent] ((X in Si) & (Y in Si) & (XP in Si) & (YP in Si) & Same_frac([X,Y],[XP,YP])) •imp Same_frac([S_Rev(X),Y],[S_Rev(XP),YP])
(613) Theorem 465: [Alternate form of Theorem 464] ((X in Si) & (Y in Si) & (Y /= [0,0])) •imp (Ra_Rev(Fr_to_Ra([X,Y])) = Fr_to_Ra([S_Rev(X),Y]))
(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))))