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

Rules for reducing inequalities between products, canceling like factors, and comparing products against 0.

Definitions and Theorems

Theorem: <-*-right-cancel

(defthm <-*-right-cancel
        (implies (and (fc (real/rationalp x))
                      (fc (real/rationalp y))
                      (fc (real/rationalp z)))
                 (equal (< (* x z) (* y z))
                        (cond ((< 0 z) (< x y))
                              ((equal z 0) nil)
                              (t (< y x))))))

Theorem: <-*-left-cancel

(defthm <-*-left-cancel
        (implies (and (fc (real/rationalp x))
                      (fc (real/rationalp y))
                      (fc (real/rationalp z)))
                 (equal (< (* z x) (* z y))
                        (cond ((< 0 z) (< x y))
                              ((equal z 0) nil)
                              (t (< y x))))))

Theorem: <-*-0

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

Theorem: 0-<-*

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

Theorem: <-*-x-y-y

(defthm <-*-x-y-y
        (implies (and (fc (real/rationalp x))
                      (fc (real/rationalp y)))
                 (equal (< (* x y) y)
                        (cond ((equal y 0) nil)
                              ((< 0 y) (< x 1))
                              (t (< 1 x))))))

Theorem: <-*-y-x-y

(defthm <-*-y-x-y
        (implies (and (fc (real/rationalp x))
                      (fc (real/rationalp y)))
                 (equal (< (* y x) y)
                        (cond ((equal y 0) nil)
                              ((< 0 y) (< x 1))
                              (t (< 1 x))))))

Theorem: <-y-*-x-y

(defthm <-y-*-x-y
        (implies (and (fc (real/rationalp x))
                      (fc (real/rationalp y)))
                 (equal (< y (* x y))
                        (cond ((equal y 0) nil)
                              ((< 0 y) (< 1 x))
                              (t (< x 1))))))

Theorem: <-y-*-y-x

(defthm <-y-*-y-x
        (implies (and (fc (real/rationalp x))
                      (fc (real/rationalp y)))
                 (equal (< y (* y x))
                        (cond ((equal y 0) nil)
                              ((< 0 y) (< 1 x))
                              (t (< x 1))))))

Theorem: *-preserves->=-for-nonnegatives

(defthm *-preserves->=-for-nonnegatives
        (implies (and (>= x1 x2)
                      (>= y1 y2)
                      (>= x2 0)
                      (>= y2 0)
                      (fc (real/rationalp x1))
                      (fc (real/rationalp x2))
                      (fc (real/rationalp y1))
                      (fc (real/rationalp y2)))
                 (>= (* x1 y1) (* x2 y2))))

Theorem: *-preserves->-for-nonnegatives-1

(defthm *-preserves->-for-nonnegatives-1
        (implies (and (> x1 x2)
                      (>= y1 y2)
                      (>= x2 0)
                      (> y2 0)
                      (fc (real/rationalp x1))
                      (fc (real/rationalp x2))
                      (fc (real/rationalp y1))
                      (fc (real/rationalp y2)))
                 (> (* x1 y1) (* x2 y2))))

Theorem: x*y>1-positive-lemma

(defthm x*y>1-positive-lemma
        (implies (and (> x i)
                      (> y j)
                      (real/rationalp i)
                      (real/rationalp j)
                      (< 0 i)
                      (< 0 j)
                      (fc (real/rationalp x))
                      (fc (real/rationalp y)))
                 (> (* x y) (* i j))))

Theorem: x*y>1-positive

(defthm x*y>1-positive
        (implies (and (> x 1)
                      (> y 1)
                      (fc (real/rationalp x))
                      (fc (real/rationalp y)))
                 (> (* x y) 1))
        :rule-classes (:linear :rewrite))