Metamath Proof Explorer


Theorem lgsle1

Description: The Legendre symbol has absolute value less than or equal to 1. Together with lgscl this implies that it takes values in { -u 1 , 0 , 1 } . (Contributed by Mario Carneiro, 4-Feb-2015)

Ref Expression
Assertion lgsle1 ( ( 𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ) → ( abs ‘ ( 𝐴 /L 𝑁 ) ) ≤ 1 )

Proof

Step Hyp Ref Expression
1 eqid { 𝑥 ∈ ℤ ∣ ( abs ‘ 𝑥 ) ≤ 1 } = { 𝑥 ∈ ℤ ∣ ( abs ‘ 𝑥 ) ≤ 1 }
2 1 lgscl2 ( ( 𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ) → ( 𝐴 /L 𝑁 ) ∈ { 𝑥 ∈ ℤ ∣ ( abs ‘ 𝑥 ) ≤ 1 } )
3 fveq2 ( 𝑥 = ( 𝐴 /L 𝑁 ) → ( abs ‘ 𝑥 ) = ( abs ‘ ( 𝐴 /L 𝑁 ) ) )
4 3 breq1d ( 𝑥 = ( 𝐴 /L 𝑁 ) → ( ( abs ‘ 𝑥 ) ≤ 1 ↔ ( abs ‘ ( 𝐴 /L 𝑁 ) ) ≤ 1 ) )
5 4 elrab ( ( 𝐴 /L 𝑁 ) ∈ { 𝑥 ∈ ℤ ∣ ( abs ‘ 𝑥 ) ≤ 1 } ↔ ( ( 𝐴 /L 𝑁 ) ∈ ℤ ∧ ( abs ‘ ( 𝐴 /L 𝑁 ) ) ≤ 1 ) )
6 5 simprbi ( ( 𝐴 /L 𝑁 ) ∈ { 𝑥 ∈ ℤ ∣ ( abs ‘ 𝑥 ) ≤ 1 } → ( abs ‘ ( 𝐴 /L 𝑁 ) ) ≤ 1 )
7 2 6 syl ( ( 𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ) → ( abs ‘ ( 𝐴 /L 𝑁 ) ) ≤ 1 )