Metamath Proof Explorer

Theorem lgsfval

Description: Value 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∈ℕ⟼ifn∈ℙifn=2if2∥A0ifAmod8∈171−1An−12+1modn−1npCntN1
Assertion lgsfval ⊢M∈ℕ→F⁡M=ifM∈ℙifM=2if2∥A0ifAmod8∈171−1AM−12+1modM−1MpCntN1

Proof

Step Hyp Ref Expression
1 lgsval.1 ⊢F=n∈ℕ⟼ifn∈ℙifn=2if2∥A0ifAmod8∈171−1An−12+1modn−1npCntN1
2 eleq1 ⊢n=M→n∈ℙ↔M∈ℙ
3 eqeq1 ⊢n=M→n=2↔M=2
4 oveq1 ⊢n=M→n−1=M−1
5 4 oveq1d ⊢n=M→n−12=M−12
6 5 oveq2d ⊢n=M→An−12=AM−12
7 6 oveq1d ⊢n=M→An−12+1=AM−12+1
8 id ⊢n=M→n=M
9 7 8 oveq12d ⊢n=M→An−12+1modn=AM−12+1modM
10 9 oveq1d ⊢n=M→An−12+1modn−1=AM−12+1modM−1
11 3 10 ifbieq2d ⊢n=M→ifn=2if2∥A0ifAmod8∈171−1An−12+1modn−1=ifM=2if2∥A0ifAmod8∈171−1AM−12+1modM−1
12 oveq1 ⊢n=M→npCntN=MpCntN
13 11 12 oveq12d ⊢n=M→ifn=2if2∥A0ifAmod8∈171−1An−12+1modn−1npCntN=ifM=2if2∥A0ifAmod8∈171−1AM−12+1modM−1MpCntN
14 2 13 ifbieq1d ⊢n=M→ifn∈ℙifn=2if2∥A0ifAmod8∈171−1An−12+1modn−1npCntN1=ifM∈ℙifM=2if2∥A0ifAmod8∈171−1AM−12+1modM−1MpCntN1
15 ovex ⊢ifM=2if2∥A0ifAmod8∈171−1AM−12+1modM−1MpCntN∈V
16 1ex ⊢1∈V
17 15 16 ifex ⊢ifM∈ℙifM=2if2∥A0ifAmod8∈171−1AM−12+1modM−1MpCntN1∈V
18 14 1 17 fvmpt ⊢M∈ℕ→F⁡M=ifM∈ℙifM=2if2∥A0ifAmod8∈171−1AM−12+1modM−1MpCntN1