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 ( ( 𝑃 ∈ ( ℙ ∖ { 2 } ) ∧ 𝑄 ∈ ( ℙ ∖ { 2 } ) ∧ 𝑃 ≠ 𝑄 ) → ( ( 𝑃 /L 𝑄 ) · ( 𝑄 /L 𝑃 ) ) = ( - 1 ↑ ( ( ( 𝑃 − 1 ) / 2 ) · ( ( 𝑄 − 1 ) / 2 ) ) ) )

Proof

Step Hyp Ref Expression
1 simp1 ⊢ ( ( 𝑃 ∈ ( ℙ ∖ { 2 } ) ∧ 𝑄 ∈ ( ℙ ∖ { 2 } ) ∧ 𝑃 ≠ 𝑄 ) → 𝑃 ∈ ( ℙ ∖ { 2 } ) )
2 simp2 ⊢ ( ( 𝑃 ∈ ( ℙ ∖ { 2 } ) ∧ 𝑄 ∈ ( ℙ ∖ { 2 } ) ∧ 𝑃 ≠ 𝑄 ) → 𝑄 ∈ ( ℙ ∖ { 2 } ) )
3 simp3 ⊢ ( ( 𝑃 ∈ ( ℙ ∖ { 2 } ) ∧ 𝑄 ∈ ( ℙ ∖ { 2 } ) ∧ 𝑃 ≠ 𝑄 ) → 𝑃 ≠ 𝑄 )
4 eqid ⊢ ( ( 𝑃 − 1 ) / 2 ) = ( ( 𝑃 − 1 ) / 2 )
5 eqid ⊢ ( ( 𝑄 − 1 ) / 2 ) = ( ( 𝑄 − 1 ) / 2 )
6 eleq1w ⊢ ( 𝑥 = 𝑧 → ( 𝑥 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ↔ 𝑧 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ) )
7 eleq1w ⊢ ( 𝑦 = 𝑤 → ( 𝑦 ∈ ( 1 ... ( ( 𝑄 − 1 ) / 2 ) ) ↔ 𝑤 ∈ ( 1 ... ( ( 𝑄 − 1 ) / 2 ) ) ) )
8 6 7 bi2anan9 ⊢ ( ( 𝑥 = 𝑧 ∧ 𝑦 = 𝑤 ) → ( ( 𝑥 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ∧ 𝑦 ∈ ( 1 ... ( ( 𝑄 − 1 ) / 2 ) ) ) ↔ ( 𝑧 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ∧ 𝑤 ∈ ( 1 ... ( ( 𝑄 − 1 ) / 2 ) ) ) ) )
9 oveq1 ⊢ ( 𝑦 = 𝑤 → ( 𝑦 · 𝑃 ) = ( 𝑤 · 𝑃 ) )
10 oveq1 ⊢ ( 𝑥 = 𝑧 → ( 𝑥 · 𝑄 ) = ( 𝑧 · 𝑄 ) )
11 9 10 breqan12rd ⊢ ( ( 𝑥 = 𝑧 ∧ 𝑦 = 𝑤 ) → ( ( 𝑦 · 𝑃 ) < ( 𝑥 · 𝑄 ) ↔ ( 𝑤 · 𝑃 ) < ( 𝑧 · 𝑄 ) ) )
12 8 11 anbi12d ⊢ ( ( 𝑥 = 𝑧 ∧ 𝑦 = 𝑤 ) → ( ( ( 𝑥 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ∧ 𝑦 ∈ ( 1 ... ( ( 𝑄 − 1 ) / 2 ) ) ) ∧ ( 𝑦 · 𝑃 ) < ( 𝑥 · 𝑄 ) ) ↔ ( ( 𝑧 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ∧ 𝑤 ∈ ( 1 ... ( ( 𝑄 − 1 ) / 2 ) ) ) ∧ ( 𝑤 · 𝑃 ) < ( 𝑧 · 𝑄 ) ) ) )
13 12 cbvopabv ⊢ { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( ( 𝑥 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ∧ 𝑦 ∈ ( 1 ... ( ( 𝑄 − 1 ) / 2 ) ) ) ∧ ( 𝑦 · 𝑃 ) < ( 𝑥 · 𝑄 ) ) } = { ⟨ 𝑧 , 𝑤 ⟩ ∣ ( ( 𝑧 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ∧ 𝑤 ∈ ( 1 ... ( ( 𝑄 − 1 ) / 2 ) ) ) ∧ ( 𝑤 · 𝑃 ) < ( 𝑧 · 𝑄 ) ) }
14 1 2 3 4 5 13 lgsquadlem3 ⊢ ( ( 𝑃 ∈ ( ℙ ∖ { 2 } ) ∧ 𝑄 ∈ ( ℙ ∖ { 2 } ) ∧ 𝑃 ≠ 𝑄 ) → ( ( 𝑃 /L 𝑄 ) · ( 𝑄 /L 𝑃 ) ) = ( - 1 ↑ ( ( ( 𝑃 − 1 ) / 2 ) · ( ( 𝑄 − 1 ) / 2 ) ) ) )