---

Step * of Lemma exp-greater

∀[x:{2...}]. ∀[n:ℕ].  n < x^n
BY
{ (InductionOnNat
   THEN Reduce 0
   THEN Auto
   THEN RWO "exp1 exp_step" 0
   THEN Auto
   THEN InstLemma `mul_preserves_lt` [⌜n - 1⌝;⌜x^n - 1⌝;⌜x⌝]⋅
   THEN Auto
   THEN CaseNat 1 `n'⋅
   THEN Reduce 0
   THEN Auto'
   THEN Assert ⌜((n - 1) + 1) ≤ (x * (n - 1))⌝⋅
   THEN Auto'
   THEN GenConcl ⌜(n - 1) = m ∈ ℕ+⌝⋅
   THEN Auto
   THEN All Thin) }

1
1. x : {2...}
2. m : ℕ+
⊢ (m + 1) ≤ (x * m)

---

Latex:

---

Latex:
\mforall{}[x:\{2...\}].  \mforall{}[n:\mBbbN{}].    n  <  x\^{}n


By

---

Latex:
(InductionOnNat
  THEN  Reduce  0
  THEN  Auto
  THEN  RWO  "exp1  exp\_step"  0
  THEN  Auto
  THEN  InstLemma  `mul\_preserves\_lt`  [\mkleeneopen{}n  -  1\mkleeneclose{};\mkleeneopen{}x\^{}n  -  1\mkleeneclose{};\mkleeneopen{}x\mkleeneclose{}]\mcdot{}
  THEN  Auto
  THEN  CaseNat  1  `n'\mcdot{}
  THEN  Reduce  0
  THEN  Auto'
  THEN  Assert  \mkleeneopen{}((n  -  1)  +  1)  \mleq{}  (x  *  (n  -  1))\mkleeneclose{}\mcdot{}
  THEN  Auto'
  THEN  GenConcl  \mkleeneopen{}(n  -  1)  =  m\mkleeneclose{}\mcdot{}
  THEN  Auto
  THEN  All  Thin)

---

Home Index