---

Step * of Lemma rexp-non-decreasing

∀[a,b:ℝ].  e^a ≤ e^b supposing a ≤ b
BY
{ (Auto THEN (InstLemma `rexp-radd` [⌜a⌝;⌜b - a⌝]⋅ THENA Auto)) }

1
1. a : ℝ
2. b : ℝ
3. a ≤ b
4. e^a + (b - a) = (e^a * e^b - a)
⊢ e^a ≤ e^b

---

Latex:

---

Latex:
\mforall{}[a,b:\mBbbR{}].    e\^{}a  \mleq{}  e\^{}b  supposing  a  \mleq{}  b


By

---

Latex:
(Auto  THEN  (InstLemma  `rexp-radd`  [\mkleeneopen{}a\mkleeneclose{};\mkleeneopen{}b  -  a\mkleeneclose{}]\mcdot{}  THENA  Auto))

---

Home Index