# 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}=\left({a}\in ℤ,{n}\in ℤ⟼if\left({n}=0,if\left({{a}}^{2}=1,1,0\right),if\left(\left({n}<0\wedge {a}<0\right),-1,1\right)seq1\left(×,\left({m}\in ℕ⟼if\left({m}\in ℙ,{if\left({m}=2,if\left(2\parallel {a},0,if\left({a}\mathrm{mod}8\in \left\{1,7\right\},1,-1\right)\right),\left(\left({{a}}^{\frac{{m}-1}{2}}+1\right)\mathrm{mod}{m}\right)-1\right)}^{{m}\mathrm{pCnt}{n}},1\right)\right)\right)\left(\left|{n}\right|\right)\right)\right)$

### 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\left({{a}}^{2}=1,1,0\right)$
14 clt ${class}<$
15 4 5 14 wbr ${wff}{n}<0$
16 7 5 14 wbr ${wff}{a}<0$
17 15 16 wa ${wff}\left({n}<0\wedge {a}<0\right)$
18 11 cneg ${class}-1$
19 17 18 11 cif ${class}if\left(\left({n}<0\wedge {a}<0\right),-1,1\right)$
20 cmul ${class}×$
21 vm ${setvar}{m}$
22 cn ${class}ℕ$
23 21 cv ${setvar}{m}$
24 cprime ${class}ℙ$
25 23 24 wcel ${wff}{m}\in ℙ$
26 23 9 wceq ${wff}{m}=2$
27 cdvds ${class}\parallel$
28 9 7 27 wbr ${wff}2\parallel {a}$
29 cmo ${class}\mathrm{mod}$
30 c8 ${class}8$
31 7 30 29 co ${class}\left({a}\mathrm{mod}8\right)$
32 c7 ${class}7$
33 11 32 cpr ${class}\left\{1,7\right\}$
34 31 33 wcel ${wff}{a}\mathrm{mod}8\in \left\{1,7\right\}$
35 34 11 18 cif ${class}if\left({a}\mathrm{mod}8\in \left\{1,7\right\},1,-1\right)$
36 28 5 35 cif ${class}if\left(2\parallel {a},0,if\left({a}\mathrm{mod}8\in \left\{1,7\right\},1,-1\right)\right)$
37 cmin ${class}-$
38 23 11 37 co ${class}\left({m}-1\right)$
39 cdiv ${class}÷$
40 38 9 39 co ${class}\left(\frac{{m}-1}{2}\right)$
41 7 40 8 co ${class}{{a}}^{\frac{{m}-1}{2}}$
42 caddc ${class}+$
43 41 11 42 co ${class}\left({{a}}^{\frac{{m}-1}{2}}+1\right)$
44 43 23 29 co ${class}\left(\left({{a}}^{\frac{{m}-1}{2}}+1\right)\mathrm{mod}{m}\right)$
45 44 11 37 co ${class}\left(\left(\left({{a}}^{\frac{{m}-1}{2}}+1\right)\mathrm{mod}{m}\right)-1\right)$
46 26 36 45 cif ${class}if\left({m}=2,if\left(2\parallel {a},0,if\left({a}\mathrm{mod}8\in \left\{1,7\right\},1,-1\right)\right),\left(\left({{a}}^{\frac{{m}-1}{2}}+1\right)\mathrm{mod}{m}\right)-1\right)$
47 cpc ${class}\mathrm{pCnt}$
48 23 4 47 co ${class}\left({m}\mathrm{pCnt}{n}\right)$
49 46 48 8 co ${class}{if\left({m}=2,if\left(2\parallel {a},0,if\left({a}\mathrm{mod}8\in \left\{1,7\right\},1,-1\right)\right),\left(\left({{a}}^{\frac{{m}-1}{2}}+1\right)\mathrm{mod}{m}\right)-1\right)}^{{m}\mathrm{pCnt}{n}}$
50 25 49 11 cif ${class}if\left({m}\in ℙ,{if\left({m}=2,if\left(2\parallel {a},0,if\left({a}\mathrm{mod}8\in \left\{1,7\right\},1,-1\right)\right),\left(\left({{a}}^{\frac{{m}-1}{2}}+1\right)\mathrm{mod}{m}\right)-1\right)}^{{m}\mathrm{pCnt}{n}},1\right)$
51 21 22 50 cmpt ${class}\left({m}\in ℕ⟼if\left({m}\in ℙ,{if\left({m}=2,if\left(2\parallel {a},0,if\left({a}\mathrm{mod}8\in \left\{1,7\right\},1,-1\right)\right),\left(\left({{a}}^{\frac{{m}-1}{2}}+1\right)\mathrm{mod}{m}\right)-1\right)}^{{m}\mathrm{pCnt}{n}},1\right)\right)$
52 20 51 11 cseq ${class}seq1\left(×,\left({m}\in ℕ⟼if\left({m}\in ℙ,{if\left({m}=2,if\left(2\parallel {a},0,if\left({a}\mathrm{mod}8\in \left\{1,7\right\},1,-1\right)\right),\left(\left({{a}}^{\frac{{m}-1}{2}}+1\right)\mathrm{mod}{m}\right)-1\right)}^{{m}\mathrm{pCnt}{n}},1\right)\right)\right)$
53 cabs ${class}\mathrm{abs}$
54 4 53 cfv ${class}\left|{n}\right|$
55 54 52 cfv ${class}seq1\left(×,\left({m}\in ℕ⟼if\left({m}\in ℙ,{if\left({m}=2,if\left(2\parallel {a},0,if\left({a}\mathrm{mod}8\in \left\{1,7\right\},1,-1\right)\right),\left(\left({{a}}^{\frac{{m}-1}{2}}+1\right)\mathrm{mod}{m}\right)-1\right)}^{{m}\mathrm{pCnt}{n}},1\right)\right)\right)\left(\left|{n}\right|\right)$
56 19 55 20 co ${class}if\left(\left({n}<0\wedge {a}<0\right),-1,1\right)seq1\left(×,\left({m}\in ℕ⟼if\left({m}\in ℙ,{if\left({m}=2,if\left(2\parallel {a},0,if\left({a}\mathrm{mod}8\in \left\{1,7\right\},1,-1\right)\right),\left(\left({{a}}^{\frac{{m}-1}{2}}+1\right)\mathrm{mod}{m}\right)-1\right)}^{{m}\mathrm{pCnt}{n}},1\right)\right)\right)\left(\left|{n}\right|\right)$
57 6 13 56 cif ${class}if\left({n}=0,if\left({{a}}^{2}=1,1,0\right),if\left(\left({n}<0\wedge {a}<0\right),-1,1\right)seq1\left(×,\left({m}\in ℕ⟼if\left({m}\in ℙ,{if\left({m}=2,if\left(2\parallel {a},0,if\left({a}\mathrm{mod}8\in \left\{1,7\right\},1,-1\right)\right),\left(\left({{a}}^{\frac{{m}-1}{2}}+1\right)\mathrm{mod}{m}\right)-1\right)}^{{m}\mathrm{pCnt}{n}},1\right)\right)\right)\left(\left|{n}\right|\right)\right)$
58 1 3 2 2 57 cmpo ${class}\left({a}\in ℤ,{n}\in ℤ⟼if\left({n}=0,if\left({{a}}^{2}=1,1,0\right),if\left(\left({n}<0\wedge {a}<0\right),-1,1\right)seq1\left(×,\left({m}\in ℕ⟼if\left({m}\in ℙ,{if\left({m}=2,if\left(2\parallel {a},0,if\left({a}\mathrm{mod}8\in \left\{1,7\right\},1,-1\right)\right),\left(\left({{a}}^{\frac{{m}-1}{2}}+1\right)\mathrm{mod}{m}\right)-1\right)}^{{m}\mathrm{pCnt}{n}},1\right)\right)\right)\left(\left|{n}\right|\right)\right)\right)$
59 0 58 wceq ${wff}{/}_{L}=\left({a}\in ℤ,{n}\in ℤ⟼if\left({n}=0,if\left({{a}}^{2}=1,1,0\right),if\left(\left({n}<0\wedge {a}<0\right),-1,1\right)seq1\left(×,\left({m}\in ℕ⟼if\left({m}\in ℙ,{if\left({m}=2,if\left(2\parallel {a},0,if\left({a}\mathrm{mod}8\in \left\{1,7\right\},1,-1\right)\right),\left(\left({{a}}^{\frac{{m}-1}{2}}+1\right)\mathrm{mod}{m}\right)-1\right)}^{{m}\mathrm{pCnt}{n}},1\right)\right)\right)\left(\left|{n}\right|\right)\right)\right)$