Metamath Proof Explorer

Theorem lgsval4a

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

Ref Expression
Hypothesis lgsval4.1 ⊢ F = n ∈ ℕ ⟼ if n ∈ ℙ A / L n n pCnt N 1
Assertion lgsval4a ⊢ A ∈ ℤ ∧ N ∈ ℕ → A / L N = seq 1 × F ⁡ N

Proof

Step Hyp Ref Expression
1 lgsval4.1 ⊢ F = n ∈ ℕ ⟼ if n ∈ ℙ A / L n n pCnt N 1
2 simpl ⊢ A ∈ ℤ ∧ N ∈ ℕ → A ∈ ℤ
3 nnz ⊢ N ∈ ℕ → N ∈ ℤ
4 3 adantl ⊢ A ∈ ℤ ∧ N ∈ ℕ → N ∈ ℤ
5 nnne0 ⊢ N ∈ ℕ → N ≠ 0
6 5 adantl ⊢ A ∈ ℤ ∧ N ∈ ℕ → N ≠ 0
7 1 lgsval4 ⊢ A ∈ ℤ ∧ N ∈ ℤ ∧ N ≠ 0 → A / L N = if N < 0 ∧ A < 0 − 1 1 ⁢ seq 1 × F ⁡ N
8 2 4 6 7 syl3anc ⊢ A ∈ ℤ ∧ N ∈ ℕ → A / L N = if N < 0 ∧ A < 0 − 1 1 ⁢ seq 1 × F ⁡ N
9 nngt0 ⊢ N ∈ ℕ → 0 < N
10 9 adantl ⊢ A ∈ ℤ ∧ N ∈ ℕ → 0 < N
11 0re ⊢ 0 ∈ ℝ
12 nnre ⊢ N ∈ ℕ → N ∈ ℝ
13 12 adantl ⊢ A ∈ ℤ ∧ N ∈ ℕ → N ∈ ℝ
14 ltnsym ⊢ 0 ∈ ℝ ∧ N ∈ ℝ → 0 < N → ¬ N < 0
15 11 13 14 sylancr ⊢ A ∈ ℤ ∧ N ∈ ℕ → 0 < N → ¬ N < 0
16 10 15 mpd ⊢ A ∈ ℤ ∧ N ∈ ℕ → ¬ N < 0
17 16 intnanrd ⊢ A ∈ ℤ ∧ N ∈ ℕ → ¬ N < 0 ∧ A < 0
18 17 iffalsed ⊢ A ∈ ℤ ∧ N ∈ ℕ → if N < 0 ∧ A < 0 − 1 1 = 1
19 nnnn0 ⊢ N ∈ ℕ → N ∈ ℕ 0
20 19 adantl ⊢ A ∈ ℤ ∧ N ∈ ℕ → N ∈ ℕ 0
21 20 nn0ge0d ⊢ A ∈ ℤ ∧ N ∈ ℕ → 0 ≤ N
22 13 21 absidd ⊢ A ∈ ℤ ∧ N ∈ ℕ → N = N
23 22 fveq2d ⊢ A ∈ ℤ ∧ N ∈ ℕ → seq 1 × F ⁡ N = seq 1 × F ⁡ N
24 18 23 oveq12d ⊢ A ∈ ℤ ∧ N ∈ ℕ → if N < 0 ∧ A < 0 − 1 1 ⁢ seq 1 × F ⁡ N = 1 ⁢ seq 1 × F ⁡ N
25 simpr ⊢ A ∈ ℤ ∧ N ∈ ℕ → N ∈ ℕ
26 nnuz ⊢ ℕ = ℤ ≥ 1
27 25 26 eleqtrdi ⊢ A ∈ ℤ ∧ N ∈ ℕ → N ∈ ℤ ≥ 1
28 1 lgsfcl3 ⊢ A ∈ ℤ ∧ N ∈ ℤ ∧ N ≠ 0 → F : ℕ ⟶ ℤ
29 2 4 6 28 syl3anc ⊢ A ∈ ℤ ∧ N ∈ ℕ → F : ℕ ⟶ ℤ
30 elfznn ⊢ x ∈ 1 … N → x ∈ ℕ
31 ffvelrn ⊢ F : ℕ ⟶ ℤ ∧ x ∈ ℕ → F ⁡ x ∈ ℤ
32 29 30 31 syl2an ⊢ A ∈ ℤ ∧ N ∈ ℕ ∧ x ∈ 1 … N → F ⁡ x ∈ ℤ
33 zmulcl ⊢ x ∈ ℤ ∧ y ∈ ℤ → x ⁢ y ∈ ℤ
34 33 adantl ⊢ A ∈ ℤ ∧ N ∈ ℕ ∧ x ∈ ℤ ∧ y ∈ ℤ → x ⁢ y ∈ ℤ
35 27 32 34 seqcl ⊢ A ∈ ℤ ∧ N ∈ ℕ → seq 1 × F ⁡ N ∈ ℤ
36 35 zcnd ⊢ A ∈ ℤ ∧ N ∈ ℕ → seq 1 × F ⁡ N ∈ ℂ
37 36 mulid2d ⊢ A ∈ ℤ ∧ N ∈ ℕ → 1 ⁢ seq 1 × F ⁡ N = seq 1 × F ⁡ N
38 8 24 37 3eqtrd ⊢ A ∈ ℤ ∧ N ∈ ℕ → A / L N = seq 1 × F ⁡ N