I started to prove some theorems for Fermat numbers, but I got stuck
because I need the "second supplement to the law of quadratic reciprocity",
i.e the value of the Legendre/Kronecker symbol for 2. The theorem is
available in set.mm ( ~2lgs), but unfortunately without proof (and
commented out).
I think Gauss' Lemma is required for the proof, which could be (formally)
stated as follows:
Let p be an odd prime and a an integer which is not divisible by p. Let
S={a,2a,3a,...,(p-1)a/2}. Let n denote the number of elements of S whose
least positive residue modulo p is greater than p/2. Then ( a | p ) =
(-1)^n.
gausslemma $p |- ( ( ( P e. Prime /\ -. 2 || P ) /\ ( A e. ZZ /\ -. P || A )
/\ N = ( # ` { x e. ZZ | E. i e. ( 1
... ( ( P - 1 ) / 2 ) )
( x = ( i x. A ) /\ ( P / 2 ) < ( x mod P ) ) } ) )
-> ( A /L P ) = ( -u 1 ^ N ) ) $=
? $.
I succeeded already in proving ~2lg on base of ~ gausslemma (with A = 2),
but to prove ~gausslemma would still be tedious (see, for example
https://proofwiki.org/wiki/Gauss%27s_Lemma_(Number_Theory) ).
Is there an alternate way to proof ~2lg? Is there a simple proof for
~gausslemma? Which theorems are already available in set.mm which could
help to finish the proofs for ~2lg and ~gausslemma?
--
You received this message because you are subscribed to the Google Groups
"Metamath" group.
To unsubscribe from this group and stop receiving emails from it, send an email
to [email protected].
To view this discussion on the web visit
https://groups.google.com/d/msgid/metamath/5eb509b0-d6e4-4e49-b59c-d027ae7beb8fn%40googlegroups.com.
