---

Step * 1 1 of Lemma zero-mul


1. x : ℤ
2. (0 * x) + x ~ x
3. (0 * x) + x + (-x) ~ x + (-x)
⊢ 0 * x ~ 0
BY
{ ((RWW "add-inverse add-inverse2 add-zero" (-1) THENA Auto) THEN Hypothesis) }

---

Latex:

---

Latex:

1.  x  :  \mBbbZ{}
2.  (0  *  x)  +  x  \msim{}  x
3.  (0  *  x)  +  x  +  (-x)  \msim{}  x  +  (-x)
\mvdash{}  0  *  x  \msim{}  0


By

---

Latex:
((RWW  "add-inverse  add-inverse2  add-zero"  (-1)  THENA  Auto)  THEN  Hypothesis)

---

Home Index