Filtering...

integerp

books/arithmetic-3/bind-free/integerp

Included Books

top building-blocks default-hint
other
(in-package "ACL2")
local
(local (include-book "../pass1/top"))
include-book
(include-book "building-blocks")
include-book
(include-book "default-hint")
other
(set-default-hints '((nonlinearp-default-hint stable-under-simplificationp
     hist
     pspv)))
other
(table acl2-defaults-table :state-ok t)
not-integerp-1aencapsulate
(encapsulate nil
  (set-non-linearp t)
  (local (defthm not-integerp-helper
      (implies (and (rationalp a) (rationalp x) (< 0 a) (< a x))
        (and (< 0 (* (/ x) a)) (< (* (/ x) a) 1)))
      :rule-classes nil))
  (defthm not-integerp-1a
    (implies (and (rationalp a) (rationalp x) (< 0 a) (< a x))
      (not (integerp (* (/ x) a))))
    :hints (("Goal" :use not-integerp-helper))
    :rule-classes :type-prescription))
not-integerp-1btheorem
(defthm not-integerp-1b
  (implies (and (rationalp a) (rationalp x) (< 0 a) (< a x))
    (not (integerp (* a (/ x)))))
  :hints (("Goal" :use not-integerp-1a))
  :rule-classes :type-prescription)
not-integerp-1ctheorem
(defthm not-integerp-1c
  (implies (and (rationalp a)
      (rationalp b)
      (rationalp x)
      (< 0 (* a b))
      (< (* a b) x))
    (not (integerp (* (/ x) a b))))
  :rule-classes :type-prescription)
not-integerp-1dtheorem
(defthm not-integerp-1d
  (implies (and (rationalp a)
      (rationalp b)
      (rationalp x)
      (< 0 (* a b))
      (< (* a b) x))
    (not (integerp (* a (/ x) b))))
  :hints (("Goal" :use not-integerp-1c))
  :rule-classes :type-prescription)
not-integerp-1etheorem
(defthm not-integerp-1e
  (implies (and (rationalp a)
      (rationalp b)
      (rationalp x)
      (< 0 (* a b))
      (< (* a b) x))
    (not (integerp (* a b (/ x)))))
  :hints (("Goal" :use not-integerp-1c))
  :rule-classes :type-prescription)
not-integerp-1ftheorem
(defthm not-integerp-1f
  (implies (and (rationalp a)
      (rationalp x)
      (rationalp y)
      (< 0 a)
      (< a (* x y)))
    (not (integerp (* (/ x) (/ y) a))))
  :hints (("Goal" :use (:instance not-integerp-1a (a a) (x (* x y)))))
  :rule-classes :type-prescription)
not-integerp-1gtheorem
(defthm not-integerp-1g
  (implies (and (rationalp a)
      (rationalp x)
      (rationalp y)
      (< 0 a)
      (< a (* x y)))
    (not (integerp (* (/ x) a (/ y)))))
  :hints (("Goal" :use not-integerp-1f))
  :rule-classes :type-prescription)
not-integerp-1htheorem
(defthm not-integerp-1h
  (implies (and (rationalp a)
      (rationalp x)
      (rationalp y)
      (< 0 a)
      (< a (* x y)))
    (not (integerp (* a (/ x) (/ y)))))
  :hints (("Goal" :use not-integerp-1f))
  :rule-classes :type-prescription)
not-integerp-1itheorem
(defthm not-integerp-1i
  (implies (and (rationalp a)
      (rationalp b)
      (rationalp c)
      (rationalp x)
      (< 0 (* a b c))
      (< (* a b c) x))
    (not (integerp (* (/ x) a b c))))
  :rule-classes :type-prescription)
not-integerp-1jtheorem
(defthm not-integerp-1j
  (implies (and (rationalp a)
      (rationalp b)
      (rationalp c)
      (rationalp x)
      (< 0 (* a b c))
      (< (* a b c) x))
    (not (integerp (* a (/ x) b c))))
  :rule-classes :type-prescription)
not-integerp-1ktheorem
(defthm not-integerp-1k
  (implies (and (rationalp a)
      (rationalp b)
      (rationalp c)
      (rationalp x)
      (< 0 (* a b c))
      (< (* a b c) x))
    (not (integerp (* a b (/ x) c))))
  :hints (("Goal" :use not-integerp-1i))
  :rule-classes :type-prescription)
not-integerp-1ltheorem
(defthm not-integerp-1l
  (implies (and (rationalp a)
      (rationalp b)
      (rationalp c)
      (rationalp x)
      (< 0 (* a b c))
      (< (* a b c) x))
    (not (integerp (* a b c (/ x)))))
  :hints (("Goal" :use not-integerp-1i))
  :rule-classes :type-prescription)
