Metamath Proof Explorer

Theorem lgsmodeq

Description: The Legendre (Jacobi) symbol is preserved under reduction mod n when n is odd. Theorem 9.9(c) in ApostolNT p. 188. (Contributed by AV, 20-Jul-2021)

		Ref	Expression
	Assertion	lgsmodeq	$⊢ (A \in ℤ \land B \in ℤ \land (N \in ℕ \land \neg 2 ∥ N)) \to (A \mod N = B \mod N \to A /_{L} N = B /_{L} N)$

Proof

Step	Hyp	Ref	Expression
1		3anass	$⊢ (A \in ℤ \land N \in ℕ \land \neg 2 ∥ N) \leftrightarrow (A \in ℤ \land (N \in ℕ \land \neg 2 ∥ N))$
2	1	biimpri	$⊢ (A \in ℤ \land (N \in ℕ \land \neg 2 ∥ N)) \to (A \in ℤ \land N \in ℕ \land \neg 2 ∥ N)$
3	2	3adant2	$⊢ (A \in ℤ \land B \in ℤ \land (N \in ℕ \land \neg 2 ∥ N)) \to (A \in ℤ \land N \in ℕ \land \neg 2 ∥ N)$
4		lgsmod	$⊢ (A \in ℤ \land N \in ℕ \land \neg 2 ∥ N) \to (A \mod N) /_{L} N = A /_{L} N$
5	3 4	syl	$⊢ (A \in ℤ \land B \in ℤ \land (N \in ℕ \land \neg 2 ∥ N)) \to (A \mod N) /_{L} N = A /_{L} N$
6		oveq1	$⊢ A \mod N = B \mod N \to (A \mod N) /_{L} N = (B \mod N) /_{L} N$
7	5 6	sylan9req	$⊢ ((A \in ℤ \land B \in ℤ \land (N \in ℕ \land \neg 2 ∥ N)) \land A \mod N = B \mod N) \to A /_{L} N = (B \mod N) /_{L} N$
8		3anass	$⊢ (B \in ℤ \land N \in ℕ \land \neg 2 ∥ N) \leftrightarrow (B \in ℤ \land (N \in ℕ \land \neg 2 ∥ N))$
9	8	biimpri	$⊢ (B \in ℤ \land (N \in ℕ \land \neg 2 ∥ N)) \to (B \in ℤ \land N \in ℕ \land \neg 2 ∥ N)$
10	9	3adant1	$⊢ (A \in ℤ \land B \in ℤ \land (N \in ℕ \land \neg 2 ∥ N)) \to (B \in ℤ \land N \in ℕ \land \neg 2 ∥ N)$
11		lgsmod	$⊢ (B \in ℤ \land N \in ℕ \land \neg 2 ∥ N) \to (B \mod N) /_{L} N = B /_{L} N$
12	10 11	syl	$⊢ (A \in ℤ \land B \in ℤ \land (N \in ℕ \land \neg 2 ∥ N)) \to (B \mod N) /_{L} N = B /_{L} N$
13	12	adantr	$⊢ ((A \in ℤ \land B \in ℤ \land (N \in ℕ \land \neg 2 ∥ N)) \land A \mod N = B \mod N) \to (B \mod N) /_{L} N = B /_{L} N$
14	7 13	eqtrd	$⊢ ((A \in ℤ \land B \in ℤ \land (N \in ℕ \land \neg 2 ∥ N)) \land A \mod N = B \mod N) \to A /_{L} N = B /_{L} N$
15	14	ex	$⊢ (A \in ℤ \land B \in ℤ \land (N \in ℕ \land \neg 2 ∥ N)) \to (A \mod N = B \mod N \to A /_{L} N = B /_{L} N)$