Definition df-lgs 16283

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 16282	. 2 class /L
2		va	. . 3 setvar a
3		vn	. . 3 setvar n
4		cz 9649	. . 3 class ZZ
5	3	cv 1401	. . . . 5 class n
6		cc0 8180	. . . . 5 class 0
7	5, 6	wceq 1402	. . . 4 wff n = 0
8	2	cv 1401	. . . . . . 7 class a
9		c2 9358	. . . . . . 7 class 2
10		cexp 10990	. . . . . . 7 class ^
11	8, 9, 10	co 6085	. . . . . 6 class ( a ^ 2 )
12		c1 8181	. . . . . 6 class 1
13	11, 12	wceq 1402	. . . . 5 wff ( a ^ 2 ) = 1
14	13, 12, 6	cif 3638	. . . 4 class if ( ( a ^ 2 ) = 1 , 1 , 0 )
15		clt 8361	. . . . . . . 8 class <
16	5, 6, 15	wbr 4130	. . . . . . 7 wff n < 0
17	8, 6, 15	wbr 4130	. . . . . . 7 wff a < 0
18	16, 17	wa 104	. . . . . 6 wff ( n < 0 /\ a < 0 )
19	12	cneg 8500	. . . . . 6 class -u 1
20	18, 19, 12	cif 3638	. . . . 5 class if ( ( n < 0 /\ a < 0 ) , -u 1 , 1 )
21		cabs 11779	. . . . . . 7 class abs
22	5, 21	cfv 5377	. . . . . 6 class ( abs ` n )
23		cmul 8185	. . . . . . 7 class x.
24		vm	. . . . . . . 8 setvar m
25		cn 9307	. . . . . . . 8 class NN
26	24	cv 1401	. . . . . . . . . 10 class m
27		cprime 12904	. . . . . . . . . 10 class Prime
28	26, 27	wcel 2209	. . . . . . . . 9 wff m e. Prime
29	26, 9	wceq 1402	. . . . . . . . . . 11 wff m = 2
30		cdvds 12573	. . . . . . . . . . . . 13 class ||
31	9, 8, 30	wbr 4130	. . . . . . . . . . . 12 wff 2 || a
32		c8 9364	. . . . . . . . . . . . . . 15 class 8
33		cmo 10774	. . . . . . . . . . . . . . 15 class mod
34	8, 32, 33	co 6085	. . . . . . . . . . . . . 14 class ( a mod 8 )
35		c7 9363	. . . . . . . . . . . . . . 15 class 7
36	12, 35	cpr 3710	. . . . . . . . . . . . . 14 class { 1 , 7 }
37	34, 36	wcel 2209	. . . . . . . . . . . . 13 wff ( a mod 8 ) e. { 1 , 7 }
38	37, 12, 19	cif 3638	. . . . . . . . . . . 12 class if ( ( a mod 8 ) e. { 1 , 7 } , 1 , -u 1 )
39	31, 6, 38	cif 3638	. . . . . . . . . . 11 class if ( 2 || a , 0 , if ( ( a mod 8 ) e. { 1 , 7 } , 1 , -u 1 ) )
40		cmin 8499	. . . . . . . . . . . . . . . . 17 class -
41	26, 12, 40	co 6085	. . . . . . . . . . . . . . . 16 class ( m - 1 )
42		cdiv 9005	. . . . . . . . . . . . . . . 16 class /
43	41, 9, 42	co 6085	. . . . . . . . . . . . . . 15 class ( ( m - 1 ) / 2 )
44	8, 43, 10	co 6085	. . . . . . . . . . . . . 14 class ( a ^ ( ( m - 1 ) / 2 ) )
45		caddc 8183	. . . . . . . . . . . . . 14 class +
46	44, 12, 45	co 6085	. . . . . . . . . . . . 13 class ( ( a ^ ( ( m - 1 ) / 2 ) ) + 1 )
47	46, 26, 33	co 6085	. . . . . . . . . . . 12 class ( ( ( a ^ ( ( m - 1 ) / 2 ) ) + 1 ) mod m )
48	47, 12, 40	co 6085	. . . . . . . . . . 11 class ( ( ( ( a ^ ( ( m - 1 ) / 2 ) ) + 1 ) mod m ) - 1 )
49	29, 39, 48	cif 3638	. . . . . . . . . 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 13086	. . . . . . . . . . 11 class pCnt
51	26, 5, 50	co 6085	. . . . . . . . . 10 class ( m pCnt n )
52	49, 51, 10	co 6085	. . . . . . . . 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 3638	. . . . . . . 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 4192	. . . . . . 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 10899	. . . . . 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 5377	. . . . 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 6085	. . . 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 3638	. . 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 6087	. 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 1402	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 used by:  lgsval  16289