Metamath Proof Explorer

Theorem lgsval

Description: Value of the Legendre symbol at an arbitrary integer. (Contributed by Mario Carneiro, 4-Feb-2015)

Ref Expression
Hypothesis lgsval.1 ⊢F=n∈ℕ⟼ifn∈ℙifn=2if2∥A0ifAmod8∈171−1An−12+1modn−1npCntN1
Assertion lgsval ⊢A∈ℤ∧N∈ℤ→A/LN=ifN=0ifA2=110ifN<0∧A<0−11⁢seq1×F⁡N

Proof

Step Hyp Ref Expression
1 lgsval.1 ⊢F=n∈ℕ⟼ifn∈ℙifn=2if2∥A0ifAmod8∈171−1An−12+1modn−1npCntN1
2 simpr ⊢a=A∧m=N→m=N
3 2 eqeq1d ⊢a=A∧m=N→m=0↔N=0
4 simpl ⊢a=A∧m=N→a=A
5 4 oveq1d ⊢a=A∧m=N→a2=A2
6 5 eqeq1d ⊢a=A∧m=N→a2=1↔A2=1
7 6 ifbid ⊢a=A∧m=N→ifa2=110=ifA2=110
8 2 breq1d ⊢a=A∧m=N→m<0↔N<0
9 4 breq1d ⊢a=A∧m=N→a<0↔A<0
10 8 9 anbi12d ⊢a=A∧m=N→m<0∧a<0↔N<0∧A<0
11 10 ifbid ⊢a=A∧m=N→ifm<0∧a<0−11=ifN<0∧A<0−11
12 4 breq2d ⊢a=A∧m=N→2∥a↔2∥A
13 4 oveq1d ⊢a=A∧m=N→amod8=Amod8
14 13 eleq1d ⊢a=A∧m=N→amod8∈17↔Amod8∈17
15 14 ifbid ⊢a=A∧m=N→ifamod8∈171−1=ifAmod8∈171−1
16 12 15 ifbieq2d ⊢a=A∧m=N→if2∥a0ifamod8∈171−1=if2∥A0ifAmod8∈171−1
17 4 oveq1d ⊢a=A∧m=N→an−12=An−12
18 17 oveq1d ⊢a=A∧m=N→an−12+1=An−12+1
19 18 oveq1d ⊢a=A∧m=N→an−12+1modn=An−12+1modn
20 19 oveq1d ⊢a=A∧m=N→an−12+1modn−1=An−12+1modn−1
21 16 20 ifeq12d ⊢a=A∧m=N→ifn=2if2∥a0ifamod8∈171−1an−12+1modn−1=ifn=2if2∥A0ifAmod8∈171−1An−12+1modn−1
22 2 oveq2d ⊢a=A∧m=N→npCntm=npCntN
23 21 22 oveq12d ⊢a=A∧m=N→ifn=2if2∥a0ifamod8∈171−1an−12+1modn−1npCntm=ifn=2if2∥A0ifAmod8∈171−1An−12+1modn−1npCntN
24 23 ifeq1d ⊢a=A∧m=N→ifn∈ℙifn=2if2∥a0ifamod8∈171−1an−12+1modn−1npCntm1=ifn∈ℙifn=2if2∥A0ifAmod8∈171−1An−12+1modn−1npCntN1
25 24 mpteq2dv ⊢a=A∧m=N→n∈ℕ⟼ifn∈ℙifn=2if2∥a0ifamod8∈171−1an−12+1modn−1npCntm1=n∈ℕ⟼ifn∈ℙifn=2if2∥A0ifAmod8∈171−1An−12+1modn−1npCntN1
26 25 1 eqtr4di ⊢a=A∧m=N→n∈ℕ⟼ifn∈ℙifn=2if2∥a0ifamod8∈171−1an−12+1modn−1npCntm1=F
27 26 seqeq3d ⊢a=A∧m=N→seq1×n∈ℕ⟼ifn∈ℙifn=2if2∥a0ifamod8∈171−1an−12+1modn−1npCntm1=seq1×F
28 2 fveq2d ⊢a=A∧m=N→m=N
29 27 28 fveq12d ⊢a=A∧m=N→seq1×n∈ℕ⟼ifn∈ℙifn=2if2∥a0ifamod8∈171−1an−12+1modn−1npCntm1⁡m=seq1×F⁡N
30 11 29 oveq12d ⊢a=A∧m=N→ifm<0∧a<0−11⁢seq1×n∈ℕ⟼ifn∈ℙifn=2if2∥a0ifamod8∈171−1an−12+1modn−1npCntm1⁡m=ifN<0∧A<0−11⁢seq1×F⁡N
31 3 7 30 ifbieq12d ⊢a=A∧m=N→ifm=0ifa2=110ifm<0∧a<0−11⁢seq1×n∈ℕ⟼ifn∈ℙifn=2if2∥a0ifamod8∈171−1an−12+1modn−1npCntm1⁡m=ifN=0ifA2=110ifN<0∧A<0−11⁢seq1×F⁡N
32 df-lgs ⊢/L=a∈ℤ,m∈ℤ⟼ifm=0ifa2=110ifm<0∧a<0−11⁢seq1×n∈ℕ⟼ifn∈ℙifn=2if2∥a0ifamod8∈171−1an−12+1modn−1npCntm1⁡m
33 1nn0 ⊢1∈ℕ0
34 0nn0 ⊢0∈ℕ0
35 33 34 ifcli ⊢ifA2=110∈ℕ0
36 35 elexi ⊢ifA2=110∈V
37 ovex ⊢ifN<0∧A<0−11⁢seq1×F⁡N∈V
38 36 37 ifex ⊢ifN=0ifA2=110ifN<0∧A<0−11⁢seq1×F⁡N∈V
39 31 32 38 ovmpoa ⊢A∈ℤ∧N∈ℤ→A/LN=ifN=0ifA2=110ifN<0∧A<0−11⁢seq1×F⁡N