---

Step * 1 of Lemma arcsine-bounds2


1. x : {x:ℝ| (r0 < x) ∧ (x < (r(3)/r(4)))} 
2. r(-1) < r0
3. (r(3)/r(4)) < r1
⊢ |arcsine(x) - x| < (r1/r(10))
BY
{ (InstLemma `derivative-implies-strictly-increasing-closed` 
   [⌜r0⌝;⌜(r(3)/r(4))⌝;⌜λ2x.arcsine(x) - x⌝;⌜λ2x.arcsine_deriv(x) - r1⌝]⋅
   THENA (Auto THEN Try ((D -1 THEN Reduce -1 THEN MemTypeCD THEN Auto)))
   ) }

1
.....antecedent..... 
1. x : {x:ℝ| (r0 < x) ∧ (x < (r(3)/r(4)))} 
2. r(-1) < r0
3. (r(3)/r(4)) < r1
⊢ d(arcsine(x) - x)/dx = λx.arcsine_deriv(x) - r1 on [r0, (r(3)/r(4))]

2
.....antecedent..... 
1. x : {x:ℝ| (r0 < x) ∧ (x < (r(3)/r(4)))} 
2. r(-1) < r0
3. (r(3)/r(4)) < r1
⊢ ifun(λx.(arcsine_deriv(x) - r1);[r0, (r(3)/r(4))])

3
1. x : {x:ℝ| (r0 < x) ∧ (x < (r(3)/r(4)))} 
2. r(-1) < r0
3. (r(3)/r(4)) < r1
4. x1 : {x:ℝ| x ∈ [r0, (r(3)/r(4))]} 
⊢ r0 ≤ (arcsine_deriv(x1) - r1)

4
1. x : {x:ℝ| (r0 < x) ∧ (x < (r(3)/r(4)))} 
2. r(-1) < r0
3. (r(3)/r(4)) < r1
4. x1 : {x:ℝ| x ∈ (r0, (r(3)/r(4)))} 
⊢ r0 < (arcsine_deriv(x1) - r1)

5
1. x : {x:ℝ| (r0 < x) ∧ (x < (r(3)/r(4)))} 
2. r(-1) < r0
3. (r(3)/r(4)) < r1
4. arcsine(x) - x strictly-increasing for x ∈ [r0, (r(3)/r(4))]
⊢ |arcsine(x) - x| < (r1/r(10))

---

Latex:

---

Latex:

1.  x  :  \{x:\mBbbR{}|  (r0  <  x)  \mwedge{}  (x  <  (r(3)/r(4)))\} 
2.  r(-1)  <  r0
3.  (r(3)/r(4))  <  r1
\mvdash{}  |arcsine(x)  -  x|  <  (r1/r(10))


By

---

Latex:
(InstLemma  `derivative-implies-strictly-increasing-closed` 
  [\mkleeneopen{}r0\mkleeneclose{};\mkleeneopen{}(r(3)/r(4))\mkleeneclose{};\mkleeneopen{}\mlambda{}\msubtwo{}x.arcsine(x)  -  x\mkleeneclose{};\mkleeneopen{}\mlambda{}\msubtwo{}x.arcsine\_deriv(x)  -  r1\mkleeneclose{}]\mcdot{}
  THENA  (Auto  THEN  Try  ((D  -1  THEN  Reduce  -1  THEN  MemTypeCD  THEN  Auto)))
  )

---

Home Index