Metamath Proof Explorer


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
2 lgs2 2 2 / L 2 = if 2 2 0 if 2 mod 8 1 7 1 1
3 1 2 ax-mp 2 / L 2 = if 2 2 0 if 2 mod 8 1 7 1 1
4 z2even 2 2
5 4 iftruei if 2 2 0 if 2 mod 8 1 7 1 1 = 0
6 3 5 eqtri 2 / L 2 = 0