Theorem lgsfcl

Description: Closure of the function F which defines the Legendre symbol at the primes. (Contributed by Mario Carneiro, 4-Feb-2015)

	Ref	Expression
Hypothesis	lgsval.1	$$⊢F=\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)$$
Assertion	lgsfcl	$$⊢\left(A\in \mathbb{Z}\wedge N\in \mathbb{Z}\wedge N\ne 0\right)\to F:\mathbb{N}⟶\mathbb{Z}$$

Proof

Step	Hyp	Ref	Expression
1		lgsval.1	$$⊢F=\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)$$
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	1 2	lgsfcl2	$$⊢\left(A\in \mathbb{Z}\wedge N\in \mathbb{Z}\wedge N\ne 0\right)\to F:\mathbb{N}⟶\left\{x\in \mathbb{Z}|\left|x\right|\le 1\right\}$$
4		ssrab2	$$⊢\left\{x\in \mathbb{Z}|\left|x\right|\le 1\right\}\subseteq \mathbb{Z}$$
5		fss	$$⊢\left(F:\mathbb{N}⟶\left\{x\in \mathbb{Z}|\left|x\right|\le 1\right\}\wedge \left\{x\in \mathbb{Z}|\left|x\right|\le 1\right\}\subseteq \mathbb{Z}\right)\to F:\mathbb{N}⟶\mathbb{Z}$$
6	3 4 5	sylancl	$$⊢\left(A\in \mathbb{Z}\wedge N\in \mathbb{Z}\wedge N\ne 0\right)\to F:\mathbb{N}⟶\mathbb{Z}$$