Description: The Legendre symbol is an integer with absolute value less than or equal to 1. (Contributed by Mario Carneiro, 4-Feb-2015)
| Ref | Expression | ||
|---|---|---|---|
| Hypothesis | lgscl2.z | |- Z = { x e. ZZ | ( abs ` x ) <_ 1 } |
|
| Assertion | lgscl2 | |- ( ( A e. ZZ /\ N e. ZZ ) -> ( A /L N ) e. Z ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | lgscl2.z | |- Z = { x e. ZZ | ( abs ` x ) <_ 1 } |
|
| 2 | 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 N ) ) , 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 N ) ) , 1 ) ) |
|
| 3 | 2 1 | lgscllem | |- ( ( A e. ZZ /\ N e. ZZ ) -> ( A /L N ) e. Z ) |