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 e. ZZ /\ B e. ZZ /\ ( N e. NN /\ -. 2 || N ) ) -> ( ( A mod N ) = ( B mod N ) -> ( A /L N ) = ( B /L N ) ) )

Proof

Step Hyp Ref Expression
1 3anass
 |-  ( ( A e. ZZ /\ N e. NN /\ -. 2 || N ) <-> ( A e. ZZ /\ ( N e. NN /\ -. 2 || N ) ) )
2 1 biimpri
 |-  ( ( A e. ZZ /\ ( N e. NN /\ -. 2 || N ) ) -> ( A e. ZZ /\ N e. NN /\ -. 2 || N ) )
3 2 3adant2
 |-  ( ( A e. ZZ /\ B e. ZZ /\ ( N e. NN /\ -. 2 || N ) ) -> ( A e. ZZ /\ N e. NN /\ -. 2 || N ) )
4 lgsmod
 |-  ( ( A e. ZZ /\ N e. NN /\ -. 2 || N ) -> ( ( A mod N ) /L N ) = ( A /L N ) )
5 3 4 syl
 |-  ( ( A e. ZZ /\ B e. ZZ /\ ( N e. NN /\ -. 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 e. ZZ /\ B e. ZZ /\ ( N e. NN /\ -. 2 || N ) ) /\ ( A mod N ) = ( B mod N ) ) -> ( A /L N ) = ( ( B mod N ) /L N ) )
8 3anass
 |-  ( ( B e. ZZ /\ N e. NN /\ -. 2 || N ) <-> ( B e. ZZ /\ ( N e. NN /\ -. 2 || N ) ) )
9 8 biimpri
 |-  ( ( B e. ZZ /\ ( N e. NN /\ -. 2 || N ) ) -> ( B e. ZZ /\ N e. NN /\ -. 2 || N ) )
10 9 3adant1
 |-  ( ( A e. ZZ /\ B e. ZZ /\ ( N e. NN /\ -. 2 || N ) ) -> ( B e. ZZ /\ N e. NN /\ -. 2 || N ) )
11 lgsmod
 |-  ( ( B e. ZZ /\ N e. NN /\ -. 2 || N ) -> ( ( B mod N ) /L N ) = ( B /L N ) )
12 10 11 syl
 |-  ( ( A e. ZZ /\ B e. ZZ /\ ( N e. NN /\ -. 2 || N ) ) -> ( ( B mod N ) /L N ) = ( B /L N ) )
13 12 adantr
 |-  ( ( ( A e. ZZ /\ B e. ZZ /\ ( N e. NN /\ -. 2 || N ) ) /\ ( A mod N ) = ( B mod N ) ) -> ( ( B mod N ) /L N ) = ( B /L N ) )
14 7 13 eqtrd
 |-  ( ( ( A e. ZZ /\ B e. ZZ /\ ( N e. NN /\ -. 2 || N ) ) /\ ( A mod N ) = ( B mod N ) ) -> ( A /L N ) = ( B /L N ) )
15 14 ex
 |-  ( ( A e. ZZ /\ B e. ZZ /\ ( N e. NN /\ -. 2 || N ) ) -> ( ( A mod N ) = ( B mod N ) -> ( A /L N ) = ( B /L N ) ) )