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 ∈ ℤ → 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 ∈ ℤ → A gcd 1 = 1
4 1nn ⊢ 1 ∈ ℕ
5 lgssq2 ⊢ A ∈ ℤ ∧ 1 ∈ ℕ ∧ A gcd 1 = 1 → A / L 1 2 = 1
6 4 5 mp3an2 ⊢ A ∈ ℤ ∧ A gcd 1 = 1 → A / L 1 2 = 1
7 3 6 mpdan ⊢ A ∈ ℤ → A / L 1 2 = 1
8 2 7 eqtr3id ⊢ A ∈ ℤ → A / L 1 = 1