equal
deleted
inserted
replaced
189 proof (simp add: MultInv_def zcong_eq_zdvd_prop) |
189 proof (simp add: MultInv_def zcong_eq_zdvd_prop) |
190 assume "2 < p" and "zprime p" and "~ p dvd x" |
190 assume "2 < p" and "zprime p" and "~ p dvd x" |
191 have "x * x ^ nat (p - 2) = x ^ (nat (p - 2) + 1)" |
191 have "x * x ^ nat (p - 2) = x ^ (nat (p - 2) + 1)" |
192 by auto |
192 by auto |
193 also from prems have "nat (p - 2) + 1 = nat (p - 2 + 1)" |
193 also from prems have "nat (p - 2) + 1 = nat (p - 2 + 1)" |
194 by (simp only: nat_add_distrib, auto) |
194 by (simp only: nat_add_distrib) |
195 also have "p - 2 + 1 = p - 1" by arith |
195 also have "p - 2 + 1 = p - 1" by arith |
196 finally have "[x * x ^ nat (p - 2) = x ^ nat (p - 1)] (mod p)" |
196 finally have "[x * x ^ nat (p - 2) = x ^ nat (p - 1)] (mod p)" |
197 by (rule ssubst, auto) |
197 by (rule ssubst, auto) |
198 also from prems have "[x ^ nat (p - 1) = 1] (mod p)" |
198 also from prems have "[x ^ nat (p - 1) = 1] (mod p)" |
199 by (auto simp add: Little_Fermat) |
199 by (auto simp add: Little_Fermat) |