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 ↑ 𝑁 ) )