		Search-engine friendly clone of the ACL2 documentation.

More-rational-identities

Rules about numerator and denominator in the arithmetic/rationals book.

Definitions and Theorems

Theorem: denominator-unary-minus

(defthm denominator-unary-minus
  (implies (rationalp x)
           (equal (denominator (- x))
                  (denominator x))))

Theorem: numerator-goes-down-by-integer-division

(defthm numerator-goes-down-by-integer-division
  (implies (and (integerp x) (< 0 x) (rationalp r))
           (<= (abs (numerator (* (/ x) r)))
               (abs (numerator r))))
  :rule-classes
  ((:linear :corollary (implies (and (integerp x)
                                     (< 0 x)
                                     (rationalp r)
                                     (>= r 0))
                                (<= (numerator (* (/ x) r))
                                    (numerator r))))
   (:linear :corollary (implies (and (integerp x)
                                     (< 0 x)
                                     (rationalp r)
                                     (<= r 0))
                                (<= (numerator r)
                                    (numerator (* (/ x) r)))))))

Theorem: denominator-plus

(defthm denominator-plus
  (implies (and (rationalp r) (integerp i))
           (equal (denominator (+ i r))
                  (denominator r))))

Theorem: numerator-minus

(defthm numerator-minus
  (equal (numerator (- i))
         (- (numerator i))))

Theorem: numerator-/x

(defthm numerator-/x
  (implies (and (integerp x) (not (equal x 0)))
           (equal (numerator (/ x)) (signum x))))