List of theorems referencing the symbol DOT_R_TIMES

(744) Theorem 593: ({X,Y} •incin Re) •imp (((X •R_MINUS Y) in Re) & ((X •R_TIMES Y) in Re))
(748) Theorem 597: [Commutative law for real multiplication] ({X,Y} •incin Re) •imp ((X •R_TIMES Y) = (Y •R_TIMES X))
(749) Theorem 598: [Elementary algebraic lemma for real multiplication] ((X in RaCauchy) & (Y in RaCauchy)) •imp (Cauchy_to_Re(X •Ras_TIMES Y) = (Cauchy_to_Re(X) •R_TIMES Cauchy_to_Re(Y)))
(750) Theorem 599: [Associative law for real multiplication] ({X,Y,V} •incin Re) •imp ((X •R_TIMES (Y •R_TIMES V)) = ((X •R_TIMES Y) •R_TIMES V))
(751) Theorem 600: [Distributive law for real multiplication] ({X,Y,V} •incin Re) •imp ((X •R_TIMES (Y •R_PLUS V)) = ((X •R_TIMES Y) •R_PLUS (X •R_TIMES V)))
(753) Theorem 602: [Law of signs for real multiplication] ({X,Y} •incin Re) •imp (((X •R_TIMES R_Rev(Y)) = R_Rev(X •R_TIMES Y)) & ((R_Rev(X) •R_TIMES Y) = R_Rev(X •R_TIMES Y)) & ((R_Rev(X) •R_TIMES R_Rev(Y)) = (X •R_TIMES Y)))
(754) Theorem 603: [Any real times 0 is 0] (X in Re) •imp ((X •R_TIMES R_0) = R_0)
(755) Theorem 604: [0 times any real is 0] (X in Re) •imp (R_0 •R_TIMES X = R_0)
(757) Theorem 606: [1 is a right multiplicative identity for reals] (X in Re) •imp (X •R_TIMES R_1 = X)
(758) Theorem 607: [1 is a left multiplicative identity for reals] (X in Re) •imp (R_1 •R_TIMES X = X)
(771) Theorem 621: [Multiplication by R_Rev(R_1)] (X in Re) •imp (R_Rev(X) = R_Rev(R_1) •R_TIMES X)
(772) Theorem 622: [Distributivity of multiplication over subtraction] ((X in Re) & (Y in Re) & (V in Re)) •imp ((X •R_TIMES (Y •R_MINUS V)) = ((X •R_TIMES Y) •R_MINUS (X •R_TIMES V)))
(774) Theorem 624: [Real reciprocal principle] ((X in Re) & (X /= R_0)) •imp (X •R_TIMES R_Recip(X) = R_1)
(776) Theorem 626: [Basic properties of the reciprocal for reals] ((X in Re) & (X /= R_0)) •imp ((R_Recip(X) in Re) & (R_Recip(X) /= R_0) & ((R_Recip(X) •R_TIMES X) = R_1))
(779) Theorem 629: [Real multiplicative Cancellation] ((X in Re) & (Y in Re) & (V in Re) & (X •R_TIMES V = Y •R_TIMES V) & (V /= R_0)) •imp (X = Y)
(780) Theorem 630: [Reals are closed under division] ((X in Re) & (Y in Re) & (Y /= R_0)) •imp ((X •R_OVER Y in Re) & ((X /= R_0) •imp ((X •R_OVER Y /= R_0) & (X •R_TIMES Y /= R_0))))
(781) Theorem 631: [Real division is multiplication by the reciprocal] ((X in Re) & (Y in Re) & (Y /= R_0)) •imp ((X •R_OVER Y) = (X •R_TIMES R_Recip(Y)))
(782) Theorem 632: [The reciprocal of a real product is the product of the reciprocals] ((X in Re) & (Y in Re) & (X /= R_0) & (Y /= R_0)) •imp ((X •R_TIMES Y /= R_0) & R_Recip(X •R_TIMES Y) = R_Recip(X) •R_TIMES R_Recip(Y))
(783) Theorem 633: [Real multiplication-division commutativity] ((X in Re) & (Y in Re) & (Y /= R_0) & (V in Re) & (V /= R_0)) •imp (X •R_OVER (Y •R_TIMES V) = (X •R_OVER Y) •R_OVER V)
(787) Theorem 637: [Real division reverses multiplication] ((X in Re) & (Y in Re) & (Y /= R_0)) •imp ((X •R_TIMES Y) •R_OVER Y = X)
(788) Theorem 638: [Real division reverses multiplication,2] ((X in Re) & (Y in Re) & (Y /= R_0)) •imp (X = (Y •R_TIMES (X •R_OVER Y)))
(796) Theorem 646: [The sum and product of two non-negative reals is non-negative] ((X in Re) & (Y in Re) & R_is_nonneg(X) & R_is_nonneg(Y)) •imp (R_is_nonneg(X •R_PLUS Y) & R_is_nonneg(X •R_TIMES Y))
(823) Theorem 672: [The product of two reals is 0 if and only if one of them is 0] ((X in Re) & (Y in Re)) •imp (((X •R_TIMES Y) = R_0) •eq ((X = R_0) or (Y = R_0)))
(824) Theorem 673: [Monotonicity of multiplication over 2nd argument] ((X in Re) & (XP in Re) & (YP in Re) & (X •R_GE R_0) & (XP •R_GE YP)) •imp ((X •R_TIMES XP) •R_GE (X •R_TIMES YP))
(825) Theorem 674: [Monotonicity of multiplication] ((X in Re) & (Y in Re) & (XP in Re) & (YP in Re) & (X •R_GE Y) & (Y •R_GE R_0) & (YP •R_GE R_0) & (XP •R_GE YP)) •imp ((X •R_TIMES XP) •R_GE (Y •R_TIMES YP))
(826) Theorem 675: [Strict monotonicity of multiplication over 2nd argument] ((X in Re) & (XP in Re) & (YP in Re) & (X •R_GT R_0) & (XP •R_GT YP)) •imp ((X •R_TIMES XP) •R_GT (X •R_TIMES YP))
(827) Theorem 676: [Strict monotonicity of multiplication] ((X in Re) & (Y in Re) & (XP in Re) & (YP in Re) & (X •R_GE Y) & (Y •R_GT R_0) & (YP •R_GT R_0) & (XP •R_GT YP)) •imp ((X •R_TIMES XP) •R_GT (Y •R_TIMES YP))
(828) Theorem 677: [Multiplication by a positive real is strictly monotone] ((X in Re) & (Y in Re) & (Z in Re) & (X •R_GT Y) & (Z •R_GT R_0)) •imp ((X •R_TIMES Z) •R_GT (Y •R_TIMES Z))
(829) Theorem 678: [The product of reals x,y of which x is positive is non-negative iff y is non-negative] ((X in Re) & (Y in Re) & (X /= R_0) & R_is_nonneg(X)) •imp (R_is_nonneg(X •R_TIMES Y) •eq R_is_nonneg(Y))
(830) Theorem 679: [The product of nonnegative reals is non-negative] ((X in Re) & (Y in Re) & R_is_nonneg(X) & R_is_nonneg(Y)) •imp R_is_nonneg(X •R_TIMES Y)
(831) Theorem 680: [Condition for positiveness of a product of reals] ((X in Re) & (Y in Re)) •imp (((X •R_TIMES Y) •R_GT R_0) •eq (((X •R_GT R_0) & (Y •R_GT R_0)) or ((R_0 •R_GT X) & (R_0 •R_GT Y))))
(836) Theorem 684: [The square of any real is non-negative] (X in Re) •imp R_is_nonneg(X •R_TIMES X)
(837) Theorem 684a: [Monotonicity of squaring] ((X in Re) & (Y in Re) & (X •R_GE R_0) & (Y •R_GE R_0)) •imp ((X •R_GE Y) •eq ((X •R_TIMES X) •R_GE (Y •R_TIMES Y)))
(848) Theorem 695: [The absolute value of a real product is the product of absolute values] ((X in Re) & (Y in Re)) •imp (abs(X •R_TIMES Y) = (abs(X) •R_TIMES abs(Y)))
(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)))
(874) Theorem 721: [Elementary properties of the real absolute value] ((X in Re) & (Y in Re)) •imp ((abs(X) in Re) & (abs(Y) in Re) & (abs(X •R_TIMES Y) = (abs(X) •R_TIMES abs(Y))) & ((abs(X) •R_PLUS abs(Y)) •R_GE abs(X •R_PLUS Y) & (abs(R_Rev(X)) = abs(X))))
(881) Theorem 726: [The limit of a product is the product of limits] ((F in ReCauchy) & (G in ReCauchy)) •imp (limit(F •Res_TIMES G) = limit(F) •R_TIMES limit(G))
(888) Theorem 733: [For any real x and eps > 0, there exists an integer n such that n • eps > x] ((x in Re) & (eps in Re) & (eps •R_GT R_0)) •imp (EXISTS n in Za | ((ReRa(RaSi(SiZa(n))) •R_TIMES e) •R_GT x))
(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))))
(902) Theorem 747: ((F in Fin_Seqs(Re)) & (G in Fin_Seqs(Re)) & (X in Re)) •imp (((Polval(F,X) •R_PLUS Polval(G,X)) = Polval(F •PolPlus G,X)) & ((Polval(F,X) •R_MINUS Polval(G,X)) = Polval(F •PolMinus G,X)) & ((Polval(F,X) •R_TIMES Polval(G,X)) = Polval(F •PolTimes G,X)))
(915) Theorem 760: [The square of the square root of any positive x is x] ((X in Re) & (R_is_nonneg(X))) •imp ((sqrt(X) in Re) & (R_is_nonneg(sqrt(X))) & ((sqrt(X) •R_TIMES sqrt(X)) = X))
(916) Theorem 761: [The positive square root is unique] ((X in Re) & (Y in Re) & R_is_nonneg(X) & R_is_nonneg(Y) & ((Y •R_TIMES Y) = X)) •imp (Y = sqrt(X))
(918) Theorem 763: [The square root of a product is the product of the square roots] ((X in Re) & (Y in Re) & R_is_nonneg(X) & R_is_nonneg(Y)) •imp (sqrt(X •R_TIMES Y) = (sqrt(X) •R_TIMES sqrt(Y)))
(919) Theorem 763a: [The square of the square root of any real w=(x •R_TIMES x) •R_PLUS (y •R_TIMES y) is w] ((X in Re) & (Y in Re)) •imp (sqrt((X •R_TIMES X) •R_PLUS (Y •R_TIMES Y)) •R_TIMES sqrt((X •R_TIMES X) •R_PLUS (Y •R_TIMES Y)) = ((X •R_TIMES X) •R_PLUS (Y •R_TIMES Y)))
(923) Theorem 20004: ((X in Re) & (Y in Re) & (X1 in Re) & (X •R_GT Y) & (X1 •R_GT R_0)) •imp ((X •R_TIMES X1) •R_GT (Y •R_TIMES X1))
(939) Theorem 816: ((N in Cm) & (M in Cm)) •imp (C_abs(N) •R_TIMES C_abs(M) = C_abs(N •C_TIMES M))