List of theorems referencing the symbol RA_1
(582) Theorem 434: [The zero rational is the identity for rational addition] (Ra_0 in Ra) & (Ra_1 in Ra) & ((M in Ra) •imp (M = M •Ra_PLUS Ra_0))
(592) Theorem 444: [The unit rational is the rational multiplicative identity] (M in Ra) •imp (M = M •Ra_TIMES Ra_1)
(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))
(596) Theorem 448: [0 and 1 have non-negative rationals] Ra_is_nonneg(Ra_0) & Ra_is_nonneg(Ra_1)
(606) Theorem 458: [The unit rational is the identity for multiplication] (X in Ra) •imp (X = X •Ra_TIMES Ra_1)
(610) Theorem 462: [Properties of the rational zero and unit] (Ra_Rev(Ra_0) = Ra_0) & (Ra_1 /= Ra_0) & (Ra_1 •Ra_GT Ra_0)
(615) Theorem 467: [The reverse of a rational X is the reverse of 1, times X] (X in Ra) •imp (Ra_Rev(X) = (Ra_Rev(Ra_1) •Ra_TIMES X))
(647) Theorem 500: [The average of two rational numbers lies between them] ((X in Ra) & (Y in Ra) & (X •Ra_GT Y)) •imp ((X •Ra_GT ((X •Ra_PLUS Y) •Ra_OVER (Ra_1 •Ra_PLUS Ra_1))) & (((X •Ra_PLUS Y) •Ra_OVER (Ra_1 •Ra_PLUS Ra_1)) •Ra_GT Y))
(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))
(649) Theorem 502: [Any rational number can be divided into two equal halves] (X in Ra) •imp (X = ((X •Ra_OVER (Ra_1 •Ra_PLUS Ra_1)) •Ra_PLUS (X •Ra_OVER (Ra_1 •Ra_PLUS Ra_1))))
(680) Theorem 529: (U in Za) •imp (((Ra0Seq~[U]) = Ra_0) & ((Ra1Seq~[U]) = Ra_1))
(861) Theorem 708: [The embedding of rationals into reals preserves 0 and 1] (ReRa(Ra_0) = R_0) & (ReRa(Ra_1) = R_1)
(868+) Theorem 715: [The embedding of signed integers into rationals preserves 0 and 1] RaSi([0,0]) = Ra_0 & RaSi([1,0]) = Ra_1