not-integerp-1mtheorem
(defthm not-integerp-1m
  (implies (and (rationalp a)
      (rationalp b)
      (rationalp x)
      (rationalp y)
      (< 0 (* a b))
      (< (* a b) (* x y)))
    (not (integerp (* (/ x) (/ y) a b))))
  :rule-classes :type-prescription)
not-integerp-1ntheorem
(defthm not-integerp-1n
  (implies (and (rationalp a)
      (rationalp b)
      (rationalp x)
      (rationalp y)
      (< 0 (* a b))
      (< (* a b) (* x y)))
    (not (integerp (* (/ x) a (/ y) b))))
  :hints (("Goal" :use not-integerp-1m))
  :rule-classes :type-prescription)
not-integerp-1otheorem
(defthm not-integerp-1o
  (implies (and (rationalp a)
      (rationalp b)
      (rationalp x)
      (rationalp y)
      (< 0 (* a b))
      (< (* a b) (* x y)))
    (not (integerp (* (/ x) a b (/ y)))))
  :hints (("Goal" :use not-integerp-1m))
  :rule-classes :type-prescription)
not-integerp-1ptheorem
(defthm not-integerp-1p
  (implies (and (rationalp a)
      (rationalp b)
      (rationalp x)
      (rationalp y)
      (< 0 (* a b))
      (< (* a b) (* x y)))
    (not (integerp (* a (/ x) (/ y) b))))
  :hints (("Goal" :use not-integerp-1m))
  :rule-classes :type-prescription)
not-integerp-1qtheorem
(defthm not-integerp-1q
  (implies (and (rationalp a)
      (rationalp b)
      (rationalp x)
      (rationalp y)
      (< 0 (* a b))
      (< (* a b) (* x y)))
    (not (integerp (* a (/ x) b (/ y)))))
  :hints (("Goal" :use not-integerp-1m))
  :rule-classes :type-prescription)
not-integerp-1rtheorem
(defthm not-integerp-1r
  (implies (and (rationalp a)
      (rationalp b)
      (rationalp x)
      (rationalp y)
      (< 0 (* a b))
      (< (* a b) (* x y)))
    (not (integerp (* a b (/ x) (/ y)))))
  :hints (("Goal" :use not-integerp-1m))
  :rule-classes :type-prescription)
not-integerp-1stheorem
(defthm not-integerp-1s
  (implies (and (rationalp a)
      (rationalp x)
      (rationalp y)
      (rationalp z)
      (< 0 a)
      (< a (* x y z)))
    (not (integerp (* (/ x) (/ y) (/ z) a))))
  :hints (("Goal" :use (:instance not-integerp-1a (a a) (x (* x y z)))))
  :rule-classes :type-prescription)
not-integerp-1ttheorem
(defthm not-integerp-1t
  (implies (and (rationalp a)
      (rationalp x)
      (rationalp y)
      (rationalp z)
      (< 0 a)
      (< a (* x y z)))
    (not (integerp (* (/ x) (/ y) a (/ z)))))
  :hints (("Goal" :use not-integerp-1s))
  :rule-classes :type-prescription)
not-integerp-1utheorem
(defthm not-integerp-1u
  (implies (and (rationalp a)
      (rationalp x)
      (rationalp y)
      (rationalp z)
      (< 0 a)
      (< a (* x y z)))
    (not (integerp (* (/ x) a (/ y) (/ z)))))
  :hints (("Goal" :use not-integerp-1s))
  :rule-classes :type-prescription)
not-integerp-1vtheorem
(defthm not-integerp-1v
  (implies (and (rationalp a)
      (rationalp x)
      (rationalp y)
      (rationalp z)
      (< 0 a)
      (< a (* x y z)))
    (not (integerp (* a (/ x) (/ y) (/ z)))))
  :hints (("Goal" :use not-integerp-1s))
  :rule-classes :type-prescription)
not-integerp-2atheorem
(defthm not-integerp-2a
  (implies (and (rationalp a) (rationalp x) (< a 0) (< x a))
    (not (integerp (* (/ x) a))))
  :hints (("Goal" :use (:instance not-integerp-1a (a (- a)) (x (- x)))))
  :rule-classes :type-prescription)
not-integerp-2btheorem
(defthm not-integerp-2b
  (implies (and (rationalp a) (rationalp x) (< a 0) (< x a))
    (not (integerp (* a (/ x)))))
  :hints (("Goal" :use not-integerp-2a))
  :rule-classes :type-prescription)
not-integerp-2ctheorem
(defthm not-integerp-2c
  (implies (and (rationalp a)
      (rationalp b)
      (rationalp x)
      (< (* a b) 0)
      (< x (* a b)))
    (not (integerp (* (/ x) a b))))
  :rule-classes :type-prescription)
