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 
|- ( ( A e. ZZ /\ P e. ( Prime \ { 2 } ) ) -> ( ( A /L P ) = 1 -> E. x e. ZZ ( ( ( x ^ 2 ) mod P ) = ( A mod P ) /\ -. P || x ) ) )

Proof

Step Hyp Ref Expression
1 lgsqrmod 
 |-  ( ( A e. ZZ /\ P e. ( Prime \ { 2 } ) ) -> ( ( A /L P ) = 1 -> E. x e. ZZ ( ( x ^ 2 ) mod P ) = ( A mod P ) ) )
2 1 imp 
 |-  ( ( ( A e. ZZ /\ P e. ( Prime \ { 2 } ) ) /\ ( A /L P ) = 1 ) -> E. x e. ZZ ( ( x ^ 2 ) mod P ) = ( A mod P ) )
3 eldifi 
 |-  ( P e. ( Prime \ { 2 } ) -> P e. Prime )
4 prmnn 
 |-  ( P e. Prime -> P e. NN )
5 3 4 syl 
 |-  ( P e. ( Prime \ { 2 } ) -> P e. NN )
6 5 ad3antlr 
 |-  ( ( ( ( A e. ZZ /\ P e. ( Prime \ { 2 } ) ) /\ ( A /L P ) = 1 ) /\ x e. ZZ ) -> P e. NN )
7 zsqcl 
 |-  ( x e. ZZ -> ( x ^ 2 ) e. ZZ )
8 7 adantl 
 |-  ( ( ( ( A e. ZZ /\ P e. ( Prime \ { 2 } ) ) /\ ( A /L P ) = 1 ) /\ x e. ZZ ) -> ( x ^ 2 ) e. ZZ )
9 simplll 
 |-  ( ( ( ( A e. ZZ /\ P e. ( Prime \ { 2 } ) ) /\ ( A /L P ) = 1 ) /\ x e. ZZ ) -> A e. ZZ )
10 moddvds 
 |-  ( ( P e. NN /\ ( x ^ 2 ) e. ZZ /\ A e. ZZ ) -> ( ( ( x ^ 2 ) mod P ) = ( A mod P ) <-> P || ( ( x ^ 2 ) - A ) ) )
11 6 8 9 10 syl3anc 
 |-  ( ( ( ( A e. ZZ /\ P e. ( Prime \ { 2 } ) ) /\ ( A /L P ) = 1 ) /\ x e. ZZ ) -> ( ( ( x ^ 2 ) mod P ) = ( A mod P ) <-> P || ( ( x ^ 2 ) - A ) ) )
12 5 nnzd 
 |-  ( P e. ( Prime \ { 2 } ) -> P e. ZZ )
13 12 ad3antlr 
 |-  ( ( ( ( A e. ZZ /\ P e. ( Prime \ { 2 } ) ) /\ ( A /L P ) = 1 ) /\ x e. ZZ ) -> P e. ZZ )
14 13 8 9 3jca 
 |-  ( ( ( ( A e. ZZ /\ P e. ( Prime \ { 2 } ) ) /\ ( A /L P ) = 1 ) /\ x e. ZZ ) -> ( P e. ZZ /\ ( x ^ 2 ) e. ZZ /\ A e. ZZ ) )
15 14 adantl 
 |-  ( ( P || x /\ ( ( ( A e. ZZ /\ P e. ( Prime \ { 2 } ) ) /\ ( A /L P ) = 1 ) /\ x e. ZZ ) ) -> ( P e. ZZ /\ ( x ^ 2 ) e. ZZ /\ A e. ZZ ) )
16 dvdssub2 
 |-  ( ( ( P e. ZZ /\ ( x ^ 2 ) e. ZZ /\ A e. ZZ ) /\ P || ( ( x ^ 2 ) - A ) ) -> ( P || ( x ^ 2 ) <-> P || A ) )
17 15 16 sylan 
 |-  ( ( ( P || x /\ ( ( ( A e. ZZ /\ P e. ( Prime \ { 2 } ) ) /\ ( A /L P ) = 1 ) /\ x e. ZZ ) ) /\ P || ( ( x ^ 2 ) - A ) ) -> ( P || ( x ^ 2 ) <-> P || A ) )
18 17 ex 
 |-  ( ( P || x /\ ( ( ( A e. ZZ /\ P e. ( Prime \ { 2 } ) ) /\ ( A /L P ) = 1 ) /\ x e. ZZ ) ) -> ( P || ( ( x ^ 2 ) - A ) -> ( P || ( x ^ 2 ) <-> P || A ) ) )
