Metamath Proof Explorer

Theorem lgs2

Description: The Legendre symbol at 2 . (Contributed by Mario Carneiro, 4-Feb-2015)

Ref Expression
Assertion lgs2 
|- ( A e. ZZ -> ( A /L 2 ) = if ( 2 || A , 0 , if ( ( A mod 8 ) e. { 1 , 7 } , 1 , -u 1 ) ) )

Proof

Step Hyp Ref Expression
1 2prm 
 |-  2 e. Prime
2 lgsval2 
 |-  ( ( A e. ZZ /\ 2 e. Prime ) -> ( A /L 2 ) = if ( 2 = 2 , if ( 2 || A , 0 , if ( ( A mod 8 ) e. { 1 , 7 } , 1 , -u 1 ) ) , ( ( ( ( A ^ ( ( 2 - 1 ) / 2 ) ) + 1 ) mod 2 ) - 1 ) ) )
3 1 2 mpan2 
 |-  ( A e. ZZ -> ( A /L 2 ) = if ( 2 = 2 , if ( 2 || A , 0 , if ( ( A mod 8 ) e. { 1 , 7 } , 1 , -u 1 ) ) , ( ( ( ( A ^ ( ( 2 - 1 ) / 2 ) ) + 1 ) mod 2 ) - 1 ) ) )
4 eqid 
 |-  2 = 2
5 4 iftruei 
 |-  if ( 2 = 2 , if ( 2 || A , 0 , if ( ( A mod 8 ) e. { 1 , 7 } , 1 , -u 1 ) ) , ( ( ( ( A ^ ( ( 2 - 1 ) / 2 ) ) + 1 ) mod 2 ) - 1 ) ) = if ( 2 || A , 0 , if ( ( A mod 8 ) e. { 1 , 7 } , 1 , -u 1 ) )
6 3 5 eqtrdi 
 |-  ( A e. ZZ -> ( A /L 2 ) = if ( 2 || A , 0 , if ( ( A mod 8 ) e. { 1 , 7 } , 1 , -u 1 ) ) )