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 \in ℤ \land A \neq 0) \land (B \in ℤ \land B \neq 0) \land (N \in ℤ \land A \gcd N = 1)) \to A^{2} B /_{L} N = B /_{L} N$

Proof

Step	Hyp	Ref	Expression
1		zsqcl	$⊢ A \in ℤ \to A^{2} \in ℤ$
2	1	adantr	$⊢ (A \in ℤ \land A \neq 0) \to A^{2} \in ℤ$
3		simpl	$⊢ (B \in ℤ \land B \neq 0) \to B \in ℤ$
4		simpl	$⊢ (N \in ℤ \land A \gcd N = 1) \to N \in ℤ$
5	2 3 4	3anim123i	$⊢ ((A \in ℤ \land A \neq 0) \land (B \in ℤ \land B \neq 0) \land (N \in ℤ \land A \gcd N = 1)) \to (A^{2} \in ℤ \land B \in ℤ \land N \in ℤ)$
6		zcn	$⊢ A \in ℤ \to A \in ℂ$
7		sqne0	$⊢ A \in ℂ \to (A^{2} \neq 0 \leftrightarrow A \neq 0)$
8	6 7	syl	$⊢ A \in ℤ \to (A^{2} \neq 0 \leftrightarrow A \neq 0)$
9	8	biimpar	$⊢ (A \in ℤ \land A \neq 0) \to A^{2} \neq 0$
10		simpr	$⊢ (B \in ℤ \land B \neq 0) \to B \neq 0$
11	9 10	anim12i	$⊢ ((A \in ℤ \land A \neq 0) \land (B \in ℤ \land B \neq 0)) \to (A^{2} \neq 0 \land B \neq 0)$
12	11	3adant3	$⊢ ((A \in ℤ \land A \neq 0) \land (B \in ℤ \land B \neq 0) \land (N \in ℤ \land A \gcd N = 1)) \to (A^{2} \neq 0 \land B \neq 0)$
13		lgsdir	$⊢ ((A^{2} \in ℤ \land B \in ℤ \land N \in ℤ) \land (A^{2} \neq 0 \land B \neq 0)) \to A^{2} B /_{L} N = (A^{2} /_{L} N) (B /_{L} N)$
14	5 12 13	syl2anc	$⊢ ((A \in ℤ \land A \neq 0) \land (B \in ℤ \land B \neq 0) \land (N \in ℤ \land A \gcd N = 1)) \to A^{2} B /_{L} N = (A^{2} /_{L} N) (B /_{L} N)$
15		3anass	$⊢ ((A \in ℤ \land A \neq 0) \land N \in ℤ \land A \gcd N = 1) \leftrightarrow ((A \in ℤ \land A \neq 0) \land (N \in ℤ \land A \gcd N = 1))$
16	15	biimpri	$⊢ ((A \in ℤ \land A \neq 0) \land (N \in ℤ \land A \gcd N = 1)) \to ((A \in ℤ \land A \neq 0) \land N \in ℤ \land A \gcd N = 1)$
17	16	3adant2	$⊢ ((A \in ℤ \land A \neq 0) \land (B \in ℤ \land B \neq 0) \land (N \in ℤ \land A \gcd N = 1)) \to ((A \in ℤ \land A \neq 0) \land N \in ℤ \land A \gcd N = 1)$
18		lgssq	$⊢ ((A \in ℤ \land A \neq 0) \land N \in ℤ \land A \gcd N = 1) \to A^{2} /_{L} N = 1$
19	17 18	syl	$⊢ ((A \in ℤ \land A \neq 0) \land (B \in ℤ \land B \neq 0) \land (N \in ℤ \land A \gcd N = 1)) \to A^{2} /_{L} N = 1$
20	19	oveq1d	$⊢ ((A \in ℤ \land A \neq 0) \land (B \in ℤ \land B \neq 0) \land (N \in ℤ \land A \gcd N = 1)) \to (A^{2} /_{L} N) (B /_{L} N) = 1 (B /_{L} N)$
21	3 4	anim12i	$⊢ ((B \in ℤ \land B \neq 0) \land (N \in ℤ \land A \gcd N = 1)) \to (B \in ℤ \land N \in ℤ)$
22	21	3adant1	$⊢ ((A \in ℤ \land A \neq 0) \land (B \in ℤ \land B \neq 0) \land (N \in ℤ \land A \gcd N = 1)) \to (B \in ℤ \land N \in ℤ)$
23		lgscl	$⊢ (B \in ℤ \land N \in ℤ) \to B /_{L} N \in ℤ$
24	22 23	syl	$⊢ ((A \in ℤ \land A \neq 0) \land (B \in ℤ \land B \neq 0) \land (N \in ℤ \land A \gcd N = 1)) \to B /_{L} N \in ℤ$
25	24	zcnd	$⊢ ((A \in ℤ \land A \neq 0) \land (B \in ℤ \land B \neq 0) \land (N \in ℤ \land A \gcd N = 1)) \to B /_{L} N \in ℂ$
26	25	mulid2d	$⊢ ((A \in ℤ \land A \neq 0) \land (B \in ℤ \land B \neq 0) \land (N \in ℤ \land A \gcd N = 1)) \to 1 (B /_{L} N) = B /_{L} N$
27	14 20 26	3eqtrd	$⊢ ((A \in ℤ \land A \neq 0) \land (B \in ℤ \land B \neq 0) \land (N \in ℤ \land A \gcd N = 1)) \to A^{2} B /_{L} N = B /_{L} N$

Metamath Proof Explorer

Theorem lgsmulsqcoprm

Proof