---

Step * 2 of Lemma assert-isEven


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

---

Latex:

---

Latex:

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


By

---

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

---

Home Index