---

Step * of Lemma arcsin1

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

1
1. r0 < π/2
⊢ -(π/2) ≤ π/2

---

Latex:

---

Latex:
arcsin(r1)  =  \mpi{}/2


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)

---

Home Index