---

Step * 1 1 1 of Lemma expfact-property


1. k : ℕ
2. n : ℕ+
3. m : ℕ
4. n * k^0 < (0)!
5. m = 0 ∈ ℤ
⊢ 1 ≤ 0
BY
{ (Reduce (-2) THEN Auto') }

---

Latex:

---

Latex:

1.  k  :  \mBbbN{}
2.  n  :  \mBbbN{}\msupplus{}
3.  m  :  \mBbbN{}
4.  n  *  k\^{}0  <  (0)!
5.  m  =  0
\mvdash{}  1  \mleq{}  0


By

---

Latex:
(Reduce  (-2)  THEN  Auto')

---

Home Index