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 )