1lgs

Description: The Legendre symbol at 1 . See example 1 in ApostolNT p. 180. (Contributed by Mario Carneiro, 28-Apr-2016)

		Ref	Expression
	Assertion	1lgs	$⊢ N \in ℤ \to 1 /_{L} N = 1$

Step	Hyp	Ref	Expression
1		sq1	$⊢ 1^{2} = 1$
2	1	oveq1i	$⊢ 1^{2} /_{L} N = 1 /_{L} N$
3		1gcd	$⊢ N \in ℤ \to 1 \gcd N = 1$
4		1z	$⊢ 1 \in ℤ$
5		ax-1ne0	$⊢ 1 \neq 0$
6	4 5	pm3.2i	$⊢ (1 \in ℤ \land 1 \neq 0)$
7		lgssq	$⊢ ((1 \in ℤ \land 1 \neq 0) \land N \in ℤ \land 1 \gcd N = 1) \to 1^{2} /_{L} N = 1$
8	6 7	mp3an1	$⊢ (N \in ℤ \land 1 \gcd N = 1) \to 1^{2} /_{L} N = 1$
9	3 8	mpdan	$⊢ N \in ℤ \to 1^{2} /_{L} N = 1$
10	2 9	eqtr3id	$⊢ N \in ℤ \to 1 /_{L} N = 1$

Metamath Proof Explorer