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 e. ZZ
2 lgs2 
 |-  ( 2 e. ZZ -> ( 2 /L 2 ) = if ( 2 || 2 , 0 , if ( ( 2 mod 8 ) e. { 1 , 7 } , 1 , -u 1 ) ) )
3 1 2 ax-mp 
 |-  ( 2 /L 2 ) = if ( 2 || 2 , 0 , if ( ( 2 mod 8 ) e. { 1 , 7 } , 1 , -u 1 ) )
4 z2even 
 |-  2 || 2
5 4 iftruei 
 |-  if ( 2 || 2 , 0 , if ( ( 2 mod 8 ) e. { 1 , 7 } , 1 , -u 1 ) ) = 0
6 3 5 eqtri 
 |-  ( 2 /L 2 ) = 0