Theorem lgscl2

Description: The Legendre symbol is an integer with absolute value less than or equal to 1. (Contributed by Mario Carneiro, 4-Feb-2015)

	Ref	Expression
Hypothesis	lgscl2.z	⊢ 𝑍 = { 𝑥 ∈ ℤ ∣ ( abs ‘ 𝑥 ) ≤ 1 }
Assertion	lgscl2	⊢ ( ( 𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ) → ( 𝐴 /L 𝑁 ) ∈ 𝑍 )

Proof

Step	Hyp	Ref	Expression
1		lgscl2.z	⊢ 𝑍 = { 𝑥 ∈ ℤ ∣ ( abs ‘ 𝑥 ) ≤ 1 }
2		eqid	⊢ ( 𝑛 ∈ ℕ ↦ if ( 𝑛 ∈ ℙ , ( if ( 𝑛 = 2 , if ( 2 ∥ 𝐴 , 0 , if ( ( 𝐴 mod 8 ) ∈ { 1 , 7 } , 1 , - 1 ) ) , ( ( ( ( 𝐴 ↑ ( ( 𝑛 − 1 ) / 2 ) ) + 1 ) mod 𝑛 ) − 1 ) ) ↑ ( 𝑛 pCnt 𝑁 ) ) , 1 ) ) = ( 𝑛 ∈ ℕ ↦ if ( 𝑛 ∈ ℙ , ( if ( 𝑛 = 2 , if ( 2 ∥ 𝐴 , 0 , if ( ( 𝐴 mod 8 ) ∈ { 1 , 7 } , 1 , - 1 ) ) , ( ( ( ( 𝐴 ↑ ( ( 𝑛 − 1 ) / 2 ) ) + 1 ) mod 𝑛 ) − 1 ) ) ↑ ( 𝑛 pCnt 𝑁 ) ) , 1 ) )
3	2 1	lgscllem	⊢ ( ( 𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ) → ( 𝐴 /L 𝑁 ) ∈ 𝑍 )