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