MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  df-lgs Structured version   Unicode version

Definition df-lgs 22646
Description: Define the Legendre symbol (actually the Kronecker symbol, which extends the Legendre symbol to all integers). (Contributed by Mario Carneiro, 4-Feb-2015.)
Assertion
Ref Expression
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 ) ) ) ) )
Distinct variable group:    m, a, n

Detailed syntax breakdown of Definition df-lgs
StepHypRef Expression
1 clgs 22645 . 2  class  /L
2 va . . 3  setvar  a
3 vn . . 3  setvar  n
4 cz 10658 . . 3  class  ZZ
53cv 1368 . . . . 5  class  n
6 cc0 9294 . . . . 5  class  0
75, 6wceq 1369 . . . 4  wff  n  =  0
82cv 1368 . . . . . . 7  class  a
9 c2 10383 . . . . . . 7  class  2
10 cexp 11877 . . . . . . 7  class  ^
118, 9, 10co 6103 . . . . . 6  class  ( a ^ 2 )
12 c1 9295 . . . . . 6  class  1
1311, 12wceq 1369 . . . . 5  wff  ( a ^ 2 )  =  1
1413, 12, 6cif 3803 . . . 4  class  if ( ( a ^ 2 )  =  1 ,  1 ,  0 )
15 clt 9430 . . . . . . . 8  class  <
165, 6, 15wbr 4304 . . . . . . 7  wff  n  <  0
178, 6, 15wbr 4304 . . . . . . 7  wff  a  <  0
1816, 17wa 369 . . . . . 6  wff  ( n  <  0  /\  a  <  0 )
1912cneg 9608 . . . . . 6  class  -u 1
2018, 19, 12cif 3803 . . . . 5  class  if ( ( n  <  0  /\  a  <  0
) ,  -u 1 ,  1 )
21 cabs 12735 . . . . . . 7  class  abs
225, 21cfv 5430 . . . . . 6  class  ( abs `  n )
23 cmul 9299 . . . . . . 7  class  x.
24 vm . . . . . . . 8  setvar  m
25 cn 10334 . . . . . . . 8  class  NN
2624cv 1368 . . . . . . . . . 10  class  m
27 cprime 13775 . . . . . . . . . 10  class  Prime
2826, 27wcel 1756 . . . . . . . . 9  wff  m  e. 
Prime
2926, 9wceq 1369 . . . . . . . . . . 11  wff  m  =  2
30 cdivides 13547 . . . . . . . . . . . . 13  class  ||
319, 8, 30wbr 4304 . . . . . . . . . . . 12  wff  2  ||  a
32 c8 10389 . . . . . . . . . . . . . . 15  class  8
33 cmo 11720 . . . . . . . . . . . . . . 15  class  mod
348, 32, 33co 6103 . . . . . . . . . . . . . 14  class  ( a  mod  8 )
35 c7 10388 . . . . . . . . . . . . . . 15  class  7
3612, 35cpr 3891 . . . . . . . . . . . . . 14  class  { 1 ,  7 }
3734, 36wcel 1756 . . . . . . . . . . . . 13  wff  ( a  mod  8 )  e. 
{ 1 ,  7 }
3837, 12, 19cif 3803 . . . . . . . . . . . 12  class  if ( ( a  mod  8
)  e.  { 1 ,  7 } , 
1 ,  -u 1
)
3931, 6, 38cif 3803 . . . . . . . . . . 11  class  if ( 2  ||  a ,  0 ,  if ( ( a  mod  8
)  e.  { 1 ,  7 } , 
1 ,  -u 1
) )
40 cmin 9607 . . . . . . . . . . . . . . . . 17  class  -
4126, 12, 40co 6103 . . . . . . . . . . . . . . . 16  class  ( m  -  1 )
42 cdiv 10005 . . . . . . . . . . . . . . . 16  class  /
4341, 9, 42co 6103 . . . . . . . . . . . . . . 15  class  ( ( m  -  1 )  /  2 )
448, 43, 10co 6103 . . . . . . . . . . . . . 14  class  ( a ^ ( ( m  -  1 )  / 
2 ) )
45 caddc 9297 . . . . . . . . . . . . . 14  class  +
4644, 12, 45co 6103 . . . . . . . . . . . . 13  class  ( ( a ^ ( ( m  -  1 )  /  2 ) )  +  1 )
4746, 26, 33co 6103 . . . . . . . . . . . 12  class  ( ( ( a ^ (
( m  -  1 )  /  2 ) )  +  1 )  mod  m )
4847, 12, 40co 6103 . . . . . . . . . . 11  class  ( ( ( ( a ^
( ( m  - 
1 )  /  2
) )  +  1 )  mod  m )  -  1 )
4929, 39, 48cif 3803 . . . . . . . . . 10  class  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 ) )
50 cpc 13915 . . . . . . . . . . 11  class  pCnt
5126, 5, 50co 6103 . . . . . . . . . 10  class  ( m 
pCnt  n )
5249, 51, 10co 6103 . . . . . . . . 9  class  ( 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
) )
5328, 52, 12cif 3803 . . . . . . . 8  class  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 )
5424, 25, 53cmpt 4362 . . . . . . 7  class  ( 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 ) )
5523, 54, 12cseq 11818 . . . . . 6  class  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 ) ) )
5622, 55cfv 5430 . . . . 5  class  (  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 ) )
5720, 56, 23co 6103 . . . 4  class  ( 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 ) ) )
587, 14, 57cif 3803 . . 3  class  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 ) ) ) )
592, 3, 4, 4, 58cmpt2 6105 . 2  class  ( 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 ) ) ) ) )
601, 59wceq 1369 1  wff  /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 ) ) ) ) )
Colors of variables: wff setvar class
This definition is referenced by:  lgsval  22651
  Copyright terms: Public domain W3C validator