Theory IntArith

Up to index of Isabelle/ZF

theory IntArith
imports Bin
uses int_arith.ML
begin

theory IntArith imports Bin
uses "int_arith.ML" begin

end

theorem zless_iff_zdiff_zless_0:

  x $< y <-> x $- y $< #0

theorem eq_iff_zdiff_eq_0:

  [| x ∈ int; y ∈ int |] ==> x = y <-> x $- y = #0

theorem zle_iff_zdiff_zle_0:

  x $≤ y <-> x $- y $≤ #0

theorem left_zadd_zmult_distrib:

  iu $+ (ju $+ k) = (i $+ j) $× u $+ k

theorem eq_add_iff1:

  iu $+ m = ju $+ n <-> (i $- j) $× u $+ m = intify(n)

theorem eq_add_iff2:

  iu $+ m = ju $+ n <-> intify(m) = (j $- i) $× u $+ n

theorem less_add_iff1:

  iu $+ m $< ju $+ n <-> (i $- j) $× u $+ m $< n

theorem less_add_iff2:

  iu $+ m $< ju $+ n <-> m $< (j $- i) $× u $+ n

theorem le_add_iff1:

  iu $+ m $≤ ju $+ n <-> (i $- j) $× u $+ m $≤ n

theorem le_add_iff2:

  iu $+ m $≤ ju $+ n <-> m $≤ (j $- i) $× u $+ n