List of theorems referencing the symbol DOT_S_PLUS

(447) Theorem 354: ((N in Si) & (M in Si)) •imp ((N •S_PLUS M in Si) & (N •S_TIMES M in Si))
(452) Theorem 359: [The signed sum of two integer pairs is the sum of the first with the reduced form of the second] ((J in Za) & (K in Za) & (N in Za) & (M in Za)) •imp ([J,K] •S_PLUS [N,M] = [J,K] •S_PLUS Red([N,M]))
(453) Theorem 360: [The sum of a signed integer and an integer pair remains the same if the pair is reduced] ((K in Si) & (N in Za) & (M in Za)) •imp (K •S_PLUS [N,M] = K •S_PLUS Red([N,M]))
(455) Theorem 362: [Commutativity lemma for signed integers] ((K in Si) & (N in Za) & (M in Za)) •imp (K •S_PLUS [N,M] = [N,M] •S_PLUS K)
(456) Theorem 363: [Commutativity lemma for signed integers, 2] ((J in Za) & (K in Za) & (N in Za) & (M in Za)) •imp ([J,K] •S_PLUS [N,M] = [N,M] •S_PLUS [J,K])
(457) Theorem 364: [Commutative law for signed integer addition] ((N in Si) & (M in Si)) •imp (N •S_PLUS M = M •S_PLUS N)
(458) Theorem 365: [The sum of two integer pairs remains the same if the first is reduced] ((J in Za) & (K in Za) & (N in Za) & (M in Za)) •imp ([J,K] •S_PLUS [N,M] = Red([J,K]) •S_PLUS [N,M])
(459) Theorem 366: [The sum of two integer pairs remains the same if both are reduced] ((J in Za) & (K in Za) & (N in Za) & (M in Za)) •imp ([J,K] •S_PLUS [N,M] = Red([J,K]) •S_PLUS Red([N,M]))
(461) Theorem 368: [Associative law for signed integer addition] ((K in Si) & (N in Si) & (M in Si)) •imp (N •S_PLUS (M •S_PLUS K) = (N •S_PLUS M) •S_PLUS K)
(462) Theorem 369: [Distributive law for signed integers] ((K in Si) & (N in Si) & (M in Si)) •imp (N •S_TIMES (M •S_PLUS K) = (N •S_TIMES M) •S_PLUS (N •S_TIMES K))
(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])))
(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))
(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))
(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))
(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]))
(481) Theorem 388: [0 is the right additive identity for signed integers] (K in Si) •imp (K •S_PLUS [0,0] = K)
(482) Theorem 389: [0 is the left additive identity for signed integers] (K in Si) •imp ([0,0] •S_PLUS K = K)
(558) Theorem 408: [The sum of two non-negative signed integers is non-negative] (((X in Si) & (Y in Si) & is_nonneg(X) & is_nonneg(Y))) •imp (is_nonneg(X •S_PLUS Y) & is_nonneg(X •S_TIMES Y))
(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))
(567) Theorem 417: [Fractions are equivalent if their cross-products are equal] ((X in Fr) & (Y in Fr) & Same_frac(X,Y) & (W in Fr) & (Z in Fr) & Same_frac(W,Z)) •imp Same_frac([(car(X) •S_TIMES cdr(W)) •S_PLUS (car(W) •S_TIMES cdr(X)),cdr(X) •S_TIMES cdr(W)], [(car(Y) •S_TIMES cdr(Z)) •S_PLUS (car(Z) •S_TIMES cdr(Y)),cdr(Y) •S_TIMES cdr(Z)])
(568) Theorem 418: [If two pair of fractions are equivalent, their formal sums are also equivalent] ((X in Fr) & (Y in Fr) & Same_frac(X,Y) & (W in Fr) & (Z in Fr) & Same_frac(W,Z)) •imp (Fr_to_Ra([(car(X) •S_TIMES cdr(W)) •S_PLUS (car(W) •S_TIMES cdr(X)),cdr(X) •S_TIMES cdr(W)]) = Fr_to_Ra([(car(Y) •S_TIMES cdr(Z)) •S_PLUS (car(Z) •S_TIMES cdr(Y)),cdr(Y) •S_TIMES cdr(Z)]))
(570) Theorem 421: [The sum of a rational number and a formal fraction can be expressed as a sum of formal fractions] ((X in Ra) & (Y in Si) & (Z in Si) & (Z /= [0,0])) •imp (X •Ra_PLUS Fr_to_Ra([Y,Z]) = Fr_to_Ra([(car(arb(X)) •S_TIMES Z) •S_PLUS (cdr(arb(X)) •S_TIMES Y),(cdr(arb(X)) •S_TIMES Z)]))
(578) Theorem 429: [?] ((X in Ra) & (Y in Si) & (Z in Si) & (Z /= [0,0])) •imp (Fr_to_Ra([Y,Z]) •Ra_PLUS X = Fr_to_Ra([(car(arb(X)) •S_TIMES Z) •S_PLUS (cdr(arb(X)) •S_TIMES Y),(cdr(arb(X)) •S_TIMES Z)]))
(578+) Theorem 430: [?] ((X in Si) & (Y in Si) & (Z in Si) & (W in Si) & (Y /= [0,0]) & (W /= [0,0])) •imp (Fr_to_Ra([X,Y]) •Ra_PLUS Fr_to_Ra([Z,W]) = Fr_to_Ra([(X •S_TIMES W) •S_PLUS (Z •S_TIMES Y),Y •S_TIMES W]))
(866) Theorem 712: [The embedding of signed integers into rationals preserves all elementary algebraic operations, 2] ((X in Si) & (Y in Si)) •imp ((RaSi(X) in Ra) & (RaSi(Y) in Ra) & (RaSi(X •S_PLUS Y) = RaSi(X) •Ra_PLUS RaSi(Y)) & (RaSi(X •S_TIMES Y) = RaSi(X) •Ra_TIMES RaSi(Y)))
(870) Theorem 717: [The embedding of integers into signed integers preserves all elementary algebraic operations on integers] ((X in Za) & (Y in Za)) •imp ((SiZa(X) in Si) & (SiZa(Y) in Si) & (SiZa(X •PLUS Y) = SiZa(X) •S_PLUS SiZa(Y)) & (SiZa(X •TIMES Y) = SiZa(X) •S_TIMES SiZa(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)