---

Step * 1 of Lemma arcsin1


1. r0 < π/2
⊢ -(π/2) ≤ π/2
BY
{ (nRAdd ⌜π/2⌝ 0⋅ THEN nRMul ⌜r(2)⌝ 1⋅ THEN Auto) }

---

Latex:

---

Latex:

1.  r0  <  \mpi{}/2
\mvdash{}  -(\mpi{}/2)  \mleq{}  \mpi{}/2


By

---

Latex:
(nRAdd  \mkleeneopen{}\mpi{}/2\mkleeneclose{}  0\mcdot{}  THEN  nRMul  \mkleeneopen{}r(2)\mkleeneclose{}  1\mcdot{}  THEN  Auto)

---

Home Index