---

Step * of Lemma exp-nondecreasing

∀[b:{2...}]. ∀[i:ℕ].  ∀j:ℕ. b^i ≤ b^j supposing i ≤ j
BY
{ (Auto THEN Decide ⌜i < j⌝⋅ THEN Auto) }

1
1. b : {2...}
2. i : ℕ
3. j : ℕ
4. i ≤ j
5. i < j
⊢ b^i ≤ b^j

2
1. b : {2...}
2. i : ℕ
3. j : ℕ
4. i ≤ j
5. ¬i < j
⊢ b^i ≤ b^j

---

Latex:

---

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


By

---

Latex:
(Auto  THEN  Decide  \mkleeneopen{}i  <  j\mkleeneclose{}\mcdot{}  THEN  Auto)

---

Home Index