---

Step * of Lemma rtan-radd

∀[x,y:{x:ℝ| x ∈ (-(π/2), π/2)} ].
  rtan(x + y) = (rtan(x) + rtan(y)/r1 - rtan(x) * rtan(y)) supposing x + y ∈ (-(π/2), π/2)
BY
{ (InstLemma `rtan-radd-denom-positive` [] THEN Auto THEN (InstHyp [⌜x⌝;⌜y⌝] 1⋅ THEN Auto) THEN Thin 1) }

1
1. x : {x:ℝ| x ∈ (-(π/2), π/2)} 
2. y : {x:ℝ| x ∈ (-(π/2), π/2)} 
3. x + y ∈ (-(π/2), π/2)
4. r0 < rcos(x)
5. r0 < rcos(y)
6. r0 < (r1 - rtan(x) * rtan(y))
⊢ rtan(x + y) = (rtan(x) + rtan(y)/r1 - rtan(x) * rtan(y))

---

Latex:

---

Latex:
\mforall{}[x,y:\{x:\mBbbR{}|  x  \mmember{}  (-(\mpi{}/2),  \mpi{}/2)\}  ].
    rtan(x  +  y)  =  (rtan(x)  +  rtan(y)/r1  -  rtan(x)  *  rtan(y))  supposing  x  +  y  \mmember{}  (-(\mpi{}/2),  \mpi{}/2)


By

---

Latex:
(InstLemma  `rtan-radd-denom-positive`  []
  THEN  Auto
  THEN  (InstHyp  [\mkleeneopen{}x\mkleeneclose{};\mkleeneopen{}y\mkleeneclose{}]  1\mcdot{}  THEN  Auto)
  THEN  Thin  1)

---

Home Index