List of theorems referencing the symbol SAME_FRAC
(549+) Theorem 401: [Equivalence of fractions is reflexive and symmetric] (FORALL x in Fr,y in Fr | (Same_frac(x,y) •eq Same_frac(y,x)) & Same_frac(x,x))
(550) Theorem 402: [Equivalence of fractions is transitive] (FORALL x in Fr, y in Fr, wz in Fr | (Same_frac(x,y) & Same_frac(y,wz)) •imp Same_frac(x,wz))
(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)))
(567) Theorem 417: [Fractions are equivalent if their cross-products are equal] ((X in Fr) & (Y in Fr) & Same_frac(X,Y) & (W in Fr) & (Z in Fr) & Same_frac(W,Z)) •imp Same_frac([(car(X) •S_TIMES cdr(W)) •S_PLUS (car(W) •S_TIMES cdr(X)),cdr(X) •S_TIMES cdr(W)], [(car(Y) •S_TIMES cdr(Z)) •S_PLUS (car(Z) •S_TIMES cdr(Y)),cdr(Y) •S_TIMES cdr(Z)])
(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)]))
(568+) Theorem 419: [If two pairs of fractions are equivalent, their formal products are also equivalent] ((X in Fr) & (Y in Fr) & Same_frac(X,Y) & (W in Fr) & (Z in Fr) & Same_frac(W,Z)) •imp Same_frac([car(X) •S_TIMES car(W),cdr(X) •S_TIMES cdr(W)],[car(Y) •S_TIMES car(Z),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)]))
(572) Theorem 423: [Reversing both the numerator and denominator of a formal fraction does not change the rational it represents] (X in Fr) •imp Same_frac(X,[S_Rev(car(X)),S_Rev(cdr(X))])
(573) Theorem 424: [?] ((X in Fr) & (Y in Fr) & Same_frac(X,Y) & is_nonneg(cdr(X)) & is_nonneg(cdr(Y))) •imp ((is_nonneg(car(X)) or car(X) = [0,0]) •eq (is_nonneg(car(Y)) or car(Y) = [0,0]))
(574) Theorem 425: [The sign of the product of the numerator and denominator of a fraction defines the sign of the rational number which it represents] ((X in Fr) & (Y in Fr) & Same_frac(X,Y)) •imp (is_nonneg(car(X) •S_TIMES cdr(X)) •eq is_nonneg(car(Y) •S_TIMES cdr(Y)))
(576) Theorem 427: [?] ((X in Fr) & (Y in Fr) & Same_frac(X,Y)) •imp (Fr_is_nonneg(X) •eq Fr_is_nonneg(Y))
(612) Theorem 464: [Reversing the numerators of two equivalent rational fractions leaves them equivalent] ((X in Si) & (Y in Si) & (XP in Si) & (YP in Si) & Same_frac([X,Y],[XP,YP])) •imp Same_frac([S_Rev(X),Y],[S_Rev(XP),YP])