---

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


1. b : ℤ List
2. ∀[x:ℤ]. ((x ∈ b) ⇒ 0 < x)
⊢ 0 < accumulate (with value c and list item x):
       x * c
      over list:
        b
      with starting value:
       1)
BY
{ Assert ⌜∀n:ℕ+. 0 < accumulate (with value c and list item x): x * cover list:  bwith starting value: n)⌝⋅ }

1
.....assertion..... 
1. b : ℤ List
2. ∀[x:ℤ]. ((x ∈ b) ⇒ 0 < x)
⊢ ∀n:ℕ+. 0 < accumulate (with value c and list item x): x * cover list:  bwith starting value: n)

2
1. b : ℤ List
2. ∀[x:ℤ]. ((x ∈ b) ⇒ 0 < x)
3. ∀n:ℕ+. 0 < accumulate (with value c and list item x): x * cover list:  bwith starting value: n)
⊢ 0 < accumulate (with value c and list item x):
       x * c
      over list:
        b
      with starting value:
       1)

---

Latex:

---

Latex:

1.  b  :  \mBbbZ{}  List
2.  \mforall{}[x:\mBbbZ{}].  ((x  \mmember{}  b)  {}\mRightarrow{}  0  <  x)
\mvdash{}  0  <  accumulate  (with  value  c  and  list  item  x):
              x  *  c
            over  list:
                b
            with  starting  value:
              1)


By

---

Latex:
Assert  \mkleeneopen{}\mforall{}n:\mBbbN{}\msupplus{}
                    0  <  accumulate  (with  value  c  and  list  item  x):
                              x  *  c
                            over  list:
                                b
                            with  starting  value:
                              n)\mkleeneclose{}\mcdot{}

---

Home Index