Step * 2 2 1 1 1 1 1 of Lemma full-arctan_wf


1. : ℝ
2. : ℝ
3. arctangent(-(x))
⊢ -(arctangent(-(x))) arctangent(x)
BY
(RWO "arctangent-rminus" THEN Auto) }


Latex:


Latex:

1.  x  :  \mBbbR{}
2.  v  :  \mBbbR{}
3.  v  =  arctangent(-(x))
\mvdash{}  -(arctangent(-(x)))  =  arctangent(x)


By


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




Home Index