Metamath Proof Explorer

Theorem lgsval4lem

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

Ref Expression
Hypothesis lgsval.1 ⊢ F = n ∈ ℕ ⟼ if n ∈ ℙ if n = 2 if 2 ∥ A 0 if A mod 8 ∈ 1 7 1 − 1 A n − 1 2 + 1 mod n − 1 n pCnt N 1
Assertion lgsval4lem ⊢ A ∈ ℤ ∧ N ∈ ℤ ∧ N ≠ 0 → F = n ∈ ℕ ⟼ if n ∈ ℙ A / L n n pCnt N 1

Proof

Step Hyp Ref Expression
1 lgsval.1 ⊢ F = n ∈ ℕ ⟼ if n ∈ ℙ if n = 2 if 2 ∥ A 0 if A mod 8 ∈ 1 7 1 − 1 A n − 1 2 + 1 mod n − 1 n pCnt N 1
2 eqid ⊢ m ∈ ℕ ⟼ if m ∈ ℙ if m = 2 if 2 ∥ A 0 if A mod 8 ∈ 1 7 1 − 1 A m − 1 2 + 1 mod m − 1 m pCnt n 1 = m ∈ ℕ ⟼ if m ∈ ℙ if m = 2 if 2 ∥ A 0 if A mod 8 ∈ 1 7 1 − 1 A m − 1 2 + 1 mod m − 1 m pCnt n 1
3 2 lgsval2lem ⊢ A ∈ ℤ ∧ n ∈ ℙ → A / L n = if n = 2 if 2 ∥ A 0 if A mod 8 ∈ 1 7 1 − 1 A n − 1 2 + 1 mod n − 1
4 3 3ad2antl1 ⊢ A ∈ ℤ ∧ N ∈ ℤ ∧ N ≠ 0 ∧ n ∈ ℙ → A / L n = if n = 2 if 2 ∥ A 0 if A mod 8 ∈ 1 7 1 − 1 A n − 1 2 + 1 mod n − 1
5 4 oveq1d ⊢ A ∈ ℤ ∧ N ∈ ℤ ∧ N ≠ 0 ∧ n ∈ ℙ → A / L n n pCnt N = if n = 2 if 2 ∥ A 0 if A mod 8 ∈ 1 7 1 − 1 A n − 1 2 + 1 mod n − 1 n pCnt N
6 5 ifeq1da ⊢ A ∈ ℤ ∧ N ∈ ℤ ∧ N ≠ 0 → if n ∈ ℙ A / L n n pCnt N 1 = if n ∈ ℙ if n = 2 if 2 ∥ A 0 if A mod 8 ∈ 1 7 1 − 1 A n − 1 2 + 1 mod n − 1 n pCnt N 1
7 6 mpteq2dv ⊢ A ∈ ℤ ∧ N ∈ ℤ ∧ N ≠ 0 → n ∈ ℕ ⟼ if n ∈ ℙ A / L n n pCnt N 1 = n ∈ ℕ ⟼ if n ∈ ℙ if n = 2 if 2 ∥ A 0 if A mod 8 ∈ 1 7 1 − 1 A n − 1 2 + 1 mod n − 1 n pCnt N 1
8 1 7 eqtr4id ⊢ A ∈ ℤ ∧ N ∈ ℤ ∧ N ≠ 0 → F = n ∈ ℕ ⟼ if n ∈ ℙ A / L n n pCnt N 1