---

Step * 1 of Lemma arcsine-bounds

.....assertion..... 
1. x : {x:ℝ| x ∈ (r(-1), r1)} 
⊢ ∃y:ℝ. ((y ∈ (-(π/2), π/2)) ∧ (x = rsin(y)))
BY
{ (InstLemma `IVT-strictly-increasing-open` [⌜-(π/2)⌝;⌜π/2⌝;⌜λx.rsin(x)⌝;⌜x⌝]⋅ THENA Auto) }

1
.....wf..... 
1. x : {x:ℝ| x ∈ (r(-1), r1)} 
⊢ π/2 ∈ {b:ℝ| -(π/2) < b} 

2
1. x : {x:ℝ| x ∈ (r(-1), r1)} 
2. x1 : {x:ℝ| x ∈ [-(π/2), π/2]} 
3. y : {x:ℝ| x ∈ [-(π/2), π/2]} 
4. x1 = y
⊢ λx.rsin(x)[x1] = λx.rsin(x)[y]

3
.....antecedent..... 
1. x : {x:ℝ| x ∈ (r(-1), r1)} 
⊢ λx.rsin(x)[x] strictly-increasing for x ∈ (-(π/2), π/2)

4
.....antecedent..... 
1. x : {x:ℝ| x ∈ (r(-1), r1)} 
⊢ λx.rsin(x)(-(π/2)) < x

5
.....antecedent..... 
1. x : {x:ℝ| x ∈ (r(-1), r1)} 
⊢ x < λx.rsin(x)(π/2)

6
1. x : {x:ℝ| x ∈ (r(-1), r1)} 
2. ∃x@0:ℝ. ((x@0 ∈ (-(π/2), π/2)) ∧ (λx.rsin(x)(x@0) = x))
⊢ ∃y:ℝ. ((y ∈ (-(π/2), π/2)) ∧ (x = rsin(y)))

---

Latex:

---

Latex:
.....assertion..... 
1.  x  :  \{x:\mBbbR{}|  x  \mmember{}  (r(-1),  r1)\} 
\mvdash{}  \mexists{}y:\mBbbR{}.  ((y  \mmember{}  (-(\mpi{}/2),  \mpi{}/2))  \mwedge{}  (x  =  rsin(y)))


By

---

Latex:
(InstLemma  `IVT-strictly-increasing-open`  [\mkleeneopen{}-(\mpi{}/2)\mkleeneclose{};\mkleeneopen{}\mpi{}/2\mkleeneclose{};\mkleeneopen{}\mlambda{}x.rsin(x)\mkleeneclose{};\mkleeneopen{}x\mkleeneclose{}]\mcdot{}  THENA  Auto)

---

Home Index