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 ∈ ℕ ⟼ if n ∈ ℙ A / L n n pCnt N 1
Assertion lgsval4 ⊢ A ∈ ℤ ∧ N ∈ ℤ ∧ N ≠ 0 → A / L N = if N < 0 ∧ A < 0 − 1 1 ⁢ seq 1 × F ⁡ N

Proof

Step Hyp Ref Expression
1 lgsval4.1 ⊢ F = n ∈ ℕ ⟼ if n ∈ ℙ A / L n n pCnt N 1
2 eqid ⊢ 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 = 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
3 2 lgsval ⊢ A ∈ ℤ ∧ N ∈ ℤ → A / L N = if N = 0 if A 2 = 1 1 0 if N < 0 ∧ A < 0 − 1 1 ⁢ seq 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 ⁡ N
4 3 3adant3 ⊢ A ∈ ℤ ∧ N ∈ ℤ ∧ N ≠ 0 → A / L N = if N = 0 if A 2 = 1 1 0 if N < 0 ∧ A < 0 − 1 1 ⁢ seq 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 ⁡ 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 → if N = 0 if A 2 = 1 1 0 if N < 0 ∧ A < 0 − 1 1 ⁢ seq 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 ⁡ N = if N < 0 ∧ A < 0 − 1 1 ⁢ seq 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 ⁡ N
8 2 lgsval4lem ⊢ A ∈ ℤ ∧ N ∈ ℤ ∧ N ≠ 0 → 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 = n ∈ ℕ ⟼ if n ∈ ℙ A / L n n pCnt N 1
9 8 1 eqtr4di ⊢ A ∈ ℤ ∧ N ∈ ℤ ∧ N ≠ 0 → 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 = F
10 9 seqeq3d ⊢ A ∈ ℤ ∧ N ∈ ℤ ∧ N ≠ 0 → seq 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 = seq 1 × F
11 10 fveq1d ⊢ A ∈ ℤ ∧ N ∈ ℤ ∧ N ≠ 0 → seq 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 ⁡ N = seq 1 × F ⁡ N
12 11 oveq2d ⊢ A ∈ ℤ ∧ N ∈ ℤ ∧ N ≠ 0 → if N < 0 ∧ A < 0 − 1 1 ⁢ seq 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 ⁡ N = if N < 0 ∧ A < 0 − 1 1 ⁢ seq 1 × F ⁡ N
13 4 7 12 3eqtrd ⊢ A ∈ ℤ ∧ N ∈ ℤ ∧ N ≠ 0 → A / L N = if N < 0 ∧ A < 0 − 1 1 ⁢ seq 1 × F ⁡ N