not-integerp-2dtheorem
(defthm not-integerp-2d
  (implies (and (rationalp a)
      (rationalp b)
      (rationalp x)
      (< (* a b) 0)
      (< x (* a b)))
    (not (integerp (* a (/ x) b))))
  :hints (("Goal" :use not-integerp-2c))
  :rule-classes :type-prescription)
not-integerp-2etheorem
(defthm not-integerp-2e
  (implies (and (rationalp a)
      (rationalp b)
      (rationalp x)
      (< (* a b) 0)
      (< x (* a b)))
    (not (integerp (* a b (/ x)))))
  :hints (("Goal" :use not-integerp-2c))
  :rule-classes :type-prescription)
not-integerp-2ftheorem
(defthm not-integerp-2f
  (implies (and (rationalp a)
      (rationalp x)
      (rationalp y)
      (< a 0)
      (< (* x y) a))
    (not (integerp (* (/ x) (/ y) a))))
  :hints (("Goal" :use (:instance not-integerp-2a (a a) (x (* x y)))))
  :rule-classes :type-prescription)
not-integerp-2gtheorem
(defthm not-integerp-2g
  (implies (and (rationalp a)
      (rationalp x)
      (rationalp y)
      (< a 0)
      (< (* x y) a))
    (not (integerp (* (/ x) a (/ y)))))
  :hints (("Goal" :use not-integerp-2f))
  :rule-classes :type-prescription)
not-integerp-2htheorem
(defthm not-integerp-2h
  (implies (and (rationalp a)
      (rationalp x)
      (rationalp y)
      (< a 0)
      (< (* x y) a))
    (not (integerp (* a (/ x) (/ y)))))
  :hints (("Goal" :use not-integerp-2f))
  :rule-classes :type-prescription)
not-integerp-2itheorem
(defthm not-integerp-2i
  (implies (and (rationalp a)
      (rationalp b)
      (rationalp c)
      (rationalp x)
      (< (* a b c) 0)
      (< x (* a b c)))
    (not (integerp (* (/ x) a b c))))
  :rule-classes :type-prescription)
not-integerp-2jtheorem
(defthm not-integerp-2j
  (implies (and (rationalp a)
      (rationalp b)
      (rationalp c)
      (rationalp x)
      (< (* a b c) 0)
      (< x (* a b c)))
    (not (integerp (* a (/ x) b c))))
  :rule-classes :type-prescription)
not-integerp-2ktheorem
(defthm not-integerp-2k
  (implies (and (rationalp a)
      (rationalp b)
      (rationalp c)
      (rationalp x)
      (< (* a b c) 0)
      (< x (* a b c)))
    (not (integerp (* a b (/ x) c))))
  :hints (("Goal" :use (:instance not-integerp-2a (a (* a b c)) (x x))))
  :rule-classes :type-prescription)
not-integerp-2ltheorem
(defthm not-integerp-2l
  (implies (and (rationalp a)
      (rationalp b)
      (rationalp c)
      (rationalp x)
      (< (* a b c) 0)
      (< x (* a b c)))
    (not (integerp (* a b c (/ x)))))
  :hints (("Goal" :use not-integerp-2k))
  :rule-classes :type-prescription)
not-integerp-2mtheorem
(defthm not-integerp-2m
  (implies (and (rationalp a)
      (rationalp b)
      (rationalp x)
      (rationalp y)
      (< (* a b) 0)
      (< (* x y) (* a b)))
    (not (integerp (* (/ x) (/ y) a b))))
  :rule-classes :type-prescription)
not-integerp-2ntheorem
(defthm not-integerp-2n
  (implies (and (rationalp a)
      (rationalp b)
      (rationalp x)
      (rationalp y)
      (< (* a b) 0)
      (< (* x y) (* a b)))
    (not (integerp (* (/ x) a (/ y) b))))
  :hints (("Goal" :use (:instance not-integerp-2a (a (* a b)) (x (* x y)))))
  :rule-classes :type-prescription)
not-integerp-2otheorem
(defthm not-integerp-2o
  (implies (and (rationalp a)
      (rationalp b)
      (rationalp x)
      (rationalp y)
      (< (* a b) 0)
      (< (* x y) (* a b)))
    (not (integerp (* (/ x) a b (/ y)))))
  :hints (("Goal" :use not-integerp-2n))
  :rule-classes :type-prescription)
not-integerp-2ptheorem
(defthm not-integerp-2p
  (implies (and (rationalp a)
      (rationalp b)
      (rationalp x)
      (rationalp y)
      (< (* a b) 0)
      (< (* x y) (* a b)))
    (not (integerp (* a (/ x) (/ y) b))))
  :hints (("Goal" :use not-integerp-2n))
  :rule-classes :type-prescription)
