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 φ P 2
gausslemma2d.h H = P 1 2
gausslemma2d.r R = x 1 H if x 2 < P 2 x 2 P x 2
gausslemma2d.m M = P 4
gausslemma2d.n N = H M
Assertion gausslemma2d φ 2 / L P = 1 N

Proof

Step Hyp Ref Expression
1 gausslemma2d.p φ P 2
2 gausslemma2d.h H = P 1 2
3 gausslemma2d.r R = x 1 H if x 2 < P 2 x 2 P x 2
4 gausslemma2d.m M = P 4
5 gausslemma2d.n N = H M
6 1 2 3 4 5 gausslemma2dlem7 φ 1 N 2 H mod P = 1
7 eldifi P 2 P
8 prmnn P P
9 8 nnred P P
10 prmgt1 P 1 < P
11 9 10 jca P P 1 < P
12 1mod P 1 < P 1 mod P = 1
13 1 7 11 12 4syl φ 1 mod P = 1
14 13 eqcomd φ 1 = 1 mod P
15 14 eqeq2d φ 1 N 2 H mod P = 1 1 N 2 H mod P = 1 mod P
16 neg1z 1
17 1 4 2 5 gausslemma2dlem0h φ N 0
18 zexpcl 1 N 0 1 N
19 16 17 18 sylancr φ 1 N
20 2nn 2
21 20 a1i φ 2
22 1 2 gausslemma2dlem0b φ H
23 22 nnnn0d φ H 0
24 21 23 nnexpcld φ 2 H
25 24 nnzd φ 2 H
26 19 25 zmulcld φ 1 N 2 H
27 26 zred φ 1 N 2 H
28 1red φ 1
29 27 28 jca φ 1 N 2 H 1
30 29 adantr φ 1 N 2 H mod P = 1 mod P 1 N 2 H 1
31 1 gausslemma2dlem0a φ P
32 31 nnrpd φ P +
33 19 32 jca φ 1 N P +
34 33 adantr φ 1 N 2 H mod P = 1 mod P 1 N P +
35 simpr φ 1 N 2 H mod P = 1 mod P 1 N 2 H mod P = 1 mod P
36 modmul1 1 N 2 H 1 1 N P + 1 N 2 H mod P = 1 mod P 1 N 2 H 1 N mod P = 1 1 N mod P
37 30 34 35 36 syl3anc φ 1 N 2 H mod P = 1 mod P 1 N 2 H 1 N mod P = 1 1 N mod P
38 37 ex φ 1 N 2 H mod P = 1 mod P 1 N 2 H 1 N mod P = 1 1 N mod P
39 19 zcnd φ 1 N
40 24 nncnd φ 2 H
41 39 40 39 mul32d φ 1 N 2 H 1 N = 1 N 1 N 2 H
42 17 nn0cnd φ N
43 42 2timesd φ 2 N = N + N
44 43 eqcomd φ N + N = 2 N
45 44 oveq2d φ 1 N + N = 1 2 N
46 neg1cn 1
47 46 a1i φ 1
48 47 17 17 expaddd φ 1 N + N = 1 N 1 N
49 17 nn0zd φ N
50 m1expeven N 1 2 N = 1
51 49 50 syl φ 1 2 N = 1
52 45 48 51 3eqtr3d φ 1 N 1 N = 1
53 52 oveq1d φ 1 N 1 N 2 H = 1 2 H
54 40 mullidd φ 1 2 H = 2 H
55 41 53 54 3eqtrd φ 1 N 2 H 1 N = 2 H
56 55 oveq1d φ 1 N 2 H 1 N mod P = 2 H mod P
57 39 mullidd φ 1 1 N = 1 N
58 57 oveq1d φ 1 1 N mod P = 1 N mod P
59 56 58 eqeq12d φ 1 N 2 H 1 N mod P = 1 1 N mod P 2 H mod P = 1 N mod P
60 2 oveq2i 2 H = 2 P 1 2
61 60 oveq1i 2 H mod P = 2 P 1 2 mod P
62 61 eqeq1i 2 H mod P = 1 N mod P 2 P 1 2 mod P = 1 N mod P
63 2z 2
64 lgsvalmod 2 P 2 2 / L P mod P = 2 P 1 2 mod P
65 63 1 64 sylancr φ 2 / L P mod P = 2 P 1 2 mod P
66 65 eqcomd φ 2 P 1 2 mod P = 2 / L P mod P
67 66 eqeq1d φ 2 P 1 2 mod P = 1 N mod P 2 / L P mod P = 1 N mod P
68 1 4 2 5 gausslemma2dlem0i φ 2 / L P mod P = 1 N mod P 2 / L P = 1 N
69 67 68 sylbid φ 2 P 1 2 mod P = 1 N mod P 2 / L P = 1 N
70 62 69 biimtrid φ 2 H mod P = 1 N mod P 2 / L P = 1 N
71 59 70 sylbid φ 1 N 2 H 1 N mod P = 1 1 N mod P 2 / L P = 1 N
72 38 71 syld φ 1 N 2 H mod P = 1 mod P 2 / L P = 1 N
73 15 72 sylbid φ 1 N 2 H mod P = 1 2 / L P = 1 N
74 6 73 mpd φ 2 / L P = 1 N