List of theorems referencing the symbol RECIP
(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)
(619) Theorem 472: ((X in Ra) & (X •Ra_GT Ra_0)) •imp (Recip(X) •Ra_GT Ra_0)
(634) Theorem 487: ((X in Ra) & (X /= Ra_0)) •imp ((Recip(X) /= Ra_0) & Recip(Recip(X)) = X)
(646) Theorem 499: [The rational reciprocal is monotone decreasing for positive rationals] ((X in Ra) & (Y in Ra) & (X •Ra_GT Y) & (Y •Ra_GT Ra_0)) •imp (Recip(Y) •Ra_GT Recip(X))
(648) Theorem 501: [Properties of the rational number 2] ((Ra_1 •Ra_PLUS Ra_1) in Ra) & ((Ra_1 •Ra_PLUS Ra_1) •Ra_GT Ra_0) & (Recip(Ra_1 •Ra_PLUS Ra_1) in Ra) & ((X in Ra) •imp ((X •Ra_OVER (Ra_1 •Ra_PLUS Ra_1)) in Ra))
(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)))
(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)))
(664) Theorem 517: [The absolute value of the reciprocal equals the reciprocal of the absolute value] ((X in Ra) & (X /= Ra_0)) •imp (Ra_ABS(Recip(X)) = Recip(Ra_ABS(X)))
(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))))
(700) Theorem 549: ((F in RaCauchy) & (not Ra_eqseq(F,Ra0Seq))) •imp (EXISTS g in RaCauchy | Ra_eqseq(F,g) & (Ras_Recip(F) = Ras_Recip(g)) & (FORALL i in Za | ((g~[i]) /= Ra_0) & (Ras_Recip(g)~[i] = Recip(g~[i]))))
(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)))