---

Step * of Lemma arctangent_wf

∀[x:ℝ]. (arctangent(x) ∈ ℝ)
BY
{ (Assert ∀x:ℝ. (r0 < (r1 + x^2)) BY
         (Auto THEN (Assert r0 ≤ x^2 BY Auto) THEN RWO "-1<" 0 THEN Auto)) }

1
1. ∀x:ℝ. (r0 < (r1 + x^2))
⊢ ∀[x:ℝ]. (arctangent(x) ∈ ℝ)

---

Latex:

---

Latex:
\mforall{}[x:\mBbbR{}].  (arctangent(x)  \mmember{}  \mBbbR{})


By

---

Latex:
(Assert  \mforall{}x:\mBbbR{}.  (r0  <  (r1  +  x\^{}2))  BY
              (Auto  THEN  (Assert  r0  \mleq{}  x\^{}2  BY  Auto)  THEN  RWO  "-1<"  0  THEN  Auto))

---

Home Index