---

Step * 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|
⊢ |a - b|^n ≤ |a^n - b^n|
BY
{ ((Assert ⌜|-(a) - -(b)| = |a - b|⌝⋅
    THENA ((RW (AddrC [1] (RevLemmaC `rabs-rminus`)) 0 THENA Auto) THEN nRNorm 0 THEN Auto)
    )
   THEN (RWO "-1" (-2) THENA Auto)
   THEN (RWO "-2" 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|
⊢ |-(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|
\mvdash{}  |a  -  b|\^{}n  \mleq{}  |a\^{}n  -  b\^{}n|


By

---

Latex:
((Assert  \mkleeneopen{}|-(a)  -  -(b)|  =  |a  -  b|\mkleeneclose{}\mcdot{}
    THENA  ((RW  (AddrC  [1]  (RevLemmaC  `rabs-rminus`))  0  THENA  Auto)  THEN  nRNorm  0  THEN  Auto)
    )
  THEN  (RWO  "-1"  (-2)  THENA  Auto)
  THEN  (RWO  "-2"  0  THENA  Auto))

---

Home Index