lgssq2

Description: The Legendre symbol at a square is equal to 1 . (Contributed by Mario Carneiro, 5-Feb-2015)

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

Proof

Step	Hyp	Ref	Expression
1		simp1	$⊢ (A \in ℤ \land N \in ℕ \land A \gcd N = 1) \to A \in ℤ$
2		nnz	$⊢ N \in ℕ \to N \in ℤ$
3	2	3ad2ant2	$⊢ (A \in ℤ \land N \in ℕ \land A \gcd N = 1) \to N \in ℤ$
4		nnne0	$⊢ N \in ℕ \to N \neq 0$
5	4	3ad2ant2	$⊢ (A \in ℤ \land N \in ℕ \land A \gcd N = 1) \to N \neq 0$
6		lgsdi	$⊢ ((A \in ℤ \land N \in ℤ \land N \in ℤ) \land (N \neq 0 \land N \neq 0)) \to A /_{L} N \cdot N = (A /_{L} N) (A /_{L} N)$
7	1 3 3 5 5 6	syl32anc	$⊢ (A \in ℤ \land N \in ℕ \land A \gcd N = 1) \to A /_{L} N \cdot N = (A /_{L} N) (A /_{L} N)$
8		nncn	$⊢ N \in ℕ \to N \in ℂ$
9	8	3ad2ant2	$⊢ (A \in ℤ \land N \in ℕ \land A \gcd N = 1) \to N \in ℂ$
10	9	sqvald	$⊢ (A \in ℤ \land N \in ℕ \land A \gcd N = 1) \to N^{2} = N \cdot N$
11	10	oveq2d	$⊢ (A \in ℤ \land N \in ℕ \land A \gcd N = 1) \to A /_{L} N^{2} = A /_{L} N \cdot N$
12		lgscl	$⊢ (A \in ℤ \land N \in ℤ) \to A /_{L} N \in ℤ$
13	1 3 12	syl2anc	$⊢ (A \in ℤ \land N \in ℕ \land A \gcd N = 1) \to A /_{L} N \in ℤ$
14	13	zred	$⊢ (A \in ℤ \land N \in ℕ \land A \gcd N = 1) \to A /_{L} N \in ℝ$
15		absresq	$⊢ A /_{L} N \in ℝ \to {\|A /_{L} N\|}^{2} = {(A /_{L} N)}^{2}$
16	14 15	syl	$⊢ (A \in ℤ \land N \in ℕ \land A \gcd N = 1) \to {\|A /_{L} N\|}^{2} = {(A /_{L} N)}^{2}$
17		lgsabs1	$⊢ (A \in ℤ \land N \in ℤ) \to (\|A /_{L} N\| = 1 \leftrightarrow A \gcd N = 1)$
18	2 17	sylan2	$⊢ (A \in ℤ \land N \in ℕ) \to (\|A /_{L} N\| = 1 \leftrightarrow A \gcd N = 1)$
19	18	biimp3ar	$⊢ (A \in ℤ \land N \in ℕ \land A \gcd N = 1) \to \|A /_{L} N\| = 1$
20	19	oveq1d	$⊢ (A \in ℤ \land N \in ℕ \land A \gcd N = 1) \to {\|A /_{L} N\|}^{2} = 1^{2}$
21		sq1	$⊢ 1^{2} = 1$
22	20 21	eqtrdi	$⊢ (A \in ℤ \land N \in ℕ \land A \gcd N = 1) \to {\|A /_{L} N\|}^{2} = 1$
23	13	zcnd	$⊢ (A \in ℤ \land N \in ℕ \land A \gcd N = 1) \to A /_{L} N \in ℂ$
24	23	sqvald	$⊢ (A \in ℤ \land N \in ℕ \land A \gcd N = 1) \to {(A /_{L} N)}^{2} = (A /_{L} N) (A /_{L} N)$
25	16 22 24	3eqtr3d	$⊢ (A \in ℤ \land N \in ℕ \land A \gcd N = 1) \to 1 = (A /_{L} N) (A /_{L} N)$
26	7 11 25	3eqtr4d	$⊢ (A \in ℤ \land N \in ℕ \land A \gcd N = 1) \to A /_{L} N^{2} = 1$

Metamath Proof Explorer

Theorem lgssq2

Proof