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 ) ) ) |
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 ) ) ) |