lgs1

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

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

Step	Hyp	Ref	Expression
1		sq1	$⊢ 1^{2} = 1$
2	1	oveq2i	$⊢ A /_{L} 1^{2} = A /_{L} 1$
3		gcd1	$⊢ A \in ℤ \to A \gcd 1 = 1$
4		1nn	$⊢ 1 \in ℕ$
5		lgssq2	$⊢ (A \in ℤ \land 1 \in ℕ \land A \gcd 1 = 1) \to A /_{L} 1^{2} = 1$
6	4 5	mp3an2	$⊢ (A \in ℤ \land A \gcd 1 = 1) \to A /_{L} 1^{2} = 1$
7	3 6	mpdan	$⊢ A \in ℤ \to A /_{L} 1^{2} = 1$
8	2 7	eqtr3id	$⊢ A \in ℤ \to A /_{L} 1 = 1$

Metamath Proof Explorer