Metamath Proof Explorer


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 ) )