Theorem lgsval2

Description: The Legendre symbol at a prime (this is the traditional domain of the Legendre symbol, except for the addition of prime 2 ). (Contributed by Mario Carneiro, 4-Feb-2015)

	Ref	Expression
Assertion	lgsval2	⊢ ( ( 𝐴 ∈ ℤ ∧ 𝑃 ∈ ℙ ) → ( 𝐴 /L 𝑃 ) = if ( 𝑃 = 2 , if ( 2 ∥ 𝐴 , 0 , if ( ( 𝐴 mod 8 ) ∈ { 1 , 7 } , 1 , - 1 ) ) , ( ( ( ( 𝐴 ↑ ( ( 𝑃 − 1 ) / 2 ) ) + 1 ) mod 𝑃 ) − 1 ) ) )

Proof

Step	Hyp	Ref	Expression
1		eqid	⊢ ( 𝑛 ∈ ℕ ↦ 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 ) )
2	1	lgsval2lem	⊢ ( ( 𝐴 ∈ ℤ ∧ 𝑃 ∈ ℙ ) → ( 𝐴 /L 𝑃 ) = if ( 𝑃 = 2 , if ( 2 ∥ 𝐴 , 0 , if ( ( 𝐴 mod 8 ) ∈ { 1 , 7 } , 1 , - 1 ) ) , ( ( ( ( 𝐴 ↑ ( ( 𝑃 − 1 ) / 2 ) ) + 1 ) mod 𝑃 ) − 1 ) ) )