# Metamath Proof Explorer

## Theorem lgsqrmodndvds

Description: If the Legendre symbol of an integer A for an odd prime is 1 , then the number is a quadratic residue mod P with a solution x of the congruence ( x ^ 2 ) == A (mod P ) which is not divisible by the prime. (Contributed by AV, 20-Aug-2021) (Proof shortened by AV, 18-Mar-2022)

Ref Expression
Assertion lgsqrmodndvds ${⊢}\left({A}\in ℤ\wedge {P}\in \left(ℙ\setminus \left\{2\right\}\right)\right)\to \left({A}{/}_{L}{P}=1\to \exists {x}\in ℤ\phantom{\rule{.4em}{0ex}}\left({{x}}^{2}\mathrm{mod}{P}={A}\mathrm{mod}{P}\wedge ¬{P}\parallel {x}\right)\right)$

### Proof

Step Hyp Ref Expression
1 lgsqrmod ${⊢}\left({A}\in ℤ\wedge {P}\in \left(ℙ\setminus \left\{2\right\}\right)\right)\to \left({A}{/}_{L}{P}=1\to \exists {x}\in ℤ\phantom{\rule{.4em}{0ex}}{{x}}^{2}\mathrm{mod}{P}={A}\mathrm{mod}{P}\right)$
2 1 imp ${⊢}\left(\left({A}\in ℤ\wedge {P}\in \left(ℙ\setminus \left\{2\right\}\right)\right)\wedge {A}{/}_{L}{P}=1\right)\to \exists {x}\in ℤ\phantom{\rule{.4em}{0ex}}{{x}}^{2}\mathrm{mod}{P}={A}\mathrm{mod}{P}$
3 eldifi ${⊢}{P}\in \left(ℙ\setminus \left\{2\right\}\right)\to {P}\in ℙ$
4 prmnn ${⊢}{P}\in ℙ\to {P}\in ℕ$
5 3 4 syl ${⊢}{P}\in \left(ℙ\setminus \left\{2\right\}\right)\to {P}\in ℕ$
6 5 ad3antlr ${⊢}\left(\left(\left({A}\in ℤ\wedge {P}\in \left(ℙ\setminus \left\{2\right\}\right)\right)\wedge {A}{/}_{L}{P}=1\right)\wedge {x}\in ℤ\right)\to {P}\in ℕ$
7 zsqcl ${⊢}{x}\in ℤ\to {{x}}^{2}\in ℤ$
8 7 adantl ${⊢}\left(\left(\left({A}\in ℤ\wedge {P}\in \left(ℙ\setminus \left\{2\right\}\right)\right)\wedge {A}{/}_{L}{P}=1\right)\wedge {x}\in ℤ\right)\to {{x}}^{2}\in ℤ$
9 simplll ${⊢}\left(\left(\left({A}\in ℤ\wedge {P}\in \left(ℙ\setminus \left\{2\right\}\right)\right)\wedge {A}{/}_{L}{P}=1\right)\wedge {x}\in ℤ\right)\to {A}\in ℤ$
10 moddvds ${⊢}\left({P}\in ℕ\wedge {{x}}^{2}\in ℤ\wedge {A}\in ℤ\right)\to \left({{x}}^{2}\mathrm{mod}{P}={A}\mathrm{mod}{P}↔{P}\parallel \left({{x}}^{2}-{A}\right)\right)$
11 6 8 9 10 syl3anc ${⊢}\left(\left(\left({A}\in ℤ\wedge {P}\in \left(ℙ\setminus \left\{2\right\}\right)\right)\wedge {A}{/}_{L}{P}=1\right)\wedge {x}\in ℤ\right)\to \left({{x}}^{2}\mathrm{mod}{P}={A}\mathrm{mod}{P}↔{P}\parallel \left({{x}}^{2}-{A}\right)\right)$
12 5 nnzd ${⊢}{P}\in \left(ℙ\setminus \left\{2\right\}\right)\to {P}\in ℤ$
13 12 ad3antlr ${⊢}\left(\left(\left({A}\in ℤ\wedge {P}\in \left(ℙ\setminus \left\{2\right\}\right)\right)\wedge {A}{/}_{L}{P}=1\right)\wedge {x}\in ℤ\right)\to {P}\in ℤ$
14 13 8 9 3jca ${⊢}\left(\left(\left({A}\in ℤ\wedge {P}\in \left(ℙ\setminus \left\{2\right\}\right)\right)\wedge {A}{/}_{L}{P}=1\right)\wedge {x}\in ℤ\right)\to \left({P}\in ℤ\wedge {{x}}^{2}\in ℤ\wedge {A}\in ℤ\right)$
15 14 adantl ${⊢}\left({P}\parallel {x}\wedge \left(\left(\left({A}\in ℤ\wedge {P}\in \left(ℙ\setminus \left\{2\right\}\right)\right)\wedge {A}{/}_{L}{P}=1\right)\wedge {x}\in ℤ\right)\right)\to \left({P}\in ℤ\wedge {{x}}^{2}\in ℤ\wedge {A}\in ℤ\right)$
16 dvdssub2 ${⊢}\left(\left({P}\in ℤ\wedge {{x}}^{2}\in ℤ\wedge {A}\in ℤ\right)\wedge {P}\parallel \left({{x}}^{2}-{A}\right)\right)\to \left({P}\parallel {{x}}^{2}↔{P}\parallel {A}\right)$
17 15 16 sylan ${⊢}\left(\left({P}\parallel {x}\wedge \left(\left(\left({A}\in ℤ\wedge {P}\in \left(ℙ\setminus \left\{2\right\}\right)\right)\wedge {A}{/}_{L}{P}=1\right)\wedge {x}\in ℤ\right)\right)\wedge {P}\parallel \left({{x}}^{2}-{A}\right)\right)\to \left({P}\parallel {{x}}^{2}↔{P}\parallel {A}\right)$
18 17 ex ${⊢}\left({P}\parallel {x}\wedge \left(\left(\left({A}\in ℤ\wedge {P}\in \left(ℙ\setminus \left\{2\right\}\right)\right)\wedge {A}{/}_{L}{P}=1\right)\wedge {x}\in ℤ\right)\right)\to \left({P}\parallel \left({{x}}^{2}-{A}\right)\to \left({P}\parallel {{x}}^{2}↔{P}\parallel {A}\right)\right)$
19 bicom ${⊢}\left({P}\parallel {{x}}^{2}↔{P}\parallel {A}\right)↔\left({P}\parallel {A}↔{P}\parallel {{x}}^{2}\right)$
20 3 ad3antlr ${⊢}\left(\left(\left({A}\in ℤ\wedge {P}\in \left(ℙ\setminus \left\{2\right\}\right)\right)\wedge {A}{/}_{L}{P}=1\right)\wedge {x}\in ℤ\right)\to {P}\in ℙ$
21 simpr ${⊢}\left(\left(\left({A}\in ℤ\wedge {P}\in \left(ℙ\setminus \left\{2\right\}\right)\right)\wedge {A}{/}_{L}{P}=1\right)\wedge {x}\in ℤ\right)\to {x}\in ℤ$
22 2nn ${⊢}2\in ℕ$
23 22 a1i ${⊢}\left(\left(\left({A}\in ℤ\wedge {P}\in \left(ℙ\setminus \left\{2\right\}\right)\right)\wedge {A}{/}_{L}{P}=1\right)\wedge {x}\in ℤ\right)\to 2\in ℕ$
24 prmdvdsexp ${⊢}\left({P}\in ℙ\wedge {x}\in ℤ\wedge 2\in ℕ\right)\to \left({P}\parallel {{x}}^{2}↔{P}\parallel {x}\right)$
25 20 21 23 24 syl3anc ${⊢}\left(\left(\left({A}\in ℤ\wedge {P}\in \left(ℙ\setminus \left\{2\right\}\right)\right)\wedge {A}{/}_{L}{P}=1\right)\wedge {x}\in ℤ\right)\to \left({P}\parallel {{x}}^{2}↔{P}\parallel {x}\right)$
26 25 biimparc ${⊢}\left({P}\parallel {x}\wedge \left(\left(\left({A}\in ℤ\wedge {P}\in \left(ℙ\setminus \left\{2\right\}\right)\right)\wedge {A}{/}_{L}{P}=1\right)\wedge {x}\in ℤ\right)\right)\to {P}\parallel {{x}}^{2}$
27 bianir ${⊢}\left({P}\parallel {{x}}^{2}\wedge \left({P}\parallel {A}↔{P}\parallel {{x}}^{2}\right)\right)\to {P}\parallel {A}$
28 5 ad2antlr ${⊢}\left(\left({A}\in ℤ\wedge {P}\in \left(ℙ\setminus \left\{2\right\}\right)\right)\wedge {A}{/}_{L}{P}=1\right)\to {P}\in ℕ$
29 dvdsmod0 ${⊢}\left({P}\in ℕ\wedge {P}\parallel {A}\right)\to {A}\mathrm{mod}{P}=0$
30 29 ex ${⊢}{P}\in ℕ\to \left({P}\parallel {A}\to {A}\mathrm{mod}{P}=0\right)$
31 28 30 syl ${⊢}\left(\left({A}\in ℤ\wedge {P}\in \left(ℙ\setminus \left\{2\right\}\right)\right)\wedge {A}{/}_{L}{P}=1\right)\to \left({P}\parallel {A}\to {A}\mathrm{mod}{P}=0\right)$
32 lgsprme0 ${⊢}\left({A}\in ℤ\wedge {P}\in ℙ\right)\to \left({A}{/}_{L}{P}=0↔{A}\mathrm{mod}{P}=0\right)$
33 3 32 sylan2 ${⊢}\left({A}\in ℤ\wedge {P}\in \left(ℙ\setminus \left\{2\right\}\right)\right)\to \left({A}{/}_{L}{P}=0↔{A}\mathrm{mod}{P}=0\right)$
34 eqeq1 ${⊢}{A}{/}_{L}{P}=0\to \left({A}{/}_{L}{P}=1↔0=1\right)$
35 0ne1 ${⊢}0\ne 1$
36 eqneqall ${⊢}0=1\to \left(0\ne 1\to ¬{P}\parallel {x}\right)$
37 35 36 mpi ${⊢}0=1\to ¬{P}\parallel {x}$
38 34 37 syl6bi ${⊢}{A}{/}_{L}{P}=0\to \left({A}{/}_{L}{P}=1\to ¬{P}\parallel {x}\right)$
39 33 38 syl6bir ${⊢}\left({A}\in ℤ\wedge {P}\in \left(ℙ\setminus \left\{2\right\}\right)\right)\to \left({A}\mathrm{mod}{P}=0\to \left({A}{/}_{L}{P}=1\to ¬{P}\parallel {x}\right)\right)$
40 39 com23 ${⊢}\left({A}\in ℤ\wedge {P}\in \left(ℙ\setminus \left\{2\right\}\right)\right)\to \left({A}{/}_{L}{P}=1\to \left({A}\mathrm{mod}{P}=0\to ¬{P}\parallel {x}\right)\right)$
41 40 imp ${⊢}\left(\left({A}\in ℤ\wedge {P}\in \left(ℙ\setminus \left\{2\right\}\right)\right)\wedge {A}{/}_{L}{P}=1\right)\to \left({A}\mathrm{mod}{P}=0\to ¬{P}\parallel {x}\right)$
42 31 41 syld ${⊢}\left(\left({A}\in ℤ\wedge {P}\in \left(ℙ\setminus \left\{2\right\}\right)\right)\wedge {A}{/}_{L}{P}=1\right)\to \left({P}\parallel {A}\to ¬{P}\parallel {x}\right)$
43 42 ad2antrl ${⊢}\left({P}\parallel {x}\wedge \left(\left(\left({A}\in ℤ\wedge {P}\in \left(ℙ\setminus \left\{2\right\}\right)\right)\wedge {A}{/}_{L}{P}=1\right)\wedge {x}\in ℤ\right)\right)\to \left({P}\parallel {A}\to ¬{P}\parallel {x}\right)$
44 27 43 syl5com ${⊢}\left({P}\parallel {{x}}^{2}\wedge \left({P}\parallel {A}↔{P}\parallel {{x}}^{2}\right)\right)\to \left(\left({P}\parallel {x}\wedge \left(\left(\left({A}\in ℤ\wedge {P}\in \left(ℙ\setminus \left\{2\right\}\right)\right)\wedge {A}{/}_{L}{P}=1\right)\wedge {x}\in ℤ\right)\right)\to ¬{P}\parallel {x}\right)$
45 44 ex ${⊢}{P}\parallel {{x}}^{2}\to \left(\left({P}\parallel {A}↔{P}\parallel {{x}}^{2}\right)\to \left(\left({P}\parallel {x}\wedge \left(\left(\left({A}\in ℤ\wedge {P}\in \left(ℙ\setminus \left\{2\right\}\right)\right)\wedge {A}{/}_{L}{P}=1\right)\wedge {x}\in ℤ\right)\right)\to ¬{P}\parallel {x}\right)\right)$
46 45 com23 ${⊢}{P}\parallel {{x}}^{2}\to \left(\left({P}\parallel {x}\wedge \left(\left(\left({A}\in ℤ\wedge {P}\in \left(ℙ\setminus \left\{2\right\}\right)\right)\wedge {A}{/}_{L}{P}=1\right)\wedge {x}\in ℤ\right)\right)\to \left(\left({P}\parallel {A}↔{P}\parallel {{x}}^{2}\right)\to ¬{P}\parallel {x}\right)\right)$
47 26 46 mpcom ${⊢}\left({P}\parallel {x}\wedge \left(\left(\left({A}\in ℤ\wedge {P}\in \left(ℙ\setminus \left\{2\right\}\right)\right)\wedge {A}{/}_{L}{P}=1\right)\wedge {x}\in ℤ\right)\right)\to \left(\left({P}\parallel {A}↔{P}\parallel {{x}}^{2}\right)\to ¬{P}\parallel {x}\right)$
48 19 47 syl5bi ${⊢}\left({P}\parallel {x}\wedge \left(\left(\left({A}\in ℤ\wedge {P}\in \left(ℙ\setminus \left\{2\right\}\right)\right)\wedge {A}{/}_{L}{P}=1\right)\wedge {x}\in ℤ\right)\right)\to \left(\left({P}\parallel {{x}}^{2}↔{P}\parallel {A}\right)\to ¬{P}\parallel {x}\right)$
49 18 48 syld ${⊢}\left({P}\parallel {x}\wedge \left(\left(\left({A}\in ℤ\wedge {P}\in \left(ℙ\setminus \left\{2\right\}\right)\right)\wedge {A}{/}_{L}{P}=1\right)\wedge {x}\in ℤ\right)\right)\to \left({P}\parallel \left({{x}}^{2}-{A}\right)\to ¬{P}\parallel {x}\right)$
50 49 ex ${⊢}{P}\parallel {x}\to \left(\left(\left(\left({A}\in ℤ\wedge {P}\in \left(ℙ\setminus \left\{2\right\}\right)\right)\wedge {A}{/}_{L}{P}=1\right)\wedge {x}\in ℤ\right)\to \left({P}\parallel \left({{x}}^{2}-{A}\right)\to ¬{P}\parallel {x}\right)\right)$
51 2a1 ${⊢}¬{P}\parallel {x}\to \left(\left(\left(\left({A}\in ℤ\wedge {P}\in \left(ℙ\setminus \left\{2\right\}\right)\right)\wedge {A}{/}_{L}{P}=1\right)\wedge {x}\in ℤ\right)\to \left({P}\parallel \left({{x}}^{2}-{A}\right)\to ¬{P}\parallel {x}\right)\right)$
52 50 51 pm2.61i ${⊢}\left(\left(\left({A}\in ℤ\wedge {P}\in \left(ℙ\setminus \left\{2\right\}\right)\right)\wedge {A}{/}_{L}{P}=1\right)\wedge {x}\in ℤ\right)\to \left({P}\parallel \left({{x}}^{2}-{A}\right)\to ¬{P}\parallel {x}\right)$
53 11 52 sylbid ${⊢}\left(\left(\left({A}\in ℤ\wedge {P}\in \left(ℙ\setminus \left\{2\right\}\right)\right)\wedge {A}{/}_{L}{P}=1\right)\wedge {x}\in ℤ\right)\to \left({{x}}^{2}\mathrm{mod}{P}={A}\mathrm{mod}{P}\to ¬{P}\parallel {x}\right)$
54 53 ancld ${⊢}\left(\left(\left({A}\in ℤ\wedge {P}\in \left(ℙ\setminus \left\{2\right\}\right)\right)\wedge {A}{/}_{L}{P}=1\right)\wedge {x}\in ℤ\right)\to \left({{x}}^{2}\mathrm{mod}{P}={A}\mathrm{mod}{P}\to \left({{x}}^{2}\mathrm{mod}{P}={A}\mathrm{mod}{P}\wedge ¬{P}\parallel {x}\right)\right)$
55 54 reximdva ${⊢}\left(\left({A}\in ℤ\wedge {P}\in \left(ℙ\setminus \left\{2\right\}\right)\right)\wedge {A}{/}_{L}{P}=1\right)\to \left(\exists {x}\in ℤ\phantom{\rule{.4em}{0ex}}{{x}}^{2}\mathrm{mod}{P}={A}\mathrm{mod}{P}\to \exists {x}\in ℤ\phantom{\rule{.4em}{0ex}}\left({{x}}^{2}\mathrm{mod}{P}={A}\mathrm{mod}{P}\wedge ¬{P}\parallel {x}\right)\right)$
56 2 55 mpd ${⊢}\left(\left({A}\in ℤ\wedge {P}\in \left(ℙ\setminus \left\{2\right\}\right)\right)\wedge {A}{/}_{L}{P}=1\right)\to \exists {x}\in ℤ\phantom{\rule{.4em}{0ex}}\left({{x}}^{2}\mathrm{mod}{P}={A}\mathrm{mod}{P}\wedge ¬{P}\parallel {x}\right)$
57 56 ex ${⊢}\left({A}\in ℤ\wedge {P}\in \left(ℙ\setminus \left\{2\right\}\right)\right)\to \left({A}{/}_{L}{P}=1\to \exists {x}\in ℤ\phantom{\rule{.4em}{0ex}}\left({{x}}^{2}\mathrm{mod}{P}={A}\mathrm{mod}{P}\wedge ¬{P}\parallel {x}\right)\right)$