---

Step * 2 of Lemma rexp-unique


1. f : ℝ ⟶ ℝ
2. ∀x,y:ℝ.  ((x = y) ⇒ (f[x] = f[y]))
3. f[r0] = r1
4. d(f[x])/dx = λx.f[x] on (-∞, ∞)
5. x : ℝ
6. m : ℕ
⊢ ∃c:ℝ. ∃N:ℕ. ∀k:{N...}. ∀x:{x:ℝ| |x| ≤ r(m)} .  (|e^x| ≤ c)
BY
{ ((Assert ifun(λx.e^x;[r(-m), r(m)]) BY
          (D 0 THEN (Reduce 0 THEN Auto) THEN RWO "-1" 0 THEN Auto))
   THEN (D 0 With ⌜||e^x||_x:[r(-m), r(m)]⌝  THENA Auto)
   THEN Try ((D 0 With ⌜0⌝ 
              THEN Auto
              THEN InstLemma `I-norm-bound` [⌜[r(-m), r(m)]⌝;⌜λ2x.e^x⌝;⌜x1⌝]  ⋅
              THEN Auto
              THEN D -1
              THEN RWO "rabs-rleq-iff" (-1)
              THEN Auto))) }

---

Latex:

---

Latex:

1.  f  :  \mBbbR{}  {}\mrightarrow{}  \mBbbR{}
2.  \mforall{}x,y:\mBbbR{}.    ((x  =  y)  {}\mRightarrow{}  (f[x]  =  f[y]))
3.  f[r0]  =  r1
4.  d(f[x])/dx  =  \mlambda{}x.f[x]  on  (-\minfty{},  \minfty{})
5.  x  :  \mBbbR{}
6.  m  :  \mBbbN{}
\mvdash{}  \mexists{}c:\mBbbR{}.  \mexists{}N:\mBbbN{}.  \mforall{}k:\{N...\}.  \mforall{}x:\{x:\mBbbR{}|  |x|  \mleq{}  r(m)\}  .    (|e\^{}x|  \mleq{}  c)


By

---

Latex:
((Assert  ifun(\mlambda{}x.e\^{}x;[r(-m),  r(m)])  BY
                (D  0  THEN  (Reduce  0  THEN  Auto)  THEN  RWO  "-1"  0  THEN  Auto))
  THEN  (D  0  With  \mkleeneopen{}||e\^{}x||\_x:[r(-m),  r(m)]\mkleeneclose{}    THENA  Auto)
  THEN  Try  ((D  0  With  \mkleeneopen{}0\mkleeneclose{} 
                        THEN  Auto
                        THEN  InstLemma  `I-norm-bound`  [\mkleeneopen{}[r(-m),  r(m)]\mkleeneclose{};\mkleeneopen{}\mlambda{}\msubtwo{}x.e\^{}x\mkleeneclose{};\mkleeneopen{}x1\mkleeneclose{}]    \mcdot{}
                        THEN  Auto
                        THEN  D  -1
                        THEN  RWO  "rabs-rleq-iff"  (-1)
                        THEN  Auto)))

---

Home Index