Theorem lgscl

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

	Ref	Expression
Assertion	lgscl	$$⊢\left(A\in \mathbb{Z}\wedge N\in \mathbb{Z}\right)\to A{/}_{L}N\in \mathbb{Z}$$

Proof

Step	Hyp	Ref	Expression
1		ssrab2	$$⊢\left\{x\in \mathbb{Z}|\left|x\right|\le 1\right\}\subseteq \mathbb{Z}$$
2		eqid	$$⊢\left\{x\in \mathbb{Z}|\left|x\right|\le 1\right\}=\left\{x\in \mathbb{Z}|\left|x\right|\le 1\right\}$$
3	2	lgscl2	$$⊢\left(A\in \mathbb{Z}\wedge N\in \mathbb{Z}\right)\to A{/}_{L}N\in \left\{x\in \mathbb{Z}|\left|x\right|\le 1\right\}$$
4	1 3	sselid	$$⊢\left(A\in \mathbb{Z}\wedge N\in \mathbb{Z}\right)\to A{/}_{L}N\in \mathbb{Z}$$