• Top
  • Documentation
  • Books
  • Boolean-reasoning
  • Projects
  • Debugging
  • Std
  • Proof-automation
  • Macro-libraries
  • ACL2
  • Interfacing-tools
  • Hardware-verification
  • Software-verification
  • Math
    • 100-theorems
    • 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
      • Include-an-arithmetic-book
      • Number-theory
      • Arithmetic-3
      • Arithmetic-2
      • Arithmetic-light
      • Arithmetic-5
    • Bit-vectors
    • Algebra
  • Testing-utilities

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