---

Step * 1 1 1 of Lemma rnexp-convex3


1. a : ℝ
2. b : ℝ
3. a ≤ r0
4. b ≤ r0
5. n : ℕ+
6. |a - b|^n ≤ |-(a)^n - -(b)^n|
7. |-(a) - -(b)| = |a - b|
⊢ (r(|-1|^n) * |a^n - b^n|) ≤ |a^n - b^n|
BY
{ (Unfold `absval` 0 THEN Reduce 0 THEN RWO "exp-one" 0 THEN Auto) }

---

Latex:

---

Latex:

1.  a  :  \mBbbR{}
2.  b  :  \mBbbR{}
3.  a  \mleq{}  r0
4.  b  \mleq{}  r0
5.  n  :  \mBbbN{}\msupplus{}
6.  |a  -  b|\^{}n  \mleq{}  |-(a)\^{}n  -  -(b)\^{}n|
7.  |-(a)  -  -(b)|  =  |a  -  b|
\mvdash{}  (r(|-1|\^{}n)  *  |a\^{}n  -  b\^{}n|)  \mleq{}  |a\^{}n  -  b\^{}n|


By

---

Latex:
(Unfold  `absval`  0  THEN  Reduce  0  THEN  RWO  "exp-one"  0  THEN  Auto)

---

Home Index