Theorem lgscl2

Description: The Legendre symbol is an integer with absolute value less than or equal to 1. (Contributed by Mario Carneiro, 4-Feb-2015)

	Ref	Expression
Hypothesis	lgscl2.z	$$⊢Z=\left\{x\in \mathbb{Z}|\left|x\right|\le 1\right\}$$
Assertion	lgscl2	$$⊢\left(A\in \mathbb{Z}\wedge N\in \mathbb{Z}\right)\to A{/}_{L}N\in Z$$

Proof

Step	Hyp	Ref	Expression
1		lgscl2.z	$$⊢Z=\left\{x\in \mathbb{Z}|\left|x\right|\le 1\right\}$$
2		eqid	$$⊢\left(n\in \mathbb{N}⟼if\left(n\in \mathbb{P},{if\left(n=2,if\left(2\parallel A,0,if\left(A\mathrm{mod}8\in \left\{1,7\right\},1,-1\right)\right),\left(\left(A^{\frac{n-1}{2}}+1\right)\mathrm{mod}n\right)-1\right)}^{n\mathrm{pCnt}N},1\right)\right)=\left(n\in \mathbb{N}⟼if\left(n\in \mathbb{P},{if\left(n=2,if\left(2\parallel A,0,if\left(A\mathrm{mod}8\in \left\{1,7\right\},1,-1\right)\right),\left(\left(A^{\frac{n-1}{2}}+1\right)\mathrm{mod}n\right)-1\right)}^{n\mathrm{pCnt}N},1\right)\right)$$
3	2 1	lgscllem	$$⊢\left(A\in \mathbb{Z}\wedge N\in \mathbb{Z}\right)\to A{/}_{L}N\in Z$$