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 ) ) ) )