---

Step * 1 of Lemma arctangent-chain-rule


1. I : Interval
2. f : I ⟶ℝ
3. f' : I ⟶ℝ
4. ∀g,g':(-∞, ∞) ⟶ℝ.
     (iproper(I)
     ⇒ (∀x,y:{x:ℝ| x ∈ I} .  ((x = y) ⇒ (f'[x] = f'[y])))
     ⇒ (∀x,y:ℝ.  ((x = y) ⇒ (g'[x] = g'[y])))
     ⇒ d(f[x])/dx = λx.f'[x] on I
     ⇒ d(g[x])/dx = λx.g'[x] on (-∞, ∞)
     ⇒ d(g[f[x]])/dx = λx.g'[f[x]] * f'[x] on I)
5. iproper(I)
6. ∀x,y:{x:ℝ| x ∈ I} .  ((x = y) ⇒ (f'[x] = f'[y]))
7. d(f[x])/dx = λx.f'[x] on I
8. ∀x1:ℝ. (r0 < (r1 + x1^2))
9. d(arctangent(f[x]))/dx = λx.(r1/r1 + f[x]^2) * f'[x] on I
⊢ d(arctangent(f[x]))/dx = λx.(f'[x]/r1 + f[x]^2) on I
BY
{ (DerivativeFunctionality (-1) THEN Auto) }

---

Latex:

---

Latex:

1.  I  :  Interval
2.  f  :  I  {}\mrightarrow{}\mBbbR{}
3.  f'  :  I  {}\mrightarrow{}\mBbbR{}
4.  \mforall{}g,g':(-\minfty{},  \minfty{})  {}\mrightarrow{}\mBbbR{}.
          (iproper(I)
          {}\mRightarrow{}  (\mforall{}x,y:\{x:\mBbbR{}|  x  \mmember{}  I\}  .    ((x  =  y)  {}\mRightarrow{}  (f'[x]  =  f'[y])))
          {}\mRightarrow{}  (\mforall{}x,y:\mBbbR{}.    ((x  =  y)  {}\mRightarrow{}  (g'[x]  =  g'[y])))
          {}\mRightarrow{}  d(f[x])/dx  =  \mlambda{}x.f'[x]  on  I
          {}\mRightarrow{}  d(g[x])/dx  =  \mlambda{}x.g'[x]  on  (-\minfty{},  \minfty{})
          {}\mRightarrow{}  d(g[f[x]])/dx  =  \mlambda{}x.g'[f[x]]  *  f'[x]  on  I)
5.  iproper(I)
6.  \mforall{}x,y:\{x:\mBbbR{}|  x  \mmember{}  I\}  .    ((x  =  y)  {}\mRightarrow{}  (f'[x]  =  f'[y]))
7.  d(f[x])/dx  =  \mlambda{}x.f'[x]  on  I
8.  \mforall{}x1:\mBbbR{}.  (r0  <  (r1  +  x1\^{}2))
9.  d(arctangent(f[x]))/dx  =  \mlambda{}x.(r1/r1  +  f[x]\^{}2)  *  f'[x]  on  I
\mvdash{}  d(arctangent(f[x]))/dx  =  \mlambda{}x.(f'[x]/r1  +  f[x]\^{}2)  on  I


By

---

Latex:
(DerivativeFunctionality  (-1)  THEN  Auto)

---

Home Index