---

Step * 1 1 1 1 of Lemma int-bag-product-positive


1. u : ℤ
2. v : ℤ List
3. (∀[x:ℤ]. ((x ∈ v) ⇒ 0 < x))
⇒ (∀n:ℕ+. 0 < accumulate (with value c and list item x): x * cover list:  vwith starting value: n))
4. ∀[x:ℤ]. ((x ∈ [u / v]) ⇒ 0 < x)
5. n : ℕ+
⊢ 0 < accumulate (with value c and list item x):
       x * c
      over list:
        v
      with starting value:
       u * n)
BY
{ BHyp 3 }

1
1. u : ℤ
2. v : ℤ List
3. (∀[x:ℤ]. ((x ∈ v) ⇒ 0 < x))
⇒ (∀n:ℕ+. 0 < accumulate (with value c and list item x): x * cover list:  vwith starting value: n))
4. ∀[x:ℤ]. ((x ∈ [u / v]) ⇒ 0 < x)
5. n : ℕ+
⊢ ∀[x:ℤ]. ((x ∈ v) ⇒ 0 < x)

2
.....wf..... 
1. u : ℤ
2. v : ℤ List
3. (∀[x:ℤ]. ((x ∈ v) ⇒ 0 < x))
⇒ (∀n:ℕ+. 0 < accumulate (with value c and list item x): x * cover list:  vwith starting value: n))
4. ∀[x:ℤ]. ((x ∈ [u / v]) ⇒ 0 < x)
5. n : ℕ+
⊢ u * n ∈ ℕ+

---

Latex:

---

Latex:

1.  u  :  \mBbbZ{}
2.  v  :  \mBbbZ{}  List
3.  (\mforall{}[x:\mBbbZ{}].  ((x  \mmember{}  v)  {}\mRightarrow{}  0  <  x))
{}\mRightarrow{}  (\mforall{}n:\mBbbN{}\msupplus{}.  0  <  accumulate  (with  value  c  and  list  item  x):  x  *  cover  list:    vwith  starting  value:  n))
4.  \mforall{}[x:\mBbbZ{}].  ((x  \mmember{}  [u  /  v])  {}\mRightarrow{}  0  <  x)
5.  n  :  \mBbbN{}\msupplus{}
\mvdash{}  0  <  accumulate  (with  value  c  and  list  item  x):
              x  *  c
            over  list:
                v
            with  starting  value:
              u  *  n)


By

---

Latex:
BHyp  3

---

Home Index