List of theorems referencing the symbol DOT_TIMES
(269) Theorem 223: [Arithmetic multiplication lemma] (N •TIMES M) = (#N •TIMES #M)
(270) Theorem 224: [Arithmetic multiplication lemma 2] N •TIMES M = N •TIMES #M
(284) Theorem 237: [Anything times 0 is 0] (N •TIMES 0) = 0
(285) Theorem 238: [0 times anything is 0] (0 •TIMES N) = 0
(287) Theorem 240: [1 is a left multiplicative identity] (1 •TIMES N) = #N
(288) Theorem 241: [1 is a right multiplicative identity] (N •TIMES 1) = #N
(292) Theorem 245: [Commutative law for multiplication] N •TIMES M = M •TIMES N
(298) Theorem 251: [Associativity of arithmetic multiplication] N •TIMES (M •TIMES K) = (N •TIMES M) •TIMES K
(299) Theorem 252: [Arithmetic distributive law] N •TIMES (M •PLUS K) = (N •TIMES M) •PLUS (N •TIMES K)
(300) Theorem 253: [The arithmetic product of two finite sets is finite] (Finite(N) & Finite(M)) •imp Finite(N •TIMES M)
(302) Theorem 255: [If the product of two nonzero terms is finite, so are the terms] ((Finite(N) & Finite(M)) or N = 0 or M = 0) •eq Finite(N •TIMES 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))
(327) Theorem 280: [Monotonicity of multiplication] (M •incin N) •imp ((M •TIMES K) •incin (N •TIMES K))
(328) Theorem 281: [Strict monotonicity of integer multiplication] ((M in N) & (N in Za) & (K in Za) & (K /= 0)) •imp ((M •TIMES K) in (N •TIMES K))
(340) Theorem 293: [Integer division with remainder] ((M in Za) & (N in Za) & (N /= 0)) •imp (((M •OVER N) in Za) & (M incs ((M •OVER N) •TIMES N)) & ((M •MOD N) in N))
(341) Theorem 294: [If an integer product is zero, one of its factors is 0] (N •TIMES M = 0) •eq (N = 0 or M = 0)
(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])))
(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)))
(899) Theorem 744: ((X in Re) & (M in Za) & (N in Za)) •imp (((X •ToThe M) •ToThe N) = (X •ToThe (M •TIMES N)))