equal
deleted
inserted
replaced
215 apply (frule p_fac_forw_lemma [THEN le_imp_power_dvd, of _ k p], auto) |
215 apply (frule p_fac_forw_lemma [THEN le_imp_power_dvd, of _ k p], auto) |
216 apply (subgoal_tac "p^r dvd p^a*m") |
216 apply (subgoal_tac "p^r dvd p^a*m") |
217 prefer 2 apply (blast intro: dvd_mult2) |
217 prefer 2 apply (blast intro: dvd_mult2) |
218 apply (drule dvd_diffD1) |
218 apply (drule dvd_diffD1) |
219 apply assumption |
219 apply assumption |
220 prefer 2 apply (blast intro: nat_dvd_diff) |
220 prefer 2 apply (blast intro: dvd_diff_nat) |
221 apply (drule gr0_implies_Suc, auto) |
221 apply (drule gr0_implies_Suc, auto) |
222 done |
222 done |
223 |
223 |
224 |
224 |
225 lemma r_le_a_forw: |
225 lemma r_le_a_forw: |
231 apply (frule_tac k1 = k and p1 = p in r_le_a_forw [THEN le_imp_power_dvd], auto) |
231 apply (frule_tac k1 = k and p1 = p in r_le_a_forw [THEN le_imp_power_dvd], auto) |
232 apply (subgoal_tac "p^r dvd p^a*m") |
232 apply (subgoal_tac "p^r dvd p^a*m") |
233 prefer 2 apply (blast intro: dvd_mult2) |
233 prefer 2 apply (blast intro: dvd_mult2) |
234 apply (drule dvd_diffD1) |
234 apply (drule dvd_diffD1) |
235 apply assumption |
235 apply assumption |
236 prefer 2 apply (blast intro: nat_dvd_diff) |
236 prefer 2 apply (blast intro: dvd_diff_nat) |
237 apply (drule less_imp_Suc_add, auto) |
237 apply (drule less_imp_Suc_add, auto) |
238 done |
238 done |
239 |
239 |
240 lemma exponent_p_a_m_k_equation: "[| m>0; k>0; (p::nat)\<noteq>0; k < p^a |] |
240 lemma exponent_p_a_m_k_equation: "[| m>0; k>0; (p::nat)\<noteq>0; k < p^a |] |
241 ==> exponent p (p^a * m - k) = exponent p (p^a - k)" |
241 ==> exponent p (p^a * m - k) = exponent p (p^a - k)" |