Metamath Proof Explorer


Theorem gausslemma2d

Description: Gauss' Lemma (see also theorem 9.6 in ApostolNT p. 182) for integer 2 : Let p be an odd prime. Let S = {2, 4, 6, ..., p - 1}. Let n denote the number of elements of S whose least positive residue modulo p is greater than p/2. Then ( 2 | p ) = (-1)^n. (Contributed by AV, 14-Jul-2021)

Ref Expression
Hypotheses gausslemma2d.p φP2
gausslemma2d.h H=P12
gausslemma2d.r R=x1Hifx2<P2x2Px2
gausslemma2d.m M=P4
gausslemma2d.n N=HM
Assertion gausslemma2d φ2/LP=1N

Proof

Step Hyp Ref Expression
1 gausslemma2d.p φP2
2 gausslemma2d.h H=P12
3 gausslemma2d.r R=x1Hifx2<P2x2Px2
4 gausslemma2d.m M=P4
5 gausslemma2d.n N=HM
6 1 2 3 4 5 gausslemma2dlem7 φ1N2HmodP=1
7 eldifi P2P
8 prmnn PP
9 8 nnred PP
10 prmgt1 P1<P
11 9 10 jca PP1<P
12 1 7 11 3syl φP1<P
13 1mod P1<P1modP=1
14 12 13 syl φ1modP=1
15 14 eqcomd φ1=1modP
16 15 eqeq2d φ1N2HmodP=11N2HmodP=1modP
17 neg1z 1
18 1 4 2 5 gausslemma2dlem0h φN0
19 zexpcl 1N01N
20 17 18 19 sylancr φ1N
21 2nn 2
22 21 a1i φ2
23 1 2 gausslemma2dlem0b φH
24 23 nnnn0d φH0
25 22 24 nnexpcld φ2H
26 25 nnzd φ2H
27 20 26 zmulcld φ1N2H
28 27 zred φ1N2H
29 1red φ1
30 28 29 jca φ1N2H1
31 30 adantr φ1N2HmodP=1modP1N2H1
32 1 gausslemma2dlem0a φP
33 32 nnrpd φP+
34 20 33 jca φ1NP+
35 34 adantr φ1N2HmodP=1modP1NP+
36 simpr φ1N2HmodP=1modP1N2HmodP=1modP
37 modmul1 1N2H11NP+1N2HmodP=1modP1N2H1NmodP=11NmodP
38 31 35 36 37 syl3anc φ1N2HmodP=1modP1N2H1NmodP=11NmodP
39 38 ex φ1N2HmodP=1modP1N2H1NmodP=11NmodP
40 20 zcnd φ1N
41 25 nncnd φ2H
42 40 41 40 mul32d φ1N2H1N=1N1N2H
43 18 nn0cnd φN
44 43 2timesd φ2 N=N+N
45 44 eqcomd φN+N=2 N
46 45 oveq2d φ1N+N=12 N
47 neg1cn 1
48 47 a1i φ1
49 48 18 18 expaddd φ1N+N=1N1N
50 18 nn0zd φN
51 m1expeven N12 N=1
52 50 51 syl φ12 N=1
53 46 49 52 3eqtr3d φ1N1N=1
54 53 oveq1d φ1N1N2H=12H
55 41 mulid2d φ12H=2H
56 42 54 55 3eqtrd φ1N2H1N=2H
57 56 oveq1d φ1N2H1NmodP=2HmodP
58 40 mulid2d φ11N=1N
59 58 oveq1d φ11NmodP=1NmodP
60 57 59 eqeq12d φ1N2H1NmodP=11NmodP2HmodP=1NmodP
61 2 oveq2i 2H=2P12
62 61 oveq1i 2HmodP=2P12modP
63 62 eqeq1i 2HmodP=1NmodP2P12modP=1NmodP
64 2z 2
65 lgsvalmod 2P22/LPmodP=2P12modP
66 64 1 65 sylancr φ2/LPmodP=2P12modP
67 66 eqcomd φ2P12modP=2/LPmodP
68 67 eqeq1d φ2P12modP=1NmodP2/LPmodP=1NmodP
69 1 4 2 5 gausslemma2dlem0i φ2/LPmodP=1NmodP2/LP=1N
70 68 69 sylbid φ2P12modP=1NmodP2/LP=1N
71 63 70 syl5bi φ2HmodP=1NmodP2/LP=1N
72 60 71 sylbid φ1N2H1NmodP=11NmodP2/LP=1N
73 39 72 syld φ1N2HmodP=1modP2/LP=1N
74 16 73 sylbid φ1N2HmodP=12/LP=1N
75 6 74 mpd φ2/LP=1N