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 ∈ ℤ ∧ P ∈ ℙ ∖ 2 → A / L P = 1 → ∃ x ∈ ℤ x 2 mod P = A mod P

Proof

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