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	⊢ 𝐹 = ( 𝑛 ∈ ℕ ↦ if ( 𝑛 ∈ ℙ , ( ( 𝐴 /L 𝑛 ) ↑ ( 𝑛 pCnt 𝑁 ) ) , 1 ) )
Assertion	lgsval4	⊢ ( ( 𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0 ) → ( 𝐴 /L 𝑁 ) = ( if ( ( 𝑁 < 0 ∧ 𝐴 < 0 ) , - 1 , 1 ) · ( seq 1 ( · , 𝐹 ) ‘ ( abs ‘ 𝑁 ) ) ) )

Proof

Step	Hyp	Ref	Expression
1		lgsval4.1	⊢ 𝐹 = ( 𝑛 ∈ ℕ ↦ if ( 𝑛 ∈ ℙ , ( ( 𝐴 /L 𝑛 ) ↑ ( 𝑛 pCnt 𝑁 ) ) , 1 ) )
2		eqid	⊢ ( 𝑛 ∈ ℕ ↦ if ( 𝑛 ∈ ℙ , ( if ( 𝑛 = 2 , if ( 2 ∥ 𝐴 , 0 , if ( ( 𝐴 mod 8 ) ∈ { 1 , 7 } , 1 , - 1 ) ) , ( ( ( ( 𝐴 ↑ ( ( 𝑛 − 1 ) / 2 ) ) + 1 ) mod 𝑛 ) − 1 ) ) ↑ ( 𝑛 pCnt 𝑁 ) ) , 1 ) ) = ( 𝑛 ∈ ℕ ↦ if ( 𝑛 ∈ ℙ , ( if ( 𝑛 = 2 , if ( 2 ∥ 𝐴 , 0 , if ( ( 𝐴 mod 8 ) ∈ { 1 , 7 } , 1 , - 1 ) ) , ( ( ( ( 𝐴 ↑ ( ( 𝑛 − 1 ) / 2 ) ) + 1 ) mod 𝑛 ) − 1 ) ) ↑ ( 𝑛 pCnt 𝑁 ) ) , 1 ) )
3	2	lgsval	⊢ ( ( 𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ) → ( 𝐴 /L 𝑁 ) = if ( 𝑁 = 0 , if ( ( 𝐴 ↑ 2 ) = 1 , 1 , 0 ) , ( if ( ( 𝑁 < 0 ∧ 𝐴 < 0 ) , - 1 , 1 ) · ( seq 1 ( · , ( 𝑛 ∈ ℕ ↦ if ( 𝑛 ∈ ℙ , ( if ( 𝑛 = 2 , if ( 2 ∥ 𝐴 , 0 , if ( ( 𝐴 mod 8 ) ∈ { 1 , 7 } , 1 , - 1 ) ) , ( ( ( ( 𝐴 ↑ ( ( 𝑛 − 1 ) / 2 ) ) + 1 ) mod 𝑛 ) − 1 ) ) ↑ ( 𝑛 pCnt 𝑁 ) ) , 1 ) ) ) ‘ ( abs ‘ 𝑁 ) ) ) ) )
4	3	3adant3	⊢ ( ( 𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0 ) → ( 𝐴 /L 𝑁 ) = if ( 𝑁 = 0 , if ( ( 𝐴 ↑ 2 ) = 1 , 1 , 0 ) , ( if ( ( 𝑁 < 0 ∧ 𝐴 < 0 ) , - 1 , 1 ) · ( seq 1 ( · , ( 𝑛 ∈ ℕ ↦ if ( 𝑛 ∈ ℙ , ( if ( 𝑛 = 2 , if ( 2 ∥ 𝐴 , 0 , if ( ( 𝐴 mod 8 ) ∈ { 1 , 7 } , 1 , - 1 ) ) , ( ( ( ( 𝐴 ↑ ( ( 𝑛 − 1 ) / 2 ) ) + 1 ) mod 𝑛 ) − 1 ) ) ↑ ( 𝑛 pCnt 𝑁 ) ) , 1 ) ) ) ‘ ( abs ‘ 𝑁 ) ) ) ) )
5		simp3	⊢ ( ( 𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0 ) → 𝑁 ≠ 0 )
6	5	neneqd	⊢ ( ( 𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0 ) → ¬ 𝑁 = 0 )
7	6	iffalsed	⊢ ( ( 𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0 ) → if ( 𝑁 = 0 , if ( ( 𝐴 ↑ 2 ) = 1 , 1 , 0 ) , ( if ( ( 𝑁 < 0 ∧ 𝐴 < 0 ) , - 1 , 1 ) · ( seq 1 ( · , ( 𝑛 ∈ ℕ ↦ if ( 𝑛 ∈ ℙ , ( if ( 𝑛 = 2 , if ( 2 ∥ 𝐴 , 0 , if ( ( 𝐴 mod 8 ) ∈ { 1 , 7 } , 1 , - 1 ) ) , ( ( ( ( 𝐴 ↑ ( ( 𝑛 − 1 ) / 2 ) ) + 1 ) mod 𝑛 ) − 1 ) ) ↑ ( 𝑛 pCnt 𝑁 ) ) , 1 ) ) ) ‘ ( abs ‘ 𝑁 ) ) ) ) = ( if ( ( 𝑁 < 0 ∧ 𝐴 < 0 ) , - 1 , 1 ) · ( seq 1 ( · , ( 𝑛 ∈ ℕ ↦ if ( 𝑛 ∈ ℙ , ( if ( 𝑛 = 2 , if ( 2 ∥ 𝐴 , 0 , if ( ( 𝐴 mod 8 ) ∈ { 1 , 7 } , 1 , - 1 ) ) , ( ( ( ( 𝐴 ↑ ( ( 𝑛 − 1 ) / 2 ) ) + 1 ) mod 𝑛 ) − 1 ) ) ↑ ( 𝑛 pCnt 𝑁 ) ) , 1 ) ) ) ‘ ( abs ‘ 𝑁 ) ) ) )
8	2	lgsval4lem	⊢ ( ( 𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0 ) → ( 𝑛 ∈ ℕ ↦ if ( 𝑛 ∈ ℙ , ( if ( 𝑛 = 2 , if ( 2 ∥ 𝐴 , 0 , if ( ( 𝐴 mod 8 ) ∈ { 1 , 7 } , 1 , - 1 ) ) , ( ( ( ( 𝐴 ↑ ( ( 𝑛 − 1 ) / 2 ) ) + 1 ) mod 𝑛 ) − 1 ) ) ↑ ( 𝑛 pCnt 𝑁 ) ) , 1 ) ) = ( 𝑛 ∈ ℕ ↦ if ( 𝑛 ∈ ℙ , ( ( 𝐴 /L 𝑛 ) ↑ ( 𝑛 pCnt 𝑁 ) ) , 1 ) ) )
9	8 1	eqtr4di	⊢ ( ( 𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0 ) → ( 𝑛 ∈ ℕ ↦ if ( 𝑛 ∈ ℙ , ( if ( 𝑛 = 2 , if ( 2 ∥ 𝐴 , 0 , if ( ( 𝐴 mod 8 ) ∈ { 1 , 7 } , 1 , - 1 ) ) , ( ( ( ( 𝐴 ↑ ( ( 𝑛 − 1 ) / 2 ) ) + 1 ) mod 𝑛 ) − 1 ) ) ↑ ( 𝑛 pCnt 𝑁 ) ) , 1 ) ) = 𝐹 )
10	9	seqeq3d	⊢ ( ( 𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0 ) → seq 1 ( · , ( 𝑛 ∈ ℕ ↦ if ( 𝑛 ∈ ℙ , ( if ( 𝑛 = 2 , if ( 2 ∥ 𝐴 , 0 , if ( ( 𝐴 mod 8 ) ∈ { 1 , 7 } , 1 , - 1 ) ) , ( ( ( ( 𝐴 ↑ ( ( 𝑛 − 1 ) / 2 ) ) + 1 ) mod 𝑛 ) − 1 ) ) ↑ ( 𝑛 pCnt 𝑁 ) ) , 1 ) ) ) = seq 1 ( · , 𝐹 ) )
11	10	fveq1d	⊢ ( ( 𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0 ) → ( seq 1 ( · , ( 𝑛 ∈ ℕ ↦ if ( 𝑛 ∈ ℙ , ( if ( 𝑛 = 2 , if ( 2 ∥ 𝐴 , 0 , if ( ( 𝐴 mod 8 ) ∈ { 1 , 7 } , 1 , - 1 ) ) , ( ( ( ( 𝐴 ↑ ( ( 𝑛 − 1 ) / 2 ) ) + 1 ) mod 𝑛 ) − 1 ) ) ↑ ( 𝑛 pCnt 𝑁 ) ) , 1 ) ) ) ‘ ( abs ‘ 𝑁 ) ) = ( seq 1 ( · , 𝐹 ) ‘ ( abs ‘ 𝑁 ) ) )
12	11	oveq2d	⊢ ( ( 𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0 ) → ( if ( ( 𝑁 < 0 ∧ 𝐴 < 0 ) , - 1 , 1 ) · ( seq 1 ( · , ( 𝑛 ∈ ℕ ↦ if ( 𝑛 ∈ ℙ , ( if ( 𝑛 = 2 , if ( 2 ∥ 𝐴 , 0 , if ( ( 𝐴 mod 8 ) ∈ { 1 , 7 } , 1 , - 1 ) ) , ( ( ( ( 𝐴 ↑ ( ( 𝑛 − 1 ) / 2 ) ) + 1 ) mod 𝑛 ) − 1 ) ) ↑ ( 𝑛 pCnt 𝑁 ) ) , 1 ) ) ) ‘ ( abs ‘ 𝑁 ) ) ) = ( if ( ( 𝑁 < 0 ∧ 𝐴 < 0 ) , - 1 , 1 ) · ( seq 1 ( · , 𝐹 ) ‘ ( abs ‘ 𝑁 ) ) ) )
13	4 7 12	3eqtrd	⊢ ( ( 𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0 ) → ( 𝐴 /L 𝑁 ) = ( if ( ( 𝑁 < 0 ∧ 𝐴 < 0 ) , - 1 , 1 ) · ( seq 1 ( · , 𝐹 ) ‘ ( abs ‘ 𝑁 ) ) ) )