---

Step * of Lemma derivative-arctangent

d(arctangent(x))/dx = λx.(r1/r1 + x^2) on (-∞, ∞)
BY
{ ((Assert ∀x:ℝ. (r0 < (r1 + x^2)) BY
          (Auto THEN (Assert r0 ≤ x^2 BY Auto) THEN RWO "-1<" 0 THEN Auto))
   THEN Unfold `arctangent` 0
   THEN BLemma `derivative-of-integral`⋅
   THEN Auto) }

1
1. ∀x:ℝ. (r0 < (r1 + x^2))
⊢ λx.(r1/r1 + x^2) ∈ {f:(-∞, ∞) ⟶ℝ| ∀x,y:{a:ℝ| True} .  ((x = y) ⇒ ((f x) = (f y)))} 

---

Latex:

---

Latex:
d(arctangent(x))/dx  =  \mlambda{}x.(r1/r1  +  x\^{}2)  on  (-\minfty{},  \minfty{})


By

---

Latex:
((Assert  \mforall{}x:\mBbbR{}.  (r0  <  (r1  +  x\^{}2))  BY
                (Auto  THEN  (Assert  r0  \mleq{}  x\^{}2  BY  Auto)  THEN  RWO  "-1<"  0  THEN  Auto))
  THEN  Unfold  `arctangent`  0
  THEN  BLemma  `derivative-of-integral`\mcdot{}
  THEN  Auto)

---

Home Index