Metamath Proof Explorer


Theorem lgsfval

Description: Value of the function F which defines the Legendre symbol at the primes. (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 lgsfval ( 𝑀 ∈ ℕ → ( 𝐹𝑀 ) = if ( 𝑀 ∈ ℙ , ( if ( 𝑀 = 2 , if ( 2 ∥ 𝐴 , 0 , if ( ( 𝐴 mod 8 ) ∈ { 1 , 7 } , 1 , - 1 ) ) , ( ( ( ( 𝐴 ↑ ( ( 𝑀 − 1 ) / 2 ) ) + 1 ) mod 𝑀 ) − 1 ) ) ↑ ( 𝑀 pCnt 𝑁 ) ) , 1 ) )

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 eleq1 ( 𝑛 = 𝑀 → ( 𝑛 ∈ ℙ ↔ 𝑀 ∈ ℙ ) )
3 eqeq1 ( 𝑛 = 𝑀 → ( 𝑛 = 2 ↔ 𝑀 = 2 ) )
4 oveq1 ( 𝑛 = 𝑀 → ( 𝑛 − 1 ) = ( 𝑀 − 1 ) )
5 4 oveq1d ( 𝑛 = 𝑀 → ( ( 𝑛 − 1 ) / 2 ) = ( ( 𝑀 − 1 ) / 2 ) )
6 5 oveq2d ( 𝑛 = 𝑀 → ( 𝐴 ↑ ( ( 𝑛 − 1 ) / 2 ) ) = ( 𝐴 ↑ ( ( 𝑀 − 1 ) / 2 ) ) )
7 6 oveq1d ( 𝑛 = 𝑀 → ( ( 𝐴 ↑ ( ( 𝑛 − 1 ) / 2 ) ) + 1 ) = ( ( 𝐴 ↑ ( ( 𝑀 − 1 ) / 2 ) ) + 1 ) )
8 id ( 𝑛 = 𝑀𝑛 = 𝑀 )
9 7 8 oveq12d ( 𝑛 = 𝑀 → ( ( ( 𝐴 ↑ ( ( 𝑛 − 1 ) / 2 ) ) + 1 ) mod 𝑛 ) = ( ( ( 𝐴 ↑ ( ( 𝑀 − 1 ) / 2 ) ) + 1 ) mod 𝑀 ) )
10 9 oveq1d ( 𝑛 = 𝑀 → ( ( ( ( 𝐴 ↑ ( ( 𝑛 − 1 ) / 2 ) ) + 1 ) mod 𝑛 ) − 1 ) = ( ( ( ( 𝐴 ↑ ( ( 𝑀 − 1 ) / 2 ) ) + 1 ) mod 𝑀 ) − 1 ) )
11 3 10 ifbieq2d ( 𝑛 = 𝑀 → 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 ) ) )
12 oveq1 ( 𝑛 = 𝑀 → ( 𝑛 pCnt 𝑁 ) = ( 𝑀 pCnt 𝑁 ) )
13 11 12 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 𝑁 ) ) )
14 2 13 ifbieq1d ( 𝑛 = 𝑀 → 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 ) )
15 ovex ( if ( 𝑀 = 2 , if ( 2 ∥ 𝐴 , 0 , if ( ( 𝐴 mod 8 ) ∈ { 1 , 7 } , 1 , - 1 ) ) , ( ( ( ( 𝐴 ↑ ( ( 𝑀 − 1 ) / 2 ) ) + 1 ) mod 𝑀 ) − 1 ) ) ↑ ( 𝑀 pCnt 𝑁 ) ) ∈ V
16 1ex 1 ∈ V
17 15 16 ifex if ( 𝑀 ∈ ℙ , ( if ( 𝑀 = 2 , if ( 2 ∥ 𝐴 , 0 , if ( ( 𝐴 mod 8 ) ∈ { 1 , 7 } , 1 , - 1 ) ) , ( ( ( ( 𝐴 ↑ ( ( 𝑀 − 1 ) / 2 ) ) + 1 ) mod 𝑀 ) − 1 ) ) ↑ ( 𝑀 pCnt 𝑁 ) ) , 1 ) ∈ V
18 14 1 17 fvmpt ( 𝑀 ∈ ℕ → ( 𝐹𝑀 ) = if ( 𝑀 ∈ ℙ , ( if ( 𝑀 = 2 , if ( 2 ∥ 𝐴 , 0 , if ( ( 𝐴 mod 8 ) ∈ { 1 , 7 } , 1 , - 1 ) ) , ( ( ( ( 𝐴 ↑ ( ( 𝑀 − 1 ) / 2 ) ) + 1 ) mod 𝑀 ) − 1 ) ) ↑ ( 𝑀 pCnt 𝑁 ) ) , 1 ) )