---

Step * of Lemma even-implies-two-times

∀n:ℕ. ((↑isEven(n)) ⇒ (∃k:ℕ. (n = (2 * k) ∈ ℤ)))
BY
{ (Auto THEN (RWO "assert-isEven" (-1) THENA Auto) THEN ParallelLast THEN Auto') }

---

Latex:

---

Latex:
\mforall{}n:\mBbbN{}.  ((\muparrow{}isEven(n))  {}\mRightarrow{}  (\mexists{}k:\mBbbN{}.  (n  =  (2  *  k))))


By

---

Latex:
(Auto  THEN  (RWO  "assert-isEven"  (-1)  THENA  Auto)  THEN  ParallelLast  THEN  Auto')

---

Home Index