ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  df-lgs GIF version

Definition df-lgs 14066
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 14065 . 2 class /L
2 va . . 3 setvar 𝑎
3 vn . . 3 setvar 𝑛
4 cz 9242 . . 3 class
53cv 1352 . . . . 5 class 𝑛
6 cc0 7802 . . . . 5 class 0
75, 6wceq 1353 . . . 4 wff 𝑛 = 0
82cv 1352 . . . . . . 7 class 𝑎
9 c2 8959 . . . . . . 7 class 2
10 cexp 10505 . . . . . . 7 class
118, 9, 10co 5869 . . . . . 6 class (𝑎↑2)
12 c1 7803 . . . . . 6 class 1
1311, 12wceq 1353 . . . . 5 wff (𝑎↑2) = 1
1413, 12, 6cif 3534 . . . 4 class if((𝑎↑2) = 1, 1, 0)
15 clt 7982 . . . . . . . 8 class <
165, 6, 15wbr 4000 . . . . . . 7 wff 𝑛 < 0
178, 6, 15wbr 4000 . . . . . . 7 wff 𝑎 < 0
1816, 17wa 104 . . . . . 6 wff (𝑛 < 0 ∧ 𝑎 < 0)
1912cneg 8119 . . . . . 6 class -1
2018, 19, 12cif 3534 . . . . 5 class if((𝑛 < 0 ∧ 𝑎 < 0), -1, 1)
21 cabs 10990 . . . . . . 7 class abs
225, 21cfv 5212 . . . . . 6 class (abs‘𝑛)
23 cmul 7807 . . . . . . 7 class ·
24 vm . . . . . . . 8 setvar 𝑚
25 cn 8908 . . . . . . . 8 class
2624cv 1352 . . . . . . . . . 10 class 𝑚
27 cprime 12090 . . . . . . . . . 10 class
2826, 27wcel 2148 . . . . . . . . 9 wff 𝑚 ∈ ℙ
2926, 9wceq 1353 . . . . . . . . . . 11 wff 𝑚 = 2
30 cdvds 11778 . . . . . . . . . . . . 13 class
319, 8, 30wbr 4000 . . . . . . . . . . . 12 wff 2 ∥ 𝑎
32 c8 8965 . . . . . . . . . . . . . . 15 class 8
33 cmo 10308 . . . . . . . . . . . . . . 15 class mod
348, 32, 33co 5869 . . . . . . . . . . . . . 14 class (𝑎 mod 8)
35 c7 8964 . . . . . . . . . . . . . . 15 class 7
3612, 35cpr 3592 . . . . . . . . . . . . . 14 class {1, 7}
3734, 36wcel 2148 . . . . . . . . . . . . 13 wff (𝑎 mod 8) ∈ {1, 7}
3837, 12, 19cif 3534 . . . . . . . . . . . 12 class if((𝑎 mod 8) ∈ {1, 7}, 1, -1)
3931, 6, 38cif 3534 . . . . . . . . . . 11 class if(2 ∥ 𝑎, 0, if((𝑎 mod 8) ∈ {1, 7}, 1, -1))
40 cmin 8118 . . . . . . . . . . . . . . . . 17 class
4126, 12, 40co 5869 . . . . . . . . . . . . . . . 16 class (𝑚 − 1)
42 cdiv 8618 . . . . . . . . . . . . . . . 16 class /
4341, 9, 42co 5869 . . . . . . . . . . . . . . 15 class ((𝑚 − 1) / 2)
448, 43, 10co 5869 . . . . . . . . . . . . . 14 class (𝑎↑((𝑚 − 1) / 2))
45 caddc 7805 . . . . . . . . . . . . . 14 class +
4644, 12, 45co 5869 . . . . . . . . . . . . 13 class ((𝑎↑((𝑚 − 1) / 2)) + 1)
4746, 26, 33co 5869 . . . . . . . . . . . 12 class (((𝑎↑((𝑚 − 1) / 2)) + 1) mod 𝑚)
4847, 12, 40co 5869 . . . . . . . . . . 11 class ((((𝑎↑((𝑚 − 1) / 2)) + 1) mod 𝑚) − 1)
4929, 39, 48cif 3534 . . . . . . . . . 10 class if(𝑚 = 2, if(2 ∥ 𝑎, 0, if((𝑎 mod 8) ∈ {1, 7}, 1, -1)), ((((𝑎↑((𝑚 − 1) / 2)) + 1) mod 𝑚) − 1))
50 cpc 12267 . . . . . . . . . . 11 class pCnt
5126, 5, 50co 5869 . . . . . . . . . 10 class (𝑚 pCnt 𝑛)
5249, 51, 10co 5869 . . . . . . . . 9 class (if(𝑚 = 2, if(2 ∥ 𝑎, 0, if((𝑎 mod 8) ∈ {1, 7}, 1, -1)), ((((𝑎↑((𝑚 − 1) / 2)) + 1) mod 𝑚) − 1))↑(𝑚 pCnt 𝑛))
5328, 52, 12cif 3534 . . . . . . . 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 4061 . . . . . . 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 10431 . . . . . 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 5212 . . . . 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 5869 . . . 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 3534 . . 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 5871 . 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 1353 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 set class
This definition is referenced by:  lgsval  14072
  Copyright terms: Public domain W3C validator