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=n∈ℕ⟼ifn∈ℙA/LnnpCntN1
Assertion lgsval4 ⊢A∈ℤ∧N∈ℤ∧N≠0→A/LN=ifN<0∧A<0−11⁢seq1×F⁡N

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 lgsval ⊢A∈ℤ∧N∈ℤ→A/LN=ifN=0ifA2=110ifN<0∧A<0−11⁢seq1×n∈ℕ⟼ifn∈ℙifn=2if2∥A0ifAmod8∈171−1An−12+1modn−1npCntN1⁡N
4 3 3adant3 ⊢A∈ℤ∧N∈ℤ∧N≠0→A/LN=ifN=0ifA2=110ifN<0∧A<0−11⁢seq1×n∈ℕ⟼ifn∈ℙifn=2if2∥A0ifAmod8∈171−1An−12+1modn−1npCntN1⁡N
5 simp3 ⊢A∈ℤ∧N∈ℤ∧N≠0→N≠0
6 5 neneqd ⊢A∈ℤ∧N∈ℤ∧N≠0→¬N=0
7 6 iffalsed ⊢A∈ℤ∧N∈ℤ∧N≠0→ifN=0ifA2=110ifN<0∧A<0−11⁢seq1×n∈ℕ⟼ifn∈ℙifn=2if2∥A0ifAmod8∈171−1An−12+1modn−1npCntN1⁡N=ifN<0∧A<0−11⁢seq1×n∈ℕ⟼ifn∈ℙifn=2if2∥A0ifAmod8∈171−1An−12+1modn−1npCntN1⁡N
8 2 lgsval4lem ⊢A∈ℤ∧N∈ℤ∧N≠0→n∈ℕ⟼ifn∈ℙifn=2if2∥A0ifAmod8∈171−1An−12+1modn−1npCntN1=n∈ℕ⟼ifn∈ℙA/LnnpCntN1
9 8 1 eqtr4di ⊢A∈ℤ∧N∈ℤ∧N≠0→n∈ℕ⟼ifn∈ℙifn=2if2∥A0ifAmod8∈171−1An−12+1modn−1npCntN1=F
10 9 seqeq3d ⊢A∈ℤ∧N∈ℤ∧N≠0→seq1×n∈ℕ⟼ifn∈ℙifn=2if2∥A0ifAmod8∈171−1An−12+1modn−1npCntN1=seq1×F
11 10 fveq1d ⊢A∈ℤ∧N∈ℤ∧N≠0→seq1×n∈ℕ⟼ifn∈ℙifn=2if2∥A0ifAmod8∈171−1An−12+1modn−1npCntN1⁡N=seq1×F⁡N
12 11 oveq2d ⊢A∈ℤ∧N∈ℤ∧N≠0→ifN<0∧A<0−11⁢seq1×n∈ℕ⟼ifn∈ℙifn=2if2∥A0ifAmod8∈171−1An−12+1modn−1npCntN1⁡N=ifN<0∧A<0−11⁢seq1×F⁡N
13 4 7 12 3eqtrd ⊢A∈ℤ∧N∈ℤ∧N≠0→A/LN=ifN<0∧A<0−11⁢seq1×F⁡N