2lgsoddprm

Description: The second supplement to the law of quadratic reciprocity for odd primes (common representation, see theorem 9.5 in ApostolNT p. 181): The Legendre symbol for 2 at an odd prime is minus one to the power of the square of the odd prime minus one divided by eight ( ( 2 /L P ) = -1^(((P^2)-1)/8) ). (Contributed by AV, 20-Jul-2021)

		Ref	Expression
	Assertion	2lgsoddprm	$⊢ P \in (ℙ ∖ \{2\}) \to 2 /_{L} P = {(- 1)}^{\frac{P^{2} - 1}{8}}$

Proof

Step	Hyp	Ref	Expression
1		eldifi	$⊢ P \in (ℙ ∖ \{2\}) \to P \in ℙ$
2		2lgs	$⊢ P \in ℙ \to (2 /_{L} P = 1 \leftrightarrow P \mod 8 \in \{1, 7\})$
3	1 2	syl	$⊢ P \in (ℙ ∖ \{2\}) \to (2 /_{L} P = 1 \leftrightarrow P \mod 8 \in \{1, 7\})$
4		simpl	$⊢ (2 /_{L} P = 1 \land (P \mod 8 \in \{1, 7\} \land P \in (ℙ ∖ \{2\}))) \to 2 /_{L} P = 1$
5		eqcom	$⊢ 1 = {(- 1)}^{\frac{P^{2} - 1}{8}} \leftrightarrow {(- 1)}^{\frac{P^{2} - 1}{8}} = 1$
6	5	a1i	$⊢ P \in (ℙ ∖ \{2\}) \to (1 = {(- 1)}^{\frac{P^{2} - 1}{8}} \leftrightarrow {(- 1)}^{\frac{P^{2} - 1}{8}} = 1)$
7		nnoddn2prm	$⊢ P \in (ℙ ∖ \{2\}) \to (P \in ℕ \land \neg 2 ∥ P)$
8		nnz	$⊢ P \in ℕ \to P \in ℤ$
9	8	anim1i	$⊢ (P \in ℕ \land \neg 2 ∥ P) \to (P \in ℤ \land \neg 2 ∥ P)$
10	7 9	syl	$⊢ P \in (ℙ ∖ \{2\}) \to (P \in ℤ \land \neg 2 ∥ P)$
11		sqoddm1div8z	$⊢ (P \in ℤ \land \neg 2 ∥ P) \to \frac{P^{2} - 1}{8} \in ℤ$
12	10 11	syl	$⊢ P \in (ℙ ∖ \{2\}) \to \frac{P^{2} - 1}{8} \in ℤ$
13		m1exp1	$⊢ \frac{P^{2} - 1}{8} \in ℤ \to ({(- 1)}^{\frac{P^{2} - 1}{8}} = 1 \leftrightarrow 2 ∥ (\frac{P^{2} - 1}{8}))$
14	12 13	syl	$⊢ P \in (ℙ ∖ \{2\}) \to ({(- 1)}^{\frac{P^{2} - 1}{8}} = 1 \leftrightarrow 2 ∥ (\frac{P^{2} - 1}{8}))$
15		2lgsoddprmlem4	$⊢ (P \in ℤ \land \neg 2 ∥ P) \to (2 ∥ (\frac{P^{2} - 1}{8}) \leftrightarrow P \mod 8 \in \{1, 7\})$
16	10 15	syl	$⊢ P \in (ℙ ∖ \{2\}) \to (2 ∥ (\frac{P^{2} - 1}{8}) \leftrightarrow P \mod 8 \in \{1, 7\})$
17	6 14 16	3bitrd	$⊢ P \in (ℙ ∖ \{2\}) \to (1 = {(- 1)}^{\frac{P^{2} - 1}{8}} \leftrightarrow P \mod 8 \in \{1, 7\})$
18	17	biimparc	$⊢ (P \mod 8 \in \{1, 7\} \land P \in (ℙ ∖ \{2\})) \to 1 = {(- 1)}^{\frac{P^{2} - 1}{8}}$
19	18	adantl	$⊢ (2 /_{L} P = 1 \land (P \mod 8 \in \{1, 7\} \land P \in (ℙ ∖ \{2\}))) \to 1 = {(- 1)}^{\frac{P^{2} - 1}{8}}$
20	4 19	eqtrd	$⊢ (2 /_{L} P = 1 \land (P \mod 8 \in \{1, 7\} \land P \in (ℙ ∖ \{2\}))) \to 2 /_{L} P = {(- 1)}^{\frac{P^{2} - 1}{8}}$
21	20	exp32	$⊢ 2 /_{L} P = 1 \to (P \mod 8 \in \{1, 7\} \to (P \in (ℙ ∖ \{2\}) \to 2 /_{L} P = {(- 1)}^{\frac{P^{2} - 1}{8}}))$
22		2z	$⊢ 2 \in ℤ$
23		prmz	$⊢ P \in ℙ \to P \in ℤ$
24	1 23	syl	$⊢ P \in (ℙ ∖ \{2\}) \to P \in ℤ$
25		lgscl1	$⊢ (2 \in ℤ \land P \in ℤ) \to 2 /_{L} P \in \{- 1, 0, 1\}$
26	22 24 25	sylancr	$⊢ P \in (ℙ ∖ \{2\}) \to 2 /_{L} P \in \{- 1, 0, 1\}$
27		ovex	$⊢ 2 /_{L} P \in V$
28	27	eltp	$⊢ 2 /_{L} P \in \{- 1, 0, 1\} \leftrightarrow (2 /_{L} P = - 1 \lor 2 /_{L} P = 0 \lor 2 /_{L} P = 1)$
29		simpl	$⊢ (2 /_{L} P = - 1 \land (P \in (ℙ ∖ \{2\}) \land \neg P \mod 8 \in \{1, 7\})) \to 2 /_{L} P = - 1$
30	16	notbid	$⊢ P \in (ℙ ∖ \{2\}) \to (\neg 2 ∥ (\frac{P^{2} - 1}{8}) \leftrightarrow \neg P \mod 8 \in \{1, 7\})$
31	30	biimpar	$⊢ (P \in (ℙ ∖ \{2\}) \land \neg P \mod 8 \in \{1, 7\}) \to \neg 2 ∥ (\frac{P^{2} - 1}{8})$
32		m1expo	$⊢ (\frac{P^{2} - 1}{8} \in ℤ \land \neg 2 ∥ (\frac{P^{2} - 1}{8})) \to {(- 1)}^{\frac{P^{2} - 1}{8}} = - 1$
33	12 31 32	syl2an2r	$⊢ (P \in (ℙ ∖ \{2\}) \land \neg P \mod 8 \in \{1, 7\}) \to {(- 1)}^{\frac{P^{2} - 1}{8}} = - 1$
34	33	eqcomd	$⊢ (P \in (ℙ ∖ \{2\}) \land \neg P \mod 8 \in \{1, 7\}) \to - 1 = {(- 1)}^{\frac{P^{2} - 1}{8}}$
35	34	adantl	$⊢ (2 /_{L} P = - 1 \land (P \in (ℙ ∖ \{2\}) \land \neg P \mod 8 \in \{1, 7\})) \to - 1 = {(- 1)}^{\frac{P^{2} - 1}{8}}$
36	29 35	eqtrd	$⊢ (2 /_{L} P = - 1 \land (P \in (ℙ ∖ \{2\}) \land \neg P \mod 8 \in \{1, 7\})) \to 2 /_{L} P = {(- 1)}^{\frac{P^{2} - 1}{8}}$
37	36	a1d	$⊢ (2 /_{L} P = - 1 \land (P \in (ℙ ∖ \{2\}) \land \neg P \mod 8 \in \{1, 7\})) \to (\neg 2 /_{L} P = 1 \to 2 /_{L} P = {(- 1)}^{\frac{P^{2} - 1}{8}})$
38	37	exp32	$⊢ 2 /_{L} P = - 1 \to (P \in (ℙ ∖ \{2\}) \to (\neg P \mod 8 \in \{1, 7\} \to (\neg 2 /_{L} P = 1 \to 2 /_{L} P = {(- 1)}^{\frac{P^{2} - 1}{8}})))$
39		eldifsn	$⊢ P \in (ℙ ∖ \{2\}) \leftrightarrow (P \in ℙ \land P \neq 2)$
40		simpr	$⊢ (P \in ℙ \land P \neq 2) \to P \neq 2$
41	40	necomd	$⊢ (P \in ℙ \land P \neq 2) \to 2 \neq P$
42	39 41	sylbi	$⊢ P \in (ℙ ∖ \{2\}) \to 2 \neq P$
43		2prm	$⊢ 2 \in ℙ$
44		prmrp	$⊢ (2 \in ℙ \land P \in ℙ) \to (2 \gcd P = 1 \leftrightarrow 2 \neq P)$
45	43 1 44	sylancr	$⊢ P \in (ℙ ∖ \{2\}) \to (2 \gcd P = 1 \leftrightarrow 2 \neq P)$
46	42 45	mpbird	$⊢ P \in (ℙ ∖ \{2\}) \to 2 \gcd P = 1$
47		lgsne0	$⊢ (2 \in ℤ \land P \in ℤ) \to (2 /_{L} P \neq 0 \leftrightarrow 2 \gcd P = 1)$
48	22 24 47	sylancr	$⊢ P \in (ℙ ∖ \{2\}) \to (2 /_{L} P \neq 0 \leftrightarrow 2 \gcd P = 1)$
49	46 48	mpbird	$⊢ P \in (ℙ ∖ \{2\}) \to 2 /_{L} P \neq 0$
50		eqneqall	$⊢ 2 /_{L} P = 0 \to (2 /_{L} P \neq 0 \to (\neg P \mod 8 \in \{1, 7\} \to (\neg 2 /_{L} P = 1 \to 2 /_{L} P = {(- 1)}^{\frac{P^{2} - 1}{8}})))$
51	49 50	syl5	$⊢ 2 /_{L} P = 0 \to (P \in (ℙ ∖ \{2\}) \to (\neg P \mod 8 \in \{1, 7\} \to (\neg 2 /_{L} P = 1 \to 2 /_{L} P = {(- 1)}^{\frac{P^{2} - 1}{8}})))$
52		pm2.24	$⊢ 2 /_{L} P = 1 \to (\neg 2 /_{L} P = 1 \to 2 /_{L} P = {(- 1)}^{\frac{P^{2} - 1}{8}})$
53	52	2a1d	$⊢ 2 /_{L} P = 1 \to (P \in (ℙ ∖ \{2\}) \to (\neg P \mod 8 \in \{1, 7\} \to (\neg 2 /_{L} P = 1 \to 2 /_{L} P = {(- 1)}^{\frac{P^{2} - 1}{8}})))$
54	38 51 53	3jaoi	$⊢ (2 /_{L} P = - 1 \lor 2 /_{L} P = 0 \lor 2 /_{L} P = 1) \to (P \in (ℙ ∖ \{2\}) \to (\neg P \mod 8 \in \{1, 7\} \to (\neg 2 /_{L} P = 1 \to 2 /_{L} P = {(- 1)}^{\frac{P^{2} - 1}{8}})))$
55	28 54	sylbi	$⊢ 2 /_{L} P \in \{- 1, 0, 1\} \to (P \in (ℙ ∖ \{2\}) \to (\neg P \mod 8 \in \{1, 7\} \to (\neg 2 /_{L} P = 1 \to 2 /_{L} P = {(- 1)}^{\frac{P^{2} - 1}{8}})))$
56	26 55	mpcom	$⊢ P \in (ℙ ∖ \{2\}) \to (\neg P \mod 8 \in \{1, 7\} \to (\neg 2 /_{L} P = 1 \to 2 /_{L} P = {(- 1)}^{\frac{P^{2} - 1}{8}}))$
57	56	com13	$⊢ \neg 2 /_{L} P = 1 \to (\neg P \mod 8 \in \{1, 7\} \to (P \in (ℙ ∖ \{2\}) \to 2 /_{L} P = {(- 1)}^{\frac{P^{2} - 1}{8}}))$
58	21 57	bija	$⊢ (2 /_{L} P = 1 \leftrightarrow P \mod 8 \in \{1, 7\}) \to (P \in (ℙ ∖ \{2\}) \to 2 /_{L} P = {(- 1)}^{\frac{P^{2} - 1}{8}})$
59	3 58	mpcom	$⊢ P \in (ℙ ∖ \{2\}) \to 2 /_{L} P = {(- 1)}^{\frac{P^{2} - 1}{8}}$

Metamath Proof Explorer

Theorem 2lgsoddprm

Proof