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	$⊢ φ \to P \in (ℙ ∖ \{2\})$
	gausslemma2d.h	$⊢ H = \frac{P - 1}{2}$
	gausslemma2d.r	$⊢ R = (x \in (1 \dots H) ⟼ if (x \cdot 2 < \frac{P}{2}, x \cdot 2, P - x \cdot 2))$
	gausslemma2d.m	$⊢ M = ⌊\frac{P}{4}⌋$
	gausslemma2d.n	$⊢ N = H - M$
Assertion	gausslemma2d	$⊢ φ \to 2 /_{L} P = {(- 1)}^{N}$

Proof

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

Metamath Proof Explorer

Theorem gausslemma2d

Proof