lgssq

Description: The Legendre symbol at a square is equal to 1 . Together with lgsmod this implies that the Legendre symbol takes value 1 at every quadratic residue. (Contributed by Mario Carneiro, 5-Feb-2015) (Revised by AV, 20-Jul-2021)

		Ref	Expression
	Assertion	lgssq	$⊢ ((A \in ℤ \land A \neq 0) \land N \in ℤ \land A \gcd N = 1) \to A^{2} /_{L} N = 1$

Proof

Step	Hyp	Ref	Expression
1		simp1l	$⊢ ((A \in ℤ \land A \neq 0) \land N \in ℤ \land A \gcd N = 1) \to A \in ℤ$
2		simp2	$⊢ ((A \in ℤ \land A \neq 0) \land N \in ℤ \land A \gcd N = 1) \to N \in ℤ$
3		simp1r	$⊢ ((A \in ℤ \land A \neq 0) \land N \in ℤ \land A \gcd N = 1) \to A \neq 0$
4		lgsdir	$⊢ ((A \in ℤ \land A \in ℤ \land N \in ℤ) \land (A \neq 0 \land A \neq 0)) \to A A /_{L} N = (A /_{L} N) (A /_{L} N)$
5	1 1 2 3 3 4	syl32anc	$⊢ ((A \in ℤ \land A \neq 0) \land N \in ℤ \land A \gcd N = 1) \to A A /_{L} N = (A /_{L} N) (A /_{L} N)$
6		zcn	$⊢ A \in ℤ \to A \in ℂ$
7	6	adantr	$⊢ (A \in ℤ \land A \neq 0) \to A \in ℂ$
8	7	3ad2ant1	$⊢ ((A \in ℤ \land A \neq 0) \land N \in ℤ \land A \gcd N = 1) \to A \in ℂ$
9	8	sqvald	$⊢ ((A \in ℤ \land A \neq 0) \land N \in ℤ \land A \gcd N = 1) \to A^{2} = A A$
10	9	oveq1d	$⊢ ((A \in ℤ \land A \neq 0) \land N \in ℤ \land A \gcd N = 1) \to A^{2} /_{L} N = A A /_{L} N$
11		lgscl	$⊢ (A \in ℤ \land N \in ℤ) \to A /_{L} N \in ℤ$
12	1 2 11	syl2anc	$⊢ ((A \in ℤ \land A \neq 0) \land N \in ℤ \land A \gcd N = 1) \to A /_{L} N \in ℤ$
13	12	zred	$⊢ ((A \in ℤ \land A \neq 0) \land N \in ℤ \land A \gcd N = 1) \to A /_{L} N \in ℝ$
14		absresq	$⊢ A /_{L} N \in ℝ \to {\|A /_{L} N\|}^{2} = {(A /_{L} N)}^{2}$
15	13 14	syl	$⊢ ((A \in ℤ \land A \neq 0) \land N \in ℤ \land A \gcd N = 1) \to {\|A /_{L} N\|}^{2} = {(A /_{L} N)}^{2}$
16		lgsabs1	$⊢ (A \in ℤ \land N \in ℤ) \to (\|A /_{L} N\| = 1 \leftrightarrow A \gcd N = 1)$
17	16	adantlr	$⊢ ((A \in ℤ \land A \neq 0) \land N \in ℤ) \to (\|A /_{L} N\| = 1 \leftrightarrow A \gcd N = 1)$
18	17	biimp3ar	$⊢ ((A \in ℤ \land A \neq 0) \land N \in ℤ \land A \gcd N = 1) \to \|A /_{L} N\| = 1$
19	18	oveq1d	$⊢ ((A \in ℤ \land A \neq 0) \land N \in ℤ \land A \gcd N = 1) \to {\|A /_{L} N\|}^{2} = 1^{2}$
20		sq1	$⊢ 1^{2} = 1$
21	19 20	eqtrdi	$⊢ ((A \in ℤ \land A \neq 0) \land N \in ℤ \land A \gcd N = 1) \to {\|A /_{L} N\|}^{2} = 1$
22	12	zcnd	$⊢ ((A \in ℤ \land A \neq 0) \land N \in ℤ \land A \gcd N = 1) \to A /_{L} N \in ℂ$
23	22	sqvald	$⊢ ((A \in ℤ \land A \neq 0) \land N \in ℤ \land A \gcd N = 1) \to {(A /_{L} N)}^{2} = (A /_{L} N) (A /_{L} N)$
24	15 21 23	3eqtr3d	$⊢ ((A \in ℤ \land A \neq 0) \land N \in ℤ \land A \gcd N = 1) \to 1 = (A /_{L} N) (A /_{L} N)$
25	5 10 24	3eqtr4d	$⊢ ((A \in ℤ \land A \neq 0) \land N \in ℤ \land A \gcd N = 1) \to A^{2} /_{L} N = 1$

Metamath Proof Explorer

Theorem lgssq

Proof