---

Step * of Lemma partial-arcsin_wf

∀a:{a:ℝ| ((r(-3)/r(4)) < a) ∧ (a < (r(3)/r(4)))} . (partial-arcsin(a) ∈ {x:ℝ| x = arcsine(a)} )
BY
{ (((Assert (r(3)/r(4)) ≤ r1 BY Auto) THEN (Assert r(-1) ≤ (r(-3)/r(4)) BY Auto)) THEN ProveWfLemma) }

---

Latex:

---

Latex:
\mforall{}a:\{a:\mBbbR{}|  ((r(-3)/r(4))  <  a)  \mwedge{}  (a  <  (r(3)/r(4)))\}  .  (partial-arcsin(a)  \mmember{}  \{x:\mBbbR{}|  x  =  arcsine(a)\}  )


By

---

Latex:
(((Assert  (r(3)/r(4))  \mleq{}  r1  BY  Auto)  THEN  (Assert  r(-1)  \mleq{}  (r(-3)/r(4))  BY  Auto))  THEN  ProveWfLemma)

---

Home Index