Metamath Proof Explorer

Theorem lgsfcl

Description: Closure of the function F which defines the Legendre symbol at the primes. (Contributed by Mario Carneiro, 4-Feb-2015)

Ref Expression
Hypothesis lgsval.1 ⊢ F = 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
Assertion lgsfcl ⊢ A ∈ ℤ ∧ N ∈ ℤ ∧ N ≠ 0 → F : ℕ ⟶ ℤ

Proof

Step Hyp Ref Expression
1 lgsval.1 ⊢ F = 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
2 eqid ⊢ x ∈ ℤ | x ≤ 1 = x ∈ ℤ | x ≤ 1
3 1 2 lgsfcl2 ⊢ A ∈ ℤ ∧ N ∈ ℤ ∧ N ≠ 0 → F : ℕ ⟶ x ∈ ℤ | x ≤ 1
4 ssrab2 ⊢ x ∈ ℤ | x ≤ 1 ⊆ ℤ
5 fss ⊢ F : ℕ ⟶ x ∈ ℤ | x ≤ 1 ∧ x ∈ ℤ | x ≤ 1 ⊆ ℤ → F : ℕ ⟶ ℤ
6 3 4 5 sylancl ⊢ A ∈ ℤ ∧ N ∈ ℤ ∧ N ≠ 0 → F : ℕ ⟶ ℤ