Metamath Proof Explorer

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∈ℤ∧N∈ℤ→A/LN∈−101

Proof

Step Hyp Ref Expression
1 lgsle1 ⊢A∈ℤ∧N∈ℤ→A/LN≤1
2 lgscl ⊢A∈ℤ∧N∈ℤ→A/LN∈ℤ
3 zabsle1 ⊢A/LN∈ℤ→A/LN∈−101↔A/LN≤1
4 2 3 syl ⊢A∈ℤ∧N∈ℤ→A/LN∈−101↔A/LN≤1
5 1 4 mpbird ⊢A∈ℤ∧N∈ℤ→A/LN∈−101