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 ) )