Step * of Lemma odd-implies-succ-two-times

n:ℕ((↑isOdd(n))  (∃k:ℕ(n ((2 k) 1) ∈ ℤ)))
BY
Auto }

1
1. : ℕ@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