src/HOL/Old_Number_Theory/Quadratic_Reciprocity.thy
changeset 45627 a0336f8b6558
parent 44890 22f665a2e91c
child 45630 0dd654a01217
equal deleted inserted replaced
45626:b4f374a45668 45627:a0336f8b6558
   112 
   112 
   113 lemma QRLemma5: "a \<in> zOdd ==>
   113 lemma QRLemma5: "a \<in> zOdd ==>
   114    (-1::int)^(card E) = (-1::int)^(nat(setsum (%x. ((x * a) div p)) A))"
   114    (-1::int)^(card E) = (-1::int)^(nat(setsum (%x. ((x * a) div p)) A))"
   115 proof -
   115 proof -
   116   assume "a \<in> zOdd"
   116   assume "a \<in> zOdd"
   117   from QRLemma4 [OF this] have
   117   from QRLemma4 [OF this, symmetric] have
   118     "(int(card E): zEven) = (setsum (%x. ((x * a) div p)) A \<in> zEven)" ..
   118     "(int(card E): zEven) = (setsum (%x. ((x * a) div p)) A \<in> zEven)" .
   119   moreover have "0 \<le> int(card E)"
   119   moreover have "0 \<le> int(card E)"
   120     by auto
   120     by auto
   121   moreover have "0 \<le> setsum (%x. ((x * a) div p)) A"
   121   moreover have "0 \<le> setsum (%x. ((x * a) div p)) A"
   122     proof (intro setsum_nonneg)
   122     proof (intro setsum_nonneg)
   123       show "\<forall>x \<in> A. 0 \<le> x * a div p"
   123       show "\<forall>x \<in> A. 0 \<le> x * a div p"