Metamath Proof Explorer

Definition df-lgs

Description: Define the Legendre symbol (actually the Kronecker symbol, which extends the Legendre symbol to all integers, and also the Jacobi symbol, which restricts the Kronecker symbol to positive odd integers). See definition in ApostolNT p. 179 resp. definition in ApostolNT p. 188. (Contributed by Mario Carneiro, 4-Feb-2015)

Ref Expression
Assertion df-lgs 
|- /L = ( a e. ZZ , n e. ZZ |-> if ( n = 0 , if ( ( a ^ 2 ) = 1 , 1 , 0 ) , ( if ( ( n < 0 /\ a < 0 ) , -u 1 , 1 ) x. ( seq 1 ( x. , ( m e. NN |-> if ( m e. Prime , ( if ( m = 2 , if ( 2 || a , 0 , if ( ( a mod 8 ) e. { 1 , 7 } , 1 , -u 1 ) ) , ( ( ( ( a ^ ( ( m - 1 ) / 2 ) ) + 1 ) mod m ) - 1 ) ) ^ ( m pCnt n ) ) , 1 ) ) ) ` ( abs ` n ) ) ) ) )

Detailed syntax breakdown

Step Hyp Ref Expression
0 clgs 
 |-  /L
1 va 
 |-  a
2 cz 
 |-  ZZ
3 vn 
 |-  n
4 3 cv 
 |-  n
5 cc0 
 |-  0
6 4 5 wceq 
 |-  n = 0
7 1 cv 
 |-  a
8 cexp 
 |-  ^
9 c2 
 |-  2
10 7 9 8 co 
 |-  ( a ^ 2 )
11 c1 
 |-  1
12 10 11 wceq 
 |-  ( a ^ 2 ) = 1
13 12 11 5 cif 
 |-  if ( ( a ^ 2 ) = 1 , 1 , 0 )
14 clt 
 |-  <
15 4 5 14 wbr 
 |-  n < 0
16 7 5 14 wbr 
 |-  a < 0
17 15 16 wa 
 |-  ( n < 0 /\ a < 0 )
18 11 cneg 
 |-  -u 1
19 17 18 11 cif 
 |-  if ( ( n < 0 /\ a < 0 ) , -u 1 , 1 )
20 cmul 
 |-  x.
21 vm 
 |-  m
22 cn 
 |-  NN
23 21 cv 
 |-  m
24 cprime 
 |-  Prime
25 23 24 wcel 
 |-  m e. Prime
26 23 9 wceq 
 |-  m = 2
27 cdvds 
 |-  ||
28 9 7 27 wbr 
 |-  2 || a
29 cmo 
 |-  mod
30 c8 
 |-  8
31 7 30 29 co 
 |-  ( a mod 8 )
32 c7 
 |-  7
33 11 32 cpr 
 |-  { 1 , 7 }
34 31 33 wcel 
 |-  ( a mod 8 ) e. { 1 , 7 }
35 34 11 18 cif 
 |-  if ( ( a mod 8 ) e. { 1 , 7 } , 1 , -u 1 )
36 28 5 35 cif 
 |-  if ( 2 || a , 0 , if ( ( a mod 8 ) e. { 1 , 7 } , 1 , -u 1 ) )
37 cmin 
 |-  -
38 23 11 37 co 
 |-  ( m - 1 )
39 cdiv 
 |-  /
40 38 9 39 co 
 |-  ( ( m - 1 ) / 2 )
41 7 40 8 co 
 |-  ( a ^ ( ( m - 1 ) / 2 ) )
42 caddc 
 |-  +
43 41 11 42 co 
 |-  ( ( a ^ ( ( m - 1 ) / 2 ) ) + 1 )
44 43 23 29 co 
 |-  ( ( ( a ^ ( ( m - 1 ) / 2 ) ) + 1 ) mod m )
45 44 11 37 co 
 |-  ( ( ( ( a ^ ( ( m - 1 ) / 2 ) ) + 1 ) mod m ) - 1 )
46 26 36 45 cif 
 |-  if ( m = 2 , if ( 2 || a , 0 , if ( ( a mod 8 ) e. { 1 , 7 } , 1 , -u 1 ) ) , ( ( ( ( a ^ ( ( m - 1 ) / 2 ) ) + 1 ) mod m ) - 1 ) )
47 cpc 
 |-  pCnt
48 23 4 47 co 
 |-  ( m pCnt n )
49 46 48 8 co 
 |-  ( if ( m = 2 , if ( 2 || a , 0 , if ( ( a mod 8 ) e. { 1 , 7 } , 1 , -u 1 ) ) , ( ( ( ( a ^ ( ( m - 1 ) / 2 ) ) + 1 ) mod m ) - 1 ) ) ^ ( m pCnt n ) )
