equal
deleted
inserted
replaced
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) |
101 apply (subst gcd.commute) |
102 apply (rule setprod_coprime_nat) |
102 apply (rule setprod_coprime) |
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" |