List of theorems referencing the symbol DOT_PLUS

(258) Theorem 212: [Monotonicity of arithmetic addition] ((N incs N1) and (M incs M1)) •imp (N •PLUS M incs N1 •PLUS M1)
(259) Theorem 213: [Disjoint sum lemma] (N * M = 0) •imp (N •PLUS M = #(N + M))
(260) Theorem 214: [Arithmetic addition lemma] N •PLUS M = #N •PLUS #M
(261) Theorem 215: [Second Disjoint sum lemma] (N * M = 0) •imp (#N •PLUS #M = #(N + M))
(264) Theorem 218: [Cardinality of a Cartesian product union] (A /= B) •imp (#N •PLUS #M = #((N •PROD {A}) + (M •PROD {B})))
(265) Theorem 219: [Arithmetic addition lemma 2] N •PLUS M = N •PLUS #M
(266) Theorem 220: [Arithmetic addition lemma 3] N •PLUS M = #N •PLUS M
(267) Theorem 221: [Arithmetic associativity lemma] ((N * M = 0) & (N * K = 0) & (M * K = 0)) •imp (((N •PLUS M) •PLUS K) = #((N + M) + K))
(268) Theorem 222: [Arithmetic associativity lemma 2] ((N * M = 0) & (N * K = 0) & (M * K = 0)) •imp ((N •PLUS (M •PLUS K)) = #(N + (M + K)))
(279) Theorem 232: [An arithmetic sum is finite if its two terms are finite] Finite(N •PLUS M) •eq Finite(N + M)
(280) Theorem 233: [An arithmetic sum is finite if and only if both its terms are finite] (Finite(N) & Finite(M)) •eq Finite(N •PLUS M)
(286) Theorem 239: [0 is a right additive identity] (#N •PLUS 0) = #N
(290) Theorem 243: [Distributivity lemma] (A /= B) •imp (N •PLUS M = #((N •PROD {A}) + (M •PROD {B})))
(291) Theorem 244: [Commutative law for addition] (N •PLUS M) = (M •PLUS N)
(293) Theorem 246: [0 is bilateral additive identity] (X in Za) •imp (((X •PLUS 0) = X) & ((0 •PLUS X) = X))
(297) Theorem 250: [Associativity of arithmetic addition] N •PLUS (M •PLUS K) = (N •PLUS M) •PLUS K
(299) Theorem 252: [Arithmetic distributive law] N •TIMES (M •PLUS K) = (N •TIMES M) •PLUS (N •TIMES K)
(309) Theorem 262: [Subtraction lemma] (M •incin N) •imp (#N = #M •PLUS (N •MINUS M))
(310) Theorem 263: [Subtraction in the non-negative case] (M •incin N) •imp (#N = (N •MINUS M) •PLUS M)
(311) Theorem 264: [Subtraction lemma 2] (#M in #N or #M = #N) •imp (#N = #M •PLUS (#N •MINUS #M))
(317) Theorem 270: [Closure properties of arithmetic operators] ((N in Za) & (M in Za)) •imp ((N •PLUS M in Za) & (N •TIMES M in Za) & (N •MINUS M in Za))
(318) Theorem 271: [Strict monotonicity of addition] ((M in Za) & (N in Za) & (N /= 0)) •imp (M in (M •PLUS N))
(320) Theorem 273: [Strict monotonicity of addition] ((M in Za) & (N in Za) & (K in N)) •imp (M •PLUS K in M •PLUS N)
(321) Theorem 274: [Strict monotonicity of addition] ((M in Za) & (N in Za) & (K in N)) •imp (M •PLUS K in M •PLUS N)
(322) Theorem 275: [Strict monotonicity of addition, 2] ((M in Za) & (N in Za) & (K in N)) •imp (K •PLUS M in N •PLUS M)
(323) Theorem 276: [Cancellation] ((M in Za) & (N in Za) & (K in Za) & (M •PLUS K = N •PLUS K)) •imp (M = N)
(324) Theorem 277: [Monotonicity of addition] (M •incin N) •imp ((M •PLUS K) •incin (N •PLUS K))
(325) Theorem 278: [Monotonicity of addition, 2] Card(M) •imp ((M •incin (I •PLUS M)) & (M •incin (M •PLUS I)))
(326) Theorem 279: [Monotonicity of addition, 3] (M in Za) •imp ((M •incin (I •PLUS M)) & (M •incin (M •PLUS I)) & ((M •PLUS I) notin M) & ((I •PLUS M) notin M))
(329) Theorem 282: [The sum of non-negative integers is at least as big at each addend] ((X in Za) & (Y in Za)) •imp ((X •PLUS Y) notin Y)
(330) Theorem 283: [Strict monotonicity of addition] ((M in Za) & (N in Za) & (K in Za)) •imp (((M •PLUS K) •incin (N •PLUS K)) •eq (M •incin N))
(331) Theorem 284: [Strict monotonicity of addition] ((M in Za) & (N in M) & (K in Za)) •imp ((N •PLUS K) in (M •PLUS K))
(337) Theorem 290: [Addition-subtraction commutativity] ((M in Za) & (N in Za) & (K in Za) & (N incs M) & ((N •MINUS M) incs K)) •imp ((N incs (M •PLUS K)) & (N •MINUS (M •PLUS K) = (N •MINUS M) •MINUS K))
(338) Theorem 291: [Subtraction reverses addition] ((M in Za) & (N in Za)) •imp ((M •PLUS N) •MINUS N = M)
(344) Theorem 297: [Strong monotonicity of integer addition] ((N in Za) & (M in Za) & (K in Za)) •imp ((N incs M) •eq ((N •PLUS K) incs (M •PLUS K)))
(345) Theorem 298: [Addition reverses subtraction] (N incs M) •imp (#N = #M •PLUS #(N - M))
(346) Theorem 299: [Addition-subtraction commutativity, 2] ((N in Za) & (M in Za) & (K in Za) & (N incs M)) •imp ((N •PLUS K) •MINUS (M •PLUS K) = N •MINUS M)
(347) Theorem 300: [Addition-subtraction lemma] ((N in Za) & (M in Za)) •imp (N = (M •PLUS (N •MINUS M)) or N = (M •MINUS (M •MINUS N)))
(348) Theorem 301: [The successor integer as a sum] (N •PLUS 1) = #next(N)
(349) Theorem 302: [The successor integer as a sum, 2] (N in Za) •imp ((next(N) in Za) & ((N •PLUS 1) = next(N)))
(352) Theorem 305: [Every nonzero integer has a predecessor] ((M in Za) & (M /= 0)) •imp (M = (Un(M) •PLUS 1))
(353) Theorem 306: [The sum of integers as the union of smaller sums] ((X in Za) & (Y in Za)) •imp ((X •PLUS Y) = X + {(X •PLUS u): u in Y})
(354) Theorem 307: [The sum of integers as the union of smaller sums, 2] ((X in Za) & (Y in Za)) •imp ((X •PLUS Y) = X + {(u •PLUS X): u in Y})
(355) Theorem 308: [Subtraction reverses addition] ((X in Za) & (Y in Za) & (Y •incin X)) •imp (X = Y •PLUS (X •MINUS Y))
(356) Theorem 309: [Subtraction monotonicity lemma, 2] ((X in Za) & (Y in Za) & (U in (X •PLUS Y)) & (Y /= 0)) •imp ((U •MINUS X) in Y)
(358) Theorem 311: [The integer difference as a set of smaller differences] ((N in Za) & (M in Za)) •imp ((N •MINUS M) = {k in Za | (k •PLUS M) in N})
(373) Theorem 322: [The shift-map of an integer is single-valued and maps Za into Za] ((M in Za) & (N in Za)) •imp (Svm(Shift(M)) & (domain(Shift(M)) = Za) & (range(Shift(M)) •incin Za) & (Shift(M)~[N] = M •PLUS N))
(374) Theorem 323: [Composition of shift-maps yields a shift-map] ((M in Za) & (N in Za)) •imp (Shift(M) @ Shift(N) = Shift(M •PLUS N))
(375) Theorem 324: [Double shifting can be emulated by a single shift] ((M in Za) & (N in Za)) •imp (shifted_seq(shifted_seq(F,M),N) = shifted_seq(F,M •PLUS N))
(379) Theorem 328: [Properties of finite and shifted finite sequences] ((F in Fin_seqs(S)) & (G in Fin_seqs(S))) •imp (Svm({[car(x) •PLUS #F, cdr(x)]: x in G}) & (domain(F) * domain({[car(x) •PLUS #F, cdr(x)]: x in G}) = 0))
(381) Theorem 330: [Concatenation of finite sequences] ((F in Fin_seqs(S)) & (G in Fin_seqs(S))) •imp ((concat(F,G) in Fin_seqs(S)) & (domain(concat(F,G)) = domain(F) •PLUS domain(G)) & (range(concat(F,G)) = range(F) + range(G))) & ((U in domain(F) •PLUS domain(G)) •imp (concat(F,G)~[U] = if U in domain(F) then F~[U] else G~[U •MINUS domain(F)] end if))
(439) Theorem 346: [The sum of two infinite quantities is their maximum] (not Finite(S)) •imp ((S •PLUS T) = #S + #T)
(450) Theorem 357: [Reduction removes any common value added to the components of an integer pair] ((J in Za) & (K in Za) & (M in Za)) •imp (Red([J •PLUS M,K •PLUS M]) = Red([J,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])))
(679) Theorem 528: ((F in RaSeq) & (N in Za) & (I in Za)) •imp ((shifted_seq(F,N)~[I]) = (F~[N •PLUS I]))
(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)))
(898) Theorem 743: (X in Re) •imp ((X •ToThe 0 = R_0) & (X •ToThe 1 = X) & (((M in Za) & (N in Za)) •imp (X •ToThe (M •PLUS N) = (X •ToThe M) •R_TIMES (X •ToThe N))))