Metamath Proof Explorer

Theorem lgs0

Description: The Legendre symbol when the second argument is zero. (Contributed by Mario Carneiro, 4-Feb-2015)

Ref Expression
Assertion lgs0 
|- ( A e. ZZ -> ( A /L 0 ) = if ( ( A ^ 2 ) = 1 , 1 , 0 ) )

Proof

Step Hyp Ref Expression
1 0z 
 |-  0 e. ZZ
2 eqid 
 |-  ( n e. NN |-> if ( n e. Prime , ( if ( n = 2 , if ( 2 || A , 0 , if ( ( A mod 8 ) e. { 1 , 7 } , 1 , -u 1 ) ) , ( ( ( ( A ^ ( ( n - 1 ) / 2 ) ) + 1 ) mod n ) - 1 ) ) ^ ( n pCnt 0 ) ) , 1 ) ) = ( n e. NN |-> if ( n e. Prime , ( if ( n = 2 , if ( 2 || A , 0 , if ( ( A mod 8 ) e. { 1 , 7 } , 1 , -u 1 ) ) , ( ( ( ( A ^ ( ( n - 1 ) / 2 ) ) + 1 ) mod n ) - 1 ) ) ^ ( n pCnt 0 ) ) , 1 ) )
3 2 lgsval 
 |-  ( ( A e. ZZ /\ 0 e. ZZ ) -> ( A /L 0 ) = if ( 0 = 0 , if ( ( A ^ 2 ) = 1 , 1 , 0 ) , ( if ( ( 0 < 0 /\ A < 0 ) , -u 1 , 1 ) x. ( seq 1 ( x. , ( n e. NN |-> if ( n e. Prime , ( if ( n = 2 , if ( 2 || A , 0 , if ( ( A mod 8 ) e. { 1 , 7 } , 1 , -u 1 ) ) , ( ( ( ( A ^ ( ( n - 1 ) / 2 ) ) + 1 ) mod n ) - 1 ) ) ^ ( n pCnt 0 ) ) , 1 ) ) ) ` ( abs ` 0 ) ) ) ) )
4 1 3 mpan2 
 |-  ( A e. ZZ -> ( A /L 0 ) = if ( 0 = 0 , if ( ( A ^ 2 ) = 1 , 1 , 0 ) , ( if ( ( 0 < 0 /\ A < 0 ) , -u 1 , 1 ) x. ( seq 1 ( x. , ( n e. NN |-> if ( n e. Prime , ( if ( n = 2 , if ( 2 || A , 0 , if ( ( A mod 8 ) e. { 1 , 7 } , 1 , -u 1 ) ) , ( ( ( ( A ^ ( ( n - 1 ) / 2 ) ) + 1 ) mod n ) - 1 ) ) ^ ( n pCnt 0 ) ) , 1 ) ) ) ` ( abs ` 0 ) ) ) ) )
5 eqid 
 |-  0 = 0
6 5 iftruei 
 |-  if ( 0 = 0 , if ( ( A ^ 2 ) = 1 , 1 , 0 ) , ( if ( ( 0 < 0 /\ A < 0 ) , -u 1 , 1 ) x. ( seq 1 ( x. , ( n e. NN |-> if ( n e. Prime , ( if ( n = 2 , if ( 2 || A , 0 , if ( ( A mod 8 ) e. { 1 , 7 } , 1 , -u 1 ) ) , ( ( ( ( A ^ ( ( n - 1 ) / 2 ) ) + 1 ) mod n ) - 1 ) ) ^ ( n pCnt 0 ) ) , 1 ) ) ) ` ( abs ` 0 ) ) ) ) = if ( ( A ^ 2 ) = 1 , 1 , 0 )
7 4 6 eqtrdi 
 |-  ( A e. ZZ -> ( A /L 0 ) = if ( ( A ^ 2 ) = 1 , 1 , 0 ) )