---

Step * of Lemma arcsin0

arcsin(r0) = r0
BY
{ ((Assert r0 < π/2 BY
          (D 0 With ⌜3⌝  THEN Auto))
   THEN BLemma `arcsin-unique`
   THEN Auto
   THEN MemTypeCD
   THEN Auto
   THEN nRAdd ⌜π/2⌝ 0⋅
   THEN Auto) }

---

Latex:

---

Latex:
arcsin(r0)  =  r0


By

---

Latex:
((Assert  r0  <  \mpi{}/2  BY
                (D  0  With  \mkleeneopen{}3\mkleeneclose{}    THEN  Auto))
  THEN  BLemma  `arcsin-unique`
  THEN  Auto
  THEN  MemTypeCD
  THEN  Auto
  THEN  nRAdd  \mkleeneopen{}\mpi{}/2\mkleeneclose{}  0\mcdot{}
  THEN  Auto)

---

Home Index