mod

other

(in-package "ACL2")

flfunction

(defun fl
  (x)
  (declare (xargs :guard (real/rationalp x)))
  (floor x 1))

include-book

(include-book "ground-zero")

include-book

(include-book "negative-syntaxp")

local

(local (include-book "mod-proofs"))

mod-acl2-numberp-type-prescriptiontheorem

(defthmd mod-acl2-numberp-type-prescription
  (acl2-numberp (mod x y))
  :rule-classes (:type-prescription))

mod-acl2-numberptheorem

(defthm mod-acl2-numberp (acl2-numberp (mod x y)))

mod-rationalptheorem

(defthm mod-rationalp
  (implies (case-split (not (complex-rationalp x)))
    (rationalp (mod x y)))
  :rule-classes (:rewrite :type-prescription))

mod-rational-when-y-is-rational-rewritetheorem

(defthm mod-rational-when-y-is-rational-rewrite
  (implies (and (rationalp y) (case-split (acl2-numberp x)))
    (equal (rationalp (mod x y)) (rationalp x))))

mod-integerptheorem

(defthm mod-integerp
  (implies (and (integerp x) (integerp y))
    (integerp (mod x y)))
  :rule-classes (:rewrite :type-prescription))

mod-integerp-2theorem

(defthm mod-integerp-2
  (implies (and (integerp y) (case-split (acl2-numberp x)))
    (equal (integerp (mod x y)) (integerp x))))

mod-with-x-a-non-acl2-number-is-zerotheorem

(defthm mod-with-x-a-non-acl2-number-is-zero
  (implies (not (acl2-numberp x)) (equal (mod x y) 0)))

mod-when-y-is-not-an-acl2-numberptheorem

(defthmd mod-when-y-is-not-an-acl2-numberp
  (implies (not (acl2-numberp y)) (equal (mod x y) (fix x))))

mod-when-y-is-complex-rationalptheorem

(defthmd mod-when-y-is-complex-rationalp
  (implies (complex-rationalp y)
    (equal (mod x y)
      (if (not (complex-rationalp x))
        (fix x)
        (if (not (rationalp (/ x y)))
          x
          (if (integerp (/ x y))
            0
            (+ x (* -1 y (floor (* x (/ y)) 1)))))))))

mod-non-negativetheorem

(defthm mod-non-negative
  (implies (and (case-split (< 0 y))
      (case-split (not (complex-rationalp x)))
      (case-split (not (complex-rationalp y))))
    (<= 0 (mod x y))))

mod-non-negative-rationalp-type-prescriptiontheorem

(defthm mod-non-negative-rationalp-type-prescription
  (implies (and (case-split (< 0 y))
      (case-split (not (complex-rationalp x)))
      (case-split (not (complex-rationalp y))))
    (and (<= 0 (mod x y)) (rationalp (mod x y))))
  :rule-classes ((:type-prescription :typed-term (mod x y))))

mod-non-negative-lineartheorem

(defthm mod-non-negative-linear
  (implies (and (case-split (< 0 y))
      (case-split (not (complex-rationalp x)))
      (case-split (not (complex-rationalp y))))
    (<= 0 (mod x y)))
  :rule-classes ((:linear :trigger-terms ((mod x y)))))

mod-upper-boundtheorem

(defthm mod-upper-bound
  (implies (and (case-split (< 0 y))
      (case-split (not (complex-rationalp x)))
      (case-split (not (complex-rationalp y))))
    (< (mod x y) y)))

mod-upper-bound-lineartheorem

(defthm mod-upper-bound-linear
  (implies (and (case-split (< 0 y))
      (case-split (not (complex-rationalp x)))
      (case-split (not (complex-rationalp y))))
    (< (mod x y) y))
  :rule-classes ((:linear :trigger-terms ((mod x y)))))

mod-upper-bound-less-tight-rewritetheorem

(defthm mod-upper-bound-less-tight-rewrite
  (implies (and (case-split (< 0 y))
      (case-split (not (complex-rationalp x)))
      (case-split (not (complex-rationalp y))))
    (<= (mod x y) y)))

mod-upper-bound-3theorem

