---

Step * 2 of Lemma int2nat2int


1. i : ℤ
2. (2 * ((-i) - 1)) + 1 rem 2 ≠ 0
3. i < 0
⊢ (-((((2 * ((-i) - 1)) + 1) ÷ 2) + 1)) = i ∈ ℤ
BY
{ (Thin (-2) THEN (GenConcl ⌜((-i) - 1) = n ∈ ℕ⌝⋅ THENA Auto) THEN (Subst' i ~ -(n + 1) 0 THENA Auto) THEN All Thin) }

1
1. n : ℕ
⊢ (-((((2 * n) + 1) ÷ 2) + 1)) = (-(n + 1)) ∈ ℤ

---

Latex:

---

Latex:

1.  i  :  \mBbbZ{}
2.  (2  *  ((-i)  -  1))  +  1  rem  2  \mneq{}  0
3.  i  <  0
\mvdash{}  (-((((2  *  ((-i)  -  1))  +  1)  \mdiv{}  2)  +  1))  =  i


By

---

Latex:
(Thin  (-2)
  THEN  (GenConcl  \mkleeneopen{}((-i)  -  1)  =  n\mkleeneclose{}\mcdot{}  THENA  Auto)
  THEN  (Subst'  i  \msim{}  -(n  +  1)  0  THENA  Auto)
  THEN  All  Thin)

---

Home Index