---

Step * of Lemma absval-positive

∀[x:ℤ]. uiff(0 < |x|;x ≠ 0)
BY
{ ((UnivCD THENA Auto) THEN (RWO "absval_unfold" 0 THENA Auto) THEN AutoSplit THEN Auto') }

1
1. x : ℤ
2. ¬-1 < x
3. x ≠ 0
⊢ 0 < -x

---

Latex:

---

Latex:
\mforall{}[x:\mBbbZ{}].  uiff(0  <  |x|;x  \mneq{}  0)


By

---

Latex:
((UnivCD  THENA  Auto)  THEN  (RWO  "absval\_unfold"  0  THENA  Auto)  THEN  AutoSplit  THEN  Auto')

---

Home Index