List of theorems referencing the symbol FR_TO_RA
(551) Theorem 403: [Fractions are equivalent if and only if the rational numbers they define are equal] (FORALL x, y | ((x in Fr) & (y in Fr)) •imp ((Same_frac(x,y) •eq (Fr_to_Ra(x) = Fr_to_Ra(y))))) & (FORALL x | (x in Ra) •imp ((arb(x) in Fr) & (Fr_to_Ra(arb(x)) = x))) & (FORALL x | (x in Fr) •imp (Fr_to_Ra(x) in Ra)) & (FORALL x | (x in Fr) •imp Same_frac(x,arb(Fr_to_Ra(x))))
(552) Theorem 404: [Every fraction is equivalent to every member of its rational number class] (X in Fr) •imp ((Fr_to_Ra(X) in Ra) & Same_frac(X,arb(Fr_to_Ra(X))))
(553) Theorem 405: [Alternate version of Theorem 403] ((X in Fr) & (Y in Fr)) •imp (Same_frac(X,Y) •eq (Fr_to_Ra(X) = Fr_to_Ra(Y)))
(554) Theorem 406: [Alternate version of Theorem 404] (Y in Ra) •imp ((arb(Y) in Fr) & (Fr_to_Ra(arb(Y)) = Y))
(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)]))
(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]))
(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))
(613) Theorem 465: [Alternate form of Theorem 464] ((X in Si) & (Y in Si) & (Y /= [0,0])) •imp (Ra_Rev(Fr_to_Ra([X,Y])) = Fr_to_Ra([S_Rev(X),Y]))
(635) Theorem 488: ([2,0] in Si) & (is_nonneg([2,0])) & is_nonneg([1,0]) & (Fr_to_Ra([[1,0],[2,0]]) in Ra) & (Fr_to_Ra([[1,0],[2,0]]) •Ra_GT Ra_0)