List of theorems referencing the symbol DOT_S_MINUS
(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))
(464) Theorem 371: [Embedding of Integers in Signed Integers] ((N in Za) & (M in Za)) •imp (([N •PLUS M,0] = [N,0] •S_PLUS [M,0] & [N •TIMES M,0] = [N,0] •S_TIMES [M,0]) & ((N incs M) •imp ([N,0] •S_MINUS [M,0] = [N •MINUS M,0])))
(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)))
(475) Theorem 382: [Subtraction reverses signed integer addition] ((N in Si) & (M in Si)) •imp (N = M •S_PLUS (N •S_MINUS M))
(479) Theorem 386: [The negative of a signed integer is its product by -1] ((K in Si) & (M in Si)) •imp (K •S_MINUS M = K •S_PLUS (M •S_TIMES [0,1]))
(480) Theorem 387: [A signed integer minus itself gives 0] (K in Si) •imp (K •S_MINUS K = [0,0])
(484) Theorem 391: [Distributivity of multiplication over subtraction] ((N in Si) & (M in Si) & (K in Si)) •imp ((m •S_TIMES n) •S_MINUS (k •S_TIMES n) = (m •S_MINUS k) •S_TIMES n)
(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])))
(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))
(920) Theorem 20000: ((N in Si) & (M in Si) & (M /= [0,0]) & is_nonneg(M)) •imp (EXISTS k in Si | is_nonneg(N •S_MINUS (k •S_TIMES M)) & is_nonneg(((k •S_PLUS [1,0])•S_TIMES M)) •S_MINUS N)