19 bicom 
 |-  ( ( P || ( x ^ 2 ) <-> P || A ) <-> ( P || A <-> P || ( x ^ 2 ) ) )
20 3 ad3antlr 
 |-  ( ( ( ( A e. ZZ /\ P e. ( Prime \ { 2 } ) ) /\ ( A /L P ) = 1 ) /\ x e. ZZ ) -> P e. Prime )
21 simpr 
 |-  ( ( ( ( A e. ZZ /\ P e. ( Prime \ { 2 } ) ) /\ ( A /L P ) = 1 ) /\ x e. ZZ ) -> x e. ZZ )
22 2nn 
 |-  2 e. NN
23 22 a1i 
 |-  ( ( ( ( A e. ZZ /\ P e. ( Prime \ { 2 } ) ) /\ ( A /L P ) = 1 ) /\ x e. ZZ ) -> 2 e. NN )
24 prmdvdsexp 
 |-  ( ( P e. Prime /\ x e. ZZ /\ 2 e. NN ) -> ( P || ( x ^ 2 ) <-> P || x ) )
25 20 21 23 24 syl3anc 
 |-  ( ( ( ( A e. ZZ /\ P e. ( Prime \ { 2 } ) ) /\ ( A /L P ) = 1 ) /\ x e. ZZ ) -> ( P || ( x ^ 2 ) <-> P || x ) )
26 25 biimparc 
 |-  ( ( P || x /\ ( ( ( A e. ZZ /\ P e. ( Prime \ { 2 } ) ) /\ ( A /L P ) = 1 ) /\ x e. ZZ ) ) -> P || ( x ^ 2 ) )
27 bianir 
 |-  ( ( P || ( x ^ 2 ) /\ ( P || A <-> P || ( x ^ 2 ) ) ) -> P || A )
28 5 ad2antlr 
 |-  ( ( ( A e. ZZ /\ P e. ( Prime \ { 2 } ) ) /\ ( A /L P ) = 1 ) -> P e. NN )
29 dvdsmod0 
 |-  ( ( P e. NN /\ P || A ) -> ( A mod P ) = 0 )
30 29 ex 
 |-  ( P e. NN -> ( P || A -> ( A mod P ) = 0 ) )
31 28 30 syl 
 |-  ( ( ( A e. ZZ /\ P e. ( Prime \ { 2 } ) ) /\ ( A /L P ) = 1 ) -> ( P || A -> ( A mod P ) = 0 ) )
32 lgsprme0 
 |-  ( ( A e. ZZ /\ P e. Prime ) -> ( ( A /L P ) = 0 <-> ( A mod P ) = 0 ) )
33 3 32 sylan2 
 |-  ( ( A e. ZZ /\ P e. ( Prime \ { 2 } ) ) -> ( ( A /L P ) = 0 <-> ( A mod P ) = 0 ) )
34 eqeq1 
 |-  ( ( A /L P ) = 0 -> ( ( A /L P ) = 1 <-> 0 = 1 ) )
35 0ne1 
 |-  0 =/= 1
36 eqneqall 
 |-  ( 0 = 1 -> ( 0 =/= 1 -> -. P || x ) )
37 35 36 mpi 
 |-  ( 0 = 1 -> -. P || x )
38 34 37 biimtrdi 
 |-  ( ( A /L P ) = 0 -> ( ( A /L P ) = 1 -> -. P || x ) )
39 33 38 biimtrrdi 
 |-  ( ( A e. ZZ /\ P e. ( Prime \ { 2 } ) ) -> ( ( A mod P ) = 0 -> ( ( A /L P ) = 1 -> -. P || x ) ) )
40 39 com23 
 |-  ( ( A e. ZZ /\ P e. ( Prime \ { 2 } ) ) -> ( ( A /L P ) = 1 -> ( ( A mod P ) = 0 -> -. P || x ) ) )
41 40 imp 
 |-  ( ( ( A e. ZZ /\ P e. ( Prime \ { 2 } ) ) /\ ( A /L P ) = 1 ) -> ( ( A mod P ) = 0 -> -. P || x ) )
42 31 41 syld 
 |-  ( ( ( A e. ZZ /\ P e. ( Prime \ { 2 } ) ) /\ ( A /L P ) = 1 ) -> ( P || A -> -. P || x ) )
43 42 ad2antrl 
 |-  ( ( P || x /\ ( ( ( A e. ZZ /\ P e. ( Prime \ { 2 } ) ) /\ ( A /L P ) = 1 ) /\ x e. ZZ ) ) -> ( P || A -> -. P || x ) )
