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