---

Step * of Lemma exp-increasing

∀[b:{2...}]. ∀[i:ℕ].  ∀j:ℕ. b^i < b^j supposing i < j
BY
{ ((UnivCD THENA Auto) THEN CaseNat 0 `i') }

1
1. b : {2...}
2. i : ℕ
3. j : ℕ
4. i < j
5. i = 0 ∈ ℤ
⊢ b^0 < b^j

2
1. b : {2...}
2. i : ℕ
3. j : ℕ
4. i < j
5. ¬(i = 0 ∈ ℤ)
⊢ b^i < b^j

---

Latex:

---

Latex:
\mforall{}[b:\{2...\}].  \mforall{}[i:\mBbbN{}].    \mforall{}j:\mBbbN{}.  b\^{}i  <  b\^{}j  supposing  i  <  j


By

---

Latex:
((UnivCD  THENA  Auto)  THEN  CaseNat  0  `i')

---

Home Index