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 ) ) )