Included Books
other
(in-package "ACL2")
include-book
(include-book "building-blocks")
local
(local (include-book "default-hint"))
local
(local (include-book "../../support/top"))
local
(local (include-book "integerp-helper"))
local
(local (in-theory (disable default-*-1 default-*-2 default-+-1 default-+-2 default-<-1 default-<-2 default-unary-/ default-unary-minus default-realpart default-numerator default-imagpart default-denominator default-coerce-1 default-coerce-2 default-car default-cdr)))
local
(local (in-theory (disable expt-type-prescription-rationalp expt-type-prescription-nonzero expt-type-prescription-positive-1 expt-type-prescription-positive-2 expt-type-prescription-integerp expt-type-prescription-non-zero-base)))
local
(local (defthm expt-crock (implies (and (real/rationalp x) (integerp n)) (equal (expt x (- n)) (/ (expt x n))))))
not-integerp-1aencapsulate
(encapsulate nil (local (include-book "common")) (local (include-book "normalize")) (local (include-book "simplify")) (local (include-book "collect")) (local (in-theory (disable normalize-factors-scatter-exponents))) (local (defthm not-integerp-helper (implies (and (real/rationalp x) (< 0 a) (< a x)) (and (< 0 (* (/ x) a)) (< (* (/ x) a) 1))) :rule-classes nil)) (defthm not-integerp-1a (implies (and (real/rationalp x) (< 0 a) (< a x)) (not (integerp (* (/ x) a)))) :hints (("Goal" :use not-integerp-helper)) :rule-classes :type-prescription) (defthm not-integerp-1a-expt (implies (and (real/rationalp x) (integerp n) (< 0 a) (< a (expt x n))) (not (integerp (* (expt x (- n)) a)))) :hints (("Goal" :use (:instance not-integerp-helper (x (expt x n))))) :rule-classes :type-prescription))
local
(local (in-theory (disable not-integerp-1a not-integerp-1a-expt)))
not-integerp-1btheorem
(defthm not-integerp-1b (implies (and (real/rationalp x) (< 0 a) (< a x)) (not (integerp (* a (/ x))))) :hints (("Goal" :use not-integerp-1a)) :rule-classes :type-prescription)
not-integerp-1b-expttheorem
(defthm not-integerp-1b-expt (implies (and (real/rationalp x) (integerp n) (< 0 a) (< a (expt x n))) (not (integerp (* a (expt x (- n)))))) :hints (("Goal" :use (:instance not-integerp-1a (x (expt x n))))) :rule-classes :type-prescription)
local
(local (in-theory (disable not-integerp-1b not-integerp-1b-expt)))
not-integerp-1dtheorem
(defthm not-integerp-1d (implies (and (real/rationalp b) (real/rationalp x) (< 0 (* a b)) (< (* a b) x)) (not (integerp (* a (/ x) b)))) :hints (("Goal" :use (:instance not-integerp-1a (a (* a b)) (x x)))) :rule-classes :type-prescription)
not-integerp-1d-expttheorem
(defthm not-integerp-1d-expt (implies (and (real/rationalp b) (real/rationalp x) (integerp n) (< 0 (* a b)) (< (* a b) (expt x n))) (not (integerp (* a (expt x (- n)) b)))) :hints (("Goal" :use (:instance not-integerp-1a (a (* a b)) (x (expt x n))))) :rule-classes :type-prescription)
local
(local (in-theory (disable not-integerp-1d not-integerp-1d-expt)))
not-integerp-1etheorem
(defthm not-integerp-1e (implies (and (real/rationalp x) (< 0 (* a b)) (< (* a b) x)) (not (integerp (* a b (/ x))))) :hints (("Goal" :use (:instance not-integerp-1a (a (* a b)) (x x)))) :rule-classes :type-prescription)
not-integerp-1e-expttheorem
(defthm not-integerp-1e-expt (implies (and (real/rationalp x) (integerp n) (< 0 (* a b)) (< (* a b) (expt x n))) (not (integerp (* a b (expt x (- n)))))) :hints (("Goal" :use (:instance not-integerp-1a (a (* a b)) (x (expt x n))))) :rule-classes :type-prescription)
local
(local (in-theory (disable not-integerp-1e not-integerp-1e-expt)))
not-integerp-1ftheorem
(defthm not-integerp-1f (implies (and (real/rationalp x) (real/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-1f-expt-atheorem
(defthm not-integerp-1f-expt-a (implies (and (real/rationalp x) (integerp n) (real/rationalp y) (< 0 a) (< a (* (expt x n) y))) (not (integerp (* (expt x (- n)) (/ y) a)))) :hints (("Goal" :use (:instance not-integerp-1a (a a) (x (* (expt x n) y))))) :rule-classes :type-prescription)
not-integerp-1f-expt-btheorem
(defthm not-integerp-1f-expt-b (implies (and (real/rationalp x) (real/rationalp y) (integerp n) (< 0 a) (< a (* x (expt y n)))) (not (integerp (* (/ x) (expt y (- n)) a)))) :hints (("Goal" :use (:instance not-integerp-1a (a a) (x (* (expt y n) x))))) :rule-classes :type-prescription)
not-integerp-1f-expt-ctheorem
(defthm not-integerp-1f-expt-c (implies (and (real/rationalp x) (integerp n1) (real/rationalp y) (integerp n2) (< 0 a) (< a (* (expt x n1) (expt y n2)))) (not (integerp (* (expt x (- n1)) (expt y (- n2)) a)))) :hints (("Goal" :use (:instance not-integerp-1a (a a) (x (* (expt x n1) (expt y n2)))))) :rule-classes :type-prescription)
local
(local (in-theory (disable not-integerp-1f not-integerp-1f-expt-a not-integerp-1f-expt-b not-integerp-1f-expt-c)))
not-integerp-1gtheorem
(defthm not-integerp-1g (implies (and (real/rationalp x) (real/rationalp y) (< 0 a) (< a (* x y))) (not (integerp (* (/ x) a (/ y))))) :hints (("Goal" :use not-integerp-1f)) :rule-classes :type-prescription)
not-integerp-1g-expt-atheorem
(defthm not-integerp-1g-expt-a (implies (and (real/rationalp x) (integerp n) (real/rationalp y) (< 0 a) (< a (* (expt x n) y))) (not (integerp (* (expt x (- n)) a (/ y))))) :hints (("Goal" :use (:instance not-integerp-1f (x (expt x n))))) :rule-classes :type-prescription)
not-integerp-1g-expt-btheorem
(defthm not-integerp-1g-expt-b (implies (and (real/rationalp x) (real/rationalp y) (integerp n) (< 0 a) (< a (* x (expt y n)))) (not (integerp (* (/ x) a (expt y (- n)))))) :hints (("Goal" :use (:instance not-integerp-1f (y (expt y n))))) :rule-classes :type-prescription)
not-integerp-1g-expt-ctheorem
(defthm not-integerp-1g-expt-c (implies (and (real/rationalp x) (integerp n1) (real/rationalp y) (integerp n2) (< 0 a) (< a (* (expt x n1) (expt y n2)))) (not (integerp (* (expt x (- n1)) a (expt y (- n2)))))) :hints (("Goal" :use (:instance not-integerp-1f (x (expt x n1)) (y (expt y n2))))) :rule-classes :type-prescription)
local
(local (in-theory (disable not-integerp-1g not-integerp-1g-expt-a not-integerp-1g-expt-b not-integerp-1g-expt-c)))
not-integerp-1htheorem
(defthm not-integerp-1h (implies (and (real/rationalp x) (real/rationalp y) (< 0 a) (< a (* x y))) (not (integerp (* a (/ x) (/ y))))) :hints (("Goal" :use not-integerp-1f)) :rule-classes :type-prescription)
not-integerp-1h-expt-atheorem
(defthm not-integerp-1h-expt-a (implies (and (real/rationalp x) (integerp n) (real/rationalp y) (< 0 a) (< a (* (expt x n) y))) (not (integerp (* a (expt x (- n)) (/ y))))) :hints (("Goal" :use (:instance not-integerp-1f (x (expt x n))))) :rule-classes :type-prescription)
not-integerp-1h-expt-btheorem
(defthm not-integerp-1h-expt-b (implies (and (real/rationalp x) (real/rationalp y) (integerp n) (< 0 a) (< a (* x (expt y n)))) (not (integerp (* a (/ x) (expt y (- n)))))) :hints (("Goal" :use (:instance not-integerp-1f (y (expt y n))))) :rule-classes :type-prescription)
not-integerp-1h-expt-ctheorem
(defthm not-integerp-1h-expt-c (implies (and (real/rationalp x) (integerp n1) (real/rationalp y) (integerp n2) (< 0 a) (< a (* (expt x n1) (expt y n2)))) (not (integerp (* a (expt x (- n1)) (expt y (- n2)))))) :hints (("Goal" :use (:instance not-integerp-1f (x (expt x n1)) (y (expt y n2))))) :rule-classes :type-prescription)
local
(local (in-theory (disable not-integerp-1h not-integerp-1h-expt-a not-integerp-1h-expt-b not-integerp-1h-expt-c)))
not-integerp-1ktheorem
(defthm not-integerp-1k (implies (and (real/rationalp c) (real/rationalp x) (< 0 (* a b c)) (< (* a b c) x)) (not (integerp (* a b (/ x) c)))) :hints (("Goal" :use (:instance not-integerp-1a (a (* a b c)) (x x)))) :rule-classes :type-prescription)
not-integerp-1k-expttheorem
(defthm not-integerp-1k-expt (implies (and (real/rationalp c) (real/rationalp x) (integerp n) (< 0 (* a b c)) (< (* a b c) (expt x n))) (not (integerp (* a b (expt x (- n)) c)))) :hints (("Goal" :use (:instance not-integerp-1a (a (* a b c)) (x (expt x n))))) :rule-classes :type-prescription)
local
(local (in-theory (disable not-integerp-1k not-integerp-1k-expt)))
not-integerp-1ltheorem
(defthm not-integerp-1l (implies (and (real/rationalp x) (< 0 (* a b c)) (< (* a b c) x)) (not (integerp (* a b c (/ x))))) :hints (("Goal" :use (:instance not-integerp-1a (a (* a b c)) (x x)))) :rule-classes :type-prescription)
not-integerp-1l-expttheorem
(defthm not-integerp-1l-expt (implies (and (real/rationalp x) (integerp n) (< 0 (* a b c)) (< (* a b c) (expt x n))) (not (integerp (* a b c (expt x (- n)))))) :hints (("Goal" :use (:instance not-integerp-1a (a (* a b c)) (x (expt x n))))) :rule-classes :type-prescription)
local
(local (in-theory (disable not-integerp-1l not-integerp-1l-expt)))
not-integerp-1ntheorem
(defthm not-integerp-1n (implies (and (real/rationalp x) (real/rationalp y) (< 0 (* a b)) (< (* a b) (* x y))) (not (integerp (* (/ x) a (/ y) b)))) :hints (("Goal" :use (:instance not-integerp-1a (a (* a b)) (x (* x y))))) :rule-classes :type-prescription)
not-integerp-1n-expt-atheorem
(defthm not-integerp-1n-expt-a (implies (and (real/rationalp x) (integerp n) (real/rationalp y) (< 0 (* a b)) (< (* a b) (* (expt x n) y))) (not (integerp (* (expt x (- n)) a (/ y) b)))) :hints (("Goal" :use (:instance not-integerp-1a (a (* a b)) (x (* (expt x n) y))))) :rule-classes :type-prescription)
not-integerp-1n-expt-btheorem
(defthm not-integerp-1n-expt-b (implies (and (real/rationalp x) (real/rationalp y) (integerp n) (< 0 (* a b)) (< (* a b) (* x (expt y n)))) (not (integerp (* (/ x) a (expt y (- n)) b)))) :hints (("Goal" :use (:instance not-integerp-1a (a (* a b)) (x (* x (expt y n)))))) :rule-classes :type-prescription)
not-integerp-1n-expt-ctheorem
(defthm not-integerp-1n-expt-c (implies (and (real/rationalp x) (integerp n1) (real/rationalp y) (integerp n2) (< 0 (* a b)) (< (* a b) (* (expt x n1) (expt y n2)))) (not (integerp (* (expt x (- n1)) a (expt y (- n2)) b)))) :hints (("Goal" :use (:instance not-integerp-1a (a (* a b)) (x (* (expt x n1) (expt y n2)))))) :rule-classes :type-prescription)
local
(local (in-theory (disable not-integerp-1n not-integerp-1n-expt-a not-integerp-1n-expt-b not-integerp-1n-expt-c)))
not-integerp-1otheorem
(defthm not-integerp-1o (implies (and (real/rationalp x) (real/rationalp y) (< 0 (* a b)) (< (* a b) (* x y))) (not (integerp (* (/ x) a b (/ y))))) :hints (("Goal" :use (:instance not-integerp-1a (a (* a b)) (x (* x y))))) :rule-classes :type-prescription)
not-integerp-1o-expt-atheorem
(defthm not-integerp-1o-expt-a (implies (and (real/rationalp x) (integerp n) (real/rationalp y) (< 0 (* a b)) (< (* a b) (* (expt x n) y))) (not (integerp (* (expt x (- n)) a b (/ y))))) :hints (("Goal" :use (:instance not-integerp-1a (a (* a b)) (x (* (expt x n) y))))) :rule-classes :type-prescription)
not-integerp-1o-expt-btheorem
(defthm not-integerp-1o-expt-b (implies (and (real/rationalp x) (real/rationalp y) (integerp n) (< 0 (* a b)) (< (* a b) (* x (expt y n)))) (not (integerp (* (/ x) a b (expt y (- n)))))) :hints (("Goal" :use (:instance not-integerp-1a (a (* a b)) (x (* x (expt y n)))))) :rule-classes :type-prescription)
not-integerp-1o-expt-ctheorem
(defthm not-integerp-1o-expt-c (implies (and (real/rationalp x) (integerp n1) (real/rationalp y) (integerp n2) (< 0 (* a b)) (< (* a b) (* (expt x n1) (expt y n2)))) (not (integerp (* (expt x (- n1)) a b (expt y (- n2)))))) :hints (("Goal" :use (:instance not-integerp-1a (a (* a b)) (x (* (expt x n1) (expt y n2)))))) :rule-classes :type-prescription)
local
(local (in-theory (disable not-integerp-1o not-integerp-1o-expt-a not-integerp-1o-expt-b not-integerp-1o-expt-c)))
not-integerp-1ptheorem
(defthm not-integerp-1p (implies (and (real/rationalp x) (real/rationalp y) (< 0 (* a b)) (< (* a b) (* x y))) (not (integerp (* a (/ x) (/ y) b)))) :hints (("Goal" :use (:instance not-integerp-1a (a (* a b)) (x (* x y))))) :rule-classes :type-prescription)
not-integerp-1p-expt-atheorem
(defthm not-integerp-1p-expt-a (implies (and (real/rationalp x) (integerp n) (real/rationalp y) (< 0 (* a b)) (< (* a b) (* (expt x n) y))) (not (integerp (* a (expt x (- n)) (/ y) b)))) :hints (("Goal" :use (:instance not-integerp-1a (a (* a b)) (x (* (expt x n) y))))) :rule-classes :type-prescription)
not-integerp-1p-expt-btheorem
(defthm not-integerp-1p-expt-b (implies (and (real/rationalp x) (real/rationalp y) (integerp n) (< 0 (* a b)) (< (* a b) (* x (expt y n)))) (not (integerp (* a (/ x) (expt y (- n)) b)))) :hints (("Goal" :use (:instance not-integerp-1a (a (* a b)) (x (* x (expt y n)))))) :rule-classes :type-prescription)
not-integerp-1p-expt-ctheorem
(defthm not-integerp-1p-expt-c (implies (and (real/rationalp x) (integerp n1) (real/rationalp y) (integerp n2) (< 0 (* a b)) (< (* a b) (* (expt x n1) (expt y n2)))) (not (integerp (* a (expt x (- n1)) (expt y (- n2)) b)))) :hints (("Goal" :use (:instance not-integerp-1a (a (* a b)) (x (* (expt x n1) (expt y n2)))))) :rule-classes :type-prescription)
local
(local (in-theory (disable not-integerp-1p not-integerp-1p-expt-a not-integerp-1p-expt-b not-integerp-1p-expt-c)))
not-integerp-1qtheorem
(defthm not-integerp-1q (implies (and (real/rationalp x) (real/rationalp y) (< 0 (* a b)) (< (* a b) (* x y))) (not (integerp (* a (/ x) b (/ y))))) :hints (("Goal" :use (:instance not-integerp-1a (a (* a b)) (x (* x y))))) :rule-classes :type-prescription)
not-integerp-1q-expt-atheorem
(defthm not-integerp-1q-expt-a (implies (and (real/rationalp x) (integerp n) (real/rationalp y) (< 0 (* a b)) (< (* a b) (* (expt x n) y))) (not (integerp (* a (expt x (- n)) b (/ y))))) :hints (("Goal" :use (:instance not-integerp-1a (a (* a b)) (x (* (expt x n) y))))) :rule-classes :type-prescription)
not-integerp-1q-expt-btheorem
(defthm not-integerp-1q-expt-b (implies (and (real/rationalp x) (real/rationalp y) (integerp n) (< 0 (* a b)) (< (* a b) (* x (expt y n)))) (not (integerp (* a (/ x) b (expt y (- n)))))) :hints (("Goal" :use (:instance not-integerp-1a (a (* a b)) (x (* x (expt y n)))))) :rule-classes :type-prescription)
not-integerp-1q-expt-ctheorem
(defthm not-integerp-1q-expt-c (implies (and (real/rationalp x) (integerp n1) (real/rationalp y) (integerp n2) (< 0 (* a b)) (< (* a b) (* (expt x n1) (expt y n2)))) (not (integerp (* a (expt x (- n1)) b (expt y (- n2)))))) :hints (("Goal" :use (:instance not-integerp-1a (a (* a b)) (x (* (expt x n1) (expt y n2)))))) :rule-classes :type-prescription)
local
(local (in-theory (disable not-integerp-1q not-integerp-1q-expt-a not-integerp-1q-expt-b not-integerp-1q-expt-c)))
not-integerp-1rtheorem
(defthm not-integerp-1r (implies (and (real/rationalp x) (real/rationalp y) (< 0 (* a b)) (< (* a b) (* x y))) (not (integerp (* a b (/ x) (/ y))))) :hints (("Goal" :use (:instance not-integerp-1a (a (* a b)) (x (* x y))))) :rule-classes :type-prescription)
not-integerp-1r-expt-atheorem
(defthm not-integerp-1r-expt-a (implies (and (real/rationalp x) (integerp n) (real/rationalp y) (< 0 (* a b)) (< (* a b) (* (expt x n) y))) (not (integerp (* a b (expt x (- n)) (/ y))))) :hints (("Goal" :use (:instance not-integerp-1a (a (* a b)) (x (* (expt x n) y))))) :rule-classes :type-prescription)
not-integerp-1r-expt-btheorem
(defthm not-integerp-1r-expt-b (implies (and (real/rationalp x) (real/rationalp y) (integerp n) (< 0 (* a b)) (< (* a b) (* x (expt y n)))) (not (integerp (* a b (/ x) (expt y (- n)))))) :hints (("Goal" :use (:instance not-integerp-1a (a (* a b)) (x (* x (expt y n)))))) :rule-classes :type-prescription)
not-integerp-1r-expt-ctheorem
(defthm not-integerp-1r-expt-c (implies (and (real/rationalp x) (integerp n1) (real/rationalp y) (integerp n2) (< 0 (* a b)) (< (* a b) (* (expt x n1) (expt y n2)))) (not (integerp (* a b (expt x (- n1)) (expt y (- n2)))))) :hints (("Goal" :use (:instance not-integerp-1a (a (* a b)) (x (* (expt x n1) (expt y n2)))))) :rule-classes :type-prescription)
local
(local (in-theory (disable not-integerp-1r not-integerp-1r-expt-a not-integerp-1r-expt-b not-integerp-1r-expt-c)))
not-integerp-1stheorem
(defthm not-integerp-1s (implies (and (real/rationalp x) (real/rationalp y) (real/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-1s-expt-atheorem
(defthm not-integerp-1s-expt-a (implies (and (real/rationalp x) (integerp n) (real/rationalp y) (real/rationalp z) (< 0 a) (< a (* (expt x n) y z))) (not (integerp (* (expt x (- n)) (/ y) (/ z) a)))) :hints (("Goal" :use (:instance not-integerp-1a (a a) (x (* (expt x n) y z))))) :rule-classes :type-prescription)
not-integerp-1s-expt-btheorem
(defthm not-integerp-1s-expt-b (implies (and (real/rationalp x) (real/rationalp y) (integerp n) (real/rationalp z) (< 0 a) (< a (* x (expt y n) z))) (not (integerp (* (/ x) (expt y (- n)) (/ z) a)))) :hints (("Goal" :use (:instance not-integerp-1a (a a) (x (* x (expt y n) z))))) :rule-classes :type-prescription)
not-integerp-1s-expt-ctheorem
(defthm not-integerp-1s-expt-c (implies (and (real/rationalp x) (real/rationalp y) (real/rationalp z) (integerp n) (< 0 a) (< a (* x y (expt z n)))) (not (integerp (* (/ x) (/ y) (expt z (- n)) a)))) :hints (("Goal" :use (:instance not-integerp-1a (a a) (x (* x y (expt z n)))))) :rule-classes :type-prescription)
not-integerp-1s-expt-dtheorem
(defthm not-integerp-1s-expt-d (implies (and (real/rationalp x) (integerp n1) (real/rationalp y) (integerp n2) (real/rationalp z) (< 0 a) (< a (* (expt x n1) (expt y n2) z))) (not (integerp (* (expt x (- n1)) (expt y (- n2)) (/ z) a)))) :hints (("Goal" :use (:instance not-integerp-1a (a a) (x (* (expt x n1) (expt y n2) z))))) :rule-classes :type-prescription)
not-integerp-1s-expt-etheorem
(defthm not-integerp-1s-expt-e (implies (and (real/rationalp x) (integerp n1) (real/rationalp y) (real/rationalp z) (integerp n2) (< 0 a) (< a (* (expt x n1) y (expt z n2)))) (not (integerp (* (expt x (- n1)) (/ y) (expt z (- n2)) a)))) :hints (("Goal" :use (:instance not-integerp-1a (a a) (x (* (expt x n1) y (expt z n2)))))) :rule-classes :type-prescription)
not-integerp-1s-expt-ftheorem
(defthm not-integerp-1s-expt-f (implies (and (real/rationalp x) (real/rationalp y) (integerp n1) (real/rationalp z) (integerp n2) (< 0 a) (< a (* x (expt y n1) (expt z n2)))) (not (integerp (* (/ x) (expt y (- n1)) (expt z (- n2)) a)))) :hints (("Goal" :use (:instance not-integerp-1a (a a) (x (* x (expt y n1) (expt z n2)))))) :rule-classes :type-prescription)
not-integerp-1s-expt-gtheorem
(defthm not-integerp-1s-expt-g (implies (and (real/rationalp x) (integerp n1) (real/rationalp y) (integerp n2) (real/rationalp z) (integerp n3) (< 0 a) (< a (* (expt x n1) (expt y n2) (expt z n3)))) (not (integerp (* (expt x (- n1)) (expt y (- n2)) (expt z (- n3)) a)))) :hints (("Goal" :use (:instance not-integerp-1a (a a) (x (* (expt x n1) (expt y n2) (expt z n3)))))) :rule-classes :type-prescription)
local
(local (in-theory (disable not-integerp-1s not-integerp-1s-expt-a not-integerp-1s-expt-b not-integerp-1s-expt-c not-integerp-1s-expt-d not-integerp-1s-expt-e not-integerp-1s-expt-f not-integerp-1s-expt-g)))
not-integerp-1ttheorem
(defthm not-integerp-1t (implies (and (real/rationalp x) (real/rationalp y) (real/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-1t-expt-atheorem
(defthm not-integerp-1t-expt-a (implies (and (real/rationalp x) (integerp n) (real/rationalp y) (real/rationalp z) (< 0 a) (< a (* (expt x n) y z))) (not (integerp (* (expt x (- n)) (/ y) a (/ z))))) :hints (("Goal" :use (:instance not-integerp-1s (x (expt x n))))) :rule-classes :type-prescription)
not-integerp-1t-expt-btheorem
(defthm not-integerp-1t-expt-b (implies (and (real/rationalp x) (real/rationalp y) (integerp n) (real/rationalp z) (< 0 a) (< a (* x (expt y n) z))) (not (integerp (* (/ x) (expt y (- n)) a (/ z))))) :hints (("Goal" :use (:instance not-integerp-1s (y (expt y n))))) :rule-classes :type-prescription)
not-integerp-1t-expt-ctheorem
(defthm not-integerp-1t-expt-c (implies (and (real/rationalp x) (real/rationalp y) (real/rationalp z) (integerp n) (< 0 a) (< a (* x y (expt z n)))) (not (integerp (* (/ x) (/ y) a (expt z (- n)))))) :hints (("Goal" :use (:instance not-integerp-1s (z (expt z n))))) :rule-classes :type-prescription)
not-integerp-1t-expt-dtheorem
(defthm not-integerp-1t-expt-d (implies (and (real/rationalp x) (integerp n1) (real/rationalp y) (integerp n2) (real/rationalp z) (< 0 a) (< a (* (expt x n1) (expt y n2) z))) (not (integerp (* (expt x (- n1)) (expt y (- n2)) a (/ z))))) :hints (("Goal" :use (:instance not-integerp-1s (x (expt x n1)) (y (expt y n2))))) :rule-classes :type-prescription)
not-integerp-1t-expt-etheorem
(defthm not-integerp-1t-expt-e (implies (and (real/rationalp x) (integerp n1) (real/rationalp y) (real/rationalp z) (integerp n2) (< 0 a) (< a (* (expt x n1) y (expt z n2)))) (not (integerp (* (expt x (- n1)) (/ y) a (expt z (- n2)))))) :hints (("Goal" :use (:instance not-integerp-1s (x (expt x n1)) (z (expt z n2))))) :rule-classes :type-prescription)
not-integerp-1t-expt-ftheorem
(defthm not-integerp-1t-expt-f (implies (and (real/rationalp x) (real/rationalp y) (integerp n1) (real/rationalp z) (integerp n2) (< 0 a) (< a (* x (expt y n1) (expt z n2)))) (not (integerp (* (/ x) (expt y (- n1)) a (expt z (- n2)))))) :hints (("Goal" :use (:instance not-integerp-1s (y (expt y n1)) (z (expt z n2))))) :rule-classes :type-prescription)
not-integerp-1t-expt-gtheorem
(defthm not-integerp-1t-expt-g (implies (and (real/rationalp x) (integerp n1) (real/rationalp y) (integerp n2) (real/rationalp z) (integerp n3) (< 0 a) (< a (* (expt x n1) (expt y n2) (expt z n3)))) (not (integerp (* (expt x (- n1)) (expt y (- n2)) a (expt z (- n3)))))) :hints (("Goal" :use (:instance not-integerp-1s (x (expt x n1)) (y (expt y n2)) (z (expt z n3))))) :rule-classes :type-prescription)
local
(local (in-theory (disable not-integerp-1s not-integerp-1s-expt-a not-integerp-1s-expt-b not-integerp-1s-expt-c not-integerp-1s-expt-d not-integerp-1s-expt-e not-integerp-1s-expt-f not-integerp-1s-expt-g)))
not-integerp-1utheorem
(defthm not-integerp-1u (implies (and (real/rationalp x) (real/rationalp y) (real/rationalp z) (< 0 a) (< a (* x y z))) (not (integerp (* (/ x) a (/ y) (/ z))))) :hints (("Goal" :use (:instance not-integerp-1s))) :rule-classes :type-prescription)
not-integerp-1u-expt-atheorem
(defthm not-integerp-1u-expt-a (implies (and (real/rationalp x) (integerp n) (real/rationalp y) (real/rationalp z) (< 0 a) (< a (* (expt x n) y z))) (not (integerp (* (expt x (- n)) a (/ y) (/ z))))) :hints (("Goal" :use (:instance not-integerp-1s (x (expt x n))))) :rule-classes :type-prescription)
not-integerp-1u-expt-btheorem
(defthm not-integerp-1u-expt-b (implies (and (real/rationalp x) (real/rationalp y) (integerp n) (real/rationalp z) (< 0 a) (< a (* x (expt y n) z))) (not (integerp (* (/ x) a (expt y (- n)) (/ z))))) :hints (("Goal" :use (:instance not-integerp-1s (y (expt y n))))) :rule-classes :type-prescription)
not-integerp-1u-expt-ctheorem
(defthm not-integerp-1u-expt-c (implies (and (real/rationalp x) (real/rationalp y) (real/rationalp z) (integerp n) (< 0 a) (< a (* x y (expt z n)))) (not (integerp (* (/ x) a (/ y) (expt z (- n)))))) :hints (("Goal" :use (:instance not-integerp-1s (z (expt z n))))) :rule-classes :type-prescription)
not-integerp-1u-expt-dtheorem
(defthm not-integerp-1u-expt-d (implies (and (real/rationalp x) (integerp n1) (real/rationalp y) (integerp n2) (real/rationalp z) (< 0 a) (< a (* (expt x n1) (expt y n2) z))) (not (integerp (* (expt x (- n1)) a (expt y (- n2)) (/ z))))) :hints (("Goal" :use (:instance not-integerp-1s (x (expt x n1)) (y (expt y n2))))) :rule-classes :type-prescription)
not-integerp-1u-expt-etheorem
(defthm not-integerp-1u-expt-e (implies (and (real/rationalp x) (integerp n1) (real/rationalp y) (real/rationalp z) (integerp n2) (< 0 a) (< a (* (expt x n1) y (expt z n2)))) (not (integerp (* (expt x (- n1)) a (/ y) (expt z (- n2)))))) :hints (("Goal" :use (:instance not-integerp-1s (x (expt x n1)) (z (expt z n2))))) :rule-classes :type-prescription)
not-integerp-1u-expt-ftheorem
(defthm not-integerp-1u-expt-f (implies (and (real/rationalp x) (real/rationalp y) (integerp n1) (real/rationalp z) (integerp n2) (< 0 a) (< a (* x (expt y n1) (expt z n2)))) (not (integerp (* (/ x) a (expt y (- n1)) (expt z (- n2)))))) :hints (("Goal" :use (:instance not-integerp-1s (y (expt y n1)) (z (expt z n2))))) :rule-classes :type-prescription)
not-integerp-1u-expt-gtheorem
(defthm not-integerp-1u-expt-g (implies (and (real/rationalp x) (integerp n1) (real/rationalp y) (integerp n2) (real/rationalp z) (integerp n3) (< 0 a) (< a (* (expt x n1) (expt y n2) (expt z n3)))) (not (integerp (* (expt x (- n1)) a (expt y (- n2)) (expt z (- n3)))))) :hints (("Goal" :use (:instance not-integerp-1s (x (expt x n1)) (y (expt y n2)) (z (expt z n3))))) :rule-classes :type-prescription)
local
(local (in-theory (disable not-integerp-1u not-integerp-1u-expt-a not-integerp-1u-expt-b not-integerp-1u-expt-c not-integerp-1u-expt-d not-integerp-1u-expt-e not-integerp-1u-expt-f not-integerp-1u-expt-g)))
not-integerp-1vtheorem
(defthm not-integerp-1v (implies (and (real/rationalp x) (real/rationalp y) (real/rationalp z) (< 0 a) (< a (* x y z))) (not (integerp (* a (/ x) (/ y) (/ z))))) :hints (("Goal" :use (:instance not-integerp-1s))) :rule-classes :type-prescription)
not-integerp-1v-expt-atheorem
(defthm not-integerp-1v-expt-a (implies (and (real/rationalp x) (integerp n) (real/rationalp y) (real/rationalp z) (< 0 a) (< a (* (expt x n) y z))) (not (integerp (* a (expt x (- n)) (/ y) (/ z))))) :hints (("Goal" :use (:instance not-integerp-1s (x (expt x n))))) :rule-classes :type-prescription)
not-integerp-1v-expt-btheorem
(defthm not-integerp-1v-expt-b (implies (and (real/rationalp x) (real/rationalp y) (integerp n) (real/rationalp z) (< 0 a) (< a (* x (expt y n) z))) (not (integerp (* a (/ x) (expt y (- n)) (/ z))))) :hints (("Goal" :use (:instance not-integerp-1s (y (expt y n))))) :rule-classes :type-prescription)
not-integerp-1v-expt-ctheorem
(defthm not-integerp-1v-expt-c (implies (and (real/rationalp x) (real/rationalp y) (real/rationalp z) (integerp n) (< 0 a) (< a (* x y (expt z n)))) (not (integerp (* a (/ x) (/ y) (expt z (- n)))))) :hints (("Goal" :use (:instance not-integerp-1s (z (expt z n))))) :rule-classes :type-prescription)
not-integerp-1v-expt-dtheorem
(defthm not-integerp-1v-expt-d (implies (and (real/rationalp x) (integerp n1) (real/rationalp y) (integerp n2) (real/rationalp z) (< 0 a) (< a (* (expt x n1) (expt y n2) z))) (not (integerp (* a (expt x (- n1)) (expt y (- n2)) (/ z))))) :hints (("Goal" :use (:instance not-integerp-1s (x (expt x n1)) (y (expt y n2))))) :rule-classes :type-prescription)
not-integerp-1v-expt-etheorem
(defthm not-integerp-1v-expt-e (implies (and (real/rationalp x) (integerp n1) (real/rationalp y) (real/rationalp z) (integerp n2) (< 0 a) (< a (* (expt x n1) y (expt z n2)))) (not (integerp (* a (expt x (- n1)) (/ y) (expt z (- n2)))))) :hints (("Goal" :use (:instance not-integerp-1s (x (expt x n1)) (z (expt z n2))))) :rule-classes :type-prescription)
not-integerp-1v-expt-ftheorem
(defthm not-integerp-1v-expt-f (implies (and (real/rationalp x) (real/rationalp y) (integerp n1) (real/rationalp z) (integerp n2) (< 0 a) (< a (* x (expt y n1) (expt z n2)))) (not (integerp (* a (/ x) (expt y (- n1)) (expt z (- n2)))))) :hints (("Goal" :use (:instance not-integerp-1s (y (expt y n1)) (z (expt z n2))))) :rule-classes :type-prescription)
not-integerp-1v-expt-gtheorem
(defthm not-integerp-1v-expt-g (implies (and (real/rationalp x) (integerp n1) (real/rationalp y) (integerp n2) (real/rationalp z) (integerp n3) (< 0 a) (< a (* (expt x n1) (expt y n2) (expt z n3)))) (not (integerp (* a (expt x (- n1)) (expt y (- n2)) (expt z (- n3)))))) :hints (("Goal" :use (:instance not-integerp-1s (x (expt x n1)) (y (expt y n2)) (z (expt z n3))))) :rule-classes :type-prescription)
local
(local (in-theory (disable not-integerp-1v not-integerp-1v-expt-a not-integerp-1v-expt-b not-integerp-1v-expt-c not-integerp-1v-expt-d not-integerp-1v-expt-e not-integerp-1v-expt-f not-integerp-1v-expt-g)))
not-integerp-2atheorem
(defthm not-integerp-2a (implies (and (real/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-2a-expttheorem
(defthm not-integerp-2a-expt (implies (and (real/rationalp x) (integerp n) (< a 0) (< (expt x n) a)) (not (integerp (* (expt x (- n)) a)))) :hints (("Goal" :use (:instance not-integerp-2a (x (expt x n))))) :rule-classes :type-prescription)
local
(local (in-theory (disable not-integerp-2a not-integerp-2a-expt)))
not-integerp-2btheorem
(defthm not-integerp-2b (implies (and (real/rationalp x) (< a 0) (< x a)) (not (integerp (* a (/ x))))) :hints (("Goal" :use not-integerp-2a)) :rule-classes :type-prescription)
not-integerp-2b-expttheorem
(defthm not-integerp-2b-expt (implies (and (real/rationalp x) (integerp n) (< a 0) (< (expt x n) a)) (not (integerp (* a (expt x (- n)))))) :hints (("Goal" :use (:instance not-integerp-2a (x (expt x n))))) :rule-classes :type-prescription)
local
(local (in-theory (disable not-integerp-2b not-integerp-2b-expt)))
not-integerp-2dtheorem
(defthm not-integerp-2d (implies (and (real/rationalp b) (real/rationalp x) (< (* a b) 0) (< x (* a b))) (not (integerp (* a (/ x) b)))) :hints (("Goal" :use (:instance not-integerp-2a (a (* a b)) (x x)))) :rule-classes :type-prescription)
not-integerp-2d-expttheorem
(defthm not-integerp-2d-expt (implies (and (real/rationalp b) (real/rationalp x) (integerp n) (< (* a b) 0) (< (expt x n) (* a b))) (not (integerp (* a (expt x (- n)) b)))) :hints (("Goal" :use (:instance not-integerp-2a (a (* a b)) (x (expt x n))))) :rule-classes :type-prescription)
local
(local (in-theory (disable not-integerp-2d not-integerp-2d-expt)))
not-integerp-2etheorem
(defthm not-integerp-2e (implies (and (real/rationalp x) (< (* a b) 0) (< x (* a b))) (not (integerp (* a b (/ x))))) :hints (("Goal" :use (:instance not-integerp-2a (a (* a b)) (x x)))) :rule-classes :type-prescription)
not-integerp-2e-expttheorem
(defthm not-integerp-2e-expt (implies (and (real/rationalp x) (integerp n) (< (* a b) 0) (< (expt x n) (* a b))) (not (integerp (* a b (expt x (- n)))))) :hints (("Goal" :use (:instance not-integerp-2a (a (* a b)) (x (expt x n))))) :rule-classes :type-prescription)
local
(local (in-theory (disable not-integerp-2e not-integerp-2e-expt)))
not-integerp-2ftheorem
(defthm not-integerp-2f (implies (and (real/rationalp x) (real/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-2f-expt-atheorem
(defthm not-integerp-2f-expt-a (implies (and (real/rationalp x) (integerp n) (real/rationalp y) (< a 0) (< (* (expt x n) y) a)) (not (integerp (* (expt x (- n)) (/ y) a)))) :hints (("Goal" :use (:instance not-integerp-2a (a a) (x (* (expt x n) y))))) :rule-classes :type-prescription)
not-integerp-2f-expt-btheorem
(defthm not-integerp-2f-expt-b (implies (and (real/rationalp x) (real/rationalp y) (integerp n) (< a 0) (< (* x (expt y n)) a)) (not (integerp (* (/ x) (expt y (- n)) a)))) :hints (("Goal" :use (:instance not-integerp-2a (a a) (x (* (expt y n) x))))) :rule-classes :type-prescription)
not-integerp-2f-expt-ctheorem
(defthm not-integerp-2f-expt-c (implies (and (real/rationalp x) (integerp n1) (real/rationalp y) (integerp n2) (< a 0) (< (* (expt x n1) (expt y n2)) a)) (not (integerp (* (expt x (- n1)) (expt y (- n2)) a)))) :hints (("Goal" :use (:instance not-integerp-2a (a a) (x (* (expt x n1) (expt y n2)))))) :rule-classes :type-prescription)
local
(local (in-theory (disable not-integerp-2f not-integerp-2f-expt-a not-integerp-2f-expt-b not-integerp-2f-expt-c)))
not-integerp-2gtheorem
(defthm not-integerp-2g (implies (and (real/rationalp x) (real/rationalp y) (< a 0) (< (* x y) a)) (not (integerp (* (/ x) a (/ y))))) :hints (("Goal" :use not-integerp-2f)) :rule-classes :type-prescription)
not-integerp-2g-expt-atheorem
(defthm not-integerp-2g-expt-a (implies (and (real/rationalp x) (integerp n) (real/rationalp y) (< a 0) (< (* (expt x n) y) a)) (not (integerp (* (expt x (- n)) a (/ y))))) :hints (("Goal" :use (:instance not-integerp-2f (x (expt x n))))) :rule-classes :type-prescription)
not-integerp-2g-expt-btheorem
(defthm not-integerp-2g-expt-b (implies (and (real/rationalp x) (real/rationalp y) (integerp n) (< a 0) (< (* x (expt y n)) a)) (not (integerp (* (/ x) a (expt y (- n)))))) :hints (("Goal" :use (:instance not-integerp-2f (y (expt y n))))) :rule-classes :type-prescription)
not-integerp-2g-expt-ctheorem
(defthm not-integerp-2g-expt-c (implies (and (real/rationalp x) (integerp n1) (real/rationalp y) (integerp n2) (< a 0) (< (* (expt x n1) (expt y n2)) a)) (not (integerp (* (expt x (- n1)) a (expt y (- n2)))))) :hints (("Goal" :use (:instance not-integerp-2f (x (expt x n1)) (y (expt y n2))))) :rule-classes :type-prescription)
local
(local (in-theory (disable not-integerp-2g not-integerp-2g-expt-a not-integerp-2g-expt-b not-integerp-2g-expt-c)))
not-integerp-2htheorem
(defthm not-integerp-2h (implies (and (real/rationalp x) (real/rationalp y) (< a 0) (< (* x y) a)) (not (integerp (* a (/ x) (/ y))))) :hints (("Goal" :use not-integerp-2f)) :rule-classes :type-prescription)
not-integerp-2h-expt-atheorem
(defthm not-integerp-2h-expt-a (implies (and (real/rationalp x) (integerp n) (real/rationalp y) (< a 0) (< (* (expt x n) y) a)) (not (integerp (* a (expt x (- n)) (/ y))))) :hints (("Goal" :use (:instance not-integerp-2f (x (expt x n))))) :rule-classes :type-prescription)
not-integerp-2h-expt-btheorem
(defthm not-integerp-2h-expt-b (implies (and (real/rationalp x) (real/rationalp y) (integerp n) (< a 0) (< (* x (expt y n)) a)) (not (integerp (* a (/ x) (expt y (- n)))))) :hints (("Goal" :use (:instance not-integerp-2f (y (expt y n))))) :rule-classes :type-prescription)
not-integerp-2h-expt-ctheorem
(defthm not-integerp-2h-expt-c (implies (and (real/rationalp x) (integerp n1) (real/rationalp y) (integerp n2) (< a 0) (< (* (expt x n1) (expt y n2)) a)) (not (integerp (* a (expt x (- n1)) (expt y (- n2)))))) :hints (("Goal" :use (:instance not-integerp-2f (x (expt x n1)) (y (expt y n2))))) :rule-classes :type-prescription)
local
(local (in-theory (disable not-integerp-2h not-integerp-2h-expt-a not-integerp-2h-expt-b not-integerp-2h-expt-c)))
not-integerp-2ktheorem
(defthm not-integerp-2k (implies (and (real/rationalp c) (real/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-2k-expttheorem
(defthm not-integerp-2k-expt (implies (and (real/rationalp c) (real/rationalp x) (integerp n) (< (* a b c) 0) (< (expt x n) (* a b c))) (not (integerp (* a b (expt x (- n)) c)))) :hints (("Goal" :use (:instance not-integerp-2a (a (* a b c)) (x (expt x n))))) :rule-classes :type-prescription)
local
(local (in-theory (disable not-integerp-2k not-integerp-2k-expt)))
not-integerp-2ltheorem
(defthm not-integerp-2l (implies (and (real/rationalp x) (< (* a b c) 0) (< x (* a b c))) (not (integerp (* a b c (/ x))))) :hints (("Goal" :use (:instance not-integerp-2a (a (* a b c)) (x x)))) :rule-classes :type-prescription)
not-integerp-2l-expttheorem
(defthm not-integerp-2l-expt (implies (and (real/rationalp x) (integerp n) (< (* a b c) 0) (< (expt x n) (* a b c))) (not (integerp (* a b c (expt x (- n)))))) :hints (("Goal" :use (:instance not-integerp-2a (a (* a b c)) (x (expt x n))))) :rule-classes :type-prescription)
local
(local (in-theory (disable not-integerp-2l not-integerp-2l-expt)))
not-integerp-2ntheorem
(defthm not-integerp-2n (implies (and (real/rationalp x) (real/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-2n-expt-atheorem
(defthm not-integerp-2n-expt-a (implies (and (real/rationalp x) (integerp n) (real/rationalp y) (< (* a b) 0) (< (* (expt x n) y) (* a b))) (not (integerp (* (expt x (- n)) a (/ y) b)))) :hints (("Goal" :use (:instance not-integerp-2a (a (* a b)) (x (* (expt x n) y))))) :rule-classes :type-prescription)
not-integerp-2n-expt-btheorem
(defthm not-integerp-2n-expt-b (implies (and (real/rationalp x) (real/rationalp y) (integerp n) (< (* a b) 0) (< (* x (expt y n)) (* a b))) (not (integerp (* (/ x) a (expt y (- n)) b)))) :hints (("Goal" :use (:instance not-integerp-2a (a (* a b)) (x (* x (expt y n)))))) :rule-classes :type-prescription)
not-integerp-2n-expt-ctheorem
(defthm not-integerp-2n-expt-c (implies (and (real/rationalp x) (integerp n1) (real/rationalp y) (integerp n2) (< (* a b) 0) (< (* (expt x n1) (expt y n2)) (* a b))) (not (integerp (* (expt x (- n1)) a (expt y (- n2)) b)))) :hints (("Goal" :use (:instance not-integerp-2a (a (* a b)) (x (* (expt x n1) (expt y n2)))))) :rule-classes :type-prescription)
local
(local (in-theory (disable not-integerp-2n not-integerp-2n-expt-a not-integerp-2n-expt-b not-integerp-2n-expt-c)))
not-integerp-2otheorem
(defthm not-integerp-2o (implies (and (real/rationalp x) (real/rationalp y) (< (* a b) 0) (< (* x y) (* a b))) (not (integerp (* (/ x) a b (/ y))))) :hints (("Goal" :use (:instance not-integerp-2a (a (* a b)) (x (* x y))))) :rule-classes :type-prescription)
not-integerp-2o-expt-atheorem
(defthm not-integerp-2o-expt-a (implies (and (real/rationalp x) (integerp n) (real/rationalp y) (< (* a b) 0) (< (* (expt x n) y) (* a b))) (not (integerp (* (expt x (- n)) a b (/ y))))) :hints (("Goal" :use (:instance not-integerp-2a (a (* a b)) (x (* (expt x n) y))))) :rule-classes :type-prescription)
not-integerp-2o-expt-btheorem
(defthm not-integerp-2o-expt-b (implies (and (real/rationalp x) (real/rationalp y) (integerp n) (< (* a b) 0) (< (* x (expt y n)) (* a b))) (not (integerp (* (/ x) a b (expt y (- n)))))) :hints (("Goal" :use (:instance not-integerp-2a (a (* a b)) (x (* x (expt y n)))))) :rule-classes :type-prescription)
not-integerp-2o-expt-ctheorem
(defthm not-integerp-2o-expt-c (implies (and (real/rationalp x) (integerp n1) (real/rationalp y) (integerp n2) (< (* a b) 0) (< (* (expt x n1) (expt y n2)) (* a b))) (not (integerp (* (expt x (- n1)) a b (expt y (- n2)))))) :hints (("Goal" :use (:instance not-integerp-2a (a (* a b)) (x (* (expt x n1) (expt y n2)))))) :rule-classes :type-prescription)
local
(local (in-theory (disable not-integerp-2o not-integerp-2o-expt-a not-integerp-2o-expt-b not-integerp-2o-expt-c)))
not-integerp-2ptheorem
(defthm not-integerp-2p (implies (and (real/rationalp x) (real/rationalp y) (< (* a b) 0) (< (* x y) (* a b))) (not (integerp (* a (/ x) (/ y) b)))) :hints (("Goal" :use (:instance not-integerp-2a (a (* a b)) (x (* x y))))) :rule-classes :type-prescription)
not-integerp-2p-expt-atheorem
(defthm not-integerp-2p-expt-a (implies (and (real/rationalp x) (integerp n) (real/rationalp y) (< (* a b) 0) (< (* (expt x n) y) (* a b))) (not (integerp (* a (expt x (- n)) (/ y) b)))) :hints (("Goal" :use (:instance not-integerp-2a (a (* a b)) (x (* (expt x n) y))))) :rule-classes :type-prescription)
not-integerp-2p-expt-btheorem
(defthm not-integerp-2p-expt-b (implies (and (real/rationalp x) (real/rationalp y) (integerp n) (< (* a b) 0) (< (* x (expt y n)) (* a b))) (not (integerp (* a (/ x) (expt y (- n)) b)))) :hints (("Goal" :use (:instance not-integerp-2a (a (* a b)) (x (* x (expt y n)))))) :rule-classes :type-prescription)
not-integerp-2p-expt-ctheorem
(defthm not-integerp-2p-expt-c (implies (and (real/rationalp x) (integerp n1) (real/rationalp y) (integerp n2) (< (* a b) 0) (< (* (expt x n1) (expt y n2)) (* a b))) (not (integerp (* a (expt x (- n1)) (expt y (- n2)) b)))) :hints (("Goal" :use (:instance not-integerp-2a (a (* a b)) (x (* (expt x n1) (expt y n2)))))) :rule-classes :type-prescription)
local
(local (in-theory (disable not-integerp-2p not-integerp-2p-expt-a not-integerp-2p-expt-b not-integerp-2p-expt-c)))
not-integerp-2qtheorem
(defthm not-integerp-2q (implies (and (real/rationalp x) (real/rationalp y) (< (* a b) 0) (< (* x y) (* a b))) (not (integerp (* a (/ x) b (/ y))))) :hints (("Goal" :use (:instance not-integerp-2a (a (* a b)) (x (* x y))))) :rule-classes :type-prescription)
not-integerp-2q-expt-atheorem
(defthm not-integerp-2q-expt-a (implies (and (real/rationalp x) (integerp n) (real/rationalp y) (< (* a b) 0) (< (* (expt x n) y) (* a b))) (not (integerp (* a (expt x (- n)) b (/ y))))) :hints (("Goal" :use (:instance not-integerp-2a (a (* a b)) (x (* (expt x n) y))))) :rule-classes :type-prescription)
not-integerp-2q-expt-btheorem
(defthm not-integerp-2q-expt-b (implies (and (real/rationalp x) (real/rationalp y) (integerp n) (< (* a b) 0) (< (* x (expt y n)) (* a b))) (not (integerp (* a (/ x) b (expt y (- n)))))) :hints (("Goal" :use (:instance not-integerp-2a (a (* a b)) (x (* x (expt y n)))))) :rule-classes :type-prescription)
not-integerp-2q-expt-ctheorem
(defthm not-integerp-2q-expt-c (implies (and (real/rationalp x) (integerp n1) (real/rationalp y) (integerp n2) (< (* a b) 0) (< (* (expt x n1) (expt y n2)) (* a b))) (not (integerp (* a (expt x (- n1)) b (expt y (- n2)))))) :hints (("Goal" :use (:instance not-integerp-2a (a (* a b)) (x (* (expt x n1) (expt y n2)))))) :rule-classes :type-prescription)
local
(local (in-theory (disable not-integerp-2q not-integerp-2q-expt-a not-integerp-2q-expt-b not-integerp-2q-expt-c)))
not-integerp-2rtheorem
(defthm not-integerp-2r (implies (and (real/rationalp x) (real/rationalp y) (< (* a b) 0) (< (* x y) (* a b))) (not (integerp (* a b (/ x) (/ y))))) :hints (("Goal" :use (:instance not-integerp-2a (a (* a b)) (x (* x y))))) :rule-classes :type-prescription)
not-integerp-2r-expt-atheorem
(defthm not-integerp-2r-expt-a (implies (and (real/rationalp x) (integerp n) (real/rationalp y) (< (* a b) 0) (< (* (expt x n) y) (* a b))) (not (integerp (* a b (expt x (- n)) (/ y))))) :hints (("Goal" :use (:instance not-integerp-2a (a (* a b)) (x (* (expt x n) y))))) :rule-classes :type-prescription)
not-integerp-2r-expt-btheorem
(defthm not-integerp-2r-expt-b (implies (and (real/rationalp x) (real/rationalp y) (integerp n) (< (* a b) 0) (< (* x (expt y n)) (* a b))) (not (integerp (* a b (/ x) (expt y (- n)))))) :hints (("Goal" :use (:instance not-integerp-2a (a (* a b)) (x (* x (expt y n)))))) :rule-classes :type-prescription)
not-integerp-2r-expt-ctheorem
(defthm not-integerp-2r-expt-c (implies (and (real/rationalp x) (integerp n1) (real/rationalp y) (integerp n2) (< (* a b) 0) (< (* (expt x n1) (expt y n2)) (* a b))) (not (integerp (* a b (expt x (- n1)) (expt y (- n2)))))) :hints (("Goal" :use (:instance not-integerp-2a (a (* a b)) (x (* (expt x n1) (expt y n2)))))) :rule-classes :type-prescription)
local
(local (in-theory (disable not-integerp-2r not-integerp-2r-expt-a not-integerp-2r-expt-b not-integerp-2r-expt-c)))
not-integerp-2stheorem
(defthm not-integerp-2s (implies (and (real/rationalp x) (real/rationalp y) (real/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-2s-expt-atheorem
(defthm not-integerp-2s-expt-a (implies (and (real/rationalp x) (integerp n) (real/rationalp y) (real/rationalp z) (< a 0) (< (* (expt x n) y z) a)) (not (integerp (* (expt x (- n)) (/ y) (/ z) a)))) :hints (("Goal" :use (:instance not-integerp-2a (a a) (x (* (expt x n) y z))))) :rule-classes :type-prescription)
not-integerp-2s-expt-btheorem
(defthm not-integerp-2s-expt-b (implies (and (real/rationalp x) (real/rationalp y) (integerp n) (real/rationalp z) (< a 0) (< (* x (expt y n) z) a)) (not (integerp (* (/ x) (expt y (- n)) (/ z) a)))) :hints (("Goal" :use (:instance not-integerp-2a (a a) (x (* x (expt y n) z))))) :rule-classes :type-prescription)
not-integerp-2s-expt-ctheorem
(defthm not-integerp-2s-expt-c (implies (and (real/rationalp x) (real/rationalp y) (real/rationalp z) (integerp n) (< a 0) (< (* x y (expt z n)) a)) (not (integerp (* (/ x) (/ y) (expt z (- n)) a)))) :hints (("Goal" :use (:instance not-integerp-2a (a a) (x (* x y (expt z n)))))) :rule-classes :type-prescription)
not-integerp-2s-expt-dtheorem
(defthm not-integerp-2s-expt-d (implies (and (real/rationalp x) (integerp n1) (real/rationalp y) (integerp n2) (real/rationalp z) (< a 0) (< (* (expt x n1) (expt y n2) z) a)) (not (integerp (* (expt x (- n1)) (expt y (- n2)) (/ z) a)))) :hints (("Goal" :use (:instance not-integerp-2a (a a) (x (* (expt x n1) (expt y n2) z))))) :rule-classes :type-prescription)
not-integerp-2s-expt-etheorem
(defthm not-integerp-2s-expt-e (implies (and (real/rationalp x) (integerp n1) (real/rationalp y) (real/rationalp z) (integerp n2) (< a 0) (< (* (expt x n1) y (expt z n2)) a)) (not (integerp (* (expt x (- n1)) (/ y) (expt z (- n2)) a)))) :hints (("Goal" :use (:instance not-integerp-2a (a a) (x (* (expt x n1) y (expt z n2)))))) :rule-classes :type-prescription)
not-integerp-2s-expt-ftheorem
(defthm not-integerp-2s-expt-f (implies (and (real/rationalp x) (real/rationalp y) (integerp n1) (real/rationalp z) (integerp n2) (< a 0) (< (* x (expt y n1) (expt z n2)) a)) (not (integerp (* (/ x) (expt y (- n1)) (expt z (- n2)) a)))) :hints (("Goal" :use (:instance not-integerp-2a (a a) (x (* x (expt y n1) (expt z n2)))))) :rule-classes :type-prescription)
not-integerp-2s-expt-gtheorem
(defthm not-integerp-2s-expt-g (implies (and (real/rationalp x) (integerp n1) (real/rationalp y) (integerp n2) (real/rationalp z) (integerp n3) (< a 0) (< (* (expt x n1) (expt y n2) (expt z n3)) a)) (not (integerp (* (expt x (- n1)) (expt y (- n2)) (expt z (- n3)) a)))) :hints (("Goal" :use (:instance not-integerp-2a (a a) (x (* (expt x n1) (expt y n2) (expt z n3)))))) :rule-classes :type-prescription)
local
(local (in-theory (disable not-integerp-2s not-integerp-2s-expt-a not-integerp-2s-expt-b not-integerp-2s-expt-c not-integerp-2s-expt-d not-integerp-2s-expt-e not-integerp-2s-expt-f not-integerp-2s-expt-g)))
not-integerp-2ttheorem
(defthm not-integerp-2t (implies (and (real/rationalp x) (real/rationalp y) (real/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-2t-expt-atheorem
(defthm not-integerp-2t-expt-a (implies (and (real/rationalp x) (integerp n) (real/rationalp y) (real/rationalp z) (< a 0) (< (* (expt x n) y z) a)) (not (integerp (* (expt x (- n)) (/ y) a (/ z))))) :hints (("Goal" :use (:instance not-integerp-2s (x (expt x n))))) :rule-classes :type-prescription)
not-integerp-2t-expt-btheorem
(defthm not-integerp-2t-expt-b (implies (and (real/rationalp x) (real/rationalp y) (integerp n) (real/rationalp z) (< a 0) (< (* x (expt y n) z) a)) (not (integerp (* (/ x) (expt y (- n)) a (/ z))))) :hints (("Goal" :use (:instance not-integerp-2s (y (expt y n))))) :rule-classes :type-prescription)
not-integerp-2t-expt-ctheorem
(defthm not-integerp-2t-expt-c (implies (and (real/rationalp x) (real/rationalp y) (real/rationalp z) (integerp n) (< a 0) (< (* x y (expt z n)) a)) (not (integerp (* (/ x) (/ y) a (expt z (- n)))))) :hints (("Goal" :use (:instance not-integerp-2s (z (expt z n))))) :rule-classes :type-prescription)
not-integerp-2t-expt-dtheorem
(defthm not-integerp-2t-expt-d (implies (and (real/rationalp x) (integerp n1) (real/rationalp y) (integerp n2) (real/rationalp z) (< a 0) (< (* (expt x n1) (expt y n2) z) a)) (not (integerp (* (expt x (- n1)) (expt y (- n2)) a (/ z))))) :hints (("Goal" :use (:instance not-integerp-2s (x (expt x n1)) (y (expt y n2))))) :rule-classes :type-prescription)
not-integerp-2t-expt-etheorem
(defthm not-integerp-2t-expt-e (implies (and (real/rationalp x) (integerp n1) (real/rationalp y) (real/rationalp z) (integerp n2) (< a 0) (< (* (expt x n1) y (expt z n2)) a)) (not (integerp (* (expt x (- n1)) (/ y) a (expt z (- n2)))))) :hints (("Goal" :use (:instance not-integerp-2s (x (expt x n1)) (z (expt z n2))))) :rule-classes :type-prescription)
not-integerp-2t-expt-ftheorem
(defthm not-integerp-2t-expt-f (implies (and (real/rationalp x) (real/rationalp y) (integerp n1) (real/rationalp z) (integerp n2) (< a 0) (< (* x (expt y n1) (expt z n2)) a)) (not (integerp (* (/ x) (expt y (- n1)) a (expt z (- n2)))))) :hints (("Goal" :use (:instance not-integerp-2s (y (expt y n1)) (z (expt z n2))))) :rule-classes :type-prescription)
not-integerp-2t-expt-gtheorem
(defthm not-integerp-2t-expt-g (implies (and (real/rationalp x) (integerp n1) (real/rationalp y) (integerp n2) (real/rationalp z) (integerp n3) (< a 0) (< (* (expt x n1) (expt y n2) (expt z n3)) a)) (not (integerp (* (expt x (- n1)) (expt y (- n2)) a (expt z (- n3)))))) :hints (("Goal" :use (:instance not-integerp-2s (x (expt x n1)) (y (expt y n2)) (z (expt z n3))))) :rule-classes :type-prescription)
local
(local (in-theory (disable not-integerp-2t not-integerp-2t-expt-a not-integerp-2t-expt-b not-integerp-2t-expt-c not-integerp-2t-expt-d not-integerp-2t-expt-e not-integerp-2t-expt-f not-integerp-2t-expt-g)))
not-integerp-2utheorem
(defthm not-integerp-2u (implies (and (real/rationalp x) (real/rationalp y) (real/rationalp z) (< a 0) (< (* x y z) a)) (not (integerp (* (/ x) a (/ y) (/ z))))) :hints (("Goal" :use (:instance not-integerp-2s))) :rule-classes :type-prescription)
not-integerp-2u-expt-atheorem
(defthm not-integerp-2u-expt-a (implies (and (real/rationalp x) (integerp n) (real/rationalp y) (real/rationalp z) (< a 0) (< (* (expt x n) y z) a)) (not (integerp (* (expt x (- n)) a (/ y) (/ z))))) :hints (("Goal" :use (:instance not-integerp-2s (x (expt x n))))) :rule-classes :type-prescription)
not-integerp-2u-expt-btheorem
(defthm not-integerp-2u-expt-b (implies (and (real/rationalp x) (real/rationalp y) (integerp n) (real/rationalp z) (< a 0) (< (* x (expt y n) z) a)) (not (integerp (* (/ x) a (expt y (- n)) (/ z))))) :hints (("Goal" :use (:instance not-integerp-2s (y (expt y n))))) :rule-classes :type-prescription)
not-integerp-2u-expt-ctheorem
(defthm not-integerp-2u-expt-c (implies (and (real/rationalp x) (real/rationalp y) (real/rationalp z) (integerp n) (< a 0) (< (* x y (expt z n)) a)) (not (integerp (* (/ x) a (/ y) (expt z (- n)))))) :hints (("Goal" :use (:instance not-integerp-2s (z (expt z n))))) :rule-classes :type-prescription)
not-integerp-2u-expt-dtheorem
(defthm not-integerp-2u-expt-d (implies (and (real/rationalp x) (integerp n1) (real/rationalp y) (integerp n2) (real/rationalp z) (< a 0) (< (* (expt x n1) (expt y n2) z) a)) (not (integerp (* (expt x (- n1)) a (expt y (- n2)) (/ z))))) :hints (("Goal" :use (:instance not-integerp-2s (x (expt x n1)) (y (expt y n2))))) :rule-classes :type-prescription)
not-integerp-2u-expt-etheorem
(defthm not-integerp-2u-expt-e (implies (and (real/rationalp x) (integerp n1) (real/rationalp y) (real/rationalp z) (integerp n2) (< a 0) (< (* (expt x n1) y (expt z n2)) a)) (not (integerp (* (expt x (- n1)) a (/ y) (expt z (- n2)))))) :hints (("Goal" :use (:instance not-integerp-2s (x (expt x n1)) (z (expt z n2))))) :rule-classes :type-prescription)
not-integerp-2u-expt-ftheorem
(defthm not-integerp-2u-expt-f (implies (and (real/rationalp x) (real/rationalp y) (integerp n1) (real/rationalp z) (integerp n2) (< a 0) (< (* x (expt y n1) (expt z n2)) a)) (not (integerp (* (/ x) a (expt y (- n1)) (expt z (- n2)))))) :hints (("Goal" :use (:instance not-integerp-2s (y (expt y n1)) (z (expt z n2))))) :rule-classes :type-prescription)
not-integerp-2u-expt-gtheorem
(defthm not-integerp-2u-expt-g (implies (and (real/rationalp x) (integerp n1) (real/rationalp y) (integerp n2) (real/rationalp z) (integerp n3) (< a 0) (< (* (expt x n1) (expt y n2) (expt z n3)) a)) (not (integerp (* (expt x (- n1)) a (expt y (- n2)) (expt z (- n3)))))) :hints (("Goal" :use (:instance not-integerp-2s (x (expt x n1)) (y (expt y n2)) (z (expt z n3))))) :rule-classes :type-prescription)
local
(local (in-theory (disable not-integerp-2u not-integerp-2u-expt-a not-integerp-2u-expt-b not-integerp-2u-expt-c not-integerp-2u-expt-d not-integerp-2u-expt-e not-integerp-2u-expt-f not-integerp-2u-expt-g)))
not-integerp-2vtheorem
(defthm not-integerp-2v (implies (and (real/rationalp x) (real/rationalp y) (real/rationalp z) (< a 0) (< (* x y z) a)) (not (integerp (* a (/ x) (/ y) (/ z))))) :hints (("Goal" :use (:instance not-integerp-2s))) :rule-classes :type-prescription)
not-integerp-2v-expt-atheorem
(defthm not-integerp-2v-expt-a (implies (and (real/rationalp x) (integerp n) (real/rationalp y) (real/rationalp z) (< a 0) (< (* (expt x n) y z) a)) (not (integerp (* a (expt x (- n)) (/ y) (/ z))))) :hints (("Goal" :use (:instance not-integerp-2s (x (expt x n))))) :rule-classes :type-prescription)
not-integerp-2v-expt-btheorem
(defthm not-integerp-2v-expt-b (implies (and (real/rationalp x) (real/rationalp y) (integerp n) (real/rationalp z) (< a 0) (< (* x (expt y n) z) a)) (not (integerp (* a (/ x) (expt y (- n)) (/ z))))) :hints (("Goal" :use (:instance not-integerp-2s (y (expt y n))))) :rule-classes :type-prescription)
not-integerp-2v-expt-ctheorem
(defthm not-integerp-2v-expt-c (implies (and (real/rationalp x) (real/rationalp y) (real/rationalp z) (integerp n) (< a 0) (< (* x y (expt z n)) a)) (not (integerp (* a (/ x) (/ y) (expt z (- n)))))) :hints (("Goal" :use (:instance not-integerp-2s (z (expt z n))))) :rule-classes :type-prescription)
not-integerp-2v-expt-dtheorem
(defthm not-integerp-2v-expt-d (implies (and (real/rationalp x) (integerp n1) (real/rationalp y) (integerp n2) (real/rationalp z) (< a 0) (< (* (expt x n1) (expt y n2) z) a)) (not (integerp (* a (expt x (- n1)) (expt y (- n2)) (/ z))))) :hints (("Goal" :use (:instance not-integerp-2s (x (expt x n1)) (y (expt y n2))))) :rule-classes :type-prescription)
not-integerp-2v-expt-etheorem
(defthm not-integerp-2v-expt-e (implies (and (real/rationalp x) (integerp n1) (real/rationalp y) (real/rationalp z) (integerp n2) (< a 0) (< (* (expt x n1) y (expt z n2)) a)) (not (integerp (* a (expt x (- n1)) (/ y) (expt z (- n2)))))) :hints (("Goal" :use (:instance not-integerp-2s (x (expt x n1)) (z (expt z n2))))) :rule-classes :type-prescription)
not-integerp-2v-expt-ftheorem
(defthm not-integerp-2v-expt-f (implies (and (real/rationalp x) (real/rationalp y) (integerp n1) (real/rationalp z) (integerp n2) (< a 0) (< (* x (expt y n1) (expt z n2)) a)) (not (integerp (* a (/ x) (expt y (- n1)) (expt z (- n2)))))) :hints (("Goal" :use (:instance not-integerp-2s (y (expt y n1)) (z (expt z n2))))) :rule-classes :type-prescription)
not-integerp-2v-expt-gtheorem
(defthm not-integerp-2v-expt-g (implies (and (real/rationalp x) (integerp n1) (real/rationalp y) (integerp n2) (real/rationalp z) (integerp n3) (< a 0) (< (* (expt x n1) (expt y n2) (expt z n3)) a)) (not (integerp (* a (expt x (- n1)) (expt y (- n2)) (expt z (- n3)))))) :hints (("Goal" :use (:instance not-integerp-2s (x (expt x n1)) (y (expt y n2)) (z (expt z n3))))) :rule-classes :type-prescription)
local
(local (in-theory (disable not-integerp-2v not-integerp-2v-expt-a not-integerp-2v-expt-b not-integerp-2v-expt-c not-integerp-2v-expt-d not-integerp-2v-expt-e not-integerp-2v-expt-f not-integerp-2v-expt-g)))
not-integerp-3atheorem
(defthm not-integerp-3a (implies (and (real/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-3a-expttheorem
(defthm not-integerp-3a-expt (implies (and (real/rationalp x) (integerp n) (< 0 a) (< (expt x n) (- a))) (not (integerp (* (expt x (- n)) a)))) :hints (("Goal" :use (:instance not-integerp-3a (x (expt x n))))) :rule-classes :type-prescription)
local
(local (in-theory (disable not-integerp-3a not-integerp-3a-expt)))
not-integerp-3btheorem
(defthm not-integerp-3b (implies (and (real/rationalp x) (< 0 a) (< x (- a))) (not (integerp (* a (/ x))))) :hints (("Goal" :use not-integerp-3a)) :rule-classes :type-prescription)
not-integerp-3b-expttheorem
(defthm not-integerp-3b-expt (implies (and (real/rationalp x) (integerp n) (< 0 a) (< (expt x n) (- a))) (not (integerp (* a (expt x (- n)))))) :hints (("Goal" :use (:instance not-integerp-3a (x (expt x n))))) :rule-classes :type-prescription)
local
(local (in-theory (disable not-integerp-3b not-integerp-3b-expt)))
not-integerp-3dtheorem
(defthm not-integerp-3d (implies (and (real/rationalp b) (real/rationalp x) (< 0 (* a b)) (< x (- (* a b)))) (not (integerp (* a (/ x) b)))) :hints (("Goal" :use (:instance not-integerp-3a (a (* a b)) (x x)))) :rule-classes :type-prescription)
not-integerp-3d-expttheorem
(defthm not-integerp-3d-expt (implies (and (real/rationalp b) (real/rationalp x) (integerp n) (< 0 (* a b)) (< (expt x n) (- (* a b)))) (not (integerp (* a (expt x (- n)) b)))) :hints (("Goal" :use (:instance not-integerp-3a (a (* a b)) (x (expt x n))))) :rule-classes :type-prescription)
local
(local (in-theory (disable not-integerp-3d not-integerp-3d-expt)))
not-integerp-3etheorem
(defthm not-integerp-3e (implies (and (real/rationalp x) (< 0 (* a b)) (< x (- (* a b)))) (not (integerp (* a b (/ x))))) :hints (("Goal" :use (:instance not-integerp-3a (a (* a b)) (x x)))) :rule-classes :type-prescription)
not-integerp-3e-expttheorem
(defthm not-integerp-3e-expt (implies (and (real/rationalp x) (integerp n) (< 0 (* a b)) (< (expt x n) (- (* a b)))) (not (integerp (* a b (expt x (- n)))))) :hints (("Goal" :use (:instance not-integerp-3a (a (* a b)) (x (expt x n))))) :rule-classes :type-prescription)
local
(local (in-theory (disable not-integerp-3e not-integerp-3e-expt)))
not-integerp-3ftheorem
(defthm not-integerp-3f (implies (and (real/rationalp x) (real/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-3f-expt-atheorem
(defthm not-integerp-3f-expt-a (implies (and (real/rationalp x) (integerp n) (real/rationalp y) (< 0 a) (< (* (expt x n) y) (- a))) (not (integerp (* (expt x (- n)) (/ y) a)))) :hints (("Goal" :use (:instance not-integerp-3a (a a) (x (* (expt x n) y))))) :rule-classes :type-prescription)
not-integerp-3f-expt-btheorem
(defthm not-integerp-3f-expt-b (implies (and (real/rationalp x) (real/rationalp y) (integerp n) (< 0 a) (< (* x (expt y n)) (- a))) (not (integerp (* (/ x) (expt y (- n)) a)))) :hints (("Goal" :use (:instance not-integerp-3a (a a) (x (* (expt y n) x))))) :rule-classes :type-prescription)
not-integerp-3f-expt-ctheorem
(defthm not-integerp-3f-expt-c (implies (and (real/rationalp x) (integerp n1) (real/rationalp y) (integerp n2) (< 0 a) (< (* (expt x n1) (expt y n2)) (- a))) (not (integerp (* (expt x (- n1)) (expt y (- n2)) a)))) :hints (("Goal" :use (:instance not-integerp-3a (a a) (x (* (expt x n1) (expt y n2)))))) :rule-classes :type-prescription)
local
(local (in-theory (disable not-integerp-3f not-integerp-3f-expt-a not-integerp-3f-expt-b not-integerp-3f-expt-c)))
not-integerp-3gtheorem
(defthm not-integerp-3g (implies (and (real/rationalp x) (real/rationalp y) (< 0 a) (< (* x y) (- a))) (not (integerp (* (/ x) a (/ y))))) :hints (("Goal" :use not-integerp-3f)) :rule-classes :type-prescription)
not-integerp-3g-expt-atheorem
(defthm not-integerp-3g-expt-a (implies (and (real/rationalp x) (integerp n) (real/rationalp y) (< 0 a) (< (* (expt x n) y) (- a))) (not (integerp (* (expt x (- n)) a (/ y))))) :hints (("Goal" :use (:instance not-integerp-3f (x (expt x n))))) :rule-classes :type-prescription)
not-integerp-3g-expt-btheorem
(defthm not-integerp-3g-expt-b (implies (and (real/rationalp x) (real/rationalp y) (integerp n) (< 0 a) (< (* x (expt y n)) (- a))) (not (integerp (* (/ x) a (expt y (- n)))))) :hints (("Goal" :use (:instance not-integerp-3f (y (expt y n))))) :rule-classes :type-prescription)
not-integerp-3g-expt-ctheorem
(defthm not-integerp-3g-expt-c (implies (and (real/rationalp x) (integerp n1) (real/rationalp y) (integerp n2) (< 0 a) (< (* (expt x n1) (expt y n2)) (- a))) (not (integerp (* (expt x (- n1)) a (expt y (- n2)))))) :hints (("Goal" :use (:instance not-integerp-3f (x (expt x n1)) (y (expt y n2))))) :rule-classes :type-prescription)
local
(local (in-theory (disable not-integerp-3g not-integerp-3g-expt-a not-integerp-3g-expt-b not-integerp-3g-expt-c)))
not-integerp-3htheorem
(defthm not-integerp-3h (implies (and (real/rationalp x) (real/rationalp y) (< 0 a) (< (* x y) (- a))) (not (integerp (* a (/ x) (/ y))))) :hints (("Goal" :use not-integerp-3f)) :rule-classes :type-prescription)
not-integerp-3h-expt-atheorem
(defthm not-integerp-3h-expt-a (implies (and (real/rationalp x) (integerp n) (real/rationalp y) (< 0 a) (< (* (expt x n) y) (- a))) (not (integerp (* a (expt x (- n)) (/ y))))) :hints (("Goal" :use (:instance not-integerp-3f (x (expt x n))))) :rule-classes :type-prescription)
not-integerp-3h-expt-btheorem
(defthm not-integerp-3h-expt-b (implies (and (real/rationalp x) (real/rationalp y) (integerp n) (< 0 a) (< (* x (expt y n)) (- a))) (not (integerp (* a (/ x) (expt y (- n)))))) :hints (("Goal" :use (:instance not-integerp-3f (y (expt y n))))) :rule-classes :type-prescription)
not-integerp-3h-expt-ctheorem
(defthm not-integerp-3h-expt-c (implies (and (real/rationalp x) (integerp n1) (real/rationalp y) (integerp n2) (< 0 a) (< (* (expt x n1) (expt y n2)) (- a))) (not (integerp (* a (expt x (- n1)) (expt y (- n2)))))) :hints (("Goal" :use (:instance not-integerp-3f (x (expt x n1)) (y (expt y n2))))) :rule-classes :type-prescription)
local
(local (in-theory (disable not-integerp-3h not-integerp-3h-expt-a not-integerp-3h-expt-b not-integerp-3h-expt-c)))
not-integerp-3ktheorem
(defthm not-integerp-3k (implies (and (real/rationalp c) (real/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-3k-expttheorem
(defthm not-integerp-3k-expt (implies (and (real/rationalp c) (real/rationalp x) (integerp n) (< 0 (* a b c)) (< (expt x n) (- (* a b c)))) (not (integerp (* a b (expt x (- n)) c)))) :hints (("Goal" :use (:instance not-integerp-3a (a (* a b c)) (x (expt x n))))) :rule-classes :type-prescription)
local
(local (in-theory (disable not-integerp-3k not-integerp-3k-expt)))
not-integerp-3ltheorem
(defthm not-integerp-3l (implies (and (real/rationalp x) (< 0 (* a b c)) (< x (- (* a b c)))) (not (integerp (* a b c (/ x))))) :hints (("Goal" :use (:instance not-integerp-3a (a (* a b c)) (x x)))) :rule-classes :type-prescription)
not-integerp-3l-expttheorem
(defthm not-integerp-3l-expt (implies (and (real/rationalp x) (integerp n) (< 0 (* a b c)) (< (expt x n) (- (* a b c)))) (not (integerp (* a b c (expt x (- n)))))) :hints (("Goal" :use (:instance not-integerp-3a (a (* a b c)) (x (expt x n))))) :rule-classes :type-prescription)
local
(local (in-theory (disable not-integerp-3l not-integerp-3l-expt)))
not-integerp-3ntheorem
(defthm not-integerp-3n (implies (and (real/rationalp x) (real/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-3n-expt-atheorem
(defthm not-integerp-3n-expt-a (implies (and (real/rationalp x) (integerp n) (real/rationalp y) (< 0 (* a b)) (< (* (expt x n) y) (- (* a b)))) (not (integerp (* (expt x (- n)) a (/ y) b)))) :hints (("Goal" :use (:instance not-integerp-3a (a (* a b)) (x (* (expt x n) y))))) :rule-classes :type-prescription)
not-integerp-3n-expt-btheorem
(defthm not-integerp-3n-expt-b (implies (and (real/rationalp x) (real/rationalp y) (integerp n) (< 0 (* a b)) (< (* x (expt y n)) (- (* a b)))) (not (integerp (* (/ x) a (expt y (- n)) b)))) :hints (("Goal" :use (:instance not-integerp-3a (a (* a b)) (x (* x (expt y n)))))) :rule-classes :type-prescription)
not-integerp-3n-expt-ctheorem
(defthm not-integerp-3n-expt-c (implies (and (real/rationalp x) (integerp n1) (real/rationalp y) (integerp n2) (< 0 (* a b)) (< (* (expt x n1) (expt y n2)) (- (* a b)))) (not (integerp (* (expt x (- n1)) a (expt y (- n2)) b)))) :hints (("Goal" :use (:instance not-integerp-3a (a (* a b)) (x (* (expt x n1) (expt y n2)))))) :rule-classes :type-prescription)
local
(local (in-theory (disable not-integerp-3n not-integerp-3n-expt-a not-integerp-3n-expt-b not-integerp-3n-expt-c)))
not-integerp-3otheorem
(defthm not-integerp-3o (implies (and (real/rationalp x) (real/rationalp y) (< 0 (* a b)) (< (* x y) (- (* a b)))) (not (integerp (* (/ x) a b (/ y))))) :hints (("Goal" :use (:instance not-integerp-3a (a (* a b)) (x (* x y))))) :rule-classes :type-prescription)
not-integerp-3o-expt-atheorem
(defthm not-integerp-3o-expt-a (implies (and (real/rationalp x) (integerp n) (real/rationalp y) (< 0 (* a b)) (< (* (expt x n) y) (- (* a b)))) (not (integerp (* (expt x (- n)) a b (/ y))))) :hints (("Goal" :use (:instance not-integerp-3a (a (* a b)) (x (* (expt x n) y))))) :rule-classes :type-prescription)
not-integerp-3o-expt-btheorem
(defthm not-integerp-3o-expt-b (implies (and (real/rationalp x) (real/rationalp y) (integerp n) (< 0 (* a b)) (< (* x (expt y n)) (- (* a b)))) (not (integerp (* (/ x) a b (expt y (- n)))))) :hints (("Goal" :use (:instance not-integerp-3a (a (* a b)) (x (* x (expt y n)))))) :rule-classes :type-prescription)
not-integerp-3o-expt-ctheorem
(defthm not-integerp-3o-expt-c (implies (and (real/rationalp x) (integerp n1) (real/rationalp y) (integerp n2) (< 0 (* a b)) (< (* (expt x n1) (expt y n2)) (- (* a b)))) (not (integerp (* (expt x (- n1)) a b (expt y (- n2)))))) :hints (("Goal" :use (:instance not-integerp-3a (a (* a b)) (x (* (expt x n1) (expt y n2)))))) :rule-classes :type-prescription)
local
(local (in-theory (disable not-integerp-3o not-integerp-3o-expt-a not-integerp-3o-expt-b not-integerp-3o-expt-c)))
not-integerp-3ptheorem
(defthm not-integerp-3p (implies (and (real/rationalp x) (real/rationalp y) (< 0 (* a b)) (< (* x y) (- (* a b)))) (not (integerp (* a (/ x) (/ y) b)))) :hints (("Goal" :use (:instance not-integerp-3a (a (* a b)) (x (* x y))))) :rule-classes :type-prescription)
not-integerp-3p-expt-atheorem
(defthm not-integerp-3p-expt-a (implies (and (real/rationalp x) (integerp n) (real/rationalp y) (< 0 (* a b)) (< (* (expt x n) y) (- (* a b)))) (not (integerp (* a (expt x (- n)) (/ y) b)))) :hints (("Goal" :use (:instance not-integerp-3a (a (* a b)) (x (* (expt x n) y))))) :rule-classes :type-prescription)
not-integerp-3p-expt-btheorem
(defthm not-integerp-3p-expt-b (implies (and (real/rationalp x) (real/rationalp y) (integerp n) (< 0 (* a b)) (< (* x (expt y n)) (- (* a b)))) (not (integerp (* a (/ x) (expt y (- n)) b)))) :hints (("Goal" :use (:instance not-integerp-3a (a (* a b)) (x (* x (expt y n)))))) :rule-classes :type-prescription)
not-integerp-3p-expt-ctheorem
(defthm not-integerp-3p-expt-c (implies (and (real/rationalp x) (integerp n1) (real/rationalp y) (integerp n2) (< 0 (* a b)) (< (* (expt x n1) (expt y n2)) (- (* a b)))) (not (integerp (* a (expt x (- n1)) (expt y (- n2)) b)))) :hints (("Goal" :use (:instance not-integerp-3a (a (* a b)) (x (* (expt x n1) (expt y n2)))))) :rule-classes :type-prescription)
local
(local (in-theory (disable not-integerp-3p not-integerp-3p-expt-a not-integerp-3p-expt-b not-integerp-3p-expt-c)))
not-integerp-3qtheorem
(defthm not-integerp-3q (implies (and (real/rationalp x) (real/rationalp y) (< 0 (* a b)) (< (* x y) (- (* a b)))) (not (integerp (* a (/ x) b (/ y))))) :hints (("Goal" :use (:instance not-integerp-3a (a (* a b)) (x (* x y))))) :rule-classes :type-prescription)
not-integerp-3q-expt-atheorem
(defthm not-integerp-3q-expt-a (implies (and (real/rationalp x) (integerp n) (real/rationalp y) (< 0 (* a b)) (< (* (expt x n) y) (- (* a b)))) (not (integerp (* a (expt x (- n)) b (/ y))))) :hints (("Goal" :use (:instance not-integerp-3a (a (* a b)) (x (* (expt x n) y))))) :rule-classes :type-prescription)
not-integerp-3q-expt-btheorem
(defthm not-integerp-3q-expt-b (implies (and (real/rationalp x) (real/rationalp y) (integerp n) (< 0 (* a b)) (< (* x (expt y n)) (- (* a b)))) (not (integerp (* a (/ x) b (expt y (- n)))))) :hints (("Goal" :use (:instance not-integerp-3a (a (* a b)) (x (* x (expt y n)))))) :rule-classes :type-prescription)
not-integerp-3q-expt-ctheorem
(defthm not-integerp-3q-expt-c (implies (and (real/rationalp x) (integerp n1) (real/rationalp y) (integerp n2) (< 0 (* a b)) (< (* (expt x n1) (expt y n2)) (- (* a b)))) (not (integerp (* a (expt x (- n1)) b (expt y (- n2)))))) :hints (("Goal" :use (:instance not-integerp-3a (a (* a b)) (x (* (expt x n1) (expt y n2)))))) :rule-classes :type-prescription)
local
(local (in-theory (disable not-integerp-3n not-integerp-3n-expt-a not-integerp-3n-expt-b not-integerp-3n-expt-c)))
not-integerp-3rtheorem
(defthm not-integerp-3r (implies (and (real/rationalp x) (real/rationalp y) (< 0 (* a b)) (< (* x y) (- (* a b)))) (not (integerp (* a b (/ x) (/ y))))) :hints (("Goal" :use (:instance not-integerp-3a (a (* a b)) (x (* x y))))) :rule-classes :type-prescription)
not-integerp-3r-expt-atheorem
(defthm not-integerp-3r-expt-a (implies (and (real/rationalp x) (integerp n) (real/rationalp y) (< 0 (* a b)) (< (* (expt x n) y) (- (* a b)))) (not (integerp (* a b (expt x (- n)) (/ y))))) :hints (("Goal" :use (:instance not-integerp-3a (a (* a b)) (x (* (expt x n) y))))) :rule-classes :type-prescription)
not-integerp-3r-expt-btheorem
(defthm not-integerp-3r-expt-b (implies (and (real/rationalp x) (real/rationalp y) (integerp n) (< 0 (* a b)) (< (* x (expt y n)) (- (* a b)))) (not (integerp (* a b (/ x) (expt y (- n)))))) :hints (("Goal" :use (:instance not-integerp-3a (a (* a b)) (x (* x (expt y n)))))) :rule-classes :type-prescription)
not-integerp-3r-expt-ctheorem
(defthm not-integerp-3r-expt-c (implies (and (real/rationalp x) (integerp n1) (real/rationalp y) (integerp n2) (< 0 (* a b)) (< (* (expt x n1) (expt y n2)) (- (* a b)))) (not (integerp (* a b (expt x (- n1)) (expt y (- n2)))))) :hints (("Goal" :use (:instance not-integerp-3a (a (* a b)) (x (* (expt x n1) (expt y n2)))))) :rule-classes :type-prescription)
local
(local (in-theory (disable not-integerp-3r not-integerp-3r-expt-a not-integerp-3r-expt-b not-integerp-3r-expt-c)))
not-integerp-3stheorem
(defthm not-integerp-3s (implies (and (real/rationalp x) (real/rationalp y) (real/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-3s-expt-atheorem
(defthm not-integerp-3s-expt-a (implies (and (real/rationalp x) (integerp n) (real/rationalp y) (real/rationalp z) (< 0 a) (< (* (expt x n) y z) (- a))) (not (integerp (* (expt x (- n)) (/ y) (/ z) a)))) :hints (("Goal" :use (:instance not-integerp-3a (a a) (x (* (expt x n) y z))))) :rule-classes :type-prescription)
not-integerp-3s-expt-btheorem
(defthm not-integerp-3s-expt-b (implies (and (real/rationalp x) (real/rationalp y) (integerp n) (real/rationalp z) (< 0 a) (< (* x (expt y n) z) (- a))) (not (integerp (* (/ x) (expt y (- n)) (/ z) a)))) :hints (("Goal" :use (:instance not-integerp-3a (a a) (x (* x (expt y n) z))))) :rule-classes :type-prescription)
not-integerp-3s-expt-ctheorem
(defthm not-integerp-3s-expt-c (implies (and (real/rationalp x) (real/rationalp y) (real/rationalp z) (integerp n) (< 0 a) (< (* x y (expt z n)) (- a))) (not (integerp (* (/ x) (/ y) (expt z (- n)) a)))) :hints (("Goal" :use (:instance not-integerp-3a (a a) (x (* x y (expt z n)))))) :rule-classes :type-prescription)
not-integerp-3s-expt-dtheorem
(defthm not-integerp-3s-expt-d (implies (and (real/rationalp x) (integerp n1) (real/rationalp y) (integerp n2) (real/rationalp z) (< 0 a) (< (* (expt x n1) (expt y n2) z) (- a))) (not (integerp (* (expt x (- n1)) (expt y (- n2)) (/ z) a)))) :hints (("Goal" :use (:instance not-integerp-3a (a a) (x (* (expt x n1) (expt y n2) z))))) :rule-classes :type-prescription)
not-integerp-3s-expt-etheorem
(defthm not-integerp-3s-expt-e (implies (and (real/rationalp x) (integerp n1) (real/rationalp y) (real/rationalp z) (integerp n2) (< 0 a) (< (* (expt x n1) y (expt z n2)) (- a))) (not (integerp (* (expt x (- n1)) (/ y) (expt z (- n2)) a)))) :hints (("Goal" :use (:instance not-integerp-3a (a a) (x (* (expt x n1) y (expt z n2)))))) :rule-classes :type-prescription)
not-integerp-3s-expt-ftheorem
(defthm not-integerp-3s-expt-f (implies (and (real/rationalp x) (real/rationalp y) (integerp n1) (real/rationalp z) (integerp n2) (< 0 a) (< (* x (expt y n1) (expt z n2)) (- a))) (not (integerp (* (/ x) (expt y (- n1)) (expt z (- n2)) a)))) :hints (("Goal" :use (:instance not-integerp-3a (a a) (x (* x (expt y n1) (expt z n2)))))) :rule-classes :type-prescription)
not-integerp-3s-expt-gtheorem
(defthm not-integerp-3s-expt-g (implies (and (real/rationalp x) (integerp n1) (real/rationalp y) (integerp n2) (real/rationalp z) (integerp n3) (< 0 a) (< (* (expt x n1) (expt y n2) (expt z n3)) (- a))) (not (integerp (* (expt x (- n1)) (expt y (- n2)) (expt z (- n3)) a)))) :hints (("Goal" :use (:instance not-integerp-3a (a a) (x (* (expt x n1) (expt y n2) (expt z n3)))))) :rule-classes :type-prescription)
local
(local (in-theory (disable not-integerp-3s not-integerp-3s-expt-a not-integerp-3s-expt-b not-integerp-3s-expt-c not-integerp-3s-expt-d not-integerp-3s-expt-e not-integerp-3s-expt-f not-integerp-3s-expt-g)))
not-integerp-3ttheorem
(defthm not-integerp-3t (implies (and (real/rationalp x) (real/rationalp y) (real/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-3t-expt-atheorem
(defthm not-integerp-3t-expt-a (implies (and (real/rationalp x) (integerp n) (real/rationalp y) (real/rationalp z) (< 0 a) (< (* (expt x n) y z) (- a))) (not (integerp (* (expt x (- n)) (/ y) a (/ z))))) :hints (("Goal" :use (:instance not-integerp-3s (x (expt x n))))) :rule-classes :type-prescription)
not-integerp-3t-expt-btheorem
(defthm not-integerp-3t-expt-b (implies (and (real/rationalp x) (real/rationalp y) (integerp n) (real/rationalp z) (< 0 a) (< (* x (expt y n) z) (- a))) (not (integerp (* (/ x) (expt y (- n)) a (/ z))))) :hints (("Goal" :use (:instance not-integerp-3s (y (expt y n))))) :rule-classes :type-prescription)
not-integerp-3t-expt-ctheorem
(defthm not-integerp-3t-expt-c (implies (and (real/rationalp x) (real/rationalp y) (real/rationalp z) (integerp n) (< 0 a) (< (* x y (expt z n)) (- a))) (not (integerp (* (/ x) (/ y) a (expt z (- n)))))) :hints (("Goal" :use (:instance not-integerp-3s (z (expt z n))))) :rule-classes :type-prescription)
not-integerp-3t-expt-dtheorem
(defthm not-integerp-3t-expt-d (implies (and (real/rationalp x) (integerp n1) (real/rationalp y) (integerp n2) (real/rationalp z) (< 0 a) (< (* (expt x n1) (expt y n2) z) (- a))) (not (integerp (* (expt x (- n1)) (expt y (- n2)) a (/ z))))) :hints (("Goal" :use (:instance not-integerp-3s (x (expt x n1)) (y (expt y n2))))) :rule-classes :type-prescription)
not-integerp-3t-expt-etheorem
(defthm not-integerp-3t-expt-e (implies (and (real/rationalp x) (integerp n1) (real/rationalp y) (real/rationalp z) (integerp n2) (< 0 a) (< (* (expt x n1) y (expt z n2)) (- a))) (not (integerp (* (expt x (- n1)) (/ y) a (expt z (- n2)))))) :hints (("Goal" :use (:instance not-integerp-3s (x (expt x n1)) (z (expt z n2))))) :rule-classes :type-prescription)
not-integerp-3t-expt-ftheorem
(defthm not-integerp-3t-expt-f (implies (and (real/rationalp x) (real/rationalp y) (integerp n1) (real/rationalp z) (integerp n2) (< 0 a) (< (* x (expt y n1) (expt z n2)) (- a))) (not (integerp (* (/ x) (expt y (- n1)) a (expt z (- n2)))))) :hints (("Goal" :use (:instance not-integerp-3s (y (expt y n1)) (z (expt z n2))))) :rule-classes :type-prescription)
not-integerp-3t-expt-gtheorem
(defthm not-integerp-3t-expt-g (implies (and (real/rationalp x) (integerp n1) (real/rationalp y) (integerp n2) (real/rationalp z) (integerp n3) (< 0 a) (< (* (expt x n1) (expt y n2) (expt z n3)) (- a))) (not (integerp (* (expt x (- n1)) (expt y (- n2)) a (expt z (- n3)))))) :hints (("Goal" :use (:instance not-integerp-3s (x (expt x n1)) (y (expt y n2)) (z (expt z n3))))) :rule-classes :type-prescription)
local
(local (in-theory (disable not-integerp-3t not-integerp-3t-expt-a not-integerp-3t-expt-b not-integerp-3t-expt-c not-integerp-3t-expt-d not-integerp-3t-expt-e not-integerp-3t-expt-f not-integerp-3t-expt-g)))
not-integerp-3utheorem
(defthm not-integerp-3u (implies (and (real/rationalp x) (real/rationalp y) (real/rationalp z) (< 0 a) (< (* x y z) (- a))) (not (integerp (* (/ x) a (/ y) (/ z))))) :hints (("Goal" :use (:instance not-integerp-3s))) :rule-classes :type-prescription)
not-integerp-3u-expt-atheorem
(defthm not-integerp-3u-expt-a (implies (and (real/rationalp x) (integerp n) (real/rationalp y) (real/rationalp z) (< 0 a) (< (* (expt x n) y z) (- a))) (not (integerp (* (expt x (- n)) a (/ y) (/ z))))) :hints (("Goal" :use (:instance not-integerp-3s (x (expt x n))))) :rule-classes :type-prescription)
not-integerp-3u-expt-btheorem
(defthm not-integerp-3u-expt-b (implies (and (real/rationalp x) (real/rationalp y) (integerp n) (real/rationalp z) (< 0 a) (< (* x (expt y n) z) (- a))) (not (integerp (* (/ x) a (expt y (- n)) (/ z))))) :hints (("Goal" :use (:instance not-integerp-3s (y (expt y n))))) :rule-classes :type-prescription)
not-integerp-3u-expt-ctheorem
(defthm not-integerp-3u-expt-c (implies (and (real/rationalp x) (real/rationalp y) (real/rationalp z) (integerp n) (< 0 a) (< (* x y (expt z n)) (- a))) (not (integerp (* (/ x) a (/ y) (expt z (- n)))))) :hints (("Goal" :use (:instance not-integerp-3s (z (expt z n))))) :rule-classes :type-prescription)
not-integerp-3u-expt-dtheorem
(defthm not-integerp-3u-expt-d (implies (and (real/rationalp x) (integerp n1) (real/rationalp y) (integerp n2) (real/rationalp z) (< 0 a) (< (* (expt x n1) (expt y n2) z) (- a))) (not (integerp (* (expt x (- n1)) a (expt y (- n2)) (/ z))))) :hints (("Goal" :use (:instance not-integerp-3s (x (expt x n1)) (y (expt y n2))))) :rule-classes :type-prescription)
not-integerp-3u-expt-etheorem
(defthm not-integerp-3u-expt-e (implies (and (real/rationalp x) (integerp n1) (real/rationalp y) (real/rationalp z) (integerp n2) (< 0 a) (< (* (expt x n1) y (expt z n2)) (- a))) (not (integerp (* (expt x (- n1)) a (/ y) (expt z (- n2)))))) :hints (("Goal" :use (:instance not-integerp-3s (x (expt x n1)) (z (expt z n2))))) :rule-classes :type-prescription)
not-integerp-3u-expt-ftheorem
(defthm not-integerp-3u-expt-f (implies (and (real/rationalp x) (real/rationalp y) (integerp n1) (real/rationalp z) (integerp n2) (< 0 a) (< (* x (expt y n1) (expt z n2)) (- a))) (not (integerp (* (/ x) a (expt y (- n1)) (expt z (- n2)))))) :hints (("Goal" :use (:instance not-integerp-3s (y (expt y n1)) (z (expt z n2))))) :rule-classes :type-prescription)
not-integerp-3u-expt-gtheorem
(defthm not-integerp-3u-expt-g (implies (and (real/rationalp x) (integerp n1) (real/rationalp y) (integerp n2) (real/rationalp z) (integerp n3) (< 0 a) (< (* (expt x n1) (expt y n2) (expt z n3)) (- a))) (not (integerp (* (expt x (- n1)) a (expt y (- n2)) (expt z (- n3)))))) :hints (("Goal" :use (:instance not-integerp-3s (x (expt x n1)) (y (expt y n2)) (z (expt z n3))))) :rule-classes :type-prescription)
local
(local (in-theory (disable not-integerp-3u not-integerp-3u-expt-a not-integerp-3u-expt-b not-integerp-3u-expt-c not-integerp-3u-expt-d not-integerp-3u-expt-e not-integerp-3u-expt-f not-integerp-3u-expt-g)))
not-integerp-3vtheorem
(defthm not-integerp-3v (implies (and (real/rationalp x) (real/rationalp y) (real/rationalp z) (< 0 a) (< (* x y z) (- a))) (not (integerp (* a (/ x) (/ y) (/ z))))) :hints (("Goal" :use (:instance not-integerp-3s))) :rule-classes :type-prescription)
not-integerp-3v-expt-atheorem
(defthm not-integerp-3v-expt-a (implies (and (real/rationalp x) (integerp n) (real/rationalp y) (real/rationalp z) (< 0 a) (< (* (expt x n) y z) (- a))) (not (integerp (* a (expt x (- n)) (/ y) (/ z))))) :hints (("Goal" :use (:instance not-integerp-3s (x (expt x n))))) :rule-classes :type-prescription)
not-integerp-3v-expt-btheorem
(defthm not-integerp-3v-expt-b (implies (and (real/rationalp x) (real/rationalp y) (integerp n) (real/rationalp z) (< 0 a) (< (* x (expt y n) z) (- a))) (not (integerp (* a (/ x) (expt y (- n)) (/ z))))) :hints (("Goal" :use (:instance not-integerp-3s (y (expt y n))))) :rule-classes :type-prescription)
not-integerp-3v-expt-ctheorem
(defthm not-integerp-3v-expt-c (implies (and (real/rationalp x) (real/rationalp y) (real/rationalp z) (integerp n) (< 0 a) (< (* x y (expt z n)) (- a))) (not (integerp (* a (/ x) (/ y) (expt z (- n)))))) :hints (("Goal" :use (:instance not-integerp-3s (z (expt z n))))) :rule-classes :type-prescription)
not-integerp-3v-expt-dtheorem
(defthm not-integerp-3v-expt-d (implies (and (real/rationalp x) (integerp n1) (real/rationalp y) (integerp n2) (real/rationalp z) (< 0 a) (< (* (expt x n1) (expt y n2) z) (- a))) (not (integerp (* a (expt x (- n1)) (expt y (- n2)) (/ z))))) :hints (("Goal" :use (:instance not-integerp-3s (x (expt x n1)) (y (expt y n2))))) :rule-classes :type-prescription)
not-integerp-3v-expt-etheorem
(defthm not-integerp-3v-expt-e (implies (and (real/rationalp x) (integerp n1) (real/rationalp y) (real/rationalp z) (integerp n2) (< 0 a) (< (* (expt x n1) y (expt z n2)) (- a))) (not (integerp (* a (expt x (- n1)) (/ y) (expt z (- n2)))))) :hints (("Goal" :use (:instance not-integerp-3s (x (expt x n1)) (z (expt z n2))))) :rule-classes :type-prescription)
not-integerp-3v-expt-ftheorem
(defthm not-integerp-3v-expt-f (implies (and (real/rationalp x) (real/rationalp y) (integerp n1) (real/rationalp z) (integerp n2) (< 0 a) (< (* x (expt y n1) (expt z n2)) (- a))) (not (integerp (* a (/ x) (expt y (- n1)) (expt z (- n2)))))) :hints (("Goal" :use (:instance not-integerp-3s (y (expt y n1)) (z (expt z n2))))) :rule-classes :type-prescription)
not-integerp-3v-expt-gtheorem
(defthm not-integerp-3v-expt-g (implies (and (real/rationalp x) (integerp n1) (real/rationalp y) (integerp n2) (real/rationalp z) (integerp n3) (< 0 a) (< (* (expt x n1) (expt y n2) (expt z n3)) (- a))) (not (integerp (* a (expt x (- n1)) (expt y (- n2)) (expt z (- n3)))))) :hints (("Goal" :use (:instance not-integerp-3s (x (expt x n1)) (y (expt y n2)) (z (expt z n3))))) :rule-classes :type-prescription)
local
(local (in-theory (disable not-integerp-3v not-integerp-3v-expt-a not-integerp-3v-expt-b not-integerp-3v-expt-c not-integerp-3v-expt-d not-integerp-3v-expt-e not-integerp-3v-expt-f not-integerp-3v-expt-g)))
not-integerp-4atheorem
(defthm not-integerp-4a (implies (and (real/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-4a-expttheorem
(defthm not-integerp-4a-expt (implies (and (real/rationalp x) (integerp n) (< a 0) (< (- a) (expt x n))) (not (integerp (* (expt x (- n)) a)))) :hints (("Goal" :use (:instance not-integerp-4a (x (expt x n))))) :rule-classes :type-prescription)
local
(local (in-theory (disable not-integerp-4a not-integerp-4a-expt)))
not-integerp-4btheorem
(defthm not-integerp-4b (implies (and (real/rationalp x) (< a 0) (< (- a) x)) (not (integerp (* a (/ x))))) :hints (("Goal" :use not-integerp-4a)) :rule-classes :type-prescription)
not-integerp-4b-expttheorem
(defthm not-integerp-4b-expt (implies (and (real/rationalp x) (integerp n) (< a 0) (< (- a) (expt x n))) (not (integerp (* a (expt x (- n)))))) :hints (("Goal" :use (:instance not-integerp-4a (x (expt x n))))) :rule-classes :type-prescription)
local
(local (in-theory (disable not-integerp-4b not-integerp-4b-expt)))
not-integerp-4dtheorem
(defthm not-integerp-4d (implies (and (real/rationalp b) (real/rationalp x) (< (* a b) 0) (< (- (* a b)) x)) (not (integerp (* a (/ x) b)))) :hints (("Goal" :use (:instance not-integerp-4a (a (* a b)) (x x)))) :rule-classes :type-prescription)
not-integerp-4d-expttheorem
(defthm not-integerp-4d-expt (implies (and (real/rationalp b) (real/rationalp x) (integerp n) (< (* a b) 0) (< (- (* a b)) (expt x n))) (not (integerp (* a (expt x (- n)) b)))) :hints (("Goal" :use (:instance not-integerp-4a (a (* a b)) (x (expt x n))))) :rule-classes :type-prescription)
local
(local (in-theory (disable not-integerp-4d not-integerp-4d-expt)))
not-integerp-4etheorem
(defthm not-integerp-4e (implies (and (real/rationalp x) (< (* a b) 0) (< (- (* a b)) x)) (not (integerp (* a b (/ x))))) :hints (("Goal" :use (:instance not-integerp-4a (a (* a b)) (x x)))) :rule-classes :type-prescription)
not-integerp-4e-expttheorem
(defthm not-integerp-4e-expt (implies (and (real/rationalp x) (integerp n) (< (* a b) 0) (< (- (* a b)) (expt x n))) (not (integerp (* a b (expt x (- n)))))) :hints (("Goal" :use (:instance not-integerp-4a (a (* a b)) (x (expt x n))))) :rule-classes :type-prescription)
local
(local (in-theory (disable not-integerp-4e not-integerp-4e-expt)))
not-integerp-4ftheorem
(defthm not-integerp-4f (implies (and (real/rationalp x) (real/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-4f-expt-atheorem
(defthm not-integerp-4f-expt-a (implies (and (real/rationalp x) (integerp n) (real/rationalp y) (< a 0) (< (- a) (* (expt x n) y))) (not (integerp (* (expt x (- n)) (/ y) a)))) :hints (("Goal" :use (:instance not-integerp-4a (a a) (x (* (expt x n) y))))) :rule-classes :type-prescription)
not-integerp-4f-expt-btheorem
(defthm not-integerp-4f-expt-b (implies (and (real/rationalp x) (real/rationalp y) (integerp n) (< a 0) (< (- a) (* x (expt y n)))) (not (integerp (* (/ x) (expt y (- n)) a)))) :hints (("Goal" :use (:instance not-integerp-4a (a a) (x (* (expt y n) x))))) :rule-classes :type-prescription)
not-integerp-4f-expt-ctheorem
(defthm not-integerp-4f-expt-c (implies (and (real/rationalp x) (integerp n1) (real/rationalp y) (integerp n2) (< a 0) (< (- a) (* (expt x n1) (expt y n2)))) (not (integerp (* (expt x (- n1)) (expt y (- n2)) a)))) :hints (("Goal" :use (:instance not-integerp-4a (a a) (x (* (expt x n1) (expt y n2)))))) :rule-classes :type-prescription)
local
(local (in-theory (disable not-integerp-4f not-integerp-4f-expt-a not-integerp-4f-expt-b not-integerp-4f-expt-c)))
not-integerp-4gtheorem
(defthm not-integerp-4g (implies (and (real/rationalp x) (real/rationalp y) (< a 0) (< (- a) (* x y))) (not (integerp (* (/ x) a (/ y))))) :hints (("Goal" :use not-integerp-4f)) :rule-classes :type-prescription)
not-integerp-4g-expt-atheorem
(defthm not-integerp-4g-expt-a (implies (and (real/rationalp x) (integerp n) (real/rationalp y) (< a 0) (< (- a) (* (expt x n) y))) (not (integerp (* (expt x (- n)) a (/ y))))) :hints (("Goal" :use (:instance not-integerp-4f (x (expt x n))))) :rule-classes :type-prescription)
not-integerp-4g-expt-btheorem
(defthm not-integerp-4g-expt-b (implies (and (real/rationalp x) (real/rationalp y) (integerp n) (< a 0) (< (- a) (* x (expt y n)))) (not (integerp (* (/ x) a (expt y (- n)))))) :hints (("Goal" :use (:instance not-integerp-4f (y (expt y n))))) :rule-classes :type-prescription)
not-integerp-4g-expt-ctheorem
(defthm not-integerp-4g-expt-c (implies (and (real/rationalp x) (integerp n1) (real/rationalp y) (integerp n2) (< a 0) (< (- a) (* (expt x n1) (expt y n2)))) (not (integerp (* (expt x (- n1)) a (expt y (- n2)))))) :hints (("Goal" :use (:instance not-integerp-4f (x (expt x n1)) (y (expt y n2))))) :rule-classes :type-prescription)
local
(local (in-theory (disable not-integerp-4g not-integerp-4g-expt-a not-integerp-4g-expt-b not-integerp-4g-expt-c)))
not-integerp-4htheorem
(defthm not-integerp-4h (implies (and (real/rationalp x) (real/rationalp y) (< a 0) (< (- a) (* x y))) (not (integerp (* a (/ x) (/ y))))) :hints (("Goal" :use not-integerp-4f)) :rule-classes :type-prescription)
not-integerp-4h-expt-atheorem
(defthm not-integerp-4h-expt-a (implies (and (real/rationalp x) (integerp n) (real/rationalp y) (< a 0) (< (- a) (* (expt x n) y))) (not (integerp (* a (expt x (- n)) (/ y))))) :hints (("Goal" :use (:instance not-integerp-4f (x (expt x n))))) :rule-classes :type-prescription)
not-integerp-4h-expt-btheorem
(defthm not-integerp-4h-expt-b (implies (and (real/rationalp x) (real/rationalp y) (integerp n) (< a 0) (< (- a) (* x (expt y n)))) (not (integerp (* a (/ x) (expt y (- n)))))) :hints (("Goal" :use (:instance not-integerp-4f (y (expt y n))))) :rule-classes :type-prescription)
not-integerp-4h-expt-ctheorem
(defthm not-integerp-4h-expt-c (implies (and (real/rationalp x) (integerp n1) (real/rationalp y) (integerp n2) (< a 0) (< (- a) (* (expt x n1) (expt y n2)))) (not (integerp (* a (expt x (- n1)) (expt y (- n2)))))) :hints (("Goal" :use (:instance not-integerp-4f (x (expt x n1)) (y (expt y n2))))) :rule-classes :type-prescription)
local
(local (in-theory (disable not-integerp-4h not-integerp-4h-expt-a not-integerp-4h-expt-b not-integerp-4h-expt-c)))
not-integerp-4ktheorem
(defthm not-integerp-4k (implies (and (real/rationalp c) (real/rationalp x) (< (* a b c) 0) (< (- (* a b c)) x)) (not (integerp (* a b (/ x) c)))) :hints (("Goal" :use (:instance not-integerp-4a (a (* a b c)) (x x)))) :rule-classes :type-prescription)
not-integerp-4k-expttheorem
(defthm not-integerp-4k-expt (implies (and (real/rationalp c) (real/rationalp x) (integerp n) (< (* a b c) 0) (< (- (* a b c)) (expt x n))) (not (integerp (* a b (expt x (- n)) c)))) :hints (("Goal" :use (:instance not-integerp-4a (a (* a b c)) (x (expt x n))))) :rule-classes :type-prescription)
local
(local (in-theory (disable not-integerp-4k not-integerp-4k-expt)))
not-integerp-4ltheorem
(defthm not-integerp-4l (implies (and (real/rationalp x) (< (* a b c) 0) (< (- (* a b c)) x)) (not (integerp (* a b c (/ x))))) :hints (("Goal" :use (:instance not-integerp-4a (a (* a b c)) (x x)))) :rule-classes :type-prescription)
not-integerp-4l-expttheorem
(defthm not-integerp-4l-expt (implies (and (real/rationalp x) (integerp n) (< (* a b c) 0) (< (- (* a b c)) (expt x n))) (not (integerp (* a b c (expt x (- n)))))) :hints (("Goal" :use (:instance not-integerp-4a (a (* a b c)) (x (expt x n))))) :rule-classes :type-prescription)
local
(local (in-theory (disable not-integerp-4l not-integerp-4l-expt)))
not-integerp-4ntheorem
(defthm not-integerp-4n (implies (and (real/rationalp x) (real/rationalp y) (< (* a b) 0) (< (- (* a b)) (* x y))) (not (integerp (* (/ x) a (/ y) b)))) :hints (("Goal" :use (:instance not-integerp-4a (a (* a b)) (x (* x y))))) :rule-classes :type-prescription)
not-integerp-4n-expt-atheorem
(defthm not-integerp-4n-expt-a (implies (and (real/rationalp x) (integerp n) (real/rationalp y) (< (* a b) 0) (< (- (* a b)) (* (expt x n) y))) (not (integerp (* (expt x (- n)) a (/ y) b)))) :hints (("Goal" :use (:instance not-integerp-4a (a (* a b)) (x (* (expt x n) y))))) :rule-classes :type-prescription)
not-integerp-4n-expt-btheorem
(defthm not-integerp-4n-expt-b (implies (and (real/rationalp x) (real/rationalp y) (integerp n) (< (* a b) 0) (< (- (* a b)) (* x (expt y n)))) (not (integerp (* (/ x) a (expt y (- n)) b)))) :hints (("Goal" :use (:instance not-integerp-4a (a (* a b)) (x (* x (expt y n)))))) :rule-classes :type-prescription)
not-integerp-4n-expt-ctheorem
(defthm not-integerp-4n-expt-c (implies (and (real/rationalp x) (integerp n1) (real/rationalp y) (integerp n2) (< (* a b) 0) (< (- (* a b)) (* (expt x n1) (expt y n2)))) (not (integerp (* (expt x (- n1)) a (expt y (- n2)) b)))) :hints (("Goal" :use (:instance not-integerp-4a (a (* a b)) (x (* (expt x n1) (expt y n2)))))) :rule-classes :type-prescription)
local
(local (in-theory (disable not-integerp-4n not-integerp-4n-expt-a not-integerp-4n-expt-b not-integerp-4n-expt-c)))
not-integerp-4otheorem
(defthm not-integerp-4o (implies (and (real/rationalp x) (real/rationalp y) (< (* a b) 0) (< (- (* a b)) (* x y))) (not (integerp (* (/ x) a b (/ y))))) :hints (("Goal" :use (:instance not-integerp-4a (a (* a b)) (x (* x y))))) :rule-classes :type-prescription)
not-integerp-4o-expt-atheorem
(defthm not-integerp-4o-expt-a (implies (and (real/rationalp x) (integerp n) (real/rationalp y) (< (* a b) 0) (< (- (* a b)) (* (expt x n) y))) (not (integerp (* (expt x (- n)) a b (/ y))))) :hints (("Goal" :use (:instance not-integerp-4a (a (* a b)) (x (* (expt x n) y))))) :rule-classes :type-prescription)
not-integerp-4o-expt-btheorem
(defthm not-integerp-4o-expt-b (implies (and (real/rationalp x) (real/rationalp y) (integerp n) (< (* a b) 0) (< (- (* a b)) (* x (expt y n)))) (not (integerp (* (/ x) a b (expt y (- n)))))) :hints (("Goal" :use (:instance not-integerp-4a (a (* a b)) (x (* x (expt y n)))))) :rule-classes :type-prescription)
not-integerp-4o-expt-ctheorem
(defthm not-integerp-4o-expt-c (implies (and (real/rationalp x) (integerp n1) (real/rationalp y) (integerp n2) (< (* a b) 0) (< (- (* a b)) (* (expt x n1) (expt y n2)))) (not (integerp (* (expt x (- n1)) a b (expt y (- n2)))))) :hints (("Goal" :use (:instance not-integerp-4a (a (* a b)) (x (* (expt x n1) (expt y n2)))))) :rule-classes :type-prescription)
local
(local (in-theory (disable not-integerp-4o not-integerp-4o-expt-a not-integerp-4o-expt-b not-integerp-4o-expt-c)))
not-integerp-4ptheorem
(defthm not-integerp-4p (implies (and (real/rationalp x) (real/rationalp y) (< (* a b) 0) (< (- (* a b)) (* x y))) (not (integerp (* a (/ x) (/ y) b)))) :hints (("Goal" :use (:instance not-integerp-4a (a (* a b)) (x (* x y))))) :rule-classes :type-prescription)
not-integerp-4p-expt-atheorem
(defthm not-integerp-4p-expt-a (implies (and (real/rationalp x) (integerp n) (real/rationalp y) (< (* a b) 0) (< (- (* a b)) (* (expt x n) y))) (not (integerp (* a (expt x (- n)) (/ y) b)))) :hints (("Goal" :use (:instance not-integerp-4a (a (* a b)) (x (* (expt x n) y))))) :rule-classes :type-prescription)
not-integerp-4p-expt-btheorem
(defthm not-integerp-4p-expt-b (implies (and (real/rationalp x) (real/rationalp y) (integerp n) (< (* a b) 0) (< (- (* a b)) (* x (expt y n)))) (not (integerp (* a (/ x) (expt y (- n)) b)))) :hints (("Goal" :use (:instance not-integerp-4a (a (* a b)) (x (* x (expt y n)))))) :rule-classes :type-prescription)
not-integerp-4p-expt-ctheorem
(defthm not-integerp-4p-expt-c (implies (and (real/rationalp x) (integerp n1) (real/rationalp y) (integerp n2) (< (* a b) 0) (< (- (* a b)) (* (expt x n1) (expt y n2)))) (not (integerp (* a (expt x (- n1)) (expt y (- n2)) b)))) :hints (("Goal" :use (:instance not-integerp-4a (a (* a b)) (x (* (expt x n1) (expt y n2)))))) :rule-classes :type-prescription)
local
(local (in-theory (disable not-integerp-4p not-integerp-4p-expt-a not-integerp-4p-expt-b not-integerp-4p-expt-c)))
not-integerp-4qtheorem
(defthm not-integerp-4q (implies (and (real/rationalp x) (real/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-4q-expt-atheorem
(defthm not-integerp-4q-expt-a (implies (and (real/rationalp x) (integerp n) (real/rationalp y) (< (* a b) 0) (< (- (* a b)) (* (expt x n) y))) (not (integerp (* a (expt x (- n)) b (/ y))))) :hints (("Goal" :use (:instance not-integerp-4a (a (* a b)) (x (* (expt x n) y))))) :rule-classes :type-prescription)
not-integerp-4q-expt-btheorem
(defthm not-integerp-4q-expt-b (implies (and (real/rationalp x) (real/rationalp y) (integerp n) (< (* a b) 0) (< (- (* a b)) (* x (expt y n)))) (not (integerp (* a (/ x) b (expt y (- n)))))) :hints (("Goal" :use (:instance not-integerp-4a (a (* a b)) (x (* x (expt y n)))))) :rule-classes :type-prescription)
not-integerp-4q-expt-ctheorem
(defthm not-integerp-4q-expt-c (implies (and (real/rationalp x) (integerp n1) (real/rationalp y) (integerp n2) (< (* a b) 0) (< (- (* a b)) (* (expt x n1) (expt y n2)))) (not (integerp (* a (expt x (- n1)) b (expt y (- n2)))))) :hints (("Goal" :use (:instance not-integerp-4a (a (* a b)) (x (* (expt x n1) (expt y n2)))))) :rule-classes :type-prescription)
local
(local (in-theory (disable not-integerp-4q not-integerp-4q-expt-a not-integerp-4q-expt-b not-integerp-4q-expt-c)))
not-integerp-4rtheorem
(defthm not-integerp-4r (implies (and (real/rationalp x) (real/rationalp y) (< (* a b) 0) (< (- (* a b)) (* x y))) (not (integerp (* a b (/ x) (/ y))))) :hints (("Goal" :use (:instance not-integerp-4a (a (* a b)) (x (* x y))))) :rule-classes :type-prescription)
not-integerp-4r-expt-atheorem
(defthm not-integerp-4r-expt-a (implies (and (real/rationalp x) (integerp n) (real/rationalp y) (< (* a b) 0) (< (- (* a b)) (* (expt x n) y))) (not (integerp (* a b (expt x (- n)) (/ y))))) :hints (("Goal" :use (:instance not-integerp-4a (a (* a b)) (x (* (expt x n) y))))) :rule-classes :type-prescription)
not-integerp-4r-expt-btheorem
(defthm not-integerp-4r-expt-b (implies (and (real/rationalp x) (real/rationalp y) (integerp n) (< (* a b) 0) (< (- (* a b)) (* x (expt y n)))) (not (integerp (* a b (/ x) (expt y (- n)))))) :hints (("Goal" :use (:instance not-integerp-4a (a (* a b)) (x (* x (expt y n)))))) :rule-classes :type-prescription)
not-integerp-4r-expt-ctheorem
(defthm not-integerp-4r-expt-c (implies (and (real/rationalp x) (integerp n1) (real/rationalp y) (integerp n2) (< (* a b) 0) (< (- (* a b)) (* (expt x n1) (expt y n2)))) (not (integerp (* a b (expt x (- n1)) (expt y (- n2)))))) :hints (("Goal" :use (:instance not-integerp-4a (a (* a b)) (x (* (expt x n1) (expt y n2)))))) :rule-classes :type-prescription)
local
(local (in-theory (disable not-integerp-4r not-integerp-4r-expt-a not-integerp-4r-expt-b not-integerp-4r-expt-c)))
not-integerp-4stheorem
(defthm not-integerp-4s (implies (and (real/rationalp x) (real/rationalp y) (real/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-4s-expt-atheorem
(defthm not-integerp-4s-expt-a (implies (and (real/rationalp x) (integerp n) (real/rationalp y) (real/rationalp z) (< a 0) (< (- a) (* (expt x n) y z))) (not (integerp (* (expt x (- n)) (/ y) (/ z) a)))) :hints (("Goal" :use (:instance not-integerp-4a (a a) (x (* (expt x n) y z))))) :rule-classes :type-prescription)
not-integerp-4s-expt-btheorem
(defthm not-integerp-4s-expt-b (implies (and (real/rationalp x) (real/rationalp y) (integerp n) (real/rationalp z) (< a 0) (< (- a) (* x (expt y n) z))) (not (integerp (* (/ x) (expt y (- n)) (/ z) a)))) :hints (("Goal" :use (:instance not-integerp-4a (a a) (x (* x (expt y n) z))))) :rule-classes :type-prescription)
not-integerp-4s-expt-ctheorem
(defthm not-integerp-4s-expt-c (implies (and (real/rationalp x) (real/rationalp y) (real/rationalp z) (integerp n) (< a 0) (< (- a) (* x y (expt z n)))) (not (integerp (* (/ x) (/ y) (expt z (- n)) a)))) :hints (("Goal" :use (:instance not-integerp-4a (a a) (x (* x y (expt z n)))))) :rule-classes :type-prescription)
not-integerp-4s-expt-dtheorem
(defthm not-integerp-4s-expt-d (implies (and (real/rationalp x) (integerp n1) (real/rationalp y) (integerp n2) (real/rationalp z) (< a 0) (< (- a) (* (expt x n1) (expt y n2) z))) (not (integerp (* (expt x (- n1)) (expt y (- n2)) (/ z) a)))) :hints (("Goal" :use (:instance not-integerp-4a (a a) (x (* (expt x n1) (expt y n2) z))))) :rule-classes :type-prescription)
not-integerp-4s-expt-etheorem
(defthm not-integerp-4s-expt-e (implies (and (real/rationalp x) (integerp n1) (real/rationalp y) (real/rationalp z) (integerp n2) (< a 0) (< (- a) (* (expt x n1) y (expt z n2)))) (not (integerp (* (expt x (- n1)) (/ y) (expt z (- n2)) a)))) :hints (("Goal" :use (:instance not-integerp-4a (a a) (x (* (expt x n1) y (expt z n2)))))) :rule-classes :type-prescription)
not-integerp-4s-expt-ftheorem
(defthm not-integerp-4s-expt-f (implies (and (real/rationalp x) (real/rationalp y) (integerp n1) (real/rationalp z) (integerp n2) (< a 0) (< (- a) (* x (expt y n1) (expt z n2)))) (not (integerp (* (/ x) (expt y (- n1)) (expt z (- n2)) a)))) :hints (("Goal" :use (:instance not-integerp-4a (a a) (x (* x (expt y n1) (expt z n2)))))) :rule-classes :type-prescription)
not-integerp-4s-expt-gtheorem
(defthm not-integerp-4s-expt-g (implies (and (real/rationalp x) (integerp n1) (real/rationalp y) (integerp n2) (real/rationalp z) (integerp n3) (< a 0) (< (- a) (* (expt x n1) (expt y n2) (expt z n3)))) (not (integerp (* (expt x (- n1)) (expt y (- n2)) (expt z (- n3)) a)))) :hints (("Goal" :use (:instance not-integerp-4a (a a) (x (* (expt x n1) (expt y n2) (expt z n3)))))) :rule-classes :type-prescription)
local
(local (in-theory (disable not-integerp-4s not-integerp-4s-expt-a not-integerp-4s-expt-b not-integerp-4s-expt-c not-integerp-4s-expt-d not-integerp-4s-expt-e not-integerp-4s-expt-f not-integerp-4s-expt-g)))
not-integerp-4ttheorem
(defthm not-integerp-4t (implies (and (real/rationalp x) (real/rationalp y) (real/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-4t-expt-atheorem
(defthm not-integerp-4t-expt-a (implies (and (real/rationalp x) (integerp n) (real/rationalp y) (real/rationalp z) (< a 0) (< (- a) (* (expt x n) y z))) (not (integerp (* (expt x (- n)) (/ y) a (/ z))))) :hints (("Goal" :use (:instance not-integerp-4s (x (expt x n))))) :rule-classes :type-prescription)
not-integerp-4t-expt-btheorem
(defthm not-integerp-4t-expt-b (implies (and (real/rationalp x) (real/rationalp y) (integerp n) (real/rationalp z) (< a 0) (< (- a) (* x (expt y n) z))) (not (integerp (* (/ x) (expt y (- n)) a (/ z))))) :hints (("Goal" :use (:instance not-integerp-4s (y (expt y n))))) :rule-classes :type-prescription)
not-integerp-4t-expt-ctheorem
(defthm not-integerp-4t-expt-c (implies (and (real/rationalp x) (real/rationalp y) (real/rationalp z) (integerp n) (< a 0) (< (- a) (* x y (expt z n)))) (not (integerp (* (/ x) (/ y) a (expt z (- n)))))) :hints (("Goal" :use (:instance not-integerp-4s (z (expt z n))))) :rule-classes :type-prescription)
not-integerp-4t-expt-dtheorem
(defthm not-integerp-4t-expt-d (implies (and (real/rationalp x) (integerp n1) (real/rationalp y) (integerp n2) (real/rationalp z) (< a 0) (< (- a) (* (expt x n1) (expt y n2) z))) (not (integerp (* (expt x (- n1)) (expt y (- n2)) a (/ z))))) :hints (("Goal" :use (:instance not-integerp-4s (x (expt x n1)) (y (expt y n2))))) :rule-classes :type-prescription)
not-integerp-4t-expt-etheorem
(defthm not-integerp-4t-expt-e (implies (and (real/rationalp x) (integerp n1) (real/rationalp y) (real/rationalp z) (integerp n2) (< a 0) (< (- a) (* (expt x n1) y (expt z n2)))) (not (integerp (* (expt x (- n1)) (/ y) a (expt z (- n2)))))) :hints (("Goal" :use (:instance not-integerp-4s (x (expt x n1)) (z (expt z n2))))) :rule-classes :type-prescription)
not-integerp-4t-expt-ftheorem
(defthm not-integerp-4t-expt-f (implies (and (real/rationalp x) (real/rationalp y) (integerp n1) (real/rationalp z) (integerp n2) (< a 0) (< (- a) (* x (expt y n1) (expt z n2)))) (not (integerp (* (/ x) (expt y (- n1)) a (expt z (- n2)))))) :hints (("Goal" :use (:instance not-integerp-4s (y (expt y n1)) (z (expt z n2))))) :rule-classes :type-prescription)
not-integerp-4t-expt-gtheorem
(defthm not-integerp-4t-expt-g (implies (and (real/rationalp x) (integerp n1) (real/rationalp y) (integerp n2) (real/rationalp z) (integerp n3) (< a 0) (< (- a) (* (expt x n1) (expt y n2) (expt z n3)))) (not (integerp (* (expt x (- n1)) (expt y (- n2)) a (expt z (- n3)))))) :hints (("Goal" :use (:instance not-integerp-4s (x (expt x n1)) (y (expt y n2)) (z (expt z n3))))) :rule-classes :type-prescription)
local
(local (in-theory (disable not-integerp-4t not-integerp-4t-expt-a not-integerp-4t-expt-b not-integerp-4t-expt-c not-integerp-4t-expt-d not-integerp-4t-expt-e not-integerp-4t-expt-f not-integerp-4t-expt-g)))
not-integerp-4utheorem
(defthm not-integerp-4u (implies (and (real/rationalp x) (real/rationalp y) (real/rationalp z) (< a 0) (< (- a) (* x y z))) (not (integerp (* (/ x) a (/ y) (/ z))))) :hints (("Goal" :use (:instance not-integerp-4s))) :rule-classes :type-prescription)
not-integerp-4u-expt-atheorem
(defthm not-integerp-4u-expt-a (implies (and (real/rationalp x) (integerp n) (real/rationalp y) (real/rationalp z) (< a 0) (< (- a) (* (expt x n) y z))) (not (integerp (* (expt x (- n)) a (/ y) (/ z))))) :hints (("Goal" :use (:instance not-integerp-4s (x (expt x n))))) :rule-classes :type-prescription)
not-integerp-4u-expt-btheorem
(defthm not-integerp-4u-expt-b (implies (and (real/rationalp x) (real/rationalp y) (integerp n) (real/rationalp z) (< a 0) (< (- a) (* x (expt y n) z))) (not (integerp (* (/ x) a (expt y (- n)) (/ z))))) :hints (("Goal" :use (:instance not-integerp-4s (y (expt y n))))) :rule-classes :type-prescription)
not-integerp-4u-expt-ctheorem
(defthm not-integerp-4u-expt-c (implies (and (real/rationalp x) (real/rationalp y) (real/rationalp z) (integerp n) (< a 0) (< (- a) (* x y (expt z n)))) (not (integerp (* (/ x) a (/ y) (expt z (- n)))))) :hints (("Goal" :use (:instance not-integerp-4s (z (expt z n))))) :rule-classes :type-prescription)
not-integerp-4u-expt-dtheorem
(defthm not-integerp-4u-expt-d (implies (and (real/rationalp x) (integerp n1) (real/rationalp y) (integerp n2) (real/rationalp z) (< a 0) (< (- a) (* (expt x n1) (expt y n2) z))) (not (integerp (* (expt x (- n1)) a (expt y (- n2)) (/ z))))) :hints (("Goal" :use (:instance not-integerp-4s (x (expt x n1)) (y (expt y n2))))) :rule-classes :type-prescription)
not-integerp-4u-expt-etheorem
(defthm not-integerp-4u-expt-e (implies (and (real/rationalp x) (integerp n1) (real/rationalp y) (real/rationalp z) (integerp n2) (< a 0) (< (- a) (* (expt x n1) y (expt z n2)))) (not (integerp (* (expt x (- n1)) a (/ y) (expt z (- n2)))))) :hints (("Goal" :use (:instance not-integerp-4s (x (expt x n1)) (z (expt z n2))))) :rule-classes :type-prescription)
not-integerp-4u-expt-ftheorem
(defthm not-integerp-4u-expt-f (implies (and (real/rationalp x) (real/rationalp y) (integerp n1) (real/rationalp z) (integerp n2) (< a 0) (< (- a) (* x (expt y n1) (expt z n2)))) (not (integerp (* (/ x) a (expt y (- n1)) (expt z (- n2)))))) :hints (("Goal" :use (:instance not-integerp-4s (y (expt y n1)) (z (expt z n2))))) :rule-classes :type-prescription)
not-integerp-4u-expt-gtheorem
(defthm not-integerp-4u-expt-g (implies (and (real/rationalp x) (integerp n1) (real/rationalp y) (integerp n2) (real/rationalp z) (integerp n3) (< a 0) (< (- a) (* (expt x n1) (expt y n2) (expt z n3)))) (not (integerp (* (expt x (- n1)) a (expt y (- n2)) (expt z (- n3)))))) :hints (("Goal" :use (:instance not-integerp-4s (x (expt x n1)) (y (expt y n2)) (z (expt z n3))))) :rule-classes :type-prescription)
local
(local (in-theory (disable not-integerp-4u not-integerp-4u-expt-a not-integerp-4u-expt-b not-integerp-4u-expt-c not-integerp-4u-expt-d not-integerp-4u-expt-e not-integerp-4u-expt-f not-integerp-4u-expt-g)))
not-integerp-4vtheorem
(defthm not-integerp-4v (implies (and (real/rationalp x) (real/rationalp y) (real/rationalp z) (< a 0) (< (- a) (* x y z))) (not (integerp (* a (/ x) (/ y) (/ z))))) :hints (("Goal" :use (:instance not-integerp-4s))) :rule-classes :type-prescription)
not-integerp-4v-expt-atheorem
(defthm not-integerp-4v-expt-a (implies (and (real/rationalp x) (integerp n) (real/rationalp y) (real/rationalp z) (< a 0) (< (- a) (* (expt x n) y z))) (not (integerp (* a (expt x (- n)) (/ y) (/ z))))) :hints (("Goal" :use (:instance not-integerp-4s (x (expt x n))))) :rule-classes :type-prescription)
not-integerp-4v-expt-btheorem
(defthm not-integerp-4v-expt-b (implies (and (real/rationalp x) (real/rationalp y) (integerp n) (real/rationalp z) (< a 0) (< (- a) (* x (expt y n) z))) (not (integerp (* a (/ x) (expt y (- n)) (/ z))))) :hints (("Goal" :use (:instance not-integerp-4s (y (expt y n))))) :rule-classes :type-prescription)
not-integerp-4v-expt-ctheorem
(defthm not-integerp-4v-expt-c (implies (and (real/rationalp x) (real/rationalp y) (real/rationalp z) (integerp n) (< a 0) (< (- a) (* x y (expt z n)))) (not (integerp (* a (/ x) (/ y) (expt z (- n)))))) :hints (("Goal" :use (:instance not-integerp-4s (z (expt z n))))) :rule-classes :type-prescription)
not-integerp-4v-expt-dtheorem
(defthm not-integerp-4v-expt-d (implies (and (real/rationalp x) (integerp n1) (real/rationalp y) (integerp n2) (real/rationalp z) (< a 0) (< (- a) (* (expt x n1) (expt y n2) z))) (not (integerp (* a (expt x (- n1)) (expt y (- n2)) (/ z))))) :hints (("Goal" :use (:instance not-integerp-4s (x (expt x n1)) (y (expt y n2))))) :rule-classes :type-prescription)
not-integerp-4v-expt-etheorem
(defthm not-integerp-4v-expt-e (implies (and (real/rationalp x) (integerp n1) (real/rationalp y) (real/rationalp z) (integerp n2) (< a 0) (< (- a) (* (expt x n1) y (expt z n2)))) (not (integerp (* a (expt x (- n1)) (/ y) (expt z (- n2)))))) :hints (("Goal" :use (:instance not-integerp-4s (x (expt x n1)) (z (expt z n2))))) :rule-classes :type-prescription)
not-integerp-4v-expt-ftheorem
(defthm not-integerp-4v-expt-f (implies (and (real/rationalp x) (real/rationalp y) (integerp n1) (real/rationalp z) (integerp n2) (< a 0) (< (- a) (* x (expt y n1) (expt z n2)))) (not (integerp (* a (/ x) (expt y (- n1)) (expt z (- n2)))))) :hints (("Goal" :use (:instance not-integerp-4s (y (expt y n1)) (z (expt z n2))))) :rule-classes :type-prescription)
not-integerp-4v-expt-gtheorem
(defthm not-integerp-4v-expt-g (implies (and (real/rationalp x) (integerp n1) (real/rationalp y) (integerp n2) (real/rationalp z) (integerp n3) (< a 0) (< (- a) (* (expt x n1) (expt y n2) (expt z n3)))) (not (integerp (* a (expt x (- n1)) (expt y (- n2)) (expt z (- n3)))))) :hints (("Goal" :use (:instance not-integerp-4s (x (expt x n1)) (y (expt y n2)) (z (expt z n3))))) :rule-classes :type-prescription)
local
(local (in-theory (disable not-integerp-4v not-integerp-4v-expt-a not-integerp-4v-expt-b not-integerp-4v-expt-c not-integerp-4v-expt-d not-integerp-4v-expt-e not-integerp-4v-expt-f not-integerp-4v-expt-g)))
other
(deftheory not-integerp-type-set-rules '(not-integerp-1a not-integerp-1a-expt not-integerp-1b not-integerp-1b-expt not-integerp-1d not-integerp-1d-expt not-integerp-1e not-integerp-1e-expt not-integerp-1f not-integerp-1f-expt-a not-integerp-1f-expt-b not-integerp-1f-expt-c not-integerp-1g not-integerp-1g-expt-a not-integerp-1g-expt-b not-integerp-1g-expt-c not-integerp-1h not-integerp-1h-expt-a not-integerp-1h-expt-b not-integerp-1h-expt-c not-integerp-1k not-integerp-1k-expt not-integerp-1l not-integerp-1l-expt not-integerp-1n not-integerp-1n-expt-a not-integerp-1n-expt-b not-integerp-1n-expt-c not-integerp-1o not-integerp-1o-expt-a not-integerp-1o-expt-b not-integerp-1o-expt-c not-integerp-1p not-integerp-1p-expt-a not-integerp-1p-expt-b not-integerp-1p-expt-c not-integerp-1q not-integerp-1q-expt-a not-integerp-1q-expt-b not-integerp-1q-expt-c not-integerp-1r not-integerp-1r-expt-a not-integerp-1r-expt-b not-integerp-1r-expt-c not-integerp-1s not-integerp-1s-expt-a not-integerp-1s-expt-b not-integerp-1s-expt-c not-integerp-1s-expt-d not-integerp-1s-expt-e not-integerp-1s-expt-f not-integerp-1s-expt-g not-integerp-1t not-integerp-1t-expt-a not-integerp-1t-expt-b not-integerp-1t-expt-c not-integerp-1t-expt-d not-integerp-1t-expt-e not-integerp-1t-expt-f not-integerp-1t-expt-g not-integerp-1u not-integerp-1u-expt-a not-integerp-1u-expt-b not-integerp-1u-expt-c not-integerp-1u-expt-d not-integerp-1u-expt-e not-integerp-1u-expt-f not-integerp-1u-expt-g not-integerp-1v not-integerp-1v-expt-a not-integerp-1v-expt-b not-integerp-1v-expt-c not-integerp-1v-expt-d not-integerp-1v-expt-e not-integerp-1v-expt-f not-integerp-1v-expt-g not-integerp-2a not-integerp-2a-expt not-integerp-2b not-integerp-2b-expt not-integerp-2d not-integerp-2d-expt not-integerp-2e not-integerp-2e-expt not-integerp-2f not-integerp-2f-expt-a not-integerp-2f-expt-b not-integerp-2f-expt-c not-integerp-2g not-integerp-2g-expt-a not-integerp-2g-expt-b not-integerp-2g-expt-c not-integerp-2h not-integerp-2h-expt-a not-integerp-2h-expt-b not-integerp-2h-expt-c not-integerp-2k not-integerp-2k-expt not-integerp-2l not-integerp-2l-expt not-integerp-2n not-integerp-2n-expt-a not-integerp-2n-expt-b not-integerp-2n-expt-c not-integerp-2o not-integerp-2o-expt-a not-integerp-2o-expt-b not-integerp-2o-expt-c not-integerp-2p not-integerp-2p-expt-a not-integerp-2p-expt-b not-integerp-2p-expt-c not-integerp-2q not-integerp-2q-expt-a not-integerp-2q-expt-b not-integerp-2q-expt-c not-integerp-2r not-integerp-2r-expt-a not-integerp-2r-expt-b not-integerp-2r-expt-c not-integerp-2s not-integerp-2s-expt-a not-integerp-2s-expt-b not-integerp-2s-expt-c not-integerp-2s-expt-d not-integerp-2s-expt-e not-integerp-2s-expt-f not-integerp-2s-expt-g not-integerp-2t not-integerp-2t-expt-a not-integerp-2t-expt-b not-integerp-2t-expt-c not-integerp-2t-expt-d not-integerp-2t-expt-e not-integerp-2t-expt-f not-integerp-2t-expt-g not-integerp-2u not-integerp-2u-expt-a not-integerp-2u-expt-b not-integerp-2u-expt-c not-integerp-2u-expt-d not-integerp-2u-expt-e not-integerp-2u-expt-f not-integerp-2u-expt-g not-integerp-2v not-integerp-2v-expt-a not-integerp-2v-expt-b not-integerp-2v-expt-c not-integerp-2v-expt-d not-integerp-2v-expt-e not-integerp-2v-expt-f not-integerp-2v-expt-g not-integerp-3a not-integerp-3a-expt not-integerp-3b not-integerp-3b-expt not-integerp-3d not-integerp-3d-expt not-integerp-3e not-integerp-3e-expt not-integerp-3f not-integerp-3f-expt-a not-integerp-3f-expt-b not-integerp-3f-expt-c not-integerp-3g not-integerp-3g-expt-a not-integerp-3g-expt-b not-integerp-3g-expt-c not-integerp-3h not-integerp-3h-expt-a not-integerp-3h-expt-b not-integerp-3h-expt-c not-integerp-3k not-integerp-3k-expt not-integerp-3l not-integerp-3l-expt not-integerp-3n not-integerp-3n-expt-a not-integerp-3n-expt-b not-integerp-3n-expt-c not-integerp-3o not-integerp-3o-expt-a not-integerp-3o-expt-b not-integerp-3o-expt-c not-integerp-3p not-integerp-3p-expt-a not-integerp-3p-expt-b not-integerp-3p-expt-c not-integerp-3q not-integerp-3q-expt-a not-integerp-3q-expt-b not-integerp-3q-expt-c not-integerp-3r not-integerp-3r-expt-a not-integerp-3r-expt-b not-integerp-3r-expt-c not-integerp-3s not-integerp-3s-expt-a not-integerp-3s-expt-b not-integerp-3s-expt-c not-integerp-3s-expt-d not-integerp-3s-expt-e not-integerp-3s-expt-f not-integerp-3s-expt-g not-integerp-3t not-integerp-3t-expt-a not-integerp-3t-expt-b not-integerp-3t-expt-c not-integerp-3t-expt-d not-integerp-3t-expt-e not-integerp-3t-expt-f not-integerp-3t-expt-g not-integerp-3u not-integerp-3u-expt-a not-integerp-3u-expt-b not-integerp-3u-expt-c not-integerp-3u-expt-d not-integerp-3u-expt-e not-integerp-3u-expt-f not-integerp-3u-expt-g not-integerp-3v not-integerp-3v-expt-a not-integerp-3v-expt-b not-integerp-3v-expt-c not-integerp-3v-expt-d not-integerp-3v-expt-e not-integerp-3v-expt-f not-integerp-3v-expt-g not-integerp-4a not-integerp-4a-expt not-integerp-4b not-integerp-4b-expt not-integerp-4d not-integerp-4d-expt not-integerp-4e not-integerp-4e-expt not-integerp-4f not-integerp-4f-expt-a not-integerp-4f-expt-b not-integerp-4f-expt-c not-integerp-4g not-integerp-4g-expt-a not-integerp-4g-expt-b not-integerp-4g-expt-c not-integerp-4h not-integerp-4h-expt-a not-integerp-4h-expt-b not-integerp-4h-expt-c not-integerp-4k not-integerp-4k-expt not-integerp-4l not-integerp-4l-expt not-integerp-4n not-integerp-4n-expt-a not-integerp-4n-expt-b not-integerp-4n-expt-c not-integerp-4o not-integerp-4o-expt-a not-integerp-4o-expt-b not-integerp-4o-expt-c not-integerp-4p not-integerp-4p-expt-a not-integerp-4p-expt-b not-integerp-4p-expt-c not-integerp-4q not-integerp-4q-expt-a not-integerp-4q-expt-b not-integerp-4q-expt-c not-integerp-4r not-integerp-4r-expt-a not-integerp-4r-expt-b not-integerp-4r-expt-c not-integerp-4s not-integerp-4s-expt-a not-integerp-4s-expt-b not-integerp-4s-expt-c not-integerp-4s-expt-d not-integerp-4s-expt-e not-integerp-4s-expt-f not-integerp-4s-expt-g not-integerp-4t not-integerp-4t-expt-a not-integerp-4t-expt-b not-integerp-4t-expt-c not-integerp-4t-expt-d not-integerp-4t-expt-e not-integerp-4t-expt-f not-integerp-4t-expt-g not-integerp-4u not-integerp-4u-expt-a not-integerp-4u-expt-b not-integerp-4u-expt-c not-integerp-4u-expt-d not-integerp-4u-expt-e not-integerp-4u-expt-f not-integerp-4u-expt-g not-integerp-4v not-integerp-4v-expt-a not-integerp-4v-expt-b not-integerp-4v-expt-c not-integerp-4v-expt-d not-integerp-4v-expt-e not-integerp-4v-expt-f not-integerp-4v-expt-g))
reduce-integerp-+-fn-1function
(defun reduce-integerp-+-fn-1 (x intp-flag mfc state) (declare (xargs :guard (eq (fn-symb x) 'binary-+))) (cond ((and (not (equal (arg1 x) ''0)) (if intp-flag (proveably-integer 'x `((x . ,(ARG1 X))) mfc state) (proveably-real/rational 'x `((x . ,(ARG1 X))) mfc state)) (stable-under-rewriting-sums (negate-match (arg1 x)) mfc state)) (list (cons 'z (negate-match (arg1 x))))) ((eq (fn-symb (arg2 x)) 'binary-+) (reduce-integerp-+-fn-1 (arg2 x) intp-flag mfc state)) ((and (not (equal (arg2 x) ''0)) (if intp-flag (proveably-integer 'x `((x . ,(ARG2 X))) mfc state) (proveably-real/rational 'x `((x . ,(ARG2 X))) mfc state)) (stable-under-rewriting-sums (negate-match (arg2 x)) mfc state)) (list (cons 'z (negate-match (arg2 x))))) (t nil)))
reduce-integerp-+-fnfunction
(defun reduce-integerp-+-fn (x intp-flag mfc state) (declare (xargs :guard t)) (if (eq (fn-symb x) 'binary-+) (reduce-integerp-+-fn-1 x intp-flag mfc state) nil))
local
(local (defthm iff-integerp (equal (equal (integerp x) (integerp y)) (iff (integerp x) (integerp y)))))
local
(local (defthm iff-rationalp (equal (equal (real/rationalp x) (real/rationalp y)) (iff (real/rationalp x) (real/rationalp y)))))
reduce-integerp-+theorem
(defthm reduce-integerp-+ (implies (and (syntaxp (rewriting-goal-literal x mfc state)) (syntaxp (in-term-order-+ x mfc state)) (bind-free (reduce-integerp-+-fn x t mfc state) (z)) (integerp z) (acl2-numberp x)) (equal (integerp x) (integerp (+ z x)))))
reduce-rationalp-+theorem
(defthm reduce-rationalp-+ (implies (and (syntaxp (rewriting-goal-literal x mfc state)) (syntaxp (in-term-order-+ x mfc state)) (bind-free (reduce-integerp-+-fn x nil mfc state) (z)) (rationalp z) (acl2-numberp x)) (equal (real/rationalp x) (real/rationalp (+ z x)))))
reduce-rationalp-*-fn-1function
(defun reduce-rationalp-*-fn-1 (x mfc state) (declare (xargs :guard (eq (fn-symb x) 'binary-*))) (cond ((and (not (equal (arg1 x) ''1)) (proveably-non-zero-rational 'x `((x . ,(ARG1 X))) mfc state) (stable-under-rewriting-products (invert-match (arg1 x)) mfc state)) (list (cons 'z (invert-match (arg1 x))))) ((eq (fn-symb (arg2 x)) 'binary-*) (reduce-rationalp-*-fn-1 (arg2 x) mfc state)) ((and (not (equal (arg2 x) ''1)) (proveably-non-zero-rational 'x `((x . ,(ARG2 X))) mfc state) (stable-under-rewriting-products (invert-match (arg2 x)) mfc state)) (list (cons 'z (invert-match (arg2 x))))) (t nil)))
reduce-rationalp-*-fnfunction
(defun reduce-rationalp-*-fn (x mfc state) (declare (xargs :guard t)) (if (eq (fn-symb x) 'binary-*) (reduce-rationalp-*-fn-1 x mfc state) nil))
reduce-rationalp-*theorem
(defthm reduce-rationalp-* (implies (and (syntaxp (rewriting-goal-literal x mfc state)) (syntaxp (in-term-order-* x mfc state)) (bind-free (reduce-rationalp-*-fn x mfc state) (z)) (rationalp z) (not (equal z 0)) (acl2-numberp x)) (equal (real/rationalp x) (real/rationalp (* z x)))))
integerp-minus-xtheorem
(defthm integerp-minus-x (implies (and (syntaxp (weak-mostly-negative-addends-p x mfc state)) (acl2-numberp x)) (equal (integerp x) (integerp (- x)))))
rationalp-minus-xtheorem
(defthm rationalp-minus-x (implies (and (syntaxp (weak-mostly-negative-addends-p x mfc state)) (acl2-numberp x)) (equal (real/rationalp x) (real/rationalp (- x)))))
local
(local (defthm integerp-helper (implies (integerp x) (equal (integerp (+ y z x)) (integerp (+ y z))))))
integerp-+-reduce-constanttheorem
(defthm integerp-+-reduce-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-alternatetheorem
(defthm even-and-odd-alternate (implies (acl2-numberp x) (equal (integerp (+ 1/2 x)) (and (integerp (* 2 x)) (not (integerp x))))))
sum-is-eventheorem
(defthm sum-is-even (implies (and (syntaxp (rewriting-goal-literal x mfc state)) (integerp x) (integerp y)) (equal (integerp (+ (* 1/2 x) (* 1/2 y))) (if (integerp (* 1/2 x)) (integerp (* 1/2 y)) (not (integerp (* 1/2 y)))))) :rule-classes ((:rewrite) (:rewrite :corollary (implies (and (integerp x) (integerp y) (not (integerp (* 1/2 x))) (not (integerp (* 1/2 y)))) (integerp (+ (* 1/2 x) (* 1/2 y)))))))