---

Step * 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))
⊢ (rtan(x + y) + -(rtan(x + y) * rtan(x) * rtan(y))) = (rtan(x) + rtan(y))
BY
{ ((InstLemma `rcos-positive` [⌜x + y⌝]⋅ THENA Auto) THEN RepUR ``rtan`` 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)
⊢ ((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)))

---

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))
\mvdash{}  (rtan(x  +  y)  +  -(rtan(x  +  y)  *  rtan(x)  *  rtan(y)))  =  (rtan(x)  +  rtan(y))


By

---

Latex:
((InstLemma  `rcos-positive`  [\mkleeneopen{}x  +  y\mkleeneclose{}]\mcdot{}  THENA  Auto)  THEN  RepUR  ``rtan``  0)

---

Home Index