---

Step * of Lemma exp-ge-1

∀[b:{2...}]. ∀[j:ℕ+].  1 < b^j
BY
{ InductionOnNat }

1
.....basecase..... 
1. b : {2...}
2. j : ℕ+
⊢ 1 < b^1

2
.....upcase..... 
1. b : {2...}
2. j : ℤ
3. 0 < j
4. 1 < b^j
⊢ 1 < b^j + 1

---

Latex:

---

Latex:
\mforall{}[b:\{2...\}].  \mforall{}[j:\mBbbN{}\msupplus{}].    1  <  b\^{}j


By

---

Latex:
InductionOnNat

---

Home Index