Step
*
of Lemma
odd-implies-succ-two-times
∀n:ℕ. ((↑isOdd(n)) 
⇒ (∃k:ℕ. (n = ((2 * k) + 1) ∈ ℤ)))
BY
{ Auto }
1
1. n : ℕ@i
2. ↑isOdd(n)@i
⊢ ∃k:ℕ. (n = ((2 * k) + 1) ∈ ℤ)
Latex:
Latex:
\mforall{}n:\mBbbN{}.  ((\muparrow{}isOdd(n))  {}\mRightarrow{}  (\mexists{}k:\mBbbN{}.  (n  =  ((2  *  k)  +  1))))
By
Latex:
Auto
Home
Index