equal
deleted
inserted
replaced
177 apply (auto simp add: prime_def) |
177 apply (auto simp add: prime_def) |
178 apply (drule_tac x = "gcd (p, n)" in spec) |
178 apply (drule_tac x = "gcd (p, n)" in spec) |
179 apply auto |
179 apply auto |
180 apply (insert gcd_dvd2 [of p n]) |
180 apply (insert gcd_dvd2 [of p n]) |
181 apply simp |
181 apply simp |
|
182 done |
|
183 |
|
184 lemma two_is_prime: "2 \<in> prime" |
|
185 apply (auto simp add: prime_def) |
|
186 apply (case_tac m) |
|
187 apply (auto dest!: dvd_imp_le) |
|
188 apply arith |
182 done |
189 done |
183 |
190 |
184 text {* |
191 text {* |
185 This theorem leads immediately to a proof of the uniqueness of |
192 This theorem leads immediately to a proof of the uniqueness of |
186 factorization. If @{term p} divides a product of primes then it is |
193 factorization. If @{term p} divides a product of primes then it is |