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

Proof

Step	Hyp	Ref	Expression
1		lgsqr	|- ( ( A e. ZZ /\ P e. ( Prime \ { 2 } ) ) -> ( ( A /L P ) = 1 <-> ( -. P || A /\ E. x e. ZZ P || ( ( x ^ 2 ) - A ) ) ) )
2		eldifi	|- ( P e. ( Prime \ { 2 } ) -> P e. Prime )
3		prmnn	|- ( P e. Prime -> P e. NN )
4	2 3	syl	|- ( P e. ( Prime \ { 2 } ) -> P e. NN )
5	4	ad2antlr	|- ( ( ( A e. ZZ /\ P e. ( Prime \ { 2 } ) ) /\ x e. ZZ ) -> P e. NN )
6		zsqcl	|- ( x e. ZZ -> ( x ^ 2 ) e. ZZ )
7	6	adantl	|- ( ( ( A e. ZZ /\ P e. ( Prime \ { 2 } ) ) /\ x e. ZZ ) -> ( x ^ 2 ) e. ZZ )
8		simpll	|- ( ( ( A e. ZZ /\ P e. ( Prime \ { 2 } ) ) /\ x e. ZZ ) -> A e. ZZ )
9		moddvds	|- ( ( P e. NN /\ ( x ^ 2 ) e. ZZ /\ A e. ZZ ) -> ( ( ( x ^ 2 ) mod P ) = ( A mod P ) <-> P || ( ( x ^ 2 ) - A ) ) )
10	5 7 8 9	syl3anc	|- ( ( ( A e. ZZ /\ P e. ( Prime \ { 2 } ) ) /\ x e. ZZ ) -> ( ( ( x ^ 2 ) mod P ) = ( A mod P ) <-> P || ( ( x ^ 2 ) - A ) ) )
11	10	biimprd	|- ( ( ( A e. ZZ /\ P e. ( Prime \ { 2 } ) ) /\ x e. ZZ ) -> ( P || ( ( x ^ 2 ) - A ) -> ( ( x ^ 2 ) mod P ) = ( A mod P ) ) )
12	11	reximdva	|- ( ( A e. ZZ /\ P e. ( Prime \ { 2 } ) ) -> ( E. x e. ZZ P || ( ( x ^ 2 ) - A ) -> E. x e. ZZ ( ( x ^ 2 ) mod P ) = ( A mod P ) ) )
13	12	adantld	|- ( ( A e. ZZ /\ P e. ( Prime \ { 2 } ) ) -> ( ( -. P || A /\ E. x e. ZZ P || ( ( x ^ 2 ) - A ) ) -> E. x e. ZZ ( ( x ^ 2 ) mod P ) = ( A mod P ) ) )
14	1 13	sylbid	|- ( ( A e. ZZ /\ P e. ( Prime \ { 2 } ) ) -> ( ( A /L P ) = 1 -> E. x e. ZZ ( ( x ^ 2 ) mod P ) = ( A mod P ) ) )