equal
deleted
inserted
replaced
647 hence eq: "(a^((n - 1) div p))^p = a^(n - 1)" |
647 hence eq: "(a^((n - 1) div p))^p = a^(n - 1)" |
648 by (simp only: power_mult[symmetric]) |
648 by (simp only: power_mult[symmetric]) |
649 have "p - 1 \<noteq> 0" using prime_ge_2_nat [OF p(1)] by arith |
649 have "p - 1 \<noteq> 0" using prime_ge_2_nat [OF p(1)] by arith |
650 then have pS: "Suc (p - 1) = p" by arith |
650 then have pS: "Suc (p - 1) = p" by arith |
651 from b have d: "n dvd a^((n - 1) div p)" unfolding b0 |
651 from b have d: "n dvd a^((n - 1) div p)" unfolding b0 |
652 by (metis b0 diff_0_eq_0 gcd_dvd2_nat gcd_lcm_complete_lattice_nat.inf_bot_left |
652 by (metis b0 diff_0_eq_0 gcd_dvd2 gcd_lcm_complete_lattice_nat.inf_bot_left |
653 gcd_lcm_complete_lattice_nat.inf_top_left) |
653 gcd_lcm_complete_lattice_nat.inf_top_left) |
654 from divides_rexp[OF d, of "p - 1"] pS eq cong_dvd_eq_nat [OF an] n |
654 from divides_rexp[OF d, of "p - 1"] pS eq cong_dvd_eq_nat [OF an] n |
655 have False |
655 have False |
656 by simp} |
656 by simp} |
657 then have b0: "b \<noteq> 0" .. |
657 then have b0: "b \<noteq> 0" .. |