490 hence ceq: "card ?S' = card ?S" |
490 hence ceq: "card ?S' = card ?S" |
491 using n finite_number_segment[of n] phi_another[OF n(2)] by simp |
491 using n finite_number_segment[of n] phi_another[OF n(2)] by simp |
492 {fix m assume m: "0 < m" "m < n" "\<not> coprime m n" |
492 {fix m assume m: "0 < m" "m < n" "\<not> coprime m n" |
493 hence mS': "m \<notin> ?S'" by auto |
493 hence mS': "m \<notin> ?S'" by auto |
494 have "insert m ?S' \<le> ?S" using m by auto |
494 have "insert m ?S' \<le> ?S" using m by auto |
495 from m have "card (insert m ?S') \<le> card ?S" |
495 have "card (insert m ?S') \<le> card ?S" |
496 by - (rule card_mono[of ?S "insert m ?S'"], auto) |
496 by (rule card_mono[of ?S "insert m ?S'"]) (use m in auto) |
497 hence False |
497 hence False |
498 unfolding card_insert_disjoint[of "?S'" m, OF fS' mS'] ceq |
498 unfolding card_insert_disjoint[of "?S'" m, OF fS' mS'] ceq |
499 by simp } |
499 by simp } |
500 hence "\<forall>m. 0 <m \<and> m < n \<longrightarrow> coprime m n" by blast |
500 hence "\<forall>m. 0 <m \<and> m < n \<longrightarrow> coprime m n" by blast |
501 hence "prime n" unfolding prime using n by (simp add: coprime_commute)} |
501 hence "prime n" unfolding prime using n by (simp add: coprime_commute)} |
765 less_trans[OF mod_less_divisor[OF m(1), of "n - 1"] m(2)] th1 |
765 less_trans[OF mod_less_divisor[OF m(1), of "n - 1"] m(2)] th1 |
766 have False by blast } |
766 have False by blast } |
767 hence "(n - 1) mod m = 0" by auto |
767 hence "(n - 1) mod m = 0" by auto |
768 then have mn: "m dvd n - 1" by presburger |
768 then have mn: "m dvd n - 1" by presburger |
769 then obtain r where r: "n - 1 = m*r" unfolding dvd_def by blast |
769 then obtain r where r: "n - 1 = m*r" unfolding dvd_def by blast |
770 from n01 r m(2) have r01: "r\<noteq>0" "r\<noteq>1" by - (rule ccontr, simp)+ |
770 from n01 r m(2) have r01: "r\<noteq>0" "r\<noteq>1" by auto |
771 from prime_factor[OF r01(2)] obtain p where p: "prime p" "p dvd r" by blast |
771 from prime_factor[OF r01(2)] obtain p where p: "prime p" "p dvd r" by blast |
772 hence th: "prime p \<and> p dvd n - 1" unfolding r by (auto intro: dvd_mult) |
772 hence th: "prime p \<and> p dvd n - 1" unfolding r by (auto intro: dvd_mult) |
773 have "(a ^ ((n - 1) div p)) mod n = (a^(m*r div p)) mod n" using r |
773 have "(a ^ ((n - 1) div p)) mod n = (a^(m*r div p)) mod n" using r |
774 by (simp add: power_mult) |
774 by (simp add: power_mult) |
775 also have "\<dots> = (a^(m*(r div p))) mod n" using div_mult1_eq[of m r p] p(2)[unfolded dvd_eq_mod_eq_0] by simp |
775 also have "\<dots> = (a^(m*(r div p))) mod n" using div_mult1_eq[of m r p] p(2)[unfolded dvd_eq_mod_eq_0] by simp |
798 from na have o: "ord n a = Least ?P" by (simp add: ord_def) |
798 from na have o: "ord n a = Least ?P" by (simp add: ord_def) |
799 {assume "n=0 \<or> n=1" with na have "\<exists>m>0. ?P m" apply auto apply (rule exI[where x=1]) by (simp add: modeq_def)} |
799 {assume "n=0 \<or> n=1" with na have "\<exists>m>0. ?P m" apply auto apply (rule exI[where x=1]) by (simp add: modeq_def)} |
800 moreover |
800 moreover |
801 {assume "n\<noteq>0 \<and> n\<noteq>1" hence n2:"n \<ge> 2" by arith |
801 {assume "n\<noteq>0 \<and> n\<noteq>1" hence n2:"n \<ge> 2" by arith |
802 from na have na': "coprime a n" by (simp add: coprime_commute) |
802 from na have na': "coprime a n" by (simp add: coprime_commute) |
803 from phi_lowerbound_1[OF n2] fermat_little[OF na'] |
803 have ex: "\<exists>m>0. ?P m" |
804 have ex: "\<exists>m>0. ?P m" by - (rule exI[where x="\<phi> n"], auto) } |
804 by (rule exI[where x="\<phi> n"]) (use phi_lowerbound_1[OF n2] fermat_little[OF na'] in auto) } |
805 ultimately have ex: "\<exists>m>0. ?P m" by blast |
805 ultimately have ex: "\<exists>m>0. ?P m" by blast |
806 from nat_exists_least_iff'[of ?P] ex na show ?thesis |
806 from nat_exists_least_iff'[of ?P] ex na show ?thesis |
807 unfolding o[symmetric] by auto |
807 unfolding o[symmetric] by auto |
808 qed |
808 qed |
809 (* With the special value 0 for non-coprime case, it's more convenient. *) |
809 (* With the special value 0 for non-coprime case, it's more convenient. *) |
990 {assume H: ?rhs |
990 {assume H: ?rhs |
991 {fix d assume d: "d dvd n" "d\<^sup>2 \<le> n" "d\<noteq>1" |
991 {fix d assume d: "d dvd n" "d\<^sup>2 \<le> n" "d\<noteq>1" |
992 from prime_factor[OF d(3)] |
992 from prime_factor[OF d(3)] |
993 obtain p where p: "prime p" "p dvd d" by blast |
993 obtain p where p: "prime p" "p dvd d" by blast |
994 from n have np: "n > 0" by arith |
994 from n have np: "n > 0" by arith |
995 from d(1) n have "d \<noteq> 0" by - (rule ccontr, auto) |
995 have "d \<noteq> 0" by (rule ccontr) (use d(1) n in auto) |
996 hence dp: "d > 0" by arith |
996 hence dp: "d > 0" by arith |
997 from mult_mono[OF dvd_imp_le[OF p(2) dp] dvd_imp_le[OF p(2) dp]] d(2) |
997 from mult_mono[OF dvd_imp_le[OF p(2) dp] dvd_imp_le[OF p(2) dp]] d(2) |
998 have "p\<^sup>2 \<le> n" unfolding power2_eq_square by arith |
998 have "p\<^sup>2 \<le> n" unfolding power2_eq_square by arith |
999 with H n p(1) dvd_trans[OF p(2) d(1)] have False by blast} |
999 with H n p(1) dvd_trans[OF p(2) d(1)] have False by blast} |
1000 with n prime_divisor_sqrt have ?lhs by auto} |
1000 with n prime_divisor_sqrt have ?lhs by auto} |
1027 {assume d1: "d \<noteq> 1" |
1027 {assume d1: "d \<noteq> 1" |
1028 from prime_factor[OF d1] obtain P where P: "prime P" "P dvd d" by blast |
1028 from prime_factor[OF d1] obtain P where P: "prime P" "P dvd d" by blast |
1029 from d dvd_mult[OF P(2), of "ord p (a^r)"] have Pq: "P dvd q" by simp |
1029 from d dvd_mult[OF P(2), of "ord p (a^r)"] have Pq: "P dvd q" by simp |
1030 from aq P(1) Pq have caP:"coprime (a^ ((n - 1) div P) - 1) n" by blast |
1030 from aq P(1) Pq have caP:"coprime (a^ ((n - 1) div P) - 1) n" by blast |
1031 from Pq obtain s where s: "q = P*s" unfolding dvd_def by blast |
1031 from Pq obtain s where s: "q = P*s" unfolding dvd_def by blast |
1032 have P0: "P \<noteq> 0" using P(1) prime_0 by - (rule ccontr, simp) |
1032 have P0: "P \<noteq> 0" by (rule ccontr) (use P(1) prime_0 in simp) |
1033 from P(2) obtain t where t: "d = P*t" unfolding dvd_def by blast |
1033 from P(2) obtain t where t: "d = P*t" unfolding dvd_def by blast |
1034 from d s t P0 have s': "ord p (a^r) * t = s" by algebra |
1034 from d s t P0 have s': "ord p (a^r) * t = s" by algebra |
1035 have "ord p (a^r) * t*r = r * ord p (a^r) * t" by algebra |
1035 have "ord p (a^r) * t*r = r * ord p (a^r) * t" by algebra |
1036 hence exps: "a^(ord p (a^r) * t*r) = ((a ^ r) ^ ord p (a^r)) ^ t" |
1036 hence exps: "a^(ord p (a^r) * t*r) = ((a ^ r) ^ ord p (a^r)) ^ t" |
1037 by (simp only: power_mult) |
1037 by (simp only: power_mult) |
1050 from pp[unfolded prime_def] d have dp: "d = p" by blast |
1050 from pp[unfolded prime_def] d have dp: "d = p" by blast |
1051 from n have n12:"Suc (n - 2) = n - 1" by arith |
1051 from n have n12:"Suc (n - 2) = n - 1" by arith |
1052 with divides_rexp[OF d(2)[unfolded dp], of "n - 2"] |
1052 with divides_rexp[OF d(2)[unfolded dp], of "n - 2"] |
1053 have th0: "p dvd a ^ (n - 1)" by simp |
1053 have th0: "p dvd a ^ (n - 1)" by simp |
1054 from n have n0: "n \<noteq> 0" by simp |
1054 from n have n0: "n \<noteq> 0" by simp |
1055 from d(2) an n12[symmetric] have a0: "a \<noteq> 0" |
1055 have a0: "a \<noteq> 0" |
1056 by - (rule ccontr, simp add: modeq_def) |
1056 by (rule ccontr) (use d(2) an n12[symmetric] in \<open>simp add: modeq_def\<close>) |
1057 have th1: "a^ (n - 1) \<noteq> 0" using n d(2) dp a0 by auto |
1057 have th1: "a^ (n - 1) \<noteq> 0" using n d(2) dp a0 by auto |
1058 from coprime_minus1[OF th1, unfolded coprime] |
1058 from coprime_minus1[OF th1, unfolded coprime] |
1059 dvd_trans[OF pn cong_1_divides[OF an]] th0 d(3) dp |
1059 dvd_trans[OF pn cong_1_divides[OF an]] th0 d(3) dp |
1060 have False by auto} |
1060 have False by auto} |
1061 hence cpa: "coprime p a" using coprime by auto |
1061 hence cpa: "coprime p a" using coprime by auto |
1062 from coprime_exp[OF cpa, of r] coprime_commute |
1062 from coprime_exp[OF cpa, of r] coprime_commute |
1063 have arp: "coprime (a^r) p" by blast |
1063 have arp: "coprime (a^r) p" by blast |
1064 from fermat_little[OF arp, simplified ord_divides] o phip |
1064 from fermat_little[OF arp, simplified ord_divides] o phip |
1065 have "q dvd (p - 1)" by simp |
1065 have "q dvd (p - 1)" by simp |
1066 then obtain d where d:"p - 1 = q * d" unfolding dvd_def by blast |
1066 then obtain d where d:"p - 1 = q * d" unfolding dvd_def by blast |
1067 from prime_0 pp have p0:"p \<noteq> 0" by - (rule ccontr, auto) |
1067 have p0: "p \<noteq> 0" by (rule ccontr) (use prime_0 pp in auto) |
1068 from p0 d have "p + q * 0 = 1 + q * d" by simp |
1068 from p0 d have "p + q * 0 = 1 + q * d" by simp |
1069 with nat_mod[of p 1 q, symmetric] |
1069 with nat_mod[of p 1 q, symmetric] |
1070 show ?thesis by blast |
1070 show ?thesis by blast |
1071 qed |
1071 qed |
1072 |
1072 |