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	⊢ ( ( 𝐴 ∈ ℤ ∧ 𝑃 ∈ ( ℙ ∖ { 2 } ) ) → ( ( 𝐴 /L 𝑃 ) = 1 → ∃ 𝑥 ∈ ℤ ( ( 𝑥 ↑ 2 ) mod 𝑃 ) = ( 𝐴 mod 𝑃 ) ) )

Proof

Step	Hyp	Ref	Expression
1		lgsqr	⊢ ( ( 𝐴 ∈ ℤ ∧ 𝑃 ∈ ( ℙ ∖ { 2 } ) ) → ( ( 𝐴 /L 𝑃 ) = 1 ↔ ( ¬ 𝑃 ∥ 𝐴 ∧ ∃ 𝑥 ∈ ℤ 𝑃 ∥ ( ( 𝑥 ↑ 2 ) − 𝐴 ) ) ) )
2		eldifi	⊢ ( 𝑃 ∈ ( ℙ ∖ { 2 } ) → 𝑃 ∈ ℙ )
3		prmnn	⊢ ( 𝑃 ∈ ℙ → 𝑃 ∈ ℕ )
4	2 3	syl	⊢ ( 𝑃 ∈ ( ℙ ∖ { 2 } ) → 𝑃 ∈ ℕ )
5	4	ad2antlr	⊢ ( ( ( 𝐴 ∈ ℤ ∧ 𝑃 ∈ ( ℙ ∖ { 2 } ) ) ∧ 𝑥 ∈ ℤ ) → 𝑃 ∈ ℕ )
6		zsqcl	⊢ ( 𝑥 ∈ ℤ → ( 𝑥 ↑ 2 ) ∈ ℤ )
7	6	adantl	⊢ ( ( ( 𝐴 ∈ ℤ ∧ 𝑃 ∈ ( ℙ ∖ { 2 } ) ) ∧ 𝑥 ∈ ℤ ) → ( 𝑥 ↑ 2 ) ∈ ℤ )
8		simpll	⊢ ( ( ( 𝐴 ∈ ℤ ∧ 𝑃 ∈ ( ℙ ∖ { 2 } ) ) ∧ 𝑥 ∈ ℤ ) → 𝐴 ∈ ℤ )
9		moddvds	⊢ ( ( 𝑃 ∈ ℕ ∧ ( 𝑥 ↑ 2 ) ∈ ℤ ∧ 𝐴 ∈ ℤ ) → ( ( ( 𝑥 ↑ 2 ) mod 𝑃 ) = ( 𝐴 mod 𝑃 ) ↔ 𝑃 ∥ ( ( 𝑥 ↑ 2 ) − 𝐴 ) ) )
10	5 7 8 9	syl3anc	⊢ ( ( ( 𝐴 ∈ ℤ ∧ 𝑃 ∈ ( ℙ ∖ { 2 } ) ) ∧ 𝑥 ∈ ℤ ) → ( ( ( 𝑥 ↑ 2 ) mod 𝑃 ) = ( 𝐴 mod 𝑃 ) ↔ 𝑃 ∥ ( ( 𝑥 ↑ 2 ) − 𝐴 ) ) )
11	10	biimprd	⊢ ( ( ( 𝐴 ∈ ℤ ∧ 𝑃 ∈ ( ℙ ∖ { 2 } ) ) ∧ 𝑥 ∈ ℤ ) → ( 𝑃 ∥ ( ( 𝑥 ↑ 2 ) − 𝐴 ) → ( ( 𝑥 ↑ 2 ) mod 𝑃 ) = ( 𝐴 mod 𝑃 ) ) )
12	11	reximdva	⊢ ( ( 𝐴 ∈ ℤ ∧ 𝑃 ∈ ( ℙ ∖ { 2 } ) ) → ( ∃ 𝑥 ∈ ℤ 𝑃 ∥ ( ( 𝑥 ↑ 2 ) − 𝐴 ) → ∃ 𝑥 ∈ ℤ ( ( 𝑥 ↑ 2 ) mod 𝑃 ) = ( 𝐴 mod 𝑃 ) ) )
13	12	adantld	⊢ ( ( 𝐴 ∈ ℤ ∧ 𝑃 ∈ ( ℙ ∖ { 2 } ) ) → ( ( ¬ 𝑃 ∥ 𝐴 ∧ ∃ 𝑥 ∈ ℤ 𝑃 ∥ ( ( 𝑥 ↑ 2 ) − 𝐴 ) ) → ∃ 𝑥 ∈ ℤ ( ( 𝑥 ↑ 2 ) mod 𝑃 ) = ( 𝐴 mod 𝑃 ) ) )
14	1 13	sylbid	⊢ ( ( 𝐴 ∈ ℤ ∧ 𝑃 ∈ ( ℙ ∖ { 2 } ) ) → ( ( 𝐴 /L 𝑃 ) = 1 → ∃ 𝑥 ∈ ℤ ( ( 𝑥 ↑ 2 ) mod 𝑃 ) = ( 𝐴 mod 𝑃 ) ) )