---

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


1. b : bag(ℤ)
2. ∀[x:ℤ]. (x ↓∈ b ⇒ 0 < x)
⊢ 0 < Π(b)
BY
{ (BagToList 1
   THEN Auto
   THEN (RWO "bag-member-list" (-1) THENA Auto)
   THEN RepUR ``int-bag-product bag-product bag-summation bag-accum`` 0) }

1
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)

---

Latex:

---

Latex:

1.  b  :  bag(\mBbbZ{})
2.  \mforall{}[x:\mBbbZ{}].  (x  \mdownarrow{}\mmember{}  b  {}\mRightarrow{}  0  <  x)
\mvdash{}  0  <  \mPi{}(b)


By

---

Latex:
(BagToList  1
  THEN  Auto
  THEN  (RWO  "bag-member-list"  (-1)  THENA  Auto)
  THEN  RepUR  ``int-bag-product  bag-product  bag-summation  bag-accum``  0)

---

Home Index