Metamath Proof Explorer

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 ⊢ Z = x ∈ ℤ | x ≤ 1
Assertion lgscl2 ⊢ A ∈ ℤ ∧ N ∈ ℤ → A / L N ∈ Z

Proof

Step Hyp Ref Expression
1 lgscl2.z ⊢ Z = x ∈ ℤ | x ≤ 1
2 eqid ⊢ n ∈ ℕ ⟼ if n ∈ ℙ if n = 2 if 2 ∥ A 0 if A mod 8 ∈ 1 7 1 − 1 A n − 1 2 + 1 mod n − 1 n pCnt N 1 = n ∈ ℕ ⟼ if n ∈ ℙ if n = 2 if 2 ∥ A 0 if A mod 8 ∈ 1 7 1 − 1 A n − 1 2 + 1 mod n − 1 n pCnt N 1
3 2 1 lgscllem ⊢ A ∈ ℤ ∧ N ∈ ℤ → A / L N ∈ Z