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∈ℤ⟼ifn=0ifa2=110ifn<0∧a<0−11⁢seq1×m∈ℕ⟼ifm∈ℙifm=2if2∥a0ifamod8∈171−1am−12+1modm−1mpCntn1⁡n

Detailed syntax breakdown

Step Hyp Ref Expression
0 clgs class/L
1 va setvara
2 cz classℤ
3 vn setvarn
4 3 cv setvarn
5 cc0 class0
6 4 5 wceq wffn=0
7 1 cv setvara
8 cexp class^
9 c2 class2
10 7 9 8 co classa2
11 c1 class1
12 10 11 wceq wffa2=1
13 12 11 5 cif classifa2=110
14 clt class<
15 4 5 14 wbr wffn<0
16 7 5 14 wbr wffa<0
17 15 16 wa wffn<0∧a<0
18 11 cneg class-1
19 17 18 11 cif classifn<0∧a<0−11
20 cmul class×
21 vm setvarm
22 cn classℕ
23 21 cv setvarm
24 cprime classℙ
25 23 24 wcel wffm∈ℙ
26 23 9 wceq wffm=2
27 cdvds class∥
28 9 7 27 wbr wff2∥a
29 cmo classmod
30 c8 class8
31 7 30 29 co classamod8
32 c7 class7
33 11 32 cpr class17
34 31 33 wcel wffamod8∈17
35 34 11 18 cif classifamod8∈171−1
36 28 5 35 cif classif2∥a0ifamod8∈171−1
37 cmin class−
38 23 11 37 co classm−1
39 cdiv class÷
40 38 9 39 co classm−12
41 7 40 8 co classam−12
42 caddc class+
43 41 11 42 co classam−12+1
44 43 23 29 co classam−12+1modm
45 44 11 37 co classam−12+1modm−1
46 26 36 45 cif classifm=2if2∥a0ifamod8∈171−1am−12+1modm−1
47 cpc classpCnt
48 23 4 47 co classmpCntn
49 46 48 8 co classifm=2if2∥a0ifamod8∈171−1am−12+1modm−1mpCntn
50 25 49 11 cif classifm∈ℙifm=2if2∥a0ifamod8∈171−1am−12+1modm−1mpCntn1
51 21 22 50 cmpt classm∈ℕ⟼ifm∈ℙifm=2if2∥a0ifamod8∈171−1am−12+1modm−1mpCntn1
52 20 51 11 cseq classseq1×m∈ℕ⟼ifm∈ℙifm=2if2∥a0ifamod8∈171−1am−12+1modm−1mpCntn1
53 cabs classabs
54 4 53 cfv classn
55 54 52 cfv classseq1×m∈ℕ⟼ifm∈ℙifm=2if2∥a0ifamod8∈171−1am−12+1modm−1mpCntn1⁡n
56 19 55 20 co classifn<0∧a<0−11⁢seq1×m∈ℕ⟼ifm∈ℙifm=2if2∥a0ifamod8∈171−1am−12+1modm−1mpCntn1⁡n
57 6 13 56 cif classifn=0ifa2=110ifn<0∧a<0−11⁢seq1×m∈ℕ⟼ifm∈ℙifm=2if2∥a0ifamod8∈171−1am−12+1modm−1mpCntn1⁡n
58 1 3 2 2 57 cmpo classa∈ℤ,n∈ℤ⟼ifn=0ifa2=110ifn<0∧a<0−11⁢seq1×m∈ℕ⟼ifm∈ℙifm=2if2∥a0ifamod8∈171−1am−12+1modm−1mpCntn1⁡n
59 0 58 wceq wff/L=a∈ℤ,n∈ℤ⟼ifn=0ifa2=110ifn<0∧a<0−11⁢seq1×m∈ℕ⟼ifm∈ℙifm=2if2∥a0ifamod8∈171−1am−12+1modm−1mpCntn1⁡n