(defthm mod-upper-bound-3
  (implies (and (<= y z)
      (case-split (< 0 y))
      (case-split (not (complex-rationalp x)))
      (case-split (not (complex-rationalp y))))
    (< (mod x y) z)))

mod-upper-bound-2theorem

(defthm mod-upper-bound-2
  (implies (and (<= 0 x) (case-split (not (complex-rationalp x))))
    (<= (mod x y) x))
  :rule-classes (:rewrite (:linear :trigger-terms ((mod x y)))))

mod-0theorem

(defthm mod-0
  (and (equal (mod 0 y) 0) (equal (mod x 0) (fix x))))

mod-complex-rationalp-rewritetheorem

(defthm mod-complex-rationalp-rewrite
  (implies (case-split (rationalp y))
    (equal (complex-rationalp (mod x y)) (complex-rationalp x))))

mod-non-positive-type-prescriptiontheorem

(defthm mod-non-positive-type-prescription
  (implies (and (< y 0) (rationalp x) (rationalp y))
    (and (rationalp (mod x y)) (<= (mod x y) 0)))
  :rule-classes (:type-prescription))

mod-non-positivetheorem

(defthm mod-non-positive
  (implies (and (< y 0)
      (case-split (rationalp x))
      (case-split (rationalp y)))
    (<= (mod x y) 0)))

local

(local (include-book "fl"))

mod-drop-irrelevant-first-termtheorem

(defthm mod-drop-irrelevant-first-term
  (implies (and (integerp (* k (/ y)))
      (case-split (not (equal y 0)))
      (case-split (rationalp y))
      (case-split (not (complex-rationalp x))))
    (equal (mod (+ k x) y) (mod x y))))

mod-drop-irrelevant-second-termtheorem

(defthm mod-drop-irrelevant-second-term
  (implies (and (integerp (* k (/ y)))
      (case-split (not (equal y 0)))
      (case-split (rationalp y))
      (case-split (not (complex-rationalp x))))
    (equal (mod (+ x k) y) (mod x y))))

mod-drop-irrelevant-second-term-with-more-termstheorem

(defthm mod-drop-irrelevant-second-term-with-more-terms
  (implies (and (integerp (* k (/ y)))
      (case-split (not (equal y 0)))
      (case-split (rationalp y))
      (case-split (not (complex-rationalp x)))
      (case-split (not (complex-rationalp x2))))
    (equal (mod (+ x k x2) y) (mod (+ x x2) y))))

mod-drop-irrelevant-third-termtheorem

(defthm mod-drop-irrelevant-third-term
  (implies (and (integerp (* k (/ y)))
      (case-split (not (equal y 0)))
      (case-split (rationalp y))
      (case-split (not (complex-rationalp x)))
      (case-split (not (complex-rationalp x2))))
    (equal (mod (+ x x2 k) y) (mod (+ x x2) y))))

mod-mult-erictheorem

(defthm mod-mult-eric
  (implies (and (integerp a)
      (case-split (not (complex-rationalp x)))
      (case-split (not (complex-rationalp y))))
    (equal (mod (+ x (* a y)) y) (mod x y))))

mod-sum-elim-secondtheorem

(defthm mod-sum-elim-second
  (implies (and (case-split (not (complex-rationalp x1)))
      (case-split (not (complex-rationalp x2))))
    (equal (mod (+ x1 (mod x2 y)) y) (mod (+ x1 x2) y))))

mod-sum-elim-second-gentheorem

(defthm mod-sum-elim-second-gen
  (implies (and (integerp (/ y2 y))
      (case-split (not (complex-rationalp x1)))
      (case-split (not (complex-rationalp x2)))
      (case-split (not (equal y 0)))
      (case-split (rationalp y)))
    (equal (mod (+ x1 (mod x2 y2)) y) (mod (+ x1 x2) y))))

mod-sum-elim-firsttheorem

(defthm mod-sum-elim-first
  (implies (and (case-split (not (complex-rationalp a)))
      (case-split (not (complex-rationalp b))))
    (equal (mod (+ (mod b y) a) y) (mod (+ a b) y))))

mod-sum-elim-first-gentheorem

(defthm mod-sum-elim-first-gen
  (implies (and (integerp (/ y2 y))
      (case-split (not (complex-rationalp x1)))
      (case-split (not (complex-rationalp x2)))
      (case-split (not (equal y 0)))
      (case-split (rationalp y)))
    (equal (mod (+ (mod x2 y2) x1) y) (mod (+ x1 x2) y))))

