ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  df-lgs Unicode version

Definition df-lgs 13970
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.)
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 13969 . 2  class  /L
2 va . . 3  setvar  a
3 vn . . 3  setvar  n
4 cz 9226 . . 3  class  ZZ
53cv 1352 . . . . 5  class  n
6 cc0 7786 . . . . 5  class  0
75, 6wceq 1353 . . . 4  wff  n  =  0
82cv 1352 . . . . . . 7  class  a
9 c2 8943 . . . . . . 7  class  2
10 cexp 10489 . . . . . . 7  class  ^
118, 9, 10co 5865 . . . . . 6  class  ( a ^ 2 )
12 c1 7787 . . . . . 6  class  1
1311, 12wceq 1353 . . . . 5  wff  ( a ^ 2 )  =  1
1413, 12, 6cif 3532 . . . 4  class  if ( ( a ^ 2 )  =  1 ,  1 ,  0 )
15 clt 7966 . . . . . . . 8  class  <
165, 6, 15wbr 3998 . . . . . . 7  wff  n  <  0
178, 6, 15wbr 3998 . . . . . . 7  wff  a  <  0
1816, 17wa 104 . . . . . 6  wff  ( n  <  0  /\  a  <  0 )
1912cneg 8103 . . . . . 6  class  -u 1
2018, 19, 12cif 3532 . . . . 5  class  if ( ( n  <  0  /\  a  <  0
) ,  -u 1 ,  1 )
21 cabs 10974 . . . . . . 7  class  abs
225, 21cfv 5208 . . . . . 6  class  ( abs `  n )
23 cmul 7791 . . . . . . 7  class  x.
24 vm . . . . . . . 8  setvar  m
25 cn 8892 . . . . . . . 8  class  NN
2624cv 1352 . . . . . . . . . 10  class  m
27 cprime 12074 . . . . . . . . . 10  class  Prime
2826, 27wcel 2146 . . . . . . . . 9  wff  m  e. 
Prime
2926, 9wceq 1353 . . . . . . . . . . 11  wff  m  =  2
30 cdvds 11762 . . . . . . . . . . . . 13  class  ||
319, 8, 30wbr 3998 . . . . . . . . . . . 12  wff  2  ||  a
32 c8 8949 . . . . . . . . . . . . . . 15  class  8
33 cmo 10292 . . . . . . . . . . . . . . 15  class  mod
348, 32, 33co 5865 . . . . . . . . . . . . . 14  class  ( a  mod  8 )
35 c7 8948 . . . . . . . . . . . . . . 15  class  7
3612, 35cpr 3590 . . . . . . . . . . . . . 14  class  { 1 ,  7 }
3734, 36wcel 2146 . . . . . . . . . . . . 13  wff  ( a  mod  8 )  e. 
{ 1 ,  7 }
3837, 12, 19cif 3532 . . . . . . . . . . . 12  class  if ( ( a  mod  8
)  e.  { 1 ,  7 } , 
1 ,  -u 1
)
3931, 6, 38cif 3532 . . . . . . . . . . 11  class  if ( 2  ||  a ,  0 ,  if ( ( a  mod  8
)  e.  { 1 ,  7 } , 
1 ,  -u 1
) )
40 cmin 8102 . . . . . . . . . . . . . . . . 17  class  -
4126, 12, 40co 5865 . . . . . . . . . . . . . . . 16  class  ( m  -  1 )
42 cdiv 8602 . . . . . . . . . . . . . . . 16  class  /
4341, 9, 42co 5865 . . . . . . . . . . . . . . 15  class  ( ( m  -  1 )  /  2 )
448, 43, 10co 5865 . . . . . . . . . . . . . 14  class  ( a ^ ( ( m  -  1 )  / 
2 ) )
45 caddc 7789 . . . . . . . . . . . . . 14  class  +
4644, 12, 45co 5865 . . . . . . . . . . . . 13  class  ( ( a ^ ( ( m  -  1 )  /  2 ) )  +  1 )
4746, 26, 33co 5865 . . . . . . . . . . . 12  class  ( ( ( a ^ (
( m  -  1 )  /  2 ) )  +  1 )  mod  m )
4847, 12, 40co 5865 . . . . . . . . . . 11  class  ( ( ( ( a ^
( ( m  - 
1 )  /  2
) )  +  1 )  mod  m )  -  1 )
4929, 39, 48cif 3532 . . . . . . . . . 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 12251 . . . . . . . . . . 11  class  pCnt
5126, 5, 50co 5865 . . . . . . . . . 10  class  ( m 
pCnt  n )
5249, 51, 10co 5865 . . . . . . . . 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 3532 . . . . . . . 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 4059 . . . . . . 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 10415 . . . . . 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 5208 . . . . 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 5865 . . . 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 3532 . . 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, 58cmpo 5867 . 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 1353 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 set class
This definition is referenced by:  lgsval  13976
  Copyright terms: Public domain W3C validator