---

Step * of Lemma mul_positive

∀a,b:ℤ.  (0 < a ⇒ 0 < b ⇒ 0 < a * b)
BY
{ (TACTIC:(UnivCD THENA Auto) THEN D 0 THEN Auto THEN UnfoldTopAb 0) }

1
1. a : ℤ@i
2. b : ℤ@i
3. 0 < a
4. 0 < b
⊢ if (0) < (a * b)  then True  else False

---

Latex:

---

Latex:
\mforall{}a,b:\mBbbZ{}.    (0  <  a  {}\mRightarrow{}  0  <  b  {}\mRightarrow{}  0  <  a  *  b)


By

---

Latex:
(TACTIC:(UnivCD  THENA  Auto)  THEN  D  0  THEN  Auto  THEN  UnfoldTopAb  0)

---

Home Index