# HG changeset patch # User haftmann # Date 1267017593 -3600 # Node ID 19b340c3f1ffdeba0f87fc406222621b9680ff13 # Parent 45a193f0ed0c94dcba5e24ec9bf2b80eea06ff9a crossproduct coprimality lemmas diff -r 45a193f0ed0c -r 19b340c3f1ff src/HOL/GCD.thy --- a/src/HOL/GCD.thy Wed Feb 24 14:19:53 2010 +0100 +++ b/src/HOL/GCD.thy Wed Feb 24 14:19:53 2010 +0100 @@ -412,6 +412,33 @@ apply (rule gcd_mult_cancel_nat [transferred], auto) done +lemma coprime_crossproduct_nat: + fixes a b c d :: nat + assumes "coprime a d" and "coprime b c" + shows "a * c = b * d \ a = b \ c = d" (is "?lhs \ ?rhs") +proof + assume ?rhs then show ?lhs by simp +next + assume ?lhs + from `?lhs` have "a dvd b * d" by (auto intro: dvdI dest: sym) + with `coprime a d` have "a dvd b" by (simp add: coprime_dvd_mult_iff_nat) + from `?lhs` have "b dvd a * c" by (auto intro: dvdI dest: sym) + with `coprime b c` have "b dvd a" by (simp add: coprime_dvd_mult_iff_nat) + from `?lhs` have "c dvd d * b" by (auto intro: dvdI dest: sym simp add: mult_commute) + with `coprime b c` have "c dvd d" by (simp add: coprime_dvd_mult_iff_nat gcd_commute_nat) + from `?lhs` have "d dvd c * a" by (auto intro: dvdI dest: sym simp add: mult_commute) + with `coprime a d` have "d dvd c" by (simp add: coprime_dvd_mult_iff_nat gcd_commute_nat) + from `a dvd b` `b dvd a` have "a = b" by (rule Nat.dvd.antisym) + moreover from `c dvd d` `d dvd c` have "c = d" by (rule Nat.dvd.antisym) + ultimately show ?rhs .. +qed + +lemma coprime_crossproduct_int: + fixes a b c d :: int + assumes "coprime a d" and "coprime b c" + shows "\a\ * \c\ = \b\ * \d\ \ \a\ = \b\ \ \c\ = \d\" + using assms by (intro coprime_crossproduct_nat [transferred]) auto + text {* \medskip Addition laws *} lemma gcd_add1_nat [simp]: "gcd ((m::nat) + n) n = gcd m n"