---

Step * 1 1 of Lemma expfact-property

.....antecedent..... 
1. k : ℕ@i
2. n : ℕ+@i
3. m : ℕ
4. n * k^m < (m)!
⊢ 1 ≤ m
BY
{ (CaseNat 0 `m' THEN Auto THEN HypSubst' (-1) (-2)) }

1
1. k : ℕ@i
2. n : ℕ+@i
3. m : ℕ
4. n * k^0 < (0)!
5. m = 0 ∈ ℤ
⊢ 1 ≤ 0

---

Latex:

---

Latex:
.....antecedent..... 
1.  k  :  \mBbbN{}@i
2.  n  :  \mBbbN{}\msupplus{}@i
3.  m  :  \mBbbN{}
4.  n  *  k\^{}m  <  (m)!
\mvdash{}  1  \mleq{}  m


By

---

Latex:
(CaseNat  0  `m'  THEN  Auto  THEN  HypSubst'  (-1)  (-2))

---

Home Index