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∈ℕ⟼ifn∈ℙA/LnnpCntN1
Assertion lgsfcl3 ⊢A∈ℤ∧N∈ℤ∧N≠0→F:ℕ⟶ℤ

Proof

Step Hyp Ref Expression
1 lgsval4.1 ⊢F=n∈ℕ⟼ifn∈ℙA/LnnpCntN1
2 eqid ⊢n∈ℕ⟼ifn∈ℙifn=2if2∥A0ifAmod8∈171−1An−12+1modn−1npCntN1=n∈ℕ⟼ifn∈ℙifn=2if2∥A0ifAmod8∈171−1An−12+1modn−1npCntN1
3 2 lgsfcl ⊢A∈ℤ∧N∈ℤ∧N≠0→n∈ℕ⟼ifn∈ℙifn=2if2∥A0ifAmod8∈171−1An−12+1modn−1npCntN1:ℕ⟶ℤ
4 2 lgsval4lem ⊢A∈ℤ∧N∈ℤ∧N≠0→n∈ℕ⟼ifn∈ℙifn=2if2∥A0ifAmod8∈171−1An−12+1modn−1npCntN1=n∈ℕ⟼ifn∈ℙA/LnnpCntN1
5 4 1 eqtr4di ⊢A∈ℤ∧N∈ℤ∧N≠0→n∈ℕ⟼ifn∈ℙifn=2if2∥A0ifAmod8∈171−1An−12+1modn−1npCntN1=F
6 5 feq1d ⊢A∈ℤ∧N∈ℤ∧N≠0→n∈ℕ⟼ifn∈ℙifn=2if2∥A0ifAmod8∈171−1An−12+1modn−1npCntN1:ℕ⟶ℤ↔F:ℕ⟶ℤ
7 3 6 mpbid ⊢A∈ℤ∧N∈ℤ∧N≠0→F:ℕ⟶ℤ