mod-sum-elim-boththeorem

(defthm mod-sum-elim-both
  (implies (and (case-split (not (complex-rationalp a)))
      (case-split (not (complex-rationalp b))))
    (equal (mod (+ (mod a y) (mod b y)) y) (mod (+ a b) y))))

mod-difference-elim-secondtheorem

(defthm mod-difference-elim-second
  (implies (and (case-split (rationalp x1))
      (case-split (rationalp x2)))
    (equal (mod (+ x1 (* -1 (mod x2 y))) y)
      (mod (+ x1 (* -1 x2)) y))))

mod-sum-elim-negative-first-argtheorem

(defthm mod-sum-elim-negative-first-arg
  (implies (and (case-split (rationalp x1))
      (case-split (rationalp x2)))
    (equal (mod (+ (* -1 (mod x2 y)) x1) y)
      (mod (+ (* -1 x2) x1) y))))

mod-by-1theorem

(defthm mod-by-1 (implies (integerp m) (equal (mod m 1) 0)))

mod-mult-of-ntheorem

(defthmd mod-mult-of-n
  (implies (and (integerp (* x (/ y)))
      (not (equal y 0))
      (rationalp x)
      (rationalp y))
    (equal (mod x y) 0)))

mod-negative-ytheorem

(defthmd mod-negative-y
  (implies (and (< 0 y) (integerp x) (integerp y))
    (equal (mod x (- y))
      (if (integerp (/ x y))
        0
        (+ (- y) (mod x y))))))

mod-does-nothingtheorem

(defthm mod-does-nothing
  (implies (and (< m n) (<= 0 m) (case-split (rationalp m)))
    (equal (mod m n) m)))

mod-mod-etheorem

(defthm mod-mod-e
  (implies (and (integerp (/ y1 y2))
      (case-split (not (equal y2 0)))
      (case-split (rationalp y1))
      (case-split (rationalp y2)))
    (equal (mod (mod x y1) y2) (mod x y2))))

mod-of-modtheorem

(defthm mod-of-mod
  (implies (and (case-split (natp k)) (case-split (natp n)))
    (equal (mod (mod x (* k n)) n) (mod x n))))

mod-idempotenttheorem

(defthm mod-idempotent
  (implies (and (case-split (rationalp x)) (case-split (rationalp y)))
    (equal (mod (mod x y) y) (mod x y))))

mod-fl-2theorem

(defthm mod-fl-2
  (implies (case-split (acl2-numberp x))
    (equal (+ (* y (fl (/ x y))) (mod x y)) x))
  :rule-classes nil)

mod-deftheorem

(defthm mod-def
  (implies (case-split (acl2-numberp x))
    (equal (mod x y) (- x (* y (fl (/ x y))))))
  :rule-classes nil)

quot-modtheorem

(defthm quot-mod
  (implies (case-split (acl2-numberp m))
    (equal (+ (* n (fl (/ m n))) (mod m n)) m))
  :rule-classes nil)

mod-force-erictheorem

(defthmd mod-force-eric
  (implies (and (<= (* a y) x)
      (< x (* (1+ a) y))
      (integerp a)
      (rationalp x)
      (rationalp y))
    (equal (mod x y) (- x (* a y)))))

mod-force-chosen-a-negtheorem

(defthmd mod-force-chosen-a-neg
  (implies (and (< x 0) (<= (* -1 y) x) (rationalp x) (rationalp y))
    (equal (mod x y) (- x (* -1 y)))))

mod-eventheorem

(defthm mod-even
  (implies (rationalp x)
    (equal (integerp (* 1/2 (mod x 2))) (integerp (* 1/2 x)))))

mod-even-gentheorem

(defthm mod-even-gen
  (implies (and (rationalp x) (integerp n) (integerp (* 1/2 n)))
    (equal (integerp (* 1/2 (mod x n))) (integerp (* 1/2 x)))))

mod-canceltheorem

