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