---

Step * of Lemma arctangent_functionality_wrt_rless

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

1
1. ∀x:ℝ. (r0 < (r1 + x^2))
2. x : ℝ
3. y : ℝ
4. [%] : x < y
⊢ arctangent(x) < arctangent(y)

---

Latex:

---

Latex:
\mforall{}x,y:\mBbbR{}.    arctangent(x)  <  arctangent(y)  supposing  x  <  y


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))
  THEN  Auto
  )

---

Home Index