not-integerp-2qtheorem
(defthm not-integerp-2q
  (implies (and (rationalp a)
      (rationalp b)
      (rationalp x)
      (rationalp y)
      (< (* a b) 0)
      (< (* x y) (* a b)))
    (not (integerp (* a (/ x) b (/ y)))))
  :hints (("Goal" :use not-integerp-2n))
  :rule-classes :type-prescription)
not-integerp-2rtheorem
(defthm not-integerp-2r
  (implies (and (rationalp a)
      (rationalp b)
      (rationalp x)
      (rationalp y)
      (< (* a b) 0)
      (< (* x y) (* a b)))
    (not (integerp (* a b (/ x) (/ y)))))
  :hints (("Goal" :use not-integerp-2n))
  :rule-classes :type-prescription)
not-integerp-2stheorem
(defthm not-integerp-2s
  (implies (and (rationalp a)
      (rationalp x)
      (rationalp y)
      (rationalp z)
      (< a 0)
      (< (* x y z) a))
    (not (integerp (* (/ x) (/ y) (/ z) a))))
  :hints (("Goal" :use (:instance not-integerp-2a (a a) (x (* x y z)))))
  :rule-classes :type-prescription)
not-integerp-2ttheorem
(defthm not-integerp-2t
  (implies (and (rationalp a)
      (rationalp x)
      (rationalp y)
      (rationalp z)
      (< a 0)
      (< (* x y z) a))
    (not (integerp (* (/ x) (/ y) a (/ z)))))
  :hints (("Goal" :use not-integerp-2s))
  :rule-classes :type-prescription)
not-integerp-2utheorem
(defthm not-integerp-2u
  (implies (and (rationalp a)
      (rationalp x)
      (rationalp y)
      (rationalp z)
      (< a 0)
      (< (* x y z) a))
    (not (integerp (* (/ x) a (/ y) (/ z)))))
  :hints (("Goal" :use not-integerp-2s))
  :rule-classes :type-prescription)
not-integerp-2vtheorem
(defthm not-integerp-2v
  (implies (and (rationalp a)
      (rationalp x)
      (rationalp y)
      (rationalp z)
      (< a 0)
      (< (* x y z) a))
    (not (integerp (* a (/ x) (/ y) (/ z)))))
  :hints (("Goal" :use not-integerp-2s))
  :rule-classes :type-prescription)
not-integerp-3atheorem
(defthm not-integerp-3a
  (implies (and (rationalp a) (rationalp x) (< 0 a) (< x (- a)))
    (not (integerp (* (/ x) a))))
  :hints (("Goal" :use (:instance not-integerp-1a (a a) (x (- x)))))
  :rule-classes :type-prescription)
not-integerp-3btheorem
(defthm not-integerp-3b
  (implies (and (rationalp a) (rationalp x) (< 0 a) (< x (- a)))
    (not (integerp (* a (/ x)))))
  :hints (("Goal" :use not-integerp-3a))
  :rule-classes :type-prescription)
not-integerp-3ctheorem
(defthm not-integerp-3c
  (implies (and (rationalp a)
      (rationalp b)
      (rationalp x)
      (< 0 (* a b))
      (< x (- (* a b))))
    (not (integerp (* (/ x) a b))))
  :rule-classes :type-prescription)
not-integerp-3dtheorem
(defthm not-integerp-3d
  (implies (and (rationalp a)
      (rationalp b)
      (rationalp x)
      (< 0 (* a b))
      (< x (- (* a b))))
    (not (integerp (* a (/ x) b))))
  :hints (("Goal" :use not-integerp-3c))
  :rule-classes :type-prescription)
not-integerp-3etheorem
(defthm not-integerp-3e
  (implies (and (rationalp a)
      (rationalp b)
      (rationalp x)
      (< 0 (* a b))
      (< x (- (* a b))))
    (not (integerp (* a b (/ x)))))
  :hints (("Goal" :use not-integerp-3d))
  :rule-classes :type-prescription)
not-integerp-3ftheorem
(defthm not-integerp-3f
  (implies (and (rationalp a)
      (rationalp x)
      (rationalp y)
      (< 0 a)
      (< (* x y) (- a)))
    (not (integerp (* (/ x) (/ y) a))))
  :hints (("Goal" :use (:instance not-integerp-3a (a a) (x (* x y)))))
  :rule-classes :type-prescription)
not-integerp-3gtheorem
(defthm not-integerp-3g
  (implies (and (rationalp a)
      (rationalp x)
      (rationalp y)
      (< 0 a)
      (< (* x y) (- a)))
    (not (integerp (* (/ x) a (/ y)))))
  :hints (("Goal" :use not-integerp-3f))
  :rule-classes :type-prescription)
not-integerp-3htheorem
(defthm not-integerp-3h
  (implies (and (rationalp a)
      (rationalp x)
      (rationalp y)
      (< 0 a)
      (< (* x y) (- a)))
    (not (integerp (* a (/ x) (/ y)))))
  :hints (("Goal" :use not-integerp-3f))
  :rule-classes :type-prescription)
