---

Step * 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) + rtan(y)/r1 - rtan(x) * rtan(y))
BY
{ nRMul ⌜r1 - rtan(x) * rtan(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))
⊢ (rtan(x + y) + -(rtan(x + y) * rtan(x) * rtan(y))) = (rtan(x) + rtan(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)  +  rtan(y)/r1  -  rtan(x)  *  rtan(y))


By

---

Latex:
nRMul  \mkleeneopen{}r1  -  rtan(x)  *  rtan(y)\mkleeneclose{}  0\mcdot{}

---

Home Index