src/HOL/Number_Theory/Pocklington.thy
changeset 55346 d344d663658a
parent 55337 5d45fb978d5a
child 55370 e6be866b5f5b
equal deleted inserted replaced
55345:8a53ee72e595 55346:d344d663658a
   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" ..
   658     hence b1: "b \<ge> 1" by arith thm Cong.cong_diff_nat[OF cong_sym_nat [OF b(1)] cong_refl_nat[of 1]]
   658     hence b1: "b \<ge> 1" by arith 
   659     from cong_imp_coprime_nat[OF Cong.cong_diff_nat[OF cong_sym_nat [OF b(1)] cong_refl_nat[of 1] b1]] ath b1 b(2) nqr
   659     from cong_imp_coprime_nat[OF Cong.cong_diff_nat[OF cong_sym_nat [OF b(1)] cong_refl_nat[of 1] b1]] 
       
   660          ath b1 b nqr
   660     have "coprime (a ^ ((n - 1) div p) - 1) n"
   661     have "coprime (a ^ ((n - 1) div p) - 1) n"
   661       by simp}
   662       by simp}
   662   hence th: "\<forall>p. prime p \<and> p dvd q \<longrightarrow> coprime (a ^ ((n - 1) div p) - 1) n "
   663   hence th: "\<forall>p. prime p \<and> p dvd q \<longrightarrow> coprime (a ^ ((n - 1) div p) - 1) n "
   663     by blast
   664     by blast
   664   from pocklington[OF n nqr sqr an th] show ?thesis .
   665   from pocklington[OF n nqr sqr an th] show ?thesis .