coprime

Scratch.thy

theory Scratch
  imports Main
begin

lemma
  fixes m n
  assumes "m ≥ 2" "n ≥ 2"
  shows "coprime m n ⟷ (∃a b. a * int m + b * int n = 1)"
proof
  let ?A = "{1..n}"
  let ?B = "{0..<n}"
  let ?f = "λx. m * x mod n"
  have inj_on: "coprime m n ⟹ inj_on ?f ?A"
  proof
    fix x y
    let ?k = "m * x mod n"
    assume "m * x mod n = m * y mod n"
    then obtain p q where
      p: "m * x = p * n + ?k" and
      q: "m * y = q * n + ?k"
      by (metis div_mult_mod_eq)
    then have "m * (x - y) = (p - q) * n"
      using diff_mult_distrib diff_mult_distrib2 by auto
    then have "n dvd m * (x - y)" by simp
    then have dvd1: "coprime m n ⟹ n dvd (x - y)"
      using coprime_commute coprime_dvd_mult_right_iff by blast
    have "m * (y - x) = (q - p) * n"
      using p q diff_mult_distrib diff_mult_distrib2 by auto
    then have "n dvd m * (y - x)" by simp
    then have dvd2: "coprime m n ⟹ n dvd (y - x)"
      using coprime_commute coprime_dvd_mult_right_iff by blast

    assume "x ∈ {1..n}" and "y ∈ {1..n}"
    then have less1: "x - y < n"
      by (metis atLeastAtMost_iff diff_less le_neq_implies_less less_imp_diff_less less_one)
    assume "x ∈ {1..n}" and "y ∈ {1..n}"
    then have less2: "y - x < n"
      by (metis atLeastAtMost_iff diff_less le_neq_implies_less less_imp_diff_less less_one)

    assume "coprime m n"
    then have "x - y = 0" using dvd1 less1 by auto
    moreover
    assume "coprime m n"
    then have "y - x = 0" using dvd2 less2 by auto
    ultimately
    show "x = y" by auto
  qed

  have "?f ` ?A ⊆ ?B" by auto
  moreover have "coprime m n ⟹ card (?f ` ?A) = card ?B"
    using card_image inj_on by fastforce
  ultimately
  have surj: "coprime m n ⟹ ?f ` ?A = ?B" by (simp add: card_subset_eq)
  then have "coprime m n ⟹ ∃x ∈ ?A. 1 = ?f x"
    (* apply (subgoal_tac "1 ∈ ?f ` ?A")
     apply (erule imageE)
    by auto *)
    using imageE assms by auto
  then have "coprime m n ⟹ ∃x ∈ ?A. ∃k. m * x = k * n + 1"
    by (metis add.commute mod_eq_nat1E mod_less_eq_dividend mod_mod_trivial mult.commute)
  then have "coprime m n ⟹ ∃x ∈ ?A. ∃k. int m * int x = int k * int n + 1"
    by (metis add.commute mult.left_neutral mult_Suc_right of_nat_Suc of_nat_mult)
  then have "coprime m n ⟹ ∃x ∈ ?A. ∃k. int x * int m + (-int k) * int n = 1"
    by (metis add.commute add_minus_cancel mult.commute mult_minus_right)
  then show "coprime m n ⟹ ∃a b. a * int m + b * int n = 1" by blast
next
  have contra: "¬coprime m n ⟹ ¬(∃a b. a * int m + b * int n = 1)"
  proof -
    assume "¬coprime m n"
    then obtain k where
      "k dvd m"
      "k dvd n"
      "k ≠ 1"
      "k ≠ 0"
      by (metis (no_types, hide_lams) dvd_0_right gcd_nat.strict_trans1 
          gt_ex less_not_refl not_coprimeE not_less_zero one_dvd)
    then obtain m' n' where
      "m = m' * k"
      "n = n' * k"
      by fastforce
    then have "∀a b. a * int m + b * int n = (a * int m' + b * int n') * int k"
      by (simp add: int_distrib(2) mult.commute)
    then have "∀a b. (int k) dvd (a * int m + b * int n)"
      by simp
    then have "∀a b c. a * int m + b * int n = c ⟶ (int k) dvd c"
      by simp
    then show "¬(∃a b. a * int m + b * int n = 1)"
      using ‹k ≠ 1› by fastforce
  qed

  assume "∃a b. a * int m + b * int n = 1"
  then show "coprime m n" using contra by auto
qed

end