---

Step * 1 of Lemma arctangent-negative-rinv


1. x : {x:ℝ| x ∈ (-∞, r0)} 
2. -(x) ∈ {x:ℝ| x ∈ (r0, ∞)} 
3. arctangent(rinv(-(x))) = (π/2 - arctangent(-(x)))
⊢ arctangent(rinv(x)) = (-(π/2) - arctangent(x))
BY
{ (Assert r0 < -(x) BY
         (All Reduce THEN MemTypeHD 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)))
\mvdash{}  arctangent(rinv(x))  =  (-(\mpi{}/2)  -  arctangent(x))


By

---

Latex:
(Assert  r0  <  -(x)  BY
              (All  Reduce  THEN  MemTypeHD  2  THEN  Auto))

---

Home Index