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 26643
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 26642 . 2 class /L
2 va . . 3 setvar 𝑎
3 vn . . 3 setvar 𝑛
4 cz 12499 . . 3 class
53cv 1540 . . . . 5 class 𝑛
6 cc0 11051 . . . . 5 class 0
75, 6wceq 1541 . . . 4 wff 𝑛 = 0
82cv 1540 . . . . . . 7 class 𝑎
9 c2 12208 . . . . . . 7 class 2
10 cexp 13967 . . . . . . 7 class
118, 9, 10co 7357 . . . . . 6 class (𝑎↑2)
12 c1 11052 . . . . . 6 class 1
1311, 12wceq 1541 . . . . 5 wff (𝑎↑2) = 1
1413, 12, 6cif 4486 . . . 4 class if((𝑎↑2) = 1, 1, 0)
15 clt 11189 . . . . . . . 8 class <
165, 6, 15wbr 5105 . . . . . . 7 wff 𝑛 < 0
178, 6, 15wbr 5105 . . . . . . 7 wff 𝑎 < 0
1816, 17wa 396 . . . . . 6 wff (𝑛 < 0 ∧ 𝑎 < 0)
1912cneg 11386 . . . . . 6 class -1
2018, 19, 12cif 4486 . . . . 5 class if((𝑛 < 0 ∧ 𝑎 < 0), -1, 1)
21 cabs 15119 . . . . . . 7 class abs
225, 21cfv 6496 . . . . . 6 class (abs‘𝑛)
23 cmul 11056 . . . . . . 7 class ·
24 vm . . . . . . . 8 setvar 𝑚
25 cn 12153 . . . . . . . 8 class
2624cv 1540 . . . . . . . . . 10 class 𝑚
27 cprime 16547 . . . . . . . . . 10 class
2826, 27wcel 2106 . . . . . . . . 9 wff 𝑚 ∈ ℙ
2926, 9wceq 1541 . . . . . . . . . . 11 wff 𝑚 = 2
30 cdvds 16136 . . . . . . . . . . . . 13 class
319, 8, 30wbr 5105 . . . . . . . . . . . 12 wff 2 ∥ 𝑎
32 c8 12214 . . . . . . . . . . . . . . 15 class 8
33 cmo 13774 . . . . . . . . . . . . . . 15 class mod
348, 32, 33co 7357 . . . . . . . . . . . . . 14 class (𝑎 mod 8)
35 c7 12213 . . . . . . . . . . . . . . 15 class 7
3612, 35cpr 4588 . . . . . . . . . . . . . 14 class {1, 7}
3734, 36wcel 2106 . . . . . . . . . . . . 13 wff (𝑎 mod 8) ∈ {1, 7}
3837, 12, 19cif 4486 . . . . . . . . . . . 12 class if((𝑎 mod 8) ∈ {1, 7}, 1, -1)
3931, 6, 38cif 4486 . . . . . . . . . . 11 class if(2 ∥ 𝑎, 0, if((𝑎 mod 8) ∈ {1, 7}, 1, -1))
40 cmin 11385 . . . . . . . . . . . . . . . . 17 class
4126, 12, 40co 7357 . . . . . . . . . . . . . . . 16 class (𝑚 − 1)
42 cdiv 11812 . . . . . . . . . . . . . . . 16 class /
4341, 9, 42co 7357 . . . . . . . . . . . . . . 15 class ((𝑚 − 1) / 2)
448, 43, 10co 7357 . . . . . . . . . . . . . 14 class (𝑎↑((𝑚 − 1) / 2))
45 caddc 11054 . . . . . . . . . . . . . 14 class +
4644, 12, 45co 7357 . . . . . . . . . . . . 13 class ((𝑎↑((𝑚 − 1) / 2)) + 1)
4746, 26, 33co 7357 . . . . . . . . . . . 12 class (((𝑎↑((𝑚 − 1) / 2)) + 1) mod 𝑚)
4847, 12, 40co 7357 . . . . . . . . . . 11 class ((((𝑎↑((𝑚 − 1) / 2)) + 1) mod 𝑚) − 1)
4929, 39, 48cif 4486 . . . . . . . . . 10 class if(𝑚 = 2, if(2 ∥ 𝑎, 0, if((𝑎 mod 8) ∈ {1, 7}, 1, -1)), ((((𝑎↑((𝑚 − 1) / 2)) + 1) mod 𝑚) − 1))
50 cpc 16708 . . . . . . . . . . 11 class pCnt
5126, 5, 50co 7357 . . . . . . . . . 10 class (𝑚 pCnt 𝑛)
5249, 51, 10co 7357 . . . . . . . . 9 class (if(𝑚 = 2, if(2 ∥ 𝑎, 0, if((𝑎 mod 8) ∈ {1, 7}, 1, -1)), ((((𝑎↑((𝑚 − 1) / 2)) + 1) mod 𝑚) − 1))↑(𝑚 pCnt 𝑛))
5328, 52, 12cif 4486 . . . . . . . 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 5188 . . . . . . 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 13906 . . . . . 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 6496 . . . . 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 7357 . . . 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 4486 . . 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 7359 . 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 1541 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  26649
  Copyright terms: Public domain W3C validator