equal
deleted
inserted
replaced
84 apply (rule_tac [2] zcong_zless_imp_eq, auto) |
84 apply (rule_tac [2] zcong_zless_imp_eq, auto) |
85 done |
85 done |
86 |
86 |
87 lemma inv_not_p_minus_1_aux: "[a * (p - 1) = 1] (mod p) = [a = p - 1] (mod p)" |
87 lemma inv_not_p_minus_1_aux: "[a * (p - 1) = 1] (mod p) = [a = p - 1] (mod p)" |
88 apply (unfold zcong_def) |
88 apply (unfold zcong_def) |
89 apply (simp add: Ring_and_Field.diff_diff_eq diff_diff_eq2 zdiff_zmult_distrib2) |
89 apply (simp add: OrderedGroup.diff_diff_eq diff_diff_eq2 zdiff_zmult_distrib2) |
90 apply (rule_tac s = "p dvd -((a + 1) + (p * -a))" in trans) |
90 apply (rule_tac s = "p dvd -((a + 1) + (p * -a))" in trans) |
91 apply (simp add: mult_commute) |
91 apply (simp add: mult_commute) |
92 apply (subst zdvd_zminus_iff) |
92 apply (subst zdvd_zminus_iff) |
93 apply (subst zdvd_reduce) |
93 apply (subst zdvd_reduce) |
94 apply (rule_tac s = "p dvd (a + 1) + (p * -1)" in trans) |
94 apply (rule_tac s = "p dvd (a + 1) + (p * -1)" in trans) |