---

Step * of Lemma absval_wf

∀[x:ℤ]. (|x| ∈ ℕ)
BY
{ ((D 0 THENA Auto) THEN RWO "absval_unfold2" 0 THEN Auto) }

1
1. x : ℤ
2. 0 ∈ ℤ
3. x ∈ ℤ
4. ¬0 < x
⊢ -x ∈ ℕ

---

Latex:

---

Latex:
\mforall{}[x:\mBbbZ{}].  (|x|  \mmember{}  \mBbbN{})


By

---

Latex:
((D  0  THENA  Auto)  THEN  RWO  "absval\_unfold2"  0  THEN  Auto)

---

Home Index