Theorem lgscl1

Description: The value of the Legendre symbol is either -1 or 0 or 1. (Contributed by AV, 13-Jul-2021)

	Ref	Expression
Assertion	lgscl1	|- ( ( A e. ZZ /\ N e. ZZ ) -> ( A /L N ) e. { -u 1 , 0 , 1 } )

Proof

Step	Hyp	Ref	Expression
1		lgsle1	|- ( ( A e. ZZ /\ N e. ZZ ) -> ( abs ` ( A /L N ) ) <_ 1 )
2		lgscl	|- ( ( A e. ZZ /\ N e. ZZ ) -> ( A /L N ) e. ZZ )
3		zabsle1	|- ( ( A /L N ) e. ZZ -> ( ( A /L N ) e. { -u 1 , 0 , 1 } <-> ( abs ` ( A /L N ) ) <_ 1 ) )
4	2 3	syl	|- ( ( A e. ZZ /\ N e. ZZ ) -> ( ( A /L N ) e. { -u 1 , 0 , 1 } <-> ( abs ` ( A /L N ) ) <_ 1 ) )
5	1 4	mpbird	|- ( ( A e. ZZ /\ N e. ZZ ) -> ( A /L N ) e. { -u 1 , 0 , 1 } )