(defthmd mod-cancel
  (implies (syntaxp (not (and (quotep y) (equal (cadr y) 1))))
    (equal (mod x y)
      (if (acl2-numberp x)
        (if (acl2-numberp y)
          (if (equal 0 y)
            x
            (* y (mod (/ x y) 1)))
          x)
        0))))

mod-minustheorem

(defthmd mod-minus
  (implies (and (case-split (rationalp x)) (case-split (rationalp y)))
    (equal (mod (* -1 x) y)
      (if (equal 0 y)
        (- x)
        (if (integerp (/ x y))
          0
          (- y (mod x y)))))))

mod-minus-alttheorem

(defthm mod-minus-alt
  (implies (and (syntaxp (negative-syntaxp x))
      (case-split (rationalp x))
      (case-split (rationalp y)))
    (equal (mod x y)
      (if (equal 0 y)
        x
        (if (integerp (/ (- x) y))
          0
          (- y (mod (- x) y)))))))

mod-1-integerptheorem

(defthm mod-1-integerp
  (implies (case-split (acl2-numberp x))
    (equal (integerp (mod x 1)) (integerp x))))

mod-by-2-rewrite-to-eventheorem

(defthmd mod-by-2-rewrite-to-even
  (implies (integerp x)
    (equal (equal (mod x 2) 0) (integerp (* 1/2 x)))))

fl-plus-mdtheorem

(defthm fl-plus-md
  (implies (rationalp x) (equal (+ (fl x) (mod x 1)) x)))

mod-1-sum-integertheorem

(defthm mod-1-sum-integer
  (implies (and (rationalp x) (rationalp y))
    (equal (integerp (+ x (mod y 1))) (integerp (+ x y)))))

mod-quotient-integerptheorem

(defthm mod-quotient-integerp
  (implies (and (integerp (* y k))
      (rationalp x)
      (rationalp y)
      (rationalp k))
    (equal (integerp (* k (mod x y))) (integerp (* k x)))))

mod-mod-2-thmtheorem

(defthm mod-mod-2-thm
  (implies (and (<= y1 y2)
      (case-split (< 0 y1))
      (case-split (acl2-numberp x))
      (case-split (rationalp y1))
      (case-split (rationalp y2))
      (case-split (not (equal y1 0))))
    (equal (mod (mod x y1) y2) (mod x y1))))

mod-equal-0theorem

(defthmd mod-equal-0
  (implies (and (case-split (rationalp y))
      (case-split (not (equal y 0))))
    (equal (equal (mod x y) 0) (integerp (* (/ y) x)))))

mod-2-1-means-oddtheorem

(defthmd mod-2-1-means-odd
  (implies (integerp x)
    (equal (equal (mod x 2) 1) (not (integerp (* 1/2 x))))))

mod-integerp-2-2theorem

(defthm mod-integerp-2-2
  (implies (and (integerp y) (integerp x))
    (integerp (mod x (/ y)))))

mod-cancel-special-1theorem

(defthm mod-cancel-special-1
  (implies (and (acl2-numberp x)
      (rationalp k)
      (acl2-numberp y)
      (not (equal y 0))
      (not (equal k 0)))
    (equal (mod (* k x) (* y k)) (* k (mod x y)))))

mod-integerp-when-y-is-an-inversetheorem

(defthm mod-integerp-when-y-is-an-inverse
  (implies (and (integerp (/ y)) (integerp x))
    (integerp (mod x y))))

mod-when-y-is-an-inversetheorem

(defthm mod-when-y-is-an-inverse
  (implies (and (integerp (/ y)) (integerp x) (case-split (< 0 y)))
    (equal (mod x y) 0)))

fl-mod-x-1theorem

(defthm fl-mod-x-1 (equal (fl (mod x 1)) 0))

mod-by-2theorem

(defthmd mod-by-2
  (implies (integerp x)
    (equal (mod x 2)
      (if (integerp (* 1/2 x))
        0
        1))))

mod-sum-movetheorem

(defthm mod-sum-move
  (implies (and (case-split (<= 0 k1))
      (case-split (< k1 y))
      (case-split (rationalp y))
      (case-split (rationalp x))
      (case-split (rationalp k1)))
    (equal (equal k1 (mod (+ k2 x) y))
      (equal (mod (+ k1 (- k2)) y) (mod x y))))
  :rule-classes nil)

