---

Step * 2 of Lemma arctangent-rtan

.....antecedent..... 
∃x:{x:ℝ| x ∈ (-(π/2), π/2)} . (arctangent(rtan(x)) = x)
BY
{ (D 0 With ⌜r0⌝  THEN Auto) }

1
r0 ∈ {x:ℝ| (-(π/2) < x) ∧ (x < π/2)} 

2
arctangent(rtan(r0)) = r0

---

Latex:

---

Latex:
.....antecedent..... 
\mexists{}x:\{x:\mBbbR{}|  x  \mmember{}  (-(\mpi{}/2),  \mpi{}/2)\}  .  (arctangent(rtan(x))  =  x)


By

---

Latex:
(D  0  With  \mkleeneopen{}r0\mkleeneclose{}    THEN  Auto)

---

Home Index