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 ⊢ A ∈ ℤ ∧ N ∈ ℤ → A / L N ≤ 1

Proof

Step Hyp Ref Expression
1 eqid ⊢ x ∈ ℤ | x ≤ 1 = x ∈ ℤ | x ≤ 1
2 1 lgscl2 ⊢ A ∈ ℤ ∧ N ∈ ℤ → A / L N ∈ x ∈ ℤ | x ≤ 1
3 fveq2 ⊢ x = A / L N → x = A / L N
4 3 breq1d ⊢ x = A / L N → x ≤ 1 ↔ A / L N ≤ 1
5 4 elrab ⊢ A / L N ∈ x ∈ ℤ | x ≤ 1 ↔ A / L N ∈ ℤ ∧ A / L N ≤ 1
6 5 simprbi ⊢ A / L N ∈ x ∈ ℤ | x ≤ 1 → A / L N ≤ 1
7 2 6 syl ⊢ A ∈ ℤ ∧ N ∈ ℤ → A / L N ≤ 1