Metamath Proof Explorer

Theorem lgsval4lem

Description: Lemma for lgsval4 . (Contributed by Mario Carneiro, 4-Feb-2015)

Ref Expression
Hypothesis lgsval.1 ⊢F=n∈ℕ⟼ifn∈ℙifn=2if2∥A0ifAmod8∈171−1An−12+1modn−1npCntN1
Assertion lgsval4lem ⊢A∈ℤ∧N∈ℤ∧N≠0→F=n∈ℕ⟼ifn∈ℙA/LnnpCntN1

Proof

Step Hyp Ref Expression
1 lgsval.1 ⊢F=n∈ℕ⟼ifn∈ℙifn=2if2∥A0ifAmod8∈171−1An−12+1modn−1npCntN1
2 eqid ⊢m∈ℕ⟼ifm∈ℙifm=2if2∥A0ifAmod8∈171−1Am−12+1modm−1mpCntn1=m∈ℕ⟼ifm∈ℙifm=2if2∥A0ifAmod8∈171−1Am−12+1modm−1mpCntn1
3 2 lgsval2lem ⊢A∈ℤ∧n∈ℙ→A/Ln=ifn=2if2∥A0ifAmod8∈171−1An−12+1modn−1
4 3 3ad2antl1 ⊢A∈ℤ∧N∈ℤ∧N≠0∧n∈ℙ→A/Ln=ifn=2if2∥A0ifAmod8∈171−1An−12+1modn−1
5 4 oveq1d ⊢A∈ℤ∧N∈ℤ∧N≠0∧n∈ℙ→A/LnnpCntN=ifn=2if2∥A0ifAmod8∈171−1An−12+1modn−1npCntN
6 5 ifeq1da ⊢A∈ℤ∧N∈ℤ∧N≠0→ifn∈ℙA/LnnpCntN1=ifn∈ℙifn=2if2∥A0ifAmod8∈171−1An−12+1modn−1npCntN1
7 6 mpteq2dv ⊢A∈ℤ∧N∈ℤ∧N≠0→n∈ℕ⟼ifn∈ℙA/LnnpCntN1=n∈ℕ⟼ifn∈ℙifn=2if2∥A0ifAmod8∈171−1An−12+1modn−1npCntN1
8 1 7 eqtr4id ⊢A∈ℤ∧N∈ℤ∧N≠0→F=n∈ℕ⟼ifn∈ℙA/LnnpCntN1