Theorem lgsval3

Description: The Legendre symbol at an odd prime (this is the traditional domain of the Legendre symbol). (Contributed by Mario Carneiro, 4-Feb-2015)

	Ref	Expression
Assertion	lgsval3	⊢ ( ( 𝐴 ∈ ℤ ∧ 𝑃 ∈ ( ℙ ∖ { 2 } ) ) → ( 𝐴 /L 𝑃 ) = ( ( ( ( 𝐴 ↑ ( ( 𝑃 − 1 ) / 2 ) ) + 1 ) mod 𝑃 ) − 1 ) )

Proof

Step	Hyp	Ref	Expression
1		eldifsn	⊢ ( 𝑃 ∈ ( ℙ ∖ { 2 } ) ↔ ( 𝑃 ∈ ℙ ∧ 𝑃 ≠ 2 ) )
2		lgsval2	⊢ ( ( 𝐴 ∈ ℤ ∧ 𝑃 ∈ ℙ ) → ( 𝐴 /L 𝑃 ) = if ( 𝑃 = 2 , if ( 2 ∥ 𝐴 , 0 , if ( ( 𝐴 mod 8 ) ∈ { 1 , 7 } , 1 , - 1 ) ) , ( ( ( ( 𝐴 ↑ ( ( 𝑃 − 1 ) / 2 ) ) + 1 ) mod 𝑃 ) − 1 ) ) )
3		ifnefalse	⊢ ( 𝑃 ≠ 2 → if ( 𝑃 = 2 , if ( 2 ∥ 𝐴 , 0 , if ( ( 𝐴 mod 8 ) ∈ { 1 , 7 } , 1 , - 1 ) ) , ( ( ( ( 𝐴 ↑ ( ( 𝑃 − 1 ) / 2 ) ) + 1 ) mod 𝑃 ) − 1 ) ) = ( ( ( ( 𝐴 ↑ ( ( 𝑃 − 1 ) / 2 ) ) + 1 ) mod 𝑃 ) − 1 ) )
4	2 3	sylan9eq	⊢ ( ( ( 𝐴 ∈ ℤ ∧ 𝑃 ∈ ℙ ) ∧ 𝑃 ≠ 2 ) → ( 𝐴 /L 𝑃 ) = ( ( ( ( 𝐴 ↑ ( ( 𝑃 − 1 ) / 2 ) ) + 1 ) mod 𝑃 ) − 1 ) )
5	4	anasss	⊢ ( ( 𝐴 ∈ ℤ ∧ ( 𝑃 ∈ ℙ ∧ 𝑃 ≠ 2 ) ) → ( 𝐴 /L 𝑃 ) = ( ( ( ( 𝐴 ↑ ( ( 𝑃 − 1 ) / 2 ) ) + 1 ) mod 𝑃 ) − 1 ) )
6	1 5	sylan2b	⊢ ( ( 𝐴 ∈ ℤ ∧ 𝑃 ∈ ( ℙ ∖ { 2 } ) ) → ( 𝐴 /L 𝑃 ) = ( ( ( ( 𝐴 ↑ ( ( 𝑃 − 1 ) / 2 ) ) + 1 ) mod 𝑃 ) − 1 ) )