---

Step * of Lemma arctangent-chain-rule

∀I:Interval. ∀f,f':I ⟶ℝ.
  (iproper(I)
  ⇒ (∀x,y:{x:ℝ| x ∈ I} .  ((x = y) ⇒ (f'[x] = f'[y])))
  ⇒ d(f[x])/dx = λx.f'[x] on I
  ⇒ d(arctangent(f[x]))/dx = λx.(f'[x]/r1 + f[x]^2) on I)
BY
{ ((InstLemma `simple-chain-rule` [] THEN RepeatFor 3 (ParallelLast'))
   THEN (Auto
         THEN (Assert ∀x1:ℝ. (r0 < (r1 + x1^2)) BY
                     (Auto THEN (Assert r0 ≤ x1^2 BY EAuto 1) THEN RWO "-1<" 0 THEN Auto))
         )
   THEN (InstHyp [⌜λ2x.arctangent(x)⌝;⌜λ2x.(r1/r1 + x^2)⌝] (-5)⋅ THENA Auto)) }

1
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

---

Latex:

---

Latex:
\mforall{}I:Interval.  \mforall{}f,f':I  {}\mrightarrow{}\mBbbR{}.
    (iproper(I)
    {}\mRightarrow{}  (\mforall{}x,y:\{x:\mBbbR{}|  x  \mmember{}  I\}  .    ((x  =  y)  {}\mRightarrow{}  (f'[x]  =  f'[y])))
    {}\mRightarrow{}  d(f[x])/dx  =  \mlambda{}x.f'[x]  on  I
    {}\mRightarrow{}  d(arctangent(f[x]))/dx  =  \mlambda{}x.(f'[x]/r1  +  f[x]\^{}2)  on  I)


By

---

Latex:
((InstLemma  `simple-chain-rule`  []  THEN  RepeatFor  3  (ParallelLast'))
  THEN  (Auto
              THEN  (Assert  \mforall{}x1:\mBbbR{}.  (r0  <  (r1  +  x1\^{}2))  BY
                                      (Auto  THEN  (Assert  r0  \mleq{}  x1\^{}2  BY  EAuto  1)  THEN  RWO  "-1<"  0  THEN  Auto))
              )
  THEN  (InstHyp  [\mkleeneopen{}\mlambda{}\msubtwo{}x.arctangent(x)\mkleeneclose{};\mkleeneopen{}\mlambda{}\msubtwo{}x.(r1/r1  +  x\^{}2)\mkleeneclose{}]  (-5)\mcdot{}  THENA  Auto))

---

Home Index