changeset 45627 a0336f8b6558 parent 44890 22f665a2e91c child 45630 0dd654a01217
equal 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"`