---

Step * 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)
⊢ ((rsin(x + y)/rcos(x + y)) + -((rsin(x + y)/rcos(x + y)) * (rsin(x)/rcos(x)) * (rsin(y)/rcos(y))))
= ((rsin(x)/rcos(x)) + (rsin(y)/rcos(y)))
BY
{ (nRMul ⌜rcos(x)⌝ 0⋅ THEN nRMul ⌜rcos(y)⌝ 0⋅ THEN nRMul ⌜rcos(x + y)⌝ 0⋅) }

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))
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)))

---

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{}  ((rsin(x  +  y)/rcos(x  +  y))  +  -((rsin(x  +  y)/rcos(x  +  y))  *  (rsin(x)/rcos(x))  *  (rsin(y)/rcos(y))))
=  ((rsin(x)/rcos(x))  +  (rsin(y)/rcos(y)))


By

---

Latex:
(nRMul  \mkleeneopen{}rcos(x)\mkleeneclose{}  0\mcdot{}  THEN  nRMul  \mkleeneopen{}rcos(y)\mkleeneclose{}  0\mcdot{}  THEN  nRMul  \mkleeneopen{}rcos(x  +  y)\mkleeneclose{}  0\mcdot{})

---

Home Index