---

Step * of Lemma rsin-strictly-increasing2

rsin(x) strictly-increasing for x ∈ [-(π/2), π/2]
BY
{ (InstLemma `rsin-strictly-increasing` []⋅
   THEN FLemma `strictly-increasing-on-closed-interval2` [-1]
   THEN Auto
   THEN RWW "rsin-halfpi rsin-rminus" 0
   THEN Auto
   THEN (InstLemma `rsin-bounds` [⌜x⌝]⋅ THENM Reduce -1)
   THEN Auto) }

---

Latex:

---

Latex:
rsin(x)  strictly-increasing  for  x  \mmember{}  [-(\mpi{}/2),  \mpi{}/2]


By

---

Latex:
(InstLemma  `rsin-strictly-increasing`  []\mcdot{}
  THEN  FLemma  `strictly-increasing-on-closed-interval2`  [-1]
  THEN  Auto
  THEN  RWW  "rsin-halfpi  rsin-rminus"  0
  THEN  Auto
  THEN  (InstLemma  `rsin-bounds`  [\mkleeneopen{}x\mkleeneclose{}]\mcdot{}  THENM  Reduce  -1)
  THEN  Auto)

---

Home Index