• 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

Inequalities-of-reciprocals

Basic rules for moving reciprocals across inequalities, comparing reciprocals, and canceling reciprocals by multiplying across an inequality.

Definitions and Theorems

Theorem: /-preserves-positive

(defthm /-preserves-positive
        (implies (fc (real/rationalp x))
                 (equal (< 0 (/ x)) (< 0 x))))

Theorem: /-preserves-negative

(defthm /-preserves-negative
        (implies (fc (real/rationalp x))
                 (equal (< (/ x) 0) (< x 0))))

Theorem: /-inverts-order-1

(defthm /-inverts-order-1
        (implies (and (< 0 x)
                      (< x y)
                      (fc (real/rationalp x))
                      (fc (real/rationalp y)))
                 (< (/ y) (/ x))))

Theorem: /-inverts-order-2

(defthm /-inverts-order-2
        (implies (and (< y 0)
                      (< x y)
                      (fc (real/rationalp x))
                      (fc (real/rationalp y)))
                 (< (/ y) (/ x))))

Theorem: /-inverts-weak-order

(defthm /-inverts-weak-order
        (implies (and (< 0 x)
                      (<= x y)
                      (fc (real/rationalp x))
                      (fc (real/rationalp y)))
                 (not (< (/ x) (/ y)))))

Theorem: <-unary-/-negative-left

(defthm <-unary-/-negative-left
        (implies (and (< x 0)
                      (fc (real/rationalp x))
                      (fc (real/rationalp y)))
                 (equal (< (/ x) y) (< (* x y) 1))))

Theorem: <-unary-/-negative-right

(defthm <-unary-/-negative-right
        (implies (and (< x 0)
                      (fc (real/rationalp x))
                      (fc (real/rationalp y)))
                 (equal (< y (/ x)) (< 1 (* x y)))))

Theorem: <-unary-/-positive-left

(defthm <-unary-/-positive-left
        (implies (and (< 0 x)
                      (fc (real/rationalp x))
                      (fc (real/rationalp y)))
                 (equal (< (/ x) y) (< 1 (* x y)))))

Theorem: <-unary-/-positive-right

(defthm <-unary-/-positive-right
        (implies (and (< 0 x)
                      (fc (real/rationalp x))
                      (fc (real/rationalp y)))
                 (equal (< y (/ x)) (< (* x y) 1))))

Theorem: <-*-/-right

(defthm <-*-/-right
        (implies (and (< 0 y)
                      (fc (real/rationalp a))
                      (fc (real/rationalp x))
                      (fc (real/rationalp y)))
                 (equal (< a (* x (/ y)))
                        (< (* a y) x))))

Theorem: <-*-/-right-commuted

(defthm <-*-/-right-commuted
        (implies (and (< 0 y)
                      (fc (real/rationalp x))
                      (fc (real/rationalp y))
                      (fc (real/rationalp a)))
                 (equal (< x (* (/ y) a))
                        (< (* x y) a))))

Theorem: <-*-/-left

(defthm <-*-/-left
        (implies (and (< 0 y)
                      (fc (real/rationalp x))
                      (fc (real/rationalp y))
                      (fc (real/rationalp a)))
                 (equal (< (* x (/ y)) a)
                        (< x (* a y)))))

Theorem: <-*-/-left-commuted

(defthm <-*-/-left-commuted
        (implies (and (< 0 y)
                      (fc (real/rationalp x))
                      (fc (real/rationalp y))
                      (fc (real/rationalp a)))
                 (equal (< (* (/ y) x) a)
                        (< x (* y a)))))