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 e. ZZ -> ( 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 e. ZZ -> ( A gcd 1 ) = 1 )
4 1nn 
 |-  1 e. NN
5 lgssq2 
 |-  ( ( A e. ZZ /\ 1 e. NN /\ ( A gcd 1 ) = 1 ) -> ( A /L ( 1 ^ 2 ) ) = 1 )
6 4 5 mp3an2 
 |-  ( ( A e. ZZ /\ ( A gcd 1 ) = 1 ) -> ( A /L ( 1 ^ 2 ) ) = 1 )
7 3 6 mpdan 
 |-  ( A e. ZZ -> ( A /L ( 1 ^ 2 ) ) = 1 )
8 2 7 eqtr3id 
 |-  ( A e. ZZ -> ( A /L 1 ) = 1 )