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 )