---

Step * of Lemma assert-isEven

∀n:ℤ. (↑isEven(n) ⇐⇒ ∃k:ℤ. (n = (2 * k) ∈ ℤ))
BY
{ TACTIC:Auto }

1
1. n : ℤ@i
2. ↑isEven(n)
⊢ ∃k:ℤ. (n = (2 * k) ∈ ℤ)

2
1. n : ℤ@i
2. ∃k:ℤ. (n = (2 * k) ∈ ℤ)
⊢ ↑isEven(n)

---

Latex:

---

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


By

---

Latex:
TACTIC:Auto

---

Home Index