Metamath Proof Explorer


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 ANA/LN1

Proof

Step Hyp Ref Expression
1 eqid x|x1=x|x1
2 1 lgscl2 ANA/LNx|x1
3 fveq2 x=A/LNx=A/LN
4 3 breq1d x=A/LNx1A/LN1
5 4 elrab A/LNx|x1A/LNA/LN1
6 5 simprbi A/LNx|x1A/LN1
7 2 6 syl ANA/LN1