---

Step * 1 1 1 of Lemma minus-one-mul


1. x : ℤ
⊢ (x + ((-1) * x)) = 0 ∈ ℤ
BY
{ (InstLemma `mul-distributes-right` [⌜x⌝;⌜1⌝;⌜-1⌝]⋅ THENA Trivial) }

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

---

Latex:

---

Latex:

1.  x  :  \mBbbZ{}
\mvdash{}  (x  +  ((-1)  *  x))  =  0


By

---

Latex:
(InstLemma  `mul-distributes-right`  [\mkleeneopen{}x\mkleeneclose{};\mkleeneopen{}1\mkleeneclose{};\mkleeneopen{}-1\mkleeneclose{}]\mcdot{}  THENA  Trivial)

---

Home Index