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 ∈ ℤ ∧ B ∈ ℤ ∧ N ∈ ℕ ∧ ¬ 2 ∥ N → A mod N = B mod N → A / L N = B / L N

Proof

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