src/HOL/Old_Number_Theory/Gauss.thy
author wenzelm
Sat Oct 10 16:26:23 2015 +0200 (2015-10-10)
changeset 61382 efac889fccbc
parent 58889 5b7a9633cfa8
child 63566 e5abbdee461a
permissions -rw-r--r--
isabelle update_cartouches;
     1 (*  Title:      HOL/Old_Number_Theory/Gauss.thy
     2     Authors:    Jeremy Avigad, David Gray, and Adam Kramer
     3 *)
     4 
     5 section \<open>Gauss' Lemma\<close>
     6 
     7 theory Gauss
     8 imports Euler
     9 begin
    10 
    11 locale GAUSS =
    12   fixes p :: "int"
    13   fixes a :: "int"
    14 
    15   assumes p_prime: "zprime p"
    16   assumes p_g_2: "2 < p"
    17   assumes p_a_relprime: "~[a = 0](mod p)"
    18   assumes a_nonzero:    "0 < a"
    19 begin
    20 
    21 definition "A = {(x::int). 0 < x & x \<le> ((p - 1) div 2)}"
    22 definition "B = (%x. x * a) ` A"
    23 definition "C = StandardRes p ` B"
    24 definition "D = C \<inter> {x. x \<le> ((p - 1) div 2)}"
    25 definition "E = C \<inter> {x. ((p - 1) div 2) < x}"
    26 definition "F = (%x. (p - x)) ` E"
    27 
    28 
    29 subsection \<open>Basic properties of p\<close>
    30 
    31 lemma p_odd: "p \<in> zOdd"
    32   by (auto simp add: p_prime p_g_2 zprime_zOdd_eq_grt_2)
    33 
    34 lemma p_g_0: "0 < p"
    35   using p_g_2 by auto
    36 
    37 lemma int_nat: "int (nat ((p - 1) div 2)) = (p - 1) div 2"
    38   using ListMem.insert p_g_2 by (auto simp add: pos_imp_zdiv_nonneg_iff)
    39 
    40 lemma p_minus_one_l: "(p - 1) div 2 < p"
    41 proof -
    42   have "(p - 1) div 2 \<le> (p - 1) div 1"
    43     by (rule zdiv_mono2) (auto simp add: p_g_0)
    44   also have "\<dots> = p - 1" by simp
    45   finally show ?thesis by simp
    46 qed
    47 
    48 lemma p_eq: "p = (2 * (p - 1) div 2) + 1"
    49   using div_mult_self1_is_id [of 2 "p - 1"] by auto
    50 
    51 
    52 lemma (in -) zodd_imp_zdiv_eq: "x \<in> zOdd ==> 2 * (x - 1) div 2 = 2 * ((x - 1) div 2)"
    53   apply (frule odd_minus_one_even)
    54   apply (simp add: zEven_def)
    55   apply (subgoal_tac "2 \<noteq> 0")
    56   apply (frule_tac b = "2 :: int" and a = "x - 1" in div_mult_self1_is_id)
    57   apply (auto simp add: even_div_2_prop2)
    58   done
    59 
    60 
    61 lemma p_eq2: "p = (2 * ((p - 1) div 2)) + 1"
    62   apply (insert p_eq p_prime p_g_2 zprime_zOdd_eq_grt_2 [of p], auto)
    63   apply (frule zodd_imp_zdiv_eq, auto)
    64   done
    65 
    66 
    67 subsection \<open>Basic Properties of the Gauss Sets\<close>
    68 
    69 lemma finite_A: "finite (A)"
    70 by (auto simp add: A_def)
    71 
    72 lemma finite_B: "finite (B)"
    73 by (auto simp add: B_def finite_A)
    74 
    75 lemma finite_C: "finite (C)"
    76 by (auto simp add: C_def finite_B)
    77 
    78 lemma finite_D: "finite (D)"
    79 by (auto simp add: D_def finite_C)
    80 
    81 lemma finite_E: "finite (E)"
    82 by (auto simp add: E_def finite_C)
    83 
    84 lemma finite_F: "finite (F)"
    85 by (auto simp add: F_def finite_E)
    86 
    87 lemma C_eq: "C = D \<union> E"
    88 by (auto simp add: C_def D_def E_def)
    89 
    90 lemma A_card_eq: "card A = nat ((p - 1) div 2)"
    91   apply (auto simp add: A_def)
    92   apply (insert int_nat)
    93   apply (erule subst)
    94   apply (auto simp add: card_bdd_int_set_l_le)
    95   done
    96 
    97 lemma inj_on_xa_A: "inj_on (%x. x * a) A"
    98   using a_nonzero by (simp add: A_def inj_on_def)
    99 
   100 lemma A_res: "ResSet p A"
   101   apply (auto simp add: A_def ResSet_def)
   102   apply (rule_tac m = p in zcong_less_eq)
   103   apply (insert p_g_2, auto)
   104   done
   105 
   106 lemma B_res: "ResSet p B"
   107   apply (insert p_g_2 p_a_relprime p_minus_one_l)
   108   apply (auto simp add: B_def)
   109   apply (rule ResSet_image)
   110   apply (auto simp add: A_res)
   111   apply (auto simp add: A_def)
   112 proof -
   113   fix x fix y
   114   assume a: "[x * a = y * a] (mod p)"
   115   assume b: "0 < x"
   116   assume c: "x \<le> (p - 1) div 2"
   117   assume d: "0 < y"
   118   assume e: "y \<le> (p - 1) div 2"
   119   from a p_a_relprime p_prime a_nonzero zcong_cancel [of p a x y]
   120   have "[x = y](mod p)"
   121     by (simp add: zprime_imp_zrelprime zcong_def p_g_0 order_le_less)
   122   with zcong_less_eq [of x y p] p_minus_one_l
   123       order_le_less_trans [of x "(p - 1) div 2" p]
   124       order_le_less_trans [of y "(p - 1) div 2" p] show "x = y"
   125     by (simp add: b c d e p_minus_one_l p_g_0)
   126 qed
   127 
   128 lemma SR_B_inj: "inj_on (StandardRes p) B"
   129   apply (auto simp add: B_def StandardRes_def inj_on_def A_def)
   130 proof -
   131   fix x fix y
   132   assume a: "x * a mod p = y * a mod p"
   133   assume b: "0 < x"
   134   assume c: "x \<le> (p - 1) div 2"
   135   assume d: "0 < y"
   136   assume e: "y \<le> (p - 1) div 2"
   137   assume f: "x \<noteq> y"
   138   from a have "[x * a = y * a](mod p)"
   139     by (simp add: zcong_zmod_eq p_g_0)
   140   with p_a_relprime p_prime a_nonzero zcong_cancel [of p a x y]
   141   have "[x = y](mod p)"
   142     by (simp add: zprime_imp_zrelprime zcong_def p_g_0 order_le_less)
   143   with zcong_less_eq [of x y p] p_minus_one_l
   144     order_le_less_trans [of x "(p - 1) div 2" p]
   145     order_le_less_trans [of y "(p - 1) div 2" p] have "x = y"
   146     by (simp add: b c d e p_minus_one_l p_g_0)
   147   then have False
   148     by (simp add: f)
   149   then show "a = 0"
   150     by simp
   151 qed
   152 
   153 lemma inj_on_pminusx_E: "inj_on (%x. p - x) E"
   154   apply (auto simp add: E_def C_def B_def A_def)
   155   apply (rule_tac g = "%x. -1 * (x - p)" in inj_on_inverseI)
   156   apply auto
   157   done
   158 
   159 lemma A_ncong_p: "x \<in> A ==> ~[x = 0](mod p)"
   160   apply (auto simp add: A_def)
   161   apply (frule_tac m = p in zcong_not_zero)
   162   apply (insert p_minus_one_l)
   163   apply auto
   164   done
   165 
   166 lemma A_greater_zero: "x \<in> A ==> 0 < x"
   167   by (auto simp add: A_def)
   168 
   169 lemma B_ncong_p: "x \<in> B ==> ~[x = 0](mod p)"
   170   apply (auto simp add: B_def)
   171   apply (frule A_ncong_p)
   172   apply (insert p_a_relprime p_prime a_nonzero)
   173   apply (frule_tac a = xa and b = a in zcong_zprime_prod_zero_contra)
   174   apply (auto simp add: A_greater_zero)
   175   done
   176 
   177 lemma B_greater_zero: "x \<in> B ==> 0 < x"
   178   using a_nonzero by (auto simp add: B_def A_greater_zero)
   179 
   180 lemma C_ncong_p: "x \<in> C ==>  ~[x = 0](mod p)"
   181   apply (auto simp add: C_def)
   182   apply (frule B_ncong_p)
   183   apply (subgoal_tac "[xa = StandardRes p xa](mod p)")
   184   defer apply (simp add: StandardRes_prop1)
   185   apply (frule_tac a = xa and b = "StandardRes p xa" and c = 0 in zcong_trans)
   186   apply auto
   187   done
   188 
   189 lemma C_greater_zero: "y \<in> C ==> 0 < y"
   190   apply (auto simp add: C_def)
   191 proof -
   192   fix x
   193   assume a: "x \<in> B"
   194   from p_g_0 have "0 \<le> StandardRes p x"
   195     by (simp add: StandardRes_lbound)
   196   moreover have "~[x = 0] (mod p)"
   197     by (simp add: a B_ncong_p)
   198   then have "StandardRes p x \<noteq> 0"
   199     by (simp add: StandardRes_prop3)
   200   ultimately show "0 < StandardRes p x"
   201     by (simp add: order_le_less)
   202 qed
   203 
   204 lemma D_ncong_p: "x \<in> D ==> ~[x = 0](mod p)"
   205   by (auto simp add: D_def C_ncong_p)
   206 
   207 lemma E_ncong_p: "x \<in> E ==> ~[x = 0](mod p)"
   208   by (auto simp add: E_def C_ncong_p)
   209 
   210 lemma F_ncong_p: "x \<in> F ==> ~[x = 0](mod p)"
   211   apply (auto simp add: F_def)
   212 proof -
   213   fix x assume a: "x \<in> E" assume b: "[p - x = 0] (mod p)"
   214   from E_ncong_p have "~[x = 0] (mod p)"
   215     by (simp add: a)
   216   moreover from a have "0 < x"
   217     by (simp add: a E_def C_greater_zero)
   218   moreover from a have "x < p"
   219     by (auto simp add: E_def C_def p_g_0 StandardRes_ubound)
   220   ultimately have "~[p - x = 0] (mod p)"
   221     by (simp add: zcong_not_zero)
   222   from this show False by (simp add: b)
   223 qed
   224 
   225 lemma F_subset: "F \<subseteq> {x. 0 < x & x \<le> ((p - 1) div 2)}"
   226   apply (auto simp add: F_def E_def)
   227   apply (insert p_g_0)
   228   apply (frule_tac x = xa in StandardRes_ubound)
   229   apply (frule_tac x = x in StandardRes_ubound)
   230   apply (subgoal_tac "xa = StandardRes p xa")
   231   apply (auto simp add: C_def StandardRes_prop2 StandardRes_prop1)
   232 proof -
   233   from zodd_imp_zdiv_eq p_prime p_g_2 zprime_zOdd_eq_grt_2 have
   234     "2 * (p - 1) div 2 = 2 * ((p - 1) div 2)"
   235     by simp
   236   with p_eq2 show " !!x. [| (p - 1) div 2 < StandardRes p x; x \<in> B |]
   237       ==> p - StandardRes p x \<le> (p - 1) div 2"
   238     by simp
   239 qed
   240 
   241 lemma D_subset: "D \<subseteq> {x. 0 < x & x \<le> ((p - 1) div 2)}"
   242   by (auto simp add: D_def C_greater_zero)
   243 
   244 lemma F_eq: "F = {x. \<exists>y \<in> A. ( x = p - (StandardRes p (y*a)) & (p - 1) div 2 < StandardRes p (y*a))}"
   245   by (auto simp add: F_def E_def D_def C_def B_def A_def)
   246 
   247 lemma D_eq: "D = {x. \<exists>y \<in> A. ( x = StandardRes p (y*a) & StandardRes p (y*a) \<le> (p - 1) div 2)}"
   248   by (auto simp add: D_def C_def B_def A_def)
   249 
   250 lemma D_leq: "x \<in> D ==> x \<le> (p - 1) div 2"
   251   by (auto simp add: D_eq)
   252 
   253 lemma F_ge: "x \<in> F ==> x \<le> (p - 1) div 2"
   254   apply (auto simp add: F_eq A_def)
   255 proof -
   256   fix y
   257   assume "(p - 1) div 2 < StandardRes p (y * a)"
   258   then have "p - StandardRes p (y * a) < p - ((p - 1) div 2)"
   259     by arith
   260   also from p_eq2 have "... = 2 * ((p - 1) div 2) + 1 - ((p - 1) div 2)"
   261     by auto
   262   also have "2 * ((p - 1) div 2) + 1 - (p - 1) div 2 = (p - 1) div 2 + 1"
   263     by arith
   264   finally show "p - StandardRes p (y * a) \<le> (p - 1) div 2"
   265     using zless_add1_eq [of "p - StandardRes p (y * a)" "(p - 1) div 2"] by auto
   266 qed
   267 
   268 lemma all_A_relprime: "\<forall>x \<in> A. zgcd x p = 1"
   269   using p_prime p_minus_one_l by (auto simp add: A_def zless_zprime_imp_zrelprime)
   270 
   271 lemma A_prod_relprime: "zgcd (setprod id A) p = 1"
   272 by(rule all_relprime_prod_relprime[OF finite_A all_A_relprime])
   273 
   274 
   275 subsection \<open>Relationships Between Gauss Sets\<close>
   276 
   277 lemma B_card_eq_A: "card B = card A"
   278   using finite_A by (simp add: finite_A B_def inj_on_xa_A card_image)
   279 
   280 lemma B_card_eq: "card B = nat ((p - 1) div 2)"
   281   by (simp add: B_card_eq_A A_card_eq)
   282 
   283 lemma F_card_eq_E: "card F = card E"
   284   using finite_E by (simp add: F_def inj_on_pminusx_E card_image)
   285 
   286 lemma C_card_eq_B: "card C = card B"
   287   apply (insert finite_B)
   288   apply (subgoal_tac "inj_on (StandardRes p) B")
   289   apply (simp add: B_def C_def card_image)
   290   apply (rule StandardRes_inj_on_ResSet)
   291   apply (simp add: B_res)
   292   done
   293 
   294 lemma D_E_disj: "D \<inter> E = {}"
   295   by (auto simp add: D_def E_def)
   296 
   297 lemma C_card_eq_D_plus_E: "card C = card D + card E"
   298   by (auto simp add: C_eq card_Un_disjoint D_E_disj finite_D finite_E)
   299 
   300 lemma C_prod_eq_D_times_E: "setprod id E * setprod id D = setprod id C"
   301   apply (insert D_E_disj finite_D finite_E C_eq)
   302   apply (frule setprod.union_disjoint [of D E id])
   303   apply auto
   304   done
   305 
   306 lemma C_B_zcong_prod: "[setprod id C = setprod id B] (mod p)"
   307   apply (auto simp add: C_def)
   308   apply (insert finite_B SR_B_inj)
   309   apply (frule setprod.reindex [of "StandardRes p" B id])
   310   apply auto
   311   apply (rule setprod_same_function_zcong)
   312   apply (auto simp add: StandardRes_prop1 zcong_sym p_g_0)
   313   done
   314 
   315 lemma F_Un_D_subset: "(F \<union> D) \<subseteq> A"
   316   apply (rule Un_least)
   317   apply (auto simp add: A_def F_subset D_subset)
   318   done
   319 
   320 lemma F_D_disj: "(F \<inter> D) = {}"
   321   apply (simp add: F_eq D_eq)
   322   apply (auto simp add: F_eq D_eq)
   323 proof -
   324   fix y fix ya
   325   assume "p - StandardRes p (y * a) = StandardRes p (ya * a)"
   326   then have "p = StandardRes p (y * a) + StandardRes p (ya * a)"
   327     by arith
   328   moreover have "p dvd p"
   329     by auto
   330   ultimately have "p dvd (StandardRes p (y * a) + StandardRes p (ya * a))"
   331     by auto
   332   then have a: "[StandardRes p (y * a) + StandardRes p (ya * a) = 0] (mod p)"
   333     by (auto simp add: zcong_def)
   334   have "[y * a = StandardRes p (y * a)] (mod p)"
   335     by (simp only: zcong_sym StandardRes_prop1)
   336   moreover have "[ya * a = StandardRes p (ya * a)] (mod p)"
   337     by (simp only: zcong_sym StandardRes_prop1)
   338   ultimately have "[y * a + ya * a =
   339     StandardRes p (y * a) + StandardRes p (ya * a)] (mod p)"
   340     by (rule zcong_zadd)
   341   with a have "[y * a + ya * a = 0] (mod p)"
   342     apply (elim zcong_trans)
   343     by (simp only: zcong_refl)
   344   also have "y * a + ya * a = a * (y + ya)"
   345     by (simp add: distrib_left mult.commute)
   346   finally have "[a * (y + ya) = 0] (mod p)" .
   347   with p_prime a_nonzero zcong_zprime_prod_zero [of p a "y + ya"]
   348     p_a_relprime
   349   have a: "[y + ya = 0] (mod p)"
   350     by auto
   351   assume b: "y \<in> A" and c: "ya: A"
   352   with A_def have "0 < y + ya"
   353     by auto
   354   moreover from b c A_def have "y + ya \<le> (p - 1) div 2 + (p - 1) div 2"
   355     by auto
   356   moreover from b c p_eq2 A_def have "y + ya < p"
   357     by auto
   358   ultimately show False
   359     apply simp
   360     apply (frule_tac m = p in zcong_not_zero)
   361     apply (auto simp add: a)
   362     done
   363 qed
   364 
   365 lemma F_Un_D_card: "card (F \<union> D) = nat ((p - 1) div 2)"
   366 proof -
   367   have "card (F \<union> D) = card E + card D"
   368     by (auto simp add: finite_F finite_D F_D_disj
   369       card_Un_disjoint F_card_eq_E)
   370   then have "card (F \<union> D) = card C"
   371     by (simp add: C_card_eq_D_plus_E)
   372   from this show "card (F \<union> D) = nat ((p - 1) div 2)"
   373     by (simp add: C_card_eq_B B_card_eq)
   374 qed
   375 
   376 lemma F_Un_D_eq_A: "F \<union> D = A"
   377   using finite_A F_Un_D_subset A_card_eq F_Un_D_card by (auto simp add: card_seteq)
   378 
   379 lemma prod_D_F_eq_prod_A:
   380     "(setprod id D) * (setprod id F) = setprod id A"
   381   apply (insert F_D_disj finite_D finite_F)
   382   apply (frule setprod.union_disjoint [of F D id])
   383   apply (auto simp add: F_Un_D_eq_A)
   384   done
   385 
   386 lemma prod_F_zcong:
   387   "[setprod id F = ((-1) ^ (card E)) * (setprod id E)] (mod p)"
   388 proof -
   389   have "setprod id F = setprod id (op - p ` E)"
   390     by (auto simp add: F_def)
   391   then have "setprod id F = setprod (op - p) E"
   392     apply simp
   393     apply (insert finite_E inj_on_pminusx_E)
   394     apply (frule setprod.reindex [of "minus p" E id])
   395     apply auto
   396     done
   397   then have one:
   398     "[setprod id F = setprod (StandardRes p o (op - p)) E] (mod p)"
   399     apply simp
   400     apply (insert p_g_0 finite_E StandardRes_prod)
   401     by (auto)
   402   moreover have a: "\<forall>x \<in> E. [p - x = 0 - x] (mod p)"
   403     apply clarify
   404     apply (insert zcong_id [of p])
   405     apply (rule_tac a = p and m = p and c = x and d = x in zcong_zdiff, auto)
   406     done
   407   moreover have b: "\<forall>x \<in> E. [StandardRes p (p - x) = p - x](mod p)"
   408     apply clarify
   409     apply (simp add: StandardRes_prop1 zcong_sym)
   410     done
   411   moreover have "\<forall>x \<in> E. [StandardRes p (p - x) = - x](mod p)"
   412     apply clarify
   413     apply (insert a b)
   414     apply (rule_tac b = "p - x" in zcong_trans, auto)
   415     done
   416   ultimately have c:
   417     "[setprod (StandardRes p o (op - p)) E = setprod (uminus) E](mod p)"
   418     apply simp
   419     using finite_E p_g_0
   420       setprod_same_function_zcong [of E "StandardRes p o (op - p)" uminus p]
   421     by auto
   422   then have two: "[setprod id F = setprod (uminus) E](mod p)"
   423     apply (insert one c)
   424     apply (rule zcong_trans [of "setprod id F"
   425                                "setprod (StandardRes p o op - p) E" p
   426                                "setprod uminus E"], auto)
   427     done
   428   also have "setprod uminus E = (setprod id E) * (-1)^(card E)"
   429     using finite_E by (induct set: finite) auto
   430   then have "setprod uminus E = (-1) ^ (card E) * (setprod id E)"
   431     by (simp add: mult.commute)
   432   with two show ?thesis
   433     by simp
   434 qed
   435 
   436 
   437 subsection \<open>Gauss' Lemma\<close>
   438 
   439 lemma aux: "setprod id A * (- 1) ^ card E * a ^ card A * (- 1) ^ card E = setprod id A * a ^ card A"
   440   by (auto simp add: finite_E neg_one_special)
   441 
   442 theorem pre_gauss_lemma:
   443   "[a ^ nat((p - 1) div 2) = (-1) ^ (card E)] (mod p)"
   444 proof -
   445   have "[setprod id A = setprod id F * setprod id D](mod p)"
   446     by (auto simp add: prod_D_F_eq_prod_A mult.commute cong del:setprod.cong)
   447   then have "[setprod id A = ((-1)^(card E) * setprod id E) *
   448       setprod id D] (mod p)"
   449     apply (rule zcong_trans)
   450     apply (auto simp add: prod_F_zcong zcong_scalar cong del: setprod.cong)
   451     done
   452   then have "[setprod id A = ((-1)^(card E) * setprod id C)] (mod p)"
   453     apply (rule zcong_trans)
   454     apply (insert C_prod_eq_D_times_E, erule subst)
   455     apply (subst mult.assoc, auto)
   456     done
   457   then have "[setprod id A = ((-1)^(card E) * setprod id B)] (mod p)"
   458     apply (rule zcong_trans)
   459     apply (simp add: C_B_zcong_prod zcong_scalar2 cong del:setprod.cong)
   460     done
   461   then have "[setprod id A = ((-1)^(card E) *
   462     (setprod id ((%x. x * a) ` A)))] (mod p)"
   463     by (simp add: B_def)
   464   then have "[setprod id A = ((-1)^(card E) * (setprod (%x. x * a) A))]
   465     (mod p)"
   466     by (simp add:finite_A inj_on_xa_A setprod.reindex cong del:setprod.cong)
   467   moreover have "setprod (%x. x * a) A =
   468     setprod (%x. a) A * setprod id A"
   469     using finite_A by (induct set: finite) auto
   470   ultimately have "[setprod id A = ((-1)^(card E) * (setprod (%x. a) A *
   471     setprod id A))] (mod p)"
   472     by simp
   473   then have "[setprod id A = ((-1)^(card E) * a^(card A) *
   474       setprod id A)](mod p)"
   475     apply (rule zcong_trans)
   476     apply (simp add: zcong_scalar2 zcong_scalar finite_A setprod_constant mult.assoc)
   477     done
   478   then have a: "[setprod id A * (-1)^(card E) =
   479       ((-1)^(card E) * a^(card A) * setprod id A * (-1)^(card E))](mod p)"
   480     by (rule zcong_scalar)
   481   then have "[setprod id A * (-1)^(card E) = setprod id A *
   482       (-1)^(card E) * a^(card A) * (-1)^(card E)](mod p)"
   483     apply (rule zcong_trans)
   484     apply (simp add: a mult.commute mult.left_commute)
   485     done
   486   then have "[setprod id A * (-1)^(card E) = setprod id A *
   487       a^(card A)](mod p)"
   488     apply (rule zcong_trans)
   489     apply (simp add: aux cong del:setprod.cong)
   490     done
   491   with this zcong_cancel2 [of p "setprod id A" "(- 1) ^ card E" "a ^ card A"]
   492       p_g_0 A_prod_relprime have "[(- 1) ^ card E = a ^ card A](mod p)"
   493     by (simp add: order_less_imp_le)
   494   from this show ?thesis
   495     by (simp add: A_card_eq zcong_sym)
   496 qed
   497 
   498 theorem gauss_lemma: "(Legendre a p) = (-1) ^ (card E)"
   499 proof -
   500   from Euler_Criterion p_prime p_g_2 have
   501       "[(Legendre a p) = a^(nat (((p) - 1) div 2))] (mod p)"
   502     by auto
   503   moreover note pre_gauss_lemma
   504   ultimately have "[(Legendre a p) = (-1) ^ (card E)] (mod p)"
   505     by (rule zcong_trans)
   506   moreover from p_a_relprime have "(Legendre a p) = 1 | (Legendre a p) = (-1)"
   507     by (auto simp add: Legendre_def)
   508   moreover have "(-1::int) ^ (card E) = 1 | (-1::int) ^ (card E) = -1"
   509     by (rule neg_one_power)
   510   ultimately show ?thesis
   511     by (auto simp add: p_g_2 one_not_neg_one_mod_m zcong_sym)
   512 qed
   513 
   514 end
   515 
   516 end