---

Step * 1 of Lemma arctangent-reduction


1. B : {B:ℝ| r0 < B} 
2. x : {x:ℝ| (r(-1)/B) < x} 
⊢ arctangent(x) = (arctangent(B) + arctangent((x - B/r1 + (x * B))))
BY
{ ((Assert ∀x:{x:ℝ| (r(-1)/B) < x} . (r0 < (r1 + (x * B))) BY
          (Auto THEN DSetVars THEN Unhide THEN Auto THEN nRMul ⌜B⌝ (-1)⋅ THEN Auto))
   THEN (Assert ∀x:ℝ. (r0 < (r1 + x^2)) BY
               (Auto THEN (Assert r0 ≤ x1^2 BY EAuto 2) THEN RWO "-1<" 0 THEN Auto))
   THEN InstLemma `derivative-arctangent` []) }

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

---

Latex:

---

Latex:

1.  B  :  \{B:\mBbbR{}|  r0  <  B\} 
2.  x  :  \{x:\mBbbR{}|  (r(-1)/B)  <  x\} 
\mvdash{}  arctangent(x)  =  (arctangent(B)  +  arctangent((x  -  B/r1  +  (x  *  B))))


By

---

Latex:
((Assert  \mforall{}x:\{x:\mBbbR{}|  (r(-1)/B)  <  x\}  .  (r0  <  (r1  +  (x  *  B)))  BY
                (Auto  THEN  DSetVars  THEN  Unhide  THEN  Auto  THEN  nRMul  \mkleeneopen{}B\mkleeneclose{}  (-1)\mcdot{}  THEN  Auto))
  THEN  (Assert  \mforall{}x:\mBbbR{}.  (r0  <  (r1  +  x\^{}2))  BY
                          (Auto  THEN  (Assert  r0  \mleq{}  x1\^{}2  BY  EAuto  2)  THEN  RWO  "-1<"  0  THEN  Auto))
  THEN  InstLemma  `derivative-arctangent`  [])

---

Home Index