Metamath Proof Explorer


Theorem 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 A / L 1 = 1

Proof

Step Hyp Ref Expression
1 sq1 1 2 = 1
2 1 oveq2i A / L 1 2 = A / L 1
3 gcd1 A A gcd 1 = 1
4 1nn 1
5 lgssq2 A 1 A gcd 1 = 1 A / L 1 2 = 1
6 4 5 mp3an2 A A gcd 1 = 1 A / L 1 2 = 1
7 3 6 mpdan A A / L 1 2 = 1
8 2 7 eqtr3id A A / L 1 = 1