---

Step * 1 of Lemma rcos-nonpositive


1. x : {x:ℝ| x ∈ [π/2, π + π/2]} 
2. r0 ≤ rcos(x - π)
⊢ rcos(x) ≤ r0
BY
{ ((Assert x = ((x - π) + π) BY (nRNorm 0 THEN Auto)) THEN RepeatFor 2 ((RWO  "-1 rcos-shift-pi" 0 THEN Auto))) }

---

Latex:

---

Latex:

1.  x  :  \{x:\mBbbR{}|  x  \mmember{}  [\mpi{}/2,  \mpi{}  +  \mpi{}/2]\} 
2.  r0  \mleq{}  rcos(x  -  \mpi{})
\mvdash{}  rcos(x)  \mleq{}  r0


By

---

Latex:
((Assert  x  =  ((x  -  \mpi{})  +  \mpi{})  BY
                (nRNorm  0  THEN  Auto))
  THEN  RepeatFor  2  ((RWO    "-1  rcos-shift-pi"  0  THEN  Auto))
  )

---

Home Index