mod-sum-move-constantstheorem

(defthm mod-sum-move-constants
  (implies (and (syntaxp (and (quotep k1) (quotep k2)))
      (case-split (<= 0 k1))
      (case-split (< k1 y))
      (rationalp y)
      (rationalp x)
      (rationalp k1))
    (equal (equal k1 (mod (+ k2 x) y))
      (equal (mod (+ k1 (- k2)) y) (mod x y)))))

mod-sums-cancel-1theorem

(defthm mod-sums-cancel-1
  (implies (and (case-split (<= 0 y))
      (case-split (rationalp k))
      (case-split (rationalp y))
      (case-split (rationalp x1))
      (case-split (rationalp x2)))
    (equal (equal (mod (+ k x1) y) (mod (+ k x2) y))
      (equal (mod x1 y) (mod x2 y)))))

mod-sums-cancel-2theorem

(defthm mod-sums-cancel-2
  (implies (and (case-split (<= 0 y))
      (case-split (rationalp k))
      (case-split (rationalp y))
      (case-split (rationalp x1))
      (case-split (rationalp x2)))
    (equal (equal (mod (+ x1 k) y) (mod (+ k x2) y))
      (equal (mod x1 y) (mod x2 y)))))

mod-sums-cancel-3theorem

(defthm mod-sums-cancel-3
  (implies (and (case-split (<= 0 y))
      (case-split (rationalp k))
      (case-split (rationalp y))
      (case-split (rationalp x1))
      (case-split (rationalp x2)))
    (equal (equal (mod (+ x1 k) y) (mod (+ x2 k) y))
      (equal (mod x1 y) (mod x2 y)))))

mod-sums-cancel-4theorem

(defthm mod-sums-cancel-4
  (implies (and (case-split (<= 0 y))
      (case-split (rationalp k))
      (case-split (rationalp y))
      (case-split (rationalp x1))
      (case-split (rationalp x2)))
    (equal (equal (mod (+ k x1) y) (mod (+ x2 k) y))
      (equal (mod x1 y) (mod x2 y)))))

mod-sums-cancel-5theorem

(defthm mod-sums-cancel-5
  (implies (and (case-split (<= 0 y))
      (case-split (rationalp k))
      (case-split (rationalp y))
      (case-split (rationalp x)))
    (equal (equal (mod k y) (mod (+ x k) y))
      (equal 0 (mod x y)))))

mod-sums-cancel-6theorem

(defthm mod-sums-cancel-6
  (implies (and (case-split (<= 0 y))
      (case-split (rationalp k))
      (case-split (rationalp y))
      (case-split (rationalp x)))
    (equal (equal (mod k y) (mod (+ k x) y))
      (equal 0 (mod x y)))))

mod-sums-cancel-7theorem

(defthm mod-sums-cancel-7
  (implies (and (case-split (<= 0 y))
      (case-split (rationalp k))
      (case-split (rationalp y))
      (case-split (rationalp x)))
    (equal (equal (mod (+ k x) y) (mod k y))
      (equal 0 (mod x y)))))

mod-sums-cancel-8theorem

(defthm mod-sums-cancel-8
  (implies (and (case-split (<= 0 y))
      (case-split (rationalp k))
      (case-split (rationalp y))
      (case-split (rationalp x)))
    (equal (equal (mod (+ x k) y) (mod k y))
      (equal 0 (mod x y)))))

fl-mod-equaltheorem

(defthm fl-mod-equal
  (implies (and (equal (fl (/ x 2)) (fl (/ y 2)))
      (equal (mod x 2) (mod y 2))
      (acl2-numberp x)
      (acl2-numberp y))
    (equal x y))
  :rule-classes nil)

natpfunction

(defun natp
  (x)
  (declare (xargs :guard t))
  (and (integerp x) (<= 0 x)))

mod-bnd-1theorem

(defthmd mod-bnd-1
  (implies (and (case-split (< 0 n))
      (case-split (not (complex-rationalp m)))
      (case-split (not (complex-rationalp n))))
    (< (mod m n) n))
  :rule-classes :linear)

mod-mult-erictheorem

(defthm mod-mult-eric
  (implies (and (integerp a)
      (case-split (not (complex-rationalp x)))
      (case-split (not (complex-rationalp y))))
    (equal (mod (+ x (* a y)) y) (mod x y))))

