Theorem lgsle1

Description: The Legendre symbol has absolute value less than or equal to 1. Together with lgscl this implies that it takes values in { -u 1 , 0 , 1 } . (Contributed by Mario Carneiro, 4-Feb-2015)

	Ref	Expression
Assertion	lgsle1	|- ( ( A e. ZZ /\ N e. ZZ ) -> ( abs ` ( A /L N ) ) <_ 1 )

Proof

Step	Hyp	Ref	Expression
1		eqid	|- { x e. ZZ | ( abs ` x ) <_ 1 } = { x e. ZZ | ( abs ` x ) <_ 1 }
2	1	lgscl2	|- ( ( A e. ZZ /\ N e. ZZ ) -> ( A /L N ) e. { x e. ZZ | ( abs ` x ) <_ 1 } )
3		fveq2	|- ( x = ( A /L N ) -> ( abs ` x ) = ( abs ` ( A /L N ) ) )
4	3	breq1d	|- ( x = ( A /L N ) -> ( ( abs ` x ) <_ 1 <-> ( abs ` ( A /L N ) ) <_ 1 ) )
5	4	elrab	|- ( ( A /L N ) e. { x e. ZZ | ( abs ` x ) <_ 1 } <-> ( ( A /L N ) e. ZZ /\ ( abs ` ( A /L N ) ) <_ 1 ) )
6	5	simprbi	|- ( ( A /L N ) e. { x e. ZZ | ( abs ` x ) <_ 1 } -> ( abs ` ( A /L N ) ) <_ 1 )
7	2 6	syl	|- ( ( A e. ZZ /\ N e. ZZ ) -> ( abs ` ( A /L N ) ) <_ 1 )