Metamath Proof Explorer

Theorem lgsqrmod

Description: If the Legendre symbol of an integer for an odd prime is 1 , then the number is a quadratic residue mod P . (Contributed by AV, 20-Aug-2021)

		Ref	Expression
	Assertion	lgsqrmod	$⊢ (A \in ℤ \land P \in (ℙ ∖ \{2\})) \to (A /_{L} P = 1 \to \exists x \in ℤ x^{2} \mod P = A \mod P)$

Proof

Step	Hyp	Ref	Expression
1		lgsqr	$⊢ (A \in ℤ \land P \in (ℙ ∖ \{2\})) \to (A /_{L} P = 1 \leftrightarrow (\neg P ∥ A \land \exists x \in ℤ P ∥ (x^{2} - A)))$
2		eldifi	$⊢ P \in (ℙ ∖ \{2\}) \to P \in ℙ$
3		prmnn	$⊢ P \in ℙ \to P \in ℕ$
4	2 3	syl	$⊢ P \in (ℙ ∖ \{2\}) \to P \in ℕ$
5	4	ad2antlr	$⊢ ((A \in ℤ \land P \in (ℙ ∖ \{2\})) \land x \in ℤ) \to P \in ℕ$
6		zsqcl	$⊢ x \in ℤ \to x^{2} \in ℤ$
7	6	adantl	$⊢ ((A \in ℤ \land P \in (ℙ ∖ \{2\})) \land x \in ℤ) \to x^{2} \in ℤ$
8		simpll	$⊢ ((A \in ℤ \land P \in (ℙ ∖ \{2\})) \land x \in ℤ) \to A \in ℤ$
9		moddvds	$⊢ (P \in ℕ \land x^{2} \in ℤ \land A \in ℤ) \to (x^{2} \mod P = A \mod P \leftrightarrow P ∥ (x^{2} - A))$
10	5 7 8 9	syl3anc	$⊢ ((A \in ℤ \land P \in (ℙ ∖ \{2\})) \land x \in ℤ) \to (x^{2} \mod P = A \mod P \leftrightarrow P ∥ (x^{2} - A))$
11	10	biimprd	$⊢ ((A \in ℤ \land P \in (ℙ ∖ \{2\})) \land x \in ℤ) \to (P ∥ (x^{2} - A) \to x^{2} \mod P = A \mod P)$
12	11	reximdva	$⊢ (A \in ℤ \land P \in (ℙ ∖ \{2\})) \to (\exists x \in ℤ P ∥ (x^{2} - A) \to \exists x \in ℤ x^{2} \mod P = A \mod P)$
13	12	adantld	$⊢ (A \in ℤ \land P \in (ℙ ∖ \{2\})) \to ((\neg P ∥ A \land \exists x \in ℤ P ∥ (x^{2} - A)) \to \exists x \in ℤ x^{2} \mod P = A \mod P)$
14	1 13	sylbid	$⊢ (A \in ℤ \land P \in (ℙ ∖ \{2\})) \to (A /_{L} P = 1 \to \exists x \in ℤ x^{2} \mod P = A \mod P)$