---

Step * of Lemma zero-mul

∀[x:ℤ]. (0 * x ~ 0)
BY
{ ((UnivCD THENA Auto)
   THEN (Assert (0 * x) + (1 * x) ~ x BY
               ((RWO "mul-distributes-right<" 0 THENA Auto) THEN Reduce 0 THEN BLemma `one-mul` THEN Declaration))
   THEN (RWO "one-mul" (-1) THENA Auto)) }

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

---

Latex:

---

Latex:
\mforall{}[x:\mBbbZ{}].  (0  *  x  \msim{}  0)


By

---

Latex:
((UnivCD  THENA  Auto)
  THEN  (Assert  (0  *  x)  +  (1  *  x)  \msim{}  x  BY
                          ((RWO  "mul-distributes-right<"  0  THENA  Auto)
                            THEN  Reduce  0
                            THEN  BLemma  `one-mul`
                            THEN  Declaration))
  THEN  (RWO  "one-mul"  (-1)  THENA  Auto))

---

Home Index