---

Step * of Lemma rabs-rexp-difference-bound

∀x,y:ℝ.  (|e^x - e^y| ≤ (e^rmax(x;y) * |x - y|))
BY
{ (Auto
   THEN BLemma `rleq-iff-all-rless`
   THEN Auto
   THEN (InstLemma `rless-cases` [⌜e^x⌝;⌜e^x + e⌝;⌜e^y⌝]⋅ THENA Auto)
   THEN (D -1
         THENL [((DupHyp (-1) THEN (RWO "rexp-rless<" (-1) THENA Auto))
                 THEN (FLemma `rexp-difference-bound` [-1] THENA Auto)
                 )
               ; ((InstLemma `rless-cases` [⌜e^y⌝;⌜e^y + e⌝;⌜e^x⌝]⋅ THENA Auto)
                  THEN (D -1
                        THENL [((DupHyp (-1) THEN (RWO "rexp-rless<" (-1) THENA Auto))
                                THEN (FLemma `rexp-difference-bound` [-1] THENA Auto)
                                )
                              ; (Assert |e^x - e^y| < e BY
                                       (BLemma `rabs-difference-bound-iff` THEN Auto THEN nRAdd ⌜e⌝ 0⋅ THEN Auto))]
                       )
                  )]
   )) }

1
1. x : ℝ
2. y : ℝ
3. e : {e:ℝ| r0 < e} 
4. e^x < e^y
5. x < y
6. (e^y - e^x) ≤ (e^y * (y - x))
⊢ |e^x - e^y| ≤ ((e^rmax(x;y) * |x - y|) + e)

2
1. x : ℝ
2. y : ℝ
3. e : {e:ℝ| r0 < e} 
4. e^y < (e^x + e)
5. e^y < e^x
6. y < x
7. (e^x - e^y) ≤ (e^x * (x - y))
⊢ |e^x - e^y| ≤ ((e^rmax(x;y) * |x - y|) + e)

3
1. x : ℝ
2. y : ℝ
3. e : {e:ℝ| r0 < e} 
4. e^y < (e^x + e)
5. e^x < (e^y + e)
6. |e^x - e^y| < e
⊢ |e^x - e^y| ≤ ((e^rmax(x;y) * |x - y|) + e)

---

Latex:

---

Latex:
\mforall{}x,y:\mBbbR{}.    (|e\^{}x  -  e\^{}y|  \mleq{}  (e\^{}rmax(x;y)  *  |x  -  y|))


By

---

Latex:
(Auto
  THEN  BLemma  `rleq-iff-all-rless`
  THEN  Auto
  THEN  (InstLemma  `rless-cases`  [\mkleeneopen{}e\^{}x\mkleeneclose{};\mkleeneopen{}e\^{}x  +  e\mkleeneclose{};\mkleeneopen{}e\^{}y\mkleeneclose{}]\mcdot{}  THENA  Auto)
  THEN  (D  -1
              THENL  [((DupHyp  (-1)  THEN  (RWO  "rexp-rless<"  (-1)  THENA  Auto))
                              THEN  (FLemma  `rexp-difference-bound`  [-1]  THENA  Auto)
                              )
                          ;  ((InstLemma  `rless-cases`  [\mkleeneopen{}e\^{}y\mkleeneclose{};\mkleeneopen{}e\^{}y  +  e\mkleeneclose{};\mkleeneopen{}e\^{}x\mkleeneclose{}]\mcdot{}  THENA  Auto)
                                THEN  (D  -1
                                            THENL  [((DupHyp  (-1)  THEN  (RWO  "rexp-rless<"  (-1)  THENA  Auto))
                                                            THEN  (FLemma  `rexp-difference-bound`  [-1]  THENA  Auto)
                                                            )
                                                        ;  (Assert  |e\^{}x  -  e\^{}y|  <  e  BY
                                                                          (BLemma  `rabs-difference-bound-iff`
                                                                            THEN  Auto
                                                                            THEN  nRAdd  \mkleeneopen{}e\mkleeneclose{}  0\mcdot{}
                                                                            THEN  Auto))]
                                          )
                                )]
  ))

---

Home Index