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 e. ZZ -> ( 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 e. ZZ -> ( 1 gcd N ) = 1 )
4 1z
 |-  1 e. ZZ
5 ax-1ne0
 |-  1 =/= 0
6 4 5 pm3.2i
 |-  ( 1 e. ZZ /\ 1 =/= 0 )
7 lgssq
 |-  ( ( ( 1 e. ZZ /\ 1 =/= 0 ) /\ N e. ZZ /\ ( 1 gcd N ) = 1 ) -> ( ( 1 ^ 2 ) /L N ) = 1 )
8 6 7 mp3an1
 |-  ( ( N e. ZZ /\ ( 1 gcd N ) = 1 ) -> ( ( 1 ^ 2 ) /L N ) = 1 )
9 3 8 mpdan
 |-  ( N e. ZZ -> ( ( 1 ^ 2 ) /L N ) = 1 )
10 2 9 eqtr3id
 |-  ( N e. ZZ -> ( 1 /L N ) = 1 )