		Search-engine friendly clone of the ACL2 documentation.

Basic-rational-identities

Basic cancellation rules for numerator and denominator terms.

See also more-rational-identities for additional reductions involving numerator and denominator terms.

Definitions and Theorems

Theorem: numerator-when-integerp

(defthm numerator-when-integerp
        (implies (integerp x)
                 (equal (numerator x) x)))

Theorem: integerp==>denominator=1

(defthm integerp==>denominator=1
        (implies (integerp x)
                 (equal (denominator x) 1)))

Theorem: equal-denominator-1

(defthm equal-denominator-1
        (equal (equal (denominator x) 1)
               (or (integerp x) (not (rationalp x)))))

Theorem: *-r-denominator-r

(defthm *-r-denominator-r
        (equal (* r (denominator r))
               (if (rationalp r)
                   (numerator r)
                   (fix r))))

Theorem: /r-when-abs-numerator=1

(defthm /r-when-abs-numerator=1
        (and (implies (equal (numerator r) 1)
                      (equal (/ r) (denominator r)))
             (implies (equal (numerator r) -1)
                      (equal (/ r) (- (denominator r))))))