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	⊢ ( ( 𝐴 ∈ ℤ ∧ 𝑃 ∈ ℙ ) → ( ( 𝐴 /L 𝑃 ) = 0 ↔ ( 𝐴 mod 𝑃 ) = 0 ) )

Proof

Step	Hyp	Ref	Expression
1		prmz	⊢ ( 𝑃 ∈ ℙ → 𝑃 ∈ ℤ )
2		lgsne0	⊢ ( ( 𝐴 ∈ ℤ ∧ 𝑃 ∈ ℤ ) → ( ( 𝐴 /L 𝑃 ) ≠ 0 ↔ ( 𝐴 gcd 𝑃 ) = 1 ) )
3	1 2	sylan2	⊢ ( ( 𝐴 ∈ ℤ ∧ 𝑃 ∈ ℙ ) → ( ( 𝐴 /L 𝑃 ) ≠ 0 ↔ ( 𝐴 gcd 𝑃 ) = 1 ) )
4		coprm	⊢ ( ( 𝑃 ∈ ℙ ∧ 𝐴 ∈ ℤ ) → ( ¬ 𝑃 ∥ 𝐴 ↔ ( 𝑃 gcd 𝐴 ) = 1 ) )
5	4	ancoms	⊢ ( ( 𝐴 ∈ ℤ ∧ 𝑃 ∈ ℙ ) → ( ¬ 𝑃 ∥ 𝐴 ↔ ( 𝑃 gcd 𝐴 ) = 1 ) )
6	1	anim1i	⊢ ( ( 𝑃 ∈ ℙ ∧ 𝐴 ∈ ℤ ) → ( 𝑃 ∈ ℤ ∧ 𝐴 ∈ ℤ ) )
7	6	ancoms	⊢ ( ( 𝐴 ∈ ℤ ∧ 𝑃 ∈ ℙ ) → ( 𝑃 ∈ ℤ ∧ 𝐴 ∈ ℤ ) )
8		gcdcom	⊢ ( ( 𝑃 ∈ ℤ ∧ 𝐴 ∈ ℤ ) → ( 𝑃 gcd 𝐴 ) = ( 𝐴 gcd 𝑃 ) )
9	7 8	syl	⊢ ( ( 𝐴 ∈ ℤ ∧ 𝑃 ∈ ℙ ) → ( 𝑃 gcd 𝐴 ) = ( 𝐴 gcd 𝑃 ) )
10	9	eqeq1d	⊢ ( ( 𝐴 ∈ ℤ ∧ 𝑃 ∈ ℙ ) → ( ( 𝑃 gcd 𝐴 ) = 1 ↔ ( 𝐴 gcd 𝑃 ) = 1 ) )
11	5 10	bitr2d	⊢ ( ( 𝐴 ∈ ℤ ∧ 𝑃 ∈ ℙ ) → ( ( 𝐴 gcd 𝑃 ) = 1 ↔ ¬ 𝑃 ∥ 𝐴 ) )
12		prmnn	⊢ ( 𝑃 ∈ ℙ → 𝑃 ∈ ℕ )
13		dvdsval3	⊢ ( ( 𝑃 ∈ ℕ ∧ 𝐴 ∈ ℤ ) → ( 𝑃 ∥ 𝐴 ↔ ( 𝐴 mod 𝑃 ) = 0 ) )
14	12 13	sylan	⊢ ( ( 𝑃 ∈ ℙ ∧ 𝐴 ∈ ℤ ) → ( 𝑃 ∥ 𝐴 ↔ ( 𝐴 mod 𝑃 ) = 0 ) )
15	14	ancoms	⊢ ( ( 𝐴 ∈ ℤ ∧ 𝑃 ∈ ℙ ) → ( 𝑃 ∥ 𝐴 ↔ ( 𝐴 mod 𝑃 ) = 0 ) )
16	15	notbid	⊢ ( ( 𝐴 ∈ ℤ ∧ 𝑃 ∈ ℙ ) → ( ¬ 𝑃 ∥ 𝐴 ↔ ¬ ( 𝐴 mod 𝑃 ) = 0 ) )
17	3 11 16	3bitrd	⊢ ( ( 𝐴 ∈ ℤ ∧ 𝑃 ∈ ℙ ) → ( ( 𝐴 /L 𝑃 ) ≠ 0 ↔ ¬ ( 𝐴 mod 𝑃 ) = 0 ) )
18	17	necon4abid	⊢ ( ( 𝐴 ∈ ℤ ∧ 𝑃 ∈ ℙ ) → ( ( 𝐴 /L 𝑃 ) = 0 ↔ ( 𝐴 mod 𝑃 ) = 0 ) )