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	⊢ ( ( 𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ) → ( 𝐴 /L 𝑁 ) ∈ { - 1 , 0 , 1 } )

Proof

Step	Hyp	Ref	Expression
1		lgsle1	⊢ ( ( 𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ) → ( abs ‘ ( 𝐴 /L 𝑁 ) ) ≤ 1 )
2		lgscl	⊢ ( ( 𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ) → ( 𝐴 /L 𝑁 ) ∈ ℤ )
3		zabsle1	⊢ ( ( 𝐴 /L 𝑁 ) ∈ ℤ → ( ( 𝐴 /L 𝑁 ) ∈ { - 1 , 0 , 1 } ↔ ( abs ‘ ( 𝐴 /L 𝑁 ) ) ≤ 1 ) )
4	2 3	syl	⊢ ( ( 𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ) → ( ( 𝐴 /L 𝑁 ) ∈ { - 1 , 0 , 1 } ↔ ( abs ‘ ( 𝐴 /L 𝑁 ) ) ≤ 1 ) )
5	1 4	mpbird	⊢ ( ( 𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ) → ( 𝐴 /L 𝑁 ) ∈ { - 1 , 0 , 1 } )