equal
deleted
inserted
replaced
25 apply (auto simp add: prime_def) |
25 apply (auto simp add: prime_def) |
26 apply (erule dvdE) |
26 apply (erule dvdE) |
27 apply (case_tac "k=0", simp) |
27 apply (case_tac "k=0", simp) |
28 apply (drule_tac x = m in spec) |
28 apply (drule_tac x = m in spec) |
29 apply (drule_tac x = k in spec) |
29 apply (drule_tac x = k in spec) |
30 apply (simp add: dvd_mult_cancel1 dvd_mult_cancel2, auto) |
30 apply (simp add: dvd_mult_cancel1 dvd_mult_cancel2) |
31 done |
31 done |
32 |
32 |
33 lemma zero_less_prime_power: "prime p ==> 0 < p^a" |
33 lemma zero_less_prime_power: "prime p ==> 0 < p^a" |
34 by (force simp add: prime_iff) |
34 by (force simp add: prime_iff) |
35 |
35 |