---

Step * 1 of Lemma arctangent-rinv

.....antecedent..... 
1. x : {x:ℝ| x ∈ (r0, ∞)} 
⊢ d(arctangent((r1/x)) + arctangent(x))/dx = λx.r0 on (r0, ∞)
BY
{ ((Assert ∀x1:{x:ℝ| x ∈ (r0, ∞)} . (r0 < x1^2) BY
          ((D 0 THEN Auto) THEN D -1 THEN Unhide THEN Auto THEN Reduce -1 THEN BLemma `rnexp-positive` THEN Auto))
   THEN (Assert ∀x1:{x:ℝ| x ∈ (r0, ∞)} . (r1 < (r1 + x1^2)) BY
               Auto)
   THEN (Assert ∀x1:{x:ℝ| x ∈ (r0, ∞)} . (r0 < (r1 + x1^2)) BY
               (RWO "-1<" 0 THEN Auto))) }

1
1. x : {x:ℝ| x ∈ (r0, ∞)} 
2. ∀x1:{x:ℝ| x ∈ (r0, ∞)} . (r0 < x1^2)
3. ∀x1:{x:ℝ| x ∈ (r0, ∞)} . (r1 < (r1 + x1^2))
4. ∀x1:{x:ℝ| x ∈ (r0, ∞)} . (r0 < (r1 + x1^2))
⊢ d(arctangent((r1/x)) + arctangent(x))/dx = λx.r0 on (r0, ∞)

---

Latex:

---

Latex:
.....antecedent..... 
1.  x  :  \{x:\mBbbR{}|  x  \mmember{}  (r0,  \minfty{})\} 
\mvdash{}  d(arctangent((r1/x))  +  arctangent(x))/dx  =  \mlambda{}x.r0  on  (r0,  \minfty{})


By

---

Latex:
((Assert  \mforall{}x1:\{x:\mBbbR{}|  x  \mmember{}  (r0,  \minfty{})\}  .  (r0  <  x1\^{}2)  BY
                ((D  0  THEN  Auto)
                  THEN  D  -1
                  THEN  Unhide
                  THEN  Auto
                  THEN  Reduce  -1
                  THEN  BLemma  `rnexp-positive`
                  THEN  Auto))
  THEN  (Assert  \mforall{}x1:\{x:\mBbbR{}|  x  \mmember{}  (r0,  \minfty{})\}  .  (r1  <  (r1  +  x1\^{}2))  BY
                          Auto)
  THEN  (Assert  \mforall{}x1:\{x:\mBbbR{}|  x  \mmember{}  (r0,  \minfty{})\}  .  (r0  <  (r1  +  x1\^{}2))  BY
                          (RWO  "-1<"  0  THEN  Auto)))

---

Home Index