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 27339
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 27338 . 2 class /L
2 va . . 3 setvar 𝑎
3 vn . . 3 setvar 𝑛
4 cz 12613 . . 3 class
53cv 1539 . . . . 5 class 𝑛
6 cc0 11155 . . . . 5 class 0
75, 6wceq 1540 . . . 4 wff 𝑛 = 0
82cv 1539 . . . . . . 7 class 𝑎
9 c2 12321 . . . . . . 7 class 2
10 cexp 14102 . . . . . . 7 class
118, 9, 10co 7431 . . . . . 6 class (𝑎↑2)
12 c1 11156 . . . . . 6 class 1
1311, 12wceq 1540 . . . . 5 wff (𝑎↑2) = 1
1413, 12, 6cif 4525 . . . 4 class if((𝑎↑2) = 1, 1, 0)
15 clt 11295 . . . . . . . 8 class <
165, 6, 15wbr 5143 . . . . . . 7 wff 𝑛 < 0
178, 6, 15wbr 5143 . . . . . . 7 wff 𝑎 < 0
1816, 17wa 395 . . . . . 6 wff (𝑛 < 0 ∧ 𝑎 < 0)
1912cneg 11493 . . . . . 6 class -1
2018, 19, 12cif 4525 . . . . 5 class if((𝑛 < 0 ∧ 𝑎 < 0), -1, 1)
21 cabs 15273 . . . . . . 7 class abs
225, 21cfv 6561 . . . . . 6 class (abs‘𝑛)
23 cmul 11160 . . . . . . 7 class ·
24 vm . . . . . . . 8 setvar 𝑚
25 cn 12266 . . . . . . . 8 class
2624cv 1539 . . . . . . . . . 10 class 𝑚
27 cprime 16708 . . . . . . . . . 10 class
2826, 27wcel 2108 . . . . . . . . 9 wff 𝑚 ∈ ℙ
2926, 9wceq 1540 . . . . . . . . . . 11 wff 𝑚 = 2
30 cdvds 16290 . . . . . . . . . . . . 13 class
319, 8, 30wbr 5143 . . . . . . . . . . . 12 wff 2 ∥ 𝑎
32 c8 12327 . . . . . . . . . . . . . . 15 class 8
33 cmo 13909 . . . . . . . . . . . . . . 15 class mod
348, 32, 33co 7431 . . . . . . . . . . . . . 14 class (𝑎 mod 8)
35 c7 12326 . . . . . . . . . . . . . . 15 class 7
3612, 35cpr 4628 . . . . . . . . . . . . . 14 class {1, 7}
3734, 36wcel 2108 . . . . . . . . . . . . 13 wff (𝑎 mod 8) ∈ {1, 7}
3837, 12, 19cif 4525 . . . . . . . . . . . 12 class if((𝑎 mod 8) ∈ {1, 7}, 1, -1)
3931, 6, 38cif 4525 . . . . . . . . . . 11 class if(2 ∥ 𝑎, 0, if((𝑎 mod 8) ∈ {1, 7}, 1, -1))
40 cmin 11492 . . . . . . . . . . . . . . . . 17 class
4126, 12, 40co 7431 . . . . . . . . . . . . . . . 16 class (𝑚 − 1)
42 cdiv 11920 . . . . . . . . . . . . . . . 16 class /
4341, 9, 42co 7431 . . . . . . . . . . . . . . 15 class ((𝑚 − 1) / 2)
448, 43, 10co 7431 . . . . . . . . . . . . . 14 class (𝑎↑((𝑚 − 1) / 2))
45 caddc 11158 . . . . . . . . . . . . . 14 class +
4644, 12, 45co 7431 . . . . . . . . . . . . 13 class ((𝑎↑((𝑚 − 1) / 2)) + 1)
4746, 26, 33co 7431 . . . . . . . . . . . 12 class (((𝑎↑((𝑚 − 1) / 2)) + 1) mod 𝑚)
4847, 12, 40co 7431 . . . . . . . . . . 11 class ((((𝑎↑((𝑚 − 1) / 2)) + 1) mod 𝑚) − 1)
4929, 39, 48cif 4525 . . . . . . . . . 10 class if(𝑚 = 2, if(2 ∥ 𝑎, 0, if((𝑎 mod 8) ∈ {1, 7}, 1, -1)), ((((𝑎↑((𝑚 − 1) / 2)) + 1) mod 𝑚) − 1))
50 cpc 16874 . . . . . . . . . . 11 class pCnt
5126, 5, 50co 7431 . . . . . . . . . 10 class (𝑚 pCnt 𝑛)
5249, 51, 10co 7431 . . . . . . . . 9 class (if(𝑚 = 2, if(2 ∥ 𝑎, 0, if((𝑎 mod 8) ∈ {1, 7}, 1, -1)), ((((𝑎↑((𝑚 − 1) / 2)) + 1) mod 𝑚) − 1))↑(𝑚 pCnt 𝑛))
5328, 52, 12cif 4525 . . . . . . . 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 5225 . . . . . . 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 14042 . . . . . 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 6561 . . . . 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 7431 . . . 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 4525 . . 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, 58cmpo 7433 . 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 1540 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  27345
  Copyright terms: Public domain W3C validator