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 11584 . . 3 class
53cv 1630 . . . . 5 class 𝑛
6 cc0 10142 . . . . 5 class 0
75, 6wceq 1631 . . . 4 wff 𝑛 = 0
82cv 1630 . . . . . . 7 class 𝑎
9 c2 11276 . . . . . . 7 class 2
10 cexp 13067 . . . . . . 7 class
118, 9, 10co 6796 . . . . . 6 class (𝑎↑2)
12 c1 10143 . . . . . 6 class 1
1311, 12wceq 1631 . . . . 5 wff (𝑎↑2) = 1
1413, 12, 6cif 4226 . . . 4 class if((𝑎↑2) = 1, 1, 0)
15 clt 10280 . . . . . . . 8 class <
165, 6, 15wbr 4787 . . . . . . 7 wff 𝑛 < 0
178, 6, 15wbr 4787 . . . . . . 7 wff 𝑎 < 0
1816, 17wa 382 . . . . . 6 wff (𝑛 < 0 ∧ 𝑎 < 0)
1912cneg 10473 . . . . . 6 class -1
2018, 19, 12cif 4226 . . . . 5 class if((𝑛 < 0 ∧ 𝑎 < 0), -1, 1)
21 cabs 14182 . . . . . . 7 class abs
225, 21cfv 6030 . . . . . 6 class (abs‘𝑛)
23 cmul 10147 . . . . . . 7 class ·
24 vm . . . . . . . 8 setvar 𝑚
25 cn 11226 . . . . . . . 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 4787 . . . . . . . . . . . 12 wff 2 ∥ 𝑎
32 c8 11282 . . . . . . . . . . . . . . 15 class 8
33 cmo 12876 . . . . . . . . . . . . . . 15 class mod
348, 32, 33co 6796 . . . . . . . . . . . . . 14 class (𝑎 mod 8)
35 c7 11281 . . . . . . . . . . . . . . 15 class 7
3612, 35cpr 4319 . . . . . . . . . . . . . 14 class {1, 7}
3734, 36wcel 2145 . . . . . . . . . . . . 13 wff (𝑎 mod 8) ∈ {1, 7}
3837, 12, 19cif 4226 . . . . . . . . . . . 12 class if((𝑎 mod 8) ∈ {1, 7}, 1, -1)
3931, 6, 38cif 4226 . . . . . . . . . . 11 class if(2 ∥ 𝑎, 0, if((𝑎 mod 8) ∈ {1, 7}, 1, -1))
40 cmin 10472 . . . . . . . . . . . . . . . . 17 class
4126, 12, 40co 6796 . . . . . . . . . . . . . . . 16 class (𝑚 − 1)
42 cdiv 10890 . . . . . . . . . . . . . . . 16 class /
4341, 9, 42co 6796 . . . . . . . . . . . . . . 15 class ((𝑚 − 1) / 2)
448, 43, 10co 6796 . . . . . . . . . . . . . 14 class (𝑎↑((𝑚 − 1) / 2))
45 caddc 10145 . . . . . . . . . . . . . 14 class +
4644, 12, 45co 6796 . . . . . . . . . . . . 13 class ((𝑎↑((𝑚 − 1) / 2)) + 1)
4746, 26, 33co 6796 . . . . . . . . . . . 12 class (((𝑎↑((𝑚 − 1) / 2)) + 1) mod 𝑚)
4847, 12, 40co 6796 . . . . . . . . . . 11 class ((((𝑎↑((𝑚 − 1) / 2)) + 1) mod 𝑚) − 1)
4929, 39, 48cif 4226 . . . . . . . . . 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 6796 . . . . . . . . . 10 class (𝑚 pCnt 𝑛)
5249, 51, 10co 6796 . . . . . . . . 9 class (if(𝑚 = 2, if(2 ∥ 𝑎, 0, if((𝑎 mod 8) ∈ {1, 7}, 1, -1)), ((((𝑎↑((𝑚 − 1) / 2)) + 1) mod 𝑚) − 1))↑(𝑚 pCnt 𝑛))
5328, 52, 12cif 4226 . . . . . . . 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 4864 . . . . . . 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 6030 . . . . 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 6796 . . . 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 4226 . . 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 6798 . 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