---

Step * 1 of Lemma biject-int-nat


1. a1 : ℤ
2. a2 : ℤ
3. if 0 ≤z a1 then 2 * a1 else (2 * ((-a1) - 1)) + 1 fi  = if 0 ≤z a2 then 2 * a2 else (2 * ((-a2) - 1)) + 1 fi  ∈ ℕ
⊢ a1 = a2 ∈ ℤ
BY
{ (MoveToConcl (-1) THEN RepeatFor 2 (AutoSplit) THEN Auto') }

---

Latex:

---

Latex:

1.  a1  :  \mBbbZ{}
2.  a2  :  \mBbbZ{}
3.  if  0  \mleq{}z  a1  then  2  *  a1  else  (2  *  ((-a1)  -  1))  +  1  fi 
=  if  0  \mleq{}z  a2  then  2  *  a2  else  (2  *  ((-a2)  -  1))  +  1  fi 
\mvdash{}  a1  =  a2


By

---

Latex:
(MoveToConcl  (-1)  THEN  RepeatFor  2  (AutoSplit)  THEN  Auto')

---

Home Index