---

Step * of Lemma rnexp-convex2

∀a,b:ℝ.  ((r0 ≤ a) ⇒ (r0 ≤ b) ⇒ (∀n:ℕ+. (|a - b|^n ≤ |a^n - b^n|)))
BY
{ (Auto THEN (InstLemma `rnexp-convex` [⌜rmax(a;b)⌝;⌜rmin(a;b)⌝;⌜n⌝]⋅ THENA Auto)) }

1
1. a : ℝ@i
2. b : ℝ@i
3. r0 ≤ a@i
4. r0 ≤ b@i
5. n : ℕ+@i
6. rmax(a;b) - rmin(a;b)^n ≤ (rmax(a;b)^n - rmin(a;b)^n)
⊢ |a - b|^n ≤ |a^n - b^n|

---

Latex:

---

Latex:
\mforall{}a,b:\mBbbR{}.    ((r0  \mleq{}  a)  {}\mRightarrow{}  (r0  \mleq{}  b)  {}\mRightarrow{}  (\mforall{}n:\mBbbN{}\msupplus{}.  (|a  -  b|\^{}n  \mleq{}  |a\^{}n  -  b\^{}n|)))


By

---

Latex:
(Auto  THEN  (InstLemma  `rnexp-convex`  [\mkleeneopen{}rmax(a;b)\mkleeneclose{};\mkleeneopen{}rmin(a;b)\mkleeneclose{};\mkleeneopen{}n\mkleeneclose{}]\mcdot{}  THENA  Auto))

---

Home Index