---

Step * of Lemma arctangent-negative-rinv

∀[x:{x:ℝ| x ∈ (-∞, r0)} ]. (arctangent(rinv(x)) = (-(π/2) - arctangent(x)))
BY
{ (Auto
   THEN (Assert -(x) ∈ {x:ℝ| x ∈ (r0, ∞)}  BY
               (D -1 THEN MemTypeCD THEN Auto THEN All Reduce THEN Auto))
   THEN (InstLemma `arctangent-rinv` [⌜-(x)⌝]⋅ THENA Auto)) }

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

---

Latex:

---

Latex:
\mforall{}[x:\{x:\mBbbR{}|  x  \mmember{}  (-\minfty{},  r0)\}  ].  (arctangent(rinv(x))  =  (-(\mpi{}/2)  -  arctangent(x)))


By

---

Latex:
(Auto
  THEN  (Assert  -(x)  \mmember{}  \{x:\mBbbR{}|  x  \mmember{}  (r0,  \minfty{})\}    BY
                          (D  -1  THEN  MemTypeCD  THEN  Auto  THEN  All  Reduce  THEN  Auto))
  THEN  (InstLemma  `arctangent-rinv`  [\mkleeneopen{}-(x)\mkleeneclose{}]\mcdot{}  THENA  Auto))

---

Home Index