Definition df-lgs

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)

	Ref	Expression
Assertion	df-lgs	⊢ /L = ( 𝑎 ∈ ℤ , 𝑛 ∈ ℤ ↦ if ( 𝑛 = 0 , if ( ( 𝑎 ↑ 2 ) = 1 , 1 , 0 ) , ( if ( ( 𝑛 < 0 ∧ 𝑎 < 0 ) , - 1 , 1 ) · ( seq 1 ( · , ( 𝑚 ∈ ℕ ↦ if ( 𝑚 ∈ ℙ , ( if ( 𝑚 = 2 , if ( 2 ∥ 𝑎 , 0 , if ( ( 𝑎 mod 8 ) ∈ { 1 , 7 } , 1 , - 1 ) ) , ( ( ( ( 𝑎 ↑ ( ( 𝑚 − 1 ) / 2 ) ) + 1 ) mod 𝑚 ) − 1 ) ) ↑ ( 𝑚 pCnt 𝑛 ) ) , 1 ) ) ) ‘ ( abs ‘ 𝑛 ) ) ) ) )

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		clgs	⊢ /L
1		va	⊢ 𝑎
2		cz	⊢ ℤ
3		vn	⊢ 𝑛
4	3	cv	⊢ 𝑛
5		cc0	⊢ 0
6	4 5	wceq	⊢ 𝑛 = 0
7	1	cv	⊢ 𝑎
8		cexp	⊢ ↑
9		c2	⊢ 2
10	7 9 8	co	⊢ ( 𝑎 ↑ 2 )
11		c1	⊢ 1
12	10 11	wceq	⊢ ( 𝑎 ↑ 2 ) = 1
13	12 11 5	cif	⊢ if ( ( 𝑎 ↑ 2 ) = 1 , 1 , 0 )
14		clt	⊢ <
15	4 5 14	wbr	⊢ 𝑛 < 0
16	7 5 14	wbr	⊢ 𝑎 < 0
17	15 16	wa	⊢ ( 𝑛 < 0 ∧ 𝑎 < 0 )
18	11	cneg	⊢ - 1
19	17 18 11	cif	⊢ if ( ( 𝑛 < 0 ∧ 𝑎 < 0 ) , - 1 , 1 )
20		cmul	⊢ ·
21		vm	⊢ 𝑚
22		cn	⊢ ℕ
23	21	cv	⊢ 𝑚
24		cprime	⊢ ℙ
25	23 24	wcel	⊢ 𝑚 ∈ ℙ
26	23 9	wceq	⊢ 𝑚 = 2
27		cdvds	⊢ ∥
28	9 7 27	wbr	⊢ 2 ∥ 𝑎
29		cmo	⊢ mod
30		c8	⊢ 8
31	7 30 29	co	⊢ ( 𝑎 mod 8 )
32		c7	⊢ 7
33	11 32	cpr	⊢ { 1 , 7 }
34	31 33	wcel	⊢ ( 𝑎 mod 8 ) ∈ { 1 , 7 }
35	34 11 18	cif	⊢ if ( ( 𝑎 mod 8 ) ∈ { 1 , 7 } , 1 , - 1 )
36	28 5 35	cif	⊢ if ( 2 ∥ 𝑎 , 0 , if ( ( 𝑎 mod 8 ) ∈ { 1 , 7 } , 1 , - 1 ) )
37		cmin	⊢ −
38	23 11 37	co	⊢ ( 𝑚 − 1 )
39		cdiv	⊢ /
40	38 9 39	co	⊢ ( ( 𝑚 − 1 ) / 2 )
41	7 40 8	co	⊢ ( 𝑎 ↑ ( ( 𝑚 − 1 ) / 2 ) )
42		caddc	⊢ +
43	41 11 42	co	⊢ ( ( 𝑎 ↑ ( ( 𝑚 − 1 ) / 2 ) ) + 1 )
44	43 23 29	co	⊢ ( ( ( 𝑎 ↑ ( ( 𝑚 − 1 ) / 2 ) ) + 1 ) mod 𝑚 )
45	44 11 37	co	⊢ ( ( ( ( 𝑎 ↑ ( ( 𝑚 − 1 ) / 2 ) ) + 1 ) mod 𝑚 ) − 1 )
46	26 36 45	cif	⊢ if ( 𝑚 = 2 , if ( 2 ∥ 𝑎 , 0 , if ( ( 𝑎 mod 8 ) ∈ { 1 , 7 } , 1 , - 1 ) ) , ( ( ( ( 𝑎 ↑ ( ( 𝑚 − 1 ) / 2 ) ) + 1 ) mod 𝑚 ) − 1 ) )
47		cpc	⊢ pCnt
48	23 4 47	co	⊢ ( 𝑚 pCnt 𝑛 )
49	46 48 8	co	⊢ ( if ( 𝑚 = 2 , if ( 2 ∥ 𝑎 , 0 , if ( ( 𝑎 mod 8 ) ∈ { 1 , 7 } , 1 , - 1 ) ) , ( ( ( ( 𝑎 ↑ ( ( 𝑚 − 1 ) / 2 ) ) + 1 ) mod 𝑚 ) − 1 ) ) ↑ ( 𝑚 pCnt 𝑛 ) )
50	25 49 11	cif	⊢ if ( 𝑚 ∈ ℙ , ( if ( 𝑚 = 2 , if ( 2 ∥ 𝑎 , 0 , if ( ( 𝑎 mod 8 ) ∈ { 1 , 7 } , 1 , - 1 ) ) , ( ( ( ( 𝑎 ↑ ( ( 𝑚 − 1 ) / 2 ) ) + 1 ) mod 𝑚 ) − 1 ) ) ↑ ( 𝑚 pCnt 𝑛 ) ) , 1 )
51	21 22 50	cmpt	⊢ ( 𝑚 ∈ ℕ ↦ if ( 𝑚 ∈ ℙ , ( if ( 𝑚 = 2 , if ( 2 ∥ 𝑎 , 0 , if ( ( 𝑎 mod 8 ) ∈ { 1 , 7 } , 1 , - 1 ) ) , ( ( ( ( 𝑎 ↑ ( ( 𝑚 − 1 ) / 2 ) ) + 1 ) mod 𝑚 ) − 1 ) ) ↑ ( 𝑚 pCnt 𝑛 ) ) , 1 ) )
52	20 51 11	cseq	⊢ seq 1 ( · , ( 𝑚 ∈ ℕ ↦ if ( 𝑚 ∈ ℙ , ( if ( 𝑚 = 2 , if ( 2 ∥ 𝑎 , 0 , if ( ( 𝑎 mod 8 ) ∈ { 1 , 7 } , 1 , - 1 ) ) , ( ( ( ( 𝑎 ↑ ( ( 𝑚 − 1 ) / 2 ) ) + 1 ) mod 𝑚 ) − 1 ) ) ↑ ( 𝑚 pCnt 𝑛 ) ) , 1 ) ) )
53		cabs	⊢ abs
54	4 53	cfv	⊢ ( abs ‘ 𝑛 )
55	54 52	cfv	⊢ ( seq 1 ( · , ( 𝑚 ∈ ℕ ↦ if ( 𝑚 ∈ ℙ , ( if ( 𝑚 = 2 , if ( 2 ∥ 𝑎 , 0 , if ( ( 𝑎 mod 8 ) ∈ { 1 , 7 } , 1 , - 1 ) ) , ( ( ( ( 𝑎 ↑ ( ( 𝑚 − 1 ) / 2 ) ) + 1 ) mod 𝑚 ) − 1 ) ) ↑ ( 𝑚 pCnt 𝑛 ) ) , 1 ) ) ) ‘ ( abs ‘ 𝑛 ) )
56	19 55 20	co	⊢ ( if ( ( 𝑛 < 0 ∧ 𝑎 < 0 ) , - 1 , 1 ) · ( seq 1 ( · , ( 𝑚 ∈ ℕ ↦ if ( 𝑚 ∈ ℙ , ( if ( 𝑚 = 2 , if ( 2 ∥ 𝑎 , 0 , if ( ( 𝑎 mod 8 ) ∈ { 1 , 7 } , 1 , - 1 ) ) , ( ( ( ( 𝑎 ↑ ( ( 𝑚 − 1 ) / 2 ) ) + 1 ) mod 𝑚 ) − 1 ) ) ↑ ( 𝑚 pCnt 𝑛 ) ) , 1 ) ) ) ‘ ( abs ‘ 𝑛 ) ) )
57	6 13 56	cif	⊢ if ( 𝑛 = 0 , if ( ( 𝑎 ↑ 2 ) = 1 , 1 , 0 ) , ( if ( ( 𝑛 < 0 ∧ 𝑎 < 0 ) , - 1 , 1 ) · ( seq 1 ( · , ( 𝑚 ∈ ℕ ↦ if ( 𝑚 ∈ ℙ , ( if ( 𝑚 = 2 , if ( 2 ∥ 𝑎 , 0 , if ( ( 𝑎 mod 8 ) ∈ { 1 , 7 } , 1 , - 1 ) ) , ( ( ( ( 𝑎 ↑ ( ( 𝑚 − 1 ) / 2 ) ) + 1 ) mod 𝑚 ) − 1 ) ) ↑ ( 𝑚 pCnt 𝑛 ) ) , 1 ) ) ) ‘ ( abs ‘ 𝑛 ) ) ) )
58	1 3 2 2 57	cmpo	⊢ ( 𝑎 ∈ ℤ , 𝑛 ∈ ℤ ↦ if ( 𝑛 = 0 , if ( ( 𝑎 ↑ 2 ) = 1 , 1 , 0 ) , ( if ( ( 𝑛 < 0 ∧ 𝑎 < 0 ) , - 1 , 1 ) · ( seq 1 ( · , ( 𝑚 ∈ ℕ ↦ if ( 𝑚 ∈ ℙ , ( if ( 𝑚 = 2 , if ( 2 ∥ 𝑎 , 0 , if ( ( 𝑎 mod 8 ) ∈ { 1 , 7 } , 1 , - 1 ) ) , ( ( ( ( 𝑎 ↑ ( ( 𝑚 − 1 ) / 2 ) ) + 1 ) mod 𝑚 ) − 1 ) ) ↑ ( 𝑚 pCnt 𝑛 ) ) , 1 ) ) ) ‘ ( abs ‘ 𝑛 ) ) ) ) )
59	0 58	wceq	⊢ /L = ( 𝑎 ∈ ℤ , 𝑛 ∈ ℤ ↦ if ( 𝑛 = 0 , if ( ( 𝑎 ↑ 2 ) = 1 , 1 , 0 ) , ( if ( ( 𝑛 < 0 ∧ 𝑎 < 0 ) , - 1 , 1 ) · ( seq 1 ( · , ( 𝑚 ∈ ℕ ↦ if ( 𝑚 ∈ ℙ , ( if ( 𝑚 = 2 , if ( 2 ∥ 𝑎 , 0 , if ( ( 𝑎 mod 8 ) ∈ { 1 , 7 } , 1 , - 1 ) ) , ( ( ( ( 𝑎 ↑ ( ( 𝑚 − 1 ) / 2 ) ) + 1 ) mod 𝑚 ) − 1 ) ) ↑ ( 𝑚 pCnt 𝑛 ) ) , 1 ) ) ) ‘ ( abs ‘ 𝑛 ) ) ) ) )