---

Step * of Lemma rnexp-convex3

∀a,b:ℝ.  ((((r0 ≤ a) ∧ (r0 ≤ b)) ∨ ((a ≤ r0) ∧ (b ≤ r0))) ⇒ (∀n:ℕ+. (|a - b|^n ≤ |a^n - b^n|)))
BY
{ (Auto
   THEN D -2
   THEN Auto
   THEN Try (Complete ((BLemma `rnexp-convex2` THEN Auto)))
   THEN (InstLemma `rnexp-convex2` [⌜-(a)⌝;⌜-(b)⌝;⌜n⌝]⋅ THENA (Auto THEN nRMul ⌜r(-1)⌝ 0⋅ THEN Auto))) }

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

---

Latex:

---

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


By

---

Latex:
(Auto
  THEN  D  -2
  THEN  Auto
  THEN  Try  (Complete  ((BLemma  `rnexp-convex2`  THEN  Auto)))
  THEN  (InstLemma  `rnexp-convex2`  [\mkleeneopen{}-(a)\mkleeneclose{};\mkleeneopen{}-(b)\mkleeneclose{};\mkleeneopen{}n\mkleeneclose{}]\mcdot{}  THENA  (Auto  THEN  nRMul  \mkleeneopen{}r(-1)\mkleeneclose{}  0\mcdot{}  THEN  Auto)))

---

Home Index