Metamath Proof Explorer

Theorem lgscl

Description: The Legendre symbol is an integer. (Contributed by Mario Carneiro, 4-Feb-2015)

Ref Expression
Assertion lgscl ⊢ A ∈ ℤ ∧ N ∈ ℤ → A / L N ∈ ℤ

Proof

Step Hyp Ref Expression
1 ssrab2 ⊢ x ∈ ℤ | x ≤ 1 ⊆ ℤ
2 eqid ⊢ x ∈ ℤ | x ≤ 1 = x ∈ ℤ | x ≤ 1
3 2 lgscl2 ⊢ A ∈ ℤ ∧ N ∈ ℤ → A / L N ∈ x ∈ ℤ | x ≤ 1
4 1 3 sseldi ⊢ A ∈ ℤ ∧ N ∈ ℤ → A / L N ∈ ℤ