Metamath Proof Explorer

Definition df-lgs

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)

Ref Expression
Assertion df-lgs ⊢ / L = a ∈ ℤ , n ∈ ℤ ⟼ if n = 0 if a 2 = 1 1 0 if n < 0 ∧ a < 0 − 1 1 ⁢ seq 1 × m ∈ ℕ ⟼ if m ∈ ℙ if m = 2 if 2 ∥ a 0 if a mod 8 ∈ 1 7 1 − 1 a m − 1 2 + 1 mod m − 1 m pCnt n 1 ⁡ n

Detailed syntax breakdown

Step Hyp Ref Expression
0 clgs class / L
1 va setvar a
2 cz class ℤ
3 vn setvar n
4 3 cv setvar n
5 cc0 class 0
6 4 5 wceq wff n = 0
7 1 cv setvar a
8 cexp class ^
9 c2 class 2
10 7 9 8 co class a 2
11 c1 class 1
12 10 11 wceq wff a 2 = 1
13 12 11 5 cif class if a 2 = 1 1 0
14 clt class <
15 4 5 14 wbr wff n < 0
16 7 5 14 wbr wff a < 0
17 15 16 wa wff n < 0 ∧ a < 0
18 11 cneg class -1
19 17 18 11 cif class if n < 0 ∧ a < 0 − 1 1
20 cmul class ×
21 vm setvar m
22 cn class ℕ
23 21 cv setvar m
24 cprime class ℙ
25 23 24 wcel wff m ∈ ℙ
26 23 9 wceq wff m = 2
27 cdvds class ∥
28 9 7 27 wbr wff 2 ∥ a
29 cmo class mod
30 c8 class 8
31 7 30 29 co class a mod 8
32 c7 class 7
33 11 32 cpr class 1 7
34 31 33 wcel wff a mod 8 ∈ 1 7
35 34 11 18 cif class if a mod 8 ∈ 1 7 1 − 1
36 28 5 35 cif class if 2 ∥ a 0 if a mod 8 ∈ 1 7 1 − 1
37 cmin class −
38 23 11 37 co class m − 1
39 cdiv class ÷
40 38 9 39 co class m − 1 2
41 7 40 8 co class a m − 1 2
42 caddc class +
43 41 11 42 co class a m − 1 2 + 1
44 43 23 29 co class a m − 1 2 + 1 mod m
45 44 11 37 co class a m − 1 2 + 1 mod m − 1
46 26 36 45 cif class if m = 2 if 2 ∥ a 0 if a mod 8 ∈ 1 7 1 − 1 a m − 1 2 + 1 mod m − 1
47 cpc class pCnt
48 23 4 47 co class m pCnt n
49 46 48 8 co class if m = 2 if 2 ∥ a 0 if a mod 8 ∈ 1 7 1 − 1 a m − 1 2 + 1 mod m − 1 m pCnt n
50 25 49 11 cif class if m ∈ ℙ if m = 2 if 2 ∥ a 0 if a mod 8 ∈ 1 7 1 − 1 a m − 1 2 + 1 mod m − 1 m pCnt n 1
51 21 22 50 cmpt class m ∈ ℕ ⟼ if m ∈ ℙ if m = 2 if 2 ∥ a 0 if a mod 8 ∈ 1 7 1 − 1 a m − 1 2 + 1 mod m − 1 m pCnt n 1
52 20 51 11 cseq class seq 1 × m ∈ ℕ ⟼ if m ∈ ℙ if m = 2 if 2 ∥ a 0 if a mod 8 ∈ 1 7 1 − 1 a m − 1 2 + 1 mod m − 1 m pCnt n 1
53 cabs class abs
54 4 53 cfv class n
55 54 52 cfv class seq 1 × m ∈ ℕ ⟼ if m ∈ ℙ if m = 2 if 2 ∥ a 0 if a mod 8 ∈ 1 7 1 − 1 a m − 1 2 + 1 mod m − 1 m pCnt n 1 ⁡ n
56 19 55 20 co class if n < 0 ∧ a < 0 − 1 1 ⁢ seq 1 × m ∈ ℕ ⟼ if m ∈ ℙ if m = 2 if 2 ∥ a 0 if a mod 8 ∈ 1 7 1 − 1 a m − 1 2 + 1 mod m − 1 m pCnt n 1 ⁡ n
57 6 13 56 cif class if n = 0 if a 2 = 1 1 0 if n < 0 ∧ a < 0 − 1 1 ⁢ seq 1 × m ∈ ℕ ⟼ if m ∈ ℙ if m = 2 if 2 ∥ a 0 if a mod 8 ∈ 1 7 1 − 1 a m − 1 2 + 1 mod m − 1 m pCnt n 1 ⁡ n
58 1 3 2 2 57 cmpo class a ∈ ℤ , n ∈ ℤ ⟼ if n = 0 if a 2 = 1 1 0 if n < 0 ∧ a < 0 − 1 1 ⁢ seq 1 × m ∈ ℕ ⟼ if m ∈ ℙ if m = 2 if 2 ∥ a 0 if a mod 8 ∈ 1 7 1 − 1 a m − 1 2 + 1 mod m − 1 m pCnt n 1 ⁡ n
59 0 58 wceq wff / L = a ∈ ℤ , n ∈ ℤ ⟼ if n = 0 if a 2 = 1 1 0 if n < 0 ∧ a < 0 − 1 1 ⁢ seq 1 × m ∈ ℕ ⟼ if m ∈ ℙ if m = 2 if 2 ∥ a 0 if a mod 8 ∈ 1 7 1 − 1 a m − 1 2 + 1 mod m − 1 m pCnt n 1 ⁡ n