2lgs

Description: The second supplement to the law of quadratic reciprocity (for the Legendre symbol extended to arbitrary primes as second argument). Two is a square modulo a prime P iff P == +- 1 (mod 8 ), see first case of theorem 9.5 in ApostolNT p. 181. This theorem justifies our definition of ( N /L 2 ) ( lgs2 ) to some degree, by demanding that reciprocity extend to the case Q = 2 . (Proposed by Mario Carneiro, 19-Jun-2015.) (Contributed by AV, 16-Jul-2021)

		Ref	Expression
	Assertion	2lgs	$⊢ P \in ℙ \to (2 /_{L} P = 1 \leftrightarrow P \mod 8 \in \{1, 7\})$

Proof

Step	Hyp	Ref	Expression
1		prm2orodd	$⊢ P \in ℙ \to (P = 2 \lor \neg 2 ∥ P)$
2		2lgslem4	$⊢ 2 /_{L} 2 = 1 \leftrightarrow 2 \mod 8 \in \{1, 7\}$
3	2	a1i	$⊢ P = 2 \to (2 /_{L} 2 = 1 \leftrightarrow 2 \mod 8 \in \{1, 7\})$
4		oveq2	$⊢ P = 2 \to 2 /_{L} P = 2 /_{L} 2$
5	4	eqeq1d	$⊢ P = 2 \to (2 /_{L} P = 1 \leftrightarrow 2 /_{L} 2 = 1)$
6		oveq1	$⊢ P = 2 \to P \mod 8 = 2 \mod 8$
7	6	eleq1d	$⊢ P = 2 \to (P \mod 8 \in \{1, 7\} \leftrightarrow 2 \mod 8 \in \{1, 7\})$
8	3 5 7	3bitr4d	$⊢ P = 2 \to (2 /_{L} P = 1 \leftrightarrow P \mod 8 \in \{1, 7\})$
9	8	a1d	$⊢ P = 2 \to (P \in ℙ \to (2 /_{L} P = 1 \leftrightarrow P \mod 8 \in \{1, 7\}))$
10		2prm	$⊢ 2 \in ℙ$
11		prmnn	$⊢ P \in ℙ \to P \in ℕ$
12		dvdsprime	$⊢ (2 \in ℙ \land P \in ℕ) \to (P ∥ 2 \leftrightarrow (P = 2 \lor P = 1))$
13	10 11 12	sylancr	$⊢ P \in ℙ \to (P ∥ 2 \leftrightarrow (P = 2 \lor P = 1))$
14		z2even	$⊢ 2 ∥ 2$
15		breq2	$⊢ P = 2 \to (2 ∥ P \leftrightarrow 2 ∥ 2)$
16	14 15	mpbiri	$⊢ P = 2 \to 2 ∥ P$
17	16	a1d	$⊢ P = 2 \to (P \in ℙ \to 2 ∥ P)$
18		eleq1	$⊢ P = 1 \to (P \in ℙ \leftrightarrow 1 \in ℙ)$
19		1nprm	$⊢ \neg 1 \in ℙ$
20	19	pm2.21i	$⊢ 1 \in ℙ \to 2 ∥ P$
21	18 20	syl6bi	$⊢ P = 1 \to (P \in ℙ \to 2 ∥ P)$
22	17 21	jaoi	$⊢ (P = 2 \lor P = 1) \to (P \in ℙ \to 2 ∥ P)$
23	22	com12	$⊢ P \in ℙ \to ((P = 2 \lor P = 1) \to 2 ∥ P)$
24	13 23	sylbid	$⊢ P \in ℙ \to (P ∥ 2 \to 2 ∥ P)$
25	24	con3dimp	$⊢ (P \in ℙ \land \neg 2 ∥ P) \to \neg P ∥ 2$
26		2z	$⊢ 2 \in ℤ$
27	25 26	jctil	$⊢ (P \in ℙ \land \neg 2 ∥ P) \to (2 \in ℤ \land \neg P ∥ 2)$
28		2lgslem1	$⊢ (P \in ℙ \land \neg 2 ∥ P) \to \|\{x \in ℤ \| \exists i \in (1 \dots \frac{P - 1}{2}) (x = i \cdot 2 \land \frac{P}{2} < x \mod P)\}\| = (\frac{P - 1}{2}) - ⌊\frac{P}{4}⌋$
29	28	eqcomd	$⊢ (P \in ℙ \land \neg 2 ∥ P) \to (\frac{P - 1}{2}) - ⌊\frac{P}{4}⌋ = \|\{x \in ℤ \| \exists i \in (1 \dots \frac{P - 1}{2}) (x = i \cdot 2 \land \frac{P}{2} < x \mod P)\}\|$
30		nnoddn2prmb	$⊢ P \in (ℙ ∖ \{2\}) \leftrightarrow (P \in ℙ \land \neg 2 ∥ P)$
31	30	biimpri	$⊢ (P \in ℙ \land \neg 2 ∥ P) \to P \in (ℙ ∖ \{2\})$
32	31	3ad2ant1	$⊢ ((P \in ℙ \land \neg 2 ∥ P) \land (2 \in ℤ \land \neg P ∥ 2) \land (\frac{P - 1}{2}) - ⌊\frac{P}{4}⌋ = \|\{x \in ℤ \| \exists i \in (1 \dots \frac{P - 1}{2}) (x = i \cdot 2 \land \frac{P}{2} < x \mod P)\}\|) \to P \in (ℙ ∖ \{2\})$
33		eqid	$⊢ \frac{P - 1}{2} = \frac{P - 1}{2}$
34		eqid	$⊢ (y \in (1 \dots \frac{P - 1}{2}) ⟼ if (y \cdot 2 < \frac{P}{2}, y \cdot 2, P - y \cdot 2)) = (y \in (1 \dots \frac{P - 1}{2}) ⟼ if (y \cdot 2 < \frac{P}{2}, y \cdot 2, P - y \cdot 2))$
35		eqid	$⊢ ⌊\frac{P}{4}⌋ = ⌊\frac{P}{4}⌋$
36		eqid	$⊢ (\frac{P - 1}{2}) - ⌊\frac{P}{4}⌋ = (\frac{P - 1}{2}) - ⌊\frac{P}{4}⌋$
37	32 33 34 35 36	gausslemma2d	$⊢ ((P \in ℙ \land \neg 2 ∥ P) \land (2 \in ℤ \land \neg P ∥ 2) \land (\frac{P - 1}{2}) - ⌊\frac{P}{4}⌋ = \|\{x \in ℤ \| \exists i \in (1 \dots \frac{P - 1}{2}) (x = i \cdot 2 \land \frac{P}{2} < x \mod P)\}\|) \to 2 /_{L} P = {(- 1)}^{(\frac{P - 1}{2}) - ⌊\frac{P}{4}⌋}$
38	37	eqeq1d	$⊢ ((P \in ℙ \land \neg 2 ∥ P) \land (2 \in ℤ \land \neg P ∥ 2) \land (\frac{P - 1}{2}) - ⌊\frac{P}{4}⌋ = \|\{x \in ℤ \| \exists i \in (1 \dots \frac{P - 1}{2}) (x = i \cdot 2 \land \frac{P}{2} < x \mod P)\}\|) \to (2 /_{L} P = 1 \leftrightarrow {(- 1)}^{(\frac{P - 1}{2}) - ⌊\frac{P}{4}⌋} = 1)$
39	27 29 38	mpd3an23	$⊢ (P \in ℙ \land \neg 2 ∥ P) \to (2 /_{L} P = 1 \leftrightarrow {(- 1)}^{(\frac{P - 1}{2}) - ⌊\frac{P}{4}⌋} = 1)$
40	36	2lgslem2	$⊢ (P \in ℙ \land \neg 2 ∥ P) \to (\frac{P - 1}{2}) - ⌊\frac{P}{4}⌋ \in ℤ$
41		m1exp1	$⊢ (\frac{P - 1}{2}) - ⌊\frac{P}{4}⌋ \in ℤ \to ({(- 1)}^{(\frac{P - 1}{2}) - ⌊\frac{P}{4}⌋} = 1 \leftrightarrow 2 ∥ ((\frac{P - 1}{2}) - ⌊\frac{P}{4}⌋))$
42	40 41	syl	$⊢ (P \in ℙ \land \neg 2 ∥ P) \to ({(- 1)}^{(\frac{P - 1}{2}) - ⌊\frac{P}{4}⌋} = 1 \leftrightarrow 2 ∥ ((\frac{P - 1}{2}) - ⌊\frac{P}{4}⌋))$
43		2nn	$⊢ 2 \in ℕ$
44		dvdsval3	$⊢ (2 \in ℕ \land (\frac{P - 1}{2}) - ⌊\frac{P}{4}⌋ \in ℤ) \to (2 ∥ ((\frac{P - 1}{2}) - ⌊\frac{P}{4}⌋) \leftrightarrow ((\frac{P - 1}{2}) - ⌊\frac{P}{4}⌋) \mod 2 = 0)$
45	43 40 44	sylancr	$⊢ (P \in ℙ \land \neg 2 ∥ P) \to (2 ∥ ((\frac{P - 1}{2}) - ⌊\frac{P}{4}⌋) \leftrightarrow ((\frac{P - 1}{2}) - ⌊\frac{P}{4}⌋) \mod 2 = 0)$
46	36	2lgslem3	$⊢ (P \in ℕ \land \neg 2 ∥ P) \to ((\frac{P - 1}{2}) - ⌊\frac{P}{4}⌋) \mod 2 = if (P \mod 8 \in \{1, 7\}, 0, 1)$
47	11 46	sylan	$⊢ (P \in ℙ \land \neg 2 ∥ P) \to ((\frac{P - 1}{2}) - ⌊\frac{P}{4}⌋) \mod 2 = if (P \mod 8 \in \{1, 7\}, 0, 1)$
48	47	eqeq1d	$⊢ (P \in ℙ \land \neg 2 ∥ P) \to (((\frac{P - 1}{2}) - ⌊\frac{P}{4}⌋) \mod 2 = 0 \leftrightarrow if (P \mod 8 \in \{1, 7\}, 0, 1) = 0)$
49		ax-1	$⊢ P \mod 8 \in \{1, 7\} \to (if (P \mod 8 \in \{1, 7\}, 0, 1) = 0 \to P \mod 8 \in \{1, 7\})$
50		iffalse	$⊢ \neg P \mod 8 \in \{1, 7\} \to if (P \mod 8 \in \{1, 7\}, 0, 1) = 1$
51	50	eqeq1d	$⊢ \neg P \mod 8 \in \{1, 7\} \to (if (P \mod 8 \in \{1, 7\}, 0, 1) = 0 \leftrightarrow 1 = 0)$
52		ax-1ne0	$⊢ 1 \neq 0$
53		eqneqall	$⊢ 1 = 0 \to (1 \neq 0 \to P \mod 8 \in \{1, 7\})$
54	52 53	mpi	$⊢ 1 = 0 \to P \mod 8 \in \{1, 7\}$
55	51 54	syl6bi	$⊢ \neg P \mod 8 \in \{1, 7\} \to (if (P \mod 8 \in \{1, 7\}, 0, 1) = 0 \to P \mod 8 \in \{1, 7\})$
56	49 55	pm2.61i	$⊢ if (P \mod 8 \in \{1, 7\}, 0, 1) = 0 \to P \mod 8 \in \{1, 7\}$
57		iftrue	$⊢ P \mod 8 \in \{1, 7\} \to if (P \mod 8 \in \{1, 7\}, 0, 1) = 0$
58	56 57	impbii	$⊢ if (P \mod 8 \in \{1, 7\}, 0, 1) = 0 \leftrightarrow P \mod 8 \in \{1, 7\}$
59	58	a1i	$⊢ (P \in ℙ \land \neg 2 ∥ P) \to (if (P \mod 8 \in \{1, 7\}, 0, 1) = 0 \leftrightarrow P \mod 8 \in \{1, 7\})$
60	45 48 59	3bitrd	$⊢ (P \in ℙ \land \neg 2 ∥ P) \to (2 ∥ ((\frac{P - 1}{2}) - ⌊\frac{P}{4}⌋) \leftrightarrow P \mod 8 \in \{1, 7\})$
61	39 42 60	3bitrd	$⊢ (P \in ℙ \land \neg 2 ∥ P) \to (2 /_{L} P = 1 \leftrightarrow P \mod 8 \in \{1, 7\})$
62	61	expcom	$⊢ \neg 2 ∥ P \to (P \in ℙ \to (2 /_{L} P = 1 \leftrightarrow P \mod 8 \in \{1, 7\}))$
63	9 62	jaoi	$⊢ (P = 2 \lor \neg 2 ∥ P) \to (P \in ℙ \to (2 /_{L} P = 1 \leftrightarrow P \mod 8 \in \{1, 7\}))$
64	1 63	mpcom	$⊢ P \in ℙ \to (2 /_{L} P = 1 \leftrightarrow P \mod 8 \in \{1, 7\})$

Metamath Proof Explorer

Theorem 2lgs

Proof