---

Step * of Lemma arctangent-rtan

∀[x:{x:ℝ| x ∈ (-(π/2), π/2)} ]. (arctangent(rtan(x)) = x)
BY
{ (InstLemma `antiderivatives-equal`  [⌜(-(π/2), π/2)⌝;⌜λ2x.r1⌝;⌜λ2x.arctangent(rtan(x))⌝;⌜λ2x.x⌝]⋅ THEN Auto) }

1
.....antecedent..... 
d(arctangent(rtan(x)))/dx = λx.r1 on (-(π/2), π/2)

2
.....antecedent..... 
∃x:{x:ℝ| x ∈ (-(π/2), π/2)} . (arctangent(rtan(x)) = x)

---

Latex:

---

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


By

---

Latex:
(InstLemma  `antiderivatives-equal` 
  [\mkleeneopen{}(-(\mpi{}/2),  \mpi{}/2)\mkleeneclose{};\mkleeneopen{}\mlambda{}\msubtwo{}x.r1\mkleeneclose{};\mkleeneopen{}\mlambda{}\msubtwo{}x.arctangent(rtan(x))\mkleeneclose{};\mkleeneopen{}\mlambda{}\msubtwo{}x.x\mkleeneclose{}]\mcdot{}
  THEN  Auto
  )

---

Home Index