---

Step * of Lemma minus-is-int-iff

∀[a:Base]. uiff(-a ∈ ℤ;a ∈ ℤ)
BY
{ TACTIC:((UnivCD THENA Auto) THEN RepeatFor 2 ((D 0 THENA Auto))) }

1
1. a : Base
2. -a ∈ ℤ
⊢ a ∈ ℤ

2
1. a : Base
2. a ∈ ℤ
⊢ -a ∈ ℤ

---

Latex:

---

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


By

---

Latex:
TACTIC:((UnivCD  THENA  Auto)  THEN  RepeatFor  2  ((D  0  THENA  Auto)))

---

Home Index