Definition df-lgs 13693

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 13692	. 2 class /L
2		va	. . 3 setvar a
3		vn	. . 3 setvar n
4		cz 9212	. . 3 class ZZ
5	3	cv 1347	. . . . 5 class n
6		cc0 7774	. . . . 5 class 0
7	5, 6	wceq 1348	. . . 4 wff n = 0
8	2	cv 1347	. . . . . . 7 class a
9		c2 8929	. . . . . . 7 class 2
10		cexp 10475	. . . . . . 7 class ^
11	8, 9, 10	co 5853	. . . . . 6 class ( a ^ 2 )
12		c1 7775	. . . . . 6 class 1
13	11, 12	wceq 1348	. . . . 5 wff ( a ^ 2 ) = 1
14	13, 12, 6	cif 3526	. . . 4 class if ( ( a ^ 2 ) = 1 , 1 , 0 )
15		clt 7954	. . . . . . . 8 class <
16	5, 6, 15	wbr 3989	. . . . . . 7 wff n < 0
17	8, 6, 15	wbr 3989	. . . . . . 7 wff a < 0
18	16, 17	wa 103	. . . . . 6 wff ( n < 0 /\ a < 0 )
19	12	cneg 8091	. . . . . 6 class -u 1
20	18, 19, 12	cif 3526	. . . . 5 class if ( ( n < 0 /\ a < 0 ) , -u 1 , 1 )
21		cabs 10961	. . . . . . 7 class abs
22	5, 21	cfv 5198	. . . . . 6 class ( abs ` n )
23		cmul 7779	. . . . . . 7 class x.
24		vm	. . . . . . . 8 setvar m
25		cn 8878	. . . . . . . 8 class NN
26	24	cv 1347	. . . . . . . . . 10 class m
27		cprime 12061	. . . . . . . . . 10 class Prime
28	26, 27	wcel 2141	. . . . . . . . 9 wff m e. Prime
29	26, 9	wceq 1348	. . . . . . . . . . 11 wff m = 2
30		cdvds 11749	. . . . . . . . . . . . 13 class ||
31	9, 8, 30	wbr 3989	. . . . . . . . . . . 12 wff 2 || a
32		c8 8935	. . . . . . . . . . . . . . 15 class 8
33		cmo 10278	. . . . . . . . . . . . . . 15 class mod
34	8, 32, 33	co 5853	. . . . . . . . . . . . . 14 class ( a mod 8 )
35		c7 8934	. . . . . . . . . . . . . . 15 class 7
36	12, 35	cpr 3584	. . . . . . . . . . . . . 14 class { 1 , 7 }
37	34, 36	wcel 2141	. . . . . . . . . . . . 13 wff ( a mod 8 ) e. { 1 , 7 }
38	37, 12, 19	cif 3526	. . . . . . . . . . . 12 class if ( ( a mod 8 ) e. { 1 , 7 } , 1 , -u 1 )
39	31, 6, 38	cif 3526	. . . . . . . . . . 11 class if ( 2 || a , 0 , if ( ( a mod 8 ) e. { 1 , 7 } , 1 , -u 1 ) )
40		cmin 8090	. . . . . . . . . . . . . . . . 17 class -
41	26, 12, 40	co 5853	. . . . . . . . . . . . . . . 16 class ( m - 1 )
42		cdiv 8589	. . . . . . . . . . . . . . . 16 class /
43	41, 9, 42	co 5853	. . . . . . . . . . . . . . 15 class ( ( m - 1 ) / 2 )
44	8, 43, 10	co 5853	. . . . . . . . . . . . . 14 class ( a ^ ( ( m - 1 ) / 2 ) )
45		caddc 7777	. . . . . . . . . . . . . 14 class +
46	44, 12, 45	co 5853	. . . . . . . . . . . . 13 class ( ( a ^ ( ( m - 1 ) / 2 ) ) + 1 )
47	46, 26, 33	co 5853	. . . . . . . . . . . 12 class ( ( ( a ^ ( ( m - 1 ) / 2 ) ) + 1 ) mod m )
48	47, 12, 40	co 5853	. . . . . . . . . . 11 class ( ( ( ( a ^ ( ( m - 1 ) / 2 ) ) + 1 ) mod m ) - 1 )
49	29, 39, 48	cif 3526	. . . . . . . . . 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 12238	. . . . . . . . . . 11 class pCnt
51	26, 5, 50	co 5853	. . . . . . . . . 10 class ( m pCnt n )
52	49, 51, 10	co 5853	. . . . . . . . 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 3526	. . . . . . . 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 4050	. . . . . . 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 10401	. . . . . 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 5198	. . . . 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 5853	. . . 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 3526	. . 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	cmpo 5855	. 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 1348	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  13699