Definition df-lgs 27275

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 27274	. 2 class /L
2		va	. . 3 setvar 𝑎
3		vn	. . 3 setvar 𝑛
4		cz 12518	. . 3 class ℤ
5	3	cv 1541	. . . . 5 class 𝑛
6		cc0 11032	. . . . 5 class 0
7	5, 6	wceq 1542	. . . 4 wff 𝑛 = 0
8	2	cv 1541	. . . . . . 7 class 𝑎
9		c2 12230	. . . . . . 7 class 2
10		cexp 14017	. . . . . . 7 class ↑
11	8, 9, 10	co 7361	. . . . . 6 class (𝑎↑2)
12		c1 11033	. . . . . 6 class 1
13	11, 12	wceq 1542	. . . . 5 wff (𝑎↑2) = 1
14	13, 12, 6	cif 4467	. . . 4 class if((𝑎↑2) = 1, 1, 0)
15		clt 11173	. . . . . . . 8 class <
16	5, 6, 15	wbr 5086	. . . . . . 7 wff 𝑛 < 0
17	8, 6, 15	wbr 5086	. . . . . . 7 wff 𝑎 < 0
18	16, 17	wa 395	. . . . . 6 wff (𝑛 < 0 ∧ 𝑎 < 0)
19	12	cneg 11372	. . . . . 6 class -1
20	18, 19, 12	cif 4467	. . . . 5 class if((𝑛 < 0 ∧ 𝑎 < 0), -1, 1)
21		cabs 15190	. . . . . . 7 class abs
22	5, 21	cfv 6493	. . . . . 6 class (abs‘𝑛)
23		cmul 11037	. . . . . . 7 class ·
24		vm	. . . . . . . 8 setvar 𝑚
25		cn 12168	. . . . . . . 8 class ℕ
26	24	cv 1541	. . . . . . . . . 10 class 𝑚
27		cprime 16634	. . . . . . . . . 10 class ℙ
28	26, 27	wcel 2114	. . . . . . . . 9 wff 𝑚 ∈ ℙ
29	26, 9	wceq 1542	. . . . . . . . . . 11 wff 𝑚 = 2
30		cdvds 16215	. . . . . . . . . . . . 13 class ∥
31	9, 8, 30	wbr 5086	. . . . . . . . . . . 12 wff 2 ∥ 𝑎
32		c8 12236	. . . . . . . . . . . . . . 15 class 8
33		cmo 13822	. . . . . . . . . . . . . . 15 class mod
34	8, 32, 33	co 7361	. . . . . . . . . . . . . 14 class (𝑎 mod 8)
35		c7 12235	. . . . . . . . . . . . . . 15 class 7
36	12, 35	cpr 4570	. . . . . . . . . . . . . 14 class {1, 7}
37	34, 36	wcel 2114	. . . . . . . . . . . . 13 wff (𝑎 mod 8) ∈ {1, 7}
38	37, 12, 19	cif 4467	. . . . . . . . . . . 12 class if((𝑎 mod 8) ∈ {1, 7}, 1, -1)
39	31, 6, 38	cif 4467	. . . . . . . . . . 11 class if(2 ∥ 𝑎, 0, if((𝑎 mod 8) ∈ {1, 7}, 1, -1))
40		cmin 11371	. . . . . . . . . . . . . . . . 17 class −
41	26, 12, 40	co 7361	. . . . . . . . . . . . . . . 16 class (𝑚 − 1)
42		cdiv 11801	. . . . . . . . . . . . . . . 16 class /
43	41, 9, 42	co 7361	. . . . . . . . . . . . . . 15 class ((𝑚 − 1) / 2)
44	8, 43, 10	co 7361	. . . . . . . . . . . . . 14 class (𝑎↑((𝑚 − 1) / 2))
45		caddc 11035	. . . . . . . . . . . . . 14 class +
46	44, 12, 45	co 7361	. . . . . . . . . . . . 13 class ((𝑎↑((𝑚 − 1) / 2)) + 1)
47	46, 26, 33	co 7361	. . . . . . . . . . . 12 class (((𝑎↑((𝑚 − 1) / 2)) + 1) mod 𝑚)
48	47, 12, 40	co 7361	. . . . . . . . . . 11 class ((((𝑎↑((𝑚 − 1) / 2)) + 1) mod 𝑚) − 1)
49	29, 39, 48	cif 4467	. . . . . . . . . 10 class if(𝑚 = 2, if(2 ∥ 𝑎, 0, if((𝑎 mod 8) ∈ {1, 7}, 1, -1)), ((((𝑎↑((𝑚 − 1) / 2)) + 1) mod 𝑚) − 1))
50		cpc 16801	. . . . . . . . . . 11 class pCnt
51	26, 5, 50	co 7361	. . . . . . . . . 10 class (𝑚 pCnt 𝑛)
52	49, 51, 10	co 7361	. . . . . . . . 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 4467	. . . . . . . 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 5167	. . . . . . 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 13957	. . . . . 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 6493	. . . . 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 7361	. . . 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 4467	. . 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 7363	. 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  27281