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 ( ( ( 𝐴 ∈ ℤ ∧ 𝐴 ≠ 0 ) ∧ ( 𝐵 ∈ ℤ ∧ 𝐵 ≠ 0 ) ∧ ( 𝑁 ∈ ℤ ∧ ( 𝐴 gcd 𝑁 ) = 1 ) ) → ( ( ( 𝐴 ↑ 2 ) · 𝐵 ) /L 𝑁 ) = ( 𝐵 /L 𝑁 ) )

Proof

Step Hyp Ref Expression
1 zsqcl ⊢ ( 𝐴 ∈ ℤ → ( 𝐴 ↑ 2 ) ∈ ℤ )
2 1 adantr ⊢ ( ( 𝐴 ∈ ℤ ∧ 𝐴 ≠ 0 ) → ( 𝐴 ↑ 2 ) ∈ ℤ )
3 simpl ⊢ ( ( 𝐵 ∈ ℤ ∧ 𝐵 ≠ 0 ) → 𝐵 ∈ ℤ )
4 simpl ⊢ ( ( 𝑁 ∈ ℤ ∧ ( 𝐴 gcd 𝑁 ) = 1 ) → 𝑁 ∈ ℤ )
5 2 3 4 3anim123i ⊢ ( ( ( 𝐴 ∈ ℤ ∧ 𝐴 ≠ 0 ) ∧ ( 𝐵 ∈ ℤ ∧ 𝐵 ≠ 0 ) ∧ ( 𝑁 ∈ ℤ ∧ ( 𝐴 gcd 𝑁 ) = 1 ) ) → ( ( 𝐴 ↑ 2 ) ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝑁 ∈ ℤ ) )
6 zcn ⊢ ( 𝐴 ∈ ℤ → 𝐴 ∈ ℂ )
7 sqne0 ⊢ ( 𝐴 ∈ ℂ → ( ( 𝐴 ↑ 2 ) ≠ 0 ↔ 𝐴 ≠ 0 ) )
8 6 7 syl ⊢ ( 𝐴 ∈ ℤ → ( ( 𝐴 ↑ 2 ) ≠ 0 ↔ 𝐴 ≠ 0 ) )
9 8 biimpar ⊢ ( ( 𝐴 ∈ ℤ ∧ 𝐴 ≠ 0 ) → ( 𝐴 ↑ 2 ) ≠ 0 )
10 simpr ⊢ ( ( 𝐵 ∈ ℤ ∧ 𝐵 ≠ 0 ) → 𝐵 ≠ 0 )
11 9 10 anim12i ⊢ ( ( ( 𝐴 ∈ ℤ ∧ 𝐴 ≠ 0 ) ∧ ( 𝐵 ∈ ℤ ∧ 𝐵 ≠ 0 ) ) → ( ( 𝐴 ↑ 2 ) ≠ 0 ∧ 𝐵 ≠ 0 ) )
12 11 3adant3 ⊢ ( ( ( 𝐴 ∈ ℤ ∧ 𝐴 ≠ 0 ) ∧ ( 𝐵 ∈ ℤ ∧ 𝐵 ≠ 0 ) ∧ ( 𝑁 ∈ ℤ ∧ ( 𝐴 gcd 𝑁 ) = 1 ) ) → ( ( 𝐴 ↑ 2 ) ≠ 0 ∧ 𝐵 ≠ 0 ) )
13 lgsdir ⊢ ( ( ( ( 𝐴 ↑ 2 ) ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ∧ ( ( 𝐴 ↑ 2 ) ≠ 0 ∧ 𝐵 ≠ 0 ) ) → ( ( ( 𝐴 ↑ 2 ) · 𝐵 ) /L 𝑁 ) = ( ( ( 𝐴 ↑ 2 ) /L 𝑁 ) · ( 𝐵 /L 𝑁 ) ) )
14 5 12 13 syl2anc ⊢ ( ( ( 𝐴 ∈ ℤ ∧ 𝐴 ≠ 0 ) ∧ ( 𝐵 ∈ ℤ ∧ 𝐵 ≠ 0 ) ∧ ( 𝑁 ∈ ℤ ∧ ( 𝐴 gcd 𝑁 ) = 1 ) ) → ( ( ( 𝐴 ↑ 2 ) · 𝐵 ) /L 𝑁 ) = ( ( ( 𝐴 ↑ 2 ) /L 𝑁 ) · ( 𝐵 /L 𝑁 ) ) )
15 3anass ⊢ ( ( ( 𝐴 ∈ ℤ ∧ 𝐴 ≠ 0 ) ∧ 𝑁 ∈ ℤ ∧ ( 𝐴 gcd 𝑁 ) = 1 ) ↔ ( ( 𝐴 ∈ ℤ ∧ 𝐴 ≠ 0 ) ∧ ( 𝑁 ∈ ℤ ∧ ( 𝐴 gcd 𝑁 ) = 1 ) ) )
16 15 biimpri ⊢ ( ( ( 𝐴 ∈ ℤ ∧ 𝐴 ≠ 0 ) ∧ ( 𝑁 ∈ ℤ ∧ ( 𝐴 gcd 𝑁 ) = 1 ) ) → ( ( 𝐴 ∈ ℤ ∧ 𝐴 ≠ 0 ) ∧ 𝑁 ∈ ℤ ∧ ( 𝐴 gcd 𝑁 ) = 1 ) )
17 16 3adant2 ⊢ ( ( ( 𝐴 ∈ ℤ ∧ 𝐴 ≠ 0 ) ∧ ( 𝐵 ∈ ℤ ∧ 𝐵 ≠ 0 ) ∧ ( 𝑁 ∈ ℤ ∧ ( 𝐴 gcd 𝑁 ) = 1 ) ) → ( ( 𝐴 ∈ ℤ ∧ 𝐴 ≠ 0 ) ∧ 𝑁 ∈ ℤ ∧ ( 𝐴 gcd 𝑁 ) = 1 ) )
18 lgssq ⊢ ( ( ( 𝐴 ∈ ℤ ∧ 𝐴 ≠ 0 ) ∧ 𝑁 ∈ ℤ ∧ ( 𝐴 gcd 𝑁 ) = 1 ) → ( ( 𝐴 ↑ 2 ) /L 𝑁 ) = 1 )
19 17 18 syl ⊢ ( ( ( 𝐴 ∈ ℤ ∧ 𝐴 ≠ 0 ) ∧ ( 𝐵 ∈ ℤ ∧ 𝐵 ≠ 0 ) ∧ ( 𝑁 ∈ ℤ ∧ ( 𝐴 gcd 𝑁 ) = 1 ) ) → ( ( 𝐴 ↑ 2 ) /L 𝑁 ) = 1 )
20 19 oveq1d ⊢ ( ( ( 𝐴 ∈ ℤ ∧ 𝐴 ≠ 0 ) ∧ ( 𝐵 ∈ ℤ ∧ 𝐵 ≠ 0 ) ∧ ( 𝑁 ∈ ℤ ∧ ( 𝐴 gcd 𝑁 ) = 1 ) ) → ( ( ( 𝐴 ↑ 2 ) /L 𝑁 ) · ( 𝐵 /L 𝑁 ) ) = ( 1 · ( 𝐵 /L 𝑁 ) ) )
21 3 4 anim12i ⊢ ( ( ( 𝐵 ∈ ℤ ∧ 𝐵 ≠ 0 ) ∧ ( 𝑁 ∈ ℤ ∧ ( 𝐴 gcd 𝑁 ) = 1 ) ) → ( 𝐵 ∈ ℤ ∧ 𝑁 ∈ ℤ ) )
22 21 3adant1 ⊢ ( ( ( 𝐴 ∈ ℤ ∧ 𝐴 ≠ 0 ) ∧ ( 𝐵 ∈ ℤ ∧ 𝐵 ≠ 0 ) ∧ ( 𝑁 ∈ ℤ ∧ ( 𝐴 gcd 𝑁 ) = 1 ) ) → ( 𝐵 ∈ ℤ ∧ 𝑁 ∈ ℤ ) )
23 lgscl ⊢ ( ( 𝐵 ∈ ℤ ∧ 𝑁 ∈ ℤ ) → ( 𝐵 /L 𝑁 ) ∈ ℤ )
24 22 23 syl ⊢ ( ( ( 𝐴 ∈ ℤ ∧ 𝐴 ≠ 0 ) ∧ ( 𝐵 ∈ ℤ ∧ 𝐵 ≠ 0 ) ∧ ( 𝑁 ∈ ℤ ∧ ( 𝐴 gcd 𝑁 ) = 1 ) ) → ( 𝐵 /L 𝑁 ) ∈ ℤ )
25 24 zcnd ⊢ ( ( ( 𝐴 ∈ ℤ ∧ 𝐴 ≠ 0 ) ∧ ( 𝐵 ∈ ℤ ∧ 𝐵 ≠ 0 ) ∧ ( 𝑁 ∈ ℤ ∧ ( 𝐴 gcd 𝑁 ) = 1 ) ) → ( 𝐵 /L 𝑁 ) ∈ ℂ )
26 25 mulid2d ⊢ ( ( ( 𝐴 ∈ ℤ ∧ 𝐴 ≠ 0 ) ∧ ( 𝐵 ∈ ℤ ∧ 𝐵 ≠ 0 ) ∧ ( 𝑁 ∈ ℤ ∧ ( 𝐴 gcd 𝑁 ) = 1 ) ) → ( 1 · ( 𝐵 /L 𝑁 ) ) = ( 𝐵 /L 𝑁 ) )
27 14 20 26 3eqtrd ⊢ ( ( ( 𝐴 ∈ ℤ ∧ 𝐴 ≠ 0 ) ∧ ( 𝐵 ∈ ℤ ∧ 𝐵 ≠ 0 ) ∧ ( 𝑁 ∈ ℤ ∧ ( 𝐴 gcd 𝑁 ) = 1 ) ) → ( ( ( 𝐴 ↑ 2 ) · 𝐵 ) /L 𝑁 ) = ( 𝐵 /L 𝑁 ) )