Metamath Proof Explorer


Theorem lgscl

Description: The Legendre symbol is an integer. (Contributed by Mario Carneiro, 4-Feb-2015)

Ref Expression
Assertion lgscl
|- ( ( A e. ZZ /\ N e. ZZ ) -> ( A /L N ) e. ZZ )

Proof

Step Hyp Ref Expression
1 ssrab2
 |-  { x e. ZZ | ( abs ` x ) <_ 1 } C_ ZZ
2 eqid
 |-  { x e. ZZ | ( abs ` x ) <_ 1 } = { x e. ZZ | ( abs ` x ) <_ 1 }
3 2 lgscl2
 |-  ( ( A e. ZZ /\ N e. ZZ ) -> ( A /L N ) e. { x e. ZZ | ( abs ` x ) <_ 1 } )
4 1 3 sselid
 |-  ( ( A e. ZZ /\ N e. ZZ ) -> ( A /L N ) e. ZZ )