---

Step * 2 of Lemma assert-isOdd


1. n : ℤ@i
2. ∃k:ℤ. (n = ((2 * k) + 1) ∈ ℤ)@i
⊢ ↑isOdd(n)
BY
{ (ExRepD
   THEN HypSubst' (-1) 0
   THEN RepUR ``isOdd`` 0
   THEN InstLemma `modulus-equal-iff-eqmod` [⌜(2 * k) + 1⌝;⌜1⌝;⌜2⌝]⋅
   THEN Auto
   THEN (D -1 THENA (With ⌜k⌝ (D 0)⋅ THEN Auto))
   THEN HypSubst' (-1) 0
   THEN RepUR ``modulus`` 0
   THEN Auto)⋅ }

---

Latex:

---

Latex:

1.  n  :  \mBbbZ{}@i
2.  \mexists{}k:\mBbbZ{}.  (n  =  ((2  *  k)  +  1))@i
\mvdash{}  \muparrow{}isOdd(n)


By

---

Latex:
(ExRepD
  THEN  HypSubst'  (-1)  0
  THEN  RepUR  ``isOdd``  0
  THEN  InstLemma  `modulus-equal-iff-eqmod`  [\mkleeneopen{}(2  *  k)  +  1\mkleeneclose{};\mkleeneopen{}1\mkleeneclose{};\mkleeneopen{}2\mkleeneclose{}]\mcdot{}
  THEN  Auto
  THEN  (D  -1  THENA  (With  \mkleeneopen{}k\mkleeneclose{}  (D  0)\mcdot{}  THEN  Auto))
  THEN  HypSubst'  (-1)  0
  THEN  RepUR  ``modulus``  0
  THEN  Auto)\mcdot{}

---

Home Index