---

Step * of Lemma subtract-is-int-iff

∀[a,b:Base].  uiff(a - b ∈ ℤ;(a ∈ ℤ) ∧ (b ∈ ℤ))
BY
{ ((UnivCD THENA Auto) THEN Unfold `subtract` 0 THEN RWW "add-is-int-iff minus-is-int-iff" 0 THEN Auto) }

---

Latex:

---

Latex:
\mforall{}[a,b:Base].    uiff(a  -  b  \mmember{}  \mBbbZ{};(a  \mmember{}  \mBbbZ{})  \mwedge{}  (b  \mmember{}  \mBbbZ{}))


By

---

Latex:
((UnivCD  THENA  Auto)
  THEN  Unfold  `subtract`  0
  THEN  RWW  "add-is-int-iff  minus-is-int-iff"  0
  THEN  Auto)

---

Home Index