Definition df-lgs 15347

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 15346	. 2 class /L
2		va	. . 3 setvar a
3		vn	. . 3 setvar n
4		cz 9345	. . 3 class ZZ
5	3	cv 1363	. . . . 5 class n
6		cc0 7898	. . . . 5 class 0
7	5, 6	wceq 1364	. . . 4 wff n = 0
8	2	cv 1363	. . . . . . 7 class a
9		c2 9060	. . . . . . 7 class 2
10		cexp 10649	. . . . . . 7 class ^
11	8, 9, 10	co 5925	. . . . . 6 class ( a ^ 2 )
12		c1 7899	. . . . . 6 class 1
13	11, 12	wceq 1364	. . . . 5 wff ( a ^ 2 ) = 1
14	13, 12, 6	cif 3562	. . . 4 class if ( ( a ^ 2 ) = 1 , 1 , 0 )
15		clt 8080	. . . . . . . 8 class <
16	5, 6, 15	wbr 4034	. . . . . . 7 wff n < 0
17	8, 6, 15	wbr 4034	. . . . . . 7 wff a < 0
18	16, 17	wa 104	. . . . . 6 wff ( n < 0 /\ a < 0 )
19	12	cneg 8217	. . . . . 6 class -u 1
20	18, 19, 12	cif 3562	. . . . 5 class if ( ( n < 0 /\ a < 0 ) , -u 1 , 1 )
21		cabs 11181	. . . . . . 7 class abs
22	5, 21	cfv 5259	. . . . . 6 class ( abs ` n )
23		cmul 7903	. . . . . . 7 class x.
24		vm	. . . . . . . 8 setvar m
25		cn 9009	. . . . . . . 8 class NN
26	24	cv 1363	. . . . . . . . . 10 class m
27		cprime 12302	. . . . . . . . . 10 class Prime
28	26, 27	wcel 2167	. . . . . . . . 9 wff m e. Prime
29	26, 9	wceq 1364	. . . . . . . . . . 11 wff m = 2
30		cdvds 11971	. . . . . . . . . . . . 13 class ||
31	9, 8, 30	wbr 4034	. . . . . . . . . . . 12 wff 2 || a
32		c8 9066	. . . . . . . . . . . . . . 15 class 8
33		cmo 10433	. . . . . . . . . . . . . . 15 class mod
34	8, 32, 33	co 5925	. . . . . . . . . . . . . 14 class ( a mod 8 )
35		c7 9065	. . . . . . . . . . . . . . 15 class 7
36	12, 35	cpr 3624	. . . . . . . . . . . . . 14 class { 1 , 7 }
37	34, 36	wcel 2167	. . . . . . . . . . . . 13 wff ( a mod 8 ) e. { 1 , 7 }
38	37, 12, 19	cif 3562	. . . . . . . . . . . 12 class if ( ( a mod 8 ) e. { 1 , 7 } , 1 , -u 1 )
39	31, 6, 38	cif 3562	. . . . . . . . . . 11 class if ( 2 || a , 0 , if ( ( a mod 8 ) e. { 1 , 7 } , 1 , -u 1 ) )
40		cmin 8216	. . . . . . . . . . . . . . . . 17 class -
41	26, 12, 40	co 5925	. . . . . . . . . . . . . . . 16 class ( m - 1 )
42		cdiv 8718	. . . . . . . . . . . . . . . 16 class /
43	41, 9, 42	co 5925	. . . . . . . . . . . . . . 15 class ( ( m - 1 ) / 2 )
44	8, 43, 10	co 5925	. . . . . . . . . . . . . 14 class ( a ^ ( ( m - 1 ) / 2 ) )
45		caddc 7901	. . . . . . . . . . . . . 14 class +
46	44, 12, 45	co 5925	. . . . . . . . . . . . 13 class ( ( a ^ ( ( m - 1 ) / 2 ) ) + 1 )
47	46, 26, 33	co 5925	. . . . . . . . . . . 12 class ( ( ( a ^ ( ( m - 1 ) / 2 ) ) + 1 ) mod m )
48	47, 12, 40	co 5925	. . . . . . . . . . 11 class ( ( ( ( a ^ ( ( m - 1 ) / 2 ) ) + 1 ) mod m ) - 1 )
49	29, 39, 48	cif 3562	. . . . . . . . . 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 12480	. . . . . . . . . . 11 class pCnt
51	26, 5, 50	co 5925	. . . . . . . . . 10 class ( m pCnt n )
52	49, 51, 10	co 5925	. . . . . . . . 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 3562	. . . . . . . 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 4095	. . . . . . 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 10558	. . . . . 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 5259	. . . . 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 5925	. . . 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 3562	. . 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 5927	. 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 1364	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  15353