Step
*
of Lemma
exp-2-3-fact
∀n:ℕ. ((2 ≤ n) 
⇒ 2 * 2^n < 3^n)
BY
{ (InductionOnNat THEN Auto) }
1
1. n : ℤ
2. 0 < n
3. (2 ≤ (n - 1)) 
⇒ 2 * 2^n - 1 < 3^n - 1
4. 2 ≤ n@i
⊢ 2 * 2^n < 3^n
Latex:
Latex:
\mforall{}n:\mBbbN{}.  ((2  \mleq{}  n)  {}\mRightarrow{}  2  *  2\^{}n  <  3\^{}n)
By
Latex:
(InductionOnNat  THEN  Auto)
Home
Index