equal
deleted
inserted
replaced
96 by auto |
96 by auto |
97 qed |
97 qed |
98 finally have "a ^ count M a dvd a ^ count N a * (\<Prod>i \<in> (set_mset N - {a}). i ^ count N i)" . |
98 finally have "a ^ count M a dvd a ^ count N a * (\<Prod>i \<in> (set_mset N - {a}). i ^ count N i)" . |
99 moreover |
99 moreover |
100 have "coprime (a ^ count M a) (\<Prod>i \<in> (set_mset N - {a}). i ^ count N i)" |
100 have "coprime (a ^ count M a) (\<Prod>i \<in> (set_mset N - {a}). i ^ count N i)" |
101 apply (subst gcd_commute_nat) |
101 apply (subst gcd.commute) |
102 apply (rule setprod_coprime_nat) |
102 apply (rule setprod_coprime_nat) |
103 apply (rule primes_imp_powers_coprime_nat) |
103 apply (rule primes_imp_powers_coprime_nat) |
104 using assms True |
104 using assms True |
105 apply auto |
105 apply auto |
106 done |
106 done |
107 ultimately have "a ^ count M a dvd a ^ count N a" |
107 ultimately have "a ^ count M a dvd a ^ count N a" |
108 by (elim coprime_dvd_mult_nat) |
108 by (elim coprime_dvd_mult) |
109 with a show ?thesis |
109 with a show ?thesis |
110 using power_dvd_imp_le prime_def by blast |
110 using power_dvd_imp_le prime_def by blast |
111 next |
111 next |
112 case False |
112 case False |
113 then show ?thesis |
113 then show ?thesis |
659 |
659 |
660 lemma multiplicity_dvd'_int: |
660 lemma multiplicity_dvd'_int: |
661 fixes x y :: int |
661 fixes x y :: int |
662 shows "0 < x \<Longrightarrow> 0 \<le> y \<Longrightarrow> |
662 shows "0 < x \<Longrightarrow> 0 \<le> y \<Longrightarrow> |
663 \<forall>p. prime p \<longrightarrow> multiplicity p x \<le> multiplicity p y \<Longrightarrow> x dvd y" |
663 \<forall>p. prime p \<longrightarrow> multiplicity p x \<le> multiplicity p y \<Longrightarrow> x dvd y" |
664 by (metis GCD.dvd_int_iff abs_int_eq multiplicity_dvd'_nat multiplicity_int_def nat_int |
664 by (metis dvd_int_iff abs_of_nat multiplicity_dvd'_nat multiplicity_int_def nat_int |
665 zero_le_imp_eq_int zero_less_imp_eq_int) |
665 zero_le_imp_eq_int zero_less_imp_eq_int) |
666 |
666 |
667 lemma dvd_multiplicity_eq_nat: |
667 lemma dvd_multiplicity_eq_nat: |
668 fixes x y :: nat |
668 fixes x y :: nat |
669 shows "0 < x \<Longrightarrow> 0 < y \<Longrightarrow> x dvd y \<longleftrightarrow> (\<forall>p. multiplicity p x \<le> multiplicity p y)" |
669 shows "0 < x \<Longrightarrow> 0 < y \<Longrightarrow> x dvd y \<longleftrightarrow> (\<forall>p. multiplicity p x \<le> multiplicity p y)" |