---

Step * 1 of Lemma absval_unfold


1. x : ℤ
⊢ if (0) < (x)  then x  else (-x) = if (-1) < (x)  then x  else (-x) ∈ ℤ
BY
{ RepeatFor 2 (AutoSplit) }

1
1. x : ℤ
2. ¬0 < x
3. -1 < x
⊢ (-x) = x ∈ ℤ

---

Latex:

---

Latex:

1.  x  :  \mBbbZ{}
\mvdash{}  if  (0)  <  (x)    then  x    else  (-x)  =  if  (-1)  <  (x)    then  x    else  (-x)


By

---

Latex:
RepeatFor  2  (AutoSplit)

---

Home Index