Definition df-lgs 25020

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

Step	Hyp	Ref	Expression
1		clgs 25019	. 2 class /L
2		va	. . 3 setvar a
3		vn	. . 3 setvar n
4		cz 11377	. . 3 class ZZ
5	3	cv 1482	. . . . 5 class n
6		cc0 9936	. . . . 5 class 0
7	5, 6	wceq 1483	. . . 4 wff n = 0
8	2	cv 1482	. . . . . . 7 class a
9		c2 11070	. . . . . . 7 class 2
10		cexp 12860	. . . . . . 7 class ^
11	8, 9, 10	co 6650	. . . . . 6 class ( a ^ 2 )
12		c1 9937	. . . . . 6 class 1
13	11, 12	wceq 1483	. . . . 5 wff ( a ^ 2 ) = 1
14	13, 12, 6	cif 4086	. . . 4 class if ( ( a ^ 2 ) = 1 , 1 , 0 )
15		clt 10074	. . . . . . . 8 class <
16	5, 6, 15	wbr 4653	. . . . . . 7 wff n < 0
17	8, 6, 15	wbr 4653	. . . . . . 7 wff a < 0
18	16, 17	wa 384	. . . . . 6 wff ( n < 0 /\ a < 0 )
19	12	cneg 10267	. . . . . 6 class -u 1
20	18, 19, 12	cif 4086	. . . . 5 class if ( ( n < 0 /\ a < 0 ) , -u 1 , 1 )
21		cabs 13974	. . . . . . 7 class abs
22	5, 21	cfv 5888	. . . . . 6 class ( abs ` n )
23		cmul 9941	. . . . . . 7 class x.
24		vm	. . . . . . . 8 setvar m
25		cn 11020	. . . . . . . 8 class NN
26	24	cv 1482	. . . . . . . . . 10 class m
27		cprime 15385	. . . . . . . . . 10 class Prime
28	26, 27	wcel 1990	. . . . . . . . 9 wff m e. Prime
29	26, 9	wceq 1483	. . . . . . . . . . 11 wff m = 2
30		cdvds 14983	. . . . . . . . . . . . 13 class ||
31	9, 8, 30	wbr 4653	. . . . . . . . . . . 12 wff 2 || a
32		c8 11076	. . . . . . . . . . . . . . 15 class 8
33		cmo 12668	. . . . . . . . . . . . . . 15 class mod
34	8, 32, 33	co 6650	. . . . . . . . . . . . . 14 class ( a mod 8 )
35		c7 11075	. . . . . . . . . . . . . . 15 class 7
36	12, 35	cpr 4179	. . . . . . . . . . . . . 14 class { 1 , 7 }
37	34, 36	wcel 1990	. . . . . . . . . . . . 13 wff ( a mod 8 ) e. { 1 , 7 }
38	37, 12, 19	cif 4086	. . . . . . . . . . . 12 class if ( ( a mod 8 ) e. { 1 , 7 } , 1 , -u 1 )
39	31, 6, 38	cif 4086	. . . . . . . . . . 11 class if ( 2 || a , 0 , if ( ( a mod 8 ) e. { 1 , 7 } , 1 , -u 1 ) )
40		cmin 10266	. . . . . . . . . . . . . . . . 17 class -
41	26, 12, 40	co 6650	. . . . . . . . . . . . . . . 16 class ( m - 1 )
42		cdiv 10684	. . . . . . . . . . . . . . . 16 class /
43	41, 9, 42	co 6650	. . . . . . . . . . . . . . 15 class ( ( m - 1 ) / 2 )
44	8, 43, 10	co 6650	. . . . . . . . . . . . . 14 class ( a ^ ( ( m - 1 ) / 2 ) )
45		caddc 9939	. . . . . . . . . . . . . 14 class +
46	44, 12, 45	co 6650	. . . . . . . . . . . . 13 class ( ( a ^ ( ( m - 1 ) / 2 ) ) + 1 )
47	46, 26, 33	co 6650	. . . . . . . . . . . 12 class ( ( ( a ^ ( ( m - 1 ) / 2 ) ) + 1 ) mod m )
48	47, 12, 40	co 6650	. . . . . . . . . . 11 class ( ( ( ( a ^ ( ( m - 1 ) / 2 ) ) + 1 ) mod m ) - 1 )
49	29, 39, 48	cif 4086	. . . . . . . . . 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 15541	. . . . . . . . . . 11 class pCnt
51	26, 5, 50	co 6650	. . . . . . . . . 10 class ( m pCnt n )
52	49, 51, 10	co 6650	. . . . . . . . 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 ) )
53	28, 52, 12	cif 4086	. . . . . . . 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 )
54	24, 25, 53	cmpt 4729	. . . . . . 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 ) )
55	23, 54, 12	cseq 12801	. . . . . 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 ) ) )
56	22, 55	cfv 5888	. . . . 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 ) )
57	20, 56, 23	co 6650	. . . 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 ) ) )
58	7, 14, 57	cif 4086	. . 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 ) ) ) )
59	2, 3, 4, 4, 58	cmpt2 6652	. 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 ) ) ) ) )
60	1, 59	wceq 1483	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 ) ) ) ) )

This definition is referenced by:  lgsval  25026