Theorem 2lgs2

Description: The Legendre symbol for 2 at 2 is 0 . (Contributed by AV, 20-Jun-2021)

	Ref	Expression
Assertion	2lgs2	$$⊢2{/}_{L}2=0$$

Proof

Step	Hyp	Ref	Expression
1		2z	$$⊢2\in \mathbb{Z}$$
2		lgs2	$$⊢2\in \mathbb{Z}\to 2{/}_{L}2=if\left(2\parallel 2,0,if\left(2\mathrm{mod}8\in \left\{1,7\right\},1,-1\right)\right)$$
3	1 2	ax-mp	$$⊢2{/}_{L}2=if\left(2\parallel 2,0,if\left(2\mathrm{mod}8\in \left\{1,7\right\},1,-1\right)\right)$$
4		z2even	$$⊢2\parallel 2$$
5	4	iftruei	$$⊢if\left(2\parallel 2,0,if\left(2\mathrm{mod}8\in \left\{1,7\right\},1,-1\right)\right)=0$$
6	3 5	eqtri	$$⊢2{/}_{L}2=0$$