lgsval4a

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

		Ref	Expression
	Hypothesis	lgsval4.1	$⊢ F = (n \in ℕ ⟼ if (n \in ℙ, {(A /_{L} n)}^{n pCnt N}, 1))$
	Assertion	lgsval4a	$⊢ (A \in ℤ \land N \in ℕ) \to A /_{L} N = seq 1 (\times F) (N)$

Proof

Step	Hyp	Ref	Expression
1		lgsval4.1	$⊢ F = (n \in ℕ ⟼ if (n \in ℙ, {(A /_{L} n)}^{n pCnt N}, 1))$
2		simpl	$⊢ (A \in ℤ \land N \in ℕ) \to A \in ℤ$
3		nnz	$⊢ N \in ℕ \to N \in ℤ$
4	3	adantl	$⊢ (A \in ℤ \land N \in ℕ) \to N \in ℤ$
5		nnne0	$⊢ N \in ℕ \to N \neq 0$
6	5	adantl	$⊢ (A \in ℤ \land N \in ℕ) \to N \neq 0$
7	1	lgsval4	$⊢ (A \in ℤ \land N \in ℤ \land N \neq 0) \to A /_{L} N = if ((N < 0 \land A < 0), - 1, 1) seq 1 (\times F) (\|N\|)$
8	2 4 6 7	syl3anc	$⊢ (A \in ℤ \land N \in ℕ) \to A /_{L} N = if ((N < 0 \land A < 0), - 1, 1) seq 1 (\times F) (\|N\|)$
9		nngt0	$⊢ N \in ℕ \to 0 < N$
10	9	adantl	$⊢ (A \in ℤ \land N \in ℕ) \to 0 < N$
11		0re	$⊢ 0 \in ℝ$
12		nnre	$⊢ N \in ℕ \to N \in ℝ$
13	12	adantl	$⊢ (A \in ℤ \land N \in ℕ) \to N \in ℝ$
14		ltnsym	$⊢ (0 \in ℝ \land N \in ℝ) \to (0 < N \to \neg N < 0)$
15	11 13 14	sylancr	$⊢ (A \in ℤ \land N \in ℕ) \to (0 < N \to \neg N < 0)$
16	10 15	mpd	$⊢ (A \in ℤ \land N \in ℕ) \to \neg N < 0$
17	16	intnanrd	$⊢ (A \in ℤ \land N \in ℕ) \to \neg (N < 0 \land A < 0)$
18	17	iffalsed	$⊢ (A \in ℤ \land N \in ℕ) \to if ((N < 0 \land A < 0), - 1, 1) = 1$
19		nnnn0	$⊢ N \in ℕ \to N \in ℕ_{0}$
20	19	adantl	$⊢ (A \in ℤ \land N \in ℕ) \to N \in ℕ_{0}$
21	20	nn0ge0d	$⊢ (A \in ℤ \land N \in ℕ) \to 0 \leq N$
22	13 21	absidd	$⊢ (A \in ℤ \land N \in ℕ) \to \|N\| = N$
23	22	fveq2d	$⊢ (A \in ℤ \land N \in ℕ) \to seq 1 (\times F) (\|N\|) = seq 1 (\times F) (N)$
24	18 23	oveq12d	$⊢ (A \in ℤ \land N \in ℕ) \to if ((N < 0 \land A < 0), - 1, 1) seq 1 (\times F) (\|N\|) = 1 seq 1 (\times F) (N)$
25		simpr	$⊢ (A \in ℤ \land N \in ℕ) \to N \in ℕ$
26		nnuz	$⊢ ℕ = ℤ_{\geq 1}$
27	25 26	eleqtrdi	$⊢ (A \in ℤ \land N \in ℕ) \to N \in ℤ_{\geq 1}$
28	1	lgsfcl3	$⊢ (A \in ℤ \land N \in ℤ \land N \neq 0) \to F : ℕ ⟶ ℤ$
29	2 4 6 28	syl3anc	$⊢ (A \in ℤ \land N \in ℕ) \to F : ℕ ⟶ ℤ$
30		elfznn	$⊢ x \in (1 \dots N) \to x \in ℕ$
31		ffvelcdm	$⊢ (F : ℕ ⟶ ℤ \land x \in ℕ) \to F (x) \in ℤ$
32	29 30 31	syl2an	$⊢ ((A \in ℤ \land N \in ℕ) \land x \in (1 \dots N)) \to F (x) \in ℤ$
33		zmulcl	$⊢ (x \in ℤ \land y \in ℤ) \to x y \in ℤ$
34	33	adantl	$⊢ ((A \in ℤ \land N \in ℕ) \land (x \in ℤ \land y \in ℤ)) \to x y \in ℤ$
35	27 32 34	seqcl	$⊢ (A \in ℤ \land N \in ℕ) \to seq 1 (\times F) (N) \in ℤ$
36	35	zcnd	$⊢ (A \in ℤ \land N \in ℕ) \to seq 1 (\times F) (N) \in ℂ$
37	36	mullidd	$⊢ (A \in ℤ \land N \in ℕ) \to 1 seq 1 (\times F) (N) = seq 1 (\times F) (N)$
38	8 24 37	3eqtrd	$⊢ (A \in ℤ \land N \in ℕ) \to A /_{L} N = seq 1 (\times F) (N)$

Metamath Proof Explorer

Theorem lgsval4a

Proof