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