lgsquad

Description: The Law of Quadratic Reciprocity, see also theorem 9.8 in ApostolNT p. 185. If P and Q are distinct odd primes, then the product of the Legendre symbols ( P /L Q ) and ( Q /L P ) is the parity of ( ( P - 1 ) / 2 ) x. ( ( Q - 1 ) / 2 ) . This uses Eisenstein's proof, which also has a nice geometric interpretation - see https://en.wikipedia.org/wiki/Proofs_of_quadratic_reciprocity . This is Metamath 100 proof #7. (Contributed by Mario Carneiro, 19-Jun-2015)

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

Proof

Step	Hyp	Ref	Expression
1		simp1	$⊢ (P \in (ℙ ∖ \{2\}) \land Q \in (ℙ ∖ \{2\}) \land P \neq Q) \to P \in (ℙ ∖ \{2\})$
2		simp2	$⊢ (P \in (ℙ ∖ \{2\}) \land Q \in (ℙ ∖ \{2\}) \land P \neq Q) \to Q \in (ℙ ∖ \{2\})$
3		simp3	$⊢ (P \in (ℙ ∖ \{2\}) \land Q \in (ℙ ∖ \{2\}) \land P \neq Q) \to P \neq Q$
4		eqid	$⊢ \frac{P - 1}{2} = \frac{P - 1}{2}$
5		eqid	$⊢ \frac{Q - 1}{2} = \frac{Q - 1}{2}$
6		eleq1w	$⊢ x = z \to (x \in (1 \dots \frac{P - 1}{2}) \leftrightarrow z \in (1 \dots \frac{P - 1}{2}))$
7		eleq1w	$⊢ y = w \to (y \in (1 \dots \frac{Q - 1}{2}) \leftrightarrow w \in (1 \dots \frac{Q - 1}{2}))$
8	6 7	bi2anan9	$⊢ (x = z \land y = w) \to ((x \in (1 \dots \frac{P - 1}{2}) \land y \in (1 \dots \frac{Q - 1}{2})) \leftrightarrow (z \in (1 \dots \frac{P - 1}{2}) \land w \in (1 \dots \frac{Q - 1}{2})))$
9		oveq1	$⊢ y = w \to y P = w P$
10		oveq1	$⊢ x = z \to x Q = z Q$
11	9 10	breqan12rd	$⊢ (x = z \land y = w) \to (y P < x Q \leftrightarrow w P < z Q)$
12	8 11	anbi12d	$⊢ (x = z \land y = w) \to (((x \in (1 \dots \frac{P - 1}{2}) \land y \in (1 \dots \frac{Q - 1}{2})) \land y P < x Q) \leftrightarrow ((z \in (1 \dots \frac{P - 1}{2}) \land w \in (1 \dots \frac{Q - 1}{2})) \land w P < z Q))$
13	12	cbvopabv	$⊢ \{⟨x, y⟩ \| ((x \in (1 \dots \frac{P - 1}{2}) \land y \in (1 \dots \frac{Q - 1}{2})) \land y P < x Q)\} = \{⟨z, w⟩ \| ((z \in (1 \dots \frac{P - 1}{2}) \land w \in (1 \dots \frac{Q - 1}{2})) \land w P < z Q)\}$
14	1 2 3 4 5 13	lgsquadlem3	$⊢ (P \in (ℙ ∖ \{2\}) \land Q \in (ℙ ∖ \{2\}) \land P \neq Q) \to (P /_{L} Q) (Q /_{L} P) = {(- 1)}^{(\frac{P - 1}{2}) (\frac{Q - 1}{2})}$

Metamath Proof Explorer

Theorem lgsquad

Proof