List of theorems referencing the symbol DOT_S_TIMES

(447) Theorem 354: ((N in Si) & (M in Si)) •imp ((N •S_PLUS M in Si) & (N •S_TIMES M in Si))
(454) Theorem 361: [The product 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_TIMES [N,M] = K •S_TIMES Red([N,M]))
(460) Theorem 367: [Commutative law for signed integer multiplication] ((N in Si) & (M in Si)) •imp (N •S_TIMES M = M •S_TIMES N)
(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])))
(466) Theorem 373: [n*-m=-(n*m) for signed integers] ((N in Si) & (M in Si)) •imp (N •S_TIMES S_Rev(M) = S_Rev(N •S_TIMES M))
(468) Theorem 375: [Inversion lemma] ((N in Si) & (M in Si)) •imp ((S_Rev(N •S_TIMES M) = S_Rev(N) •S_TIMES M) & (S_Rev(N •S_TIMES M) = N •S_TIMES S_Rev(M)))
(470) Theorem 377: [Associativity lemma] ((N in Za) & (M in Za) & (K in Za)) •imp ([N,0] •S_TIMES ([M,0] •S_TIMES [K,0]) = ([N,0] •S_TIMES [M,0]) •S_TIMES [K,0])
(471) Theorem 378: [Associativity lemma] ((K in Si) & (N in Za) & (M in Za)) •imp ([N,0] •S_TIMES ([M,0] •S_TIMES K) = ([N,0] •S_TIMES [M,0]) •S_TIMES K)
(472) Theorem 379: [Associativity lemma II] ((K in Si) & (N in Za) & (M in Si)) •imp ([N,0] •S_TIMES (M •S_TIMES K) = ([N,0] •S_TIMES M) •S_TIMES K)
(473) Theorem 380: [Associative law] ((K in Si) & (N in Si) & (M in Si)) •imp (N •S_TIMES (M •S_TIMES K) = (N •S_TIMES M) •S_TIMES K)
(477) Theorem 384: [Basic properties of the signed integers 0 and 1] (([0,1] •S_TIMES [0,1]) = [1,0]) & ((X in Si) •imp ((([1,0] •S_TIMES X) = X) & (([0,0] •S_TIMES X) = [0,0])))
(478) Theorem 385: [1 is the multiplicative unit for signed integers] (K in Si) •imp (K •S_TIMES [1,0] = K)
(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]))
(483) Theorem 390: [Si is an Integral Domain] ((N in Si) & (M in Si) & ((M •S_TIMES N) = [0,0])) •imp ((M = [0,0]) or (N = [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)
(485) Theorem 392: [Si multiplicative cancellation] ((N in Si) & (M in Si) & (K in Si) & (M •S_TIMES N = K •S_TIMES N) & (N /= [0,0])) •imp (M = K)
(486) Theorem 393: [Multiplication by -1] (N in Si) •imp (S_Rev(N) = [0,1] •S_TIMES N)
(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))
(562) Theorem 412: [The square of any signed integer is non-negative] (X in Si) •imp is_nonneg(X •S_TIMES X)
(563) Theorem 413: [The product of signed integers x,y of which x is positive is non-negative iff y is non-negative] ((X in Si) & (Y in Si) & (X /= [0,0]) & is_nonneg(X)) •imp (is_nonneg(X •S_TIMES Y) •eq is_nonneg(Y))
(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)]))
(568+) Theorem 419: [If two pairs of fractions are equivalent, their formal products are also equivalent] ((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 car(W),cdr(X) •S_TIMES cdr(W)],[car(Y) •S_TIMES car(Z),cdr(Y) •S_TIMES cdr(Z)])
(569) Theorem 420: [If two pairs of fractions are equivalent, their formal sums define the same rational number] ((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 car(W),cdr(X) •S_TIMES cdr(W)]) = Fr_to_Ra([car(Y) •S_TIMES car(Z),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)]))
(571) Theorem 422: [The product of a rational number and a formal fraction can be expressed as a product of formal fractions] ((X in Ra) & (Y in Si) & (Z in Si) & (Z /= [0,0])) •imp (X •Ra_TIMES Fr_to_Ra([Y,Z]) = Fr_to_Ra([car(arb(X)) •S_TIMES Y,cdr(arb(X)) •S_TIMES Z]))
(574) Theorem 425: [The sign of the product of the numerator and denominator of a fraction defines the sign of the rational number which it represents] ((X in Fr) & (Y in Fr) & Same_frac(X,Y)) •imp (is_nonneg(car(X) •S_TIMES cdr(X)) •eq is_nonneg(car(Y) •S_TIMES cdr(Y)))
(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]))
(580) Theorem 432: [?] ((X in Ra) & (Y in Si) & (Z in Si) & (Z /= [0,0])) •imp ((Fr_to_Ra([Y,Z]) •Ra_TIMES X) = Fr_to_Ra([car(arb(X)) •S_TIMES Y,cdr(arb(X)) •S_TIMES Z]))
(588) Theorem 440: [Muliplication of numerator and denominator by a common nonzero function does not change the rational number it represents] ((K in Si) & (N in Si) & (M in Si) & (K /= [0,0]) & (M /= [0,0])) •imp (Fr_to_Ra([N,M]) = Fr_to_Ra([K •S_TIMES N,K •S_TIMES M]))
(590) Theorem 442: [Expressing the sign of a rational in terms of the numerator and denominator of any representing fraction] ((X in Si) & (Y in Si) & (Y /= [0,0])) •imp (Ra_is_nonneg(Fr_to_Ra([X,Y])) •eq is_nonneg(X •S_TIMES Y))
(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)