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

Proof

Step Hyp Ref Expression
1 lgsqrmod ⊢ ( ( 𝐴 ∈ ℤ ∧ 𝑃 ∈ ( ℙ ∖ { 2 } ) ) → ( ( 𝐴 /L 𝑃 ) = 1 → ∃ 𝑥 ∈ ℤ ( ( 𝑥 ↑ 2 ) mod 𝑃 ) = ( 𝐴 mod 𝑃 ) ) )
2 1 imp ⊢ ( ( ( 𝐴 ∈ ℤ ∧ 𝑃 ∈ ( ℙ ∖ { 2 } ) ) ∧ ( 𝐴 /L 𝑃 ) = 1 ) → ∃ 𝑥 ∈ ℤ ( ( 𝑥 ↑ 2 ) mod 𝑃 ) = ( 𝐴 mod 𝑃 ) )
3 eldifi ⊢ ( 𝑃 ∈ ( ℙ ∖ { 2 } ) → 𝑃 ∈ ℙ )
4 prmnn ⊢ ( 𝑃 ∈ ℙ → 𝑃 ∈ ℕ )
5 3 4 syl ⊢ ( 𝑃 ∈ ( ℙ ∖ { 2 } ) → 𝑃 ∈ ℕ )
6 5 ad3antlr ⊢ ( ( ( ( 𝐴 ∈ ℤ ∧ 𝑃 ∈ ( ℙ ∖ { 2 } ) ) ∧ ( 𝐴 /L 𝑃 ) = 1 ) ∧ 𝑥 ∈ ℤ ) → 𝑃 ∈ ℕ )
7 zsqcl ⊢ ( 𝑥 ∈ ℤ → ( 𝑥 ↑ 2 ) ∈ ℤ )
8 7 adantl ⊢ ( ( ( ( 𝐴 ∈ ℤ ∧ 𝑃 ∈ ( ℙ ∖ { 2 } ) ) ∧ ( 𝐴 /L 𝑃 ) = 1 ) ∧ 𝑥 ∈ ℤ ) → ( 𝑥 ↑ 2 ) ∈ ℤ )
9 simplll ⊢ ( ( ( ( 𝐴 ∈ ℤ ∧ 𝑃 ∈ ( ℙ ∖ { 2 } ) ) ∧ ( 𝐴 /L 𝑃 ) = 1 ) ∧ 𝑥 ∈ ℤ ) → 𝐴 ∈ ℤ )
10 moddvds ⊢ ( ( 𝑃 ∈ ℕ ∧ ( 𝑥 ↑ 2 ) ∈ ℤ ∧ 𝐴 ∈ ℤ ) → ( ( ( 𝑥 ↑ 2 ) mod 𝑃 ) = ( 𝐴 mod 𝑃 ) ↔ 𝑃 ∥ ( ( 𝑥 ↑ 2 ) − 𝐴 ) ) )
11 6 8 9 10 syl3anc ⊢ ( ( ( ( 𝐴 ∈ ℤ ∧ 𝑃 ∈ ( ℙ ∖ { 2 } ) ) ∧ ( 𝐴 /L 𝑃 ) = 1 ) ∧ 𝑥 ∈ ℤ ) → ( ( ( 𝑥 ↑ 2 ) mod 𝑃 ) = ( 𝐴 mod 𝑃 ) ↔ 𝑃 ∥ ( ( 𝑥 ↑ 2 ) − 𝐴 ) ) )
12 5 nnzd ⊢ ( 𝑃 ∈ ( ℙ ∖ { 2 } ) → 𝑃 ∈ ℤ )
13 12 ad3antlr ⊢ ( ( ( ( 𝐴 ∈ ℤ ∧ 𝑃 ∈ ( ℙ ∖ { 2 } ) ) ∧ ( 𝐴 /L 𝑃 ) = 1 ) ∧ 𝑥 ∈ ℤ ) → 𝑃 ∈ ℤ )
14 13 8 9 3jca ⊢ ( ( ( ( 𝐴 ∈ ℤ ∧ 𝑃 ∈ ( ℙ ∖ { 2 } ) ) ∧ ( 𝐴 /L 𝑃 ) = 1 ) ∧ 𝑥 ∈ ℤ ) → ( 𝑃 ∈ ℤ ∧ ( 𝑥 ↑ 2 ) ∈ ℤ ∧ 𝐴 ∈ ℤ ) )
15 14 adantl ⊢ ( ( 𝑃 ∥ 𝑥 ∧ ( ( ( 𝐴 ∈ ℤ ∧ 𝑃 ∈ ( ℙ ∖ { 2 } ) ) ∧ ( 𝐴 /L 𝑃 ) = 1 ) ∧ 𝑥 ∈ ℤ ) ) → ( 𝑃 ∈ ℤ ∧ ( 𝑥 ↑ 2 ) ∈ ℤ ∧ 𝐴 ∈ ℤ ) )
16 dvdssub2 ⊢ ( ( ( 𝑃 ∈ ℤ ∧ ( 𝑥 ↑ 2 ) ∈ ℤ ∧ 𝐴 ∈ ℤ ) ∧ 𝑃 ∥ ( ( 𝑥 ↑ 2 ) − 𝐴 ) ) → ( 𝑃 ∥ ( 𝑥 ↑ 2 ) ↔ 𝑃 ∥ 𝐴 ) )
17 15 16 sylan ⊢ ( ( ( 𝑃 ∥ 𝑥 ∧ ( ( ( 𝐴 ∈ ℤ ∧ 𝑃 ∈ ( ℙ ∖ { 2 } ) ) ∧ ( 𝐴 /L 𝑃 ) = 1 ) ∧ 𝑥 ∈ ℤ ) ) ∧ 𝑃 ∥ ( ( 𝑥 ↑ 2 ) − 𝐴 ) ) → ( 𝑃 ∥ ( 𝑥 ↑ 2 ) ↔ 𝑃 ∥ 𝐴 ) )
18 17 ex ⊢ ( ( 𝑃 ∥ 𝑥 ∧ ( ( ( 𝐴 ∈ ℤ ∧ 𝑃 ∈ ( ℙ ∖ { 2 } ) ) ∧ ( 𝐴 /L 𝑃 ) = 1 ) ∧ 𝑥 ∈ ℤ ) ) → ( 𝑃 ∥ ( ( 𝑥 ↑ 2 ) − 𝐴 ) → ( 𝑃 ∥ ( 𝑥 ↑ 2 ) ↔ 𝑃 ∥ 𝐴 ) ) )
19 bicom ⊢ ( ( 𝑃 ∥ ( 𝑥 ↑ 2 ) ↔ 𝑃 ∥ 𝐴 ) ↔ ( 𝑃 ∥ 𝐴 ↔ 𝑃 ∥ ( 𝑥 ↑ 2 ) ) )
20 3 ad3antlr ⊢ ( ( ( ( 𝐴 ∈ ℤ ∧ 𝑃 ∈ ( ℙ ∖ { 2 } ) ) ∧ ( 𝐴 /L 𝑃 ) = 1 ) ∧ 𝑥 ∈ ℤ ) → 𝑃 ∈ ℙ )
21 simpr ⊢ ( ( ( ( 𝐴 ∈ ℤ ∧ 𝑃 ∈ ( ℙ ∖ { 2 } ) ) ∧ ( 𝐴 /L 𝑃 ) = 1 ) ∧ 𝑥 ∈ ℤ ) → 𝑥 ∈ ℤ )
22 2nn ⊢ 2 ∈ ℕ
23 22 a1i ⊢ ( ( ( ( 𝐴 ∈ ℤ ∧ 𝑃 ∈ ( ℙ ∖ { 2 } ) ) ∧ ( 𝐴 /L 𝑃 ) = 1 ) ∧ 𝑥 ∈ ℤ ) → 2 ∈ ℕ )
24 prmdvdsexp ⊢ ( ( 𝑃 ∈ ℙ ∧ 𝑥 ∈ ℤ ∧ 2 ∈ ℕ ) → ( 𝑃 ∥ ( 𝑥 ↑ 2 ) ↔ 𝑃 ∥ 𝑥 ) )
25 20 21 23 24 syl3anc ⊢ ( ( ( ( 𝐴 ∈ ℤ ∧ 𝑃 ∈ ( ℙ ∖ { 2 } ) ) ∧ ( 𝐴 /L 𝑃 ) = 1 ) ∧ 𝑥 ∈ ℤ ) → ( 𝑃 ∥ ( 𝑥 ↑ 2 ) ↔ 𝑃 ∥ 𝑥 ) )
26 25 biimparc ⊢ ( ( 𝑃 ∥ 𝑥 ∧ ( ( ( 𝐴 ∈ ℤ ∧ 𝑃 ∈ ( ℙ ∖ { 2 } ) ) ∧ ( 𝐴 /L 𝑃 ) = 1 ) ∧ 𝑥 ∈ ℤ ) ) → 𝑃 ∥ ( 𝑥 ↑ 2 ) )
27 bianir ⊢ ( ( 𝑃 ∥ ( 𝑥 ↑ 2 ) ∧ ( 𝑃 ∥ 𝐴 ↔ 𝑃 ∥ ( 𝑥 ↑ 2 ) ) ) → 𝑃 ∥ 𝐴 )
28 5 ad2antlr ⊢ ( ( ( 𝐴 ∈ ℤ ∧ 𝑃 ∈ ( ℙ ∖ { 2 } ) ) ∧ ( 𝐴 /L 𝑃 ) = 1 ) → 𝑃 ∈ ℕ )
29 dvdsmod0 ⊢ ( ( 𝑃 ∈ ℕ ∧ 𝑃 ∥ 𝐴 ) → ( 𝐴 mod 𝑃 ) = 0 )
30 29 ex ⊢ ( 𝑃 ∈ ℕ → ( 𝑃 ∥ 𝐴 → ( 𝐴 mod 𝑃 ) = 0 ) )
31 28 30 syl ⊢ ( ( ( 𝐴 ∈ ℤ ∧ 𝑃 ∈ ( ℙ ∖ { 2 } ) ) ∧ ( 𝐴 /L 𝑃 ) = 1 ) → ( 𝑃 ∥ 𝐴 → ( 𝐴 mod 𝑃 ) = 0 ) )
32 lgsprme0 ⊢ ( ( 𝐴 ∈ ℤ ∧ 𝑃 ∈ ℙ ) → ( ( 𝐴 /L 𝑃 ) = 0 ↔ ( 𝐴 mod 𝑃 ) = 0 ) )
33 3 32 sylan2 ⊢ ( ( 𝐴 ∈ ℤ ∧ 𝑃 ∈ ( ℙ ∖ { 2 } ) ) → ( ( 𝐴 /L 𝑃 ) = 0 ↔ ( 𝐴 mod 𝑃 ) = 0 ) )
34 eqeq1 ⊢ ( ( 𝐴 /L 𝑃 ) = 0 → ( ( 𝐴 /L 𝑃 ) = 1 ↔ 0 = 1 ) )
35 0ne1 ⊢ 0 ≠ 1
36 eqneqall ⊢ ( 0 = 1 → ( 0 ≠ 1 → ¬ 𝑃 ∥ 𝑥 ) )
37 35 36 mpi ⊢ ( 0 = 1 → ¬ 𝑃 ∥ 𝑥 )
38 34 37 biimtrdi ⊢ ( ( 𝐴 /L 𝑃 ) = 0 → ( ( 𝐴 /L 𝑃 ) = 1 → ¬ 𝑃 ∥ 𝑥 ) )
39 33 38 biimtrrdi ⊢ ( ( 𝐴 ∈ ℤ ∧ 𝑃 ∈ ( ℙ ∖ { 2 } ) ) → ( ( 𝐴 mod 𝑃 ) = 0 → ( ( 𝐴 /L 𝑃 ) = 1 → ¬ 𝑃 ∥ 𝑥 ) ) )
40 39 com23 ⊢ ( ( 𝐴 ∈ ℤ ∧ 𝑃 ∈ ( ℙ ∖ { 2 } ) ) → ( ( 𝐴 /L 𝑃 ) = 1 → ( ( 𝐴 mod 𝑃 ) = 0 → ¬ 𝑃 ∥ 𝑥 ) ) )
41 40 imp ⊢ ( ( ( 𝐴 ∈ ℤ ∧ 𝑃 ∈ ( ℙ ∖ { 2 } ) ) ∧ ( 𝐴 /L 𝑃 ) = 1 ) → ( ( 𝐴 mod 𝑃 ) = 0 → ¬ 𝑃 ∥ 𝑥 ) )
42 31 41 syld ⊢ ( ( ( 𝐴 ∈ ℤ ∧ 𝑃 ∈ ( ℙ ∖ { 2 } ) ) ∧ ( 𝐴 /L 𝑃 ) = 1 ) → ( 𝑃 ∥ 𝐴 → ¬ 𝑃 ∥ 𝑥 ) )
43 42 ad2antrl ⊢ ( ( 𝑃 ∥ 𝑥 ∧ ( ( ( 𝐴 ∈ ℤ ∧ 𝑃 ∈ ( ℙ ∖ { 2 } ) ) ∧ ( 𝐴 /L 𝑃 ) = 1 ) ∧ 𝑥 ∈ ℤ ) ) → ( 𝑃 ∥ 𝐴 → ¬ 𝑃 ∥ 𝑥 ) )
44 27 43 syl5com ⊢ ( ( 𝑃 ∥ ( 𝑥 ↑ 2 ) ∧ ( 𝑃 ∥ 𝐴 ↔ 𝑃 ∥ ( 𝑥 ↑ 2 ) ) ) → ( ( 𝑃 ∥ 𝑥 ∧ ( ( ( 𝐴 ∈ ℤ ∧ 𝑃 ∈ ( ℙ ∖ { 2 } ) ) ∧ ( 𝐴 /L 𝑃 ) = 1 ) ∧ 𝑥 ∈ ℤ ) ) → ¬ 𝑃 ∥ 𝑥 ) )
45 44 ex ⊢ ( 𝑃 ∥ ( 𝑥 ↑ 2 ) → ( ( 𝑃 ∥ 𝐴 ↔ 𝑃 ∥ ( 𝑥 ↑ 2 ) ) → ( ( 𝑃 ∥ 𝑥 ∧ ( ( ( 𝐴 ∈ ℤ ∧ 𝑃 ∈ ( ℙ ∖ { 2 } ) ) ∧ ( 𝐴 /L 𝑃 ) = 1 ) ∧ 𝑥 ∈ ℤ ) ) → ¬ 𝑃 ∥ 𝑥 ) ) )
46 45 com23 ⊢ ( 𝑃 ∥ ( 𝑥 ↑ 2 ) → ( ( 𝑃 ∥ 𝑥 ∧ ( ( ( 𝐴 ∈ ℤ ∧ 𝑃 ∈ ( ℙ ∖ { 2 } ) ) ∧ ( 𝐴 /L 𝑃 ) = 1 ) ∧ 𝑥 ∈ ℤ ) ) → ( ( 𝑃 ∥ 𝐴 ↔ 𝑃 ∥ ( 𝑥 ↑ 2 ) ) → ¬ 𝑃 ∥ 𝑥 ) ) )
47 26 46 mpcom ⊢ ( ( 𝑃 ∥ 𝑥 ∧ ( ( ( 𝐴 ∈ ℤ ∧ 𝑃 ∈ ( ℙ ∖ { 2 } ) ) ∧ ( 𝐴 /L 𝑃 ) = 1 ) ∧ 𝑥 ∈ ℤ ) ) → ( ( 𝑃 ∥ 𝐴 ↔ 𝑃 ∥ ( 𝑥 ↑ 2 ) ) → ¬ 𝑃 ∥ 𝑥 ) )
48 19 47 biimtrid ⊢ ( ( 𝑃 ∥ 𝑥 ∧ ( ( ( 𝐴 ∈ ℤ ∧ 𝑃 ∈ ( ℙ ∖ { 2 } ) ) ∧ ( 𝐴 /L 𝑃 ) = 1 ) ∧ 𝑥 ∈ ℤ ) ) → ( ( 𝑃 ∥ ( 𝑥 ↑ 2 ) ↔ 𝑃 ∥ 𝐴 ) → ¬ 𝑃 ∥ 𝑥 ) )
49 18 48 syld ⊢ ( ( 𝑃 ∥ 𝑥 ∧ ( ( ( 𝐴 ∈ ℤ ∧ 𝑃 ∈ ( ℙ ∖ { 2 } ) ) ∧ ( 𝐴 /L 𝑃 ) = 1 ) ∧ 𝑥 ∈ ℤ ) ) → ( 𝑃 ∥ ( ( 𝑥 ↑ 2 ) − 𝐴 ) → ¬ 𝑃 ∥ 𝑥 ) )
50 49 ex ⊢ ( 𝑃 ∥ 𝑥 → ( ( ( ( 𝐴 ∈ ℤ ∧ 𝑃 ∈ ( ℙ ∖ { 2 } ) ) ∧ ( 𝐴 /L 𝑃 ) = 1 ) ∧ 𝑥 ∈ ℤ ) → ( 𝑃 ∥ ( ( 𝑥 ↑ 2 ) − 𝐴 ) → ¬ 𝑃 ∥ 𝑥 ) ) )
51 2a1 ⊢ ( ¬ 𝑃 ∥ 𝑥 → ( ( ( ( 𝐴 ∈ ℤ ∧ 𝑃 ∈ ( ℙ ∖ { 2 } ) ) ∧ ( 𝐴 /L 𝑃 ) = 1 ) ∧ 𝑥 ∈ ℤ ) → ( 𝑃 ∥ ( ( 𝑥 ↑ 2 ) − 𝐴 ) → ¬ 𝑃 ∥ 𝑥 ) ) )
52 50 51 pm2.61i ⊢ ( ( ( ( 𝐴 ∈ ℤ ∧ 𝑃 ∈ ( ℙ ∖ { 2 } ) ) ∧ ( 𝐴 /L 𝑃 ) = 1 ) ∧ 𝑥 ∈ ℤ ) → ( 𝑃 ∥ ( ( 𝑥 ↑ 2 ) − 𝐴 ) → ¬ 𝑃 ∥ 𝑥 ) )
53 11 52 sylbid ⊢ ( ( ( ( 𝐴 ∈ ℤ ∧ 𝑃 ∈ ( ℙ ∖ { 2 } ) ) ∧ ( 𝐴 /L 𝑃 ) = 1 ) ∧ 𝑥 ∈ ℤ ) → ( ( ( 𝑥 ↑ 2 ) mod 𝑃 ) = ( 𝐴 mod 𝑃 ) → ¬ 𝑃 ∥ 𝑥 ) )
54 53 ancld ⊢ ( ( ( ( 𝐴 ∈ ℤ ∧ 𝑃 ∈ ( ℙ ∖ { 2 } ) ) ∧ ( 𝐴 /L 𝑃 ) = 1 ) ∧ 𝑥 ∈ ℤ ) → ( ( ( 𝑥 ↑ 2 ) mod 𝑃 ) = ( 𝐴 mod 𝑃 ) → ( ( ( 𝑥 ↑ 2 ) mod 𝑃 ) = ( 𝐴 mod 𝑃 ) ∧ ¬ 𝑃 ∥ 𝑥 ) ) )
55 54 reximdva ⊢ ( ( ( 𝐴 ∈ ℤ ∧ 𝑃 ∈ ( ℙ ∖ { 2 } ) ) ∧ ( 𝐴 /L 𝑃 ) = 1 ) → ( ∃ 𝑥 ∈ ℤ ( ( 𝑥 ↑ 2 ) mod 𝑃 ) = ( 𝐴 mod 𝑃 ) → ∃ 𝑥 ∈ ℤ ( ( ( 𝑥 ↑ 2 ) mod 𝑃 ) = ( 𝐴 mod 𝑃 ) ∧ ¬ 𝑃 ∥ 𝑥 ) ) )
56 2 55 mpd ⊢ ( ( ( 𝐴 ∈ ℤ ∧ 𝑃 ∈ ( ℙ ∖ { 2 } ) ) ∧ ( 𝐴 /L 𝑃 ) = 1 ) → ∃ 𝑥 ∈ ℤ ( ( ( 𝑥 ↑ 2 ) mod 𝑃 ) = ( 𝐴 mod 𝑃 ) ∧ ¬ 𝑃 ∥ 𝑥 ) )
57 56 ex ⊢ ( ( 𝐴 ∈ ℤ ∧ 𝑃 ∈ ( ℙ ∖ { 2 } ) ) → ( ( 𝐴 /L 𝑃 ) = 1 → ∃ 𝑥 ∈ ℤ ( ( ( 𝑥 ↑ 2 ) mod 𝑃 ) = ( 𝐴 mod 𝑃 ) ∧ ¬ 𝑃 ∥ 𝑥 ) ) )