List of theorems referencing the symbol R_RECIP
(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))
(777) Theorem 627: [Basic properties of the reciprocal for reals, 2] ((X in Re) & (X /= R_0)) •imp (R_Recip(R_Recip(X)) = X)
(778) Theorem 628: [Reverse of real reciprocal] ((X in Re) & (X /= R_0)) •imp (R_Recip(R_Rev(X)) = R_Rev(R_Recip(X)))
(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))
(785) Theorem 635: [Real reciprocal as a quotient] ((X in Re) & (X /= R_0)) •imp (R_Recip(X) = R_1 •R_OVER X)
(817) Theorem 667: [Properties of the real zero and unit] (R_Rev(R_0) = R_0) & (R_1 /= R_0) & (R_1 •R_GT R_0) & (R_Recip(R_1) = R_1)
(832) Theorem 681: [The reciprocal of a positive real is positive] ((X in Re) & (X •R_GT R_0)) •imp (R_Recip(X) •R_GT R_0)
(834) Theorem 683: [The reciprocal is monotone decreasing for positive reals] ((X in Re) & (Y in Re) & (X •R_GT Y) & (Y •R_GT R_0)) •imp (R_Recip(Y) •R_GT R_Recip(X))
(835) Theorem 683a: [Two non-null reals are equal iff their reciprocals are equal] ((X in Re) & (X /= R_0) & (Y in Re) & (Y /= R_0) & (R_Recip(X) = R_Recip(Y))) •imp (X = Y)
(838) Theorem 685: [Properties of the real number 2] ((R_1 •R_PLUS R_1) in Re) & ((R_1 •R_PLUS R_1) •R_GT R_0) & (R_Recip(R_1 •R_PLUS R_1) in Re) & (R_Recip(R_1 •R_PLUS R_1) /= R_0) & ((X in Re) •imp ((X •R_OVER (R_1 •R_PLUS R_1)) in Re))
(862) Theorem 709: [The embedding of rationals into reals preserves quotients by nonzero quantities] ((X in Ra) & (Y in Ra) & (Y /= Ra_0)) •imp ((R_Recip(ReRa(Y)) = ReRa(Recip(Y))) & ((ReRa(X) •R_OVER ReRa(Y)) = ReRa(X •Ra_OVER Y)))