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 / L N ∈ − 1 0 1

Proof

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