equal
deleted
inserted
replaced
871 from H[unfolded coprime] |
871 from H[unfolded coprime] |
872 obtain p where p: "p dvd n" "p dvd a" "p \<noteq> 1" by auto |
872 obtain p where p: "p dvd n" "p dvd a" "p \<noteq> 1" by auto |
873 from lh[unfolded nat_mod] |
873 from lh[unfolded nat_mod] |
874 obtain q1 q2 where q12:"a ^ d + n * q1 = 1 + n * q2" by blast |
874 obtain q1 q2 where q12:"a ^ d + n * q1 = 1 + n * q2" by blast |
875 hence "a ^ d + n * q1 - n * q2 = 1" by simp |
875 hence "a ^ d + n * q1 - n * q2 = 1" by simp |
876 with dvd_diff [OF dvd_add [OF divides_rexp[OF p(2), of d'] dvd_mult2[OF p(1), of q1]] dvd_mult2[OF p(1), of q2]] d' have "p dvd 1" by simp |
876 with nat_dvd_diff [OF dvd_add [OF divides_rexp[OF p(2), of d'] dvd_mult2[OF p(1), of q1]] dvd_mult2[OF p(1), of q2]] d' have "p dvd 1" by simp |
877 with p(3) have False by simp |
877 with p(3) have False by simp |
878 hence ?rhs ..} |
878 hence ?rhs ..} |
879 ultimately have ?rhs by blast} |
879 ultimately have ?rhs by blast} |
880 moreover |
880 moreover |
881 {assume H: "coprime n a" |
881 {assume H: "coprime n a" |