Theorem lgsval2

Description: The Legendre symbol at a prime (this is the traditional domain of the Legendre symbol, except for the addition of prime 2 ). (Contributed by Mario Carneiro, 4-Feb-2015)

	Ref	Expression
Assertion	lgsval2	$$⊢\left(A\in \mathbb{Z}\wedge P\in \mathbb{P}\right)\to A{/}_{L}P=if\left(P=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{P-1}{2}}+1\right)\mathrm{mod}P\right)-1\right)$$

Proof

Step	Hyp	Ref	Expression
1		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}P},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}P},1\right)\right)$$
2	1	lgsval2lem	$$⊢\left(A\in \mathbb{Z}\wedge P\in \mathbb{P}\right)\to A{/}_{L}P=if\left(P=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{P-1}{2}}+1\right)\mathrm{mod}P\right)-1\right)$$