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