not-integerp-3itheorem
(defthm not-integerp-3i
  (implies (and (rationalp a)
      (rationalp b)
      (rationalp c)
      (rationalp x)
      (< 0 (* a b c))
      (< x (- (* a b c))))
    (not (integerp (* (/ x) a b c))))
  :rule-classes :type-prescription)
not-integerp-3jtheorem
(defthm not-integerp-3j
  (implies (and (rationalp a)
      (rationalp b)
      (rationalp c)
      (rationalp x)
      (< 0 (* a b c))
      (< x (- (* a b c))))
    (not (integerp (* a (/ x) b c))))
  :rule-classes :type-prescription)
not-integerp-3ktheorem
(defthm not-integerp-3k
  (implies (and (rationalp a)
      (rationalp b)
      (rationalp c)
      (rationalp x)
      (< 0 (* a b c))
      (< x (- (* a b c))))
    (not (integerp (* a b (/ x) c))))
  :hints (("Goal" :use (:instance not-integerp-3a (a (* a b c)) (x x))))
  :rule-classes :type-prescription)
not-integerp-3ltheorem
(defthm not-integerp-3l
  (implies (and (rationalp a)
      (rationalp b)
      (rationalp c)
      (rationalp x)
      (< 0 (* a b c))
      (< x (- (* a b c))))
    (not (integerp (* a b c (/ x)))))
  :hints (("Goal" :use not-integerp-3k))
  :rule-classes :type-prescription)
not-integerp-3mtheorem
(defthm not-integerp-3m
  (implies (and (rationalp a)
      (rationalp b)
      (rationalp x)
      (rationalp y)
      (< 0 (* a b))
      (< (* x y) (- (* a b))))
    (not (integerp (* (/ x) (/ y) a b))))
  :rule-classes :type-prescription)
not-integerp-3ntheorem
(defthm not-integerp-3n
  (implies (and (rationalp a)
      (rationalp b)
      (rationalp x)
      (rationalp y)
      (< 0 (* a b))
      (< (* x y) (- (* a b))))
    (not (integerp (* (/ x) a (/ y) b))))
  :hints (("Goal" :use (:instance not-integerp-3a (a (* a b)) (x (* x y)))))
  :rule-classes :type-prescription)
not-integerp-3otheorem
(defthm not-integerp-3o
  (implies (and (rationalp a)
      (rationalp b)
      (rationalp x)
      (rationalp y)
      (< 0 (* a b))
      (< (* x y) (- (* a b))))
    (not (integerp (* (/ x) a b (/ y)))))
  :hints (("Goal" :use not-integerp-3n))
  :rule-classes :type-prescription)
not-integerp-3ptheorem
(defthm not-integerp-3p
  (implies (and (rationalp a)
      (rationalp b)
      (rationalp x)
      (rationalp y)
      (< 0 (* a b))
      (< (* x y) (- (* a b))))
    (not (integerp (* a (/ x) (/ y) b))))
  :hints (("Goal" :use not-integerp-3n))
  :rule-classes :type-prescription)
not-integerp-3qtheorem
(defthm not-integerp-3q
  (implies (and (rationalp a)
      (rationalp b)
      (rationalp x)
      (rationalp y)
      (< 0 (* a b))
      (< (* x y) (- (* a b))))
    (not (integerp (* a (/ x) b (/ y)))))
  :hints (("Goal" :use not-integerp-3n))
  :rule-classes :type-prescription)
not-integerp-3rtheorem
(defthm not-integerp-3r
  (implies (and (rationalp a)
      (rationalp b)
      (rationalp x)
      (rationalp y)
      (< 0 (* a b))
      (< (* x y) (- (* a b))))
    (not (integerp (* a b (/ x) (/ y)))))
  :hints (("Goal" :use not-integerp-3n))
  :rule-classes :type-prescription)
not-integerp-3stheorem
(defthm not-integerp-3s
  (implies (and (rationalp a)
      (rationalp x)
      (rationalp y)
      (rationalp z)
      (< 0 a)
      (< (* x y z) (- a)))
    (not (integerp (* (/ x) (/ y) (/ z) a))))
  :hints (("Goal" :use (:instance not-integerp-3a (a a) (x (* x y z)))))
  :rule-classes :type-prescription)
not-integerp-3ttheorem
(defthm not-integerp-3t
  (implies (and (rationalp a)
      (rationalp x)
      (rationalp y)
      (rationalp z)
      (< 0 a)
      (< (* x y z) (- a)))
    (not (integerp (* (/ x) (/ y) a (/ z)))))
  :hints (("Goal" :use not-integerp-3s))
  :rule-classes :type-prescription)
