[STATEMENT]
lemma iMOD_plus: "
  x \<in> [r, mod m] \<Longrightarrow> (x + k \<in> [r, mod m]) = (k mod m = 0)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x \<in> [ r, mod m ] \<Longrightarrow> (x + k \<in> [ r, mod m ]) = (k mod m = 0)
[PROOF STEP]
apply safe
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>x \<in> [ r, mod m ]; x + k \<in> [ r, mod m ]\<rbrakk> \<Longrightarrow> k mod m = 0
 2. \<lbrakk>x \<in> [ r, mod m ]; m dvd k\<rbrakk> \<Longrightarrow> x + k \<in> [ r, mod m ]
[PROOF STEP]
apply (drule iMOD_modD)+
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>x mod m = r mod m; (x + k) mod m = r mod m\<rbrakk> \<Longrightarrow> k mod m = 0
 2. \<lbrakk>x \<in> [ r, mod m ]; m dvd k\<rbrakk> \<Longrightarrow> x + k \<in> [ r, mod m ]
[PROOF STEP]
apply (rule mod_add_eq_imp_mod_0[of x, THEN iffD1])
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>x mod m = r mod m; (x + k) mod m = r mod m\<rbrakk> \<Longrightarrow> (x + k) mod m = x mod m
 2. \<lbrakk>x \<in> [ r, mod m ]; m dvd k\<rbrakk> \<Longrightarrow> x + k \<in> [ r, mod m ]
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>x \<in> [ r, mod m ]; m dvd k\<rbrakk> \<Longrightarrow> x + k \<in> [ r, mod m ]
[PROOF STEP]
apply (erule dvdE)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>ka. \<lbrakk>x \<in> [ r, mod m ]; k = m * ka\<rbrakk> \<Longrightarrow> x + k \<in> [ r, mod m ]
[PROOF STEP]
apply (simp add: mult.commute iMOD_plus_divisor_mult)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done