Metamath Proof Explorer

Theorem 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 ∈ ℙ ∖ 2 ∧ Q ∈ ℙ ∖ 2 ∧ P ≠ Q → P / L Q ⁢ Q / L P = − 1 P − 1 2 ⁢ Q − 1 2

Proof

Step Hyp Ref Expression
1 simp1 ⊢ P ∈ ℙ ∖ 2 ∧ Q ∈ ℙ ∖ 2 ∧ P ≠ Q → P ∈ ℙ ∖ 2
2 simp2 ⊢ P ∈ ℙ ∖ 2 ∧ Q ∈ ℙ ∖ 2 ∧ P ≠ Q → Q ∈ ℙ ∖ 2
3 simp3 ⊢ P ∈ ℙ ∖ 2 ∧ Q ∈ ℙ ∖ 2 ∧ P ≠ Q → P ≠ Q
4 eqid ⊢ P − 1 2 = P − 1 2
5 eqid ⊢ Q − 1 2 = Q − 1 2
6 eleq1w ⊢ x = z → x ∈ 1 … P − 1 2 ↔ z ∈ 1 … P − 1 2
7 eleq1w ⊢ y = w → y ∈ 1 … Q − 1 2 ↔ w ∈ 1 … Q − 1 2
8 6 7 bi2anan9 ⊢ x = z ∧ y = w → x ∈ 1 … P − 1 2 ∧ y ∈ 1 … Q − 1 2 ↔ z ∈ 1 … P − 1 2 ∧ w ∈ 1 … Q − 1 2
9 oveq1 ⊢ y = w → y ⁢ P = w ⁢ P
10 oveq1 ⊢ x = z → x ⁢ Q = z ⁢ Q
11 9 10 breqan12rd ⊢ x = z ∧ y = w → y ⁢ P < x ⁢ Q ↔ w ⁢ P < z ⁢ Q
12 8 11 anbi12d ⊢ x = z ∧ y = w → x ∈ 1 … P − 1 2 ∧ y ∈ 1 … Q − 1 2 ∧ y ⁢ P < x ⁢ Q ↔ z ∈ 1 … P − 1 2 ∧ w ∈ 1 … Q − 1 2 ∧ w ⁢ P < z ⁢ Q
13 12 cbvopabv ⊢ x y | x ∈ 1 … P − 1 2 ∧ y ∈ 1 … Q − 1 2 ∧ y ⁢ P < x ⁢ Q = z w | z ∈ 1 … P − 1 2 ∧ w ∈ 1 … Q − 1 2 ∧ w ⁢ P < z ⁢ Q
14 1 2 3 4 5 13 lgsquadlem3 ⊢ P ∈ ℙ ∖ 2 ∧ Q ∈ ℙ ∖ 2 ∧ P ≠ Q → P / L Q ⁢ Q / L P = − 1 P − 1 2 ⁢ Q − 1 2