# Metamath Proof Explorer

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 ${⊢}\left({P}\in \left(ℙ\setminus \left\{2\right\}\right)\wedge {Q}\in \left(ℙ\setminus \left\{2\right\}\right)\wedge {P}\ne {Q}\right)\to \left({P}{/}_{L}{Q}\right)\left({Q}{/}_{L}{P}\right)={\left(-1\right)}^{\left(\frac{{P}-1}{2}\right)\left(\frac{{Q}-1}{2}\right)}$

### Proof

Step Hyp Ref Expression
1 simp1 ${⊢}\left({P}\in \left(ℙ\setminus \left\{2\right\}\right)\wedge {Q}\in \left(ℙ\setminus \left\{2\right\}\right)\wedge {P}\ne {Q}\right)\to {P}\in \left(ℙ\setminus \left\{2\right\}\right)$
2 simp2 ${⊢}\left({P}\in \left(ℙ\setminus \left\{2\right\}\right)\wedge {Q}\in \left(ℙ\setminus \left\{2\right\}\right)\wedge {P}\ne {Q}\right)\to {Q}\in \left(ℙ\setminus \left\{2\right\}\right)$
3 simp3 ${⊢}\left({P}\in \left(ℙ\setminus \left\{2\right\}\right)\wedge {Q}\in \left(ℙ\setminus \left\{2\right\}\right)\wedge {P}\ne {Q}\right)\to {P}\ne {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 \left({x}\in \left(1\dots \frac{{P}-1}{2}\right)↔{z}\in \left(1\dots \frac{{P}-1}{2}\right)\right)$
7 eleq1w ${⊢}{y}={w}\to \left({y}\in \left(1\dots \frac{{Q}-1}{2}\right)↔{w}\in \left(1\dots \frac{{Q}-1}{2}\right)\right)$
8 6 7 bi2anan9 ${⊢}\left({x}={z}\wedge {y}={w}\right)\to \left(\left({x}\in \left(1\dots \frac{{P}-1}{2}\right)\wedge {y}\in \left(1\dots \frac{{Q}-1}{2}\right)\right)↔\left({z}\in \left(1\dots \frac{{P}-1}{2}\right)\wedge {w}\in \left(1\dots \frac{{Q}-1}{2}\right)\right)\right)$
9 oveq1 ${⊢}{y}={w}\to {y}{P}={w}{P}$
10 oveq1 ${⊢}{x}={z}\to {x}{Q}={z}{Q}$
11 9 10 breqan12rd ${⊢}\left({x}={z}\wedge {y}={w}\right)\to \left({y}{P}<{x}{Q}↔{w}{P}<{z}{Q}\right)$
12 8 11 anbi12d ${⊢}\left({x}={z}\wedge {y}={w}\right)\to \left(\left(\left({x}\in \left(1\dots \frac{{P}-1}{2}\right)\wedge {y}\in \left(1\dots \frac{{Q}-1}{2}\right)\right)\wedge {y}{P}<{x}{Q}\right)↔\left(\left({z}\in \left(1\dots \frac{{P}-1}{2}\right)\wedge {w}\in \left(1\dots \frac{{Q}-1}{2}\right)\right)\wedge {w}{P}<{z}{Q}\right)\right)$
13 12 cbvopabv ${⊢}\left\{⟨{x},{y}⟩|\left(\left({x}\in \left(1\dots \frac{{P}-1}{2}\right)\wedge {y}\in \left(1\dots \frac{{Q}-1}{2}\right)\right)\wedge {y}{P}<{x}{Q}\right)\right\}=\left\{⟨{z},{w}⟩|\left(\left({z}\in \left(1\dots \frac{{P}-1}{2}\right)\wedge {w}\in \left(1\dots \frac{{Q}-1}{2}\right)\right)\wedge {w}{P}<{z}{Q}\right)\right\}$
14 1 2 3 4 5 13 lgsquadlem3 ${⊢}\left({P}\in \left(ℙ\setminus \left\{2\right\}\right)\wedge {Q}\in \left(ℙ\setminus \left\{2\right\}\right)\wedge {P}\ne {Q}\right)\to \left({P}{/}_{L}{Q}\right)\left({Q}{/}_{L}{P}\right)={\left(-1\right)}^{\left(\frac{{P}-1}{2}\right)\left(\frac{{Q}-1}{2}\right)}$