Metamath Proof Explorer

Theorem lgsval

Description: Value of the Legendre symbol at an arbitrary integer. (Contributed by Mario Carneiro, 4-Feb-2015)

Ref Expression
Hypothesis lgsval.1 ⊢ 𝐹 = ( 𝑛 ∈ ℕ ↦ if ( 𝑛 ∈ ℙ , ( if ( 𝑛 = 2 , if ( 2 ∥ 𝐴 , 0 , if ( ( 𝐴 mod 8 ) ∈ { 1 , 7 } , 1 , - 1 ) ) , ( ( ( ( 𝐴 ↑ ( ( 𝑛 − 1 ) / 2 ) ) + 1 ) mod 𝑛 ) − 1 ) ) ↑ ( 𝑛 pCnt 𝑁 ) ) , 1 ) )
Assertion lgsval ( ( 𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ) → ( 𝐴 /L 𝑁 ) = if ( 𝑁 = 0 , if ( ( 𝐴 ↑ 2 ) = 1 , 1 , 0 ) , ( if ( ( 𝑁 < 0 ∧ 𝐴 < 0 ) , - 1 , 1 ) · ( seq 1 ( · , 𝐹 ) ‘ ( abs ‘ 𝑁 ) ) ) ) )

Proof

Step Hyp Ref Expression
1 lgsval.1 ⊢ 𝐹 = ( 𝑛 ∈ ℕ ↦ if ( 𝑛 ∈ ℙ , ( if ( 𝑛 = 2 , if ( 2 ∥ 𝐴 , 0 , if ( ( 𝐴 mod 8 ) ∈ { 1 , 7 } , 1 , - 1 ) ) , ( ( ( ( 𝐴 ↑ ( ( 𝑛 − 1 ) / 2 ) ) + 1 ) mod 𝑛 ) − 1 ) ) ↑ ( 𝑛 pCnt 𝑁 ) ) , 1 ) )
2 simpr ⊢ ( ( 𝑎 = 𝐴 ∧ 𝑚 = 𝑁 ) → 𝑚 = 𝑁 )
3 2 eqeq1d ⊢ ( ( 𝑎 = 𝐴 ∧ 𝑚 = 𝑁 ) → ( 𝑚 = 0 ↔ 𝑁 = 0 ) )
4 simpl ⊢ ( ( 𝑎 = 𝐴 ∧ 𝑚 = 𝑁 ) → 𝑎 = 𝐴 )
5 4 oveq1d ⊢ ( ( 𝑎 = 𝐴 ∧ 𝑚 = 𝑁 ) → ( 𝑎 ↑ 2 ) = ( 𝐴 ↑ 2 ) )
6 5 eqeq1d ⊢ ( ( 𝑎 = 𝐴 ∧ 𝑚 = 𝑁 ) → ( ( 𝑎 ↑ 2 ) = 1 ↔ ( 𝐴 ↑ 2 ) = 1 ) )
7 6 ifbid ⊢ ( ( 𝑎 = 𝐴 ∧ 𝑚 = 𝑁 ) → if ( ( 𝑎 ↑ 2 ) = 1 , 1 , 0 ) = if ( ( 𝐴 ↑ 2 ) = 1 , 1 , 0 ) )
8 2 breq1d ⊢ ( ( 𝑎 = 𝐴 ∧ 𝑚 = 𝑁 ) → ( 𝑚 < 0 ↔ 𝑁 < 0 ) )
9 4 breq1d ⊢ ( ( 𝑎 = 𝐴 ∧ 𝑚 = 𝑁 ) → ( 𝑎 < 0 ↔ 𝐴 < 0 ) )
10 8 9 anbi12d ⊢ ( ( 𝑎 = 𝐴 ∧ 𝑚 = 𝑁 ) → ( ( 𝑚 < 0 ∧ 𝑎 < 0 ) ↔ ( 𝑁 < 0 ∧ 𝐴 < 0 ) ) )
11 10 ifbid ⊢ ( ( 𝑎 = 𝐴 ∧ 𝑚 = 𝑁 ) → if ( ( 𝑚 < 0 ∧ 𝑎 < 0 ) , - 1 , 1 ) = if ( ( 𝑁 < 0 ∧ 𝐴 < 0 ) , - 1 , 1 ) )
12 4 breq2d ⊢ ( ( 𝑎 = 𝐴 ∧ 𝑚 = 𝑁 ) → ( 2 ∥ 𝑎 ↔ 2 ∥ 𝐴 ) )
13 4 oveq1d ⊢ ( ( 𝑎 = 𝐴 ∧ 𝑚 = 𝑁 ) → ( 𝑎 mod 8 ) = ( 𝐴 mod 8 ) )
14 13 eleq1d ⊢ ( ( 𝑎 = 𝐴 ∧ 𝑚 = 𝑁 ) → ( ( 𝑎 mod 8 ) ∈ { 1 , 7 } ↔ ( 𝐴 mod 8 ) ∈ { 1 , 7 } ) )
15 14 ifbid ⊢ ( ( 𝑎 = 𝐴 ∧ 𝑚 = 𝑁 ) → if ( ( 𝑎 mod 8 ) ∈ { 1 , 7 } , 1 , - 1 ) = if ( ( 𝐴 mod 8 ) ∈ { 1 , 7 } , 1 , - 1 ) )
16 12 15 ifbieq2d ⊢ ( ( 𝑎 = 𝐴 ∧ 𝑚 = 𝑁 ) → if ( 2 ∥ 𝑎 , 0 , if ( ( 𝑎 mod 8 ) ∈ { 1 , 7 } , 1 , - 1 ) ) = if ( 2 ∥ 𝐴 , 0 , if ( ( 𝐴 mod 8 ) ∈ { 1 , 7 } , 1 , - 1 ) ) )
17 4 oveq1d ⊢ ( ( 𝑎 = 𝐴 ∧ 𝑚 = 𝑁 ) → ( 𝑎 ↑ ( ( 𝑛 − 1 ) / 2 ) ) = ( 𝐴 ↑ ( ( 𝑛 − 1 ) / 2 ) ) )
18 17 oveq1d ⊢ ( ( 𝑎 = 𝐴 ∧ 𝑚 = 𝑁 ) → ( ( 𝑎 ↑ ( ( 𝑛 − 1 ) / 2 ) ) + 1 ) = ( ( 𝐴 ↑ ( ( 𝑛 − 1 ) / 2 ) ) + 1 ) )
19 18 oveq1d ⊢ ( ( 𝑎 = 𝐴 ∧ 𝑚 = 𝑁 ) → ( ( ( 𝑎 ↑ ( ( 𝑛 − 1 ) / 2 ) ) + 1 ) mod 𝑛 ) = ( ( ( 𝐴 ↑ ( ( 𝑛 − 1 ) / 2 ) ) + 1 ) mod 𝑛 ) )
20 19 oveq1d ⊢ ( ( 𝑎 = 𝐴 ∧ 𝑚 = 𝑁 ) → ( ( ( ( 𝑎 ↑ ( ( 𝑛 − 1 ) / 2 ) ) + 1 ) mod 𝑛 ) − 1 ) = ( ( ( ( 𝐴 ↑ ( ( 𝑛 − 1 ) / 2 ) ) + 1 ) mod 𝑛 ) − 1 ) )
21 16 20 ifeq12d ⊢ ( ( 𝑎 = 𝐴 ∧ 𝑚 = 𝑁 ) → if ( 𝑛 = 2 , if ( 2 ∥ 𝑎 , 0 , if ( ( 𝑎 mod 8 ) ∈ { 1 , 7 } , 1 , - 1 ) ) , ( ( ( ( 𝑎 ↑ ( ( 𝑛 − 1 ) / 2 ) ) + 1 ) mod 𝑛 ) − 1 ) ) = if ( 𝑛 = 2 , if ( 2 ∥ 𝐴 , 0 , if ( ( 𝐴 mod 8 ) ∈ { 1 , 7 } , 1 , - 1 ) ) , ( ( ( ( 𝐴 ↑ ( ( 𝑛 − 1 ) / 2 ) ) + 1 ) mod 𝑛 ) − 1 ) ) )
22 2 oveq2d ⊢ ( ( 𝑎 = 𝐴 ∧ 𝑚 = 𝑁 ) → ( 𝑛 pCnt 𝑚 ) = ( 𝑛 pCnt 𝑁 ) )
23 21 22 oveq12d ⊢ ( ( 𝑎 = 𝐴 ∧ 𝑚 = 𝑁 ) → ( if ( 𝑛 = 2 , if ( 2 ∥ 𝑎 , 0 , if ( ( 𝑎 mod 8 ) ∈ { 1 , 7 } , 1 , - 1 ) ) , ( ( ( ( 𝑎 ↑ ( ( 𝑛 − 1 ) / 2 ) ) + 1 ) mod 𝑛 ) − 1 ) ) ↑ ( 𝑛 pCnt 𝑚 ) ) = ( if ( 𝑛 = 2 , if ( 2 ∥ 𝐴 , 0 , if ( ( 𝐴 mod 8 ) ∈ { 1 , 7 } , 1 , - 1 ) ) , ( ( ( ( 𝐴 ↑ ( ( 𝑛 − 1 ) / 2 ) ) + 1 ) mod 𝑛 ) − 1 ) ) ↑ ( 𝑛 pCnt 𝑁 ) ) )
24 23 ifeq1d ⊢ ( ( 𝑎 = 𝐴 ∧ 𝑚 = 𝑁 ) → if ( 𝑛 ∈ ℙ , ( if ( 𝑛 = 2 , if ( 2 ∥ 𝑎 , 0 , if ( ( 𝑎 mod 8 ) ∈ { 1 , 7 } , 1 , - 1 ) ) , ( ( ( ( 𝑎 ↑ ( ( 𝑛 − 1 ) / 2 ) ) + 1 ) mod 𝑛 ) − 1 ) ) ↑ ( 𝑛 pCnt 𝑚 ) ) , 1 ) = if ( 𝑛 ∈ ℙ , ( if ( 𝑛 = 2 , if ( 2 ∥ 𝐴 , 0 , if ( ( 𝐴 mod 8 ) ∈ { 1 , 7 } , 1 , - 1 ) ) , ( ( ( ( 𝐴 ↑ ( ( 𝑛 − 1 ) / 2 ) ) + 1 ) mod 𝑛 ) − 1 ) ) ↑ ( 𝑛 pCnt 𝑁 ) ) , 1 ) )
25 24 mpteq2dv ⊢ ( ( 𝑎 = 𝐴 ∧ 𝑚 = 𝑁 ) → ( 𝑛 ∈ ℕ ↦ if ( 𝑛 ∈ ℙ , ( if ( 𝑛 = 2 , if ( 2 ∥ 𝑎 , 0 , if ( ( 𝑎 mod 8 ) ∈ { 1 , 7 } , 1 , - 1 ) ) , ( ( ( ( 𝑎 ↑ ( ( 𝑛 − 1 ) / 2 ) ) + 1 ) mod 𝑛 ) − 1 ) ) ↑ ( 𝑛 pCnt 𝑚 ) ) , 1 ) ) = ( 𝑛 ∈ ℕ ↦ if ( 𝑛 ∈ ℙ , ( if ( 𝑛 = 2 , if ( 2 ∥ 𝐴 , 0 , if ( ( 𝐴 mod 8 ) ∈ { 1 , 7 } , 1 , - 1 ) ) , ( ( ( ( 𝐴 ↑ ( ( 𝑛 − 1 ) / 2 ) ) + 1 ) mod 𝑛 ) − 1 ) ) ↑ ( 𝑛 pCnt 𝑁 ) ) , 1 ) ) )
26 25 1 eqtr4di ⊢ ( ( 𝑎 = 𝐴 ∧ 𝑚 = 𝑁 ) → ( 𝑛 ∈ ℕ ↦ if ( 𝑛 ∈ ℙ , ( if ( 𝑛 = 2 , if ( 2 ∥ 𝑎 , 0 , if ( ( 𝑎 mod 8 ) ∈ { 1 , 7 } , 1 , - 1 ) ) , ( ( ( ( 𝑎 ↑ ( ( 𝑛 − 1 ) / 2 ) ) + 1 ) mod 𝑛 ) − 1 ) ) ↑ ( 𝑛 pCnt 𝑚 ) ) , 1 ) ) = 𝐹 )
27 26 seqeq3d ⊢ ( ( 𝑎 = 𝐴 ∧ 𝑚 = 𝑁 ) → seq 1 ( · , ( 𝑛 ∈ ℕ ↦ if ( 𝑛 ∈ ℙ , ( if ( 𝑛 = 2 , if ( 2 ∥ 𝑎 , 0 , if ( ( 𝑎 mod 8 ) ∈ { 1 , 7 } , 1 , - 1 ) ) , ( ( ( ( 𝑎 ↑ ( ( 𝑛 − 1 ) / 2 ) ) + 1 ) mod 𝑛 ) − 1 ) ) ↑ ( 𝑛 pCnt 𝑚 ) ) , 1 ) ) ) = seq 1 ( · , 𝐹 ) )
28 2 fveq2d ⊢ ( ( 𝑎 = 𝐴 ∧ 𝑚 = 𝑁 ) → ( abs ‘ 𝑚 ) = ( abs ‘ 𝑁 ) )
29 27 28 fveq12d ⊢ ( ( 𝑎 = 𝐴 ∧ 𝑚 = 𝑁 ) → ( seq 1 ( · , ( 𝑛 ∈ ℕ ↦ if ( 𝑛 ∈ ℙ , ( if ( 𝑛 = 2 , if ( 2 ∥ 𝑎 , 0 , if ( ( 𝑎 mod 8 ) ∈ { 1 , 7 } , 1 , - 1 ) ) , ( ( ( ( 𝑎 ↑ ( ( 𝑛 − 1 ) / 2 ) ) + 1 ) mod 𝑛 ) − 1 ) ) ↑ ( 𝑛 pCnt 𝑚 ) ) , 1 ) ) ) ‘ ( abs ‘ 𝑚 ) ) = ( seq 1 ( · , 𝐹 ) ‘ ( abs ‘ 𝑁 ) ) )
30 11 29 oveq12d ⊢ ( ( 𝑎 = 𝐴 ∧ 𝑚 = 𝑁 ) → ( 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 ‘ 𝑚 ) ) ) = ( if ( ( 𝑁 < 0 ∧ 𝐴 < 0 ) , - 1 , 1 ) · ( seq 1 ( · , 𝐹 ) ‘ ( abs ‘ 𝑁 ) ) ) )
31 3 7 30 ifbieq12d ⊢ ( ( 𝑎 = 𝐴 ∧ 𝑚 = 𝑁 ) → 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 ‘ 𝑚 ) ) ) ) = if ( 𝑁 = 0 , if ( ( 𝐴 ↑ 2 ) = 1 , 1 , 0 ) , ( if ( ( 𝑁 < 0 ∧ 𝐴 < 0 ) , - 1 , 1 ) · ( seq 1 ( · , 𝐹 ) ‘ ( abs ‘ 𝑁 ) ) ) ) )
32 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 ‘ 𝑚 ) ) ) ) )
33 1nn0 ⊢ 1 ∈ ℕ0
34 0nn0 ⊢ 0 ∈ ℕ0
35 33 34 ifcli ⊢ if ( ( 𝐴 ↑ 2 ) = 1 , 1 , 0 ) ∈ ℕ0
36 35 elexi ⊢ if ( ( 𝐴 ↑ 2 ) = 1 , 1 , 0 ) ∈ V
37 ovex ⊢ ( if ( ( 𝑁 < 0 ∧ 𝐴 < 0 ) , - 1 , 1 ) · ( seq 1 ( · , 𝐹 ) ‘ ( abs ‘ 𝑁 ) ) ) ∈ V
38 36 37 ifex ⊢ if ( 𝑁 = 0 , if ( ( 𝐴 ↑ 2 ) = 1 , 1 , 0 ) , ( if ( ( 𝑁 < 0 ∧ 𝐴 < 0 ) , - 1 , 1 ) · ( seq 1 ( · , 𝐹 ) ‘ ( abs ‘ 𝑁 ) ) ) ) ∈ V
39 31 32 38 ovmpoa ⊢ ( ( 𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ) → ( 𝐴 /L 𝑁 ) = if ( 𝑁 = 0 , if ( ( 𝐴 ↑ 2 ) = 1 , 1 , 0 ) , ( if ( ( 𝑁 < 0 ∧ 𝐴 < 0 ) , - 1 , 1 ) · ( seq 1 ( · , 𝐹 ) ‘ ( abs ‘ 𝑁 ) ) ) ) )