---

Step * of Lemma arctangent-rleq

∀x:ℝ. arctangent(x) ≤ x supposing r0 ≤ x
BY
{ ((Auto
    THEN (Assert ∀x:ℝ. (r0 < (r1 + x^2)) BY
                ((D 0 THENA Auto) THEN (Assert r0 ≤ x1^2 BY Auto) THEN RWO "-1<" 0 THEN Auto))
    )
   THEN (InstLemma  `derivative-implies-increasing` [⌜[r0, ∞)⌝;⌜λ2x.x - arctangent(x)⌝;⌜λ2x.r1 - (r1/r1 + x^2)⌝]⋅
         THENA (Auto THEN RepUR ``iproper i-finite`` 0 THEN Auto)
         )
   ) }

1
.....antecedent..... 
1. x : ℝ
2. r0 ≤ x
3. ∀x:ℝ. (r0 < (r1 + x^2))
⊢ d(x - arctangent(x))/dx = λx.r1 - (r1/r1 + x^2) on [r0, ∞)

2
.....antecedent..... 
1. x : ℝ
2. r0 ≤ x
3. ∀x:ℝ. (r0 < (r1 + x^2))
⊢ r1 - (r1/r1 + x^2) continuous for x ∈ [r0, ∞)

3
1. x : ℝ
2. r0 ≤ x
3. ∀x:ℝ. (r0 < (r1 + x^2))
4. x1 : {x:ℝ| x ∈ [r0, ∞)} 
⊢ r0 ≤ (r1 - (r1/r1 + x1^2))

4
1. x : ℝ
2. r0 ≤ x
3. ∀x:ℝ. (r0 < (r1 + x^2))
4. x - arctangent(x) increasing for x ∈ [r0, ∞)
⊢ arctangent(x) ≤ x

---

Latex:

---

Latex:
\mforall{}x:\mBbbR{}.  arctangent(x)  \mleq{}  x  supposing  r0  \mleq{}  x


By

---

Latex:
((Auto
    THEN  (Assert  \mforall{}x:\mBbbR{}.  (r0  <  (r1  +  x\^{}2))  BY
                            ((D  0  THENA  Auto)  THEN  (Assert  r0  \mleq{}  x1\^{}2  BY  Auto)  THEN  RWO  "-1<"  0  THEN  Auto))
    )
  THEN  (InstLemma    `derivative-implies-increasing`  [\mkleeneopen{}[r0,  \minfty{})\mkleeneclose{};\mkleeneopen{}\mlambda{}\msubtwo{}x.x  -  arctangent(x)\mkleeneclose{};
              \mkleeneopen{}\mlambda{}\msubtwo{}x.r1  -  (r1/r1  +  x\^{}2)\mkleeneclose{}]\mcdot{}
              THENA  (Auto  THEN  RepUR  ``iproper  i-finite``  0  THEN  Auto)
              )
  )

---

Home Index