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