List of theorems referencing the symbol DOT_RA_TIMES

(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]))
(579) Theorem 431: [Commutativity of rational multiplication] ((N in Ra) & (M in Ra)) •imp ((N •Ra_TIMES M in Ra) & (N •Ra_TIMES M = M •Ra_TIMES N))
(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]))
(587) Theorem 439: [Associative law for rational multiplication] ((K in Ra) & (N in Ra) & (M in Ra)) •imp (N •Ra_TIMES (M •Ra_TIMES K) = (N •Ra_TIMES M) •Ra_TIMES K)
(589) Theorem 441: [Distributive law for rationals] ((K in Ra) & (N in Ra) & (M in Ra)) •imp (N •Ra_TIMES (M •Ra_PLUS K) = (N •Ra_TIMES M) •Ra_PLUS (N •Ra_TIMES K))
(592) Theorem 444: [The unit rational is the rational multiplicative identity] (M in Ra) •imp (M = M •Ra_TIMES Ra_1)
(593) Theorem 445: [Multiplication of a rational by its reciprocal gives 1] ((M in Ra) & (M /= Ra_0)) •imp ((Recip(M) in Ra) & (M •Ra_TIMES Recip(M) = Ra_1))
(594) Theorem 446: ((N in Ra) & (M in Ra) & (M /= Ra_0)) •imp (((N •Ra_TIMES (M •Ra_TIMES M)) •Ra_TIMES (Recip(M) •Ra_TIMES Recip(M))) = N)
(595) Theorem 447: [Rational division is multiplication by the reciprocal] ((N in Ra) & (M in Ra) & (M /= Ra_0)) •imp (N = M •Ra_TIMES (N •Ra_OVER M))
(606) Theorem 458: [The unit rational is the identity for multiplication] (X in Ra) •imp (X = X •Ra_TIMES Ra_1)
(608) Theorem 460: [The sum and product of two non-negative rationals is non-negative] ((X in Ra) & (Y in Ra) & Ra_is_nonneg(X) & Ra_is_nonneg(Y)) •imp (Ra_is_nonneg(X •Ra_PLUS Y) & Ra_is_nonneg(X •Ra_TIMES Y))
(614) Theorem 466: [First law of signs for rational multiplication] ((X in Ra) & (Y in Ra)) •imp ((X •Ra_TIMES Ra_Rev(Y)) = Ra_Rev(X •Ra_TIMES Y))
(615) Theorem 467: [The reverse of a rational X is the reverse of 1, times X] (X in Ra) •imp (Ra_Rev(X) = (Ra_Rev(Ra_1) •Ra_TIMES X))
(616) Theorem 468: ((X in Ra) & (Y in Ra) & (Z in Ra)) •imp ((X •Ra_TIMES (Y •Ra_MINUS Z)) = (X •Ra_TIMES Y) •Ra_MINUS (X •Ra_TIMES Z))
(617) Theorem 469: [Strict monotonicity of rational multiplication over 1st argument] ((X in Ra) & (Y in Ra) & (X1 in Ra) & (X •Ra_GT Y) & (X1 •Ra_GT Ra_0)) •imp ((X •Ra_TIMES X1) •Ra_GT (Y •Ra_TIMES X1))
(618) Theorem 470: (X in Ra) •imp (X •Ra_TIMES Ra_0 = Ra_0)
(618+) Theorem 471: ((X in Ra) & (Y in Ra) & (X •Ra_GT Ra_0) & (Y •Ra_GT Ra_0)) •imp ((X •Ra_TIMES Y) •Ra_GT Ra_0)
(644) Theorem 497: ((X in Ra) & (Y in Ra) & (XP in Ra) & (YP in Ra) & (X •Ra_GE Y) & (Y •Ra_GE Ra_0) & (YP •Ra_GE Ra_0) & (XP •Ra_GE YP)) •imp ((X •Ra_TIMES XP) •Ra_GE (Y •Ra_TIMES YP))
(645) Theorem 498: ((X in Ra) & (Y in Ra) & (XP in Ra) & (YP in Ra) & (X •Ra_GT Y) & (Y •Ra_GT Ra_0) & (YP •Ra_GT Ra_0) & (XP •Ra_GE YP)) •imp ((X •Ra_TIMES XP) •Ra_GT (Y •Ra_TIMES YP))
(652) Theorem 505: [?] (X in Ra) •imp ((X •Ra_TIMES X) •Ra_GE Ra_0)
(658) Theorem 511: [The absolute value of a rational product is the product of the absolute values] ((X in Ra) & (Y in Ra)) •imp (Ra_ABS(X •Ra_TIMES Y) = (Ra_ABS(X) •Ra_TIMES Ra_ABS(Y)))
(659) Theorem 512: [If the product of two rationals is 0, one of them is 0] ((X in Ra) & (Y in Ra)) •imp (((X •Ra_TIMES Y) = Ra_0) •eq ((X = Ra_0) or (Y = Ra_0)))
(660) Theorem 513: [Cancellation rule for rational multiplication] ((X in Ra) & (Y in Ra) & (U in Ra) & (X /= Ra_0) & ((X •Ra_TIMES Y) = (X •Ra_TIMES U))) •imp (Y = U)
(661) Theorem 514: [The reciprocal of a rational product is the product of the reciprocals] ((X in Ra) & (Y in Ra) & (X /= Ra_0) & (Y /= Ra_0)) •imp (Recip(X •Ra_TIMES Y) = (Recip(X) •Ra_TIMES Recip(Y)))
(662) Theorem 515: [Formula for the sum of two rational quotients] ((X in Ra) & (Y in Ra) & (U in Ra) & (V in Ra) & (X /= Ra_0) & (Y /= Ra_0)) •imp (((U •Ra_OVER X) •Ra_PLUS (V •Ra_OVER Y)) = (((Y •Ra_TIMES U) •Ra_PLUS (X •Ra_TIMES V)) •Ra_OVER (X •Ra_TIMES Y)))
(663) Theorem 516: ((X in Ra) & (Y in Ra) & (X /= Ra_0) & (Y /= Ra_0)) •imp ((Recip(X) •Ra_MINUS Recip(Y)) = ((Y •Ra_MINUS X) •Ra_OVER (X •Ra_TIMES Y)))
(665) Theorem 519: ((X in Ra) & (Y in Ra) & (A in Ra) & (B in Ra) & (Ra_ABS(X) •Ra_GT A) & (Ra_ABS(Y) •Ra_GT B) & (A •Ra_GT Ra_0) & (B •Ra_GT Ra_0)) •imp (Ra_ABS(Recip(X) •Ra_MINUS Recip(Y)) •Ra_LE (Ra_ABS(X •Ra_MINUS Y) •Ra_TIMES (Recip(A) •Ra_TIMES Recip(B))))
(686) Theorem 535: ({F,G} •incin RaSeq) •imp (((F •Ras_PLUS G) in RaSeq) & (Ras_ABS(G) in RaSeq) & (Ras_Rev(G) in RaSeq) & ((F •Ras_TIMES G) in RaSeq) & ((F •Ras_PLUS G) = {[u,((F~[u]) •Ra_PLUS (G~[u]))]: u in Za}) & (Ras_ABS(G) = {[u,Ra_ABS(G~[u])]: u in Za}) & (Ras_Rev(G) = {[u,Ra_Rev(G~[u])]: u in Za}) & ((F •Ras_TIMES G) = {[u,((F~[u]) •Ra_TIMES (G~[u]))]: u in Za}))
(687) Theorem 536: (({F1,G1} •incin RaSeq) & (N in Za)) •imp ((F1~[N] in Ra) & (G1~[N] in Ra) & ((F1 •Ras_PLUS G1 in RaSeq) & ((F1 •Ras_PLUS G1)~[N] = (F1~[N]) •Ra_PLUS (G1~[N]))) & (((Ras_ABS(G1) in RaSeq) & (Ras_ABS(G1)~[N] = Ra_ABS(G1~[N])))) & (((Ras_Rev(G1) in RaSeq) & (Ras_Rev(G1)~[N] = Ra_Rev(G1~[N])))) & (((F1 •Ras_TIMES G1 in RaSeq) & (F1 •Ras_TIMES G1)~[N] = ((F1~[N]) •Ra_TIMES (G1~[N])))))
(858) Theorem 705: [The embedding of rationals into reals preserves all elementary algebraic operations, 2] ((X in Ra) & (Y in Ra)) •imp ((ReRa(X) in Re) & (ReRa(Y) in Re) & (ReRa(X •Ra_PLUS Y) = ReRa(X) •R_PLUS ReRa(Y)) & (ReRa(X •Ra_TIMES Y) = ReRa(X) •R_TIMES ReRa(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)))