Metamath Proof Explorer


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

Proof

Step Hyp Ref Expression
1 sq1 1 2 = 1
2 1 oveq1i 1 2 / L N = 1 / L N
3 1gcd N 1 gcd N = 1
4 1z 1
5 ax-1ne0 1 0
6 4 5 pm3.2i 1 1 0
7 lgssq 1 1 0 N 1 gcd N = 1 1 2 / L N = 1
8 6 7 mp3an1 N 1 gcd N = 1 1 2 / L N = 1
9 3 8 mpdan N 1 2 / L N = 1
10 2 9 eqtr3id N 1 / L N = 1