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 e. ( Prime \ { 2 } ) /\ Q e. ( Prime \ { 2 } ) /\ P =/= Q ) -> ( ( P /L Q ) x. ( Q /L P ) ) = ( -u 1 ^ ( ( ( P - 1 ) / 2 ) x. ( ( Q - 1 ) / 2 ) ) ) )

Proof

Step Hyp Ref Expression
1 simp1 
 |-  ( ( P e. ( Prime \ { 2 } ) /\ Q e. ( Prime \ { 2 } ) /\ P =/= Q ) -> P e. ( Prime \ { 2 } ) )
2 simp2 
 |-  ( ( P e. ( Prime \ { 2 } ) /\ Q e. ( Prime \ { 2 } ) /\ P =/= Q ) -> Q e. ( Prime \ { 2 } ) )
3 simp3 
 |-  ( ( P e. ( Prime \ { 2 } ) /\ Q e. ( Prime \ { 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 e. ( 1 ... ( ( P - 1 ) / 2 ) ) <-> z e. ( 1 ... ( ( P - 1 ) / 2 ) ) ) )
7 eleq1w 
 |-  ( y = w -> ( y e. ( 1 ... ( ( Q - 1 ) / 2 ) ) <-> w e. ( 1 ... ( ( Q - 1 ) / 2 ) ) ) )
8 6 7 bi2anan9 
 |-  ( ( x = z /\ y = w ) -> ( ( x e. ( 1 ... ( ( P - 1 ) / 2 ) ) /\ y e. ( 1 ... ( ( Q - 1 ) / 2 ) ) ) <-> ( z e. ( 1 ... ( ( P - 1 ) / 2 ) ) /\ w e. ( 1 ... ( ( Q - 1 ) / 2 ) ) ) ) )
9 oveq1 
 |-  ( y = w -> ( y x. P ) = ( w x. P ) )
10 oveq1 
 |-  ( x = z -> ( x x. Q ) = ( z x. Q ) )
11 9 10 breqan12rd 
 |-  ( ( x = z /\ y = w ) -> ( ( y x. P ) < ( x x. Q ) <-> ( w x. P ) < ( z x. Q ) ) )
12 8 11 anbi12d 
 |-  ( ( x = z /\ y = w ) -> ( ( ( x e. ( 1 ... ( ( P - 1 ) / 2 ) ) /\ y e. ( 1 ... ( ( Q - 1 ) / 2 ) ) ) /\ ( y x. P ) < ( x x. Q ) ) <-> ( ( z e. ( 1 ... ( ( P - 1 ) / 2 ) ) /\ w e. ( 1 ... ( ( Q - 1 ) / 2 ) ) ) /\ ( w x. P ) < ( z x. Q ) ) ) )
13 12 cbvopabv 
 |-  { <. x , y >. | ( ( x e. ( 1 ... ( ( P - 1 ) / 2 ) ) /\ y e. ( 1 ... ( ( Q - 1 ) / 2 ) ) ) /\ ( y x. P ) < ( x x. Q ) ) } = { <. z , w >. | ( ( z e. ( 1 ... ( ( P - 1 ) / 2 ) ) /\ w e. ( 1 ... ( ( Q - 1 ) / 2 ) ) ) /\ ( w x. P ) < ( z x. Q ) ) }
14 1 2 3 4 5 13 lgsquadlem3 
 |-  ( ( P e. ( Prime \ { 2 } ) /\ Q e. ( Prime \ { 2 } ) /\ P =/= Q ) -> ( ( P /L Q ) x. ( Q /L P ) ) = ( -u 1 ^ ( ( ( P - 1 ) / 2 ) x. ( ( Q - 1 ) / 2 ) ) ) )