---

Step * 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|
⊢ |-(a)^n - -(b)^n| ≤ |a^n - b^n|
BY
{ (RWW "rminus-as-rmul rnexp-rmul rmul-rsub-distrib.1<       rabs-rmul rabs-rnexp rabs-int rnexp-int" 0⋅ THENA Auto) }

1
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|

---

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{}  |-(a)\^{}n  -  -(b)\^{}n|  \mleq{}  |a\^{}n  -  b\^{}n|


By

---

Latex:
(RWW  "rminus-as-rmul  rnexp-rmul  rmul-rsub-distrib.1< 
            rabs-rmul  rabs-rnexp  rabs-int  rnexp-int"  0\mcdot{}
  THENA  Auto
  )

---

Home Index