integerp-modtheorem

(defthm integerp-mod
  (implies (and (integerp m) (integerp n))
    (integerp (mod m n)))
  :rule-classes (:rewrite :type-prescription))

rationalp-modtheorem

(defthm rationalp-mod
  (implies (rationalp x) (rationalp (mod x y)))
  :rule-classes (:rewrite :type-prescription))

rationalp-mod-case-splittheorem

(defthm rationalp-mod-case-split
  (implies (case-split (rationalp x)) (rationalp (mod x y)))
  :rule-classes (:rewrite :type-prescription)
  :hints (("Goal" :in-theory (enable mod))))

in-theory

(in-theory (disable rationalp-mod))

mod-0-fltheorem

(defthm mod-0-fl
  (implies (acl2-numberp m)
    (iff (= (mod m n) 0) (= m (* (fl (/ m n)) n))))
  :rule-classes nil)

mod-0-0theorem

(defthm mod-0-0
  (implies (and (integerp p) (rationalp m) (rationalp n))
    (iff (= (mod m (* n p)) 0)
      (and (= (mod m n) 0) (= (mod (fl (/ m n)) p) 0))))
  :rule-classes nil)

mod-prodtheorem

(defthmd mod-prod
  (implies (and (rationalp m) (rationalp n) (rationalp k))
    (equal (mod (* k m) (* k n)) (* k (mod m n)))))

mod012theorem

(defthm mod012
  (implies (integerp m)
    (or (equal (mod m 2) 0) (equal (mod m 2) 1)))
  :rule-classes nil)

mod-mod-2-not-equaltheorem

(defthm mod-mod-2-not-equal
  (implies (acl2-numberp m)
    (not (= (mod m 2) (mod (1+ m) 2))))
  :rule-classes nil)

mod-mod-sumencapsulate

(encapsulate nil
  (defthmd mod-sum
    (implies (and (rationalp a) (rationalp b))
      (equal (mod (+ a (mod b n)) n) (mod (+ a b) n))))
  (defthm mod-mod-sum
    (implies (and (rationalp a) (rationalp b))
      (equal (mod (+ (mod a n) (mod b n)) n) (mod (+ a b) n))))
  (defthmd mod-bnd-2
    (implies (and (<= 0 m) (case-split (rationalp m)))
      (<= (mod m n) m))
    :rule-classes :linear))

mod-plus-mod-2theorem

(defthm mod-plus-mod-2
  (implies (and (integerp a) (integerp b))
    (iff (= (mod (+ a b) 2) (mod a 2)) (= (mod b 2) 0)))
  :rule-classes nil)

mod-must-be-ntheorem

(defthm mod-must-be-n
  (implies (and (= (mod m n) 0)
      (< m (* 2 n))
      (< 0 m)
      (rationalp m)
      (rationalp n))
    (= m n))
  :rule-classes nil)

natp-compound-recognizertheorem

(defthm natp-compound-recognizer
  (equal (natp x) (and (integerp x) (<= 0 x)))
  :rule-classes :compound-recognizer)

natp-modtheorem

(defthm natp-mod
  (implies (and (natp m) (natp n)) (natp (mod m n)))
  :rule-classes ((:type-prescription :typed-term (mod m n))))

natp-mod-rewritetheorem

(defthm natp-mod-rewrite
  (implies (and (natp m) (natp n)) (natp (mod m n))))

mod-multtheorem

(defthmd mod-mult
  (implies (and (integerp a) (rationalp m) (rationalp n))
    (equal (mod (+ m (* a n)) n) (mod m n))))

mod-difftheorem

(defthmd mod-diff
  (implies (and (case-split (rationalp a)) (case-split (rationalp b)))
    (equal (mod (- a (mod b n)) n) (mod (- a b) n))))

mod-bnd-3theorem

(defthmd mod-bnd-3
  (implies (and (< m (+ (* a n) r))
      (<= (* a n) m)
      (integerp a)
      (case-split (rationalp m))
      (case-split (rationalp n)))
    (< (mod m n) r))
  :rule-classes :linear)

mod-forcetheorem

