Metamath Proof Explorer

Theorem lgsmulsqcoprm

Description: The Legendre (Jacobi) symbol is preserved under multiplication with a square of an integer coprime to the second argument. Theorem 9.9(d) in ApostolNT p. 188. (Contributed by AV, 20-Jul-2021)

Ref Expression
Assertion lgsmulsqcoprm 
|- ( ( ( A e. ZZ /\ A =/= 0 ) /\ ( B e. ZZ /\ B =/= 0 ) /\ ( N e. ZZ /\ ( A gcd N ) = 1 ) ) -> ( ( ( A ^ 2 ) x. B ) /L N ) = ( B /L N ) )

Proof

Step Hyp Ref Expression
1 zsqcl 
 |-  ( A e. ZZ -> ( A ^ 2 ) e. ZZ )
2 1 adantr 
 |-  ( ( A e. ZZ /\ A =/= 0 ) -> ( A ^ 2 ) e. ZZ )
3 simpl 
 |-  ( ( B e. ZZ /\ B =/= 0 ) -> B e. ZZ )
4 simpl 
 |-  ( ( N e. ZZ /\ ( A gcd N ) = 1 ) -> N e. ZZ )
5 2 3 4 3anim123i 
 |-  ( ( ( A e. ZZ /\ A =/= 0 ) /\ ( B e. ZZ /\ B =/= 0 ) /\ ( N e. ZZ /\ ( A gcd N ) = 1 ) ) -> ( ( A ^ 2 ) e. ZZ /\ B e. ZZ /\ N e. ZZ ) )
6 zcn 
 |-  ( A e. ZZ -> A e. CC )
7 sqne0 
 |-  ( A e. CC -> ( ( A ^ 2 ) =/= 0 <-> A =/= 0 ) )
8 6 7 syl 
 |-  ( A e. ZZ -> ( ( A ^ 2 ) =/= 0 <-> A =/= 0 ) )
9 8 biimpar 
 |-  ( ( A e. ZZ /\ A =/= 0 ) -> ( A ^ 2 ) =/= 0 )
10 simpr 
 |-  ( ( B e. ZZ /\ B =/= 0 ) -> B =/= 0 )
11 9 10 anim12i 
 |-  ( ( ( A e. ZZ /\ A =/= 0 ) /\ ( B e. ZZ /\ B =/= 0 ) ) -> ( ( A ^ 2 ) =/= 0 /\ B =/= 0 ) )
12 11 3adant3 
 |-  ( ( ( A e. ZZ /\ A =/= 0 ) /\ ( B e. ZZ /\ B =/= 0 ) /\ ( N e. ZZ /\ ( A gcd N ) = 1 ) ) -> ( ( A ^ 2 ) =/= 0 /\ B =/= 0 ) )
13 lgsdir 
 |-  ( ( ( ( A ^ 2 ) e. ZZ /\ B e. ZZ /\ N e. ZZ ) /\ ( ( A ^ 2 ) =/= 0 /\ B =/= 0 ) ) -> ( ( ( A ^ 2 ) x. B ) /L N ) = ( ( ( A ^ 2 ) /L N ) x. ( B /L N ) ) )
14 5 12 13 syl2anc 
 |-  ( ( ( A e. ZZ /\ A =/= 0 ) /\ ( B e. ZZ /\ B =/= 0 ) /\ ( N e. ZZ /\ ( A gcd N ) = 1 ) ) -> ( ( ( A ^ 2 ) x. B ) /L N ) = ( ( ( A ^ 2 ) /L N ) x. ( B /L N ) ) )
15 3anass 
 |-  ( ( ( A e. ZZ /\ A =/= 0 ) /\ N e. ZZ /\ ( A gcd N ) = 1 ) <-> ( ( A e. ZZ /\ A =/= 0 ) /\ ( N e. ZZ /\ ( A gcd N ) = 1 ) ) )
16 15 biimpri 
 |-  ( ( ( A e. ZZ /\ A =/= 0 ) /\ ( N e. ZZ /\ ( A gcd N ) = 1 ) ) -> ( ( A e. ZZ /\ A =/= 0 ) /\ N e. ZZ /\ ( A gcd N ) = 1 ) )
17 16 3adant2 
 |-  ( ( ( A e. ZZ /\ A =/= 0 ) /\ ( B e. ZZ /\ B =/= 0 ) /\ ( N e. ZZ /\ ( A gcd N ) = 1 ) ) -> ( ( A e. ZZ /\ A =/= 0 ) /\ N e. ZZ /\ ( A gcd N ) = 1 ) )
18 lgssq 
 |-  ( ( ( A e. ZZ /\ A =/= 0 ) /\ N e. ZZ /\ ( A gcd N ) = 1 ) -> ( ( A ^ 2 ) /L N ) = 1 )
19 17 18 syl 
 |-  ( ( ( A e. ZZ /\ A =/= 0 ) /\ ( B e. ZZ /\ B =/= 0 ) /\ ( N e. ZZ /\ ( A gcd N ) = 1 ) ) -> ( ( A ^ 2 ) /L N ) = 1 )
20 19 oveq1d 
 |-  ( ( ( A e. ZZ /\ A =/= 0 ) /\ ( B e. ZZ /\ B =/= 0 ) /\ ( N e. ZZ /\ ( A gcd N ) = 1 ) ) -> ( ( ( A ^ 2 ) /L N ) x. ( B /L N ) ) = ( 1 x. ( B /L N ) ) )
21 3 4 anim12i 
 |-  ( ( ( B e. ZZ /\ B =/= 0 ) /\ ( N e. ZZ /\ ( A gcd N ) = 1 ) ) -> ( B e. ZZ /\ N e. ZZ ) )
22 21 3adant1 
 |-  ( ( ( A e. ZZ /\ A =/= 0 ) /\ ( B e. ZZ /\ B =/= 0 ) /\ ( N e. ZZ /\ ( A gcd N ) = 1 ) ) -> ( B e. ZZ /\ N e. ZZ ) )
23 lgscl 
 |-  ( ( B e. ZZ /\ N e. ZZ ) -> ( B /L N ) e. ZZ )
24 22 23 syl 
 |-  ( ( ( A e. ZZ /\ A =/= 0 ) /\ ( B e. ZZ /\ B =/= 0 ) /\ ( N e. ZZ /\ ( A gcd N ) = 1 ) ) -> ( B /L N ) e. ZZ )
25 24 zcnd 
 |-  ( ( ( A e. ZZ /\ A =/= 0 ) /\ ( B e. ZZ /\ B =/= 0 ) /\ ( N e. ZZ /\ ( A gcd N ) = 1 ) ) -> ( B /L N ) e. CC )
26 25 mulid2d 
 |-  ( ( ( A e. ZZ /\ A =/= 0 ) /\ ( B e. ZZ /\ B =/= 0 ) /\ ( N e. ZZ /\ ( A gcd N ) = 1 ) ) -> ( 1 x. ( B /L N ) ) = ( B /L N ) )
27 14 20 26 3eqtrd 
 |-  ( ( ( A e. ZZ /\ A =/= 0 ) /\ ( B e. ZZ /\ B =/= 0 ) /\ ( N e. ZZ /\ ( A gcd N ) = 1 ) ) -> ( ( ( A ^ 2 ) x. B ) /L N ) = ( B /L N ) )