Theorem lgsval4a

Description: Same as lgsval4 for positive N . (Contributed by Mario Carneiro, 4-Feb-2015)

	Ref	Expression
Hypothesis	lgsval4.1	⊢ 𝐹 = ( 𝑛 ∈ ℕ ↦ if ( 𝑛 ∈ ℙ , ( ( 𝐴 /L 𝑛 ) ↑ ( 𝑛 pCnt 𝑁 ) ) , 1 ) )
Assertion	lgsval4a	⊢ ( ( 𝐴 ∈ ℤ ∧ 𝑁 ∈ ℕ ) → ( 𝐴 /L 𝑁 ) = ( seq 1 ( · , 𝐹 ) ‘ 𝑁 ) )

Proof

Step	Hyp	Ref	Expression
1		lgsval4.1	⊢ 𝐹 = ( 𝑛 ∈ ℕ ↦ if ( 𝑛 ∈ ℙ , ( ( 𝐴 /L 𝑛 ) ↑ ( 𝑛 pCnt 𝑁 ) ) , 1 ) )
2		simpl	⊢ ( ( 𝐴 ∈ ℤ ∧ 𝑁 ∈ ℕ ) → 𝐴 ∈ ℤ )
3		nnz	⊢ ( 𝑁 ∈ ℕ → 𝑁 ∈ ℤ )
4	3	adantl	⊢ ( ( 𝐴 ∈ ℤ ∧ 𝑁 ∈ ℕ ) → 𝑁 ∈ ℤ )
5		nnne0	⊢ ( 𝑁 ∈ ℕ → 𝑁 ≠ 0 )
6	5	adantl	⊢ ( ( 𝐴 ∈ ℤ ∧ 𝑁 ∈ ℕ ) → 𝑁 ≠ 0 )
7	1	lgsval4	⊢ ( ( 𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0 ) → ( 𝐴 /L 𝑁 ) = ( if ( ( 𝑁 < 0 ∧ 𝐴 < 0 ) , - 1 , 1 ) · ( seq 1 ( · , 𝐹 ) ‘ ( abs ‘ 𝑁 ) ) ) )
8	2 4 6 7	syl3anc	⊢ ( ( 𝐴 ∈ ℤ ∧ 𝑁 ∈ ℕ ) → ( 𝐴 /L 𝑁 ) = ( if ( ( 𝑁 < 0 ∧ 𝐴 < 0 ) , - 1 , 1 ) · ( seq 1 ( · , 𝐹 ) ‘ ( abs ‘ 𝑁 ) ) ) )
9		nngt0	⊢ ( 𝑁 ∈ ℕ → 0 < 𝑁 )
10	9	adantl	⊢ ( ( 𝐴 ∈ ℤ ∧ 𝑁 ∈ ℕ ) → 0 < 𝑁 )
11		0re	⊢ 0 ∈ ℝ
12		nnre	⊢ ( 𝑁 ∈ ℕ → 𝑁 ∈ ℝ )
13	12	adantl	⊢ ( ( 𝐴 ∈ ℤ ∧ 𝑁 ∈ ℕ ) → 𝑁 ∈ ℝ )
14		ltnsym	⊢ ( ( 0 ∈ ℝ ∧ 𝑁 ∈ ℝ ) → ( 0 < 𝑁 → ¬ 𝑁 < 0 ) )
15	11 13 14	sylancr	⊢ ( ( 𝐴 ∈ ℤ ∧ 𝑁 ∈ ℕ ) → ( 0 < 𝑁 → ¬ 𝑁 < 0 ) )
16	10 15	mpd	⊢ ( ( 𝐴 ∈ ℤ ∧ 𝑁 ∈ ℕ ) → ¬ 𝑁 < 0 )
17	16	intnanrd	⊢ ( ( 𝐴 ∈ ℤ ∧ 𝑁 ∈ ℕ ) → ¬ ( 𝑁 < 0 ∧ 𝐴 < 0 ) )
18	17	iffalsed	⊢ ( ( 𝐴 ∈ ℤ ∧ 𝑁 ∈ ℕ ) → if ( ( 𝑁 < 0 ∧ 𝐴 < 0 ) , - 1 , 1 ) = 1 )
19		nnnn0	⊢ ( 𝑁 ∈ ℕ → 𝑁 ∈ ℕ0 )
20	19	adantl	⊢ ( ( 𝐴 ∈ ℤ ∧ 𝑁 ∈ ℕ ) → 𝑁 ∈ ℕ0 )
21	20	nn0ge0d	⊢ ( ( 𝐴 ∈ ℤ ∧ 𝑁 ∈ ℕ ) → 0 ≤ 𝑁 )
22	13 21	absidd	⊢ ( ( 𝐴 ∈ ℤ ∧ 𝑁 ∈ ℕ ) → ( abs ‘ 𝑁 ) = 𝑁 )
23	22	fveq2d	⊢ ( ( 𝐴 ∈ ℤ ∧ 𝑁 ∈ ℕ ) → ( seq 1 ( · , 𝐹 ) ‘ ( abs ‘ 𝑁 ) ) = ( seq 1 ( · , 𝐹 ) ‘ 𝑁 ) )
24	18 23	oveq12d	⊢ ( ( 𝐴 ∈ ℤ ∧ 𝑁 ∈ ℕ ) → ( if ( ( 𝑁 < 0 ∧ 𝐴 < 0 ) , - 1 , 1 ) · ( seq 1 ( · , 𝐹 ) ‘ ( abs ‘ 𝑁 ) ) ) = ( 1 · ( seq 1 ( · , 𝐹 ) ‘ 𝑁 ) ) )
25		simpr	⊢ ( ( 𝐴 ∈ ℤ ∧ 𝑁 ∈ ℕ ) → 𝑁 ∈ ℕ )
26		nnuz	⊢ ℕ = ( ℤ≥ ‘ 1 )
27	25 26	eleqtrdi	⊢ ( ( 𝐴 ∈ ℤ ∧ 𝑁 ∈ ℕ ) → 𝑁 ∈ ( ℤ≥ ‘ 1 ) )
28	1	lgsfcl3	⊢ ( ( 𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0 ) → 𝐹 : ℕ ⟶ ℤ )
29	2 4 6 28	syl3anc	⊢ ( ( 𝐴 ∈ ℤ ∧ 𝑁 ∈ ℕ ) → 𝐹 : ℕ ⟶ ℤ )
30		elfznn	⊢ ( 𝑥 ∈ ( 1 ... 𝑁 ) → 𝑥 ∈ ℕ )
31		ffvelrn	⊢ ( ( 𝐹 : ℕ ⟶ ℤ ∧ 𝑥 ∈ ℕ ) → ( 𝐹 ‘ 𝑥 ) ∈ ℤ )
32	29 30 31	syl2an	⊢ ( ( ( 𝐴 ∈ ℤ ∧ 𝑁 ∈ ℕ ) ∧ 𝑥 ∈ ( 1 ... 𝑁 ) ) → ( 𝐹 ‘ 𝑥 ) ∈ ℤ )
33		zmulcl	⊢ ( ( 𝑥 ∈ ℤ ∧ 𝑦 ∈ ℤ ) → ( 𝑥 · 𝑦 ) ∈ ℤ )
34	33	adantl	⊢ ( ( ( 𝐴 ∈ ℤ ∧ 𝑁 ∈ ℕ ) ∧ ( 𝑥 ∈ ℤ ∧ 𝑦 ∈ ℤ ) ) → ( 𝑥 · 𝑦 ) ∈ ℤ )
35	27 32 34	seqcl	⊢ ( ( 𝐴 ∈ ℤ ∧ 𝑁 ∈ ℕ ) → ( seq 1 ( · , 𝐹 ) ‘ 𝑁 ) ∈ ℤ )
36	35	zcnd	⊢ ( ( 𝐴 ∈ ℤ ∧ 𝑁 ∈ ℕ ) → ( seq 1 ( · , 𝐹 ) ‘ 𝑁 ) ∈ ℂ )
37	36	mulid2d	⊢ ( ( 𝐴 ∈ ℤ ∧ 𝑁 ∈ ℕ ) → ( 1 · ( seq 1 ( · , 𝐹 ) ‘ 𝑁 ) ) = ( seq 1 ( · , 𝐹 ) ‘ 𝑁 ) )
38	8 24 37	3eqtrd	⊢ ( ( 𝐴 ∈ ℤ ∧ 𝑁 ∈ ℕ ) → ( 𝐴 /L 𝑁 ) = ( seq 1 ( · , 𝐹 ) ‘ 𝑁 ) )