MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  df-lgs Structured version   Visualization version   GIF version

Definition df-lgs 25241
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
StepHypRef Expression
1 clgs 25240 . 2 class /L
2 va . . 3 setvar 𝑎
3 vn . . 3 setvar 𝑛
4 cz 11579 . . 3 class
53cv 1630 . . . . 5 class 𝑛
6 cc0 10138 . . . . 5 class 0
75, 6wceq 1631 . . . 4 wff 𝑛 = 0
82cv 1630 . . . . . . 7 class 𝑎
9 c2 11272 . . . . . . 7 class 2
10 cexp 13067 . . . . . . 7 class
118, 9, 10co 6793 . . . . . 6 class (𝑎↑2)
12 c1 10139 . . . . . 6 class 1
1311, 12wceq 1631 . . . . 5 wff (𝑎↑2) = 1
1413, 12, 6cif 4225 . . . 4 class if((𝑎↑2) = 1, 1, 0)
15 clt 10276 . . . . . . . 8 class <
165, 6, 15wbr 4786 . . . . . . 7 wff 𝑛 < 0
178, 6, 15wbr 4786 . . . . . . 7 wff 𝑎 < 0
1816, 17wa 382 . . . . . 6 wff (𝑛 < 0 ∧ 𝑎 < 0)
1912cneg 10469 . . . . . 6 class -1
2018, 19, 12cif 4225 . . . . 5 class if((𝑛 < 0 ∧ 𝑎 < 0), -1, 1)
21 cabs 14182 . . . . . . 7 class abs
225, 21cfv 6031 . . . . . 6 class (abs‘𝑛)
23 cmul 10143 . . . . . . 7 class ·
24 vm . . . . . . . 8 setvar 𝑚
25 cn 11222 . . . . . . . 8 class
2624cv 1630 . . . . . . . . . 10 class 𝑚
27 cprime 15592 . . . . . . . . . 10 class
2826, 27wcel 2145 . . . . . . . . 9 wff 𝑚 ∈ ℙ
2926, 9wceq 1631 . . . . . . . . . . 11 wff 𝑚 = 2
30 cdvds 15189 . . . . . . . . . . . . 13 class
319, 8, 30wbr 4786 . . . . . . . . . . . 12 wff 2 ∥ 𝑎
32 c8 11278 . . . . . . . . . . . . . . 15 class 8
33 cmo 12876 . . . . . . . . . . . . . . 15 class mod
348, 32, 33co 6793 . . . . . . . . . . . . . 14 class (𝑎 mod 8)
35 c7 11277 . . . . . . . . . . . . . . 15 class 7
3612, 35cpr 4318 . . . . . . . . . . . . . 14 class {1, 7}
3734, 36wcel 2145 . . . . . . . . . . . . 13 wff (𝑎 mod 8) ∈ {1, 7}
3837, 12, 19cif 4225 . . . . . . . . . . . 12 class if((𝑎 mod 8) ∈ {1, 7}, 1, -1)
3931, 6, 38cif 4225 . . . . . . . . . . 11 class if(2 ∥ 𝑎, 0, if((𝑎 mod 8) ∈ {1, 7}, 1, -1))
40 cmin 10468 . . . . . . . . . . . . . . . . 17 class
4126, 12, 40co 6793 . . . . . . . . . . . . . . . 16 class (𝑚 − 1)
42 cdiv 10886 . . . . . . . . . . . . . . . 16 class /
4341, 9, 42co 6793 . . . . . . . . . . . . . . 15 class ((𝑚 − 1) / 2)
448, 43, 10co 6793 . . . . . . . . . . . . . 14 class (𝑎↑((𝑚 − 1) / 2))
45 caddc 10141 . . . . . . . . . . . . . 14 class +
4644, 12, 45co 6793 . . . . . . . . . . . . 13 class ((𝑎↑((𝑚 − 1) / 2)) + 1)
4746, 26, 33co 6793 . . . . . . . . . . . 12 class (((𝑎↑((𝑚 − 1) / 2)) + 1) mod 𝑚)
4847, 12, 40co 6793 . . . . . . . . . . 11 class ((((𝑎↑((𝑚 − 1) / 2)) + 1) mod 𝑚) − 1)
4929, 39, 48cif 4225 . . . . . . . . . 10 class if(𝑚 = 2, if(2 ∥ 𝑎, 0, if((𝑎 mod 8) ∈ {1, 7}, 1, -1)), ((((𝑎↑((𝑚 − 1) / 2)) + 1) mod 𝑚) − 1))
50 cpc 15748 . . . . . . . . . . 11 class pCnt
5126, 5, 50co 6793 . . . . . . . . . 10 class (𝑚 pCnt 𝑛)
5249, 51, 10co 6793 . . . . . . . . 9 class (if(𝑚 = 2, if(2 ∥ 𝑎, 0, if((𝑎 mod 8) ∈ {1, 7}, 1, -1)), ((((𝑎↑((𝑚 − 1) / 2)) + 1) mod 𝑚) − 1))↑(𝑚 pCnt 𝑛))
5328, 52, 12cif 4225 . . . . . . . 8 class if(𝑚 ∈ ℙ, (if(𝑚 = 2, if(2 ∥ 𝑎, 0, if((𝑎 mod 8) ∈ {1, 7}, 1, -1)), ((((𝑎↑((𝑚 − 1) / 2)) + 1) mod 𝑚) − 1))↑(𝑚 pCnt 𝑛)), 1)
5424, 25, 53cmpt 4863 . . . . . . 7 class (𝑚 ∈ ℕ ↦ if(𝑚 ∈ ℙ, (if(𝑚 = 2, if(2 ∥ 𝑎, 0, if((𝑎 mod 8) ∈ {1, 7}, 1, -1)), ((((𝑎↑((𝑚 − 1) / 2)) + 1) mod 𝑚) − 1))↑(𝑚 pCnt 𝑛)), 1))
5523, 54, 12cseq 13008 . . . . . 6 class seq1( · , (𝑚 ∈ ℕ ↦ if(𝑚 ∈ ℙ, (if(𝑚 = 2, if(2 ∥ 𝑎, 0, if((𝑎 mod 8) ∈ {1, 7}, 1, -1)), ((((𝑎↑((𝑚 − 1) / 2)) + 1) mod 𝑚) − 1))↑(𝑚 pCnt 𝑛)), 1)))
5622, 55cfv 6031 . . . . 5 class (seq1( · , (𝑚 ∈ ℕ ↦ if(𝑚 ∈ ℙ, (if(𝑚 = 2, if(2 ∥ 𝑎, 0, if((𝑎 mod 8) ∈ {1, 7}, 1, -1)), ((((𝑎↑((𝑚 − 1) / 2)) + 1) mod 𝑚) − 1))↑(𝑚 pCnt 𝑛)), 1)))‘(abs‘𝑛))
5720, 56, 23co 6793 . . . 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‘𝑛)))
587, 14, 57cif 4225 . . 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‘𝑛))))
592, 3, 4, 4, 58cmpt2 6795 . 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‘𝑛)))))
601, 59wceq 1631 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‘𝑛)))))
Colors of variables: wff setvar class
This definition is referenced by:  lgsval  25247
  Copyright terms: Public domain W3C validator