---

Step * 1 of Lemma rtan-rminus


1. x : ℝ
2. [%1] : (-(π/2) < x) ∧ (x < π/2)
⊢ rtan(-(x)) = -(rtan(x))
BY
{ ((InstLemma `rcos-positive` [⌜x⌝]⋅ THENA Auto)
   THEN (InstLemma `rcos-positive` [⌜-(x)⌝]⋅ THENA Auto)
   THEN Unfold `rtan` 0
   THEN RWO "rsin-rminus rcos-rminus" 0
   THEN Auto) }

---

Latex:

---

Latex:

1.  x  :  \mBbbR{}
2.  [\%1]  :  (-(\mpi{}/2)  <  x)  \mwedge{}  (x  <  \mpi{}/2)
\mvdash{}  rtan(-(x))  =  -(rtan(x))


By

---

Latex:
((InstLemma  `rcos-positive`  [\mkleeneopen{}x\mkleeneclose{}]\mcdot{}  THENA  Auto)
  THEN  (InstLemma  `rcos-positive`  [\mkleeneopen{}-(x)\mkleeneclose{}]\mcdot{}  THENA  Auto)
  THEN  Unfold  `rtan`  0
  THEN  RWO  "rsin-rminus  rcos-rminus"  0
  THEN  Auto)

---

Home Index