---

Step * 1 of Lemma mul-list-positive


1. u : ℕ+
2. v : ℕ+ List
3. 0 < Π(v) 
⊢ 0 < Π([u / v]) 
BY
{ (Subst' Π([u / v])  ~ u * Π(v)  0 THEN Auto) }

---

Latex:

---

Latex:

1.  u  :  \mBbbN{}\msupplus{}
2.  v  :  \mBbbN{}\msupplus{}  List
3.  0  <  \mPi{}(v) 
\mvdash{}  0  <  \mPi{}([u  /  v]) 


By

---

Latex:
(Subst'  \mPi{}([u  /  v])    \msim{}  u  *  \mPi{}(v)    0  THEN  Auto)

---

Home Index