Definition df-lgs 27258

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 = (𝑎 ∈ ℤ, 𝑛 ∈ ℤ ↦ if(𝑛 = 0, if((𝑎↑2) = 1, 1, 0), (if((𝑛 < 0 ∧ 𝑎 < 0), -1, 1) · (seq1( · , (𝑚 ∈ ℕ ↦ if(𝑚 ∈ ℙ, (if(𝑚 = 2, if(2 ∥ 𝑎, 0, if((𝑎 mod 8) ∈ {1, 7}, 1, -1)), ((((𝑎↑((𝑚 − 1) / 2)) + 1) mod 𝑚) − 1))↑(𝑚 pCnt 𝑛)), 1)))‘(abs‘𝑛)))))

Distinct variable group:   𝑚,𝑎,𝑛

Detailed syntax breakdown of Definition df-lgs

Step	Hyp	Ref	Expression
1		clgs 27257	. 2 class /L
2		va	. . 3 setvar 𝑎
3		vn	. . 3 setvar 𝑛
4		cz 12524	. . 3 class ℤ
5	3	cv 1541	. . . . 5 class 𝑛
6		cc0 11038	. . . . 5 class 0
7	5, 6	wceq 1542	. . . 4 wff 𝑛 = 0
8	2	cv 1541	. . . . . . 7 class 𝑎
9		c2 12236	. . . . . . 7 class 2
10		cexp 14023	. . . . . . 7 class ↑
11	8, 9, 10	co 7367	. . . . . 6 class (𝑎↑2)
12		c1 11039	. . . . . 6 class 1
13	11, 12	wceq 1542	. . . . 5 wff (𝑎↑2) = 1
14	13, 12, 6	cif 4466	. . . 4 class if((𝑎↑2) = 1, 1, 0)
15		clt 11179	. . . . . . . 8 class <
16	5, 6, 15	wbr 5085	. . . . . . 7 wff 𝑛 < 0
17	8, 6, 15	wbr 5085	. . . . . . 7 wff 𝑎 < 0
18	16, 17	wa 395	. . . . . 6 wff (𝑛 < 0 ∧ 𝑎 < 0)
19	12	cneg 11378	. . . . . 6 class -1
20	18, 19, 12	cif 4466	. . . . 5 class if((𝑛 < 0 ∧ 𝑎 < 0), -1, 1)
21		cabs 15196	. . . . . . 7 class abs
22	5, 21	cfv 6498	. . . . . 6 class (abs‘𝑛)
23		cmul 11043	. . . . . . 7 class ·
24		vm	. . . . . . . 8 setvar 𝑚
25		cn 12174	. . . . . . . 8 class ℕ
26	24	cv 1541	. . . . . . . . . 10 class 𝑚
27		cprime 16640	. . . . . . . . . 10 class ℙ
28	26, 27	wcel 2114	. . . . . . . . 9 wff 𝑚 ∈ ℙ
29	26, 9	wceq 1542	. . . . . . . . . . 11 wff 𝑚 = 2
30		cdvds 16221	. . . . . . . . . . . . 13 class ∥
31	9, 8, 30	wbr 5085	. . . . . . . . . . . 12 wff 2 ∥ 𝑎
32		c8 12242	. . . . . . . . . . . . . . 15 class 8
33		cmo 13828	. . . . . . . . . . . . . . 15 class mod
34	8, 32, 33	co 7367	. . . . . . . . . . . . . 14 class (𝑎 mod 8)
35		c7 12241	. . . . . . . . . . . . . . 15 class 7
36	12, 35	cpr 4569	. . . . . . . . . . . . . 14 class {1, 7}
37	34, 36	wcel 2114	. . . . . . . . . . . . 13 wff (𝑎 mod 8) ∈ {1, 7}
38	37, 12, 19	cif 4466	. . . . . . . . . . . 12 class if((𝑎 mod 8) ∈ {1, 7}, 1, -1)
39	31, 6, 38	cif 4466	. . . . . . . . . . 11 class if(2 ∥ 𝑎, 0, if((𝑎 mod 8) ∈ {1, 7}, 1, -1))
40		cmin 11377	. . . . . . . . . . . . . . . . 17 class −
41	26, 12, 40	co 7367	. . . . . . . . . . . . . . . 16 class (𝑚 − 1)
42		cdiv 11807	. . . . . . . . . . . . . . . 16 class /
43	41, 9, 42	co 7367	. . . . . . . . . . . . . . 15 class ((𝑚 − 1) / 2)
44	8, 43, 10	co 7367	. . . . . . . . . . . . . 14 class (𝑎↑((𝑚 − 1) / 2))
45		caddc 11041	. . . . . . . . . . . . . 14 class +
46	44, 12, 45	co 7367	. . . . . . . . . . . . 13 class ((𝑎↑((𝑚 − 1) / 2)) + 1)
47	46, 26, 33	co 7367	. . . . . . . . . . . 12 class (((𝑎↑((𝑚 − 1) / 2)) + 1) mod 𝑚)
48	47, 12, 40	co 7367	. . . . . . . . . . 11 class ((((𝑎↑((𝑚 − 1) / 2)) + 1) mod 𝑚) − 1)
49	29, 39, 48	cif 4466	. . . . . . . . . 10 class if(𝑚 = 2, if(2 ∥ 𝑎, 0, if((𝑎 mod 8) ∈ {1, 7}, 1, -1)), ((((𝑎↑((𝑚 − 1) / 2)) + 1) mod 𝑚) − 1))
50		cpc 16807	. . . . . . . . . . 11 class pCnt
51	26, 5, 50	co 7367	. . . . . . . . . 10 class (𝑚 pCnt 𝑛)
52	49, 51, 10	co 7367	. . . . . . . . 9 class (if(𝑚 = 2, if(2 ∥ 𝑎, 0, if((𝑎 mod 8) ∈ {1, 7}, 1, -1)), ((((𝑎↑((𝑚 − 1) / 2)) + 1) mod 𝑚) − 1))↑(𝑚 pCnt 𝑛))
53	28, 52, 12	cif 4466	. . . . . . . 8 class if(𝑚 ∈ ℙ, (if(𝑚 = 2, if(2 ∥ 𝑎, 0, if((𝑎 mod 8) ∈ {1, 7}, 1, -1)), ((((𝑎↑((𝑚 − 1) / 2)) + 1) mod 𝑚) − 1))↑(𝑚 pCnt 𝑛)), 1)
54	24, 25, 53	cmpt 5166	. . . . . . 7 class (𝑚 ∈ ℕ ↦ if(𝑚 ∈ ℙ, (if(𝑚 = 2, if(2 ∥ 𝑎, 0, if((𝑎 mod 8) ∈ {1, 7}, 1, -1)), ((((𝑎↑((𝑚 − 1) / 2)) + 1) mod 𝑚) − 1))↑(𝑚 pCnt 𝑛)), 1))
55	23, 54, 12	cseq 13963	. . . . . 6 class seq1( · , (𝑚 ∈ ℕ ↦ if(𝑚 ∈ ℙ, (if(𝑚 = 2, if(2 ∥ 𝑎, 0, if((𝑎 mod 8) ∈ {1, 7}, 1, -1)), ((((𝑎↑((𝑚 − 1) / 2)) + 1) mod 𝑚) − 1))↑(𝑚 pCnt 𝑛)), 1)))
56	22, 55	cfv 6498	. . . . 5 class (seq1( · , (𝑚 ∈ ℕ ↦ if(𝑚 ∈ ℙ, (if(𝑚 = 2, if(2 ∥ 𝑎, 0, if((𝑎 mod 8) ∈ {1, 7}, 1, -1)), ((((𝑎↑((𝑚 − 1) / 2)) + 1) mod 𝑚) − 1))↑(𝑚 pCnt 𝑛)), 1)))‘(abs‘𝑛))
57	20, 56, 23	co 7367	. . . 4 class (if((𝑛 < 0 ∧ 𝑎 < 0), -1, 1) · (seq1( · , (𝑚 ∈ ℕ ↦ if(𝑚 ∈ ℙ, (if(𝑚 = 2, if(2 ∥ 𝑎, 0, if((𝑎 mod 8) ∈ {1, 7}, 1, -1)), ((((𝑎↑((𝑚 − 1) / 2)) + 1) mod 𝑚) − 1))↑(𝑚 pCnt 𝑛)), 1)))‘(abs‘𝑛)))
58	7, 14, 57	cif 4466	. . 3 class if(𝑛 = 0, if((𝑎↑2) = 1, 1, 0), (if((𝑛 < 0 ∧ 𝑎 < 0), -1, 1) · (seq1( · , (𝑚 ∈ ℕ ↦ if(𝑚 ∈ ℙ, (if(𝑚 = 2, if(2 ∥ 𝑎, 0, if((𝑎 mod 8) ∈ {1, 7}, 1, -1)), ((((𝑎↑((𝑚 − 1) / 2)) + 1) mod 𝑚) − 1))↑(𝑚 pCnt 𝑛)), 1)))‘(abs‘𝑛))))
59	2, 3, 4, 4, 58	cmpo 7369	. 2 class (𝑎 ∈ ℤ, 𝑛 ∈ ℤ ↦ if(𝑛 = 0, if((𝑎↑2) = 1, 1, 0), (if((𝑛 < 0 ∧ 𝑎 < 0), -1, 1) · (seq1( · , (𝑚 ∈ ℕ ↦ if(𝑚 ∈ ℙ, (if(𝑚 = 2, if(2 ∥ 𝑎, 0, if((𝑎 mod 8) ∈ {1, 7}, 1, -1)), ((((𝑎↑((𝑚 − 1) / 2)) + 1) mod 𝑚) − 1))↑(𝑚 pCnt 𝑛)), 1)))‘(abs‘𝑛)))))
60	1, 59	wceq 1542	1 wff /L = (𝑎 ∈ ℤ, 𝑛 ∈ ℤ ↦ if(𝑛 = 0, if((𝑎↑2) = 1, 1, 0), (if((𝑛 < 0 ∧ 𝑎 < 0), -1, 1) · (seq1( · , (𝑚 ∈ ℕ ↦ if(𝑚 ∈ ℙ, (if(𝑚 = 2, if(2 ∥ 𝑎, 0, if((𝑎 mod 8) ∈ {1, 7}, 1, -1)), ((((𝑎↑((𝑚 − 1) / 2)) + 1) mod 𝑚) − 1))↑(𝑚 pCnt 𝑛)), 1)))‘(abs‘𝑛)))))

This definition is referenced by:  lgsval  27264