Metamath Proof Explorer

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	$⊢ (A \in ℤ \land P \in (ℙ ∖ \{2\})) \to A /_{L} P = ((A^{\frac{P - 1}{2}} + 1) \mod P) - 1$

Proof

Step	Hyp	Ref	Expression
1		eldifsn	$⊢ P \in (ℙ ∖ \{2\}) \leftrightarrow (P \in ℙ \land P \neq 2)$
2		lgsval2	$⊢ (A \in ℤ \land P \in ℙ) \to A /_{L} P = if (P = 2, if (2 ∥ A, 0, if (A \mod 8 \in \{1, 7\}, 1, - 1)), ((A^{\frac{P - 1}{2}} + 1) \mod P) - 1)$
3		ifnefalse	$⊢ P \neq 2 \to if (P = 2, if (2 ∥ A, 0, if (A \mod 8 \in \{1, 7\}, 1, - 1)), ((A^{\frac{P - 1}{2}} + 1) \mod P) - 1) = ((A^{\frac{P - 1}{2}} + 1) \mod P) - 1$
4	2 3	sylan9eq	$⊢ ((A \in ℤ \land P \in ℙ) \land P \neq 2) \to A /_{L} P = ((A^{\frac{P - 1}{2}} + 1) \mod P) - 1$
5	4	anasss	$⊢ (A \in ℤ \land (P \in ℙ \land P \neq 2)) \to A /_{L} P = ((A^{\frac{P - 1}{2}} + 1) \mod P) - 1$
6	1 5	sylan2b	$⊢ (A \in ℤ \land P \in (ℙ ∖ \{2\})) \to A /_{L} P = ((A^{\frac{P - 1}{2}} + 1) \mod P) - 1$