Metamath Proof Explorer

Theorem lgsval2

Description: The Legendre symbol at a prime (this is the traditional domain of the Legendre symbol, except for the addition of prime 2 ). (Contributed by Mario Carneiro, 4-Feb-2015)

Ref Expression
Assertion lgsval2 
|- ( ( A e. ZZ /\ P e. Prime ) -> ( A /L P ) = if ( P = 2 , if ( 2 || A , 0 , if ( ( A mod 8 ) e. { 1 , 7 } , 1 , -u 1 ) ) , ( ( ( ( A ^ ( ( P - 1 ) / 2 ) ) + 1 ) mod P ) - 1 ) ) )

Proof

Step Hyp Ref Expression
1 eqid 
 |-  ( n e. NN |-> if ( n e. Prime , ( if ( n = 2 , if ( 2 || A , 0 , if ( ( A mod 8 ) e. { 1 , 7 } , 1 , -u 1 ) ) , ( ( ( ( A ^ ( ( n - 1 ) / 2 ) ) + 1 ) mod n ) - 1 ) ) ^ ( n pCnt P ) ) , 1 ) ) = ( n e. NN |-> if ( n e. Prime , ( if ( n = 2 , if ( 2 || A , 0 , if ( ( A mod 8 ) e. { 1 , 7 } , 1 , -u 1 ) ) , ( ( ( ( A ^ ( ( n - 1 ) / 2 ) ) + 1 ) mod n ) - 1 ) ) ^ ( n pCnt P ) ) , 1 ) )
2 1 lgsval2lem 
 |-  ( ( A e. ZZ /\ P e. Prime ) -> ( A /L P ) = if ( P = 2 , if ( 2 || A , 0 , if ( ( A mod 8 ) e. { 1 , 7 } , 1 , -u 1 ) ) , ( ( ( ( A ^ ( ( P - 1 ) / 2 ) ) + 1 ) mod P ) - 1 ) ) )