Definition df-lgs 27424

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 27423	. 2 class /L
2		va	. . 3 setvar 𝑎
3		vn	. . 3 setvar 𝑛
4		cz 12590	. . 3 class ℤ
5	3	cv 1566	. . . . 5 class 𝑛
6		cc0 11099	. . . . 5 class 0
7	5, 6	wceq 1567	. . . 4 wff 𝑛 = 0
8	2	cv 1566	. . . . . . 7 class 𝑎
9		c2 12294	. . . . . . 7 class 2
10		cexp 14096	. . . . . . 7 class ↑
11	8, 9, 10	co 7411	. . . . . 6 class (𝑎↑2)
12		c1 11100	. . . . . 6 class 1
13	11, 12	wceq 1567	. . . . 5 wff (𝑎↑2) = 1
14	13, 12, 6	cif 4492	. . . 4 class if((𝑎↑2) = 1, 1, 0)
15		clt 11242	. . . . . . . 8 class <
16	5, 6, 15	wbr 5113	. . . . . . 7 wff 𝑛 < 0
17	8, 6, 15	wbr 5113	. . . . . . 7 wff 𝑎 < 0
18	16, 17	wa 400	. . . . . 6 wff (𝑛 < 0 ∧ 𝑎 < 0)
19	12	cneg 11441	. . . . . 6 class -1
20	18, 19, 12	cif 4492	. . . . 5 class if((𝑛 < 0 ∧ 𝑎 < 0), -1, 1)
21		cabs 15284	. . . . . . 7 class abs
22	5, 21	cfv 6537	. . . . . 6 class (abs‘𝑛)
23		cmul 11104	. . . . . . 7 class ·
24		vm	. . . . . . . 8 setvar 𝑚
25		cn 12232	. . . . . . . 8 class ℕ
26	24	cv 1566	. . . . . . . . . 10 class 𝑚
27		cprime 16728	. . . . . . . . . 10 class ℙ
28	26, 27	wcel 2149	. . . . . . . . 9 wff 𝑚 ∈ ℙ
29	26, 9	wceq 1567	. . . . . . . . . . 11 wff 𝑚 = 2
30		cdvds 16309	. . . . . . . . . . . . 13 class ∥
31	9, 8, 30	wbr 5113	. . . . . . . . . . . 12 wff 2 ∥ 𝑎
32		c8 12300	. . . . . . . . . . . . . . 15 class 8
33		cmo 13901	. . . . . . . . . . . . . . 15 class mod
34	8, 32, 33	co 7411	. . . . . . . . . . . . . 14 class (𝑎 mod 8)
35		c7 12299	. . . . . . . . . . . . . . 15 class 7
36	12, 35	cpr 4596	. . . . . . . . . . . . . 14 class {1, 7}
37	34, 36	wcel 2149	. . . . . . . . . . . . 13 wff (𝑎 mod 8) ∈ {1, 7}
38	37, 12, 19	cif 4492	. . . . . . . . . . . 12 class if((𝑎 mod 8) ∈ {1, 7}, 1, -1)
39	31, 6, 38	cif 4492	. . . . . . . . . . 11 class if(2 ∥ 𝑎, 0, if((𝑎 mod 8) ∈ {1, 7}, 1, -1))
40		cmin 11440	. . . . . . . . . . . . . . . . 17 class −
41	26, 12, 40	co 7411	. . . . . . . . . . . . . . . 16 class (𝑚 − 1)
42		cdiv 11870	. . . . . . . . . . . . . . . 16 class /
43	41, 9, 42	co 7411	. . . . . . . . . . . . . . 15 class ((𝑚 − 1) / 2)
44	8, 43, 10	co 7411	. . . . . . . . . . . . . 14 class (𝑎↑((𝑚 − 1) / 2))
45		caddc 11102	. . . . . . . . . . . . . 14 class +
46	44, 12, 45	co 7411	. . . . . . . . . . . . 13 class ((𝑎↑((𝑚 − 1) / 2)) + 1)
47	46, 26, 33	co 7411	. . . . . . . . . . . 12 class (((𝑎↑((𝑚 − 1) / 2)) + 1) mod 𝑚)
48	47, 12, 40	co 7411	. . . . . . . . . . 11 class ((((𝑎↑((𝑚 − 1) / 2)) + 1) mod 𝑚) − 1)
49	29, 39, 48	cif 4492	. . . . . . . . . 10 class if(𝑚 = 2, if(2 ∥ 𝑎, 0, if((𝑎 mod 8) ∈ {1, 7}, 1, -1)), ((((𝑎↑((𝑚 − 1) / 2)) + 1) mod 𝑚) − 1))
50		cpc 16895	. . . . . . . . . . 11 class pCnt
51	26, 5, 50	co 7411	. . . . . . . . . 10 class (𝑚 pCnt 𝑛)
52	49, 51, 10	co 7411	. . . . . . . . 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 4492	. . . . . . . 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 5196	. . . . . . 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 14036	. . . . . 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 6537	. . . . 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 7411	. . . 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 4492	. . 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 7413	. 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 1567	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  27430