equal
deleted
inserted
replaced
94 lemma prime_dvd_mult_eq_int [simp]: |
94 lemma prime_dvd_mult_eq_int [simp]: |
95 fixes n::int |
95 fixes n::int |
96 shows "prime p \<Longrightarrow> p dvd m * n = (p dvd m \<or> p dvd n)" |
96 shows "prime p \<Longrightarrow> p dvd m * n = (p dvd m \<or> p dvd n)" |
97 by (rule iffI, rule prime_dvd_mult_int, auto) |
97 by (rule iffI, rule prime_dvd_mult_int, auto) |
98 |
98 |
99 lemma not_prime_eq_prod_nat: "(n::nat) > 1 \<Longrightarrow> ~ prime n \<Longrightarrow> |
99 lemma not_prime_eq_prod_nat: |
100 EX m k. n = m * k & 1 < m & m < n & 1 < k & k < n" |
100 "1 < n \<Longrightarrow> \<not> prime n \<Longrightarrow> |
101 unfolding prime_def dvd_def apply auto |
101 \<exists>m k. n = m * k \<and> 1 < m \<and> m < n \<and> 1 < k \<and> k < n" |
102 by (metis mult.commute linorder_neq_iff linorder_not_le mult_1 |
102 unfolding prime_def dvd_def apply (auto simp add: ac_simps) |
103 n_less_n_mult_m one_le_mult_iff less_imp_le_nat) |
103 by (metis Suc_lessD Suc_lessI n_less_m_mult_n n_less_n_mult_m nat_0_less_mult_iff) |
104 |
104 |
105 lemma prime_dvd_power_nat: "prime p \<Longrightarrow> p dvd x^n \<Longrightarrow> p dvd x" |
105 lemma prime_dvd_power_nat: "prime p \<Longrightarrow> p dvd x^n \<Longrightarrow> p dvd x" |
106 by (induct n) auto |
106 by (induct n) auto |
107 |
107 |
108 lemma prime_dvd_power_int: |
108 lemma prime_dvd_power_int: |