not-integerp-3utheorem
(defthm not-integerp-3u
  (implies (and (rationalp a)
      (rationalp x)
      (rationalp y)
      (rationalp z)
      (< 0 a)
      (< (* x y z) (- a)))
    (not (integerp (* (/ x) a (/ y) (/ z)))))
  :hints (("Goal" :use not-integerp-3s))
  :rule-classes :type-prescription)
not-integerp-3vtheorem
(defthm not-integerp-3v
  (implies (and (rationalp a)
      (rationalp x)
      (rationalp y)
      (rationalp z)
      (< 0 a)
      (< (* x y z) (- a)))
    (not (integerp (* a (/ x) (/ y) (/ z)))))
  :hints (("Goal" :use not-integerp-3s))
  :rule-classes :type-prescription)
not-integerp-4atheorem
(defthm not-integerp-4a
  (implies (and (rationalp a) (rationalp x) (< a 0) (< (- a) x))
    (not (integerp (* (/ x) a))))
  :hints (("Goal" :use (:instance not-integerp-1a (a (- a)) (x x))))
  :rule-classes :type-prescription)
not-integerp-4btheorem
(defthm not-integerp-4b
  (implies (and (rationalp a) (rationalp x) (< a 0) (< (- a) x))
    (not (integerp (* a (/ x)))))
  :hints (("Goal" :use not-integerp-4a))
  :rule-classes :type-prescription)
not-integerp-4ctheorem
(defthm not-integerp-4c
  (implies (and (rationalp a)
      (rationalp b)
      (rationalp x)
      (< (* a b) 0)
      (< (- (* a b)) x))
    (not (integerp (* (/ x) a b))))
  :rule-classes :type-prescription)
not-integerp-4dtheorem
(defthm not-integerp-4d
  (implies (and (rationalp a)
      (rationalp b)
      (rationalp x)
      (< (* a b) 0)
      (< (- (* a b)) x))
    (not (integerp (* a (/ x) b))))
  :hints (("Goal" :use not-integerp-4c))
  :rule-classes :type-prescription)
not-integerp-4etheorem
(defthm not-integerp-4e
  (implies (and (rationalp a)
      (rationalp b)
      (rationalp x)
      (< (* a b) 0)
      (< (- (* a b)) x))
    (not (integerp (* a b (/ x)))))
  :hints (("Goal" :use not-integerp-4c))
  :rule-classes :type-prescription)
not-integerp-4ftheorem
(defthm not-integerp-4f
  (implies (and (rationalp a)
      (rationalp x)
      (rationalp y)
      (< a 0)
      (< (- a) (* x y)))
    (not (integerp (* (/ x) (/ y) a))))
  :hints (("Goal" :use (:instance not-integerp-4a (a a) (x (* x y)))))
  :rule-classes :type-prescription)
not-integerp-4gtheorem
(defthm not-integerp-4g
  (implies (and (rationalp a)
      (rationalp x)
      (rationalp y)
      (< a 0)
      (< (- a) (* x y)))
    (not (integerp (* (/ x) a (/ y)))))
  :hints (("Goal" :use not-integerp-4f))
  :rule-classes :type-prescription)
not-integerp-4htheorem
(defthm not-integerp-4h
  (implies (and (rationalp a)
      (rationalp x)
      (rationalp y)
      (< a 0)
      (< (- a) (* x y)))
    (not (integerp (* a (/ x) (/ y)))))
  :hints (("Goal" :use not-integerp-4f))
  :rule-classes :type-prescription)
not-integerp-4itheorem
(defthm not-integerp-4i
  (implies (and (rationalp a)
      (rationalp b)
      (rationalp c)
      (rationalp x)
      (< (* a b c) 0)
      (< (- (* a b c)) x))
    (not (integerp (* (/ x) a b c))))
  :rule-classes :type-prescription)
not-integerp-4jtheorem
(defthm not-integerp-4j
  (implies (and (rationalp a)
      (rationalp b)
      (rationalp c)
      (rationalp x)
      (< (* a b c) 0)
      (< (- (* a b c)) x))
    (not (integerp (* a (/ x) b c))))
  :rule-classes :type-prescription)
not-integerp-4ktheorem
(defthm not-integerp-4k
  (implies (and (rationalp a)
      (rationalp b)
      (rationalp c)
      (rationalp x)
      (< (* a b c) 0)
      (< (- (* a b c)) x))
    (not (integerp (* a b (/ x) c))))
  :hints (("Goal" :use not-integerp-4i))
  :rule-classes :type-prescription)
not-integerp-4ltheorem
(defthm not-integerp-4l
  (implies (and (rationalp a)
      (rationalp b)
      (rationalp c)
      (rationalp x)
      (< (* a b c) 0)
      (< (- (* a b c)) x))
    (not (integerp (* a b c (/ x)))))
  :hints (("Goal" :use not-integerp-4i))
  :rule-classes :type-prescription)