44 27 43 syl5com 
 |-  ( ( P || ( x ^ 2 ) /\ ( P || A <-> P || ( x ^ 2 ) ) ) -> ( ( P || x /\ ( ( ( A e. ZZ /\ P e. ( Prime \ { 2 } ) ) /\ ( A /L P ) = 1 ) /\ x e. ZZ ) ) -> -. P || x ) )
45 44 ex 
 |-  ( P || ( x ^ 2 ) -> ( ( P || A <-> P || ( x ^ 2 ) ) -> ( ( P || x /\ ( ( ( A e. ZZ /\ P e. ( Prime \ { 2 } ) ) /\ ( A /L P ) = 1 ) /\ x e. ZZ ) ) -> -. P || x ) ) )
46 45 com23 
 |-  ( P || ( x ^ 2 ) -> ( ( P || x /\ ( ( ( A e. ZZ /\ P e. ( Prime \ { 2 } ) ) /\ ( A /L P ) = 1 ) /\ x e. ZZ ) ) -> ( ( P || A <-> P || ( x ^ 2 ) ) -> -. P || x ) ) )
47 26 46 mpcom 
 |-  ( ( P || x /\ ( ( ( A e. ZZ /\ P e. ( Prime \ { 2 } ) ) /\ ( A /L P ) = 1 ) /\ x e. ZZ ) ) -> ( ( P || A <-> P || ( x ^ 2 ) ) -> -. P || x ) )
48 19 47 biimtrid 
 |-  ( ( P || x /\ ( ( ( A e. ZZ /\ P e. ( Prime \ { 2 } ) ) /\ ( A /L P ) = 1 ) /\ x e. ZZ ) ) -> ( ( P || ( x ^ 2 ) <-> P || A ) -> -. P || x ) )
49 18 48 syld 
 |-  ( ( P || x /\ ( ( ( A e. ZZ /\ P e. ( Prime \ { 2 } ) ) /\ ( A /L P ) = 1 ) /\ x e. ZZ ) ) -> ( P || ( ( x ^ 2 ) - A ) -> -. P || x ) )
50 49 ex 
 |-  ( P || x -> ( ( ( ( A e. ZZ /\ P e. ( Prime \ { 2 } ) ) /\ ( A /L P ) = 1 ) /\ x e. ZZ ) -> ( P || ( ( x ^ 2 ) - A ) -> -. P || x ) ) )
51 2a1 
 |-  ( -. P || x -> ( ( ( ( A e. ZZ /\ P e. ( Prime \ { 2 } ) ) /\ ( A /L P ) = 1 ) /\ x e. ZZ ) -> ( P || ( ( x ^ 2 ) - A ) -> -. P || x ) ) )
52 50 51 pm2.61i 
 |-  ( ( ( ( A e. ZZ /\ P e. ( Prime \ { 2 } ) ) /\ ( A /L P ) = 1 ) /\ x e. ZZ ) -> ( P || ( ( x ^ 2 ) - A ) -> -. P || x ) )
53 11 52 sylbid 
 |-  ( ( ( ( A e. ZZ /\ P e. ( Prime \ { 2 } ) ) /\ ( A /L P ) = 1 ) /\ x e. ZZ ) -> ( ( ( x ^ 2 ) mod P ) = ( A mod P ) -> -. P || x ) )
54 53 ancld 
 |-  ( ( ( ( A e. ZZ /\ P e. ( Prime \ { 2 } ) ) /\ ( A /L P ) = 1 ) /\ x e. ZZ ) -> ( ( ( x ^ 2 ) mod P ) = ( A mod P ) -> ( ( ( x ^ 2 ) mod P ) = ( A mod P ) /\ -. P || x ) ) )
55 54 reximdva 
 |-  ( ( ( A e. ZZ /\ P e. ( Prime \ { 2 } ) ) /\ ( A /L P ) = 1 ) -> ( E. x e. ZZ ( ( x ^ 2 ) mod P ) = ( A mod P ) -> E. x e. ZZ ( ( ( x ^ 2 ) mod P ) = ( A mod P ) /\ -. P || x ) ) )
56 2 55 mpd 
 |-  ( ( ( A e. ZZ /\ P e. ( Prime \ { 2 } ) ) /\ ( A /L P ) = 1 ) -> E. x e. ZZ ( ( ( x ^ 2 ) mod P ) = ( A mod P ) /\ -. P || x ) )
57 56 ex 
 |-  ( ( A e. ZZ /\ P e. ( Prime \ { 2 } ) ) -> ( ( A /L P ) = 1 -> E. x e. ZZ ( ( ( x ^ 2 ) mod P ) = ( A mod P ) /\ -. P || x ) ) )