---

Step * of Lemma rexp-unique

∀f:ℝ ⟶ ℝ
  ((∀x,y:ℝ.  ((x = y) ⇒ (f[x] = f[y]))) ⇒ (f[r0] = r1) ⇒ d(f[x])/dx = λx.f[x] on (-∞, ∞) ⇒ (∀x:ℝ. (f[x] = e^x)))
BY
{ (Auto
   THEN InstLemma `equal-functions-by-Taylor` [⌜λ2n x.f[x]⌝;⌜λ2n x.e^x⌝]⋅
   THEN Auto
   THEN Try ((D 0 THEN Complete (Auto)))) }

1
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)} .  (|f[x]| ≤ c)

2
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)

3
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. n : ℕ
⊢ f[r0] = e^r0

---

Latex:

---

Latex:
\mforall{}f:\mBbbR{}  {}\mrightarrow{}  \mBbbR{}
    ((\mforall{}x,y:\mBbbR{}.    ((x  =  y)  {}\mRightarrow{}  (f[x]  =  f[y])))
    {}\mRightarrow{}  (f[r0]  =  r1)
    {}\mRightarrow{}  d(f[x])/dx  =  \mlambda{}x.f[x]  on  (-\minfty{},  \minfty{})
    {}\mRightarrow{}  (\mforall{}x:\mBbbR{}.  (f[x]  =  e\^{}x)))


By

---

Latex:
(Auto
  THEN  InstLemma  `equal-functions-by-Taylor`  [\mkleeneopen{}\mlambda{}\msubtwo{}n  x.f[x]\mkleeneclose{};\mkleeneopen{}\mlambda{}\msubtwo{}n  x.e\^{}x\mkleeneclose{}]\mcdot{}
  THEN  Auto
  THEN  Try  ((D  0  THEN  Complete  (Auto))))

---

Home Index