---

Step * 1 of Lemma zero-mul


1. x : ℤ
2. (0 * x) + x ~ x
⊢ 0 * x ~ 0
BY
{ ((Assert ((0 * x) + x) + (-x) ~ x + (-x) BY (EqCD THEN Trivial)) THEN (RWO "add-associates" (-1) THENA Auto)) }

1
1. x : ℤ
2. (0 * x) + x ~ x
3. (0 * x) + x + (-x) ~ x + (-x)
⊢ 0 * x ~ 0

---

Latex:

---

Latex:

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


By

---

Latex:
((Assert  ((0  *  x)  +  x)  +  (-x)  \msim{}  x  +  (-x)  BY
                (EqCD  THEN  Trivial))
  THEN  (RWO  "add-associates"  (-1)  THENA  Auto)
  )

---

Home Index