---

Step * of Lemma assert-isOdd

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

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

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

---

Latex:

---

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


By

---

Latex:
Auto

---

Home Index