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 \in ℤ \land P \in ℙ) \to (A /_{L} P = 0 \leftrightarrow A \mod P = 0)$

Proof

Step	Hyp	Ref	Expression
1		prmz	$⊢ P \in ℙ \to P \in ℤ$
2		lgsne0	$⊢ (A \in ℤ \land P \in ℤ) \to (A /_{L} P \neq 0 \leftrightarrow A \gcd P = 1)$
3	1 2	sylan2	$⊢ (A \in ℤ \land P \in ℙ) \to (A /_{L} P \neq 0 \leftrightarrow A \gcd P = 1)$
4		coprm	$⊢ (P \in ℙ \land A \in ℤ) \to (\neg P ∥ A \leftrightarrow P \gcd A = 1)$
5	4	ancoms	$⊢ (A \in ℤ \land P \in ℙ) \to (\neg P ∥ A \leftrightarrow P \gcd A = 1)$
6	1	anim1i	$⊢ (P \in ℙ \land A \in ℤ) \to (P \in ℤ \land A \in ℤ)$
7	6	ancoms	$⊢ (A \in ℤ \land P \in ℙ) \to (P \in ℤ \land A \in ℤ)$
8		gcdcom	$⊢ (P \in ℤ \land A \in ℤ) \to P \gcd A = A \gcd P$
9	7 8	syl	$⊢ (A \in ℤ \land P \in ℙ) \to P \gcd A = A \gcd P$
10	9	eqeq1d	$⊢ (A \in ℤ \land P \in ℙ) \to (P \gcd A = 1 \leftrightarrow A \gcd P = 1)$
11	5 10	bitr2d	$⊢ (A \in ℤ \land P \in ℙ) \to (A \gcd P = 1 \leftrightarrow \neg P ∥ A)$
12		prmnn	$⊢ P \in ℙ \to P \in ℕ$
13		dvdsval3	$⊢ (P \in ℕ \land A \in ℤ) \to (P ∥ A \leftrightarrow A \mod P = 0)$
14	12 13	sylan	$⊢ (P \in ℙ \land A \in ℤ) \to (P ∥ A \leftrightarrow A \mod P = 0)$
15	14	ancoms	$⊢ (A \in ℤ \land P \in ℙ) \to (P ∥ A \leftrightarrow A \mod P = 0)$
16	15	notbid	$⊢ (A \in ℤ \land P \in ℙ) \to (\neg P ∥ A \leftrightarrow \neg A \mod P = 0)$
17	3 11 16	3bitrd	$⊢ (A \in ℤ \land P \in ℙ) \to (A /_{L} P \neq 0 \leftrightarrow \neg A \mod P = 0)$
18	17	necon4abid	$⊢ (A \in ℤ \land P \in ℙ) \to (A /_{L} P = 0 \leftrightarrow A \mod P = 0)$