---

Step * 1 1 1 1 of Lemma rtan-radd


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))
7. r0 < rcos(x + y)
⊢ ((rcos(x) * rcos(y) * rsin(x + y)) + -(rsin(x + y) * rsin(x) * rsin(y)))
= ((rcos(x + y) * rcos(x) * rsin(y)) + (rcos(x + y) * rcos(y) * rsin(x)))
BY
{ (RWO "rcos-radd rsin-radd" 0 THEN Auto) }

---

Latex:

---

Latex:

1.  x  :  \{x:\mBbbR{}|  x  \mmember{}  (-(\mpi{}/2),  \mpi{}/2)\} 
2.  y  :  \{x:\mBbbR{}|  x  \mmember{}  (-(\mpi{}/2),  \mpi{}/2)\} 
3.  x  +  y  \mmember{}  (-(\mpi{}/2),  \mpi{}/2)
4.  r0  <  rcos(x)
5.  r0  <  rcos(y)
6.  r0  <  (r1  -  rtan(x)  *  rtan(y))
7.  r0  <  rcos(x  +  y)
\mvdash{}  ((rcos(x)  *  rcos(y)  *  rsin(x  +  y))  +  -(rsin(x  +  y)  *  rsin(x)  *  rsin(y)))
=  ((rcos(x  +  y)  *  rcos(x)  *  rsin(y))  +  (rcos(x  +  y)  *  rcos(y)  *  rsin(x)))


By

---

Latex:
(RWO  "rcos-radd  rsin-radd"  0  THEN  Auto)

---

Home Index