Metamath Proof Explorer

Theorem 1lgs

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 ∈ ℤ → 1 / L N = 1

Proof

Step Hyp Ref Expression
1 sq1 ⊢ 1 2 = 1
2 1 oveq1i ⊢ 1 2 / L N = 1 / L N
3 1gcd ⊢ N ∈ ℤ → 1 gcd N = 1
4 1z ⊢ 1 ∈ ℤ
5 ax-1ne0 ⊢ 1 ≠ 0
6 4 5 pm3.2i ⊢ 1 ∈ ℤ ∧ 1 ≠ 0
7 lgssq ⊢ 1 ∈ ℤ ∧ 1 ≠ 0 ∧ N ∈ ℤ ∧ 1 gcd N = 1 → 1 2 / L N = 1
8 6 7 mp3an1 ⊢ N ∈ ℤ ∧ 1 gcd N = 1 → 1 2 / L N = 1
9 3 8 mpdan ⊢ N ∈ ℤ → 1 2 / L N = 1
10 2 9 eqtr3id ⊢ N ∈ ℤ → 1 / L N = 1