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 ( 𝐴 ∈ ℤ → ( 𝐴 /L 1 ) = 1 )

Proof

Step Hyp Ref Expression
1 sq1 ( 1 ↑ 2 ) = 1
2 1 oveq2i ( 𝐴 /L ( 1 ↑ 2 ) ) = ( 𝐴 /L 1 )
3 gcd1 ( 𝐴 ∈ ℤ → ( 𝐴 gcd 1 ) = 1 )
4 1nn 1 ∈ ℕ
5 lgssq2 ( ( 𝐴 ∈ ℤ ∧ 1 ∈ ℕ ∧ ( 𝐴 gcd 1 ) = 1 ) → ( 𝐴 /L ( 1 ↑ 2 ) ) = 1 )
6 4 5 mp3an2 ( ( 𝐴 ∈ ℤ ∧ ( 𝐴 gcd 1 ) = 1 ) → ( 𝐴 /L ( 1 ↑ 2 ) ) = 1 )
7 3 6 mpdan ( 𝐴 ∈ ℤ → ( 𝐴 /L ( 1 ↑ 2 ) ) = 1 )
8 2 7 eqtr3id ( 𝐴 ∈ ℤ → ( 𝐴 /L 1 ) = 1 )