equal
deleted
inserted
replaced
249 next |
249 next |
250 assume "UNIV = {uu. EX x. uu = x * int p}" |
250 assume "UNIV = {uu. EX x. uu = x * int p}" |
251 then obtain x where "1 = x * int p" by best |
251 then obtain x where "1 = x * int p" by best |
252 then have "\<bar>int p * x\<bar> = 1" by (simp add: mult.commute) |
252 then have "\<bar>int p * x\<bar> = 1" by (simp add: mult.commute) |
253 then show False |
253 then show False |
254 by (metis abs_of_nat int_1 of_nat_eq_iff abs_zmult_eq_1 one_not_prime_nat prime) |
254 by (metis abs_of_nat of_nat_1 of_nat_eq_iff abs_zmult_eq_1 one_not_prime_nat prime) |
255 qed |
255 qed |
256 |
256 |
257 |
257 |
258 subsection \<open>Ideals and Divisibility\<close> |
258 subsection \<open>Ideals and Divisibility\<close> |
259 |
259 |