---

Step * 1 of Lemma arcsine-rsin


1. ∀x:{x:ℝ| x ∈ (-(π/2), π/2)} . (rsin(x) ∈ (r(-1), r1))
⊢ ∀[x:{x:ℝ| x ∈ (-(π/2), π/2)} ]. (arcsine(rsin(x)) = x)
BY
{ (DupHyp (-1)
   THEN Reduce -1
   THEN ((Assert ∀x:{x:ℝ| x ∈ (-(π/2), π/2)} . (arcsine(rsin(x)) = x) BY
                (InstLemma `antiderivatives-equal` 
                 [⌜(-(π/2), π/2)⌝;⌜λ2x.r1⌝;⌜λ2x.arcsine(rsin(x))⌝;⌜λ2x.x⌝]⋅
                 THEN Auto
                 ))
   THENM Auto
   )) }

1
.....antecedent..... 
1. ∀x:{x:ℝ| x ∈ (-(π/2), π/2)} . (rsin(x) ∈ (r(-1), r1))
2. ∀x:{x:ℝ| (-(π/2) < x) ∧ (x < π/2)} . ((r(-1) < rsin(x)) ∧ (rsin(x) < r1))
⊢ d(arcsine(rsin(x)))/dx = λx.r1 on (-(π/2), π/2)

2
.....antecedent..... 
1. ∀x:{x:ℝ| x ∈ (-(π/2), π/2)} . (rsin(x) ∈ (r(-1), r1))
2. ∀x:{x:ℝ| (-(π/2) < x) ∧ (x < π/2)} . ((r(-1) < rsin(x)) ∧ (rsin(x) < r1))
⊢ ∃x:{x:ℝ| x ∈ (-(π/2), π/2)} . (arcsine(rsin(x)) = x)

---

Latex:

---

Latex:

1.  \mforall{}x:\{x:\mBbbR{}|  x  \mmember{}  (-(\mpi{}/2),  \mpi{}/2)\}  .  (rsin(x)  \mmember{}  (r(-1),  r1))
\mvdash{}  \mforall{}[x:\{x:\mBbbR{}|  x  \mmember{}  (-(\mpi{}/2),  \mpi{}/2)\}  ].  (arcsine(rsin(x))  =  x)


By

---

Latex:
(DupHyp  (-1)
  THEN  Reduce  -1
  THEN  ((Assert  \mforall{}x:\{x:\mBbbR{}|  x  \mmember{}  (-(\mpi{}/2),  \mpi{}/2)\}  .  (arcsine(rsin(x))  =  x)  BY
                            (InstLemma  `antiderivatives-equal` 
                              [\mkleeneopen{}(-(\mpi{}/2),  \mpi{}/2)\mkleeneclose{};\mkleeneopen{}\mlambda{}\msubtwo{}x.r1\mkleeneclose{};\mkleeneopen{}\mlambda{}\msubtwo{}x.arcsine(rsin(x))\mkleeneclose{};\mkleeneopen{}\mlambda{}\msubtwo{}x.x\mkleeneclose{}]\mcdot{}
                              THEN  Auto
                              ))
  THENM  Auto
  ))

---

Home Index