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	⊢ ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ ( 𝑁 ∈ ℕ ∧ ¬ 2 ∥ 𝑁 ) ) → ( ( 𝐴 mod 𝑁 ) = ( 𝐵 mod 𝑁 ) → ( 𝐴 /L 𝑁 ) = ( 𝐵 /L 𝑁 ) ) )

Proof

Step	Hyp	Ref	Expression
1		3anass	⊢ ( ( 𝐴 ∈ ℤ ∧ 𝑁 ∈ ℕ ∧ ¬ 2 ∥ 𝑁 ) ↔ ( 𝐴 ∈ ℤ ∧ ( 𝑁 ∈ ℕ ∧ ¬ 2 ∥ 𝑁 ) ) )
2	1	biimpri	⊢ ( ( 𝐴 ∈ ℤ ∧ ( 𝑁 ∈ ℕ ∧ ¬ 2 ∥ 𝑁 ) ) → ( 𝐴 ∈ ℤ ∧ 𝑁 ∈ ℕ ∧ ¬ 2 ∥ 𝑁 ) )
3	2	3adant2	⊢ ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ ( 𝑁 ∈ ℕ ∧ ¬ 2 ∥ 𝑁 ) ) → ( 𝐴 ∈ ℤ ∧ 𝑁 ∈ ℕ ∧ ¬ 2 ∥ 𝑁 ) )
4		lgsmod	⊢ ( ( 𝐴 ∈ ℤ ∧ 𝑁 ∈ ℕ ∧ ¬ 2 ∥ 𝑁 ) → ( ( 𝐴 mod 𝑁 ) /L 𝑁 ) = ( 𝐴 /L 𝑁 ) )
5	3 4	syl	⊢ ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ ( 𝑁 ∈ ℕ ∧ ¬ 2 ∥ 𝑁 ) ) → ( ( 𝐴 mod 𝑁 ) /L 𝑁 ) = ( 𝐴 /L 𝑁 ) )
6		oveq1	⊢ ( ( 𝐴 mod 𝑁 ) = ( 𝐵 mod 𝑁 ) → ( ( 𝐴 mod 𝑁 ) /L 𝑁 ) = ( ( 𝐵 mod 𝑁 ) /L 𝑁 ) )
7	5 6	sylan9req	⊢ ( ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ ( 𝑁 ∈ ℕ ∧ ¬ 2 ∥ 𝑁 ) ) ∧ ( 𝐴 mod 𝑁 ) = ( 𝐵 mod 𝑁 ) ) → ( 𝐴 /L 𝑁 ) = ( ( 𝐵 mod 𝑁 ) /L 𝑁 ) )
8		3anass	⊢ ( ( 𝐵 ∈ ℤ ∧ 𝑁 ∈ ℕ ∧ ¬ 2 ∥ 𝑁 ) ↔ ( 𝐵 ∈ ℤ ∧ ( 𝑁 ∈ ℕ ∧ ¬ 2 ∥ 𝑁 ) ) )
9	8	biimpri	⊢ ( ( 𝐵 ∈ ℤ ∧ ( 𝑁 ∈ ℕ ∧ ¬ 2 ∥ 𝑁 ) ) → ( 𝐵 ∈ ℤ ∧ 𝑁 ∈ ℕ ∧ ¬ 2 ∥ 𝑁 ) )
10	9	3adant1	⊢ ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ ( 𝑁 ∈ ℕ ∧ ¬ 2 ∥ 𝑁 ) ) → ( 𝐵 ∈ ℤ ∧ 𝑁 ∈ ℕ ∧ ¬ 2 ∥ 𝑁 ) )
11		lgsmod	⊢ ( ( 𝐵 ∈ ℤ ∧ 𝑁 ∈ ℕ ∧ ¬ 2 ∥ 𝑁 ) → ( ( 𝐵 mod 𝑁 ) /L 𝑁 ) = ( 𝐵 /L 𝑁 ) )
12	10 11	syl	⊢ ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ ( 𝑁 ∈ ℕ ∧ ¬ 2 ∥ 𝑁 ) ) → ( ( 𝐵 mod 𝑁 ) /L 𝑁 ) = ( 𝐵 /L 𝑁 ) )
13	12	adantr	⊢ ( ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ ( 𝑁 ∈ ℕ ∧ ¬ 2 ∥ 𝑁 ) ) ∧ ( 𝐴 mod 𝑁 ) = ( 𝐵 mod 𝑁 ) ) → ( ( 𝐵 mod 𝑁 ) /L 𝑁 ) = ( 𝐵 /L 𝑁 ) )
14	7 13	eqtrd	⊢ ( ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ ( 𝑁 ∈ ℕ ∧ ¬ 2 ∥ 𝑁 ) ) ∧ ( 𝐴 mod 𝑁 ) = ( 𝐵 mod 𝑁 ) ) → ( 𝐴 /L 𝑁 ) = ( 𝐵 /L 𝑁 ) )
15	14	ex	⊢ ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ ( 𝑁 ∈ ℕ ∧ ¬ 2 ∥ 𝑁 ) ) → ( ( 𝐴 mod 𝑁 ) = ( 𝐵 mod 𝑁 ) → ( 𝐴 /L 𝑁 ) = ( 𝐵 /L 𝑁 ) ) )