---

Step * 1 1 1 of Lemma arctangent-negative-rinv


1. x : {x:ℝ| x ∈ (-∞, r0)} 
2. -(x) ∈ {x:ℝ| x ∈ (r0, ∞)} 
3. arctangent(-(rinv(x))) = (π/2 - arctangent(-(x)))
4. r0 < -(x)
⊢ arctangent(rinv(x)) = (-(π/2) - arctangent(x))
BY
{ (RWO "arctangent-rminus" (-2) THEN Auto) }

1
1. x : {x:ℝ| x ∈ (-∞, r0)} 
2. -(x) ∈ {x:ℝ| x ∈ (r0, ∞)} 
3. -(arctangent(rinv(x))) = (π/2 - -(arctangent(x)))
4. r0 < -(x)
⊢ arctangent(rinv(x)) = (-(π/2) - arctangent(x))

---

Latex:

---

Latex:

1.  x  :  \{x:\mBbbR{}|  x  \mmember{}  (-\minfty{},  r0)\} 
2.  -(x)  \mmember{}  \{x:\mBbbR{}|  x  \mmember{}  (r0,  \minfty{})\} 
3.  arctangent(-(rinv(x)))  =  (\mpi{}/2  -  arctangent(-(x)))
4.  r0  <  -(x)
\mvdash{}  arctangent(rinv(x))  =  (-(\mpi{}/2)  -  arctangent(x))


By

---

Latex:
(RWO  "arctangent-rminus"  (-2)  THEN  Auto)

---

Home Index