On Sunday, June 20, 2021 at 12:01:38 PM UTC+2 Alexander van der Vekens
wrote:
> 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 could prove ~2lgs now - it's available in the latest version of set.mm.
> 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) ).
>
> I proved the special case of Gauss' lemma (for A = 2, see ~ gausslemma2d
), which was sufficient to prove ~2lgs. The general version of Gauss' lemma
is still unproven. If anybody wants to prove it, the theorem is available
as ~gausslemma in set.mm (commented out).
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/cc9a1cbe-5138-44d6-9c57-dd172791eb5bn%40googlegroups.com.