not-integerp-4mtheorem
(defthm not-integerp-4m
  (implies (and (rationalp a)
      (rationalp b)
      (rationalp x)
      (rationalp y)
      (< (* a b) 0)
      (< (- (* a b)) (* x y)))
    (not (integerp (* (/ x) (/ y) a b))))
  :rule-classes :type-prescription)
not-integerp-4ntheorem
(defthm not-integerp-4n
  (implies (and (rationalp a)
      (rationalp b)
      (rationalp x)
      (rationalp y)
      (< (* a b) 0)
      (< (- (* a b)) (* x y)))
    (not (integerp (* (/ x) a (/ y) b))))
  :hints (("Goal" :use not-integerp-4m))
  :rule-classes :type-prescription)
not-integerp-4otheorem
(defthm not-integerp-4o
  (implies (and (rationalp a)
      (rationalp b)
      (rationalp x)
      (rationalp y)
      (< (* a b) 0)
      (< (- (* a b)) (* x y)))
    (not (integerp (* (/ x) a b (/ y)))))
  :hints (("Goal" :use not-integerp-4m))
  :rule-classes :type-prescription)
not-integerp-4ptheorem
(defthm not-integerp-4p
  (implies (and (rationalp a)
      (rationalp b)
      (rationalp x)
      (rationalp y)
      (< (* a b) 0)
      (< (- (* a b)) (* x y)))
    (not (integerp (* a (/ x) (/ y) b))))
  :hints (("Goal" :use not-integerp-4m))
  :rule-classes :type-prescription)
not-integerp-4qtheorem
(defthm not-integerp-4q
  (implies (and (rationalp a)
      (rationalp b)
      (rationalp x)
      (rationalp y)
      (< (* a b) 0)
      (< (- (* a b)) (* x y)))
    (not (integerp (* a (/ x) b (/ y)))))
  :hints (("Goal" :use (:instance not-integerp-4a (a (* a b)) (x (* x y)))))
  :rule-classes :type-prescription)
not-integerp-4rtheorem
(defthm not-integerp-4r
  (implies (and (rationalp a)
      (rationalp b)
      (rationalp x)
      (rationalp y)
      (< (* a b) 0)
      (< (- (* a b)) (* x y)))
    (not (integerp (* a b (/ x) (/ y)))))
  :hints (("Goal" :use not-integerp-4q))
  :rule-classes :type-prescription)
not-integerp-4stheorem
(defthm not-integerp-4s
  (implies (and (rationalp a)
      (rationalp x)
      (rationalp y)
      (rationalp z)
      (< a 0)
      (< (- a) (* x y z)))
    (not (integerp (* (/ x) (/ y) (/ z) a))))
  :hints (("Goal" :use (:instance not-integerp-4a (a a) (x (* x y z)))))
  :rule-classes :type-prescription)
not-integerp-4ttheorem
(defthm not-integerp-4t
  (implies (and (rationalp a)
      (rationalp x)
      (rationalp y)
      (rationalp z)
      (< a 0)
      (< (- a) (* x y z)))
    (not (integerp (* (/ x) (/ y) a (/ z)))))
  :hints (("Goal" :use not-integerp-4s))
  :rule-classes :type-prescription)
not-integerp-4utheorem
(defthm not-integerp-4u
  (implies (and (rationalp a)
      (rationalp x)
      (rationalp y)
      (rationalp z)
      (< a 0)
      (< (- a) (* x y z)))
    (not (integerp (* (/ x) a (/ y) (/ z)))))
  :hints (("Goal" :use not-integerp-4s))
  :rule-classes :type-prescription)
not-integerp-4vtheorem
(defthm not-integerp-4v
  (implies (and (rationalp a)
      (rationalp x)
      (rationalp y)
      (rationalp z)
      (< a 0)
      (< (- a) (* x y z)))
    (not (integerp (* a (/ x) (/ y) (/ z)))))
  :hints (("Goal" :use not-integerp-4s))
  :rule-classes :type-prescription)
