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 ( ( 𝐴 ∈ ℤ ∧ 𝑃 ∈ ( ℙ ∖ { 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 𝑃 ) ) )