(defthm mod-force
  (implies (and (<= (* a n) m)
      (< m (* (1+ a) n))
      (integerp a)
      (rationalp m)
      (rationalp n))
    (= (mod m n) (- m (* a n))))
  :rule-classes nil)

mod-equal-inttheorem

(defthm mod-equal-int
  (implies (and (= (mod a n) (mod b n)) (rationalp a) (rationalp b))
    (integerp (/ (- a b) n)))
  :rule-classes nil)

mod-equal-int-reversetheorem

(defthm mod-equal-int-reverse
  (implies (and (integerp (/ (- a b) n))
      (rationalp a)
      (rationalp b)
      (rationalp n)
      (< 0 n))
    (= (mod a n) (mod b n)))
  :rule-classes nil)

mod-mult-2theorem

(defthmd mod-mult-2
  (implies (integerp a) (equal (mod (* a n) n) 0)))

mod-mult-2-alttheorem

(defthmd mod-mult-2-alt
  (implies (integerp a) (equal (mod (* n a) n) 0)))

mod-mult-ntheorem

(defthmd mod-mult-n (equal (mod (* a n) n) (* n (mod a 1))))

mod-mult-n-commutedtheorem

(defthmd mod-mult-n-commuted
  (equal (mod (* n a) n) (* n (mod a 1))))

mod-0-inttheorem

(defthm mod-0-int
  (implies (and (integerp m) (integerp n) (not (= n 0)))
    (iff (= (mod m n) 0) (integerp (/ m n))))
  :rule-classes nil)

mod-mult-2-gentheorem

(defthm mod-mult-2-gen
  (equal (mod (* a n) n) (* n (mod a 1))))

mod-mult-2-alt-gentheorem

(defthm mod-mult-2-alt-gen
  (equal (mod (* n a) n) (* n (mod a 1))))

mod-2*itheorem

(defthm mod-2*i
  (implies (integerp i) (equal (mod (* 2 i) 2) 0)))

mod-2*m+1-rewritetheorem

(defthm mod-2*m+1-rewrite
  (implies (integerp m) (equal (mod (1+ (* 2 m)) 2) 1)))

mod-2*i+1theorem

(defthm mod-2*i+1
  (implies (integerp i) (not (equal (mod (1+ (* 2 i)) 2) 0))))

induct-natfunction

(defun induct-nat
  (x)
  (if (and (integerp x) (> x 0))
    (induct-nat (1- x))
    nil))

nk>=ktheorem

(defthm nk>=k
  (implies (and (integerp n) (integerp k) (> k 0) (not (= (* n k) 0)))
    (>= (abs (* n k)) k))
  :rule-classes nil)

mod-force-equaltheorem

(defthm mod-force-equal
  (implies (and (< (abs (- a b)) n)
      (rationalp a)
      (rationalp b)
      (integerp n))
    (iff (= (mod a n) (mod b n)) (= a b)))
  :rule-classes nil
  :hints (("goal" :use (mod-equal-int (:instance nk>=k (k n) (n (/ (- a b) n)))))))

nk>=k-lineartheorem

(defthmd nk>=k-linear
  (implies (and (integerp n) (integerp k) (not (= n 0)))
    (>= (abs (* n k)) k))
  :rule-classes :linear)

fl-modtheorem

(defthm fl-mod
  (implies (and (rationalp x) (natp y))
    (equal (fl (mod x y)) (mod (fl x) y))))

mod-sum-casestheorem

(defthmd mod-sum-cases
  (implies (and (<= 0 y) (rationalp x) (rationalp y) (rationalp k))
    (equal (mod (+ k x) y)
      (if (< (+ (mod k y) (mod x y)) y)
        (+ (mod k y) (mod x y))
        (+ (mod k y) (mod x y) (* -1 y))))))

mod-fl-erictheorem

(defthmd mod-fl-eric
  (implies (and (<= 0 y) (integerp y))
    (equal (mod (fl x) y) (fl (mod x y)))))

mod-squeezetheorem

(defthm mod-squeeze
  (implies (and (= (mod m n) 0)
      (< m (* (1+ a) n))
      (< (* (1- a) n) m)
      (integerp a)
      (integerp m)
      (integerp n))
    (= m (* a n)))
  :rule-classes nil)

Included Books