---

Step * 1 of Lemma absval_unfold3


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

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

---

Latex:

---

Latex:

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


By

---

Latex:
RepeatFor  2  (AutoSplit)

---

Home Index