equal
deleted
inserted
replaced
269 assume "a * b = x * int p" |
269 assume "a * b = x * int p" |
270 then have "p dvd a * b" by simp |
270 then have "p dvd a * b" by simp |
271 then have "p dvd a \<or> p dvd b" |
271 then have "p dvd a \<or> p dvd b" |
272 by (metis prime prime_dvd_mult_eq_int) |
272 by (metis prime prime_dvd_mult_eq_int) |
273 then show "(\<exists>x. a = x * int p) \<or> (\<exists>x. b = x * int p)" |
273 then show "(\<exists>x. a = x * int p) \<or> (\<exists>x. b = x * int p)" |
274 by (metis dvd_def mult_commute) |
274 by (metis dvd_def mult.commute) |
275 next |
275 next |
276 assume "UNIV = {uu. EX x. uu = x * int p}" |
276 assume "UNIV = {uu. EX x. uu = x * int p}" |
277 then obtain x where "1 = x * int p" by best |
277 then obtain x where "1 = x * int p" by best |
278 then have "\<bar>int p * x\<bar> = 1" by (simp add: mult_commute) |
278 then have "\<bar>int p * x\<bar> = 1" by (simp add: mult.commute) |
279 then show False |
279 then show False |
280 by (metis abs_of_nat int_1 of_nat_eq_iff abs_zmult_eq_1 one_not_prime_nat prime) |
280 by (metis abs_of_nat int_1 of_nat_eq_iff abs_zmult_eq_1 one_not_prime_nat prime) |
281 qed |
281 qed |
282 |
282 |
283 |
283 |