---

Step * of Lemma arctangent_functionality

∀[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)) }

1
1. ∀x:ℝ. (r0 < (r1 + x^2))
⊢ ∀[x,y:ℝ].  arctangent(x) = arctangent(y) supposing x = 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))

---

Home Index