Metamath Proof Explorer

Theorem lgsfcl3

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

Ref Expression
Hypothesis lgsval4.1 ⊢ F = n ∈ ℕ ⟼ if n ∈ ℙ A / L n n pCnt N 1
Assertion lgsfcl3 ⊢ A ∈ ℤ ∧ N ∈ ℤ ∧ N ≠ 0 → F : ℕ ⟶ ℤ

Proof

Step Hyp Ref Expression
1 lgsval4.1 ⊢ F = n ∈ ℕ ⟼ if n ∈ ℙ A / L n n pCnt N 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 lgsfcl ⊢ A ∈ ℤ ∧ N ∈ ℤ ∧ N ≠ 0 → 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 : ℕ ⟶ ℤ
4 2 lgsval4lem ⊢ A ∈ ℤ ∧ N ∈ ℤ ∧ N ≠ 0 → 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 ∈ ℙ A / L n n pCnt N 1
5 4 1 eqtr4di ⊢ A ∈ ℤ ∧ N ∈ ℤ ∧ N ≠ 0 → 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 = F
6 5 feq1d ⊢ A ∈ ℤ ∧ N ∈ ℤ ∧ N ≠ 0 → 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 : ℕ ⟶ ℤ ↔ F : ℕ ⟶ ℤ
7 3 6 mpbid ⊢ A ∈ ℤ ∧ N ∈ ℤ ∧ N ≠ 0 → F : ℕ ⟶ ℤ