Description: The Legendre symbol at 1 . See example 1 in ApostolNT p. 180. (Contributed by Mario Carneiro, 28-Apr-2016)
Ref | Expression | ||
---|---|---|---|
Assertion | 1lgs |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | sq1 | ||
2 | 1 | oveq1i | |
3 | 1gcd | ||
4 | 1z | ||
5 | ax-1ne0 | ||
6 | 4 5 | pm3.2i | |
7 | lgssq | ||
8 | 6 7 | mp3an1 | |
9 | 3 8 | mpdan | |
10 | 2 9 | syl5eqr |