equal
deleted
inserted
replaced
115 cong_mult_self_int gcd.commute prime_imp_coprime_int) |
115 cong_mult_self_int gcd.commute prime_imp_coprime_int) |
116 with cong_less_imp_eq_int [of x y p] p_minus_one_l |
116 with cong_less_imp_eq_int [of x y p] p_minus_one_l |
117 order_le_less_trans [of x "(int p - 1) div 2" p] |
117 order_le_less_trans [of x "(int p - 1) div 2" p] |
118 order_le_less_trans [of y "(int p - 1) div 2" p] |
118 order_le_less_trans [of y "(int p - 1) div 2" p] |
119 have "x = y" |
119 have "x = y" |
120 by (metis b c cong_less_imp_eq_int d e zero_less_imp_eq_int zero_zle_int) |
120 by (metis b c cong_less_imp_eq_int d e zero_less_imp_eq_int of_nat_0_le_iff) |
121 } note xy = this |
121 } note xy = this |
122 show ?thesis |
122 show ?thesis |
123 apply (insert p_ge_2 p_a_relprime p_minus_one_l) |
123 apply (insert p_ge_2 p_a_relprime p_minus_one_l) |
124 apply (auto simp add: B_def) |
124 apply (auto simp add: B_def) |
125 apply (rule ResSet_image) |
125 apply (rule ResSet_image) |
139 assume f: "x \<noteq> y" |
139 assume f: "x \<noteq> y" |
140 from a have "[x * a = y * a](mod p)" |
140 from a have "[x * a = y * a](mod p)" |
141 by (metis cong_int_def) |
141 by (metis cong_int_def) |
142 with p_a_relprime p_prime cong_mult_rcancel_int [of a p x y] |
142 with p_a_relprime p_prime cong_mult_rcancel_int [of a p x y] |
143 have "[x = y](mod p)" |
143 have "[x = y](mod p)" |
144 by (metis cong_mult_self_int dvd_div_mult_self gcd_commute_int prime_imp_coprime_int) |
144 by (metis cong_mult_self_int dvd_div_mult_self gcd.commute prime_imp_coprime_int) |
145 with cong_less_imp_eq_int [of x y p] p_minus_one_l |
145 with cong_less_imp_eq_int [of x y p] p_minus_one_l |
146 order_le_less_trans [of x "(int p - 1) div 2" p] |
146 order_le_less_trans [of x "(int p - 1) div 2" p] |
147 order_le_less_trans [of y "(int p - 1) div 2" p] |
147 order_le_less_trans [of y "(int p - 1) div 2" p] |
148 have "x = y" |
148 have "x = y" |
149 by (metis b c cong_less_imp_eq_int d e zero_less_imp_eq_int zero_zle_int) |
149 by (metis b c cong_less_imp_eq_int d e zero_less_imp_eq_int of_nat_0_le_iff) |
150 then have False |
150 then have False |
151 by (simp add: f)} |
151 by (simp add: f)} |
152 then show ?thesis |
152 then show ?thesis |
153 by (auto simp add: B_def inj_on_def A_def) metis |
153 by (auto simp add: B_def inj_on_def A_def) metis |
154 qed |
154 qed |