• Top
  • Documentation
  • Books
  • Recursion-and-induction
  • Boolean-reasoning
  • Projects
  • Debugging
  • Std
  • Proof-automation
  • Macro-libraries
  • ACL2
  • Interfacing-tools
  • Hardware-verification
  • Software-verification
  • Testing-utilities
  • Math
    • Arithmetic
      • Lispfloat
      • Arithmetic-1
        • Inequalities-of-products
        • Basic-product-normalization
        • Inequalities-of-reciprocals
        • Arithmetic/natp-posp
        • Basic-expt-normalization
        • More-rational-identities
        • Inequalities-of-exponents
        • Basic-sum-normalization
        • Basic-rational-identities
        • Basic-expt-type-rules
        • Inequalities-of-sums
        • Basic-products-with-negations
        • Fc
      • Number-theory
      • Proof-by-arith
      • Arith-equivs
      • Number-theory
      • Arithmetic-3
      • Arithmetic-2
      • Arithmetic-light
      • Arithmetic-5
    • Bit-vectors
    • Algebra

• Arithmetic-1
• Numerator
• Denominator

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))))