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

Metamath Proof Explorer

Theorem gausslemma2d

Proof