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 ) |
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 | syl5eqr | |- ( A e. ZZ -> ( A /L 1 ) = 1 ) |