Definition df-lgs 15475

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 15474	. 2 class /L
2		va	. . 3 setvar a
3		vn	. . 3 setvar n
4		cz 9372	. . 3 class ZZ
5	3	cv 1372	. . . . 5 class n
6		cc0 7925	. . . . 5 class 0
7	5, 6	wceq 1373	. . . 4 wff n = 0
8	2	cv 1372	. . . . . . 7 class a
9		c2 9087	. . . . . . 7 class 2
10		cexp 10683	. . . . . . 7 class ^
11	8, 9, 10	co 5944	. . . . . 6 class ( a ^ 2 )
12		c1 7926	. . . . . 6 class 1
13	11, 12	wceq 1373	. . . . 5 wff ( a ^ 2 ) = 1
14	13, 12, 6	cif 3571	. . . 4 class if ( ( a ^ 2 ) = 1 , 1 , 0 )
15		clt 8107	. . . . . . . 8 class <
16	5, 6, 15	wbr 4044	. . . . . . 7 wff n < 0
17	8, 6, 15	wbr 4044	. . . . . . 7 wff a < 0
18	16, 17	wa 104	. . . . . 6 wff ( n < 0 /\ a < 0 )
19	12	cneg 8244	. . . . . 6 class -u 1
20	18, 19, 12	cif 3571	. . . . 5 class if ( ( n < 0 /\ a < 0 ) , -u 1 , 1 )
21		cabs 11308	. . . . . . 7 class abs
22	5, 21	cfv 5271	. . . . . 6 class ( abs ` n )
23		cmul 7930	. . . . . . 7 class x.
24		vm	. . . . . . . 8 setvar m
25		cn 9036	. . . . . . . 8 class NN
26	24	cv 1372	. . . . . . . . . 10 class m
27		cprime 12429	. . . . . . . . . 10 class Prime
28	26, 27	wcel 2176	. . . . . . . . 9 wff m e. Prime
29	26, 9	wceq 1373	. . . . . . . . . . 11 wff m = 2
30		cdvds 12098	. . . . . . . . . . . . 13 class ||
31	9, 8, 30	wbr 4044	. . . . . . . . . . . 12 wff 2 || a
32		c8 9093	. . . . . . . . . . . . . . 15 class 8
33		cmo 10467	. . . . . . . . . . . . . . 15 class mod
34	8, 32, 33	co 5944	. . . . . . . . . . . . . 14 class ( a mod 8 )
35		c7 9092	. . . . . . . . . . . . . . 15 class 7
36	12, 35	cpr 3634	. . . . . . . . . . . . . 14 class { 1 , 7 }
37	34, 36	wcel 2176	. . . . . . . . . . . . 13 wff ( a mod 8 ) e. { 1 , 7 }
38	37, 12, 19	cif 3571	. . . . . . . . . . . 12 class if ( ( a mod 8 ) e. { 1 , 7 } , 1 , -u 1 )
39	31, 6, 38	cif 3571	. . . . . . . . . . 11 class if ( 2 || a , 0 , if ( ( a mod 8 ) e. { 1 , 7 } , 1 , -u 1 ) )
40		cmin 8243	. . . . . . . . . . . . . . . . 17 class -
41	26, 12, 40	co 5944	. . . . . . . . . . . . . . . 16 class ( m - 1 )
42		cdiv 8745	. . . . . . . . . . . . . . . 16 class /
43	41, 9, 42	co 5944	. . . . . . . . . . . . . . 15 class ( ( m - 1 ) / 2 )
44	8, 43, 10	co 5944	. . . . . . . . . . . . . 14 class ( a ^ ( ( m - 1 ) / 2 ) )
45		caddc 7928	. . . . . . . . . . . . . 14 class +
46	44, 12, 45	co 5944	. . . . . . . . . . . . 13 class ( ( a ^ ( ( m - 1 ) / 2 ) ) + 1 )
47	46, 26, 33	co 5944	. . . . . . . . . . . 12 class ( ( ( a ^ ( ( m - 1 ) / 2 ) ) + 1 ) mod m )
48	47, 12, 40	co 5944	. . . . . . . . . . 11 class ( ( ( ( a ^ ( ( m - 1 ) / 2 ) ) + 1 ) mod m ) - 1 )
49	29, 39, 48	cif 3571	. . . . . . . . . 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 12607	. . . . . . . . . . 11 class pCnt
51	26, 5, 50	co 5944	. . . . . . . . . 10 class ( m pCnt n )
52	49, 51, 10	co 5944	. . . . . . . . 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 3571	. . . . . . . 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 4105	. . . . . . 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 10592	. . . . . 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 5271	. . . . 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 5944	. . . 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 3571	. . 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 5946	. 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 1373	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  15481