Theorem lgsprme0

Description: The Legendre symbol at any prime (even at 2) is 0 iff the prime does not divide the first argument. See definition in ApostolNT p. 179. (Contributed by AV, 20-Jul-2021)

	Ref	Expression
Assertion	lgsprme0	|- ( ( A e. ZZ /\ P e. Prime ) -> ( ( A /L P ) = 0 <-> ( A mod P ) = 0 ) )

Proof

Step	Hyp	Ref	Expression
1		prmz	|- ( P e. Prime -> P e. ZZ )
2		lgsne0	|- ( ( A e. ZZ /\ P e. ZZ ) -> ( ( A /L P ) =/= 0 <-> ( A gcd P ) = 1 ) )
3	1 2	sylan2	|- ( ( A e. ZZ /\ P e. Prime ) -> ( ( A /L P ) =/= 0 <-> ( A gcd P ) = 1 ) )
4		coprm	|- ( ( P e. Prime /\ A e. ZZ ) -> ( -. P || A <-> ( P gcd A ) = 1 ) )
5	4	ancoms	|- ( ( A e. ZZ /\ P e. Prime ) -> ( -. P || A <-> ( P gcd A ) = 1 ) )
6	1	anim1i	|- ( ( P e. Prime /\ A e. ZZ ) -> ( P e. ZZ /\ A e. ZZ ) )
7	6	ancoms	|- ( ( A e. ZZ /\ P e. Prime ) -> ( P e. ZZ /\ A e. ZZ ) )
8		gcdcom	|- ( ( P e. ZZ /\ A e. ZZ ) -> ( P gcd A ) = ( A gcd P ) )
9	7 8	syl	|- ( ( A e. ZZ /\ P e. Prime ) -> ( P gcd A ) = ( A gcd P ) )
10	9	eqeq1d	|- ( ( A e. ZZ /\ P e. Prime ) -> ( ( P gcd A ) = 1 <-> ( A gcd P ) = 1 ) )
11	5 10	bitr2d	|- ( ( A e. ZZ /\ P e. Prime ) -> ( ( A gcd P ) = 1 <-> -. P || A ) )
12		prmnn	|- ( P e. Prime -> P e. NN )
13		dvdsval3	|- ( ( P e. NN /\ A e. ZZ ) -> ( P || A <-> ( A mod P ) = 0 ) )
14	12 13	sylan	|- ( ( P e. Prime /\ A e. ZZ ) -> ( P || A <-> ( A mod P ) = 0 ) )
15	14	ancoms	|- ( ( A e. ZZ /\ P e. Prime ) -> ( P || A <-> ( A mod P ) = 0 ) )
16	15	notbid	|- ( ( A e. ZZ /\ P e. Prime ) -> ( -. P || A <-> -. ( A mod P ) = 0 ) )
17	3 11 16	3bitrd	|- ( ( A e. ZZ /\ P e. Prime ) -> ( ( A /L P ) =/= 0 <-> -. ( A mod P ) = 0 ) )
18	17	necon4abid	|- ( ( A e. ZZ /\ P e. Prime ) -> ( ( A /L P ) = 0 <-> ( A mod P ) = 0 ) )