equal
deleted
inserted
replaced
328 qed |
328 qed |
329 |
329 |
330 lemma mod_mult_mult2: |
330 lemma mod_mult_mult2: |
331 "(a * c) mod (b * c) = (a mod b) * c" |
331 "(a * c) mod (b * c) = (a mod b) * c" |
332 using mod_mult_mult1 [of c a b] by (simp add: mult_commute) |
332 using mod_mult_mult1 [of c a b] by (simp add: mult_commute) |
|
333 |
|
334 lemma dvd_mod: "k dvd m \<Longrightarrow> k dvd n \<Longrightarrow> k dvd (m mod n)" |
|
335 unfolding dvd_def by (auto simp add: mod_mult_mult1) |
|
336 |
|
337 lemma dvd_mod_iff: "k dvd n \<Longrightarrow> k dvd (m mod n) \<longleftrightarrow> k dvd m" |
|
338 by (blast intro: dvd_mod_imp_dvd dvd_mod) |
333 |
339 |
334 lemma div_power: |
340 lemma div_power: |
335 "y dvd x \<Longrightarrow> (x div y) ^ n = x ^ n div y ^ n" |
341 "y dvd x \<Longrightarrow> (x div y) ^ n = x ^ n div y ^ n" |
336 apply (induct n) |
342 apply (induct n) |
337 apply simp |
343 apply simp |
901 prefer 2 apply simp |
907 prefer 2 apply simp |
902 apply (erule ssubst) |
908 apply (erule ssubst) |
903 apply (erule nat_dvd_diff) |
909 apply (erule nat_dvd_diff) |
904 apply (rule dvd_refl) |
910 apply (rule dvd_refl) |
905 done |
911 done |
906 |
|
907 lemma dvd_mod: "!!n::nat. [| f dvd m; f dvd n |] ==> f dvd m mod n" |
|
908 unfolding dvd_def |
|
909 apply (case_tac "n = 0", auto) |
|
910 apply (blast intro: mod_mult_distrib2 [symmetric]) |
|
911 done |
|
912 |
|
913 lemma dvd_mod_iff: "k dvd n ==> ((k::nat) dvd m mod n) = (k dvd m)" |
|
914 by (blast intro: dvd_mod_imp_dvd dvd_mod) |
|
915 |
912 |
916 lemma dvd_mult_cancel: "!!k::nat. [| k*m dvd k*n; 0<k |] ==> m dvd n" |
913 lemma dvd_mult_cancel: "!!k::nat. [| k*m dvd k*n; 0<k |] ==> m dvd n" |
917 unfolding dvd_def |
914 unfolding dvd_def |
918 apply (erule exE) |
915 apply (erule exE) |
919 apply (simp add: mult_ac) |
916 apply (simp add: mult_ac) |