Definition df-lgs 27260

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 27259	. 2 class /L
2		va	. . 3 setvar 𝑎
3		vn	. . 3 setvar 𝑛
4		cz 12486	. . 3 class ℤ
5	3	cv 1540	. . . . 5 class 𝑛
6		cc0 11024	. . . . 5 class 0
7	5, 6	wceq 1541	. . . 4 wff 𝑛 = 0
8	2	cv 1540	. . . . . . 7 class 𝑎
9		c2 12198	. . . . . . 7 class 2
10		cexp 13982	. . . . . . 7 class ↑
11	8, 9, 10	co 7356	. . . . . 6 class (𝑎↑2)
12		c1 11025	. . . . . 6 class 1
13	11, 12	wceq 1541	. . . . 5 wff (𝑎↑2) = 1
14	13, 12, 6	cif 4477	. . . 4 class if((𝑎↑2) = 1, 1, 0)
15		clt 11164	. . . . . . . 8 class <
16	5, 6, 15	wbr 5096	. . . . . . 7 wff 𝑛 < 0
17	8, 6, 15	wbr 5096	. . . . . . 7 wff 𝑎 < 0
18	16, 17	wa 395	. . . . . 6 wff (𝑛 < 0 ∧ 𝑎 < 0)
19	12	cneg 11363	. . . . . 6 class -1
20	18, 19, 12	cif 4477	. . . . 5 class if((𝑛 < 0 ∧ 𝑎 < 0), -1, 1)
21		cabs 15155	. . . . . . 7 class abs
22	5, 21	cfv 6490	. . . . . 6 class (abs‘𝑛)
23		cmul 11029	. . . . . . 7 class ·
24		vm	. . . . . . . 8 setvar 𝑚
25		cn 12143	. . . . . . . 8 class ℕ
26	24	cv 1540	. . . . . . . . . 10 class 𝑚
27		cprime 16596	. . . . . . . . . 10 class ℙ
28	26, 27	wcel 2113	. . . . . . . . 9 wff 𝑚 ∈ ℙ
29	26, 9	wceq 1541	. . . . . . . . . . 11 wff 𝑚 = 2
30		cdvds 16177	. . . . . . . . . . . . 13 class ∥
31	9, 8, 30	wbr 5096	. . . . . . . . . . . 12 wff 2 ∥ 𝑎
32		c8 12204	. . . . . . . . . . . . . . 15 class 8
33		cmo 13787	. . . . . . . . . . . . . . 15 class mod
34	8, 32, 33	co 7356	. . . . . . . . . . . . . 14 class (𝑎 mod 8)
35		c7 12203	. . . . . . . . . . . . . . 15 class 7
36	12, 35	cpr 4580	. . . . . . . . . . . . . 14 class {1, 7}
37	34, 36	wcel 2113	. . . . . . . . . . . . 13 wff (𝑎 mod 8) ∈ {1, 7}
38	37, 12, 19	cif 4477	. . . . . . . . . . . 12 class if((𝑎 mod 8) ∈ {1, 7}, 1, -1)
39	31, 6, 38	cif 4477	. . . . . . . . . . 11 class if(2 ∥ 𝑎, 0, if((𝑎 mod 8) ∈ {1, 7}, 1, -1))
40		cmin 11362	. . . . . . . . . . . . . . . . 17 class −
41	26, 12, 40	co 7356	. . . . . . . . . . . . . . . 16 class (𝑚 − 1)
42		cdiv 11792	. . . . . . . . . . . . . . . 16 class /
43	41, 9, 42	co 7356	. . . . . . . . . . . . . . 15 class ((𝑚 − 1) / 2)
44	8, 43, 10	co 7356	. . . . . . . . . . . . . 14 class (𝑎↑((𝑚 − 1) / 2))
45		caddc 11027	. . . . . . . . . . . . . 14 class +
46	44, 12, 45	co 7356	. . . . . . . . . . . . 13 class ((𝑎↑((𝑚 − 1) / 2)) + 1)
47	46, 26, 33	co 7356	. . . . . . . . . . . 12 class (((𝑎↑((𝑚 − 1) / 2)) + 1) mod 𝑚)
48	47, 12, 40	co 7356	. . . . . . . . . . 11 class ((((𝑎↑((𝑚 − 1) / 2)) + 1) mod 𝑚) − 1)
49	29, 39, 48	cif 4477	. . . . . . . . . 10 class if(𝑚 = 2, if(2 ∥ 𝑎, 0, if((𝑎 mod 8) ∈ {1, 7}, 1, -1)), ((((𝑎↑((𝑚 − 1) / 2)) + 1) mod 𝑚) − 1))
50		cpc 16762	. . . . . . . . . . 11 class pCnt
51	26, 5, 50	co 7356	. . . . . . . . . 10 class (𝑚 pCnt 𝑛)
52	49, 51, 10	co 7356	. . . . . . . . 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 4477	. . . . . . . 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 5177	. . . . . . 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 13922	. . . . . 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 6490	. . . . 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 7356	. . . 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 4477	. . 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 7358	. 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 1541	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  27266