50 25 49 11 cif 
 |-  if ( m e. Prime , ( if ( m = 2 , if ( 2 || a , 0 , if ( ( a mod 8 ) e. { 1 , 7 } , 1 , -u 1 ) ) , ( ( ( ( a ^ ( ( m - 1 ) / 2 ) ) + 1 ) mod m ) - 1 ) ) ^ ( m pCnt n ) ) , 1 )
51 21 22 50 cmpt 
 |-  ( m e. NN |-> if ( m e. Prime , ( if ( m = 2 , if ( 2 || a , 0 , if ( ( a mod 8 ) e. { 1 , 7 } , 1 , -u 1 ) ) , ( ( ( ( a ^ ( ( m - 1 ) / 2 ) ) + 1 ) mod m ) - 1 ) ) ^ ( m pCnt n ) ) , 1 ) )
52 20 51 11 cseq 
 |-  seq 1 ( x. , ( m e. NN |-> if ( m e. Prime , ( if ( m = 2 , if ( 2 || a , 0 , if ( ( a mod 8 ) e. { 1 , 7 } , 1 , -u 1 ) ) , ( ( ( ( a ^ ( ( m - 1 ) / 2 ) ) + 1 ) mod m ) - 1 ) ) ^ ( m pCnt n ) ) , 1 ) ) )
53 cabs 
 |-  abs
54 4 53 cfv 
 |-  ( abs ` n )
55 54 52 cfv 
 |-  ( seq 1 ( x. , ( m e. NN |-> if ( m e. Prime , ( if ( m = 2 , if ( 2 || a , 0 , if ( ( a mod 8 ) e. { 1 , 7 } , 1 , -u 1 ) ) , ( ( ( ( a ^ ( ( m - 1 ) / 2 ) ) + 1 ) mod m ) - 1 ) ) ^ ( m pCnt n ) ) , 1 ) ) ) ` ( abs ` n ) )
56 19 55 20 co 
 |-  ( if ( ( n < 0 /\ a < 0 ) , -u 1 , 1 ) x. ( seq 1 ( x. , ( m e. NN |-> if ( m e. Prime , ( if ( m = 2 , if ( 2 || a , 0 , if ( ( a mod 8 ) e. { 1 , 7 } , 1 , -u 1 ) ) , ( ( ( ( a ^ ( ( m - 1 ) / 2 ) ) + 1 ) mod m ) - 1 ) ) ^ ( m pCnt n ) ) , 1 ) ) ) ` ( abs ` n ) ) )
57 6 13 56 cif 
 |-  if ( n = 0 , if ( ( a ^ 2 ) = 1 , 1 , 0 ) , ( if ( ( n < 0 /\ a < 0 ) , -u 1 , 1 ) x. ( seq 1 ( x. , ( m e. NN |-> if ( m e. Prime , ( if ( m = 2 , if ( 2 || a , 0 , if ( ( a mod 8 ) e. { 1 , 7 } , 1 , -u 1 ) ) , ( ( ( ( a ^ ( ( m - 1 ) / 2 ) ) + 1 ) mod m ) - 1 ) ) ^ ( m pCnt n ) ) , 1 ) ) ) ` ( abs ` n ) ) ) )
58 1 3 2 2 57 cmpo 
 |-  ( a e. ZZ , n e. ZZ |-> if ( n = 0 , if ( ( a ^ 2 ) = 1 , 1 , 0 ) , ( if ( ( n < 0 /\ a < 0 ) , -u 1 , 1 ) x. ( seq 1 ( x. , ( m e. NN |-> if ( m e. Prime , ( if ( m = 2 , if ( 2 || a , 0 , if ( ( a mod 8 ) e. { 1 , 7 } , 1 , -u 1 ) ) , ( ( ( ( a ^ ( ( m - 1 ) / 2 ) ) + 1 ) mod m ) - 1 ) ) ^ ( m pCnt n ) ) , 1 ) ) ) ` ( abs ` n ) ) ) ) )
59 0 58 wceq 
 |-  /L = ( a e. ZZ , n e. ZZ |-> if ( n = 0 , if ( ( a ^ 2 ) = 1 , 1 , 0 ) , ( if ( ( n < 0 /\ a < 0 ) , -u 1 , 1 ) x. ( seq 1 ( x. , ( m e. NN |-> if ( m e. Prime , ( if ( m = 2 , if ( 2 || a , 0 , if ( ( a mod 8 ) e. { 1 , 7 } , 1 , -u 1 ) ) , ( ( ( ( a ^ ( ( m - 1 ) / 2 ) ) + 1 ) mod m ) - 1 ) ) ^ ( m pCnt n ) ) , 1 ) ) ) ` ( abs ` n ) ) ) ) )