Metamath Proof Explorer


Theorem lgsval4

Description: Restate lgsval for nonzero N , where the function F has been abbreviated into a self-referential expression taking the value of /L on the primes as given. (Contributed by Mario Carneiro, 4-Feb-2015)

Ref Expression
Hypothesis lgsval4.1 F=nifnA/LnnpCntN1
Assertion lgsval4 ANN0A/LN=ifN<0A<011seq1×FN

Proof

Step Hyp Ref Expression
1 lgsval4.1 F=nifnA/LnnpCntN1
2 eqid nifnifn=2if2A0ifAmod81711An12+1modn1npCntN1=nifnifn=2if2A0ifAmod81711An12+1modn1npCntN1
3 2 lgsval ANA/LN=ifN=0ifA2=110ifN<0A<011seq1×nifnifn=2if2A0ifAmod81711An12+1modn1npCntN1N
4 3 3adant3 ANN0A/LN=ifN=0ifA2=110ifN<0A<011seq1×nifnifn=2if2A0ifAmod81711An12+1modn1npCntN1N
5 simp3 ANN0N0
6 5 neneqd ANN0¬N=0
7 6 iffalsed ANN0ifN=0ifA2=110ifN<0A<011seq1×nifnifn=2if2A0ifAmod81711An12+1modn1npCntN1N=ifN<0A<011seq1×nifnifn=2if2A0ifAmod81711An12+1modn1npCntN1N
8 2 lgsval4lem ANN0nifnifn=2if2A0ifAmod81711An12+1modn1npCntN1=nifnA/LnnpCntN1
9 8 1 eqtr4di ANN0nifnifn=2if2A0ifAmod81711An12+1modn1npCntN1=F
10 9 seqeq3d ANN0seq1×nifnifn=2if2A0ifAmod81711An12+1modn1npCntN1=seq1×F
11 10 fveq1d ANN0seq1×nifnifn=2if2A0ifAmod81711An12+1modn1npCntN1N=seq1×FN
12 11 oveq2d ANN0ifN<0A<011seq1×nifnifn=2if2A0ifAmod81711An12+1modn1npCntN1N=ifN<0A<011seq1×FN
13 4 7 12 3eqtrd ANN0A/LN=ifN<0A<011seq1×FN