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 ( 𝜑𝑃 ∈ ( ℙ ∖ { 2 } ) )
gausslemma2d.h 𝐻 = ( ( 𝑃 − 1 ) / 2 )
gausslemma2d.r 𝑅 = ( 𝑥 ∈ ( 1 ... 𝐻 ) ↦ if ( ( 𝑥 · 2 ) < ( 𝑃 / 2 ) , ( 𝑥 · 2 ) , ( 𝑃 − ( 𝑥 · 2 ) ) ) )
gausslemma2d.m 𝑀 = ( ⌊ ‘ ( 𝑃 / 4 ) )
gausslemma2d.n 𝑁 = ( 𝐻𝑀 )
Assertion gausslemma2d ( 𝜑 → ( 2 /L 𝑃 ) = ( - 1 ↑ 𝑁 ) )

Proof

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