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 )