Definition df-lgs 27280

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 27279	. 2 class /L
2		va	. . 3 setvar 𝑎
3		vn	. . 3 setvar 𝑛
4		cz 12519	. . 3 class ℤ
5	3	cv 1547	. . . . 5 class 𝑛
6		cc0 11033	. . . . 5 class 0
7	5, 6	wceq 1548	. . . 4 wff 𝑛 = 0
8	2	cv 1547	. . . . . . 7 class 𝑎
9		c2 12231	. . . . . . 7 class 2
10		cexp 14018	. . . . . . 7 class ↑
11	8, 9, 10	co 7360	. . . . . 6 class (𝑎↑2)
12		c1 11034	. . . . . 6 class 1
13	11, 12	wceq 1548	. . . . 5 wff (𝑎↑2) = 1
14	13, 12, 6	cif 4457	. . . 4 class if((𝑎↑2) = 1, 1, 0)
15		clt 11174	. . . . . . . 8 class <
16	5, 6, 15	wbr 5075	. . . . . . 7 wff 𝑛 < 0
17	8, 6, 15	wbr 5075	. . . . . . 7 wff 𝑎 < 0
18	16, 17	wa 397	. . . . . 6 wff (𝑛 < 0 ∧ 𝑎 < 0)
19	12	cneg 11373	. . . . . 6 class -1
20	18, 19, 12	cif 4457	. . . . 5 class if((𝑛 < 0 ∧ 𝑎 < 0), -1, 1)
21		cabs 15191	. . . . . . 7 class abs
22	5, 21	cfv 6489	. . . . . 6 class (abs‘𝑛)
23		cmul 11038	. . . . . . 7 class ·
24		vm	. . . . . . . 8 setvar 𝑚
25		cn 12169	. . . . . . . 8 class ℕ
26	24	cv 1547	. . . . . . . . . 10 class 𝑚
27		cprime 16635	. . . . . . . . . 10 class ℙ
28	26, 27	wcel 2121	. . . . . . . . 9 wff 𝑚 ∈ ℙ
29	26, 9	wceq 1548	. . . . . . . . . . 11 wff 𝑚 = 2
30		cdvds 16216	. . . . . . . . . . . . 13 class ∥
31	9, 8, 30	wbr 5075	. . . . . . . . . . . 12 wff 2 ∥ 𝑎
32		c8 12237	. . . . . . . . . . . . . . 15 class 8
33		cmo 13823	. . . . . . . . . . . . . . 15 class mod
34	8, 32, 33	co 7360	. . . . . . . . . . . . . 14 class (𝑎 mod 8)
35		c7 12236	. . . . . . . . . . . . . . 15 class 7
36	12, 35	cpr 4560	. . . . . . . . . . . . . 14 class {1, 7}
37	34, 36	wcel 2121	. . . . . . . . . . . . 13 wff (𝑎 mod 8) ∈ {1, 7}
38	37, 12, 19	cif 4457	. . . . . . . . . . . 12 class if((𝑎 mod 8) ∈ {1, 7}, 1, -1)
39	31, 6, 38	cif 4457	. . . . . . . . . . 11 class if(2 ∥ 𝑎, 0, if((𝑎 mod 8) ∈ {1, 7}, 1, -1))
40		cmin 11372	. . . . . . . . . . . . . . . . 17 class −
41	26, 12, 40	co 7360	. . . . . . . . . . . . . . . 16 class (𝑚 − 1)
42		cdiv 11802	. . . . . . . . . . . . . . . 16 class /
43	41, 9, 42	co 7360	. . . . . . . . . . . . . . 15 class ((𝑚 − 1) / 2)
44	8, 43, 10	co 7360	. . . . . . . . . . . . . 14 class (𝑎↑((𝑚 − 1) / 2))
45		caddc 11036	. . . . . . . . . . . . . 14 class +
46	44, 12, 45	co 7360	. . . . . . . . . . . . 13 class ((𝑎↑((𝑚 − 1) / 2)) + 1)
47	46, 26, 33	co 7360	. . . . . . . . . . . 12 class (((𝑎↑((𝑚 − 1) / 2)) + 1) mod 𝑚)
48	47, 12, 40	co 7360	. . . . . . . . . . 11 class ((((𝑎↑((𝑚 − 1) / 2)) + 1) mod 𝑚) − 1)
49	29, 39, 48	cif 4457	. . . . . . . . . 10 class if(𝑚 = 2, if(2 ∥ 𝑎, 0, if((𝑎 mod 8) ∈ {1, 7}, 1, -1)), ((((𝑎↑((𝑚 − 1) / 2)) + 1) mod 𝑚) − 1))
50		cpc 16802	. . . . . . . . . . 11 class pCnt
51	26, 5, 50	co 7360	. . . . . . . . . 10 class (𝑚 pCnt 𝑛)
52	49, 51, 10	co 7360	. . . . . . . . 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 4457	. . . . . . . 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 5156	. . . . . . 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 13958	. . . . . 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 6489	. . . . 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 7360	. . . 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 4457	. . 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 7362	. 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 1548	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  27286