---

Step * 1 1 1 1 of Lemma rsin-half-pi


1. rsin(π/2(slower))^2 = r1
⊢ (-(r1) 5) + 4 < rsin(π/2(slower)) 5
BY
{ ((Subst' rsin(π/2(slower)) 5 ~ 9 0 THENA Refine `computeAll` [])
   THEN (Subst' -(r1) 5 ~ -10 0 THENA Refine `computeAll` [])
   ) }

1
1. rsin(π/2(slower))^2 = r1
⊢ (-10) + 4 < 9

---

Latex:

---

Latex:

1.  rsin(\mpi{}/2(slower))\^{}2  =  r1
\mvdash{}  (-(r1)  5)  +  4  <  rsin(\mpi{}/2(slower))  5


By

---

Latex:
((Subst'  rsin(\mpi{}/2(slower))  5  \msim{}  9  0  THENA  Refine  `computeAll`  [])
  THEN  (Subst'  -(r1)  5  \msim{}  -10  0  THENA  Refine  `computeAll`  [])
  )

---

Home Index