List of theorems referencing the symbol DOT_MINUS
(305) Theorem 258: [Arithmetic subtraction principle] N •MINUS N = 0
(306) Theorem 259: [0 is right identity for arithmetic subtraction] N •MINUS 0 = #N
(308) Theorem 261: [Excess subtraction lemma] (Ord(Y) & (X in Y)) •imp ((X •MINUS Y) = 0)
(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))
(332) Theorem 285: [Subtraction Lemma] (N in Za) •imp ((N •MINUS M) in Za)
(333) Theorem 286: [Strict monotonicity of subtraction] ((N in Za) & (M in Za) & (K in N) & (M incs N)) •imp ((M •MINUS N) in (M •MINUS K))
(334) Theorem 287: [Monotonicity of subtraction] (K incs M) •imp ((K •MINUS N) incs (M •MINUS N))
(335) Theorem 288: [Monotonicity of subtraction, 2] (M incs N) •imp ((K •MINUS N) incs (K •MINUS M))
(336) Theorem 289: [Strict monotonicity of subtraction, 2] ((N in Za) & (M in Za) & (K in M) & (K incs N)) •imp ((K •MINUS N) in (M •MINUS N))
(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)
(342) Theorem 295: [Subtraction monotonicity lemma] (N incs M) •imp ((N •MINUS K) incs (M •MINUS K))
(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)))
(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)
(357) Theorem 310: [The integer difference as a set of smaller differences] ((N in Za) & (M in Za)) •imp ((N •MINUS M) = {k •MINUS M: k in N | M •incin k})
(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})
(378) Theorem 327: [Form of a shifted sequence] ((M in Za) & (domain(F) •incin Za)) •imp (shifted_seq(F,M) = {[car(x) •MINUS M,cdr(x)]: x in F | car(x) incs M})
(380) Theorem 329: ((F in Fin_seqs(S)) & (M in Za)) •imp (((F •ON M) in Fin_seqs(S)) & (shifted_seq(F,M) in Fin_seqs(S)) & (domain(shifted_seq(F,M)) = (#F •MINUS M)))
(451) Theorem 358: [The intersection of two unsigned integers is the smaller of the two] ((N in Za) & (M in Za)) •imp (((N * M) in Za) & ((N * M) in {N,M}) & ((N •MINUS (N * M)) in Za) & ((M •MINUS (N * M)) in Za))
(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])))