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