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 ) |
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 ) |