reduce-integerp-+-fn-1function
(defun reduce-integerp-+-fn-1
  (x mfc state)
  (declare (xargs :guard (and (pseudo-termp x) (eq (fn-symb x) 'binary-+))))
  (cond ((and (not (equal (fargn x 1) ''0))
       (proveably-integer (fargn x 1) mfc state)) (list (cons 'z (fargn x 1))))
    ((eq (fn-symb (fargn x 2)) 'binary-+) (reduce-integerp-+-fn-1 (fargn x 2) mfc state))
    ((and (not (equal (fargn x 2) ''0))
       (proveably-integer (fargn x 2) mfc state)) (list (cons 'z (fargn x 2))))
    (t nil)))
reduce-integerp-+-fnfunction
(defun reduce-integerp-+-fn
  (x mfc state)
  (declare (xargs :guard (pseudo-termp x)))
  (if (eq (fn-symb x) 'binary-+)
    (reduce-integerp-+-fn-1 x mfc state)
    nil))
local
(local (defthm iff-integerp
    (equal (equal (integerp x) (integerp y))
      (iff (integerp x) (integerp y)))))
reduce-integerp-+theorem
(defthm reduce-integerp-+
  (implies (and (syntaxp (rewriting-goal-literal x mfc state))
      (bind-free (reduce-integerp-+-fn x mfc state) (z))
      (equal y (- x z))
      (integerp z)
      (acl2-numberp x))
    (equal (integerp x) (integerp y))))
integerp-minus-xtheorem
(defthm integerp-minus-x
  (implies (and (syntaxp (weak-negative-addends-p x)) (acl2-numberp x))
    (equal (integerp x) (integerp (- x)))))
find-integerp-hyp-1function
(defun find-integerp-hyp-1
  (type-alist c x)
  (cond ((endp type-alist) nil)
    ((let ((typed-term (caar type-alist)) (type (cadar type-alist)))
       (and (eq (fn-symb typed-term) 'binary-*)
         (quotep (fargn typed-term 1))
         (equal (fargn typed-term 2) x)
         (ts-subsetp type *ts-integer*)
         (integerp (/ (unquote c) (unquote (fargn typed-term 1)))))) (list (cons 'd (fargn (caar type-alist) 1))
        (cons 'a
          (kwote (/ (unquote c) (unquote (fargn (caar type-alist) 1)))))))
    (t (find-integerp-hyp-1 (cdr type-alist) c x))))
find-integerp-hypfunction
(defun find-integerp-hyp
  (c x mfc state)
  (declare (ignore state))
  (find-integerp-hyp-1 c x (mfc-type-alist mfc)))
|(integerp (* c x))|theorem
(defthm |(integerp (* c x))|
  (implies (and (bind-free (find-integerp-hyp c x mfc state) (d a))
      (equal (* d a) c)
      (integerp (* d x))
      (integerp a))
    (integerp (* c x))))
nintergerp-extratheorem
(defthm nintergerp-extra
  (implies (and (rationalp x)
      (< 0 x)
      (rationalp y)
      (< 0 y)
      (integerp i)
      (< 0 i)
      (< x (expt y i)))
    (not (integerp (* x (expt (/ y) i))))))
integerp-+-reduce-leading-rational-constanttheorem
(defthm integerp-+-reduce-leading-rational-constant
  (implies (and (syntaxp (rational-constant-p c))
      (syntaxp (or (<= 1 (unquote c)) (< (unquote c) 0))))
    (equal (integerp (+ c x))
      (integerp (+ (+ c (- (floor c 1))) x))))
  :hints (("Goal" :in-theory (disable floor))))
even-and-odd-alternateencapsulate
(encapsulate nil
  (local (defun induct-nat
      (x)
      (if (and (integerp x) (> x 0))
        (induct-nat (1- x))
        nil)))
  (local (defthm x-or-x/2-4
      (implies (and (integerp x) (>= x 0))
        (or (integerp (/ x 2)) (integerp (/ (1+ x) 2))))
      :rule-classes nil
      :hints (("Goal" :induct (induct-nat x)))))
  (local (defthm x-or-x/2-5
      (implies (integerp x) (integerp (- x)))
      :rule-classes nil))
  (local (defthm x-or-x/2-11
      (implies (and (integerp x) (<= x 0))
        (or (integerp (/ x 2)) (integerp (/ (1+ x) 2))))
      :rule-classes nil
      :hints (("Goal" :in-theory (disable functional-self-inversion-of-minus)
         :use ((:instance x-or-x/2-4 (x (- x))) (:instance x-or-x/2-5 (x (* -1/2 x))))) ("Subgoal 1" :in-theory (enable functional-self-inversion-of-minus)))))
  (local (defthm x-or-x/2
      (implies (integerp x)
        (or (integerp (/ x 2)) (integerp (/ (1+ x) 2))))
      :rule-classes nil
      :hints (("Goal" :in-theory (disable functional-self-inversion-of-minus)
         :use ((:instance x-or-x/2-4) (:instance x-or-x/2-11))))))
  (defthm even-and-odd-alternate
    (implies (rationalp x)
      (equal (integerp (+ 1/2 x))
        (and (integerp (* 2 x)) (not (integerp x)))))
    :hints (("Subgoal 3'" :use ((:instance (:theorem (implies (and (integerp x) (integerp y)) (integerp (* x y))))
          (x (+ 1/2 x))
          (y 2)))) ("Subgoal 2'" :use ((:instance x-or-x/2 (x (* 2 x))))))))